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