Refactor the typechecker to use ExpTypes.
[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 TcType
16 import RnEnv( unknownNameSuggestions )
17 import Type
18 import TyCoRep
19 import Kind
20 import Unify ( tcMatchTys )
21 import Module
22 import FamInst
23 import FamInstEnv ( flattenTys )
24 import Inst
25 import InstEnv
26 import TyCon
27 import Class
28 import DataCon
29 import TcEvidence
30 import Name
31 import RdrName ( lookupGRE_Name, GlobalRdrEnv, mkRdrUnqual )
32 import PrelNames ( typeableClassName, hasKey
33 , liftedDataConKey, unliftedDataConKey )
34 import Id
35 import Var
36 import VarSet
37 import VarEnv
38 import NameSet
39 import Bag
40 import ErrUtils ( ErrMsg, errDoc, pprLocErrMsg )
41 import BasicTypes
42 import Util
43 import FastString
44 import Outputable
45 import SrcLoc
46 import DynFlags
47 import StaticFlags ( opt_PprStyle_Debug )
48 import ListSetOps ( equivClasses )
49 import Maybes
50 import qualified GHC.LanguageExtensions as LangExt
51
52 import Control.Monad ( when )
53 import Data.List ( partition, mapAccumL, nub, sortBy )
54
55 #if __GLASGOW_HASKELL__ > 710
56 import Data.Semigroup ( Semigroup )
57 import qualified Data.Semigroup as Semigroup
58 #endif
59
60
61 {-
62 ************************************************************************
63 * *
64 \section{Errors and contexts}
65 * *
66 ************************************************************************
67
68 ToDo: for these error messages, should we note the location as coming
69 from the insts, or just whatever seems to be around in the monad just
70 now?
71
72 Note [Deferring coercion errors to runtime]
73 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
74 While developing, sometimes it is desirable to allow compilation to succeed even
75 if there are type errors in the code. Consider the following case:
76
77 module Main where
78
79 a :: Int
80 a = 'a'
81
82 main = print "b"
83
84 Even though `a` is ill-typed, it is not used in the end, so if all that we're
85 interested in is `main` it is handy to be able to ignore the problems in `a`.
86
87 Since we treat type equalities as evidence, this is relatively simple. Whenever
88 we run into a type mismatch in TcUnify, we normally just emit an error. But it
89 is always safe to defer the mismatch to the main constraint solver. If we do
90 that, `a` will get transformed into
91
92 co :: Int ~ Char
93 co = ...
94
95 a :: Int
96 a = 'a' `cast` co
97
98 The constraint solver would realize that `co` is an insoluble constraint, and
99 emit an error with `reportUnsolved`. But we can also replace the right-hand side
100 of `co` with `error "Deferred type error: Int ~ Char"`. This allows the program
101 to compile, and it will run fine unless we evaluate `a`. This is what
102 `deferErrorsToRuntime` does.
103
104 It does this by keeping track of which errors correspond to which coercion
105 in TcErrors. TcErrors.reportTidyWanteds does not print the errors
106 and does not fail if -fdefer-type-errors is on, so that we can continue
107 compilation. The errors are turned into warnings in `reportUnsolved`.
108 -}
109
110 -- | Report unsolved goals as errors or warnings. We may also turn some into
111 -- deferred run-time errors if `-fdefer-type-errors` is on.
112 reportUnsolved :: WantedConstraints -> TcM (Bag EvBind)
113 reportUnsolved wanted
114 = do { binds_var <- newTcEvBinds
115 ; defer_errors <- goptM Opt_DeferTypeErrors
116 ; warn_errors <- woptM Opt_WarnDeferredTypeErrors -- implement #10283
117 ; let type_errors | not defer_errors = TypeError
118 | warn_errors = TypeWarn
119 | otherwise = TypeDefer
120
121 ; defer_holes <- goptM Opt_DeferTypedHoles
122 ; warn_holes <- woptM Opt_WarnTypedHoles
123 ; let expr_holes | not defer_holes = HoleError
124 | warn_holes = HoleWarn
125 | otherwise = HoleDefer
126
127 ; partial_sigs <- xoptM LangExt.PartialTypeSignatures
128 ; warn_partial_sigs <- woptM Opt_WarnPartialTypeSignatures
129 ; let type_holes | not partial_sigs = HoleError
130 | warn_partial_sigs = HoleWarn
131 | otherwise = HoleDefer
132
133 ; report_unsolved (Just binds_var) False type_errors expr_holes type_holes wanted
134 ; getTcEvBinds binds_var }
135
136 -- | Report *all* unsolved goals as errors, even if -fdefer-type-errors is on
137 -- See Note [Deferring coercion errors to runtime]
138 reportAllUnsolved :: WantedConstraints -> TcM ()
139 reportAllUnsolved wanted
140 = report_unsolved Nothing False TypeError HoleError HoleError wanted
141
142 -- | Report all unsolved goals as warnings (but without deferring any errors to
143 -- run-time). See Note [Safe Haskell Overlapping Instances Implementation] in
144 -- TcSimplify
145 warnAllUnsolved :: WantedConstraints -> TcM ()
146 warnAllUnsolved wanted
147 = report_unsolved Nothing True TypeWarn HoleWarn HoleWarn wanted
148
149 -- | Report unsolved goals as errors or warnings.
150 report_unsolved :: Maybe EvBindsVar -- cec_binds
151 -> Bool -- Errors as warnings
152 -> TypeErrorChoice -- Deferred type errors
153 -> HoleChoice -- Expression holes
154 -> HoleChoice -- Type holes
155 -> WantedConstraints -> TcM ()
156 report_unsolved mb_binds_var err_as_warn type_errors expr_holes type_holes wanted
157 | isEmptyWC wanted
158 = return ()
159 | otherwise
160 = do { traceTc "reportUnsolved (before zonking and tidying)" (ppr wanted)
161
162 ; wanted <- zonkWC wanted -- Zonk to reveal all information
163 ; env0 <- tcInitTidyEnv
164 -- If we are deferring we are going to need /all/ evidence around,
165 -- including the evidence produced by unflattening (zonkWC)
166 ; let tidy_env = tidyFreeTyCoVars env0 free_tvs
167 free_tvs = tyCoVarsOfWC wanted
168
169 ; traceTc "reportUnsolved (after zonking and tidying):" $
170 vcat [ pprTvBndrs (varSetElems free_tvs)
171 , ppr wanted ]
172
173 ; warn_redundant <- woptM Opt_WarnRedundantConstraints
174 ; let err_ctxt = CEC { cec_encl = []
175 , cec_tidy = tidy_env
176 , cec_defer_type_errors = type_errors
177 , cec_errors_as_warns = err_as_warn
178 , cec_expr_holes = expr_holes
179 , cec_type_holes = type_holes
180 , cec_suppress = False -- See Note [Suppressing error messages]
181 , cec_warn_redundant = warn_redundant
182 , cec_binds = mb_binds_var }
183
184 ; tc_lvl <- getTcLevel
185 ; reportWanteds err_ctxt tc_lvl wanted }
186
187 --------------------------------------------
188 -- Internal functions
189 --------------------------------------------
190
191 -- | An error Report collects messages categorised by their importance.
192 -- See Note [Error report] for details.
193 data Report
194 = Report { report_important :: [SDoc]
195 , report_relevant_bindings :: [SDoc]
196 }
197
198 {- Note [Error report]
199 The idea is that error msgs are divided into three parts: the main msg, the
200 context block (\"In the second argument of ...\"), and the relevant bindings
201 block, which are displayed in that order, with a mark to divide them. The
202 idea is that the main msg ('report_important') varies depending on the error
203 in question, but context and relevant bindings are always the same, which
204 should simplify visual parsing.
205
206 The context is added when the the Report is passed off to 'mkErrorReport'.
207 Unfortunately, unlike the context, the relevant bindings are added in
208 multiple places so they have to be in the Report.
209 -}
210
211 #if __GLASGOW_HASKELL__ > 710
212 instance Semigroup Report where
213 Report a1 b1 <> Report a2 b2 = Report (a1 ++ a2) (b1 ++ b2)
214 #endif
215
216 instance Monoid Report where
217 mempty = Report [] []
218 mappend (Report a1 b1) (Report a2 b2) = Report (a1 ++ a2) (b1 ++ b2)
219
220 -- | Put a doc into the important msgs block.
221 important :: SDoc -> Report
222 important doc = mempty { report_important = [doc] }
223
224 -- | Put a doc into the relevant bindings block.
225 relevant_bindings :: SDoc -> Report
226 relevant_bindings doc = mempty { report_relevant_bindings = [doc] }
227
228 data TypeErrorChoice -- What to do for type errors found by the type checker
229 = TypeError -- A type error aborts compilation with an error message
230 | TypeWarn -- A type error is deferred to runtime, plus a compile-time warning
231 | TypeDefer -- A type error is deferred to runtime; no error or warning at compile time
232
233 data HoleChoice
234 = HoleError -- A hole is a compile-time error
235 | HoleWarn -- Defer to runtime, emit a compile-time warning
236 | HoleDefer -- Defer to runtime, no warning
237
238 data ReportErrCtxt
239 = CEC { cec_encl :: [Implication] -- Enclosing implications
240 -- (innermost first)
241 -- ic_skols and givens are tidied, rest are not
242 , cec_tidy :: TidyEnv
243 , cec_binds :: Maybe EvBindsVar
244 -- Nothinng <=> Report all errors, including holes; no bindings
245 -- Just ev <=> make some errors (depending on cec_defer)
246 -- into warnings, and emit evidence bindings
247 -- into 'ev' for unsolved constraints
248
249 , cec_errors_as_warns :: Bool -- Turn all errors into warnings
250 -- (except for Holes, which are
251 -- controlled by cec_type_holes and
252 -- cec_expr_holes)
253 , cec_defer_type_errors :: TypeErrorChoice -- Defer type errors until runtime
254 -- Irrelevant if cec_binds = Nothing
255
256 , cec_expr_holes :: HoleChoice -- Holes in expressions
257 , cec_type_holes :: HoleChoice -- Holes in types
258
259 , cec_warn_redundant :: Bool -- True <=> -Wredundant-constraints
260
261 , cec_suppress :: Bool -- True <=> More important errors have occurred,
262 -- so create bindings if need be, but
263 -- don't issue any more errors/warnings
264 -- See Note [Suppressing error messages]
265 }
266
267 {-
268 Note [Suppressing error messages]
269 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
270 The cec_suppress flag says "don't report any errors". Instead, just create
271 evidence bindings (as usual). It's used when more important errors have occurred.
272
273 Specifically (see reportWanteds)
274 * If there are insoluble Givens, then we are in unreachable code and all bets
275 are off. So don't report any further errors.
276 * If there are any insolubles (eg Int~Bool), here or in a nested implication,
277 then suppress errors from the simple constraints here. Sometimes the
278 simple-constraint errors are a knock-on effect of the insolubles.
279 -}
280
281 reportImplic :: ReportErrCtxt -> Implication -> TcM ()
282 reportImplic ctxt implic@(Implic { ic_skols = tvs, ic_given = given
283 , ic_wanted = wanted, ic_binds = m_evb
284 , ic_status = status, ic_info = info
285 , ic_env = tcl_env, ic_tclvl = tc_lvl })
286 | BracketSkol <- info
287 , not insoluble
288 = return () -- For Template Haskell brackets report only
289 -- definite errors. The whole thing will be re-checked
290 -- later when we plug it in, and meanwhile there may
291 -- certainly be un-satisfied constraints
292
293 | otherwise
294 = do { reportWanteds ctxt' tc_lvl wanted
295 ; traceTc "reportImplic" (ppr implic)
296 ; when (cec_warn_redundant ctxt) $
297 warnRedundantConstraints ctxt' tcl_env info' dead_givens }
298 where
299 insoluble = isInsolubleStatus status
300 (env1, tvs') = mapAccumL tidyTyCoVarBndr (cec_tidy ctxt) tvs
301 info' = tidySkolemInfo env1 info
302 implic' = implic { ic_skols = tvs'
303 , ic_given = map (tidyEvVar env1) given
304 , ic_info = info' }
305 ctxt' = ctxt { cec_tidy = env1
306 , cec_encl = implic' : cec_encl ctxt
307 , cec_suppress = insoluble -- Suppress inessential errors if there
308 -- are are insolubles anywhere in the
309 -- tree rooted here
310 , cec_binds = cec_binds ctxt *> m_evb }
311 -- if cec_binds ctxt is Nothing, that means
312 -- we're reporting *all* errors. Don't change
313 -- that behavior just because we're going into
314 -- an implication.
315 dead_givens = case status of
316 IC_Solved { ics_dead = dead } -> dead
317 _ -> []
318
319 warnRedundantConstraints :: ReportErrCtxt -> TcLclEnv -> SkolemInfo -> [EvVar] -> TcM ()
320 warnRedundantConstraints ctxt env info ev_vars
321 | null redundant_evs
322 = return ()
323
324 | SigSkol {} <- info
325 = setLclEnv env $ -- We want to add "In the type signature for f"
326 -- to the error context, which is a bit tiresome
327 addErrCtxt (text "In" <+> ppr info) $
328 do { env <- getLclEnv
329 ; msg <- mkErrorReport ctxt env (important doc)
330 ; reportWarning msg }
331
332 | otherwise -- But for InstSkol there already *is* a surrounding
333 -- "In the instance declaration for Eq [a]" context
334 -- and we don't want to say it twice. Seems a bit ad-hoc
335 = do { msg <- mkErrorReport ctxt env (important doc)
336 ; reportWarning msg }
337 where
338 doc = text "Redundant constraint" <> plural redundant_evs <> colon
339 <+> pprEvVarTheta redundant_evs
340
341 redundant_evs = case info of -- See Note [Redundant constraints in instance decls]
342 InstSkol -> filterOut improving ev_vars
343 _ -> ev_vars
344
345 improving ev_var = any isImprovementPred $
346 transSuperClasses (idType ev_var)
347
348 {- Note [Redundant constraints in instance decls]
349 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
350 For instance declarations, we don't report unused givens if
351 they can give rise to improvement. Example (Trac #10100):
352 class Add a b ab | a b -> ab, a ab -> b
353 instance Add Zero b b
354 instance Add a b ab => Add (Succ a) b (Succ ab)
355 The context (Add a b ab) for the instance is clearly unused in terms
356 of evidence, since the dictionary has no feilds. But it is still
357 needed! With the context, a wanted constraint
358 Add (Succ Zero) beta (Succ Zero)
359 we will reduce to (Add Zero beta Zero), and thence we get beta := Zero.
360 But without the context we won't find beta := Zero.
361
362 This only matters in instance declarations..
363 -}
364
365 reportWanteds :: ReportErrCtxt -> TcLevel -> WantedConstraints -> TcM ()
366 reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_insol = insols, wc_impl = implics })
367 = do { traceTc "reportWanteds" (vcat [ text "Simples =" <+> ppr simples
368 , text "Suppress =" <+> ppr (cec_suppress ctxt)])
369 ; let tidy_cts = bagToList (mapBag (tidyCt env) (insols `unionBags` simples))
370
371 -- First deal with things that are utterly wrong
372 -- Like Int ~ Bool (incl nullary TyCons)
373 -- or Int ~ t a (AppTy on one side)
374 -- These ones are not suppressed by the incoming context
375 ; let ctxt_for_insols = ctxt { cec_suppress = False }
376 ; (ctxt1, cts1) <- tryReporters ctxt_for_insols report1 tidy_cts
377
378 -- Now all the other constraints. We suppress errors here if
379 -- any of the first batch failed, or if the enclosing context
380 -- says to suppress
381 ; let ctxt2 = ctxt { cec_suppress = cec_suppress ctxt || cec_suppress ctxt1 }
382 ; (_, leftovers) <- tryReporters ctxt2 report2 cts1
383 ; MASSERT2( null leftovers, ppr leftovers )
384
385 -- All the Derived ones have been filtered out of simples
386 -- by the constraint solver. This is ok; we don't want
387 -- to report unsolved Derived goals as errors
388 -- See Note [Do not report derived but soluble errors]
389
390 ; mapBagM_ (reportImplic ctxt2) implics }
391 -- NB ctxt1: don't suppress inner insolubles if there's only a
392 -- wanted insoluble here; but do suppress inner insolubles
393 -- if there's a *given* insoluble here (= inaccessible code)
394 where
395 env = cec_tidy ctxt
396
397 -- report1: ones that should *not* be suppresed by
398 -- an insoluble somewhere else in the tree
399 -- It's crucial that anything that is considered insoluble
400 -- (see TcRnTypes.trulyInsoluble) is caught here, otherwise
401 -- we might suppress its error message, and proceed on past
402 -- type checking to get a Lint error later
403 report1 = [ ("custom_error", is_user_type_error,
404 True, mkUserTypeErrorReporter)
405 , ("insoluble1", is_given_eq, True, mkGroupReporter mkEqErr)
406 , ("insoluble2", utterly_wrong, True, mkGroupReporter mkEqErr)
407 , ("skolem eq1", very_wrong, True, mkSkolReporter)
408 , ("skolem eq2", skolem_eq, True, mkSkolReporter)
409 , ("non-tv eq", non_tv_eq, True, mkSkolReporter)
410 , ("Out of scope", is_out_of_scope, True, mkHoleReporter)
411 , ("Holes", is_hole, False, mkHoleReporter)
412
413 -- The only remaining equalities are alpha ~ ty,
414 -- where alpha is untouchable; and representational equalities
415 , ("Other eqs", is_equality, False, mkGroupReporter mkEqErr) ]
416
417 -- report2: we suppress these if there are insolubles elsewhere in the tree
418 report2 = [ ("Implicit params", is_ip, False, mkGroupReporter mkIPErr)
419 , ("Irreds", is_irred, False, mkGroupReporter mkIrredErr)
420 , ("Dicts", is_dict, False, mkGroupReporter mkDictErr) ]
421
422 -- rigid_nom_eq, rigid_nom_tv_eq,
423 is_hole, is_dict,
424 is_equality, is_ip, is_irred :: Ct -> PredTree -> Bool
425
426 is_given_eq ct pred
427 | EqPred {} <- pred = arisesFromGivens ct
428 | otherwise = False
429 -- I think all given residuals are equalities
430
431 -- Things like (Int ~N Bool)
432 utterly_wrong _ (EqPred NomEq ty1 ty2) = isRigidTy ty1 && isRigidTy ty2
433 utterly_wrong _ _ = False
434
435 -- Things like (a ~N Int)
436 very_wrong _ (EqPred NomEq ty1 ty2) = isSkolemTy tc_lvl ty1 && isRigidTy ty2
437 very_wrong _ _ = False
438
439 -- Things like (a ~N b) or (a ~N F Bool)
440 skolem_eq _ (EqPred NomEq ty1 _) = isSkolemTy tc_lvl ty1
441 skolem_eq _ _ = False
442
443 -- Things like (F a ~N Int)
444 non_tv_eq _ (EqPred NomEq ty1 _) = not (isTyVarTy ty1)
445 non_tv_eq _ _ = False
446
447 -- rigid_nom_eq _ pred = isRigidEqPred tc_lvl pred
448 --
449 -- rigid_nom_tv_eq _ pred
450 -- | EqPred _ ty1 _ <- pred = isRigidEqPred tc_lvl pred && isTyVarTy ty1
451 -- | otherwise = False
452
453 is_out_of_scope ct _ = isOutOfScopeCt ct
454 is_hole ct _ = isHoleCt ct
455
456 is_user_type_error ct _ = isUserTypeErrorCt ct
457
458 is_equality _ (EqPred {}) = True
459 is_equality _ _ = False
460
461 is_dict _ (ClassPred {}) = True
462 is_dict _ _ = False
463
464 is_ip _ (ClassPred cls _) = isIPClass cls
465 is_ip _ _ = False
466
467 is_irred _ (IrredPred {}) = True
468 is_irred _ _ = False
469
470
471 ---------------
472 isSkolemTy :: TcLevel -> Type -> Bool
473 isSkolemTy tc_lvl ty
474 = case getTyVar_maybe ty of
475 Nothing -> False
476 Just tv -> isSkolemTyVar tv
477 || (isSigTyVar tv && isTouchableMetaTyVar tc_lvl tv)
478 -- The latter case is for touchable SigTvs
479 -- we postpone untouchables to a latter test (too obscure)
480
481 isTyFun_maybe :: Type -> Maybe TyCon
482 isTyFun_maybe ty = case tcSplitTyConApp_maybe ty of
483 Just (tc,_) | isTypeFamilyTyCon tc -> Just tc
484 _ -> Nothing
485
486
487 --------------------------------------------
488 -- Reporters
489 --------------------------------------------
490
491 type Reporter
492 = ReportErrCtxt -> [Ct] -> TcM ()
493 type ReporterSpec
494 = ( String -- Name
495 , Ct -> PredTree -> Bool -- Pick these ones
496 , Bool -- True <=> suppress subsequent reporters
497 , Reporter) -- The reporter itself
498
499 mkSkolReporter :: Reporter
500 -- Suppress duplicates with either the same LHS, or same location
501 mkSkolReporter ctxt cts
502 = mapM_ (reportGroup mkEqErr ctxt) (group cts)
503 where
504 group [] = []
505 group (ct:cts) = (ct : yeses) : group noes
506 where
507 (yeses, noes) = partition (group_with ct) cts
508
509 group_with ct1 ct2
510 | EQ <- cmp_loc ct1 ct2 = True
511 | EQ <- cmp_lhs_type ct1 ct2 = True
512 | otherwise = False
513
514 mkHoleReporter :: Reporter
515 -- Reports errors one at a time
516 mkHoleReporter ctxt
517 = mapM_ $ \ct ->
518 do { err <- mkHoleError ctxt ct
519 ; maybeReportHoleError ctxt ct err
520 ; maybeAddDeferredHoleBinding ctxt err ct }
521
522 mkUserTypeErrorReporter :: Reporter
523 mkUserTypeErrorReporter ctxt
524 = mapM_ $ \ct -> maybeReportError ctxt =<< mkUserTypeError ctxt ct
525
526 mkUserTypeError :: ReportErrCtxt -> Ct -> TcM ErrMsg
527 mkUserTypeError ctxt ct = mkErrorMsgFromCt ctxt ct
528 $ important
529 $ pprUserTypeErrorTy
530 $ case getUserTypeErrorMsg ct of
531 Just msg -> msg
532 Nothing -> pprPanic "mkUserTypeError" (ppr ct)
533
534
535 mkGroupReporter :: (ReportErrCtxt -> [Ct] -> TcM ErrMsg)
536 -- Make error message for a group
537 -> Reporter -- Deal with lots of constraints
538 -- Group together errors from same location,
539 -- and report only the first (to avoid a cascade)
540 mkGroupReporter mk_err ctxt cts
541 = mapM_ (reportGroup mk_err ctxt) (equivClasses cmp_loc cts)
542 where
543
544 cmp_lhs_type :: Ct -> Ct -> Ordering
545 cmp_lhs_type ct1 ct2
546 = case (classifyPredType (ctPred ct1), classifyPredType (ctPred ct2)) of
547 (EqPred eq_rel1 ty1 _, EqPred eq_rel2 ty2 _) ->
548 (eq_rel1 `compare` eq_rel2) `thenCmp` (ty1 `cmpType` ty2)
549 _ -> pprPanic "mkSkolReporter" (ppr ct1 $$ ppr ct2)
550
551 cmp_loc :: Ct -> Ct -> Ordering
552 cmp_loc ct1 ct2 = ctLocSpan (ctLoc ct1) `compare` ctLocSpan (ctLoc ct2)
553
554 reportGroup :: (ReportErrCtxt -> [Ct] -> TcM ErrMsg) -> ReportErrCtxt
555 -> [Ct] -> TcM ()
556 reportGroup mk_err ctxt cts =
557 case partition isMonadFailInstanceMissing cts of
558 -- Only warn about missing MonadFail constraint when
559 -- there are no other missing contstraints!
560 (monadFailCts, []) -> do { err <- mk_err ctxt monadFailCts
561 ; reportWarning err }
562
563 (_, cts') -> do { err <- mk_err ctxt cts'
564 ; maybeReportError ctxt err
565 ; mapM_ (maybeAddDeferredBinding ctxt err) cts' }
566 -- Add deferred bindings for all
567 -- But see Note [Always warn with -fdefer-type-errors]
568 where
569 isMonadFailInstanceMissing ct =
570 case ctLocOrigin (ctLoc ct) of
571 FailablePattern _pat -> True
572 _otherwise -> False
573
574 maybeReportHoleError :: ReportErrCtxt -> Ct -> ErrMsg -> TcM ()
575 maybeReportHoleError ctxt ct err
576 -- When -XPartialTypeSignatures is on, warnings (instead of errors) are
577 -- generated for holes in partial type signatures.
578 -- Unless -fwarn_partial_type_signatures is not on,
579 -- in which case the messages are discarded.
580 | isTypeHoleCt ct
581 = -- For partial type signatures, generate warnings only, and do that
582 -- only if -fwarn_partial_type_signatures is on
583 case cec_type_holes ctxt of
584 HoleError -> reportError err
585 HoleWarn -> reportWarning err
586 HoleDefer -> return ()
587
588 -- Otherwise this is a typed hole in an expression
589 | otherwise
590 = -- If deferring, report a warning only if -Wtyped-holds is on
591 case cec_expr_holes ctxt of
592 HoleError -> reportError err
593 HoleWarn -> reportWarning err
594 HoleDefer -> return ()
595
596 maybeReportError :: ReportErrCtxt -> ErrMsg -> TcM ()
597 -- Report the error and/or make a deferred binding for it
598 maybeReportError ctxt err
599 | cec_suppress ctxt -- Some worse error has occurred;
600 = return () -- so suppress this error/warning
601
602 | cec_errors_as_warns ctxt
603 = reportWarning err
604
605 | otherwise
606 = case cec_defer_type_errors ctxt of
607 TypeDefer -> return ()
608 TypeWarn -> reportWarning err
609 TypeError -> reportError err
610
611 addDeferredBinding :: ReportErrCtxt -> ErrMsg -> Ct -> TcM ()
612 -- See Note [Deferring coercion errors to runtime]
613 addDeferredBinding ctxt err ct
614 | CtWanted { ctev_pred = pred, ctev_dest = dest } <- ctEvidence ct
615 -- Only add deferred bindings for Wanted constraints
616 , Just ev_binds_var <- cec_binds ctxt -- We have somewhere to put the bindings
617 = do { dflags <- getDynFlags
618 ; let err_msg = pprLocErrMsg err
619 err_fs = mkFastString $ showSDoc dflags $
620 err_msg $$ text "(deferred type error)"
621 err_tm = EvDelayedError pred err_fs
622
623 ; case dest of
624 EvVarDest evar
625 -> addTcEvBind ev_binds_var $ mkWantedEvBind evar err_tm
626 HoleDest hole
627 -> do { -- See Note [Deferred errors for coercion holes]
628 evar <- newEvVar pred
629 ; addTcEvBind ev_binds_var $ mkWantedEvBind evar err_tm
630 ; fillCoercionHole hole (mkTcCoVarCo evar) }}
631
632 | otherwise -- Do not set any evidence for Given/Derived
633 = return ()
634
635 maybeAddDeferredHoleBinding :: ReportErrCtxt -> ErrMsg -> Ct -> TcM ()
636 maybeAddDeferredHoleBinding ctxt err ct
637 | isExprHoleCt ct
638 , case cec_expr_holes ctxt of
639 HoleDefer -> True
640 HoleWarn -> True
641 HoleError -> False
642 = addDeferredBinding ctxt err ct -- Only add bindings for holes in expressions
643 | otherwise -- not for holes in partial type signatures
644 = return ()
645
646 maybeAddDeferredBinding :: ReportErrCtxt -> ErrMsg -> Ct -> TcM ()
647 maybeAddDeferredBinding ctxt err ct =
648 case cec_defer_type_errors ctxt of
649 TypeDefer -> deferred
650 TypeWarn -> deferred
651 TypeError -> return ()
652 where
653 deferred = addDeferredBinding ctxt err ct
654
655 tryReporters :: ReportErrCtxt -> [ReporterSpec] -> [Ct] -> TcM (ReportErrCtxt, [Ct])
656 -- Use the first reporter in the list whose predicate says True
657 tryReporters ctxt reporters cts
658 = do { traceTc "tryReporters {" (ppr cts)
659 ; (ctxt', cts') <- go ctxt reporters cts
660 ; traceTc "tryReporters }" (ppr cts')
661 ; return (ctxt', cts') }
662 where
663 go ctxt [] cts
664 = return (ctxt, cts)
665
666 go ctxt (r : rs) cts
667 = do { (ctxt', cts') <- tryReporter ctxt r cts
668 ; go ctxt' rs cts' }
669 -- Carry on with the rest, because we must make
670 -- deferred bindings for them if we have -fdefer-type-errors
671 -- But suppress their error messages
672
673 tryReporter :: ReportErrCtxt -> ReporterSpec -> [Ct] -> TcM (ReportErrCtxt, [Ct])
674 tryReporter ctxt (str, keep_me, suppress_after, reporter) cts
675 | null yeses = return (ctxt, cts)
676 | otherwise = do { traceTc "tryReporter:" (text str <+> ppr yeses)
677 ; reporter ctxt yeses
678 ; let ctxt' = ctxt { cec_suppress = suppress_after || cec_suppress ctxt }
679 ; return (ctxt', nos) }
680 where
681 (yeses, nos) = partition (\ct -> keep_me ct (classifyPredType (ctPred ct))) cts
682
683
684 pprArising :: CtOrigin -> SDoc
685 -- Used for the main, top-level error message
686 -- We've done special processing for TypeEq, KindEq, Given
687 pprArising (TypeEqOrigin {}) = empty
688 pprArising (KindEqOrigin {}) = empty
689 pprArising (GivenOrigin {}) = empty
690 pprArising orig = pprCtOrigin orig
691
692 -- Add the "arising from..." part to a message about bunch of dicts
693 addArising :: CtOrigin -> SDoc -> SDoc
694 addArising orig msg = hang msg 2 (pprArising orig)
695
696 pprWithArising :: [Ct] -> (CtLoc, SDoc)
697 -- Print something like
698 -- (Eq a) arising from a use of x at y
699 -- (Show a) arising from a use of p at q
700 -- Also return a location for the error message
701 -- Works for Wanted/Derived only
702 pprWithArising []
703 = panic "pprWithArising"
704 pprWithArising (ct:cts)
705 | null cts
706 = (loc, addArising (ctLocOrigin loc)
707 (pprTheta [ctPred ct]))
708 | otherwise
709 = (loc, vcat (map ppr_one (ct:cts)))
710 where
711 loc = ctLoc ct
712 ppr_one ct' = hang (parens (pprType (ctPred ct')))
713 2 (pprCtLoc (ctLoc ct'))
714
715 mkErrorMsgFromCt :: ReportErrCtxt -> Ct -> Report -> TcM ErrMsg
716 mkErrorMsgFromCt ctxt ct report
717 = mkErrorReport ctxt (ctLocEnv (ctLoc ct)) report
718
719 mkErrorReport :: ReportErrCtxt -> TcLclEnv -> Report -> TcM ErrMsg
720 mkErrorReport ctxt tcl_env (Report important relevant_bindings)
721 = do { context <- mkErrInfo (cec_tidy ctxt) (tcl_ctxt tcl_env)
722 ; mkErrDocAt (RealSrcSpan (tcl_loc tcl_env))
723 (errDoc important [context] relevant_bindings)
724 }
725
726 type UserGiven = ([EvVar], SkolemInfo, Bool, RealSrcSpan)
727
728 getUserGivens :: ReportErrCtxt -> [UserGiven]
729 -- One item for each enclosing implication
730 getUserGivens (CEC {cec_encl = ctxt})
731 = reverse $
732 [ (givens, info, no_eqs, tcl_loc env)
733 | Implic { ic_given = givens, ic_env = env
734 , ic_no_eqs = no_eqs, ic_info = info } <- ctxt
735 , not (null givens) ]
736
737 {-
738 Note [Always warn with -fdefer-type-errors]
739 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
740 When -fdefer-type-errors is on we warn about *all* type errors, even
741 if cec_suppress is on. This can lead to a lot more warnings than you
742 would get errors without -fdefer-type-errors, but if we suppress any of
743 them you might get a runtime error that wasn't warned about at compile
744 time.
745
746 This is an easy design choice to change; just flip the order of the
747 first two equations for maybeReportError
748
749 To be consistent, we should also report multiple warnings from a single
750 location in mkGroupReporter, when -fdefer-type-errors is on. But that
751 is perhaps a bit *over*-consistent! Again, an easy choice to change.
752
753 With #10283, you can now opt out of deferred type error warnings.
754
755 Note [Deferred errors for coercion holes]
756 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
757 Suppose we need to defer a type error where the destination for the evidence
758 is a coercion hole. We can't just put the error in the hole, because we can't
759 make an erroneous coercion. (Remember that coercions are erased for runtime.)
760 Instead, we invent a new EvVar, bind it to an error and then make a coercion
761 from that EvVar, filling the hole with that coercion. Because coercions'
762 types are unlifted, the error is guaranteed to be hit before we get to the
763 coercion.
764
765 Note [Do not report derived but soluble errors]
766 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
767 The wc_simples include Derived constraints that have not been solved, but are
768 not insoluble (in that case they'd be in wc_insols). We do not want to report
769 these as errors:
770
771 * Superclass constraints. If we have an unsolved [W] Ord a, we'll also have
772 an unsolved [D] Eq a, and we do not want to report that; it's just noise.
773
774 * Functional dependencies. For givens, consider
775 class C a b | a -> b
776 data T a where
777 MkT :: C a d => [d] -> T a
778 f :: C a b => T a -> F Int
779 f (MkT xs) = length xs
780 Then we get a [D] b~d. But there *is* a legitimate call to
781 f, namely f (MkT [True]) :: T Bool, in which b=d. So we should
782 not reject the program.
783
784 For wanteds, something similar
785 data T a where
786 MkT :: C Int b => a -> b -> T a
787 g :: C Int c => c -> ()
788 f :: T a -> ()
789 f (MkT x y) = g x
790 Here we get [G] C Int b, [W] C Int a, hence [D] a~b.
791 But again f (MkT True True) is a legitimate call.
792
793 (We leave the Deriveds in wc_simple until reportErrors, so that we don't lose
794 derived superclasses between iterations of the solver.)
795
796 For functional dependencies, here is a real example,
797 stripped off from libraries/utf8-string/Codec/Binary/UTF8/Generic.hs
798
799 class C a b | a -> b
800 g :: C a b => a -> b -> ()
801 f :: C a b => a -> b -> ()
802 f xa xb =
803 let loop = g xa
804 in loop xb
805
806 We will first try to infer a type for loop, and we will succeed:
807 C a b' => b' -> ()
808 Subsequently, we will type check (loop xb) and all is good. But,
809 recall that we have to solve a final implication constraint:
810 C a b => (C a b' => .... cts from body of loop .... ))
811 And now we have a problem as we will generate an equality b ~ b' and fail to
812 solve it.
813
814
815 ************************************************************************
816 * *
817 Irreducible predicate errors
818 * *
819 ************************************************************************
820 -}
821
822 mkIrredErr :: ReportErrCtxt -> [Ct] -> TcM ErrMsg
823 mkIrredErr ctxt cts
824 = do { (ctxt, binds_msg, ct1) <- relevantBindings True ctxt ct1
825 ; let orig = ctOrigin ct1
826 msg = couldNotDeduce (getUserGivens ctxt) (map ctPred cts, orig)
827 ; mkErrorMsgFromCt ctxt ct1 $
828 important msg `mappend` relevant_bindings binds_msg }
829 where
830 (ct1:_) = cts
831
832 ----------------
833 mkHoleError :: ReportErrCtxt -> Ct -> TcM ErrMsg
834 mkHoleError ctxt ct@(CHoleCan { cc_occ = occ, cc_hole = hole_sort })
835 | isOutOfScopeCt ct -- Out of scope variables, like 'a', where 'a' isn't bound
836 -- Suggest possible in-scope variables in the message
837 = do { dflags <- getDynFlags
838 ; rdr_env <- getGlobalRdrEnv
839 ; impInfo <- getImports
840 ; mkErrDocAt (RealSrcSpan (tcl_loc lcl_env)) $
841 errDoc [out_of_scope_msg] []
842 [unknownNameSuggestions dflags rdr_env
843 (tcl_rdr lcl_env) impInfo (mkRdrUnqual occ)] }
844
845 | otherwise -- Explicit holes, like "_" or "_f"
846 = do { (ctxt, binds_msg, ct) <- relevantBindings False ctxt ct
847 -- The 'False' means "don't filter the bindings"; see Trac #8191
848 ; mkErrorMsgFromCt ctxt ct $
849 important hole_msg `mappend` relevant_bindings binds_msg }
850
851 where
852 ct_loc = ctLoc ct
853 lcl_env = ctLocEnv ct_loc
854 hole_ty = ctEvPred (ctEvidence ct)
855 tyvars = tyCoVarsOfTypeList hole_ty
856 boring_type = isTyVarTy hole_ty
857
858 out_of_scope_msg -- Print v :: ty only if the type has structure
859 | boring_type = hang herald 2 (ppr occ)
860 | otherwise = hang herald 2 pp_with_type
861
862 pp_with_type = hang (pprPrefixOcc occ) 2 (dcolon <+> pprType hole_ty)
863 herald | isDataOcc occ = text "Data constructor not in scope:"
864 | otherwise = text "Variable not in scope:"
865
866 hole_msg = case hole_sort of
867 ExprHole -> vcat [ hang (text "Found hole:")
868 2 pp_with_type
869 , tyvars_msg, expr_hole_hint ]
870 TypeHole -> vcat [ hang (text "Found type wildcard" <+> quotes (ppr occ))
871 2 (text "standing for" <+> quotes (pprType hole_ty))
872 , tyvars_msg, type_hole_hint ]
873
874 tyvars_msg = ppUnless (null tyvars) $
875 text "Where:" <+> vcat (map loc_msg tyvars)
876
877 type_hole_hint
878 | HoleError <- cec_type_holes ctxt
879 = text "To use the inferred type, enable PartialTypeSignatures"
880 | otherwise
881 = empty
882
883 expr_hole_hint -- Give hint for, say, f x = _x
884 | lengthFS (occNameFS occ) > 1 -- Don't give this hint for plain "_"
885 = text "Or perhaps" <+> quotes (ppr occ)
886 <+> text "is mis-spelled, or not in scope"
887 | otherwise
888 = empty
889
890 loc_msg tv
891 | isTyVar tv
892 = case tcTyVarDetails tv of
893 SkolemTv {} -> pprSkol (cec_encl ctxt) tv
894 MetaTv {} -> quotes (ppr tv) <+> text "is an ambiguous type variable"
895 det -> pprTcTyVarDetails det
896 | otherwise
897 = sdocWithDynFlags $ \dflags ->
898 if gopt Opt_PrintExplicitCoercions dflags
899 then quotes (ppr tv) <+> text "is a coercion variable"
900 else empty
901
902 mkHoleError _ ct = pprPanic "mkHoleError" (ppr ct)
903
904 ----------------
905 mkIPErr :: ReportErrCtxt -> [Ct] -> TcM ErrMsg
906 mkIPErr ctxt cts
907 = do { (ctxt, binds_msg, ct1) <- relevantBindings True ctxt ct1
908 ; let orig = ctOrigin ct1
909 preds = map ctPred cts
910 givens = getUserGivens ctxt
911 msg | null givens
912 = addArising orig $
913 sep [ text "Unbound implicit parameter" <> plural cts
914 , nest 2 (pprTheta preds) ]
915 | otherwise
916 = couldNotDeduce givens (preds, orig)
917
918 ; mkErrorMsgFromCt ctxt ct1 $
919 important msg `mappend` relevant_bindings binds_msg }
920 where
921 (ct1:_) = cts
922
923 {-
924 ************************************************************************
925 * *
926 Equality errors
927 * *
928 ************************************************************************
929
930 Note [Inaccessible code]
931 ~~~~~~~~~~~~~~~~~~~~~~~~
932 Consider
933 data T a where
934 T1 :: T a
935 T2 :: T Bool
936
937 f :: (a ~ Int) => T a -> Int
938 f T1 = 3
939 f T2 = 4 -- Unreachable code
940
941 Here the second equation is unreachable. The original constraint
942 (a~Int) from the signature gets rewritten by the pattern-match to
943 (Bool~Int), so the danger is that we report the error as coming from
944 the *signature* (Trac #7293). So, for Given errors we replace the
945 env (and hence src-loc) on its CtLoc with that from the immediately
946 enclosing implication.
947 -}
948
949 mkEqErr :: ReportErrCtxt -> [Ct] -> TcM ErrMsg
950 -- Don't have multiple equality errors from the same location
951 -- E.g. (Int,Bool) ~ (Bool,Int) one error will do!
952 mkEqErr ctxt (ct:_) = mkEqErr1 ctxt ct
953 mkEqErr _ [] = panic "mkEqErr"
954
955 mkEqErr1 :: ReportErrCtxt -> Ct -> TcM ErrMsg
956 mkEqErr1 ctxt ct
957 | arisesFromGivens ct
958 = do { (ctxt, binds_msg, ct) <- relevantBindings True ctxt ct
959 ; let (given_loc, given_msg) = mk_given (ctLoc ct) (cec_encl ctxt)
960 ; dflags <- getDynFlags
961 ; let report = important given_msg `mappend` relevant_bindings binds_msg
962 ; mkEqErr_help dflags ctxt report
963 (setCtLoc ct given_loc) -- Note [Inaccessible code]
964 Nothing ty1 ty2 }
965
966 | otherwise -- Wanted or derived
967 = do { (ctxt, binds_msg, ct) <- relevantBindings True ctxt ct
968 ; rdr_env <- getGlobalRdrEnv
969 ; fam_envs <- tcGetFamInstEnvs
970 ; exp_syns <- goptM Opt_PrintExpandedSynonyms
971 ; let (keep_going, is_oriented, wanted_msg)
972 = mk_wanted_extra (ctLoc ct) exp_syns
973 coercible_msg = case ctEqRel ct of
974 NomEq -> empty
975 ReprEq -> mkCoercibleExplanation rdr_env fam_envs ty1 ty2
976 ; dflags <- getDynFlags
977 ; traceTc "mkEqErr1" (ppr ct $$ pprCtOrigin (ctOrigin ct))
978 ; let report = mconcat [important wanted_msg, important coercible_msg,
979 relevant_bindings binds_msg]
980 ; if keep_going
981 then mkEqErr_help dflags ctxt report ct is_oriented ty1 ty2
982 else mkErrorMsgFromCt ctxt ct report }
983 where
984 (ty1, ty2) = getEqPredTys (ctPred ct)
985
986 mk_given :: CtLoc -> [Implication] -> (CtLoc, SDoc)
987 -- For given constraints we overwrite the env (and hence src-loc)
988 -- with one from the implication. See Note [Inaccessible code]
989 mk_given loc [] = (loc, empty)
990 mk_given loc (implic : _) = (setCtLocEnv loc (ic_env implic)
991 , hang (text "Inaccessible code in")
992 2 (ppr (ic_info implic)))
993
994 -- If the types in the error message are the same as the types
995 -- we are unifying, don't add the extra expected/actual message
996 mk_wanted_extra :: CtLoc -> Bool -> (Bool, Maybe SwapFlag, SDoc)
997 mk_wanted_extra loc expandSyns
998 = case ctLocOrigin loc of
999 orig@TypeEqOrigin {} -> mkExpectedActualMsg ty1 ty2 orig
1000 t_or_k expandSyns
1001 where
1002 t_or_k = ctLocTypeOrKind_maybe loc
1003
1004 KindEqOrigin cty1 mb_cty2 sub_o sub_t_or_k
1005 -> (True, Nothing, msg1 $$ msg2)
1006 where
1007 sub_what = case sub_t_or_k of Just KindLevel -> text "kinds"
1008 _ -> text "types"
1009 msg1 = sdocWithDynFlags $ \dflags ->
1010 case mb_cty2 of
1011 Just cty2
1012 | gopt Opt_PrintExplicitCoercions dflags
1013 || not (cty1 `pickyEqType` cty2)
1014 -> hang (text "When matching" <+> sub_what)
1015 2 (vcat [ ppr cty1 <+> dcolon <+>
1016 ppr (typeKind cty1)
1017 , ppr cty2 <+> dcolon <+>
1018 ppr (typeKind cty2) ])
1019 _ -> text "When matching the kind of" <+> quotes (ppr cty1)
1020 msg2 = case sub_o of
1021 TypeEqOrigin {}
1022 | Just cty2 <- mb_cty2 ->
1023 thdOf3 (mkExpectedActualMsg cty1 cty2 sub_o sub_t_or_k
1024 expandSyns)
1025 _ -> empty
1026 _ -> (True, Nothing, empty)
1027
1028 -- | This function tries to reconstruct why a "Coercible ty1 ty2" constraint
1029 -- is left over.
1030 mkCoercibleExplanation :: GlobalRdrEnv -> FamInstEnvs
1031 -> TcType -> TcType -> SDoc
1032 mkCoercibleExplanation rdr_env fam_envs ty1 ty2
1033 | Just (tc, tys) <- tcSplitTyConApp_maybe ty1
1034 , (rep_tc, _, _) <- tcLookupDataFamInst fam_envs tc tys
1035 , Just msg <- coercible_msg_for_tycon rep_tc
1036 = msg
1037 | Just (tc, tys) <- splitTyConApp_maybe ty2
1038 , (rep_tc, _, _) <- tcLookupDataFamInst fam_envs tc tys
1039 , Just msg <- coercible_msg_for_tycon rep_tc
1040 = msg
1041 | Just (s1, _) <- tcSplitAppTy_maybe ty1
1042 , Just (s2, _) <- tcSplitAppTy_maybe ty2
1043 , s1 `eqType` s2
1044 , has_unknown_roles s1
1045 = hang (text "NB: We cannot know what roles the parameters to" <+>
1046 quotes (ppr s1) <+> text "have;")
1047 2 (text "we must assume that the role is nominal")
1048 | otherwise
1049 = empty
1050 where
1051 coercible_msg_for_tycon tc
1052 | isAbstractTyCon tc
1053 = Just $ hsep [ text "NB: The type constructor"
1054 , quotes (pprSourceTyCon tc)
1055 , text "is abstract" ]
1056 | isNewTyCon tc
1057 , [data_con] <- tyConDataCons tc
1058 , let dc_name = dataConName data_con
1059 , null (lookupGRE_Name rdr_env dc_name)
1060 = Just $ hang (text "The data constructor" <+> quotes (ppr dc_name))
1061 2 (sep [ text "of newtype" <+> quotes (pprSourceTyCon tc)
1062 , text "is not in scope" ])
1063 | otherwise = Nothing
1064
1065 has_unknown_roles ty
1066 | Just (tc, tys) <- tcSplitTyConApp_maybe ty
1067 = length tys >= tyConArity tc -- oversaturated tycon
1068 | Just (s, _) <- tcSplitAppTy_maybe ty
1069 = has_unknown_roles s
1070 | isTyVarTy ty
1071 = True
1072 | otherwise
1073 = False
1074
1075 {-
1076 -- | Make a listing of role signatures for all the parameterised tycons
1077 -- used in the provided types
1078
1079
1080 -- SLPJ Jun 15: I could not convince myself that these hints were really
1081 -- useful. Maybe they are, but I think we need more work to make them
1082 -- actually helpful.
1083 mkRoleSigs :: Type -> Type -> SDoc
1084 mkRoleSigs ty1 ty2
1085 = ppUnless (null role_sigs) $
1086 hang (text "Relevant role signatures:")
1087 2 (vcat role_sigs)
1088 where
1089 tcs = nameEnvElts $ tyConsOfType ty1 `plusNameEnv` tyConsOfType ty2
1090 role_sigs = mapMaybe ppr_role_sig tcs
1091
1092 ppr_role_sig tc
1093 | null roles -- if there are no parameters, don't bother printing
1094 = Nothing
1095 | isBuiltInSyntax (tyConName tc) -- don't print roles for (->), etc.
1096 = Nothing
1097 | otherwise
1098 = Just $ hsep $ [text "type role", ppr tc] ++ map ppr roles
1099 where
1100 roles = tyConRoles tc
1101 -}
1102
1103 mkEqErr_help :: DynFlags -> ReportErrCtxt -> Report
1104 -> Ct
1105 -> Maybe SwapFlag -- Nothing <=> not sure
1106 -> TcType -> TcType -> TcM ErrMsg
1107 mkEqErr_help dflags ctxt report ct oriented ty1 ty2
1108 | Just tv1 <- tcGetTyVar_maybe ty1 = mkTyVarEqErr dflags ctxt report ct oriented tv1 ty2
1109 | Just tv2 <- tcGetTyVar_maybe ty2 = mkTyVarEqErr dflags ctxt report ct swapped tv2 ty1
1110 | otherwise = reportEqErr ctxt report ct oriented ty1 ty2
1111 where
1112 swapped = fmap flipSwap oriented
1113
1114 reportEqErr :: ReportErrCtxt -> Report
1115 -> Ct
1116 -> Maybe SwapFlag -- Nothing <=> not sure
1117 -> TcType -> TcType -> TcM ErrMsg
1118 reportEqErr ctxt report ct oriented ty1 ty2
1119 = mkErrorMsgFromCt ctxt ct (mconcat [misMatch, eqInfo, report])
1120 where misMatch = important $ misMatchOrCND ctxt ct oriented ty1 ty2
1121 eqInfo = important $ mkEqInfoMsg ct ty1 ty2
1122
1123 mkTyVarEqErr :: DynFlags -> ReportErrCtxt -> Report -> Ct
1124 -> Maybe SwapFlag -> TcTyVar -> TcType -> TcM ErrMsg
1125 -- tv1 and ty2 are already tidied
1126 mkTyVarEqErr dflags ctxt report ct oriented tv1 ty2
1127 | isUserSkolem ctxt tv1 -- ty2 won't be a meta-tyvar, or else the thing would
1128 -- be oriented the other way round;
1129 -- see TcCanonical.canEqTyVarTyVar
1130 || isSigTyVar tv1 && not (isTyVarTy ty2)
1131 || ctEqRel ct == ReprEq && not (isTyVarUnderDatatype tv1 ty2)
1132 -- the cases below don't really apply to ReprEq (except occurs check)
1133 = mkErrorMsgFromCt ctxt ct $ mconcat
1134 [ important $ misMatchOrCND ctxt ct oriented ty1 ty2
1135 , important $ extraTyVarInfo ctxt tv1 ty2
1136 , report
1137 ]
1138
1139 -- So tv is a meta tyvar (or started that way before we
1140 -- generalised it). So presumably it is an *untouchable*
1141 -- meta tyvar or a SigTv, else it'd have been unified
1142 | OC_Occurs <- occ_check_expand
1143 , ctEqRel ct == NomEq || isTyVarUnderDatatype tv1 ty2
1144 -- See Note [Occurs check error] in TcCanonical
1145 = do { let occCheckMsg = important $ addArising (ctOrigin ct) $
1146 hang (text "Occurs check: cannot construct the infinite" <+> what <> colon)
1147 2 (sep [ppr ty1, char '~', ppr ty2])
1148 extra2 = important $ mkEqInfoMsg ct ty1 ty2
1149 ; mkErrorMsgFromCt ctxt ct $ mconcat [occCheckMsg, extra2, report] }
1150
1151 | OC_Forall <- occ_check_expand
1152 = do { let msg = vcat [ text "Cannot instantiate unification variable"
1153 <+> quotes (ppr tv1)
1154 , hang (text "with a" <+> what <+> text "involving foralls:") 2 (ppr ty2)
1155 , nest 2 (text "GHC doesn't yet support impredicative polymorphism") ]
1156 -- Unlike the other reports, this discards the old 'report_important'
1157 -- instead of augmenting it. This is because the details are not likely
1158 -- to be helpful since this is just an unimplemented feature.
1159 ; mkErrorMsgFromCt ctxt ct $ report { report_important = [msg] } }
1160
1161 -- If the immediately-enclosing implication has 'tv' a skolem, and
1162 -- we know by now its an InferSkol kind of skolem, then presumably
1163 -- it started life as a SigTv, else it'd have been unified, given
1164 -- that there's no occurs-check or forall problem
1165 | (implic:_) <- cec_encl ctxt
1166 , Implic { ic_skols = skols } <- implic
1167 , tv1 `elem` skols
1168 = mkErrorMsgFromCt ctxt ct $ mconcat
1169 [ important $ misMatchMsg ct oriented ty1 ty2
1170 , important $ extraTyVarInfo ctxt tv1 ty2
1171 , report
1172 ]
1173
1174 -- Check for skolem escape
1175 | (implic:_) <- cec_encl ctxt -- Get the innermost context
1176 , Implic { ic_env = env, ic_skols = skols, ic_info = skol_info } <- implic
1177 , let esc_skols = filter (`elemVarSet` (tyCoVarsOfType ty2)) skols
1178 , not (null esc_skols)
1179 = do { let msg = important $ misMatchMsg ct oriented ty1 ty2
1180 esc_doc = sep [ text "because" <+> what <+> text "variable" <> plural esc_skols
1181 <+> pprQuotedList esc_skols
1182 , text "would escape" <+>
1183 if isSingleton esc_skols then text "its scope"
1184 else text "their scope" ]
1185 tv_extra = important $
1186 vcat [ nest 2 $ esc_doc
1187 , sep [ (if isSingleton esc_skols
1188 then text "This (rigid, skolem)" <+>
1189 what <+> text "variable is"
1190 else text "These (rigid, skolem)" <+>
1191 what <+> text "variables are")
1192 <+> text "bound by"
1193 , nest 2 $ ppr skol_info
1194 , nest 2 $ text "at" <+> ppr (tcl_loc env) ] ]
1195 ; mkErrorMsgFromCt ctxt ct (mconcat [msg, tv_extra, report]) }
1196
1197 -- Nastiest case: attempt to unify an untouchable variable
1198 | (implic:_) <- cec_encl ctxt -- Get the innermost context
1199 , Implic { ic_env = env, ic_given = given, ic_info = skol_info } <- implic
1200 = do { let msg = important $ misMatchMsg ct oriented ty1 ty2
1201 tclvl_extra = important $
1202 nest 2 $
1203 sep [ quotes (ppr tv1) <+> text "is untouchable"
1204 , nest 2 $ text "inside the constraints:" <+> pprEvVarTheta given
1205 , nest 2 $ text "bound by" <+> ppr skol_info
1206 , nest 2 $ text "at" <+> ppr (tcl_loc env) ]
1207 tv_extra = important $ extraTyVarInfo ctxt tv1 ty2
1208 add_sig = important $ suggestAddSig ctxt ty1 ty2
1209 ; mkErrorMsgFromCt ctxt ct $ mconcat
1210 [msg, tclvl_extra, tv_extra, add_sig, report] }
1211
1212 | otherwise
1213 = reportEqErr ctxt report ct oriented (mkTyVarTy tv1) ty2
1214 -- This *can* happen (Trac #6123, and test T2627b)
1215 -- Consider an ambiguous top-level constraint (a ~ F a)
1216 -- Not an occurs check, because F is a type function.
1217 where
1218 occ_check_expand = occurCheckExpand dflags tv1 ty2
1219 ty1 = mkTyVarTy tv1
1220
1221 what = case ctLocTypeOrKind_maybe (ctLoc ct) of
1222 Just KindLevel -> text "kind"
1223 _ -> text "type"
1224
1225 mkEqInfoMsg :: Ct -> TcType -> TcType -> SDoc
1226 -- Report (a) ambiguity if either side is a type function application
1227 -- e.g. F a0 ~ Int
1228 -- (b) warning about injectivity if both sides are the same
1229 -- type function application F a ~ F b
1230 -- See Note [Non-injective type functions]
1231 -- (c) warning about -fprint-explicit-kinds if that might be helpful
1232 mkEqInfoMsg ct ty1 ty2
1233 = tyfun_msg $$ ambig_msg $$ invis_msg
1234 where
1235 mb_fun1 = isTyFun_maybe ty1
1236 mb_fun2 = isTyFun_maybe ty2
1237
1238 ambig_msg | isJust mb_fun1 || isJust mb_fun2
1239 = snd (mkAmbigMsg False ct)
1240 | otherwise = empty
1241
1242 invis_msg | Just vis <- tcEqTypeVis ty1 ty2
1243 , vis /= Visible
1244 = sdocWithDynFlags $ \dflags ->
1245 if gopt Opt_PrintExplicitKinds dflags
1246 then text "Use -fprint-explicit-kinds to see the kind arguments"
1247 else empty
1248
1249 | otherwise
1250 = empty
1251
1252 tyfun_msg | Just tc1 <- mb_fun1
1253 , Just tc2 <- mb_fun2
1254 , tc1 == tc2
1255 = text "NB:" <+> quotes (ppr tc1)
1256 <+> text "is a type function, and may not be injective"
1257 | otherwise = empty
1258
1259 isUserSkolem :: ReportErrCtxt -> TcTyVar -> Bool
1260 -- See Note [Reporting occurs-check errors]
1261 isUserSkolem ctxt tv
1262 = isSkolemTyVar tv && any is_user_skol_tv (cec_encl ctxt)
1263 where
1264 is_user_skol_tv (Implic { ic_skols = sks, ic_info = skol_info })
1265 = tv `elem` sks && is_user_skol_info skol_info
1266
1267 is_user_skol_info (InferSkol {}) = False
1268 is_user_skol_info _ = True
1269
1270 misMatchOrCND :: ReportErrCtxt -> Ct
1271 -> Maybe SwapFlag -> TcType -> TcType -> SDoc
1272 -- If oriented then ty1 is actual, ty2 is expected
1273 misMatchOrCND ctxt ct oriented ty1 ty2
1274 | null givens ||
1275 (isRigidTy ty1 && isRigidTy ty2) ||
1276 isGivenCt ct
1277 -- If the equality is unconditionally insoluble
1278 -- or there is no context, don't report the context
1279 = misMatchMsg ct oriented ty1 ty2
1280 | otherwise
1281 = couldNotDeduce givens ([eq_pred], orig)
1282 where
1283 ev = ctEvidence ct
1284 eq_pred = ctEvPred ev
1285 orig = ctEvOrigin ev
1286 givens = [ given | given@(_, _, no_eqs, _) <- getUserGivens ctxt, not no_eqs]
1287 -- Keep only UserGivens that have some equalities
1288
1289 couldNotDeduce :: [UserGiven] -> (ThetaType, CtOrigin) -> SDoc
1290 couldNotDeduce givens (wanteds, orig)
1291 = vcat [ addArising orig (text "Could not deduce:" <+> pprTheta wanteds)
1292 , vcat (pp_givens givens)]
1293
1294 pp_givens :: [UserGiven] -> [SDoc]
1295 pp_givens givens
1296 = case givens of
1297 [] -> []
1298 (g:gs) -> ppr_given (text "from the context:") g
1299 : map (ppr_given (text "or from:")) gs
1300 where
1301 ppr_given herald (gs, skol_info, _, loc)
1302 = hang (herald <+> pprEvVarTheta gs)
1303 2 (sep [ text "bound by" <+> ppr skol_info
1304 , text "at" <+> ppr loc])
1305
1306 extraTyVarInfo :: ReportErrCtxt -> TcTyVar -> TcType -> SDoc
1307 -- Add on extra info about skolem constants
1308 -- NB: The types themselves are already tidied
1309 extraTyVarInfo ctxt tv1 ty2
1310 = tv_extra tv1 $$ ty_extra ty2
1311 where
1312 implics = cec_encl ctxt
1313 ty_extra ty = case tcGetTyVar_maybe ty of
1314 Just tv -> tv_extra tv
1315 Nothing -> empty
1316
1317 tv_extra tv | isTcTyVar tv, isSkolemTyVar tv
1318 , let pp_tv = quotes (ppr tv)
1319 = case tcTyVarDetails tv of
1320 SkolemTv {} -> pprSkol implics tv
1321 FlatSkol {} -> pp_tv <+> text "is a flattening type variable"
1322 RuntimeUnk {} -> pp_tv <+> text "is an interactive-debugger skolem"
1323 MetaTv {} -> empty
1324
1325 | otherwise -- Normal case
1326 = empty
1327
1328 suggestAddSig :: ReportErrCtxt -> TcType -> TcType -> SDoc
1329 -- See Note [Suggest adding a type signature]
1330 suggestAddSig ctxt ty1 ty2
1331 | null inferred_bndrs
1332 = empty
1333 | [bndr] <- inferred_bndrs
1334 = text "Possible fix: add a type signature for" <+> quotes (ppr bndr)
1335 | otherwise
1336 = text "Possible fix: add type signatures for some or all of" <+> (ppr inferred_bndrs)
1337 where
1338 inferred_bndrs = nub (get_inf ty1 ++ get_inf ty2)
1339 get_inf ty | Just tv <- tcGetTyVar_maybe ty
1340 , isTcTyVar tv, isSkolemTyVar tv
1341 , (_, InferSkol prs) <- getSkolemInfo (cec_encl ctxt) tv
1342 = map fst prs
1343 | otherwise
1344 = []
1345
1346 --------------------
1347 misMatchMsg :: Ct -> Maybe SwapFlag -> TcType -> TcType -> SDoc
1348 -- Types are already tidy
1349 -- If oriented then ty1 is actual, ty2 is expected
1350 misMatchMsg ct oriented ty1 ty2
1351 | Just NotSwapped <- oriented
1352 = misMatchMsg ct (Just IsSwapped) ty2 ty1
1353
1354 | Just (tc1, []) <- splitTyConApp_maybe ty1
1355 , Just (tc2, []) <- splitTyConApp_maybe ty2
1356 , (tc1 `hasKey` liftedDataConKey && tc2 `hasKey` unliftedDataConKey) ||
1357 (tc2 `hasKey` liftedDataConKey && tc1 `hasKey` unliftedDataConKey)
1358 = addArising orig $
1359 text "Couldn't match a lifted type with an unlifted type"
1360
1361 | otherwise -- So now we have Nothing or (Just IsSwapped)
1362 -- For some reason we treat Nothign like IsSwapped
1363 = addArising orig $
1364 sep [ text herald1 <+> quotes (ppr ty1)
1365 , nest padding $
1366 text herald2 <+> quotes (ppr ty2)
1367 , sameOccExtra ty2 ty1 ]
1368 where
1369 herald1 = conc [ "Couldn't match"
1370 , if is_repr then "representation of" else ""
1371 , if is_oriented then "expected" else ""
1372 , what ]
1373 herald2 = conc [ "with"
1374 , if is_repr then "that of" else ""
1375 , if is_oriented then ("actual " ++ what) else "" ]
1376 padding = length herald1 - length herald2
1377
1378 is_repr = case ctEqRel ct of { ReprEq -> True; NomEq -> False }
1379 is_oriented = isJust oriented
1380
1381 orig = ctOrigin ct
1382 what = case ctLocTypeOrKind_maybe (ctLoc ct) of
1383 Just KindLevel -> "kind"
1384 _ -> "type"
1385
1386 conc :: [String] -> String
1387 conc = foldr1 add_space
1388
1389 add_space :: String -> String -> String
1390 add_space s1 s2 | null s1 = s2
1391 | null s2 = s1
1392 | otherwise = s1 ++ (' ' : s2)
1393
1394 mkExpectedActualMsg :: Type -> Type -> CtOrigin -> Maybe TypeOrKind -> Bool
1395 -> (Bool, Maybe SwapFlag, SDoc)
1396 -- NotSwapped means (actual, expected), IsSwapped is the reverse
1397 -- First return val is whether or not to print a herald above this msg
1398 mkExpectedActualMsg ty1 ty2 (TypeEqOrigin { uo_actual = act
1399 , uo_expected = Check exp
1400 , uo_thing = maybe_thing })
1401 m_level printExpanded
1402 | KindLevel <- level, occurs_check_error = (True, Nothing, empty)
1403 | isUnliftedTypeKind act, isLiftedTypeKind exp = (False, Nothing, msg2)
1404 | isLiftedTypeKind act, isUnliftedTypeKind exp = (False, Nothing, msg3)
1405 | isLiftedTypeKind exp && not (isConstraintKind exp)
1406 = (False, Nothing, msg4)
1407 | Just msg <- num_args_msg = (False, Nothing, msg $$ msg1)
1408 | KindLevel <- level, Just th <- maybe_thing = (False, Nothing, msg5 th)
1409 | act `pickyEqType` ty1, exp `pickyEqType` ty2 = (True, Just NotSwapped, empty)
1410 | exp `pickyEqType` ty1, act `pickyEqType` ty2 = (True, Just IsSwapped, empty)
1411 | otherwise = (True, Nothing, msg1)
1412 where
1413 level = m_level `orElse` TypeLevel
1414
1415 occurs_check_error
1416 | Just act_tv <- tcGetTyVar_maybe act
1417 , act_tv `elemVarSet` tyCoVarsOfType exp
1418 = True
1419 | Just exp_tv <- tcGetTyVar_maybe exp
1420 , exp_tv `elemVarSet` tyCoVarsOfType act
1421 = True
1422 | otherwise
1423 = False
1424
1425 sort = case level of
1426 TypeLevel -> text "type"
1427 KindLevel -> text "kind"
1428
1429 msg1 = case level of
1430 KindLevel
1431 | Just th <- maybe_thing
1432 -> msg5 th
1433
1434 _ | not (act `pickyEqType` exp)
1435 -> vcat [ text "Expected" <+> sort <> colon <+> ppr exp
1436 , text " Actual" <+> sort <> colon <+> ppr act
1437 , if printExpanded then expandedTys else empty ]
1438
1439 | otherwise
1440 -> empty
1441
1442 thing_msg = case maybe_thing of
1443 Just thing -> \_ -> quotes (ppr thing) <+> text "is"
1444 Nothing -> \vowel -> text "got a" <>
1445 if vowel then char 'n' else empty
1446 msg2 = sep [ text "Expecting a lifted type, but"
1447 , thing_msg True, text "unlifted" ]
1448 msg3 = sep [ text "Expecting an unlifted type, but"
1449 , thing_msg False, text "lifted" ]
1450 msg4 = maybe_num_args_msg $$
1451 sep [ text "Expected a type, but"
1452 , maybe (text "found something with kind")
1453 (\thing -> quotes (ppr thing) <+> text "has kind")
1454 maybe_thing
1455 , quotes (ppr act) ]
1456
1457 msg5 th = hang (text "Expected" <+> kind_desc <> comma)
1458 2 (text "but" <+> quotes (ppr th) <+> text "has kind" <+>
1459 quotes (ppr act))
1460 where
1461 kind_desc | isConstraintKind exp = text "a constraint"
1462 | otherwise = text "kind" <+> quotes (ppr exp)
1463
1464 num_args_msg = case level of
1465 TypeLevel -> Nothing
1466 KindLevel
1467 -> let n_act = count_args act
1468 n_exp = count_args exp in
1469 case n_act - n_exp of
1470 n | n /= 0
1471 , Just thing <- maybe_thing
1472 , case errorThingNumArgs_maybe thing of
1473 Nothing -> n > 0
1474 Just num_act_args -> num_act_args >= -n
1475 -- don't report to strip off args that aren't there
1476 -> Just $ text "Expecting" <+> speakN (abs n) <+>
1477 more_or_fewer <+> plural_n (abs n) (text "argument")
1478 <+> text "to" <+> quotes (ppr thing)
1479 where
1480 more_or_fewer | n < 0 = text "fewer"
1481 | otherwise = text "more"
1482 _ -> Nothing
1483
1484
1485 maybe_num_args_msg = case num_args_msg of
1486 Nothing -> empty
1487 Just m -> m
1488
1489 count_args ty = count isVisibleBinder $ fst $ splitPiTys ty
1490
1491 plural_n 1 doc = doc
1492 plural_n _ doc = doc <> char 's'
1493
1494 expandedTys =
1495 ppUnless (expTy1 `pickyEqType` exp && expTy2 `pickyEqType` act) $ vcat
1496 [ text "Type synonyms expanded:"
1497 , text "Expected type:" <+> ppr expTy1
1498 , text " Actual type:" <+> ppr expTy2
1499 ]
1500
1501 (expTy1, expTy2) = expandSynonymsToMatch exp act
1502
1503 mkExpectedActualMsg _ _ _ _ _ = panic "mkExpectedAcutalMsg"
1504
1505 {-
1506 Note [Expanding type synonyms to make types similar]
1507 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1508
1509 In type error messages, if -fprint-expanded-types is used, we want to expand
1510 type synonyms to make expected and found types as similar as possible, but we
1511 shouldn't expand types too much to make type messages even more verbose and
1512 harder to understand. The whole point here is to make the difference in expected
1513 and found types clearer.
1514
1515 `expandSynonymsToMatch` does this, it takes two types, and expands type synonyms
1516 only as much as necessary. It should work like this:
1517
1518 Given two types t1 and t2:
1519
1520 * If they're already same, it shouldn't expand any type synonyms and
1521 just return.
1522
1523 * If they're in form `C1 t1_1 .. t1_n` and `C2 t2_1 .. t2_m` (C1 and C2 are
1524 type constructors), it should expand C1 and C2 if they're different type
1525 synonyms. Then it should continue doing same thing on expanded types. If C1
1526 and C2 are same, then we should apply same procedure to arguments of C1
1527 and argument of C2 to make them as similar as possible.
1528
1529 Most important thing here is to keep number of synonym expansions at
1530 minimum. For example, if t1 is `T (T3, T5, Int)` and t2 is
1531 `T (T5, T3, Bool)` where T5 = T4, T4 = T3, ..., T1 = X, we should return
1532 `T (T3, T3, Int)` and `T (T3, T3, Bool)`.
1533
1534 In the implementation, we just search in all possible solutions for a solution
1535 that does minimum amount of expansions. This leads to a complex algorithm: If
1536 we have two synonyms like X_m = X_{m-1} = .. X and Y_n = Y_{n-1} = .. Y, where
1537 X and Y are rigid types, we expand m * n times. But in practice it's not a
1538 problem because deeply nested synonyms with no intervening rigid type
1539 constructors are vanishingly rare.
1540
1541 -}
1542
1543 -- | Expand type synonyms in given types only enough to make them as equal as
1544 -- possible. Returned types are the same in terms of used type synonyms.
1545 --
1546 -- To expand all synonyms, see 'Type.expandTypeSynonyms'.
1547 expandSynonymsToMatch :: Type -> Type -> (Type, Type)
1548 expandSynonymsToMatch ty1 ty2 = (ty1_ret, ty2_ret)
1549 where
1550 (_, ty1_ret, ty2_ret) = go 0 ty1 ty2
1551
1552 -- | Returns (number of synonym expansions done to make types similar,
1553 -- type synonym expanded version of first type,
1554 -- type synonym expanded version of second type)
1555 --
1556 -- Int argument is number of synonym expansions done so far.
1557 go :: Int -> Type -> Type -> (Int, Type, Type)
1558 go exps t1 t2
1559 | t1 `pickyEqType` t2 =
1560 -- Types are same, nothing to do
1561 (exps, t1, t2)
1562
1563 go exps t1@(TyConApp tc1 tys1) t2@(TyConApp tc2 tys2)
1564 | tc1 == tc2 =
1565 -- Type constructors are same. They may be synonyms, but we don't
1566 -- expand further.
1567 let (exps', tys1', tys2') = unzip3 $ zipWith (go 0) tys1 tys2
1568 in (exps + sum exps', TyConApp tc1 tys1', TyConApp tc2 tys2')
1569 | otherwise =
1570 -- Try to expand type constructors
1571 case (coreView t1, coreView t2) of
1572 -- When only one of the constructors is a synonym, we just
1573 -- expand it and continue search
1574 (Just t1', Nothing) ->
1575 go (exps + 1) t1' t2
1576 (Nothing, Just t2') ->
1577 go (exps + 1) t1 t2'
1578 (Just t1', Just t2') ->
1579 -- Both constructors are synonyms, but they may be synonyms of
1580 -- each other. We just search for minimally expanded solution.
1581 -- See Note [Expanding type synonyms to make types similar].
1582 let sol1@(exp1, _, _) = go (exps + 1) t1' t2
1583 sol2@(exp2, _, _) = go (exps + 1) t1 t2'
1584 in if exp1 < exp2 then sol1 else sol2
1585 (Nothing, Nothing) ->
1586 -- None of the constructors are synonyms, nothing to do
1587 (exps, t1, t2)
1588
1589 go exps t1@TyConApp{} t2
1590 | Just t1' <- coreView t1 = go (exps + 1) t1' t2
1591 | otherwise = (exps, t1, t2)
1592
1593 go exps t1 t2@TyConApp{}
1594 | Just t2' <- coreView t2 = go (exps + 1) t1 t2'
1595 | otherwise = (exps, t1, t2)
1596
1597 go exps (AppTy t1_1 t1_2) (AppTy t2_1 t2_2) =
1598 let (exps1, t1_1', t2_1') = go 0 t1_1 t2_1
1599 (exps2, t1_2', t2_2') = go 0 t1_2 t2_2
1600 in (exps + exps1 + exps2, mkAppTy t1_1' t1_2', mkAppTy t2_1' t2_2')
1601
1602 go exps (ForAllTy (Anon t1_1) t1_2) (ForAllTy (Anon t2_1) t2_2) =
1603 let (exps1, t1_1', t2_1') = go 0 t1_1 t2_1
1604 (exps2, t1_2', t2_2') = go 0 t1_2 t2_2
1605 in (exps + exps1 + exps2, mkFunTy t1_1' t1_2', mkFunTy t2_1' t2_2')
1606
1607 go exps (ForAllTy (Named tv1 vis1) t1) (ForAllTy (Named tv2 vis2) t2) =
1608 -- NOTE: We may have a bug here, but we just can't reproduce it easily.
1609 -- See D1016 comments for details and our attempts at producing a test
1610 -- case. Short version: We probably need RnEnv2 to really get this right.
1611 let (exps1, t1', t2') = go exps t1 t2
1612 in (exps1, ForAllTy (Named tv1 vis1) t1', ForAllTy (Named tv2 vis2) t2')
1613
1614 go exps (CastTy ty1 _) ty2 = go exps ty1 ty2
1615 go exps ty1 (CastTy ty2 _) = go exps ty1 ty2
1616
1617 go exps t1 t2 = (exps, t1, t2)
1618
1619 sameOccExtra :: TcType -> TcType -> SDoc
1620 -- See Note [Disambiguating (X ~ X) errors]
1621 sameOccExtra ty1 ty2
1622 | Just (tc1, _) <- tcSplitTyConApp_maybe ty1
1623 , Just (tc2, _) <- tcSplitTyConApp_maybe ty2
1624 , let n1 = tyConName tc1
1625 n2 = tyConName tc2
1626 same_occ = nameOccName n1 == nameOccName n2
1627 same_pkg = moduleUnitId (nameModule n1) == moduleUnitId (nameModule n2)
1628 , n1 /= n2 -- Different Names
1629 , same_occ -- but same OccName
1630 = text "NB:" <+> (ppr_from same_pkg n1 $$ ppr_from same_pkg n2)
1631 | otherwise
1632 = empty
1633 where
1634 ppr_from same_pkg nm
1635 | isGoodSrcSpan loc
1636 = hang (quotes (ppr nm) <+> text "is defined at")
1637 2 (ppr loc)
1638 | otherwise -- Imported things have an UnhelpfulSrcSpan
1639 = hang (quotes (ppr nm))
1640 2 (sep [ text "is defined in" <+> quotes (ppr (moduleName mod))
1641 , ppUnless (same_pkg || pkg == mainUnitId) $
1642 nest 4 $ text "in package" <+> quotes (ppr pkg) ])
1643 where
1644 pkg = moduleUnitId mod
1645 mod = nameModule nm
1646 loc = nameSrcSpan nm
1647
1648 {-
1649 Note [Suggest adding a type signature]
1650 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1651 The OutsideIn algorithm rejects GADT programs that don't have a principal
1652 type, and indeed some that do. Example:
1653 data T a where
1654 MkT :: Int -> T Int
1655
1656 f (MkT n) = n
1657
1658 Does this have type f :: T a -> a, or f :: T a -> Int?
1659 The error that shows up tends to be an attempt to unify an
1660 untouchable type variable. So suggestAddSig sees if the offending
1661 type variable is bound by an *inferred* signature, and suggests
1662 adding a declared signature instead.
1663
1664 This initially came up in Trac #8968, concerning pattern synonyms.
1665
1666 Note [Disambiguating (X ~ X) errors]
1667 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1668 See Trac #8278
1669
1670 Note [Reporting occurs-check errors]
1671 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1672 Given (a ~ [a]), if 'a' is a rigid type variable bound by a user-supplied
1673 type signature, then the best thing is to report that we can't unify
1674 a with [a], because a is a skolem variable. That avoids the confusing
1675 "occur-check" error message.
1676
1677 But nowadays when inferring the type of a function with no type signature,
1678 even if there are errors inside, we still generalise its signature and
1679 carry on. For example
1680 f x = x:x
1681 Here we will infer somethiing like
1682 f :: forall a. a -> [a]
1683 with a suspended error of (a ~ [a]). So 'a' is now a skolem, but not
1684 one bound by the programmer! Here we really should report an occurs check.
1685
1686 So isUserSkolem distinguishes the two.
1687
1688 Note [Non-injective type functions]
1689 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1690 It's very confusing to get a message like
1691 Couldn't match expected type `Depend s'
1692 against inferred type `Depend s1'
1693 so mkTyFunInfoMsg adds:
1694 NB: `Depend' is type function, and hence may not be injective
1695
1696 Warn of loopy local equalities that were dropped.
1697
1698
1699 ************************************************************************
1700 * *
1701 Type-class errors
1702 * *
1703 ************************************************************************
1704 -}
1705
1706 mkDictErr :: ReportErrCtxt -> [Ct] -> TcM ErrMsg
1707 mkDictErr ctxt cts
1708 = ASSERT( not (null cts) )
1709 do { inst_envs <- tcGetInstEnvs
1710 ; let (ct1:_) = cts -- ct1 just for its location
1711 min_cts = elim_superclasses cts
1712 lookups = map (lookup_cls_inst inst_envs) min_cts
1713 (no_inst_cts, overlap_cts) = partition is_no_inst lookups
1714
1715 -- Report definite no-instance errors,
1716 -- or (iff there are none) overlap errors
1717 -- But we report only one of them (hence 'head') because they all
1718 -- have the same source-location origin, to try avoid a cascade
1719 -- of error from one location
1720 ; (ctxt, err) <- mk_dict_err ctxt (head (no_inst_cts ++ overlap_cts))
1721 ; mkErrorMsgFromCt ctxt ct1 (important err) }
1722 where
1723 no_givens = null (getUserGivens ctxt)
1724
1725 is_no_inst (ct, (matches, unifiers, _))
1726 = no_givens
1727 && null matches
1728 && (null unifiers || all (not . isAmbiguousTyVar) (varSetElems (tyCoVarsOfCt ct)))
1729
1730 lookup_cls_inst inst_envs ct
1731 -- Note [Flattening in error message generation]
1732 = (ct, lookupInstEnv True inst_envs clas (flattenTys emptyInScopeSet tys))
1733 where
1734 (clas, tys) = getClassPredTys (ctPred ct)
1735
1736
1737 -- When simplifying [W] Ord (Set a), we need
1738 -- [W] Eq a, [W] Ord a
1739 -- but we really only want to report the latter
1740 elim_superclasses cts
1741 = filter (\ct -> any (eqType (ctPred ct)) min_preds) cts
1742 where
1743 min_preds = mkMinimalBySCs (map ctPred cts)
1744
1745 mk_dict_err :: ReportErrCtxt -> (Ct, ClsInstLookupResult)
1746 -> TcM (ReportErrCtxt, SDoc)
1747 -- Report an overlap error if this class constraint results
1748 -- from an overlap (returning Left clas), otherwise return (Right pred)
1749 mk_dict_err ctxt (ct, (matches, unifiers, unsafe_overlapped))
1750 | null matches -- No matches but perhaps several unifiers
1751 = do { (ctxt, binds_msg, ct) <- relevantBindings True ctxt ct
1752 ; return (ctxt, cannot_resolve_msg ct binds_msg) }
1753
1754 | null unsafe_overlapped -- Some matches => overlap errors
1755 = return (ctxt, overlap_msg)
1756
1757 | otherwise
1758 = return (ctxt, safe_haskell_msg)
1759 where
1760 orig = ctOrigin ct
1761 pred = ctPred ct
1762 (clas, tys) = getClassPredTys pred
1763 ispecs = [ispec | (ispec, _) <- matches]
1764 unsafe_ispecs = [ispec | (ispec, _) <- unsafe_overlapped]
1765 givens = getUserGivens ctxt
1766 all_tyvars = all isTyVarTy tys
1767
1768
1769 cannot_resolve_msg :: Ct -> SDoc -> SDoc
1770 cannot_resolve_msg ct binds_msg
1771 = vcat [ no_inst_msg
1772 , nest 2 extra_note
1773 , vcat (pp_givens givens)
1774 , ppWhen (has_ambig_tvs && not (null unifiers && null givens))
1775 (vcat [ ppUnless lead_with_ambig ambig_msg, binds_msg, potential_msg ])
1776 , show_fixes (add_to_ctxt_fixes has_ambig_tvs ++ drv_fixes) ]
1777 where
1778 orig = ctOrigin ct
1779 -- See Note [Highlighting ambiguous type variables]
1780 lead_with_ambig = has_ambig_tvs && not (any isRuntimeUnkSkol ambig_tvs)
1781 && not (null unifiers) && null givens
1782
1783 (has_ambig_tvs, ambig_msg) = mkAmbigMsg lead_with_ambig ct
1784 ambig_tvs = uncurry (++) (getAmbigTkvs ct)
1785
1786 no_inst_msg
1787 | lead_with_ambig
1788 = ambig_msg <+> pprArising orig
1789 $$ text "prevents the constraint" <+> quotes (pprParendType pred)
1790 <+> text "from being solved."
1791
1792 | null givens
1793 = addArising orig $ text "No instance for"
1794 <+> pprParendType pred
1795
1796 | otherwise
1797 = addArising orig $ text "Could not deduce"
1798 <+> pprParendType pred
1799
1800 potential_msg
1801 = ppWhen (not (null unifiers) && want_potential orig) $
1802 sdocWithDynFlags $ \dflags ->
1803 getPprStyle $ \sty ->
1804 pprPotentials dflags sty potential_hdr unifiers
1805
1806 potential_hdr
1807 = vcat [ ppWhen lead_with_ambig $
1808 text "Probable fix: use a type annotation to specify what"
1809 <+> pprQuotedList ambig_tvs <+> text "should be."
1810 , text "These potential instance" <> plural unifiers
1811 <+> text "exist:"]
1812
1813 -- Report "potential instances" only when the constraint arises
1814 -- directly from the user's use of an overloaded function
1815 want_potential (TypeEqOrigin {}) = False
1816 want_potential _ = True
1817
1818 add_to_ctxt_fixes has_ambig_tvs
1819 | not has_ambig_tvs && all_tyvars
1820 , (orig:origs) <- usefulContext ctxt pred
1821 = [sep [ text "add" <+> pprParendType pred
1822 <+> text "to the context of"
1823 , nest 2 $ ppr_skol orig $$
1824 vcat [ text "or" <+> ppr_skol orig
1825 | orig <- origs ] ] ]
1826 | otherwise = []
1827
1828 ppr_skol (PatSkol dc _) = text "the data constructor" <+> quotes (ppr dc)
1829 ppr_skol skol_info = ppr skol_info
1830
1831 extra_note | any isFunTy (filterOutInvisibleTypes (classTyCon clas) tys)
1832 = text "(maybe you haven't applied a function to enough arguments?)"
1833 | className clas == typeableClassName -- Avoid mysterious "No instance for (Typeable T)
1834 , [_,ty] <- tys -- Look for (Typeable (k->*) (T k))
1835 , Just (tc,_) <- tcSplitTyConApp_maybe ty
1836 , not (isTypeFamilyTyCon tc)
1837 = hang (text "GHC can't yet do polykinded")
1838 2 (text "Typeable" <+>
1839 parens (ppr ty <+> dcolon <+> ppr (typeKind ty)))
1840 | otherwise
1841 = empty
1842
1843 drv_fixes = case orig of
1844 DerivOrigin -> [drv_fix]
1845 DerivOriginDC {} -> [drv_fix]
1846 DerivOriginCoerce {} -> [drv_fix]
1847 _ -> []
1848
1849 drv_fix = hang (text "use a standalone 'deriving instance' declaration,")
1850 2 (text "so you can specify the instance context yourself")
1851
1852 -- Normal overlap error
1853 overlap_msg
1854 = ASSERT( not (null matches) )
1855 vcat [ addArising orig (text "Overlapping instances for"
1856 <+> pprType (mkClassPred clas tys))
1857
1858 , ppUnless (null matching_givens) $
1859 sep [text "Matching givens (or their superclasses):"
1860 , nest 2 (vcat matching_givens)]
1861
1862 , sdocWithDynFlags $ \dflags ->
1863 getPprStyle $ \sty ->
1864 pprPotentials dflags sty (text "Matching instances:") $
1865 ispecs ++ unifiers
1866
1867 , ppWhen (null matching_givens && isSingleton matches && null unifiers) $
1868 -- Intuitively, some given matched the wanted in their
1869 -- flattened or rewritten (from given equalities) form
1870 -- but the matcher can't figure that out because the
1871 -- constraints are non-flat and non-rewritten so we
1872 -- simply report back the whole given
1873 -- context. Accelerate Smart.hs showed this problem.
1874 sep [ text "There exists a (perhaps superclass) match:"
1875 , nest 2 (vcat (pp_givens givens))]
1876
1877 , ppWhen (isSingleton matches) $
1878 parens (vcat [ text "The choice depends on the instantiation of" <+>
1879 quotes (pprWithCommas ppr (tyCoVarsOfTypesList tys))
1880 , ppWhen (null (matching_givens)) $
1881 vcat [ text "To pick the first instance above, use IncoherentInstances"
1882 , text "when compiling the other instance declarations"]
1883 ])]
1884 where
1885 givens = getUserGivens ctxt
1886 matching_givens = mapMaybe matchable givens
1887
1888 matchable (evvars,skol_info,_,loc)
1889 = case ev_vars_matching of
1890 [] -> Nothing
1891 _ -> Just $ hang (pprTheta ev_vars_matching)
1892 2 (sep [ text "bound by" <+> ppr skol_info
1893 , text "at" <+> ppr loc])
1894 where ev_vars_matching = filter ev_var_matches (map evVarPred evvars)
1895 ev_var_matches ty = case getClassPredTys_maybe ty of
1896 Just (clas', tys')
1897 | clas' == clas
1898 , Just _ <- tcMatchTys tys tys'
1899 -> True
1900 | otherwise
1901 -> any ev_var_matches (immSuperClasses clas' tys')
1902 Nothing -> False
1903
1904 -- Overlap error because of Safe Haskell (first
1905 -- match should be the most specific match)
1906 safe_haskell_msg
1907 = ASSERT( length matches == 1 && not (null unsafe_ispecs) )
1908 vcat [ addArising orig (text "Unsafe overlapping instances for"
1909 <+> pprType (mkClassPred clas tys))
1910 , sep [text "The matching instance is:",
1911 nest 2 (pprInstance $ head ispecs)]
1912 , vcat [ text "It is compiled in a Safe module and as such can only"
1913 , text "overlap instances from the same module, however it"
1914 , text "overlaps the following instances from different" <+>
1915 text "modules:"
1916 , nest 2 (vcat [pprInstances $ unsafe_ispecs])
1917 ]
1918 ]
1919
1920 {- Note [Highlighting ambiguous type variables]
1921 -----------------------------------------------
1922 When we encounter ambiguous type variables (i.e. type variables
1923 that remain metavariables after type inference), we need a few more
1924 conditions before we can reason that *ambiguity* prevents constraints
1925 from being solved:
1926 - We can't have any givens, as encountering a typeclass error
1927 with given constraints just means we couldn't deduce
1928 a solution satisfying those constraints and as such couldn't
1929 bind the type variable to a known type.
1930 - If we don't have any unifiers, we don't even have potential
1931 instances from which an ambiguity could arise.
1932 - Lastly, I don't want to mess with error reporting for
1933 unknown runtime types so we just fall back to the old message there.
1934 Once these conditions are satisfied, we can safely say that ambiguity prevents
1935 the constraint from being solved. -}
1936
1937
1938 usefulContext :: ReportErrCtxt -> TcPredType -> [SkolemInfo]
1939 usefulContext ctxt pred
1940 = go (cec_encl ctxt)
1941 where
1942 pred_tvs = tyCoVarsOfType pred
1943 go [] = []
1944 go (ic : ics)
1945 | implausible ic = rest
1946 | otherwise = ic_info ic : rest
1947 where
1948 -- Stop when the context binds a variable free in the predicate
1949 rest | any (`elemVarSet` pred_tvs) (ic_skols ic) = []
1950 | otherwise = go ics
1951
1952 implausible ic
1953 | null (ic_skols ic) = True
1954 | implausible_info (ic_info ic) = True
1955 | otherwise = False
1956
1957 implausible_info (SigSkol (InfSigCtxt {}) _) = True
1958 implausible_info _ = False
1959 -- Do not suggest adding constraints to an *inferred* type signature!
1960
1961 show_fixes :: [SDoc] -> SDoc
1962 show_fixes [] = empty
1963 show_fixes (f:fs) = sep [ text "Possible fix:"
1964 , nest 2 (vcat (f : map (text "or" <+>) fs))]
1965
1966 pprPotentials :: DynFlags -> PprStyle -> SDoc -> [ClsInst] -> SDoc
1967 -- See Note [Displaying potential instances]
1968 pprPotentials dflags sty herald insts
1969 | null insts
1970 = empty
1971
1972 | null show_these
1973 = hang herald
1974 2 (vcat [ not_in_scope_msg empty
1975 , flag_hint ])
1976
1977 | otherwise
1978 = hang herald
1979 2 (vcat [ pprInstances show_these
1980 , ppWhen (n_in_scope_hidden > 0) $
1981 text "...plus"
1982 <+> speakNOf n_in_scope_hidden (text "other")
1983 , not_in_scope_msg (text "...plus")
1984 , flag_hint ])
1985 where
1986 n_show = 3 :: Int
1987 show_potentials = gopt Opt_PrintPotentialInstances dflags
1988
1989 (in_scope, not_in_scope) = partition inst_in_scope insts
1990 sorted = sortBy fuzzyClsInstCmp in_scope
1991 show_these | show_potentials = sorted
1992 | otherwise = take n_show sorted
1993 n_in_scope_hidden = length sorted - length show_these
1994
1995 -- "in scope" means that all the type constructors
1996 -- are lexically in scope; these instances are likely
1997 -- to be more useful
1998 inst_in_scope :: ClsInst -> Bool
1999 inst_in_scope cls_inst = foldNameSet ((&&) . name_in_scope) True $
2000 orphNamesOfTypes (is_tys cls_inst)
2001
2002 name_in_scope name
2003 | isBuiltInSyntax name
2004 = True -- E.g. (->)
2005 | Just mod <- nameModule_maybe name
2006 = qual_in_scope (qualName sty mod (nameOccName name))
2007 | otherwise
2008 = True
2009
2010 qual_in_scope :: QualifyName -> Bool
2011 qual_in_scope NameUnqual = True
2012 qual_in_scope (NameQual {}) = True
2013 qual_in_scope _ = False
2014
2015 not_in_scope_msg herald
2016 | null not_in_scope
2017 = empty
2018 | otherwise
2019 = hang (herald <+> speakNOf (length not_in_scope)
2020 (text "instance involving out-of-scope types"))
2021 2 (ppWhen show_potentials (pprInstances not_in_scope))
2022
2023 flag_hint = ppUnless (show_potentials || length show_these == length insts) $
2024 text "(use -fprint-potential-instances to see them all)"
2025
2026 {- Note [Displaying potential instances]
2027 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2028 When showing a list of instances for
2029 - overlapping instances (show ones that match)
2030 - no such instance (show ones that could match)
2031 we want to give it a bit of structure. Here's the plan
2032
2033 * Say that an instance is "in scope" if all of the
2034 type constructors it mentions are lexically in scope.
2035 These are the ones most likely to be useful to the programmer.
2036
2037 * Show at most n_show in-scope instances,
2038 and summarise the rest ("plus 3 others")
2039
2040 * Summarise the not-in-scope instances ("plus 4 not in scope")
2041
2042 * Add the flag -fshow-potential-instances which replaces the
2043 summary with the full list
2044 -}
2045
2046 {-
2047 Note [Flattening in error message generation]
2048 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2049 Consider (C (Maybe (F x))), where F is a type function, and we have
2050 instances
2051 C (Maybe Int) and C (Maybe a)
2052 Since (F x) might turn into Int, this is an overlap situation, and
2053 indeed (because of flattening) the main solver will have refrained
2054 from solving. But by the time we get to error message generation, we've
2055 un-flattened the constraint. So we must *re*-flatten it before looking
2056 up in the instance environment, lest we only report one matching
2057 instance when in fact there are two.
2058
2059 Re-flattening is pretty easy, because we don't need to keep track of
2060 evidence. We don't re-use the code in TcCanonical because that's in
2061 the TcS monad, and we are in TcM here.
2062
2063 Note [Suggest -fprint-explicit-kinds]
2064 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2065 It can be terribly confusing to get an error message like (Trac #9171)
2066 Couldn't match expected type ‘GetParam Base (GetParam Base Int)’
2067 with actual type ‘GetParam Base (GetParam Base Int)’
2068 The reason may be that the kinds don't match up. Typically you'll get
2069 more useful information, but not when it's as a result of ambiguity.
2070 This test suggests -fprint-explicit-kinds when all the ambiguous type
2071 variables are kind variables.
2072 -}
2073
2074 mkAmbigMsg :: Bool -- True when message has to be at beginning of sentence
2075 -> Ct -> (Bool, SDoc)
2076 mkAmbigMsg prepend_msg ct
2077 | null ambig_kvs && null ambig_tvs = (False, empty)
2078 | otherwise = (True, msg)
2079 where
2080 (ambig_kvs, ambig_tvs) = getAmbigTkvs ct
2081
2082 msg | any isRuntimeUnkSkol ambig_kvs -- See Note [Runtime skolems]
2083 || any isRuntimeUnkSkol ambig_tvs
2084 = vcat [ text "Cannot resolve unknown runtime type"
2085 <> plural ambig_tvs <+> pprQuotedList ambig_tvs
2086 , text "Use :print or :force to determine these types"]
2087
2088 | not (null ambig_tvs)
2089 = pp_ambig (text "type") ambig_tvs
2090
2091 | otherwise -- All ambiguous kind variabes; suggest -fprint-explicit-kinds
2092 = vcat [ pp_ambig (text "kind") ambig_kvs
2093 , sdocWithDynFlags suggest_explicit_kinds ]
2094
2095 pp_ambig what tkvs
2096 | prepend_msg -- "Ambiguous type variable 't0'"
2097 = text "Ambiguous" <+> what <+> text "variable"
2098 <> plural tkvs <+> pprQuotedList tkvs
2099
2100 | otherwise -- "The type variable 't0' is ambiguous"
2101 = text "The" <+> what <+> text "variable" <> plural tkvs
2102 <+> pprQuotedList tkvs <+> is_or_are tkvs <+> text "ambiguous"
2103
2104 is_or_are [_] = text "is"
2105 is_or_are _ = text "are"
2106
2107 suggest_explicit_kinds dflags -- See Note [Suggest -fprint-explicit-kinds]
2108 | gopt Opt_PrintExplicitKinds dflags = empty
2109 | otherwise = text "Use -fprint-explicit-kinds to see the kind arguments"
2110
2111 pprSkol :: [Implication] -> TcTyVar -> SDoc
2112 pprSkol implics tv
2113 | (skol_tvs, skol_info) <- getSkolemInfo implics tv
2114 = case skol_info of
2115 UnkSkol -> pp_tv <+> text "is an unknown type variable"
2116 SigSkol ctxt ty -> ppr_rigid (pprSigSkolInfo ctxt
2117 (mkCheckExpType $
2118 mkSpecForAllTys skol_tvs
2119 (checkingExpType "pprSkol" ty)))
2120 _ -> ppr_rigid (pprSkolInfo skol_info)
2121 where
2122 pp_tv = quotes (ppr tv)
2123 ppr_rigid pp_info = hang (pp_tv <+> text "is a rigid type variable bound by")
2124 2 (sep [ pp_info
2125 , text "at" <+> ppr (getSrcLoc tv) ])
2126
2127 getAmbigTkvs :: Ct -> ([Var],[Var])
2128 getAmbigTkvs ct
2129 = partition (`elemVarSet` dep_tkv_set) ambig_tkvs
2130 where
2131 tkv_set = tyCoVarsOfCt ct
2132 ambig_tkv_set = filterVarSet isAmbiguousTyVar tkv_set
2133 dep_tkv_set = tyCoVarsOfTypes (map tyVarKind (varSetElems tkv_set))
2134 ambig_tkvs = varSetElems ambig_tkv_set
2135
2136 getSkolemInfo :: [Implication] -> TcTyVar -> ([TcTyVar], SkolemInfo)
2137 -- Get the skolem info for a type variable
2138 -- from the implication constraint that binds it
2139 getSkolemInfo [] tv
2140 = pprPanic "No skolem info:" (ppr tv)
2141
2142 getSkolemInfo (implic:implics) tv
2143 | let skols = ic_skols implic
2144 , tv `elem` ic_skols implic = (skols, ic_info implic)
2145 | otherwise = getSkolemInfo implics tv
2146
2147 -----------------------
2148 -- relevantBindings looks at the value environment and finds values whose
2149 -- types mention any of the offending type variables. It has to be
2150 -- careful to zonk the Id's type first, so it has to be in the monad.
2151 -- We must be careful to pass it a zonked type variable, too.
2152 --
2153 -- We always remove closed top-level bindings, though,
2154 -- since they are never relevant (cf Trac #8233)
2155
2156 relevantBindings :: Bool -- True <=> filter by tyvar; False <=> no filtering
2157 -- See Trac #8191
2158 -> ReportErrCtxt -> Ct
2159 -> TcM (ReportErrCtxt, SDoc, Ct)
2160 -- Also returns the zonked and tidied CtOrigin of the constraint
2161 relevantBindings want_filtering ctxt ct
2162 = do { dflags <- getDynFlags
2163 ; (env1, tidy_orig) <- zonkTidyOrigin (cec_tidy ctxt) (ctLocOrigin loc)
2164 ; let ct_tvs = tyCoVarsOfCt ct `unionVarSet` extra_tvs
2165
2166 -- For *kind* errors, report the relevant bindings of the
2167 -- enclosing *type* equality, because that's more useful for the programmer
2168 extra_tvs = case tidy_orig of
2169 KindEqOrigin t1 m_t2 _ _ -> tyCoVarsOfTypes $
2170 t1 : maybeToList m_t2
2171 _ -> emptyVarSet
2172 ; traceTc "relevantBindings" $
2173 vcat [ ppr ct
2174 , pprCtOrigin (ctLocOrigin loc)
2175 , ppr ct_tvs
2176 , pprWithCommas id [ ppr id <+> dcolon <+> ppr (idType id)
2177 | TcIdBndr id _ <- tcl_bndrs lcl_env ]
2178 , pprWithCommas id
2179 [ ppr id | TcIdBndr_ExpType id _ _ <- tcl_bndrs lcl_env ] ]
2180
2181 ; (tidy_env', docs, discards)
2182 <- go env1 ct_tvs (maxRelevantBinds dflags)
2183 emptyVarSet [] False
2184 (tcl_bndrs lcl_env)
2185 -- tcl_bndrs has the innermost bindings first,
2186 -- which are probably the most relevant ones
2187
2188 ; let doc = ppUnless (null docs) $
2189 hang (text "Relevant bindings include")
2190 2 (vcat docs $$ ppWhen discards discardMsg)
2191
2192 -- Put a zonked, tidied CtOrigin into the Ct
2193 loc' = setCtLocOrigin loc tidy_orig
2194 ct' = setCtLoc ct loc'
2195 ctxt' = ctxt { cec_tidy = tidy_env' }
2196
2197 ; return (ctxt', doc, ct') }
2198 where
2199 ev = ctEvidence ct
2200 loc = ctEvLoc ev
2201 lcl_env = ctLocEnv loc
2202
2203 run_out :: Maybe Int -> Bool
2204 run_out Nothing = False
2205 run_out (Just n) = n <= 0
2206
2207 dec_max :: Maybe Int -> Maybe Int
2208 dec_max = fmap (\n -> n - 1)
2209
2210 go :: TidyEnv -> TcTyVarSet -> Maybe Int -> TcTyVarSet -> [SDoc]
2211 -> Bool -- True <=> some filtered out due to lack of fuel
2212 -> [TcIdBinder]
2213 -> TcM (TidyEnv, [SDoc], Bool) -- The bool says if we filtered any out
2214 -- because of lack of fuel
2215 go tidy_env _ _ _ docs discards []
2216 = return (tidy_env, reverse docs, discards)
2217 go tidy_env ct_tvs n_left tvs_seen docs discards (tc_bndr : tc_bndrs)
2218 = case tc_bndr of
2219 TcIdBndr id top_lvl -> go2 (idName id) (idType id) top_lvl
2220 TcIdBndr_ExpType name et top_lvl ->
2221 do { mb_ty <- readExpType_maybe et
2222 -- et really should be filled in by now. But there's a chance
2223 -- it hasn't, if, say, we're reporting a kind error en route to
2224 -- checking a term. See test indexed-types/should_fail/T8129
2225 ; ty <- case mb_ty of
2226 Just ty -> return ty
2227 Nothing -> do { traceTc "Defaulting an ExpType in relevantBindings"
2228 (ppr et)
2229 ; expTypeToType et }
2230 ; go2 name ty top_lvl }
2231 where
2232 go2 id_name id_type top_lvl
2233 = do { (tidy_env', tidy_ty) <- zonkTidyTcType tidy_env id_type
2234 ; traceTc "relevantBindings 1" (ppr id_name <+> dcolon <+> ppr tidy_ty)
2235 ; let id_tvs = tyCoVarsOfType tidy_ty
2236 doc = sep [ pprPrefixOcc id_name <+> dcolon <+> ppr tidy_ty
2237 , nest 2 (parens (text "bound at"
2238 <+> ppr (getSrcLoc id_name)))]
2239 new_seen = tvs_seen `unionVarSet` id_tvs
2240
2241 ; if (want_filtering && not opt_PprStyle_Debug
2242 && id_tvs `disjointVarSet` ct_tvs)
2243 -- We want to filter out this binding anyway
2244 -- so discard it silently
2245 then go tidy_env ct_tvs n_left tvs_seen docs discards tc_bndrs
2246
2247 else if isTopLevel top_lvl && not (isNothing n_left)
2248 -- It's a top-level binding and we have not specified
2249 -- -fno-max-relevant-bindings, so discard it silently
2250 then go tidy_env ct_tvs n_left tvs_seen docs discards tc_bndrs
2251
2252 else if run_out n_left && id_tvs `subVarSet` tvs_seen
2253 -- We've run out of n_left fuel and this binding only
2254 -- mentions aleady-seen type variables, so discard it
2255 then go tidy_env ct_tvs n_left tvs_seen docs True tc_bndrs
2256
2257 -- Keep this binding, decrement fuel
2258 else go tidy_env' ct_tvs (dec_max n_left) new_seen (doc:docs) discards tc_bndrs }
2259
2260 discardMsg :: SDoc
2261 discardMsg = text "(Some bindings suppressed;" <+>
2262 text "use -fmax-relevant-binds=N or -fno-max-relevant-binds)"
2263
2264 -----------------------
2265 warnDefaulting :: [Ct] -> Type -> TcM ()
2266 warnDefaulting wanteds default_ty
2267 = do { warn_default <- woptM Opt_WarnTypeDefaults
2268 ; env0 <- tcInitTidyEnv
2269 ; let tidy_env = tidyFreeTyCoVars env0 $
2270 foldr (unionVarSet . tyCoVarsOfCt) emptyVarSet wanteds
2271 tidy_wanteds = map (tidyCt tidy_env) wanteds
2272 (loc, ppr_wanteds) = pprWithArising tidy_wanteds
2273 warn_msg =
2274 hang (hsep [ text "Defaulting the following"
2275 , text "constraint" <> plural tidy_wanteds
2276 , text "to type"
2277 , quotes (ppr default_ty) ])
2278 2
2279 ppr_wanteds
2280 ; setCtLocM loc $ warnTc warn_default warn_msg }
2281
2282 {-
2283 Note [Runtime skolems]
2284 ~~~~~~~~~~~~~~~~~~~~~~
2285 We want to give a reasonably helpful error message for ambiguity
2286 arising from *runtime* skolems in the debugger. These
2287 are created by in RtClosureInspect.zonkRTTIType.
2288
2289 ************************************************************************
2290 * *
2291 Error from the canonicaliser
2292 These ones are called *during* constraint simplification
2293 * *
2294 ************************************************************************
2295 -}
2296
2297 solverDepthErrorTcS :: CtLoc -> TcType -> TcM a
2298 solverDepthErrorTcS loc ty
2299 = setCtLocM loc $
2300 do { ty <- zonkTcType ty
2301 ; env0 <- tcInitTidyEnv
2302 ; let tidy_env = tidyFreeTyCoVars env0 (tyCoVarsOfType ty)
2303 tidy_ty = tidyType tidy_env ty
2304 msg
2305 = vcat [ text "Reduction stack overflow; size =" <+> ppr depth
2306 , hang (text "When simplifying the following type:")
2307 2 (ppr tidy_ty)
2308 , note ]
2309 ; failWithTcM (tidy_env, msg) }
2310 where
2311 depth = ctLocDepth loc
2312 note = vcat
2313 [ text "Use -freduction-depth=0 to disable this check"
2314 , text "(any upper bound you could choose might fail unpredictably with"
2315 , text " minor updates to GHC, so disabling the check is recommended if"
2316 , text " you're sure that type checking should terminate)" ]