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