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