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