Make non-streaming LLVM and C backends streaming
[ghc.git] / compiler / typecheck / TcErrors.hs
1 {-# LANGUAGE CPP #-}
2 {-# LANGUAGE ScopedTypeVariables #-}
3 {-# LANGUAGE ViewPatterns #-}
4
5 module TcErrors(
6 reportUnsolved, reportAllUnsolved, warnAllUnsolved,
7 warnDefaulting,
8
9 solverDepthErrorTcS
10 ) where
11
12 #include "HsVersions.h"
13
14 import GhcPrelude
15
16 import TcRnTypes
17 import TcRnMonad
18 import TcMType
19 import TcUnify( occCheckForErrors, MetaTyVarUpdateResult(..) )
20 import TcEnv( tcInitTidyEnv )
21 import TcType
22 import RnUnbound ( unknownNameSuggestions )
23 import Type
24 import TyCoRep
25 import Unify ( tcMatchTys )
26 import Module
27 import FamInst
28 import FamInstEnv ( flattenTys )
29 import Inst
30 import InstEnv
31 import TyCon
32 import Class
33 import DataCon
34 import TcEvidence
35 import TcEvTerm
36 import HsExpr ( UnboundVar(..) )
37 import HsBinds ( PatSynBind(..) )
38 import Name
39 import RdrName ( lookupGlobalRdrEnv, lookupGRE_Name, GlobalRdrEnv
40 , mkRdrUnqual, isLocalGRE, greSrcSpan )
41 import PrelNames ( typeableClassName )
42 import Id
43 import Var
44 import VarSet
45 import VarEnv
46 import NameSet
47 import Bag
48 import ErrUtils ( ErrMsg, errDoc, pprLocErrMsg )
49 import BasicTypes
50 import ConLike ( ConLike(..))
51 import Util
52 import FastString
53 import Outputable
54 import SrcLoc
55 import DynFlags
56 import ListSetOps ( equivClasses )
57 import Maybes
58 import Pair
59 import qualified GHC.LanguageExtensions as LangExt
60 import FV ( fvVarList, unionFV )
61
62 import Control.Monad ( when )
63 import Data.Foldable ( toList )
64 import Data.List ( partition, mapAccumL, nub, sortBy, unfoldr )
65 import qualified Data.Set as Set
66
67 import {-# SOURCE #-} TcHoleErrors ( findValidHoleFits )
68
69 -- import Data.Semigroup ( Semigroup )
70 import qualified Data.Semigroup as Semigroup
71
72
73 {-
74 ************************************************************************
75 * *
76 \section{Errors and contexts}
77 * *
78 ************************************************************************
79
80 ToDo: for these error messages, should we note the location as coming
81 from the insts, or just whatever seems to be around in the monad just
82 now?
83
84 Note [Deferring coercion errors to runtime]
85 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
86 While developing, sometimes it is desirable to allow compilation to succeed even
87 if there are type errors in the code. Consider the following case:
88
89 module Main where
90
91 a :: Int
92 a = 'a'
93
94 main = print "b"
95
96 Even though `a` is ill-typed, it is not used in the end, so if all that we're
97 interested in is `main` it is handy to be able to ignore the problems in `a`.
98
99 Since we treat type equalities as evidence, this is relatively simple. Whenever
100 we run into a type mismatch in TcUnify, we normally just emit an error. But it
101 is always safe to defer the mismatch to the main constraint solver. If we do
102 that, `a` will get transformed into
103
104 co :: Int ~ Char
105 co = ...
106
107 a :: Int
108 a = 'a' `cast` co
109
110 The constraint solver would realize that `co` is an insoluble constraint, and
111 emit an error with `reportUnsolved`. But we can also replace the right-hand side
112 of `co` with `error "Deferred type error: Int ~ Char"`. This allows the program
113 to compile, and it will run fine unless we evaluate `a`. This is what
114 `deferErrorsToRuntime` does.
115
116 It does this by keeping track of which errors correspond to which coercion
117 in TcErrors. TcErrors.reportTidyWanteds does not print the errors
118 and does not fail if -fdefer-type-errors is on, so that we can continue
119 compilation. The errors are turned into warnings in `reportUnsolved`.
120 -}
121
122 -- | Report unsolved goals as errors or warnings. We may also turn some into
123 -- deferred run-time errors if `-fdefer-type-errors` is on.
124 reportUnsolved :: WantedConstraints -> TcM (Bag EvBind)
125 reportUnsolved wanted
126 = do { binds_var <- newTcEvBinds
127 ; defer_errors <- goptM Opt_DeferTypeErrors
128 ; warn_errors <- woptM Opt_WarnDeferredTypeErrors -- implement #10283
129 ; let type_errors | not defer_errors = TypeError
130 | warn_errors = TypeWarn (Reason Opt_WarnDeferredTypeErrors)
131 | otherwise = TypeDefer
132
133 ; defer_holes <- goptM Opt_DeferTypedHoles
134 ; warn_holes <- woptM Opt_WarnTypedHoles
135 ; let expr_holes | not defer_holes = HoleError
136 | warn_holes = HoleWarn
137 | otherwise = HoleDefer
138
139 ; partial_sigs <- xoptM LangExt.PartialTypeSignatures
140 ; warn_partial_sigs <- woptM Opt_WarnPartialTypeSignatures
141 ; let type_holes | not partial_sigs = HoleError
142 | warn_partial_sigs = HoleWarn
143 | otherwise = HoleDefer
144
145 ; defer_out_of_scope <- goptM Opt_DeferOutOfScopeVariables
146 ; warn_out_of_scope <- woptM Opt_WarnDeferredOutOfScopeVariables
147 ; let out_of_scope_holes | not defer_out_of_scope = HoleError
148 | warn_out_of_scope = HoleWarn
149 | otherwise = HoleDefer
150
151 ; report_unsolved type_errors expr_holes
152 type_holes out_of_scope_holes
153 binds_var wanted
154
155 ; ev_binds <- getTcEvBindsMap binds_var
156 ; return (evBindMapBinds ev_binds)}
157
158 -- | Report *all* unsolved goals as errors, even if -fdefer-type-errors is on
159 -- However, do not make any evidence bindings, because we don't
160 -- have any convenient place to put them.
161 -- NB: Type-level holes are OK, because there are no bindings.
162 -- See Note [Deferring coercion errors to runtime]
163 -- Used by solveEqualities for kind equalities
164 -- (see Note [Fail fast on kind errors] in TcSimplify)
165 -- and for simplifyDefault.
166 reportAllUnsolved :: WantedConstraints -> TcM ()
167 reportAllUnsolved wanted
168 = do { ev_binds <- newNoTcEvBinds
169
170 ; partial_sigs <- xoptM LangExt.PartialTypeSignatures
171 ; warn_partial_sigs <- woptM Opt_WarnPartialTypeSignatures
172 ; let type_holes | not partial_sigs = HoleError
173 | warn_partial_sigs = HoleWarn
174 | otherwise = HoleDefer
175
176 ; report_unsolved TypeError HoleError type_holes HoleError
177 ev_binds wanted }
178
179 -- | Report all unsolved goals as warnings (but without deferring any errors to
180 -- run-time). See Note [Safe Haskell Overlapping Instances Implementation] in
181 -- TcSimplify
182 warnAllUnsolved :: WantedConstraints -> TcM ()
183 warnAllUnsolved wanted
184 = do { ev_binds <- newTcEvBinds
185 ; report_unsolved (TypeWarn NoReason) HoleWarn HoleWarn HoleWarn
186 ev_binds wanted }
187
188 -- | Report unsolved goals as errors or warnings.
189 report_unsolved :: TypeErrorChoice -- Deferred type errors
190 -> HoleChoice -- Expression holes
191 -> HoleChoice -- Type holes
192 -> HoleChoice -- Out of scope holes
193 -> EvBindsVar -- cec_binds
194 -> WantedConstraints -> TcM ()
195 report_unsolved type_errors expr_holes
196 type_holes out_of_scope_holes binds_var wanted
197 | isEmptyWC wanted
198 = return ()
199 | otherwise
200 = do { traceTc "reportUnsolved {" $
201 vcat [ text "type errors:" <+> ppr type_errors
202 , text "expr holes:" <+> ppr expr_holes
203 , text "type holes:" <+> ppr type_holes
204 , text "scope holes:" <+> ppr out_of_scope_holes ]
205 ; traceTc "reportUnsolved (before zonking and tidying)" (ppr wanted)
206
207 ; wanted <- zonkWC wanted -- Zonk to reveal all information
208 ; env0 <- tcInitTidyEnv
209 -- If we are deferring we are going to need /all/ evidence around,
210 -- including the evidence produced by unflattening (zonkWC)
211 ; let tidy_env = tidyFreeTyCoVars env0 free_tvs
212 free_tvs = tyCoVarsOfWCList wanted
213
214 ; traceTc "reportUnsolved (after zonking):" $
215 vcat [ text "Free tyvars:" <+> pprTyVars free_tvs
216 , text "Tidy env:" <+> ppr tidy_env
217 , text "Wanted:" <+> ppr wanted ]
218
219 ; warn_redundant <- woptM Opt_WarnRedundantConstraints
220 ; let err_ctxt = CEC { cec_encl = []
221 , cec_tidy = tidy_env
222 , cec_defer_type_errors = type_errors
223 , cec_expr_holes = expr_holes
224 , cec_type_holes = type_holes
225 , cec_out_of_scope_holes = out_of_scope_holes
226 , cec_suppress = insolubleWC wanted
227 -- See Note [Suppressing error messages]
228 -- Suppress low-priority errors if there
229 -- are insolule errors anywhere;
230 -- See #15539 and c.f. setting ic_status
231 -- in TcSimplify.setImplicationStatus
232 , cec_warn_redundant = warn_redundant
233 , cec_binds = binds_var }
234
235 ; tc_lvl <- getTcLevel
236 ; reportWanteds err_ctxt tc_lvl wanted
237 ; traceTc "reportUnsolved }" empty }
238
239 --------------------------------------------
240 -- Internal functions
241 --------------------------------------------
242
243 -- | An error Report collects messages categorised by their importance.
244 -- See Note [Error report] for details.
245 data Report
246 = Report { report_important :: [SDoc]
247 , report_relevant_bindings :: [SDoc]
248 , report_valid_hole_fits :: [SDoc]
249 }
250
251 instance Outputable Report where -- Debugging only
252 ppr (Report { report_important = imp
253 , report_relevant_bindings = rel
254 , report_valid_hole_fits = val })
255 = vcat [ text "important:" <+> vcat imp
256 , text "relevant:" <+> vcat rel
257 , text "valid:" <+> vcat val ]
258
259 {- Note [Error report]
260 The idea is that error msgs are divided into three parts: the main msg, the
261 context block (\"In the second argument of ...\"), and the relevant bindings
262 block, which are displayed in that order, with a mark to divide them. The
263 idea is that the main msg ('report_important') varies depending on the error
264 in question, but context and relevant bindings are always the same, which
265 should simplify visual parsing.
266
267 The context is added when the Report is passed off to 'mkErrorReport'.
268 Unfortunately, unlike the context, the relevant bindings are added in
269 multiple places so they have to be in the Report.
270 -}
271
272 instance Semigroup Report where
273 Report a1 b1 c1 <> Report a2 b2 c2 = Report (a1 ++ a2) (b1 ++ b2) (c1 ++ c2)
274
275 instance Monoid Report where
276 mempty = Report [] [] []
277 mappend = (Semigroup.<>)
278
279 -- | Put a doc into the important msgs block.
280 important :: SDoc -> Report
281 important doc = mempty { report_important = [doc] }
282
283 -- | Put a doc into the relevant bindings block.
284 relevant_bindings :: SDoc -> Report
285 relevant_bindings doc = mempty { report_relevant_bindings = [doc] }
286
287 -- | Put a doc into the valid hole fits block.
288 valid_hole_fits :: SDoc -> Report
289 valid_hole_fits docs = mempty { report_valid_hole_fits = [docs] }
290
291 data TypeErrorChoice -- What to do for type errors found by the type checker
292 = TypeError -- A type error aborts compilation with an error message
293 | TypeWarn WarnReason
294 -- A type error is deferred to runtime, plus a compile-time warning
295 -- The WarnReason should usually be (Reason Opt_WarnDeferredTypeErrors)
296 -- but it isn't for the Safe Haskell Overlapping Instances warnings
297 -- see warnAllUnsolved
298 | TypeDefer -- A type error is deferred to runtime; no error or warning at compile time
299
300 data HoleChoice
301 = HoleError -- A hole is a compile-time error
302 | HoleWarn -- Defer to runtime, emit a compile-time warning
303 | HoleDefer -- Defer to runtime, no warning
304
305 instance Outputable HoleChoice where
306 ppr HoleError = text "HoleError"
307 ppr HoleWarn = text "HoleWarn"
308 ppr HoleDefer = text "HoleDefer"
309
310 instance Outputable TypeErrorChoice where
311 ppr TypeError = text "TypeError"
312 ppr (TypeWarn reason) = text "TypeWarn" <+> ppr reason
313 ppr TypeDefer = text "TypeDefer"
314
315 data ReportErrCtxt
316 = CEC { cec_encl :: [Implication] -- Enclosing implications
317 -- (innermost first)
318 -- ic_skols and givens are tidied, rest are not
319 , cec_tidy :: TidyEnv
320
321 , cec_binds :: EvBindsVar -- Make some errors (depending on cec_defer)
322 -- into warnings, and emit evidence bindings
323 -- into 'cec_binds' for unsolved constraints
324
325 , cec_defer_type_errors :: TypeErrorChoice -- Defer type errors until runtime
326
327 -- cec_expr_holes is a union of:
328 -- cec_type_holes - a set of typed holes: '_', '_a', '_foo'
329 -- cec_out_of_scope_holes - a set of variables which are
330 -- out of scope: 'x', 'y', 'bar'
331 , cec_expr_holes :: HoleChoice -- Holes in expressions
332 , cec_type_holes :: HoleChoice -- Holes in types
333 , cec_out_of_scope_holes :: HoleChoice -- Out of scope holes
334
335 , cec_warn_redundant :: Bool -- True <=> -Wredundant-constraints
336
337 , cec_suppress :: Bool -- True <=> More important errors have occurred,
338 -- so create bindings if need be, but
339 -- don't issue any more errors/warnings
340 -- See Note [Suppressing error messages]
341 }
342
343 instance Outputable ReportErrCtxt where
344 ppr (CEC { cec_binds = bvar
345 , cec_defer_type_errors = dte
346 , cec_expr_holes = eh
347 , cec_type_holes = th
348 , cec_out_of_scope_holes = osh
349 , cec_warn_redundant = wr
350 , cec_suppress = sup })
351 = text "CEC" <+> braces (vcat
352 [ text "cec_binds" <+> equals <+> ppr bvar
353 , text "cec_defer_type_errors" <+> equals <+> ppr dte
354 , text "cec_expr_holes" <+> equals <+> ppr eh
355 , text "cec_type_holes" <+> equals <+> ppr th
356 , text "cec_out_of_scope_holes" <+> equals <+> ppr osh
357 , text "cec_warn_redundant" <+> equals <+> ppr wr
358 , text "cec_suppress" <+> equals <+> ppr sup ])
359
360 -- | Returns True <=> the ReportErrCtxt indicates that something is deferred
361 deferringAnyBindings :: ReportErrCtxt -> Bool
362 -- Don't check cec_type_holes, as these don't cause bindings to be deferred
363 deferringAnyBindings (CEC { cec_defer_type_errors = TypeError
364 , cec_expr_holes = HoleError
365 , cec_out_of_scope_holes = HoleError }) = False
366 deferringAnyBindings _ = True
367
368 -- | Transforms a 'ReportErrCtxt' into one that does not defer any bindings
369 -- at all.
370 noDeferredBindings :: ReportErrCtxt -> ReportErrCtxt
371 noDeferredBindings ctxt = ctxt { cec_defer_type_errors = TypeError
372 , cec_expr_holes = HoleError
373 , cec_out_of_scope_holes = HoleError }
374
375 {- Note [Suppressing error messages]
376 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
377 The cec_suppress flag says "don't report any errors". Instead, just create
378 evidence bindings (as usual). It's used when more important errors have occurred.
379
380 Specifically (see reportWanteds)
381 * If there are insoluble Givens, then we are in unreachable code and all bets
382 are off. So don't report any further errors.
383 * If there are any insolubles (eg Int~Bool), here or in a nested implication,
384 then suppress errors from the simple constraints here. Sometimes the
385 simple-constraint errors are a knock-on effect of the insolubles.
386
387 This suppression behaviour is controlled by the Bool flag in
388 ReportErrorSpec, as used in reportWanteds.
389
390 But we need to take care: flags can turn errors into warnings, and we
391 don't want those warnings to suppress subsequent errors (including
392 suppressing the essential addTcEvBind for them: #15152). So in
393 tryReporter we use askNoErrs to see if any error messages were
394 /actually/ produced; if not, we don't switch on suppression.
395
396 A consequence is that warnings never suppress warnings, so turning an
397 error into a warning may allow subsequent warnings to appear that were
398 previously suppressed. (e.g. partial-sigs/should_fail/T14584)
399 -}
400
401 reportImplic :: ReportErrCtxt -> Implication -> TcM ()
402 reportImplic ctxt implic@(Implic { ic_skols = tvs, ic_telescope = m_telescope
403 , ic_given = given
404 , ic_wanted = wanted, ic_binds = evb
405 , ic_status = status, ic_info = info
406 , ic_tclvl = tc_lvl })
407 | BracketSkol <- info
408 , not insoluble
409 = return () -- For Template Haskell brackets report only
410 -- definite errors. The whole thing will be re-checked
411 -- later when we plug it in, and meanwhile there may
412 -- certainly be un-satisfied constraints
413
414 | otherwise
415 = do { traceTc "reportImplic" (ppr implic')
416 ; reportWanteds ctxt' tc_lvl wanted
417 ; when (cec_warn_redundant ctxt) $
418 warnRedundantConstraints ctxt' tcl_env info' dead_givens
419 ; when bad_telescope $ reportBadTelescope ctxt tcl_env m_telescope tvs }
420 where
421 tcl_env = implicLclEnv implic
422 insoluble = isInsolubleStatus status
423 (env1, tvs') = mapAccumL tidyVarBndr (cec_tidy ctxt) tvs
424 info' = tidySkolemInfo env1 info
425 implic' = implic { ic_skols = tvs'
426 , ic_given = map (tidyEvVar env1) given
427 , ic_info = info' }
428 ctxt1 | CoEvBindsVar{} <- evb = noDeferredBindings ctxt
429 | otherwise = ctxt
430 -- If we go inside an implication that has no term
431 -- evidence (e.g. unifying under a forall), we can't defer
432 -- type errors. You could imagine using the /enclosing/
433 -- bindings (in cec_binds), but that may not have enough stuff
434 -- in scope for the bindings to be well typed. So we just
435 -- switch off deferred type errors altogether. See #14605.
436
437 ctxt' = ctxt1 { cec_tidy = env1
438 , cec_encl = implic' : cec_encl ctxt
439
440 , cec_suppress = insoluble || cec_suppress ctxt
441 -- Suppress inessential errors if there
442 -- are insolubles anywhere in the
443 -- tree rooted here, or we've come across
444 -- a suppress-worthy constraint higher up (#11541)
445
446 , cec_binds = evb }
447
448 dead_givens = case status of
449 IC_Solved { ics_dead = dead } -> dead
450 _ -> []
451
452 bad_telescope = case status of
453 IC_BadTelescope -> True
454 _ -> False
455
456 warnRedundantConstraints :: ReportErrCtxt -> TcLclEnv -> SkolemInfo -> [EvVar] -> TcM ()
457 -- See Note [Tracking redundant constraints] in TcSimplify
458 warnRedundantConstraints ctxt env info ev_vars
459 | null redundant_evs
460 = return ()
461
462 | SigSkol {} <- info
463 = setLclEnv env $ -- We want to add "In the type signature for f"
464 -- to the error context, which is a bit tiresome
465 addErrCtxt (text "In" <+> ppr info) $
466 do { env <- getLclEnv
467 ; msg <- mkErrorReport ctxt env (important doc)
468 ; reportWarning (Reason Opt_WarnRedundantConstraints) msg }
469
470 | otherwise -- But for InstSkol there already *is* a surrounding
471 -- "In the instance declaration for Eq [a]" context
472 -- and we don't want to say it twice. Seems a bit ad-hoc
473 = do { msg <- mkErrorReport ctxt env (important doc)
474 ; reportWarning (Reason Opt_WarnRedundantConstraints) msg }
475 where
476 doc = text "Redundant constraint" <> plural redundant_evs <> colon
477 <+> pprEvVarTheta redundant_evs
478
479 redundant_evs =
480 filterOut is_type_error $
481 case info of -- See Note [Redundant constraints in instance decls]
482 InstSkol -> filterOut (improving . idType) ev_vars
483 _ -> ev_vars
484
485 -- See #15232
486 is_type_error = isJust . userTypeError_maybe . idType
487
488 improving pred -- (transSuperClasses p) does not include p
489 = any isImprovementPred (pred : transSuperClasses pred)
490
491 reportBadTelescope :: ReportErrCtxt -> TcLclEnv -> Maybe SDoc -> [TcTyVar] -> TcM ()
492 reportBadTelescope ctxt env (Just telescope) skols
493 = do { msg <- mkErrorReport ctxt env (important doc)
494 ; reportError msg }
495 where
496 doc = hang (text "These kind and type variables:" <+> telescope $$
497 text "are out of dependency order. Perhaps try this ordering:")
498 2 (pprTyVars sorted_tvs)
499
500 sorted_tvs = scopedSort skols
501
502 reportBadTelescope _ _ Nothing skols
503 = pprPanic "reportBadTelescope" (ppr skols)
504
505 {- Note [Redundant constraints in instance decls]
506 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
507 For instance declarations, we don't report unused givens if
508 they can give rise to improvement. Example (#10100):
509 class Add a b ab | a b -> ab, a ab -> b
510 instance Add Zero b b
511 instance Add a b ab => Add (Succ a) b (Succ ab)
512 The context (Add a b ab) for the instance is clearly unused in terms
513 of evidence, since the dictionary has no fields. But it is still
514 needed! With the context, a wanted constraint
515 Add (Succ Zero) beta (Succ Zero)
516 we will reduce to (Add Zero beta Zero), and thence we get beta := Zero.
517 But without the context we won't find beta := Zero.
518
519 This only matters in instance declarations..
520 -}
521
522 reportWanteds :: ReportErrCtxt -> TcLevel -> WantedConstraints -> TcM ()
523 reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_impl = implics })
524 = do { traceTc "reportWanteds" (vcat [ text "Simples =" <+> ppr simples
525 , text "Suppress =" <+> ppr (cec_suppress ctxt)])
526 ; traceTc "rw2" (ppr tidy_cts)
527
528 -- First deal with things that are utterly wrong
529 -- Like Int ~ Bool (incl nullary TyCons)
530 -- or Int ~ t a (AppTy on one side)
531 -- These /ones/ are not suppressed by the incoming context
532 ; let ctxt_for_insols = ctxt { cec_suppress = False }
533 ; (ctxt1, cts1) <- tryReporters ctxt_for_insols report1 tidy_cts
534
535 -- Now all the other constraints. We suppress errors here if
536 -- any of the first batch failed, or if the enclosing context
537 -- says to suppress
538 ; let ctxt2 = ctxt { cec_suppress = cec_suppress ctxt || cec_suppress ctxt1 }
539 ; (_, leftovers) <- tryReporters ctxt2 report2 cts1
540 ; MASSERT2( null leftovers, ppr leftovers )
541
542 -- All the Derived ones have been filtered out of simples
543 -- by the constraint solver. This is ok; we don't want
544 -- to report unsolved Derived goals as errors
545 -- See Note [Do not report derived but soluble errors]
546
547 ; mapBagM_ (reportImplic ctxt2) implics }
548 -- NB ctxt1: don't suppress inner insolubles if there's only a
549 -- wanted insoluble here; but do suppress inner insolubles
550 -- if there's a *given* insoluble here (= inaccessible code)
551 where
552 env = cec_tidy ctxt
553 tidy_cts = bagToList (mapBag (tidyCt env) simples)
554
555 -- report1: ones that should *not* be suppresed by
556 -- an insoluble somewhere else in the tree
557 -- It's crucial that anything that is considered insoluble
558 -- (see TcRnTypes.insolubleCt) is caught here, otherwise
559 -- we might suppress its error message, and proceed on past
560 -- type checking to get a Lint error later
561 report1 = [ ("Out of scope", is_out_of_scope, True, mkHoleReporter tidy_cts)
562 , ("Holes", is_hole, False, mkHoleReporter tidy_cts)
563 , ("custom_error", is_user_type_error, True, mkUserTypeErrorReporter)
564
565 , given_eq_spec
566 , ("insoluble2", utterly_wrong, True, mkGroupReporter mkEqErr)
567 , ("skolem eq1", very_wrong, True, mkSkolReporter)
568 , ("skolem eq2", skolem_eq, True, mkSkolReporter)
569 , ("non-tv eq", non_tv_eq, True, mkSkolReporter)
570
571 -- The only remaining equalities are alpha ~ ty,
572 -- where alpha is untouchable; and representational equalities
573 -- Prefer homogeneous equalities over hetero, because the
574 -- former might be holding up the latter.
575 -- See Note [Equalities with incompatible kinds] in TcCanonical
576 , ("Homo eqs", is_homo_equality, True, mkGroupReporter mkEqErr)
577 , ("Other eqs", is_equality, False, mkGroupReporter mkEqErr) ]
578
579 -- report2: we suppress these if there are insolubles elsewhere in the tree
580 report2 = [ ("Implicit params", is_ip, False, mkGroupReporter mkIPErr)
581 , ("Irreds", is_irred, False, mkGroupReporter mkIrredErr)
582 , ("Dicts", is_dict, False, mkGroupReporter mkDictErr) ]
583
584 -- rigid_nom_eq, rigid_nom_tv_eq,
585 is_hole, is_dict,
586 is_equality, is_ip, is_irred :: Ct -> PredTree -> Bool
587
588 is_given_eq ct pred
589 | EqPred {} <- pred = arisesFromGivens ct
590 | otherwise = False
591 -- I think all given residuals are equalities
592
593 -- Things like (Int ~N Bool)
594 utterly_wrong _ (EqPred NomEq ty1 ty2) = isRigidTy ty1 && isRigidTy ty2
595 utterly_wrong _ _ = False
596
597 -- Things like (a ~N Int)
598 very_wrong _ (EqPred NomEq ty1 ty2) = isSkolemTy tc_lvl ty1 && isRigidTy ty2
599 very_wrong _ _ = False
600
601 -- Things like (a ~N b) or (a ~N F Bool)
602 skolem_eq _ (EqPred NomEq ty1 _) = isSkolemTy tc_lvl ty1
603 skolem_eq _ _ = False
604
605 -- Things like (F a ~N Int)
606 non_tv_eq _ (EqPred NomEq ty1 _) = not (isTyVarTy ty1)
607 non_tv_eq _ _ = False
608
609 is_out_of_scope ct _ = isOutOfScopeCt ct
610 is_hole ct _ = isHoleCt ct
611
612 is_user_type_error ct _ = isUserTypeErrorCt ct
613
614 is_homo_equality _ (EqPred _ ty1 ty2) = tcTypeKind ty1 `tcEqType` tcTypeKind ty2
615 is_homo_equality _ _ = False
616
617 is_equality _ (EqPred {}) = True
618 is_equality _ _ = False
619
620 is_dict _ (ClassPred {}) = True
621 is_dict _ _ = False
622
623 is_ip _ (ClassPred cls _) = isIPClass cls
624 is_ip _ _ = False
625
626 is_irred _ (IrredPred {}) = True
627 is_irred _ _ = False
628
629 given_eq_spec -- See Note [Given errors]
630 | has_gadt_match (cec_encl ctxt)
631 = ("insoluble1a", is_given_eq, True, mkGivenErrorReporter)
632 | otherwise
633 = ("insoluble1b", is_given_eq, False, ignoreErrorReporter)
634 -- False means don't suppress subsequent errors
635 -- Reason: we don't report all given errors
636 -- (see mkGivenErrorReporter), and we should only suppress
637 -- subsequent errors if we actually report this one!
638 -- #13446 is an example
639
640 -- See Note [Given errors]
641 has_gadt_match [] = False
642 has_gadt_match (implic : implics)
643 | PatSkol {} <- ic_info implic
644 , not (ic_no_eqs implic)
645 , wopt Opt_WarnInaccessibleCode (implicDynFlags implic)
646 -- Don't bother doing this if -Winaccessible-code isn't enabled.
647 -- See Note [Avoid -Winaccessible-code when deriving] in TcInstDcls.
648 = True
649 | otherwise
650 = has_gadt_match implics
651
652 ---------------
653 isSkolemTy :: TcLevel -> Type -> Bool
654 -- The type is a skolem tyvar
655 isSkolemTy tc_lvl ty
656 | Just tv <- getTyVar_maybe ty
657 = isSkolemTyVar tv
658 || (isTyVarTyVar tv && isTouchableMetaTyVar tc_lvl tv)
659 -- The last case is for touchable TyVarTvs
660 -- we postpone untouchables to a latter test (too obscure)
661
662 | otherwise
663 = False
664
665 isTyFun_maybe :: Type -> Maybe TyCon
666 isTyFun_maybe ty = case tcSplitTyConApp_maybe ty of
667 Just (tc,_) | isTypeFamilyTyCon tc -> Just tc
668 _ -> Nothing
669
670 --------------------------------------------
671 -- Reporters
672 --------------------------------------------
673
674 type Reporter
675 = ReportErrCtxt -> [Ct] -> TcM ()
676 type ReporterSpec
677 = ( String -- Name
678 , Ct -> PredTree -> Bool -- Pick these ones
679 , Bool -- True <=> suppress subsequent reporters
680 , Reporter) -- The reporter itself
681
682 mkSkolReporter :: Reporter
683 -- Suppress duplicates with either the same LHS, or same location
684 mkSkolReporter ctxt cts
685 = mapM_ (reportGroup mkEqErr ctxt) (group cts)
686 where
687 group [] = []
688 group (ct:cts) = (ct : yeses) : group noes
689 where
690 (yeses, noes) = partition (group_with ct) cts
691
692 group_with ct1 ct2
693 | EQ <- cmp_loc ct1 ct2 = True
694 | eq_lhs_type ct1 ct2 = True
695 | otherwise = False
696
697 mkHoleReporter :: [Ct] -> Reporter
698 -- Reports errors one at a time
699 mkHoleReporter tidy_simples ctxt
700 = mapM_ $ \ct -> do { err <- mkHoleError tidy_simples ctxt ct
701 ; maybeReportHoleError ctxt ct err
702 ; maybeAddDeferredHoleBinding ctxt err ct }
703
704 mkUserTypeErrorReporter :: Reporter
705 mkUserTypeErrorReporter ctxt
706 = mapM_ $ \ct -> do { err <- mkUserTypeError ctxt ct
707 ; maybeReportError ctxt err
708 ; addDeferredBinding ctxt err ct }
709
710 mkUserTypeError :: ReportErrCtxt -> Ct -> TcM ErrMsg
711 mkUserTypeError ctxt ct = mkErrorMsgFromCt ctxt ct
712 $ important
713 $ pprUserTypeErrorTy
714 $ case getUserTypeErrorMsg ct of
715 Just msg -> msg
716 Nothing -> pprPanic "mkUserTypeError" (ppr ct)
717
718
719 mkGivenErrorReporter :: Reporter
720 -- See Note [Given errors]
721 mkGivenErrorReporter ctxt cts
722 = do { (ctxt, binds_msg, ct) <- relevantBindings True ctxt ct
723 ; dflags <- getDynFlags
724 ; let (implic:_) = cec_encl ctxt
725 -- Always non-empty when mkGivenErrorReporter is called
726 ct' = setCtLoc ct (setCtLocEnv (ctLoc ct) (implicLclEnv implic))
727 -- For given constraints we overwrite the env (and hence src-loc)
728 -- with one from the immediately-enclosing implication.
729 -- See Note [Inaccessible code]
730
731 inaccessible_msg = hang (text "Inaccessible code in")
732 2 (ppr (ic_info implic))
733 report = important inaccessible_msg `mappend`
734 relevant_bindings binds_msg
735
736 ; err <- mkEqErr_help dflags ctxt report ct'
737 Nothing ty1 ty2
738
739 ; traceTc "mkGivenErrorReporter" (ppr ct)
740 ; reportWarning (Reason Opt_WarnInaccessibleCode) err }
741 where
742 (ct : _ ) = cts -- Never empty
743 (ty1, ty2) = getEqPredTys (ctPred ct)
744
745 ignoreErrorReporter :: Reporter
746 -- Discard Given errors that don't come from
747 -- a pattern match; maybe we should warn instead?
748 ignoreErrorReporter ctxt cts
749 = do { traceTc "mkGivenErrorReporter no" (ppr cts $$ ppr (cec_encl ctxt))
750 ; return () }
751
752
753 {- Note [Given errors]
754 ~~~~~~~~~~~~~~~~~~~~~~
755 Given constraints represent things for which we have (or will have)
756 evidence, so they aren't errors. But if a Given constraint is
757 insoluble, this code is inaccessible, and we might want to at least
758 warn about that. A classic case is
759
760 data T a where
761 T1 :: T Int
762 T2 :: T a
763 T3 :: T Bool
764
765 f :: T Int -> Bool
766 f T1 = ...
767 f T2 = ...
768 f T3 = ... -- We want to report this case as inaccessible
769
770 We'd like to point out that the T3 match is inaccessible. It
771 will have a Given constraint [G] Int ~ Bool.
772
773 But we don't want to report ALL insoluble Given constraints. See Trac
774 #12466 for a long discussion. For example, if we aren't careful
775 we'll complain about
776 f :: ((Int ~ Bool) => a -> a) -> Int
777 which arguably is OK. It's more debatable for
778 g :: (Int ~ Bool) => Int -> Int
779 but it's tricky to distinguish these cases so we don't report
780 either.
781
782 The bottom line is this: has_gadt_match looks for an enclosing
783 pattern match which binds some equality constraints. If we
784 find one, we report the insoluble Given.
785 -}
786
787 mkGroupReporter :: (ReportErrCtxt -> [Ct] -> TcM ErrMsg)
788 -- Make error message for a group
789 -> Reporter -- Deal with lots of constraints
790 -- Group together errors from same location,
791 -- and report only the first (to avoid a cascade)
792 mkGroupReporter mk_err ctxt cts
793 = mapM_ (reportGroup mk_err ctxt . toList) (equivClasses cmp_loc cts)
794
795 eq_lhs_type :: Ct -> Ct -> Bool
796 eq_lhs_type ct1 ct2
797 = case (classifyPredType (ctPred ct1), classifyPredType (ctPred ct2)) of
798 (EqPred eq_rel1 ty1 _, EqPred eq_rel2 ty2 _) ->
799 (eq_rel1 == eq_rel2) && (ty1 `eqType` ty2)
800 _ -> pprPanic "mkSkolReporter" (ppr ct1 $$ ppr ct2)
801
802 cmp_loc :: Ct -> Ct -> Ordering
803 cmp_loc ct1 ct2 = ctLocSpan (ctLoc ct1) `compare` ctLocSpan (ctLoc ct2)
804
805 reportGroup :: (ReportErrCtxt -> [Ct] -> TcM ErrMsg) -> ReportErrCtxt
806 -> [Ct] -> TcM ()
807 reportGroup mk_err ctxt cts =
808 case partition isMonadFailInstanceMissing cts of
809 -- Only warn about missing MonadFail constraint when
810 -- there are no other missing constraints!
811 (monadFailCts, []) ->
812 do { err <- mk_err ctxt monadFailCts
813 ; reportWarning (Reason Opt_WarnMissingMonadFailInstances) err }
814
815 (_, cts') -> do { err <- mk_err ctxt cts'
816 ; traceTc "About to maybeReportErr" $
817 vcat [ text "Constraint:" <+> ppr cts'
818 , text "cec_suppress =" <+> ppr (cec_suppress ctxt)
819 , text "cec_defer_type_errors =" <+> ppr (cec_defer_type_errors ctxt) ]
820 ; maybeReportError ctxt err
821 -- But see Note [Always warn with -fdefer-type-errors]
822 ; traceTc "reportGroup" (ppr cts')
823 ; mapM_ (addDeferredBinding ctxt err) cts' }
824 -- Add deferred bindings for all
825 -- Redundant if we are going to abort compilation,
826 -- but that's hard to know for sure, and if we don't
827 -- abort, we need bindings for all (e.g. #12156)
828 where
829 isMonadFailInstanceMissing ct =
830 case ctLocOrigin (ctLoc ct) of
831 FailablePattern _pat -> True
832 _otherwise -> False
833
834 maybeReportHoleError :: ReportErrCtxt -> Ct -> ErrMsg -> TcM ()
835 -- Unlike maybeReportError, these "hole" errors are
836 -- /not/ suppressed by cec_suppress. We want to see them!
837 maybeReportHoleError ctxt ct err
838 -- When -XPartialTypeSignatures is on, warnings (instead of errors) are
839 -- generated for holes in partial type signatures.
840 -- Unless -fwarn-partial-type-signatures is not on,
841 -- in which case the messages are discarded.
842 | isTypeHoleCt ct
843 = -- For partial type signatures, generate warnings only, and do that
844 -- only if -fwarn-partial-type-signatures is on
845 case cec_type_holes ctxt of
846 HoleError -> reportError err
847 HoleWarn -> reportWarning (Reason Opt_WarnPartialTypeSignatures) err
848 HoleDefer -> return ()
849
850 -- Always report an error for out-of-scope variables
851 -- Unless -fdefer-out-of-scope-variables is on,
852 -- in which case the messages are discarded.
853 -- See #12170, #12406
854 | isOutOfScopeCt ct
855 = -- If deferring, report a warning only if -Wout-of-scope-variables is on
856 case cec_out_of_scope_holes ctxt of
857 HoleError -> reportError err
858 HoleWarn ->
859 reportWarning (Reason Opt_WarnDeferredOutOfScopeVariables) err
860 HoleDefer -> return ()
861
862 -- Otherwise this is a typed hole in an expression,
863 -- but not for an out-of-scope variable
864 | otherwise
865 = -- If deferring, report a warning only if -Wtyped-holes is on
866 case cec_expr_holes ctxt of
867 HoleError -> reportError err
868 HoleWarn -> reportWarning (Reason Opt_WarnTypedHoles) err
869 HoleDefer -> return ()
870
871 maybeReportError :: ReportErrCtxt -> ErrMsg -> TcM ()
872 -- Report the error and/or make a deferred binding for it
873 maybeReportError ctxt err
874 | cec_suppress ctxt -- Some worse error has occurred;
875 = return () -- so suppress this error/warning
876
877 | otherwise
878 = case cec_defer_type_errors ctxt of
879 TypeDefer -> return ()
880 TypeWarn reason -> reportWarning reason err
881 TypeError -> reportError err
882
883 addDeferredBinding :: ReportErrCtxt -> ErrMsg -> Ct -> TcM ()
884 -- See Note [Deferring coercion errors to runtime]
885 addDeferredBinding ctxt err ct
886 | deferringAnyBindings ctxt
887 , CtWanted { ctev_pred = pred, ctev_dest = dest } <- ctEvidence ct
888 -- Only add deferred bindings for Wanted constraints
889 = do { dflags <- getDynFlags
890 ; let err_msg = pprLocErrMsg err
891 err_fs = mkFastString $ showSDoc dflags $
892 err_msg $$ text "(deferred type error)"
893 err_tm = evDelayedError pred err_fs
894 ev_binds_var = cec_binds ctxt
895
896 ; case dest of
897 EvVarDest evar
898 -> addTcEvBind ev_binds_var $ mkWantedEvBind evar err_tm
899 HoleDest hole
900 -> do { -- See Note [Deferred errors for coercion holes]
901 let co_var = coHoleCoVar hole
902 ; addTcEvBind ev_binds_var $ mkWantedEvBind co_var err_tm
903 ; fillCoercionHole hole (mkTcCoVarCo co_var) }}
904
905 | otherwise -- Do not set any evidence for Given/Derived
906 = return ()
907
908 maybeAddDeferredHoleBinding :: ReportErrCtxt -> ErrMsg -> Ct -> TcM ()
909 maybeAddDeferredHoleBinding ctxt err ct
910 | isExprHoleCt ct
911 = addDeferredBinding ctxt err ct -- Only add bindings for holes in expressions
912 | otherwise -- not for holes in partial type signatures
913 = return ()
914
915 tryReporters :: ReportErrCtxt -> [ReporterSpec] -> [Ct] -> TcM (ReportErrCtxt, [Ct])
916 -- Use the first reporter in the list whose predicate says True
917 tryReporters ctxt reporters cts
918 = do { let (vis_cts, invis_cts) = partition (isVisibleOrigin . ctOrigin) cts
919 ; traceTc "tryReporters {" (ppr vis_cts $$ ppr invis_cts)
920 ; (ctxt', cts') <- go ctxt reporters vis_cts invis_cts
921 ; traceTc "tryReporters }" (ppr cts')
922 ; return (ctxt', cts') }
923 where
924 go ctxt [] vis_cts invis_cts
925 = return (ctxt, vis_cts ++ invis_cts)
926
927 go ctxt (r : rs) vis_cts invis_cts
928 -- always look at *visible* Origins before invisible ones
929 -- this is the whole point of isVisibleOrigin
930 = do { (ctxt', vis_cts') <- tryReporter ctxt r vis_cts
931 ; (ctxt'', invis_cts') <- tryReporter ctxt' r invis_cts
932 ; go ctxt'' rs vis_cts' invis_cts' }
933 -- Carry on with the rest, because we must make
934 -- deferred bindings for them if we have -fdefer-type-errors
935 -- But suppress their error messages
936
937 tryReporter :: ReportErrCtxt -> ReporterSpec -> [Ct] -> TcM (ReportErrCtxt, [Ct])
938 tryReporter ctxt (str, keep_me, suppress_after, reporter) cts
939 | null yeses
940 = return (ctxt, cts)
941 | otherwise
942 = do { traceTc "tryReporter{ " (text str <+> ppr yeses)
943 ; (_, no_errs) <- askNoErrs (reporter ctxt yeses)
944 ; let suppress_now = not no_errs && suppress_after
945 -- See Note [Suppressing error messages]
946 ctxt' = ctxt { cec_suppress = suppress_now || cec_suppress ctxt }
947 ; traceTc "tryReporter end }" (text str <+> ppr (cec_suppress ctxt) <+> ppr suppress_after)
948 ; return (ctxt', nos) }
949 where
950 (yeses, nos) = partition (\ct -> keep_me ct (classifyPredType (ctPred ct))) cts
951
952
953 pprArising :: CtOrigin -> SDoc
954 -- Used for the main, top-level error message
955 -- We've done special processing for TypeEq, KindEq, Given
956 pprArising (TypeEqOrigin {}) = empty
957 pprArising (KindEqOrigin {}) = empty
958 pprArising (GivenOrigin {}) = empty
959 pprArising orig = pprCtOrigin orig
960
961 -- Add the "arising from..." part to a message about bunch of dicts
962 addArising :: CtOrigin -> SDoc -> SDoc
963 addArising orig msg = hang msg 2 (pprArising orig)
964
965 pprWithArising :: [Ct] -> (CtLoc, SDoc)
966 -- Print something like
967 -- (Eq a) arising from a use of x at y
968 -- (Show a) arising from a use of p at q
969 -- Also return a location for the error message
970 -- Works for Wanted/Derived only
971 pprWithArising []
972 = panic "pprWithArising"
973 pprWithArising (ct:cts)
974 | null cts
975 = (loc, addArising (ctLocOrigin loc)
976 (pprTheta [ctPred ct]))
977 | otherwise
978 = (loc, vcat (map ppr_one (ct:cts)))
979 where
980 loc = ctLoc ct
981 ppr_one ct' = hang (parens (pprType (ctPred ct')))
982 2 (pprCtLoc (ctLoc ct'))
983
984 mkErrorMsgFromCt :: ReportErrCtxt -> Ct -> Report -> TcM ErrMsg
985 mkErrorMsgFromCt ctxt ct report
986 = mkErrorReport ctxt (ctLocEnv (ctLoc ct)) report
987
988 mkErrorReport :: ReportErrCtxt -> TcLclEnv -> Report -> TcM ErrMsg
989 mkErrorReport ctxt tcl_env (Report important relevant_bindings valid_subs)
990 = do { context <- mkErrInfo (cec_tidy ctxt) (tcl_ctxt tcl_env)
991 ; mkErrDocAt (RealSrcSpan (tcl_loc tcl_env))
992 (errDoc important [context] (relevant_bindings ++ valid_subs))
993 }
994
995 type UserGiven = Implication
996
997 getUserGivens :: ReportErrCtxt -> [UserGiven]
998 -- One item for each enclosing implication
999 getUserGivens (CEC {cec_encl = implics}) = getUserGivensFromImplics implics
1000
1001 getUserGivensFromImplics :: [Implication] -> [UserGiven]
1002 getUserGivensFromImplics implics
1003 = reverse (filterOut (null . ic_given) implics)
1004
1005 {- Note [Always warn with -fdefer-type-errors]
1006 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1007 When -fdefer-type-errors is on we warn about *all* type errors, even
1008 if cec_suppress is on. This can lead to a lot more warnings than you
1009 would get errors without -fdefer-type-errors, but if we suppress any of
1010 them you might get a runtime error that wasn't warned about at compile
1011 time.
1012
1013 This is an easy design choice to change; just flip the order of the
1014 first two equations for maybeReportError
1015
1016 To be consistent, we should also report multiple warnings from a single
1017 location in mkGroupReporter, when -fdefer-type-errors is on. But that
1018 is perhaps a bit *over*-consistent! Again, an easy choice to change.
1019
1020 With #10283, you can now opt out of deferred type error warnings.
1021
1022 Note [Deferred errors for coercion holes]
1023 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1024 Suppose we need to defer a type error where the destination for the evidence
1025 is a coercion hole. We can't just put the error in the hole, because we can't
1026 make an erroneous coercion. (Remember that coercions are erased for runtime.)
1027 Instead, we invent a new EvVar, bind it to an error and then make a coercion
1028 from that EvVar, filling the hole with that coercion. Because coercions'
1029 types are unlifted, the error is guaranteed to be hit before we get to the
1030 coercion.
1031
1032 Note [Do not report derived but soluble errors]
1033 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1034 The wc_simples include Derived constraints that have not been solved,
1035 but are not insoluble (in that case they'd be reported by 'report1').
1036 We do not want to report these as errors:
1037
1038 * Superclass constraints. If we have an unsolved [W] Ord a, we'll also have
1039 an unsolved [D] Eq a, and we do not want to report that; it's just noise.
1040
1041 * Functional dependencies. For givens, consider
1042 class C a b | a -> b
1043 data T a where
1044 MkT :: C a d => [d] -> T a
1045 f :: C a b => T a -> F Int
1046 f (MkT xs) = length xs
1047 Then we get a [D] b~d. But there *is* a legitimate call to
1048 f, namely f (MkT [True]) :: T Bool, in which b=d. So we should
1049 not reject the program.
1050
1051 For wanteds, something similar
1052 data T a where
1053 MkT :: C Int b => a -> b -> T a
1054 g :: C Int c => c -> ()
1055 f :: T a -> ()
1056 f (MkT x y) = g x
1057 Here we get [G] C Int b, [W] C Int a, hence [D] a~b.
1058 But again f (MkT True True) is a legitimate call.
1059
1060 (We leave the Deriveds in wc_simple until reportErrors, so that we don't lose
1061 derived superclasses between iterations of the solver.)
1062
1063 For functional dependencies, here is a real example,
1064 stripped off from libraries/utf8-string/Codec/Binary/UTF8/Generic.hs
1065
1066 class C a b | a -> b
1067 g :: C a b => a -> b -> ()
1068 f :: C a b => a -> b -> ()
1069 f xa xb =
1070 let loop = g xa
1071 in loop xb
1072
1073 We will first try to infer a type for loop, and we will succeed:
1074 C a b' => b' -> ()
1075 Subsequently, we will type check (loop xb) and all is good. But,
1076 recall that we have to solve a final implication constraint:
1077 C a b => (C a b' => .... cts from body of loop .... ))
1078 And now we have a problem as we will generate an equality b ~ b' and fail to
1079 solve it.
1080
1081
1082 ************************************************************************
1083 * *
1084 Irreducible predicate errors
1085 * *
1086 ************************************************************************
1087 -}
1088
1089 mkIrredErr :: ReportErrCtxt -> [Ct] -> TcM ErrMsg
1090 mkIrredErr ctxt cts
1091 = do { (ctxt, binds_msg, ct1) <- relevantBindings True ctxt ct1
1092 ; let orig = ctOrigin ct1
1093 msg = couldNotDeduce (getUserGivens ctxt) (map ctPred cts, orig)
1094 ; mkErrorMsgFromCt ctxt ct1 $
1095 important msg `mappend` relevant_bindings binds_msg }
1096 where
1097 (ct1:_) = cts
1098
1099 ----------------
1100 mkHoleError :: [Ct] -> ReportErrCtxt -> Ct -> TcM ErrMsg
1101 mkHoleError _ _ ct@(CHoleCan { cc_hole = ExprHole (OutOfScope occ rdr_env0) })
1102 -- Out-of-scope variables, like 'a', where 'a' isn't bound; suggest possible
1103 -- in-scope variables in the message, and note inaccessible exact matches
1104 = do { dflags <- getDynFlags
1105 ; imp_info <- getImports
1106 ; curr_mod <- getModule
1107 ; hpt <- getHpt
1108 ; let suggs_msg = unknownNameSuggestions dflags hpt curr_mod rdr_env0
1109 (tcl_rdr lcl_env) imp_info rdr
1110 ; rdr_env <- getGlobalRdrEnv
1111 ; splice_locs <- getTopLevelSpliceLocs
1112 ; let match_msgs = mk_match_msgs rdr_env splice_locs
1113 ; mkErrDocAt (RealSrcSpan err_loc) $
1114 errDoc [out_of_scope_msg] [] (match_msgs ++ [suggs_msg]) }
1115
1116 where
1117 rdr = mkRdrUnqual occ
1118 ct_loc = ctLoc ct
1119 lcl_env = ctLocEnv ct_loc
1120 err_loc = tcl_loc lcl_env
1121 hole_ty = ctEvPred (ctEvidence ct)
1122 boring_type = isTyVarTy hole_ty
1123
1124 out_of_scope_msg -- Print v :: ty only if the type has structure
1125 | boring_type = hang herald 2 (ppr occ)
1126 | otherwise = hang herald 2 (pp_with_type occ hole_ty)
1127
1128 herald | isDataOcc occ = text "Data constructor not in scope:"
1129 | otherwise = text "Variable not in scope:"
1130
1131 -- Indicate if the out-of-scope variable exactly (and unambiguously) matches
1132 -- a top-level binding in a later inter-splice group; see Note [OutOfScope
1133 -- exact matches]
1134 mk_match_msgs rdr_env splice_locs
1135 = let gres = filter isLocalGRE (lookupGlobalRdrEnv rdr_env occ)
1136 in case gres of
1137 [gre]
1138 | RealSrcSpan bind_loc <- greSrcSpan gre
1139 -- Find splice between the unbound variable and the match; use
1140 -- lookupLE, not lookupLT, since match could be in the splice
1141 , Just th_loc <- Set.lookupLE bind_loc splice_locs
1142 , err_loc < th_loc
1143 -> [mk_bind_scope_msg bind_loc th_loc]
1144 _ -> []
1145
1146 mk_bind_scope_msg bind_loc th_loc
1147 | is_th_bind
1148 = hang (quotes (ppr occ) <+> parens (text "splice on" <+> th_rng))
1149 2 (text "is not in scope before line" <+> int th_start_ln)
1150 | otherwise
1151 = hang (quotes (ppr occ) <+> bind_rng <+> text "is not in scope")
1152 2 (text "before the splice on" <+> th_rng)
1153 where
1154 bind_rng = parens (text "line" <+> int bind_ln)
1155 th_rng
1156 | th_start_ln == th_end_ln = single
1157 | otherwise = multi
1158 single = text "line" <+> int th_start_ln
1159 multi = text "lines" <+> int th_start_ln <> text "-" <> int th_end_ln
1160 bind_ln = srcSpanStartLine bind_loc
1161 th_start_ln = srcSpanStartLine th_loc
1162 th_end_ln = srcSpanEndLine th_loc
1163 is_th_bind = th_loc `containsSpan` bind_loc
1164
1165 mkHoleError tidy_simples ctxt ct@(CHoleCan { cc_hole = hole })
1166 -- Explicit holes, like "_" or "_f"
1167 = do { (ctxt, binds_msg, ct) <- relevantBindings False ctxt ct
1168 -- The 'False' means "don't filter the bindings"; see #8191
1169
1170 ; show_hole_constraints <- goptM Opt_ShowHoleConstraints
1171 ; let constraints_msg
1172 | isExprHoleCt ct, show_hole_constraints
1173 = givenConstraintsMsg ctxt
1174 | otherwise = empty
1175
1176 ; show_valid_hole_fits <- goptM Opt_ShowValidHoleFits
1177 ; (ctxt, sub_msg) <- if show_valid_hole_fits
1178 then validHoleFits ctxt tidy_simples ct
1179 else return (ctxt, empty)
1180 ; mkErrorMsgFromCt ctxt ct $
1181 important hole_msg `mappend`
1182 relevant_bindings (binds_msg $$ constraints_msg) `mappend`
1183 valid_hole_fits sub_msg}
1184
1185 where
1186 occ = holeOcc hole
1187 hole_ty = ctEvPred (ctEvidence ct)
1188 hole_kind = tcTypeKind hole_ty
1189 tyvars = tyCoVarsOfTypeList hole_ty
1190
1191 hole_msg = case hole of
1192 ExprHole {} -> vcat [ hang (text "Found hole:")
1193 2 (pp_with_type occ hole_ty)
1194 , tyvars_msg, expr_hole_hint ]
1195 TypeHole {} -> vcat [ hang (text "Found type wildcard" <+>
1196 quotes (ppr occ))
1197 2 (text "standing for" <+>
1198 quotes pp_hole_type_with_kind)
1199 , tyvars_msg, type_hole_hint ]
1200
1201 pp_hole_type_with_kind
1202 | isLiftedTypeKind hole_kind
1203 || isCoVarType hole_ty -- Don't print the kind of unlifted
1204 -- equalities (#15039)
1205 = pprType hole_ty
1206 | otherwise
1207 = pprType hole_ty <+> dcolon <+> pprKind hole_kind
1208
1209 tyvars_msg = ppUnless (null tyvars) $
1210 text "Where:" <+> (vcat (map loc_msg other_tvs)
1211 $$ pprSkols ctxt skol_tvs)
1212 where
1213 (skol_tvs, other_tvs) = partition is_skol tyvars
1214 is_skol tv = isTcTyVar tv && isSkolemTyVar tv
1215 -- Coercion variables can be free in the
1216 -- hole, via kind casts
1217
1218 type_hole_hint
1219 | HoleError <- cec_type_holes ctxt
1220 = text "To use the inferred type, enable PartialTypeSignatures"
1221 | otherwise
1222 = empty
1223
1224 expr_hole_hint -- Give hint for, say, f x = _x
1225 | lengthFS (occNameFS occ) > 1 -- Don't give this hint for plain "_"
1226 = text "Or perhaps" <+> quotes (ppr occ)
1227 <+> text "is mis-spelled, or not in scope"
1228 | otherwise
1229 = empty
1230
1231 loc_msg tv
1232 | isTyVar tv
1233 = case tcTyVarDetails tv of
1234 MetaTv {} -> quotes (ppr tv) <+> text "is an ambiguous type variable"
1235 _ -> empty -- Skolems dealt with already
1236 | otherwise -- A coercion variable can be free in the hole type
1237 = sdocWithDynFlags $ \dflags ->
1238 if gopt Opt_PrintExplicitCoercions dflags
1239 then quotes (ppr tv) <+> text "is a coercion variable"
1240 else empty
1241
1242 mkHoleError _ _ ct = pprPanic "mkHoleError" (ppr ct)
1243
1244 -- We unwrap the ReportErrCtxt here, to avoid introducing a loop in module
1245 -- imports
1246 validHoleFits :: ReportErrCtxt -- The context we're in, i.e. the
1247 -- implications and the tidy environment
1248 -> [Ct] -- Unsolved simple constraints
1249 -> Ct -- The hole constraint.
1250 -> TcM (ReportErrCtxt, SDoc) -- We return the new context
1251 -- with a possibly updated
1252 -- tidy environment, and
1253 -- the message.
1254 validHoleFits ctxt@(CEC {cec_encl = implics
1255 , cec_tidy = lcl_env}) simps ct
1256 = do { (tidy_env, msg) <- findValidHoleFits lcl_env implics simps ct
1257 ; return (ctxt {cec_tidy = tidy_env}, msg) }
1258
1259 -- See Note [Constraints include ...]
1260 givenConstraintsMsg :: ReportErrCtxt -> SDoc
1261 givenConstraintsMsg ctxt =
1262 let constraints :: [(Type, RealSrcSpan)]
1263 constraints =
1264 do { implic@Implic{ ic_given = given } <- cec_encl ctxt
1265 ; constraint <- given
1266 ; return (varType constraint, tcl_loc (implicLclEnv implic)) }
1267
1268 pprConstraint (constraint, loc) =
1269 ppr constraint <+> nest 2 (parens (text "from" <+> ppr loc))
1270
1271 in ppUnless (null constraints) $
1272 hang (text "Constraints include")
1273 2 (vcat $ map pprConstraint constraints)
1274
1275 pp_with_type :: OccName -> Type -> SDoc
1276 pp_with_type occ ty = hang (pprPrefixOcc occ) 2 (dcolon <+> pprType ty)
1277
1278 ----------------
1279 mkIPErr :: ReportErrCtxt -> [Ct] -> TcM ErrMsg
1280 mkIPErr ctxt cts
1281 = do { (ctxt, binds_msg, ct1) <- relevantBindings True ctxt ct1
1282 ; let orig = ctOrigin ct1
1283 preds = map ctPred cts
1284 givens = getUserGivens ctxt
1285 msg | null givens
1286 = addArising orig $
1287 sep [ text "Unbound implicit parameter" <> plural cts
1288 , nest 2 (pprParendTheta preds) ]
1289 | otherwise
1290 = couldNotDeduce givens (preds, orig)
1291
1292 ; mkErrorMsgFromCt ctxt ct1 $
1293 important msg `mappend` relevant_bindings binds_msg }
1294 where
1295 (ct1:_) = cts
1296
1297 {-
1298
1299 Note [Constraints include ...]
1300 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1301 'givenConstraintsMsg' returns the "Constraints include ..." message enabled by
1302 -fshow-hole-constraints. For example, the following hole:
1303
1304 foo :: (Eq a, Show a) => a -> String
1305 foo x = _
1306
1307 would generate the message:
1308
1309 Constraints include
1310 Eq a (from foo.hs:1:1-36)
1311 Show a (from foo.hs:1:1-36)
1312
1313 Constraints are displayed in order from innermost (closest to the hole) to
1314 outermost. There's currently no filtering or elimination of duplicates.
1315
1316
1317 Note [OutOfScope exact matches]
1318 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1319 When constructing an out-of-scope error message, we not only generate a list of
1320 possible in-scope alternatives but also search for an exact, unambiguous match
1321 in a later inter-splice group. If we find such a match, we report its presence
1322 (and indirectly, its scope) in the message. For example, if a module A contains
1323 the following declarations,
1324
1325 foo :: Int
1326 foo = x
1327
1328 $(return []) -- Empty top-level splice
1329
1330 x :: Int
1331 x = 23
1332
1333 we will issue an error similar to
1334
1335 A.hs:6:7: error:
1336 • Variable not in scope: x :: Int
1337 • ‘x’ (line 11) is not in scope before the splice on line 8
1338
1339 By providing information about the match, we hope to clarify why declaring a
1340 variable after a top-level splice but using it before the splice generates an
1341 out-of-scope error (a situation which is often confusing to Haskell newcomers).
1342
1343 Note that if we find multiple exact matches to the out-of-scope variable
1344 (hereafter referred to as x), we report nothing. Such matches can only be
1345 duplicate record fields, as the presence of any other duplicate top-level
1346 declarations would have already halted compilation. But if these record fields
1347 are declared in a later inter-splice group, then so too are their corresponding
1348 types. Thus, these types must not occur in the inter-splice group containing x
1349 (any unknown types would have already been reported), and so the matches to the
1350 record fields are most likely coincidental.
1351
1352 One oddity of the exact match portion of the error message is that we specify
1353 where the match to x is NOT in scope. Why not simply state where the match IS
1354 in scope? It most cases, this would be just as easy and perhaps a little
1355 clearer for the user. But now consider the following example:
1356
1357 {-# LANGUAGE TemplateHaskell #-}
1358
1359 module A where
1360
1361 import Language.Haskell.TH
1362 import Language.Haskell.TH.Syntax
1363
1364 foo = x
1365
1366 $(do -------------------------------------------------
1367 ds <- [d| ok1 = x
1368 |]
1369 addTopDecls ds
1370 return [])
1371
1372 bar = $(do
1373 ds <- [d| x = 23
1374 ok2 = x
1375 |]
1376 addTopDecls ds
1377 litE $ stringL "hello")
1378
1379 $(return []) -----------------------------------------
1380
1381 ok3 = x
1382
1383 Here, x is out-of-scope in the declaration of foo, and so we report
1384
1385 A.hs:8:7: error:
1386 • Variable not in scope: x
1387 • ‘x’ (line 16) is not in scope before the splice on lines 10-14
1388
1389 If we instead reported where x IS in scope, we would have to state that it is in
1390 scope after the second top-level splice as well as among all the top-level
1391 declarations added by both calls to addTopDecls. But doing so would not only
1392 add complexity to the code but also overwhelm the user with unneeded
1393 information.
1394
1395 The logic which determines where x is not in scope is straightforward: it simply
1396 finds the last top-level splice which occurs after x but before (or at) the
1397 match to x (assuming such a splice exists). In most cases, the check that the
1398 splice occurs after x acts only as a sanity check. For example, when the match
1399 to x is a non-TH top-level declaration and a splice S occurs before the match,
1400 then x must precede S; otherwise, it would be in scope. But when dealing with
1401 addTopDecls, this check serves a practical purpose. Consider the following
1402 declarations:
1403
1404 $(do
1405 ds <- [d| ok = x
1406 x = 23
1407 |]
1408 addTopDecls ds
1409 return [])
1410
1411 foo = x
1412
1413 In this case, x is not in scope in the declaration for foo. Since x occurs
1414 AFTER the splice containing the match, the logic does not find any splices after
1415 x but before or at its match, and so we report nothing about x's scope. If we
1416 had not checked whether x occurs before the splice, we would have instead
1417 reported that x is not in scope before the splice. While correct, such an error
1418 message is more likely to confuse than to enlighten.
1419 -}
1420
1421 {-
1422 ************************************************************************
1423 * *
1424 Equality errors
1425 * *
1426 ************************************************************************
1427
1428 Note [Inaccessible code]
1429 ~~~~~~~~~~~~~~~~~~~~~~~~
1430 Consider
1431 data T a where
1432 T1 :: T a
1433 T2 :: T Bool
1434
1435 f :: (a ~ Int) => T a -> Int
1436 f T1 = 3
1437 f T2 = 4 -- Unreachable code
1438
1439 Here the second equation is unreachable. The original constraint
1440 (a~Int) from the signature gets rewritten by the pattern-match to
1441 (Bool~Int), so the danger is that we report the error as coming from
1442 the *signature* (#7293). So, for Given errors we replace the
1443 env (and hence src-loc) on its CtLoc with that from the immediately
1444 enclosing implication.
1445
1446 Note [Error messages for untouchables]
1447 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1448 Consider (#9109)
1449 data G a where { GBool :: G Bool }
1450 foo x = case x of GBool -> True
1451
1452 Here we can't solve (t ~ Bool), where t is the untouchable result
1453 meta-var 't', because of the (a ~ Bool) from the pattern match.
1454 So we infer the type
1455 f :: forall a t. G a -> t
1456 making the meta-var 't' into a skolem. So when we come to report
1457 the unsolved (t ~ Bool), t won't look like an untouchable meta-var
1458 any more. So we don't assert that it is.
1459 -}
1460
1461 -- Don't have multiple equality errors from the same location
1462 -- E.g. (Int,Bool) ~ (Bool,Int) one error will do!
1463 mkEqErr :: ReportErrCtxt -> [Ct] -> TcM ErrMsg
1464 mkEqErr ctxt (ct:_) = mkEqErr1 ctxt ct
1465 mkEqErr _ [] = panic "mkEqErr"
1466
1467 mkEqErr1 :: ReportErrCtxt -> Ct -> TcM ErrMsg
1468 mkEqErr1 ctxt ct -- Wanted or derived;
1469 -- givens handled in mkGivenErrorReporter
1470 = do { (ctxt, binds_msg, ct) <- relevantBindings True ctxt ct
1471 ; rdr_env <- getGlobalRdrEnv
1472 ; fam_envs <- tcGetFamInstEnvs
1473 ; exp_syns <- goptM Opt_PrintExpandedSynonyms
1474 ; let (keep_going, is_oriented, wanted_msg)
1475 = mk_wanted_extra (ctLoc ct) exp_syns
1476 coercible_msg = case ctEqRel ct of
1477 NomEq -> empty
1478 ReprEq -> mkCoercibleExplanation rdr_env fam_envs ty1 ty2
1479 ; dflags <- getDynFlags
1480 ; traceTc "mkEqErr1" (ppr ct $$ pprCtOrigin (ctOrigin ct) $$ ppr keep_going)
1481 ; let report = mconcat [important wanted_msg, important coercible_msg,
1482 relevant_bindings binds_msg]
1483 ; if keep_going
1484 then mkEqErr_help dflags ctxt report ct is_oriented ty1 ty2
1485 else mkErrorMsgFromCt ctxt ct report }
1486 where
1487 (ty1, ty2) = getEqPredTys (ctPred ct)
1488
1489 -- If the types in the error message are the same as the types
1490 -- we are unifying, don't add the extra expected/actual message
1491 mk_wanted_extra :: CtLoc -> Bool -> (Bool, Maybe SwapFlag, SDoc)
1492 mk_wanted_extra loc expandSyns
1493 = case ctLocOrigin loc of
1494 orig@TypeEqOrigin {} -> mkExpectedActualMsg ty1 ty2 orig
1495 t_or_k expandSyns
1496 where
1497 t_or_k = ctLocTypeOrKind_maybe loc
1498
1499 KindEqOrigin cty1 mb_cty2 sub_o sub_t_or_k
1500 -> (True, Nothing, msg1 $$ msg2)
1501 where
1502 sub_what = case sub_t_or_k of Just KindLevel -> text "kinds"
1503 _ -> text "types"
1504 msg1 = sdocWithDynFlags $ \dflags ->
1505 case mb_cty2 of
1506 Just cty2
1507 | gopt Opt_PrintExplicitCoercions dflags
1508 || not (cty1 `pickyEqType` cty2)
1509 -> hang (text "When matching" <+> sub_what)
1510 2 (vcat [ ppr cty1 <+> dcolon <+>
1511 ppr (tcTypeKind cty1)
1512 , ppr cty2 <+> dcolon <+>
1513 ppr (tcTypeKind cty2) ])
1514 _ -> text "When matching the kind of" <+> quotes (ppr cty1)
1515 msg2 = case sub_o of
1516 TypeEqOrigin {}
1517 | Just cty2 <- mb_cty2 ->
1518 thdOf3 (mkExpectedActualMsg cty1 cty2 sub_o sub_t_or_k
1519 expandSyns)
1520 _ -> empty
1521 _ -> (True, Nothing, empty)
1522
1523 -- | This function tries to reconstruct why a "Coercible ty1 ty2" constraint
1524 -- is left over.
1525 mkCoercibleExplanation :: GlobalRdrEnv -> FamInstEnvs
1526 -> TcType -> TcType -> SDoc
1527 mkCoercibleExplanation rdr_env fam_envs ty1 ty2
1528 | Just (tc, tys) <- tcSplitTyConApp_maybe ty1
1529 , (rep_tc, _, _) <- tcLookupDataFamInst fam_envs tc tys
1530 , Just msg <- coercible_msg_for_tycon rep_tc
1531 = msg
1532 | Just (tc, tys) <- splitTyConApp_maybe ty2
1533 , (rep_tc, _, _) <- tcLookupDataFamInst fam_envs tc tys
1534 , Just msg <- coercible_msg_for_tycon rep_tc
1535 = msg
1536 | Just (s1, _) <- tcSplitAppTy_maybe ty1
1537 , Just (s2, _) <- tcSplitAppTy_maybe ty2
1538 , s1 `eqType` s2
1539 , has_unknown_roles s1
1540 = hang (text "NB: We cannot know what roles the parameters to" <+>
1541 quotes (ppr s1) <+> text "have;")
1542 2 (text "we must assume that the role is nominal")
1543 | otherwise
1544 = empty
1545 where
1546 coercible_msg_for_tycon tc
1547 | isAbstractTyCon tc
1548 = Just $ hsep [ text "NB: The type constructor"
1549 , quotes (pprSourceTyCon tc)
1550 , text "is abstract" ]
1551 | isNewTyCon tc
1552 , [data_con] <- tyConDataCons tc
1553 , let dc_name = dataConName data_con
1554 , isNothing (lookupGRE_Name rdr_env dc_name)
1555 = Just $ hang (text "The data constructor" <+> quotes (ppr dc_name))
1556 2 (sep [ text "of newtype" <+> quotes (pprSourceTyCon tc)
1557 , text "is not in scope" ])
1558 | otherwise = Nothing
1559
1560 has_unknown_roles ty
1561 | Just (tc, tys) <- tcSplitTyConApp_maybe ty
1562 = tys `lengthAtLeast` tyConArity tc -- oversaturated tycon
1563 | Just (s, _) <- tcSplitAppTy_maybe ty
1564 = has_unknown_roles s
1565 | isTyVarTy ty
1566 = True
1567 | otherwise
1568 = False
1569
1570 {-
1571 -- | Make a listing of role signatures for all the parameterised tycons
1572 -- used in the provided types
1573
1574
1575 -- SLPJ Jun 15: I could not convince myself that these hints were really
1576 -- useful. Maybe they are, but I think we need more work to make them
1577 -- actually helpful.
1578 mkRoleSigs :: Type -> Type -> SDoc
1579 mkRoleSigs ty1 ty2
1580 = ppUnless (null role_sigs) $
1581 hang (text "Relevant role signatures:")
1582 2 (vcat role_sigs)
1583 where
1584 tcs = nameEnvElts $ tyConsOfType ty1 `plusNameEnv` tyConsOfType ty2
1585 role_sigs = mapMaybe ppr_role_sig tcs
1586
1587 ppr_role_sig tc
1588 | null roles -- if there are no parameters, don't bother printing
1589 = Nothing
1590 | isBuiltInSyntax (tyConName tc) -- don't print roles for (->), etc.
1591 = Nothing
1592 | otherwise
1593 = Just $ hsep $ [text "type role", ppr tc] ++ map ppr roles
1594 where
1595 roles = tyConRoles tc
1596 -}
1597
1598 mkEqErr_help :: DynFlags -> ReportErrCtxt -> Report
1599 -> Ct
1600 -> Maybe SwapFlag -- Nothing <=> not sure
1601 -> TcType -> TcType -> TcM ErrMsg
1602 mkEqErr_help dflags ctxt report ct oriented ty1 ty2
1603 | Just (tv1, co1) <- tcGetCastedTyVar_maybe ty1
1604 = mkTyVarEqErr dflags ctxt report ct oriented tv1 co1 ty2
1605 | Just (tv2, co2) <- tcGetCastedTyVar_maybe ty2
1606 = mkTyVarEqErr dflags ctxt report ct swapped tv2 co2 ty1
1607 | otherwise
1608 = reportEqErr ctxt report ct oriented ty1 ty2
1609 where
1610 swapped = fmap flipSwap oriented
1611
1612 reportEqErr :: ReportErrCtxt -> Report
1613 -> Ct
1614 -> Maybe SwapFlag -- Nothing <=> not sure
1615 -> TcType -> TcType -> TcM ErrMsg
1616 reportEqErr ctxt report ct oriented ty1 ty2
1617 = mkErrorMsgFromCt ctxt ct (mconcat [misMatch, report, eqInfo])
1618 where misMatch = important $ misMatchOrCND ctxt ct oriented ty1 ty2
1619 eqInfo = important $ mkEqInfoMsg ct ty1 ty2
1620
1621 mkTyVarEqErr, mkTyVarEqErr'
1622 :: DynFlags -> ReportErrCtxt -> Report -> Ct
1623 -> Maybe SwapFlag -> TcTyVar -> TcCoercionN -> TcType -> TcM ErrMsg
1624 -- tv1 and ty2 are already tidied
1625 mkTyVarEqErr dflags ctxt report ct oriented tv1 co1 ty2
1626 = do { traceTc "mkTyVarEqErr" (ppr ct $$ ppr tv1 $$ ppr co1 $$ ppr ty2)
1627 ; mkTyVarEqErr' dflags ctxt report ct oriented tv1 co1 ty2 }
1628
1629 mkTyVarEqErr' dflags ctxt report ct oriented tv1 co1 ty2
1630 | not insoluble_occurs_check -- See Note [Occurs check wins]
1631 , isUserSkolem ctxt tv1 -- ty2 won't be a meta-tyvar, or else the thing would
1632 -- be oriented the other way round;
1633 -- see TcCanonical.canEqTyVarTyVar
1634 || isTyVarTyVar tv1 && not (isTyVarTy ty2)
1635 || ctEqRel ct == ReprEq
1636 -- the cases below don't really apply to ReprEq (except occurs check)
1637 = mkErrorMsgFromCt ctxt ct $ mconcat
1638 [ important $ misMatchOrCND ctxt ct oriented ty1 ty2
1639 , important $ extraTyVarEqInfo ctxt tv1 ty2
1640 , report
1641 ]
1642
1643 | MTVU_Occurs <- occ_check_expand
1644 -- We report an "occurs check" even for a ~ F t a, where F is a type
1645 -- function; it's not insoluble (because in principle F could reduce)
1646 -- but we have certainly been unable to solve it
1647 -- See Note [Occurs check error] in TcCanonical
1648 = do { let main_msg = addArising (ctOrigin ct) $
1649 hang (text "Occurs check: cannot construct the infinite" <+> what <> colon)
1650 2 (sep [ppr ty1, char '~', ppr ty2])
1651
1652 extra2 = important $ mkEqInfoMsg ct ty1 ty2
1653
1654 interesting_tyvars = filter (not . noFreeVarsOfType . tyVarKind) $
1655 filter isTyVar $
1656 fvVarList $
1657 tyCoFVsOfType ty1 `unionFV` tyCoFVsOfType ty2
1658 extra3 = relevant_bindings $
1659 ppWhen (not (null interesting_tyvars)) $
1660 hang (text "Type variable kinds:") 2 $
1661 vcat (map (tyvar_binding . tidyTyCoVarOcc (cec_tidy ctxt))
1662 interesting_tyvars)
1663
1664 tyvar_binding tv = ppr tv <+> dcolon <+> ppr (tyVarKind tv)
1665 ; mkErrorMsgFromCt ctxt ct $
1666 mconcat [important main_msg, extra2, extra3, report] }
1667
1668 | MTVU_Bad <- occ_check_expand
1669 = do { let msg = vcat [ text "Cannot instantiate unification variable"
1670 <+> quotes (ppr tv1)
1671 , hang (text "with a" <+> what <+> text "involving polytypes:") 2 (ppr ty2)
1672 , nest 2 (text "GHC doesn't yet support impredicative polymorphism") ]
1673 -- Unlike the other reports, this discards the old 'report_important'
1674 -- instead of augmenting it. This is because the details are not likely
1675 -- to be helpful since this is just an unimplemented feature.
1676 ; mkErrorMsgFromCt ctxt ct $ report { report_important = [msg] } }
1677
1678 -- check for heterogeneous equality next; see Note [Equalities with incompatible kinds]
1679 -- in TcCanonical
1680 | not (k1 `tcEqType` k2)
1681 = do { let main_msg = addArising (ctOrigin ct) $
1682 vcat [ hang (text "Kind mismatch: cannot unify" <+>
1683 parens (ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1)) <+>
1684 text "with:")
1685 2 (sep [ppr ty2, dcolon, ppr k2])
1686 , text "Their kinds differ." ]
1687 cast_msg
1688 | isTcReflexiveCo co1 = empty
1689 | otherwise = text "NB:" <+> ppr tv1 <+>
1690 text "was casted to have kind" <+>
1691 quotes (ppr k1)
1692
1693 ; mkErrorMsgFromCt ctxt ct (mconcat [important main_msg, important cast_msg, report]) }
1694
1695 -- If the immediately-enclosing implication has 'tv' a skolem, and
1696 -- we know by now its an InferSkol kind of skolem, then presumably
1697 -- it started life as a TyVarTv, else it'd have been unified, given
1698 -- that there's no occurs-check or forall problem
1699 | (implic:_) <- cec_encl ctxt
1700 , Implic { ic_skols = skols } <- implic
1701 , tv1 `elem` skols
1702 = mkErrorMsgFromCt ctxt ct $ mconcat
1703 [ important $ misMatchMsg ct oriented ty1 ty2
1704 , important $ extraTyVarEqInfo ctxt tv1 ty2
1705 , report
1706 ]
1707
1708 -- Check for skolem escape
1709 | (implic:_) <- cec_encl ctxt -- Get the innermost context
1710 , Implic { ic_skols = skols, ic_info = skol_info } <- implic
1711 , let esc_skols = filter (`elemVarSet` (tyCoVarsOfType ty2)) skols
1712 , not (null esc_skols)
1713 = do { let msg = important $ misMatchMsg ct oriented ty1 ty2
1714 esc_doc = sep [ text "because" <+> what <+> text "variable" <> plural esc_skols
1715 <+> pprQuotedList esc_skols
1716 , text "would escape" <+>
1717 if isSingleton esc_skols then text "its scope"
1718 else text "their scope" ]
1719 tv_extra = important $
1720 vcat [ nest 2 $ esc_doc
1721 , sep [ (if isSingleton esc_skols
1722 then text "This (rigid, skolem)" <+>
1723 what <+> text "variable is"
1724 else text "These (rigid, skolem)" <+>
1725 what <+> text "variables are")
1726 <+> text "bound by"
1727 , nest 2 $ ppr skol_info
1728 , nest 2 $ text "at" <+>
1729 ppr (tcl_loc (implicLclEnv implic)) ] ]
1730 ; mkErrorMsgFromCt ctxt ct (mconcat [msg, tv_extra, report]) }
1731
1732 -- Nastiest case: attempt to unify an untouchable variable
1733 -- So tv is a meta tyvar (or started that way before we
1734 -- generalised it). So presumably it is an *untouchable*
1735 -- meta tyvar or a TyVarTv, else it'd have been unified
1736 -- See Note [Error messages for untouchables]
1737 | (implic:_) <- cec_encl ctxt -- Get the innermost context
1738 , Implic { ic_given = given, ic_tclvl = lvl, ic_info = skol_info } <- implic
1739 = ASSERT2( not (isTouchableMetaTyVar lvl tv1)
1740 , ppr tv1 $$ ppr lvl ) -- See Note [Error messages for untouchables]
1741 do { let msg = important $ misMatchMsg ct oriented ty1 ty2
1742 tclvl_extra = important $
1743 nest 2 $
1744 sep [ quotes (ppr tv1) <+> text "is untouchable"
1745 , nest 2 $ text "inside the constraints:" <+> pprEvVarTheta given
1746 , nest 2 $ text "bound by" <+> ppr skol_info
1747 , nest 2 $ text "at" <+>
1748 ppr (tcl_loc (implicLclEnv implic)) ]
1749 tv_extra = important $ extraTyVarEqInfo ctxt tv1 ty2
1750 add_sig = important $ suggestAddSig ctxt ty1 ty2
1751 ; mkErrorMsgFromCt ctxt ct $ mconcat
1752 [msg, tclvl_extra, tv_extra, add_sig, report] }
1753
1754 | otherwise
1755 = reportEqErr ctxt report ct oriented (mkTyVarTy tv1) ty2
1756 -- This *can* happen (#6123, and test T2627b)
1757 -- Consider an ambiguous top-level constraint (a ~ F a)
1758 -- Not an occurs check, because F is a type function.
1759 where
1760 Pair _ k1 = tcCoercionKind co1
1761 k2 = tcTypeKind ty2
1762
1763 ty1 = mkTyVarTy tv1
1764 occ_check_expand = occCheckForErrors dflags tv1 ty2
1765 insoluble_occurs_check = isInsolubleOccursCheck (ctEqRel ct) tv1 ty2
1766
1767 what = case ctLocTypeOrKind_maybe (ctLoc ct) of
1768 Just KindLevel -> text "kind"
1769 _ -> text "type"
1770
1771 mkEqInfoMsg :: Ct -> TcType -> TcType -> SDoc
1772 -- Report (a) ambiguity if either side is a type function application
1773 -- e.g. F a0 ~ Int
1774 -- (b) warning about injectivity if both sides are the same
1775 -- type function application F a ~ F b
1776 -- See Note [Non-injective type functions]
1777 mkEqInfoMsg ct ty1 ty2
1778 = tyfun_msg $$ ambig_msg
1779 where
1780 mb_fun1 = isTyFun_maybe ty1
1781 mb_fun2 = isTyFun_maybe ty2
1782
1783 ambig_msg | isJust mb_fun1 || isJust mb_fun2
1784 = snd (mkAmbigMsg False ct)
1785 | otherwise = empty
1786
1787 tyfun_msg | Just tc1 <- mb_fun1
1788 , Just tc2 <- mb_fun2
1789 , tc1 == tc2
1790 , not (isInjectiveTyCon tc1 Nominal)
1791 = text "NB:" <+> quotes (ppr tc1)
1792 <+> text "is a non-injective type family"
1793 | otherwise = empty
1794
1795 isUserSkolem :: ReportErrCtxt -> TcTyVar -> Bool
1796 -- See Note [Reporting occurs-check errors]
1797 isUserSkolem ctxt tv
1798 = isSkolemTyVar tv && any is_user_skol_tv (cec_encl ctxt)
1799 where
1800 is_user_skol_tv (Implic { ic_skols = sks, ic_info = skol_info })
1801 = tv `elem` sks && is_user_skol_info skol_info
1802
1803 is_user_skol_info (InferSkol {}) = False
1804 is_user_skol_info _ = True
1805
1806 misMatchOrCND :: ReportErrCtxt -> Ct
1807 -> Maybe SwapFlag -> TcType -> TcType -> SDoc
1808 -- If oriented then ty1 is actual, ty2 is expected
1809 misMatchOrCND ctxt ct oriented ty1 ty2
1810 | null givens ||
1811 (isRigidTy ty1 && isRigidTy ty2) ||
1812 isGivenCt ct
1813 -- If the equality is unconditionally insoluble
1814 -- or there is no context, don't report the context
1815 = misMatchMsg ct oriented ty1 ty2
1816 | otherwise
1817 = couldNotDeduce givens ([eq_pred], orig)
1818 where
1819 ev = ctEvidence ct
1820 eq_pred = ctEvPred ev
1821 orig = ctEvOrigin ev
1822 givens = [ given | given <- getUserGivens ctxt, not (ic_no_eqs given)]
1823 -- Keep only UserGivens that have some equalities.
1824 -- See Note [Suppress redundant givens during error reporting]
1825
1826 couldNotDeduce :: [UserGiven] -> (ThetaType, CtOrigin) -> SDoc
1827 couldNotDeduce givens (wanteds, orig)
1828 = vcat [ addArising orig (text "Could not deduce:" <+> pprTheta wanteds)
1829 , vcat (pp_givens givens)]
1830
1831 pp_givens :: [UserGiven] -> [SDoc]
1832 pp_givens givens
1833 = case givens of
1834 [] -> []
1835 (g:gs) -> ppr_given (text "from the context:") g
1836 : map (ppr_given (text "or from:")) gs
1837 where
1838 ppr_given herald implic@(Implic { ic_given = gs, ic_info = skol_info })
1839 = hang (herald <+> pprEvVarTheta (mkMinimalBySCs evVarPred gs))
1840 -- See Note [Suppress redundant givens during error reporting]
1841 -- for why we use mkMinimalBySCs above.
1842 2 (sep [ text "bound by" <+> ppr skol_info
1843 , text "at" <+> ppr (tcl_loc (implicLclEnv implic)) ])
1844
1845 {-
1846 Note [Suppress redundant givens during error reporting]
1847 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1848 When GHC is unable to solve a constraint and prints out an error message, it
1849 will print out what given constraints are in scope to provide some context to
1850 the programmer. But we shouldn't print out /every/ given, since some of them
1851 are not terribly helpful to diagnose type errors. Consider this example:
1852
1853 foo :: Int :~: Int -> a :~: b -> a :~: c
1854 foo Refl Refl = Refl
1855
1856 When reporting that GHC can't solve (a ~ c), there are two givens in scope:
1857 (Int ~ Int) and (a ~ b). But (Int ~ Int) is trivially soluble (i.e.,
1858 redundant), so it's not terribly useful to report it in an error message.
1859 To accomplish this, we discard any Implications that do not bind any
1860 equalities by filtering the `givens` selected in `misMatchOrCND` (based on
1861 the `ic_no_eqs` field of the Implication).
1862
1863 But this is not enough to avoid all redundant givens! Consider this example,
1864 from #15361:
1865
1866 goo :: forall (a :: Type) (b :: Type) (c :: Type).
1867 a :~~: b -> a :~~: c
1868 goo HRefl = HRefl
1869
1870 Matching on HRefl brings the /single/ given (* ~ *, a ~ b) into scope.
1871 The (* ~ *) part arises due the kinds of (:~~:) being unified. More
1872 importantly, (* ~ *) is redundant, so we'd like not to report it. However,
1873 the Implication (* ~ *, a ~ b) /does/ bind an equality (as reported by its
1874 ic_no_eqs field), so the test above will keep it wholesale.
1875
1876 To refine this given, we apply mkMinimalBySCs on it to extract just the (a ~ b)
1877 part. This works because mkMinimalBySCs eliminates reflexive equalities in
1878 addition to superclasses (see Note [Remove redundant provided dicts]
1879 in TcPatSyn).
1880 -}
1881
1882 extraTyVarEqInfo :: ReportErrCtxt -> TcTyVar -> TcType -> SDoc
1883 -- Add on extra info about skolem constants
1884 -- NB: The types themselves are already tidied
1885 extraTyVarEqInfo ctxt tv1 ty2
1886 = extraTyVarInfo ctxt tv1 $$ ty_extra ty2
1887 where
1888 ty_extra ty = case tcGetTyVar_maybe ty of
1889 Just tv -> extraTyVarInfo ctxt tv
1890 Nothing -> empty
1891
1892 extraTyVarInfo :: ReportErrCtxt -> TcTyVar -> SDoc
1893 extraTyVarInfo ctxt tv
1894 = ASSERT2( isTyVar tv, ppr tv )
1895 case tcTyVarDetails tv of
1896 SkolemTv {} -> pprSkols ctxt [tv]
1897 RuntimeUnk {} -> quotes (ppr tv) <+> text "is an interactive-debugger skolem"
1898 MetaTv {} -> empty
1899
1900 suggestAddSig :: ReportErrCtxt -> TcType -> TcType -> SDoc
1901 -- See Note [Suggest adding a type signature]
1902 suggestAddSig ctxt ty1 ty2
1903 | null inferred_bndrs
1904 = empty
1905 | [bndr] <- inferred_bndrs
1906 = text "Possible fix: add a type signature for" <+> quotes (ppr bndr)
1907 | otherwise
1908 = text "Possible fix: add type signatures for some or all of" <+> (ppr inferred_bndrs)
1909 where
1910 inferred_bndrs = nub (get_inf ty1 ++ get_inf ty2)
1911 get_inf ty | Just tv <- tcGetTyVar_maybe ty
1912 , isSkolemTyVar tv
1913 , (implic, _) : _ <- getSkolemInfo (cec_encl ctxt) [tv]
1914 , InferSkol prs <- ic_info implic
1915 = map fst prs
1916 | otherwise
1917 = []
1918
1919 --------------------
1920 misMatchMsg :: Ct -> Maybe SwapFlag -> TcType -> TcType -> SDoc
1921 -- Types are already tidy
1922 -- If oriented then ty1 is actual, ty2 is expected
1923 misMatchMsg ct oriented ty1 ty2
1924 | Just NotSwapped <- oriented
1925 = misMatchMsg ct (Just IsSwapped) ty2 ty1
1926
1927 -- These next two cases are when we're about to report, e.g., that
1928 -- 'LiftedRep doesn't match 'VoidRep. Much better just to say
1929 -- lifted vs. unlifted
1930 | isLiftedRuntimeRep ty1
1931 = lifted_vs_unlifted
1932
1933 | isLiftedRuntimeRep ty2
1934 = lifted_vs_unlifted
1935
1936 | otherwise -- So now we have Nothing or (Just IsSwapped)
1937 -- For some reason we treat Nothing like IsSwapped
1938 = addArising orig $
1939 pprWithExplicitKindsWhenMismatch ty1 ty2 (ctOrigin ct) $
1940 sep [ text herald1 <+> quotes (ppr ty1)
1941 , nest padding $
1942 text herald2 <+> quotes (ppr ty2)
1943 , sameOccExtra ty2 ty1 ]
1944 where
1945 herald1 = conc [ "Couldn't match"
1946 , if is_repr then "representation of" else ""
1947 , if is_oriented then "expected" else ""
1948 , what ]
1949 herald2 = conc [ "with"
1950 , if is_repr then "that of" else ""
1951 , if is_oriented then ("actual " ++ what) else "" ]
1952 padding = length herald1 - length herald2
1953
1954 is_repr = case ctEqRel ct of { ReprEq -> True; NomEq -> False }
1955 is_oriented = isJust oriented
1956
1957 orig = ctOrigin ct
1958 what = case ctLocTypeOrKind_maybe (ctLoc ct) of
1959 Just KindLevel -> "kind"
1960 _ -> "type"
1961
1962 conc :: [String] -> String
1963 conc = foldr1 add_space
1964
1965 add_space :: String -> String -> String
1966 add_space s1 s2 | null s1 = s2
1967 | null s2 = s1
1968 | otherwise = s1 ++ (' ' : s2)
1969
1970 lifted_vs_unlifted
1971 = addArising orig $
1972 text "Couldn't match a lifted type with an unlifted type"
1973
1974 -- | Prints explicit kinds (with @-fprint-explicit-kinds@) in an 'SDoc' when a
1975 -- type mismatch occurs to due invisible kind arguments.
1976 --
1977 -- This function first checks to see if the 'CtOrigin' argument is a
1978 -- 'TypeEqOrigin', and if so, uses the expected/actual types from that to
1979 -- check for a kind mismatch (as these types typically have more surrounding
1980 -- types and are likelier to be able to glean information about whether a
1981 -- mismatch occurred in an invisible argument position or not). If the
1982 -- 'CtOrigin' is not a 'TypeEqOrigin', fall back on the actual mismatched types
1983 -- themselves.
1984 pprWithExplicitKindsWhenMismatch :: Type -> Type -> CtOrigin
1985 -> SDoc -> SDoc
1986 pprWithExplicitKindsWhenMismatch ty1 ty2 ct
1987 = pprWithExplicitKindsWhen show_kinds
1988 where
1989 (act_ty, exp_ty) = case ct of
1990 TypeEqOrigin { uo_actual = act
1991 , uo_expected = exp } -> (act, exp)
1992 _ -> (ty1, ty2)
1993 show_kinds = tcEqTypeVis act_ty exp_ty
1994 -- True when the visible bit of the types look the same,
1995 -- so we want to show the kinds in the displayed type
1996
1997 mkExpectedActualMsg :: Type -> Type -> CtOrigin -> Maybe TypeOrKind -> Bool
1998 -> (Bool, Maybe SwapFlag, SDoc)
1999 -- NotSwapped means (actual, expected), IsSwapped is the reverse
2000 -- First return val is whether or not to print a herald above this msg
2001 mkExpectedActualMsg ty1 ty2 ct@(TypeEqOrigin { uo_actual = act
2002 , uo_expected = exp
2003 , uo_thing = maybe_thing })
2004 m_level printExpanded
2005 | KindLevel <- level, occurs_check_error = (True, Nothing, empty)
2006 | isUnliftedTypeKind act, isLiftedTypeKind exp = (False, Nothing, msg2)
2007 | isLiftedTypeKind act, isUnliftedTypeKind exp = (False, Nothing, msg3)
2008 | tcIsLiftedTypeKind exp = (False, Nothing, msg4)
2009 | Just msg <- num_args_msg = (False, Nothing, msg $$ msg1)
2010 | KindLevel <- level, Just th <- maybe_thing = (False, Nothing, msg5 th)
2011 | act `pickyEqType` ty1, exp `pickyEqType` ty2 = (True, Just NotSwapped, empty)
2012 | exp `pickyEqType` ty1, act `pickyEqType` ty2 = (True, Just IsSwapped, empty)
2013 | otherwise = (True, Nothing, msg1)
2014 where
2015 level = m_level `orElse` TypeLevel
2016
2017 occurs_check_error
2018 | Just tv <- tcGetTyVar_maybe ty1
2019 , tv `elemVarSet` tyCoVarsOfType ty2
2020 = True
2021 | Just tv <- tcGetTyVar_maybe ty2
2022 , tv `elemVarSet` tyCoVarsOfType ty1
2023 = True
2024 | otherwise
2025 = False
2026
2027 sort = case level of
2028 TypeLevel -> text "type"
2029 KindLevel -> text "kind"
2030
2031 msg1 = case level of
2032 KindLevel
2033 | Just th <- maybe_thing
2034 -> msg5 th
2035
2036 _ | not (act `pickyEqType` exp)
2037 -> pprWithExplicitKindsWhenMismatch ty1 ty2 ct $
2038 vcat [ text "Expected" <+> sort <> colon <+> ppr exp
2039 , text " Actual" <+> sort <> colon <+> ppr act
2040 , if printExpanded then expandedTys else empty ]
2041
2042 | otherwise
2043 -> empty
2044
2045 thing_msg = case maybe_thing of
2046 Just thing -> \_ levity ->
2047 quotes thing <+> text "is" <+> levity
2048 Nothing -> \vowel levity ->
2049 text "got a" <>
2050 (if vowel then char 'n' else empty) <+>
2051 levity <+>
2052 text "type"
2053 msg2 = sep [ text "Expecting a lifted type, but"
2054 , thing_msg True (text "unlifted") ]
2055 msg3 = sep [ text "Expecting an unlifted type, but"
2056 , thing_msg False (text "lifted") ]
2057 msg4 = maybe_num_args_msg $$
2058 sep [ text "Expected a type, but"
2059 , maybe (text "found something with kind")
2060 (\thing -> quotes thing <+> text "has kind")
2061 maybe_thing
2062 , quotes (pprWithTYPE act) ]
2063
2064 msg5 th = pprWithExplicitKindsWhenMismatch ty1 ty2 ct $
2065 hang (text "Expected" <+> kind_desc <> comma)
2066 2 (text "but" <+> quotes th <+> text "has kind" <+>
2067 quotes (ppr act))
2068 where
2069 kind_desc | tcIsConstraintKind exp = text "a constraint"
2070
2071 -- TYPE t0
2072 | Just arg <- kindRep_maybe exp
2073 , tcIsTyVarTy arg = sdocWithDynFlags $ \dflags ->
2074 if gopt Opt_PrintExplicitRuntimeReps dflags
2075 then text "kind" <+> quotes (ppr exp)
2076 else text "a type"
2077
2078 | otherwise = text "kind" <+> quotes (ppr exp)
2079
2080 num_args_msg = case level of
2081 KindLevel
2082 | not (isMetaTyVarTy exp) && not (isMetaTyVarTy act)
2083 -- if one is a meta-tyvar, then it's possible that the user
2084 -- has asked for something impredicative, and we couldn't unify.
2085 -- Don't bother with counting arguments.
2086 -> let n_act = count_args act
2087 n_exp = count_args exp in
2088 case n_act - n_exp of
2089 n | n > 0 -- we don't know how many args there are, so don't
2090 -- recommend removing args that aren't
2091 , Just thing <- maybe_thing
2092 -> Just $ text "Expecting" <+> speakN (abs n) <+>
2093 more <+> quotes thing
2094 where
2095 more
2096 | n == 1 = text "more argument to"
2097 | otherwise = text "more arguments to" -- n > 1
2098 _ -> Nothing
2099
2100 _ -> Nothing
2101
2102 maybe_num_args_msg = case num_args_msg of
2103 Nothing -> empty
2104 Just m -> m
2105
2106 count_args ty = count isVisibleBinder $ fst $ splitPiTys ty
2107
2108 expandedTys =
2109 ppUnless (expTy1 `pickyEqType` exp && expTy2 `pickyEqType` act) $ vcat
2110 [ text "Type synonyms expanded:"
2111 , text "Expected type:" <+> ppr expTy1
2112 , text " Actual type:" <+> ppr expTy2
2113 ]
2114
2115 (expTy1, expTy2) = expandSynonymsToMatch exp act
2116
2117 mkExpectedActualMsg _ _ _ _ _ = panic "mkExpectedAcutalMsg"
2118
2119 {- Note [Insoluble occurs check wins]
2120 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2121 Consider [G] a ~ [a], [W] a ~ [a] (#13674). The Given is insoluble
2122 so we don't use it for rewriting. The Wanted is also insoluble, and
2123 we don't solve it from the Given. It's very confusing to say
2124 Cannot solve a ~ [a] from given constraints a ~ [a]
2125
2126 And indeed even thinking about the Givens is silly; [W] a ~ [a] is
2127 just as insoluble as Int ~ Bool.
2128
2129 Conclusion: if there's an insoluble occurs check (isInsolubleOccursCheck)
2130 then report it first.
2131
2132 (NB: there are potentially-soluble ones, like (a ~ F a b), and we don't
2133 want to be as draconian with them.)
2134
2135 Note [Expanding type synonyms to make types similar]
2136 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2137
2138 In type error messages, if -fprint-expanded-types is used, we want to expand
2139 type synonyms to make expected and found types as similar as possible, but we
2140 shouldn't expand types too much to make type messages even more verbose and
2141 harder to understand. The whole point here is to make the difference in expected
2142 and found types clearer.
2143
2144 `expandSynonymsToMatch` does this, it takes two types, and expands type synonyms
2145 only as much as necessary. Given two types t1 and t2:
2146
2147 * If they're already same, it just returns the types.
2148
2149 * If they're in form `C1 t1_1 .. t1_n` and `C2 t2_1 .. t2_m` (C1 and C2 are
2150 type constructors), it expands C1 and C2 if they're different type synonyms.
2151 Then it recursively does the same thing on expanded types. If C1 and C2 are
2152 same, then it applies the same procedure to arguments of C1 and arguments of
2153 C2 to make them as similar as possible.
2154
2155 Most important thing here is to keep number of synonym expansions at
2156 minimum. For example, if t1 is `T (T3, T5, Int)` and t2 is `T (T5, T3,
2157 Bool)` where T5 = T4, T4 = T3, ..., T1 = X, it returns `T (T3, T3, Int)` and
2158 `T (T3, T3, Bool)`.
2159
2160 * Otherwise types don't have same shapes and so the difference is clearly
2161 visible. It doesn't do any expansions and show these types.
2162
2163 Note that we only expand top-layer type synonyms. Only when top-layer
2164 constructors are the same we start expanding inner type synonyms.
2165
2166 Suppose top-layer type synonyms of t1 and t2 can expand N and M times,
2167 respectively. If their type-synonym-expanded forms will meet at some point (i.e.
2168 will have same shapes according to `sameShapes` function), it's possible to find
2169 where they meet in O(N+M) top-layer type synonym expansions and O(min(N,M))
2170 comparisons. We first collect all the top-layer expansions of t1 and t2 in two
2171 lists, then drop the prefix of the longer list so that they have same lengths.
2172 Then we search through both lists in parallel, and return the first pair of
2173 types that have same shapes. Inner types of these two types with same shapes
2174 are then expanded using the same algorithm.
2175
2176 In case they don't meet, we return the last pair of types in the lists, which
2177 has top-layer type synonyms completely expanded. (in this case the inner types
2178 are not expanded at all, as the current form already shows the type error)
2179 -}
2180
2181 -- | Expand type synonyms in given types only enough to make them as similar as
2182 -- possible. Returned types are the same in terms of used type synonyms.
2183 --
2184 -- To expand all synonyms, see 'Type.expandTypeSynonyms'.
2185 --
2186 -- See `ExpandSynsFail` tests in tests testsuite/tests/typecheck/should_fail for
2187 -- some examples of how this should work.
2188 expandSynonymsToMatch :: Type -> Type -> (Type, Type)
2189 expandSynonymsToMatch ty1 ty2 = (ty1_ret, ty2_ret)
2190 where
2191 (ty1_ret, ty2_ret) = go ty1 ty2
2192
2193 -- | Returns (type synonym expanded version of first type,
2194 -- type synonym expanded version of second type)
2195 go :: Type -> Type -> (Type, Type)
2196 go t1 t2
2197 | t1 `pickyEqType` t2 =
2198 -- Types are same, nothing to do
2199 (t1, t2)
2200
2201 go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
2202 | tc1 == tc2 =
2203 -- Type constructors are same. They may be synonyms, but we don't
2204 -- expand further.
2205 let (tys1', tys2') =
2206 unzip (zipWith (\ty1 ty2 -> go ty1 ty2) tys1 tys2)
2207 in (TyConApp tc1 tys1', TyConApp tc2 tys2')
2208
2209 go (AppTy t1_1 t1_2) (AppTy t2_1 t2_2) =
2210 let (t1_1', t2_1') = go t1_1 t2_1
2211 (t1_2', t2_2') = go t1_2 t2_2
2212 in (mkAppTy t1_1' t1_2', mkAppTy t2_1' t2_2')
2213
2214 go ty1@(FunTy _ t1_1 t1_2) ty2@(FunTy _ t2_1 t2_2) =
2215 let (t1_1', t2_1') = go t1_1 t2_1
2216 (t1_2', t2_2') = go t1_2 t2_2
2217 in ( ty1 { ft_arg = t1_1', ft_res = t1_2' }
2218 , ty2 { ft_arg = t2_1', ft_res = t2_2' })
2219
2220 go (ForAllTy b1 t1) (ForAllTy b2 t2) =
2221 -- NOTE: We may have a bug here, but we just can't reproduce it easily.
2222 -- See D1016 comments for details and our attempts at producing a test
2223 -- case. Short version: We probably need RnEnv2 to really get this right.
2224 let (t1', t2') = go t1 t2
2225 in (ForAllTy b1 t1', ForAllTy b2 t2')
2226
2227 go (CastTy ty1 _) ty2 = go ty1 ty2
2228 go ty1 (CastTy ty2 _) = go ty1 ty2
2229
2230 go t1 t2 =
2231 -- See Note [Expanding type synonyms to make types similar] for how this
2232 -- works
2233 let
2234 t1_exp_tys = t1 : tyExpansions t1
2235 t2_exp_tys = t2 : tyExpansions t2
2236 t1_exps = length t1_exp_tys
2237 t2_exps = length t2_exp_tys
2238 dif = abs (t1_exps - t2_exps)
2239 in
2240 followExpansions $
2241 zipEqual "expandSynonymsToMatch.go"
2242 (if t1_exps > t2_exps then drop dif t1_exp_tys else t1_exp_tys)
2243 (if t2_exps > t1_exps then drop dif t2_exp_tys else t2_exp_tys)
2244
2245 -- | Expand the top layer type synonyms repeatedly, collect expansions in a
2246 -- list. The list does not include the original type.
2247 --
2248 -- Example, if you have:
2249 --
2250 -- type T10 = T9
2251 -- type T9 = T8
2252 -- ...
2253 -- type T0 = Int
2254 --
2255 -- `tyExpansions T10` returns [T9, T8, T7, ... Int]
2256 --
2257 -- This only expands the top layer, so if you have:
2258 --
2259 -- type M a = Maybe a
2260 --
2261 -- `tyExpansions (M T10)` returns [Maybe T10] (T10 is not expanded)
2262 tyExpansions :: Type -> [Type]
2263 tyExpansions = unfoldr (\t -> (\x -> (x, x)) `fmap` tcView t)
2264
2265 -- | Drop the type pairs until types in a pair look alike (i.e. the outer
2266 -- constructors are the same).
2267 followExpansions :: [(Type, Type)] -> (Type, Type)
2268 followExpansions [] = pprPanic "followExpansions" empty
2269 followExpansions [(t1, t2)]
2270 | sameShapes t1 t2 = go t1 t2 -- expand subtrees
2271 | otherwise = (t1, t2) -- the difference is already visible
2272 followExpansions ((t1, t2) : tss)
2273 -- Traverse subtrees when the outer shapes are the same
2274 | sameShapes t1 t2 = go t1 t2
2275 -- Otherwise follow the expansions until they look alike
2276 | otherwise = followExpansions tss
2277
2278 sameShapes :: Type -> Type -> Bool
2279 sameShapes AppTy{} AppTy{} = True
2280 sameShapes (TyConApp tc1 _) (TyConApp tc2 _) = tc1 == tc2
2281 sameShapes (FunTy {}) (FunTy {}) = True
2282 sameShapes (ForAllTy {}) (ForAllTy {}) = True
2283 sameShapes (CastTy ty1 _) ty2 = sameShapes ty1 ty2
2284 sameShapes ty1 (CastTy ty2 _) = sameShapes ty1 ty2
2285 sameShapes _ _ = False
2286
2287 sameOccExtra :: TcType -> TcType -> SDoc
2288 -- See Note [Disambiguating (X ~ X) errors]
2289 sameOccExtra ty1 ty2
2290 | Just (tc1, _) <- tcSplitTyConApp_maybe ty1
2291 , Just (tc2, _) <- tcSplitTyConApp_maybe ty2
2292 , let n1 = tyConName tc1
2293 n2 = tyConName tc2
2294 same_occ = nameOccName n1 == nameOccName n2
2295 same_pkg = moduleUnitId (nameModule n1) == moduleUnitId (nameModule n2)
2296 , n1 /= n2 -- Different Names
2297 , same_occ -- but same OccName
2298 = text "NB:" <+> (ppr_from same_pkg n1 $$ ppr_from same_pkg n2)
2299 | otherwise
2300 = empty
2301 where
2302 ppr_from same_pkg nm
2303 | isGoodSrcSpan loc
2304 = hang (quotes (ppr nm) <+> text "is defined at")
2305 2 (ppr loc)
2306 | otherwise -- Imported things have an UnhelpfulSrcSpan
2307 = hang (quotes (ppr nm))
2308 2 (sep [ text "is defined in" <+> quotes (ppr (moduleName mod))
2309 , ppUnless (same_pkg || pkg == mainUnitId) $
2310 nest 4 $ text "in package" <+> quotes (ppr pkg) ])
2311 where
2312 pkg = moduleUnitId mod
2313 mod = nameModule nm
2314 loc = nameSrcSpan nm
2315
2316 {-
2317 Note [Suggest adding a type signature]
2318 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2319 The OutsideIn algorithm rejects GADT programs that don't have a principal
2320 type, and indeed some that do. Example:
2321 data T a where
2322 MkT :: Int -> T Int
2323
2324 f (MkT n) = n
2325
2326 Does this have type f :: T a -> a, or f :: T a -> Int?
2327 The error that shows up tends to be an attempt to unify an
2328 untouchable type variable. So suggestAddSig sees if the offending
2329 type variable is bound by an *inferred* signature, and suggests
2330 adding a declared signature instead.
2331
2332 This initially came up in #8968, concerning pattern synonyms.
2333
2334 Note [Disambiguating (X ~ X) errors]
2335 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2336 See #8278
2337
2338 Note [Reporting occurs-check errors]
2339 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2340 Given (a ~ [a]), if 'a' is a rigid type variable bound by a user-supplied
2341 type signature, then the best thing is to report that we can't unify
2342 a with [a], because a is a skolem variable. That avoids the confusing
2343 "occur-check" error message.
2344
2345 But nowadays when inferring the type of a function with no type signature,
2346 even if there are errors inside, we still generalise its signature and
2347 carry on. For example
2348 f x = x:x
2349 Here we will infer something like
2350 f :: forall a. a -> [a]
2351 with a deferred error of (a ~ [a]). So in the deferred unsolved constraint
2352 'a' is now a skolem, but not one bound by the programmer in the context!
2353 Here we really should report an occurs check.
2354
2355 So isUserSkolem distinguishes the two.
2356
2357 Note [Non-injective type functions]
2358 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2359 It's very confusing to get a message like
2360 Couldn't match expected type `Depend s'
2361 against inferred type `Depend s1'
2362 so mkTyFunInfoMsg adds:
2363 NB: `Depend' is type function, and hence may not be injective
2364
2365 Warn of loopy local equalities that were dropped.
2366
2367
2368 ************************************************************************
2369 * *
2370 Type-class errors
2371 * *
2372 ************************************************************************
2373 -}
2374
2375 mkDictErr :: ReportErrCtxt -> [Ct] -> TcM ErrMsg
2376 mkDictErr ctxt cts
2377 = ASSERT( not (null cts) )
2378 do { inst_envs <- tcGetInstEnvs
2379 ; let (ct1:_) = cts -- ct1 just for its location
2380 min_cts = elim_superclasses cts
2381 lookups = map (lookup_cls_inst inst_envs) min_cts
2382 (no_inst_cts, overlap_cts) = partition is_no_inst lookups
2383
2384 -- Report definite no-instance errors,
2385 -- or (iff there are none) overlap errors
2386 -- But we report only one of them (hence 'head') because they all
2387 -- have the same source-location origin, to try avoid a cascade
2388 -- of error from one location
2389 ; (ctxt, err) <- mk_dict_err ctxt (head (no_inst_cts ++ overlap_cts))
2390 ; mkErrorMsgFromCt ctxt ct1 (important err) }
2391 where
2392 no_givens = null (getUserGivens ctxt)
2393
2394 is_no_inst (ct, (matches, unifiers, _))
2395 = no_givens
2396 && null matches
2397 && (null unifiers || all (not . isAmbiguousTyVar) (tyCoVarsOfCtList ct))
2398
2399 lookup_cls_inst inst_envs ct
2400 -- Note [Flattening in error message generation]
2401 = (ct, lookupInstEnv True inst_envs clas (flattenTys emptyInScopeSet tys))
2402 where
2403 (clas, tys) = getClassPredTys (ctPred ct)
2404
2405
2406 -- When simplifying [W] Ord (Set a), we need
2407 -- [W] Eq a, [W] Ord a
2408 -- but we really only want to report the latter
2409 elim_superclasses cts = mkMinimalBySCs ctPred cts
2410
2411 mk_dict_err :: ReportErrCtxt -> (Ct, ClsInstLookupResult)
2412 -> TcM (ReportErrCtxt, SDoc)
2413 -- Report an overlap error if this class constraint results
2414 -- from an overlap (returning Left clas), otherwise return (Right pred)
2415 mk_dict_err ctxt@(CEC {cec_encl = implics}) (ct, (matches, unifiers, unsafe_overlapped))
2416 | null matches -- No matches but perhaps several unifiers
2417 = do { (ctxt, binds_msg, ct) <- relevantBindings True ctxt ct
2418 ; candidate_insts <- get_candidate_instances
2419 ; return (ctxt, cannot_resolve_msg ct candidate_insts binds_msg) }
2420
2421 | null unsafe_overlapped -- Some matches => overlap errors
2422 = return (ctxt, overlap_msg)
2423
2424 | otherwise
2425 = return (ctxt, safe_haskell_msg)
2426 where
2427 orig = ctOrigin ct
2428 pred = ctPred ct
2429 (clas, tys) = getClassPredTys pred
2430 ispecs = [ispec | (ispec, _) <- matches]
2431 unsafe_ispecs = [ispec | (ispec, _) <- unsafe_overlapped]
2432 useful_givens = discardProvCtxtGivens orig (getUserGivensFromImplics implics)
2433 -- useful_givens are the enclosing implications with non-empty givens,
2434 -- modulo the horrid discardProvCtxtGivens
2435
2436 get_candidate_instances :: TcM [ClsInst]
2437 -- See Note [Report candidate instances]
2438 get_candidate_instances
2439 | [ty] <- tys -- Only try for single-parameter classes
2440 = do { instEnvs <- tcGetInstEnvs
2441 ; return (filter (is_candidate_inst ty)
2442 (classInstances instEnvs clas)) }
2443 | otherwise = return []
2444
2445 is_candidate_inst ty inst -- See Note [Report candidate instances]
2446 | [other_ty] <- is_tys inst
2447 , Just (tc1, _) <- tcSplitTyConApp_maybe ty
2448 , Just (tc2, _) <- tcSplitTyConApp_maybe other_ty
2449 = let n1 = tyConName tc1
2450 n2 = tyConName tc2
2451 different_names = n1 /= n2
2452 same_occ_names = nameOccName n1 == nameOccName n2
2453 in different_names && same_occ_names
2454 | otherwise = False
2455
2456 cannot_resolve_msg :: Ct -> [ClsInst] -> SDoc -> SDoc
2457 cannot_resolve_msg ct candidate_insts binds_msg
2458 = vcat [ no_inst_msg
2459 , nest 2 extra_note
2460 , vcat (pp_givens useful_givens)
2461 , mb_patsyn_prov `orElse` empty
2462 , ppWhen (has_ambig_tvs && not (null unifiers && null useful_givens))
2463 (vcat [ ppUnless lead_with_ambig ambig_msg, binds_msg, potential_msg ])
2464
2465 , ppWhen (isNothing mb_patsyn_prov) $
2466 -- Don't suggest fixes for the provided context of a pattern
2467 -- synonym; the right fix is to bind more in the pattern
2468 show_fixes (ctxtFixes has_ambig_tvs pred implics
2469 ++ drv_fixes)
2470 , ppWhen (not (null candidate_insts))
2471 (hang (text "There are instances for similar types:")
2472 2 (vcat (map ppr candidate_insts))) ]
2473 -- See Note [Report candidate instances]
2474 where
2475 orig = ctOrigin ct
2476 -- See Note [Highlighting ambiguous type variables]
2477 lead_with_ambig = has_ambig_tvs && not (any isRuntimeUnkSkol ambig_tvs)
2478 && not (null unifiers) && null useful_givens
2479
2480 (has_ambig_tvs, ambig_msg) = mkAmbigMsg lead_with_ambig ct
2481 ambig_tvs = uncurry (++) (getAmbigTkvs ct)
2482
2483 no_inst_msg
2484 | lead_with_ambig
2485 = ambig_msg <+> pprArising orig
2486 $$ text "prevents the constraint" <+> quotes (pprParendType pred)
2487 <+> text "from being solved."
2488
2489 | null useful_givens
2490 = addArising orig $ text "No instance for"
2491 <+> pprParendType pred
2492
2493 | otherwise
2494 = addArising orig $ text "Could not deduce"
2495 <+> pprParendType pred
2496
2497 potential_msg
2498 = ppWhen (not (null unifiers) && want_potential orig) $
2499 sdocWithDynFlags $ \dflags ->
2500 getPprStyle $ \sty ->
2501 pprPotentials dflags sty potential_hdr unifiers
2502
2503 potential_hdr
2504 = vcat [ ppWhen lead_with_ambig $
2505 text "Probable fix: use a type annotation to specify what"
2506 <+> pprQuotedList ambig_tvs <+> text "should be."
2507 , text "These potential instance" <> plural unifiers
2508 <+> text "exist:"]
2509
2510 mb_patsyn_prov :: Maybe SDoc
2511 mb_patsyn_prov
2512 | not lead_with_ambig
2513 , ProvCtxtOrigin PSB{ psb_def = (dL->L _ pat) } <- orig
2514 = Just (vcat [ text "In other words, a successful match on the pattern"
2515 , nest 2 $ ppr pat
2516 , text "does not provide the constraint" <+> pprParendType pred ])
2517 | otherwise = Nothing
2518
2519 -- Report "potential instances" only when the constraint arises
2520 -- directly from the user's use of an overloaded function
2521 want_potential (TypeEqOrigin {}) = False
2522 want_potential _ = True
2523
2524 extra_note | any isFunTy (filterOutInvisibleTypes (classTyCon clas) tys)
2525 = text "(maybe you haven't applied a function to enough arguments?)"
2526 | className clas == typeableClassName -- Avoid mysterious "No instance for (Typeable T)
2527 , [_,ty] <- tys -- Look for (Typeable (k->*) (T k))
2528 , Just (tc,_) <- tcSplitTyConApp_maybe ty
2529 , not (isTypeFamilyTyCon tc)
2530 = hang (text "GHC can't yet do polykinded")
2531 2 (text "Typeable" <+>
2532 parens (ppr ty <+> dcolon <+> ppr (tcTypeKind ty)))
2533 | otherwise
2534 = empty
2535
2536 drv_fixes = case orig of
2537 DerivClauseOrigin -> [drv_fix False]
2538 StandAloneDerivOrigin -> [drv_fix True]
2539 DerivOriginDC _ _ standalone -> [drv_fix standalone]
2540 DerivOriginCoerce _ _ _ standalone -> [drv_fix standalone]
2541 _ -> []
2542
2543 drv_fix standalone_wildcard
2544 | standalone_wildcard
2545 = text "fill in the wildcard constraint yourself"
2546 | otherwise
2547 = hang (text "use a standalone 'deriving instance' declaration,")
2548 2 (text "so you can specify the instance context yourself")
2549
2550 -- Normal overlap error
2551 overlap_msg
2552 = ASSERT( not (null matches) )
2553 vcat [ addArising orig (text "Overlapping instances for"
2554 <+> pprType (mkClassPred clas tys))
2555
2556 , ppUnless (null matching_givens) $
2557 sep [text "Matching givens (or their superclasses):"
2558 , nest 2 (vcat matching_givens)]
2559
2560 , sdocWithDynFlags $ \dflags ->
2561 getPprStyle $ \sty ->
2562 pprPotentials dflags sty (text "Matching instances:") $
2563 ispecs ++ unifiers
2564
2565 , ppWhen (null matching_givens && isSingleton matches && null unifiers) $
2566 -- Intuitively, some given matched the wanted in their
2567 -- flattened or rewritten (from given equalities) form
2568 -- but the matcher can't figure that out because the
2569 -- constraints are non-flat and non-rewritten so we
2570 -- simply report back the whole given
2571 -- context. Accelerate Smart.hs showed this problem.
2572 sep [ text "There exists a (perhaps superclass) match:"
2573 , nest 2 (vcat (pp_givens useful_givens))]
2574
2575 , ppWhen (isSingleton matches) $
2576 parens (vcat [ text "The choice depends on the instantiation of" <+>
2577 quotes (pprWithCommas ppr (tyCoVarsOfTypesList tys))
2578 , ppWhen (null (matching_givens)) $
2579 vcat [ text "To pick the first instance above, use IncoherentInstances"
2580 , text "when compiling the other instance declarations"]
2581 ])]
2582
2583 matching_givens = mapMaybe matchable useful_givens
2584
2585 matchable implic@(Implic { ic_given = evvars, ic_info = skol_info })
2586 = case ev_vars_matching of
2587 [] -> Nothing
2588 _ -> Just $ hang (pprTheta ev_vars_matching)
2589 2 (sep [ text "bound by" <+> ppr skol_info
2590 , text "at" <+>
2591 ppr (tcl_loc (implicLclEnv implic)) ])
2592 where ev_vars_matching = [ pred
2593 | ev_var <- evvars
2594 , let pred = evVarPred ev_var
2595 , any can_match (pred : transSuperClasses pred) ]
2596 can_match pred
2597 = case getClassPredTys_maybe pred of
2598 Just (clas', tys') -> clas' == clas
2599 && isJust (tcMatchTys tys tys')
2600 Nothing -> False
2601
2602 -- Overlap error because of Safe Haskell (first
2603 -- match should be the most specific match)
2604 safe_haskell_msg
2605 = ASSERT( matches `lengthIs` 1 && not (null unsafe_ispecs) )
2606 vcat [ addArising orig (text "Unsafe overlapping instances for"
2607 <+> pprType (mkClassPred clas tys))
2608 , sep [text "The matching instance is:",
2609 nest 2 (pprInstance $ head ispecs)]
2610 , vcat [ text "It is compiled in a Safe module and as such can only"
2611 , text "overlap instances from the same module, however it"
2612 , text "overlaps the following instances from different" <+>
2613 text "modules:"
2614 , nest 2 (vcat [pprInstances $ unsafe_ispecs])
2615 ]
2616 ]
2617
2618
2619 ctxtFixes :: Bool -> PredType -> [Implication] -> [SDoc]
2620 ctxtFixes has_ambig_tvs pred implics
2621 | not has_ambig_tvs
2622 , isTyVarClassPred pred
2623 , (skol:skols) <- usefulContext implics pred
2624 , let what | null skols
2625 , SigSkol (PatSynCtxt {}) _ _ <- skol
2626 = text "\"required\""
2627 | otherwise
2628 = empty
2629 = [sep [ text "add" <+> pprParendType pred
2630 <+> text "to the" <+> what <+> text "context of"
2631 , nest 2 $ ppr_skol skol $$
2632 vcat [ text "or" <+> ppr_skol skol
2633 | skol <- skols ] ] ]
2634 | otherwise = []
2635 where
2636 ppr_skol (PatSkol (RealDataCon dc) _) = text "the data constructor" <+> quotes (ppr dc)
2637 ppr_skol (PatSkol (PatSynCon ps) _) = text "the pattern synonym" <+> quotes (ppr ps)
2638 ppr_skol skol_info = ppr skol_info
2639
2640 discardProvCtxtGivens :: CtOrigin -> [UserGiven] -> [UserGiven]
2641 discardProvCtxtGivens orig givens -- See Note [discardProvCtxtGivens]
2642 | ProvCtxtOrigin (PSB {psb_id = (dL->L _ name)}) <- orig
2643 = filterOut (discard name) givens
2644 | otherwise
2645 = givens
2646 where
2647 discard n (Implic { ic_info = SigSkol (PatSynCtxt n') _ _ }) = n == n'
2648 discard _ _ = False
2649
2650 usefulContext :: [Implication] -> PredType -> [SkolemInfo]
2651 -- usefulContext picks out the implications whose context
2652 -- the programmer might plausibly augment to solve 'pred'
2653 usefulContext implics pred
2654 = go implics
2655 where
2656 pred_tvs = tyCoVarsOfType pred
2657 go [] = []
2658 go (ic : ics)
2659 | implausible ic = rest
2660 | otherwise = ic_info ic : rest
2661 where
2662 -- Stop when the context binds a variable free in the predicate
2663 rest | any (`elemVarSet` pred_tvs) (ic_skols ic) = []
2664 | otherwise = go ics
2665
2666 implausible ic
2667 | null (ic_skols ic) = True
2668 | implausible_info (ic_info ic) = True
2669 | otherwise = False
2670
2671 implausible_info (SigSkol (InfSigCtxt {}) _ _) = True
2672 implausible_info _ = False
2673 -- Do not suggest adding constraints to an *inferred* type signature
2674
2675 {- Note [Report candidate instances]
2676 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2677 If we have an unsolved (Num Int), where `Int` is not the Prelude Int,
2678 but comes from some other module, then it may be helpful to point out
2679 that there are some similarly named instances elsewhere. So we get
2680 something like
2681 No instance for (Num Int) arising from the literal ‘3’
2682 There are instances for similar types:
2683 instance Num GHC.Types.Int -- Defined in ‘GHC.Num’
2684 Discussion in #9611.
2685
2686 Note [Highlighting ambiguous type variables]
2687 ~-------------------------------------------
2688 When we encounter ambiguous type variables (i.e. type variables
2689 that remain metavariables after type inference), we need a few more
2690 conditions before we can reason that *ambiguity* prevents constraints
2691 from being solved:
2692 - We can't have any givens, as encountering a typeclass error
2693 with given constraints just means we couldn't deduce
2694 a solution satisfying those constraints and as such couldn't
2695 bind the type variable to a known type.
2696 - If we don't have any unifiers, we don't even have potential
2697 instances from which an ambiguity could arise.
2698 - Lastly, I don't want to mess with error reporting for
2699 unknown runtime types so we just fall back to the old message there.
2700 Once these conditions are satisfied, we can safely say that ambiguity prevents
2701 the constraint from being solved.
2702
2703 Note [discardProvCtxtGivens]
2704 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
2705 In most situations we call all enclosing implications "useful". There is one
2706 exception, and that is when the constraint that causes the error is from the
2707 "provided" context of a pattern synonym declaration:
2708
2709 pattern Pat :: (Num a, Eq a) => Show a => a -> Maybe a
2710 -- required => provided => type
2711 pattern Pat x <- (Just x, 4)
2712
2713 When checking the pattern RHS we must check that it does actually bind all
2714 the claimed "provided" constraints; in this case, does the pattern (Just x, 4)
2715 bind the (Show a) constraint. Answer: no!
2716
2717 But the implication we generate for this will look like
2718 forall a. (Num a, Eq a) => [W] Show a
2719 because when checking the pattern we must make the required
2720 constraints available, since they are needed to match the pattern (in
2721 this case the literal '4' needs (Num a, Eq a)).
2722
2723 BUT we don't want to suggest adding (Show a) to the "required" constraints
2724 of the pattern synonym, thus:
2725 pattern Pat :: (Num a, Eq a, Show a) => Show a => a -> Maybe a
2726 It would then typecheck but it's silly. We want the /pattern/ to bind
2727 the alleged "provided" constraints, Show a.
2728
2729 So we suppress that Implication in discardProvCtxtGivens. It's
2730 painfully ad-hoc but the truth is that adding it to the "required"
2731 constraints would work. Suppressing it solves two problems. First,
2732 we never tell the user that we could not deduce a "provided"
2733 constraint from the "required" context. Second, we never give a
2734 possible fix that suggests to add a "provided" constraint to the
2735 "required" context.
2736
2737 For example, without this distinction the above code gives a bad error
2738 message (showing both problems):
2739
2740 error: Could not deduce (Show a) ... from the context: (Eq a)
2741 ... Possible fix: add (Show a) to the context of
2742 the signature for pattern synonym `Pat' ...
2743
2744 -}
2745
2746 show_fixes :: [SDoc] -> SDoc
2747 show_fixes [] = empty
2748 show_fixes (f:fs) = sep [ text "Possible fix:"
2749 , nest 2 (vcat (f : map (text "or" <+>) fs))]
2750
2751 pprPotentials :: DynFlags -> PprStyle -> SDoc -> [ClsInst] -> SDoc
2752 -- See Note [Displaying potential instances]
2753 pprPotentials dflags sty herald insts
2754 | null insts
2755 = empty
2756
2757 | null show_these
2758 = hang herald
2759 2 (vcat [ not_in_scope_msg empty
2760 , flag_hint ])
2761
2762 | otherwise
2763 = hang herald
2764 2 (vcat [ pprInstances show_these
2765 , ppWhen (n_in_scope_hidden > 0) $
2766 text "...plus"
2767 <+> speakNOf n_in_scope_hidden (text "other")
2768 , not_in_scope_msg (text "...plus")
2769 , flag_hint ])
2770 where
2771 n_show = 3 :: Int
2772 show_potentials = gopt Opt_PrintPotentialInstances dflags
2773
2774 (in_scope, not_in_scope) = partition inst_in_scope insts
2775 sorted = sortBy fuzzyClsInstCmp in_scope
2776 show_these | show_potentials = sorted
2777 | otherwise = take n_show sorted
2778 n_in_scope_hidden = length sorted - length show_these
2779
2780 -- "in scope" means that all the type constructors
2781 -- are lexically in scope; these instances are likely
2782 -- to be more useful
2783 inst_in_scope :: ClsInst -> Bool
2784 inst_in_scope cls_inst = nameSetAll name_in_scope $
2785 orphNamesOfTypes (is_tys cls_inst)
2786
2787 name_in_scope name
2788 | isBuiltInSyntax name
2789 = True -- E.g. (->)
2790 | Just mod <- nameModule_maybe name
2791 = qual_in_scope (qualName sty mod (nameOccName name))
2792 | otherwise
2793 = True
2794
2795 qual_in_scope :: QualifyName -> Bool
2796 qual_in_scope NameUnqual = True
2797 qual_in_scope (NameQual {}) = True
2798 qual_in_scope _ = False
2799
2800 not_in_scope_msg herald
2801 | null not_in_scope
2802 = empty
2803 | otherwise
2804 = hang (herald <+> speakNOf (length not_in_scope) (text "instance")
2805 <+> text "involving out-of-scope types")
2806 2 (ppWhen show_potentials (pprInstances not_in_scope))
2807
2808 flag_hint = ppUnless (show_potentials || equalLength show_these insts) $
2809 text "(use -fprint-potential-instances to see them all)"
2810
2811 {- Note [Displaying potential instances]
2812 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2813 When showing a list of instances for
2814 - overlapping instances (show ones that match)
2815 - no such instance (show ones that could match)
2816 we want to give it a bit of structure. Here's the plan
2817
2818 * Say that an instance is "in scope" if all of the
2819 type constructors it mentions are lexically in scope.
2820 These are the ones most likely to be useful to the programmer.
2821
2822 * Show at most n_show in-scope instances,
2823 and summarise the rest ("plus 3 others")
2824
2825 * Summarise the not-in-scope instances ("plus 4 not in scope")
2826
2827 * Add the flag -fshow-potential-instances which replaces the
2828 summary with the full list
2829 -}
2830
2831 {-
2832 Note [Flattening in error message generation]
2833 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2834 Consider (C (Maybe (F x))), where F is a type function, and we have
2835 instances
2836 C (Maybe Int) and C (Maybe a)
2837 Since (F x) might turn into Int, this is an overlap situation, and
2838 indeed (because of flattening) the main solver will have refrained
2839 from solving. But by the time we get to error message generation, we've
2840 un-flattened the constraint. So we must *re*-flatten it before looking
2841 up in the instance environment, lest we only report one matching
2842 instance when in fact there are two.
2843
2844 Re-flattening is pretty easy, because we don't need to keep track of
2845 evidence. We don't re-use the code in TcCanonical because that's in
2846 the TcS monad, and we are in TcM here.
2847
2848 Note [Kind arguments in error messages]
2849 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2850 It can be terribly confusing to get an error message like (#9171)
2851
2852 Couldn't match expected type ‘GetParam Base (GetParam Base Int)’
2853 with actual type ‘GetParam Base (GetParam Base Int)’
2854
2855 The reason may be that the kinds don't match up. Typically you'll get
2856 more useful information, but not when it's as a result of ambiguity.
2857
2858 To mitigate this, GHC attempts to enable the -fprint-explicit-kinds flag
2859 whenever any error message arises due to a kind mismatch. This means that
2860 the above error message would instead be displayed as:
2861
2862 Couldn't match expected type
2863 ‘GetParam @* @k2 @* Base (GetParam @* @* @k2 Base Int)’
2864 with actual type
2865 ‘GetParam @* @k20 @* Base (GetParam @* @* @k20 Base Int)’
2866
2867 Which makes it clearer that the culprit is the mismatch between `k2` and `k20`.
2868 -}
2869
2870 mkAmbigMsg :: Bool -- True when message has to be at beginning of sentence
2871 -> Ct -> (Bool, SDoc)
2872 mkAmbigMsg prepend_msg ct
2873 | null ambig_kvs && null ambig_tvs = (False, empty)
2874 | otherwise = (True, msg)
2875 where
2876 (ambig_kvs, ambig_tvs) = getAmbigTkvs ct
2877
2878 msg | any isRuntimeUnkSkol ambig_kvs -- See Note [Runtime skolems]
2879 || any isRuntimeUnkSkol ambig_tvs
2880 = vcat [ text "Cannot resolve unknown runtime type"
2881 <> plural ambig_tvs <+> pprQuotedList ambig_tvs
2882 , text "Use :print or :force to determine these types"]
2883
2884 | not (null ambig_tvs)
2885 = pp_ambig (text "type") ambig_tvs
2886
2887 | otherwise
2888 = pp_ambig (text "kind") ambig_kvs
2889
2890 pp_ambig what tkvs
2891 | prepend_msg -- "Ambiguous type variable 't0'"
2892 = text "Ambiguous" <+> what <+> text "variable"
2893 <> plural tkvs <+> pprQuotedList tkvs
2894
2895 | otherwise -- "The type variable 't0' is ambiguous"
2896 = text "The" <+> what <+> text "variable" <> plural tkvs
2897 <+> pprQuotedList tkvs <+> is_or_are tkvs <+> text "ambiguous"
2898
2899 is_or_are [_] = text "is"
2900 is_or_are _ = text "are"
2901
2902 pprSkols :: ReportErrCtxt -> [TcTyVar] -> SDoc
2903 pprSkols ctxt tvs
2904 = vcat (map pp_one (getSkolemInfo (cec_encl ctxt) tvs))
2905 where
2906 pp_one (Implic { ic_info = skol_info }, tvs)
2907 | UnkSkol <- skol_info
2908 = hang (pprQuotedList tvs)
2909 2 (is_or_are tvs "an" "unknown")
2910 | otherwise
2911 = vcat [ hang (pprQuotedList tvs)
2912 2 (is_or_are tvs "a" "rigid" <+> text "bound by")
2913 , nest 2 (pprSkolInfo skol_info)
2914 , nest 2 (text "at" <+> ppr (foldr1 combineSrcSpans (map getSrcSpan tvs))) ]
2915
2916 is_or_are [_] article adjective = text "is" <+> text article <+> text adjective
2917 <+> text "type variable"
2918 is_or_are _ _ adjective = text "are" <+> text adjective
2919 <+> text "type variables"
2920
2921 getAmbigTkvs :: Ct -> ([Var],[Var])
2922 getAmbigTkvs ct
2923 = partition (`elemVarSet` dep_tkv_set) ambig_tkvs
2924 where
2925 tkvs = tyCoVarsOfCtList ct
2926 ambig_tkvs = filter isAmbiguousTyVar tkvs
2927 dep_tkv_set = tyCoVarsOfTypes (map tyVarKind tkvs)
2928
2929 getSkolemInfo :: [Implication] -> [TcTyVar]
2930 -> [(Implication, [TcTyVar])]
2931 -- Get the skolem info for some type variables
2932 -- from the implication constraints that bind them
2933 --
2934 -- In the returned (implic, tvs) pairs, the 'tvs' part is non-empty
2935 getSkolemInfo _ []
2936 = []
2937
2938 getSkolemInfo [] tvs
2939 = pprPanic "No skolem info:" (ppr tvs)
2940
2941 getSkolemInfo (implic:implics) tvs
2942 | null tvs_here = getSkolemInfo implics tvs
2943 | otherwise = (implic, tvs_here) : getSkolemInfo implics tvs_other
2944 where
2945 (tvs_here, tvs_other) = partition (`elem` ic_skols implic) tvs
2946
2947 -----------------------
2948 -- relevantBindings looks at the value environment and finds values whose
2949 -- types mention any of the offending type variables. It has to be
2950 -- careful to zonk the Id's type first, so it has to be in the monad.
2951 -- We must be careful to pass it a zonked type variable, too.
2952 --
2953 -- We always remove closed top-level bindings, though,
2954 -- since they are never relevant (cf #8233)
2955
2956 relevantBindings :: Bool -- True <=> filter by tyvar; False <=> no filtering
2957 -- See #8191
2958 -> ReportErrCtxt -> Ct
2959 -> TcM (ReportErrCtxt, SDoc, Ct)
2960 -- Also returns the zonked and tidied CtOrigin of the constraint
2961 relevantBindings want_filtering ctxt ct
2962 = do { dflags <- getDynFlags
2963 ; (env1, tidy_orig) <- zonkTidyOrigin (cec_tidy ctxt) (ctLocOrigin loc)
2964 ; let ct_tvs = tyCoVarsOfCt ct `unionVarSet` extra_tvs
2965
2966 -- For *kind* errors, report the relevant bindings of the
2967 -- enclosing *type* equality, because that's more useful for the programmer
2968 extra_tvs = case tidy_orig of
2969 KindEqOrigin t1 m_t2 _ _ -> tyCoVarsOfTypes $
2970 t1 : maybeToList m_t2
2971 _ -> emptyVarSet
2972 ; traceTc "relevantBindings" $
2973 vcat [ ppr ct
2974 , pprCtOrigin (ctLocOrigin loc)
2975 , ppr ct_tvs
2976 , pprWithCommas id [ ppr id <+> dcolon <+> ppr (idType id)
2977 | TcIdBndr id _ <- tcl_bndrs lcl_env ]
2978 , pprWithCommas id
2979 [ ppr id | TcIdBndr_ExpType id _ _ <- tcl_bndrs lcl_env ] ]
2980
2981 ; (tidy_env', docs, discards)
2982 <- go dflags env1 ct_tvs (maxRelevantBinds dflags)
2983 emptyVarSet [] False
2984 (removeBindingShadowing $ tcl_bndrs lcl_env)
2985 -- tcl_bndrs has the innermost bindings first,
2986 -- which are probably the most relevant ones
2987
2988 ; let doc = ppUnless (null docs) $
2989 hang (text "Relevant bindings include")
2990 2 (vcat docs $$ ppWhen discards discardMsg)
2991
2992 -- Put a zonked, tidied CtOrigin into the Ct
2993 loc' = setCtLocOrigin loc tidy_orig
2994 ct' = setCtLoc ct loc'
2995 ctxt' = ctxt { cec_tidy = tidy_env' }
2996
2997 ; return (ctxt', doc, ct') }
2998 where
2999 ev = ctEvidence ct
3000 loc = ctEvLoc ev
3001 lcl_env = ctLocEnv loc
3002
3003 run_out :: Maybe Int -> Bool
3004 run_out Nothing = False
3005 run_out (Just n) = n <= 0
3006
3007 dec_max :: Maybe Int -> Maybe Int
3008 dec_max = fmap (\n -> n - 1)
3009
3010
3011 go :: DynFlags -> TidyEnv -> TcTyVarSet -> Maybe Int -> TcTyVarSet -> [SDoc]
3012 -> Bool -- True <=> some filtered out due to lack of fuel
3013 -> [TcBinder]
3014 -> TcM (TidyEnv, [SDoc], Bool) -- The bool says if we filtered any out
3015 -- because of lack of fuel
3016 go _ tidy_env _ _ _ docs discards []
3017 = return (tidy_env, reverse docs, discards)
3018 go dflags tidy_env ct_tvs n_left tvs_seen docs discards (tc_bndr : tc_bndrs)
3019 = case tc_bndr of
3020 TcTvBndr {} -> discard_it
3021 TcIdBndr id top_lvl -> go2 (idName id) (idType id) top_lvl
3022 TcIdBndr_ExpType name et top_lvl ->
3023 do { mb_ty <- readExpType_maybe et
3024 -- et really should be filled in by now. But there's a chance
3025 -- it hasn't, if, say, we're reporting a kind error en route to
3026 -- checking a term. See test indexed-types/should_fail/T8129
3027 -- Or we are reporting errors from the ambiguity check on
3028 -- a local type signature
3029 ; case mb_ty of
3030 Just ty -> go2 name ty top_lvl
3031 Nothing -> discard_it -- No info; discard
3032 }
3033 where
3034 discard_it = go dflags tidy_env ct_tvs n_left tvs_seen docs
3035 discards tc_bndrs
3036 go2 id_name id_type top_lvl
3037 = do { (tidy_env', tidy_ty) <- zonkTidyTcType tidy_env id_type
3038 ; traceTc "relevantBindings 1" (ppr id_name <+> dcolon <+> ppr tidy_ty)
3039 ; let id_tvs = tyCoVarsOfType tidy_ty
3040 doc = sep [ pprPrefixOcc id_name <+> dcolon <+> ppr tidy_ty
3041 , nest 2 (parens (text "bound at"
3042 <+> ppr (getSrcLoc id_name)))]
3043 new_seen = tvs_seen `unionVarSet` id_tvs
3044
3045 ; if (want_filtering && not (hasPprDebug dflags)
3046 && id_tvs `disjointVarSet` ct_tvs)
3047 -- We want to filter out this binding anyway
3048 -- so discard it silently
3049 then discard_it
3050
3051 else if isTopLevel top_lvl && not (isNothing n_left)
3052 -- It's a top-level binding and we have not specified
3053 -- -fno-max-relevant-bindings, so discard it silently
3054 then discard_it
3055
3056 else if run_out n_left && id_tvs `subVarSet` tvs_seen
3057 -- We've run out of n_left fuel and this binding only
3058 -- mentions already-seen type variables, so discard it
3059 then go dflags tidy_env ct_tvs n_left tvs_seen docs
3060 True -- Record that we have now discarded something
3061 tc_bndrs
3062
3063 -- Keep this binding, decrement fuel
3064 else go dflags tidy_env' ct_tvs (dec_max n_left) new_seen
3065 (doc:docs) discards tc_bndrs }
3066
3067
3068 discardMsg :: SDoc
3069 discardMsg = text "(Some bindings suppressed;" <+>
3070 text "use -fmax-relevant-binds=N or -fno-max-relevant-binds)"
3071
3072 -----------------------
3073 warnDefaulting :: [Ct] -> Type -> TcM ()
3074 warnDefaulting wanteds default_ty
3075 = do { warn_default <- woptM Opt_WarnTypeDefaults
3076 ; env0 <- tcInitTidyEnv
3077 ; let tidy_env = tidyFreeTyCoVars env0 $
3078 tyCoVarsOfCtsList (listToBag wanteds)
3079 tidy_wanteds = map (tidyCt tidy_env) wanteds
3080 (loc, ppr_wanteds) = pprWithArising tidy_wanteds
3081 warn_msg =
3082 hang (hsep [ text "Defaulting the following"
3083 , text "constraint" <> plural tidy_wanteds
3084 , text "to type"
3085 , quotes (ppr default_ty) ])
3086 2
3087 ppr_wanteds
3088 ; setCtLocM loc $ warnTc (Reason Opt_WarnTypeDefaults) warn_default warn_msg }
3089
3090 {-
3091 Note [Runtime skolems]
3092 ~~~~~~~~~~~~~~~~~~~~~~
3093 We want to give a reasonably helpful error message for ambiguity
3094 arising from *runtime* skolems in the debugger. These
3095 are created by in RtClosureInspect.zonkRTTIType.
3096
3097 ************************************************************************
3098 * *
3099 Error from the canonicaliser
3100 These ones are called *during* constraint simplification
3101 * *
3102 ************************************************************************
3103 -}
3104
3105 solverDepthErrorTcS :: CtLoc -> TcType -> TcM a
3106 solverDepthErrorTcS loc ty
3107 = setCtLocM loc $
3108 do { ty <- zonkTcType ty
3109 ; env0 <- tcInitTidyEnv
3110 ; let tidy_env = tidyFreeTyCoVars env0 (tyCoVarsOfTypeList ty)
3111 tidy_ty = tidyType tidy_env ty
3112 msg
3113 = vcat [ text "Reduction stack overflow; size =" <+> ppr depth
3114 , hang (text "When simplifying the following type:")
3115 2 (ppr tidy_ty)
3116 , note ]
3117 ; failWithTcM (tidy_env, msg) }
3118 where
3119 depth = ctLocDepth loc
3120 note = vcat
3121 [ text "Use -freduction-depth=0 to disable this check"
3122 , text "(any upper bound you could choose might fail unpredictably with"
3123 , text " minor updates to GHC, so disabling the check is recommended if"
3124 , text " you're sure that type checking should terminate)" ]