f32215b315259ba1d113133e5804eec840428578
[ghc.git] / compiler / typecheck / TcErrors.hs
1 {-# LANGUAGE CPP, ScopedTypeVariables #-}
2
3 module TcErrors(
4 reportUnsolved, reportAllUnsolved,
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 TypeRep
17 import Type
18 import Kind ( isKind )
19 import Unify ( tcMatchTys )
20 import Module
21 import FamInst
22 import Inst
23 import InstEnv
24 import TyCon
25 import DataCon
26 import TcEvidence
27 import Name
28 import RdrName ( lookupGRE_Name, GlobalRdrEnv )
29 import Id
30 import Var
31 import VarSet
32 import VarEnv
33 import NameEnv
34 import Bag
35 import ErrUtils ( ErrMsg, pprLocErrMsg )
36 import BasicTypes
37 import Util
38 import FastString
39 import Outputable
40 import SrcLoc
41 import DynFlags
42 import StaticFlags ( opt_PprStyle_Debug )
43 import ListSetOps ( equivClasses )
44
45 import Control.Monad ( when )
46 import Data.Maybe
47 import Data.List ( partition, mapAccumL, nub, sortBy )
48
49 {-
50 ************************************************************************
51 * *
52 \section{Errors and contexts}
53 * *
54 ************************************************************************
55
56 ToDo: for these error messages, should we note the location as coming
57 from the insts, or just whatever seems to be around in the monad just
58 now?
59
60 Note [Deferring coercion errors to runtime]
61 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
62 While developing, sometimes it is desirable to allow compilation to succeed even
63 if there are type errors in the code. Consider the following case:
64
65 module Main where
66
67 a :: Int
68 a = 'a'
69
70 main = print "b"
71
72 Even though `a` is ill-typed, it is not used in the end, so if all that we're
73 interested in is `main` it is handy to be able to ignore the problems in `a`.
74
75 Since we treat type equalities as evidence, this is relatively simple. Whenever
76 we run into a type mismatch in TcUnify, we normally just emit an error. But it
77 is always safe to defer the mismatch to the main constraint solver. If we do
78 that, `a` will get transformed into
79
80 co :: Int ~ Char
81 co = ...
82
83 a :: Int
84 a = 'a' `cast` co
85
86 The constraint solver would realize that `co` is an insoluble constraint, and
87 emit an error with `reportUnsolved`. But we can also replace the right-hand side
88 of `co` with `error "Deferred type error: Int ~ Char"`. This allows the program
89 to compile, and it will run fine unless we evaluate `a`. This is what
90 `deferErrorsToRuntime` does.
91
92 It does this by keeping track of which errors correspond to which coercion
93 in TcErrors. TcErrors.reportTidyWanteds does not print the errors
94 and does not fail if -fdefer-type-errors is on, so that we can continue
95 compilation. The errors are turned into warnings in `reportUnsolved`.
96 -}
97
98 reportUnsolved :: WantedConstraints -> TcM (Bag EvBind)
99 reportUnsolved wanted
100 = do { binds_var <- newTcEvBinds
101 ; defer_errors <- goptM Opt_DeferTypeErrors
102
103 ; defer_holes <- goptM Opt_DeferTypedHoles
104 ; warn_holes <- woptM Opt_WarnTypedHoles
105 ; let expr_holes | not defer_holes = HoleError
106 | warn_holes = HoleWarn
107 | otherwise = HoleDefer
108
109 ; partial_sigs <- xoptM Opt_PartialTypeSignatures
110 ; warn_partial_sigs <- woptM Opt_WarnPartialTypeSignatures
111 ; let type_holes | not partial_sigs = HoleError
112 | warn_partial_sigs = HoleWarn
113 | otherwise = HoleDefer
114
115 ; report_unsolved (Just binds_var) defer_errors expr_holes type_holes wanted
116 ; getTcEvBinds binds_var }
117
118 reportAllUnsolved :: WantedConstraints -> TcM ()
119 -- Report *all* unsolved goals as errors, even if -fdefer-type-errors is on
120 -- See Note [Deferring coercion errors to runtime]
121 reportAllUnsolved wanted
122 = report_unsolved Nothing False HoleError HoleError wanted
123
124 report_unsolved :: Maybe EvBindsVar -- cec_binds
125 -> Bool -- cec_defer_type_errors
126 -> HoleChoice -- Expression holes
127 -> HoleChoice -- Type holes
128 -> WantedConstraints -> TcM ()
129 -- Important precondition:
130 -- WantedConstraints are fully zonked and unflattened, that is,
131 -- zonkWC has already been applied to these constraints.
132 report_unsolved mb_binds_var defer_errors expr_holes type_holes wanted
133 | isEmptyWC wanted
134 = return ()
135 | otherwise
136 = do { traceTc "reportUnsolved (before unflattening)" (ppr wanted)
137 ; warn_redundant <- woptM Opt_WarnRedundantConstraints
138
139 ; env0 <- tcInitTidyEnv
140
141 -- If we are deferring we are going to need /all/ evidence around,
142 -- including the evidence produced by unflattening (zonkWC)
143 ; let tidy_env = tidyFreeTyVars env0 free_tvs
144 free_tvs = tyVarsOfWC wanted
145 err_ctxt = CEC { cec_encl = []
146 , cec_tidy = tidy_env
147 , cec_defer_type_errors = defer_errors
148 , cec_expr_holes = expr_holes
149 , cec_type_holes = type_holes
150 , cec_suppress = False -- See Note [Suppressing error messages]
151 , cec_warn_redundant = warn_redundant
152 , cec_binds = mb_binds_var }
153
154 ; traceTc "reportUnsolved (after unflattening):" $
155 vcat [ pprTvBndrs (varSetElems free_tvs)
156 , ppr wanted ]
157
158 ; reportWanteds err_ctxt wanted }
159
160 --------------------------------------------
161 -- Internal functions
162 --------------------------------------------
163
164 data HoleChoice
165 = HoleError -- A hole is a compile-time error
166 | HoleWarn -- Defer to runtime, emit a compile-time warning
167 | HoleDefer -- Defer to runtime, no warning
168
169 data ReportErrCtxt
170 = CEC { cec_encl :: [Implication] -- Enclosing implications
171 -- (innermost first)
172 -- ic_skols and givens are tidied, rest are not
173 , cec_tidy :: TidyEnv
174 , cec_binds :: Maybe EvBindsVar
175 -- Nothinng <=> Report all errors, including holes; no bindings
176 -- Just ev <=> make some errors (depending on cec_defer)
177 -- into warnings, and emit evidence bindings
178 -- into 'ev' for unsolved constraints
179
180 , cec_defer_type_errors :: Bool -- True <=> -fdefer-type-errors
181 -- Defer type errors until runtime
182 -- Irrelevant if cec_binds = Nothing
183
184 , cec_expr_holes :: HoleChoice -- Holes in expressions
185 , cec_type_holes :: HoleChoice -- Holes in types
186
187 , cec_warn_redundant :: Bool -- True <=> -fwarn-redundant-constraints
188
189 , cec_suppress :: Bool -- True <=> More important errors have occurred,
190 -- so create bindings if need be, but
191 -- don't issue any more errors/warnings
192 -- See Note [Suppressing error messages]
193 }
194
195 {-
196 Note [Suppressing error messages]
197 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
198 The cec_suppress flag says "don't report any errors". Instead, just create
199 evidence bindings (as usual). It's used when more important errors have occurred.
200
201 Specifically (see reportWanteds)
202 * If there are insoluble Givens, then we are in unreachable code and all bets
203 are off. So don't report any further errors.
204 * If there are any insolubles (eg Int~Bool), here or in a nested implication,
205 then suppress errors from the simple constraints here. Sometimes the
206 simple-constraint errors are a knock-on effect of the insolubles.
207 -}
208
209 reportImplic :: ReportErrCtxt -> Implication -> TcM ()
210 reportImplic ctxt implic@(Implic { ic_skols = tvs, ic_given = given
211 , ic_wanted = wanted, ic_binds = evb
212 , ic_status = status, ic_info = info
213 , ic_env = tcl_env })
214 | BracketSkol <- info
215 , not (isInsolubleStatus status)
216 = return () -- For Template Haskell brackets report only
217 -- definite errors. The whole thing will be re-checked
218 -- later when we plug it in, and meanwhile there may
219 -- certainly be un-satisfied constraints
220
221 | otherwise
222 = do { reportWanteds ctxt' wanted
223 ; traceTc "reportImplic" (ppr implic)
224 ; when (cec_warn_redundant ctxt) $
225 warnRedundantConstraints ctxt' tcl_env info' dead_givens }
226 where
227 (env1, tvs') = mapAccumL tidyTyVarBndr (cec_tidy ctxt) tvs
228 (env2, info') = tidySkolemInfo env1 info
229 implic' = implic { ic_skols = tvs'
230 , ic_given = map (tidyEvVar env2) given
231 , ic_info = info' }
232 ctxt' = ctxt { cec_tidy = env2
233 , cec_encl = implic' : cec_encl ctxt
234 , cec_binds = case cec_binds ctxt of
235 Nothing -> Nothing
236 Just {} -> Just evb }
237 dead_givens = case status of
238 IC_Solved { ics_dead = dead } -> dead
239 _ -> []
240
241 warnRedundantConstraints :: ReportErrCtxt -> TcLclEnv -> SkolemInfo -> [EvVar] -> TcM ()
242 warnRedundantConstraints ctxt env info ev_vars
243 | null redundant_evs
244 = return ()
245
246 | SigSkol {} <- info
247 = setLclEnv env $ -- We want to add "In the type signature for f"
248 -- to the error context, which is a bit tiresome
249 addErrCtxt (ptext (sLit "In") <+> ppr info) $
250 do { env <- getLclEnv
251 ; msg <- mkErrorMsg ctxt env doc
252 ; reportWarning msg }
253
254 | otherwise -- But for InstSkol there already *is* a surrounding
255 -- "In the instance declaration for Eq [a]" context
256 -- and we don't want to say it twice. Seems a bit ad-hoc
257 = do { msg <- mkErrorMsg ctxt env doc
258 ; reportWarning msg }
259 where
260 doc = ptext (sLit "Redundant constraint") <> plural redundant_evs <> colon
261 <+> pprEvVarTheta redundant_evs
262
263 redundant_evs = case info of -- See Note [Redundant constraints in instance decls]
264 InstSkol -> filterOut improving ev_vars
265 _ -> ev_vars
266
267 improving ev_var = any isImprovementPred $
268 transSuperClassesPred (idType ev_var)
269
270 {- Note [Redundant constraints in instance decls]
271 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
272 For instance declarations, we don't report unused givens if
273 they can give rise to improvement. Example (Trac #10100):
274 class Add a b ab | a b -> ab, a ab -> b
275 instance Add Zero b b
276 instance Add a b ab => Add (Succ a) b (Succ ab)
277 The context (Add a b ab) for the instance is clearly unused in terms
278 of evidence, since the dictionary has no feilds. But it is still
279 needed! With the context, a wanted constraint
280 Add (Succ Zero) beta (Succ Zero)
281 we will reduce to (Add Zero beta Zero), and thence we get beta := Zero.
282 But without the context we won't find beta := Zero.
283
284 This only matters in instance declarations..
285 -}
286
287 reportWanteds :: ReportErrCtxt -> WantedConstraints -> TcM ()
288 reportWanteds ctxt (WC { wc_simple = simples, wc_insol = insols, wc_impl = implics })
289 = do { ctxt1 <- reportSimples ctxt (mapBag (tidyCt env) insol_given)
290 ; ctxt2 <- reportSimples ctxt1 (mapBag (tidyCt env) insol_wanted)
291
292 -- For the simple wanteds, suppress them if there are any
293 -- insolubles in the tree, to avoid unnecessary clutter
294 ; let ctxt2' = ctxt { cec_suppress = cec_suppress ctxt2
295 || anyBag insolubleImplic implics }
296 ; _ <- reportSimples ctxt2' (mapBag (tidyCt env) simples)
297
298 -- All the Derived ones have been filtered out of simples
299 -- by the constraint solver. This is ok; we don't want
300 -- to report unsolved Derived goals as errors
301 -- See Note [Do not report derived but soluble errors]
302 ; mapBagM_ (reportImplic ctxt1) implics }
303 -- NB ctxt1: don't suppress inner insolubles if there's only a
304 -- wanted insoluble here; but do suppress inner insolubles
305 -- if there's a *given* insoluble here (= inaccessible code)
306 where
307 env = cec_tidy ctxt
308 (insol_given, insol_wanted) = partitionBag isGivenCt insols
309
310 reportSimples :: ReportErrCtxt -> Cts -> TcM ReportErrCtxt
311 reportSimples ctxt simples -- Here 'simples' includes insolble goals
312 = traceTc "reportSimples" (vcat [ ptext (sLit "Simples =") <+> ppr simples
313 , ptext (sLit "Suppress =") <+> ppr (cec_suppress ctxt)])
314 >> tryReporters ctxt
315 [ -- First deal with things that are utterly wrong
316 -- Like Int ~ Bool (incl nullary TyCons)
317 -- or Int ~ t a (AppTy on one side)
318 ("Utterly wrong (given)", utterly_wrong_given, True, mkGroupReporter mkEqErr)
319 , ("Utterly wrong (other)", utterly_wrong_other, True, mkGroupReporter mkEqErr)
320 , ("Holes", is_hole, False, mkHoleReporter)
321
322 -- Report equalities of form (a~ty). They are usually
323 -- skolem-equalities, and they cause confusing knock-on
324 -- effects in other errors; see test T4093b.
325 , ("Skolem equalities", skolem_eq, True, mkSkolReporter)
326
327 -- Other equalities; also confusing knock on effects
328 , ("Equalities", is_equality, True, mkGroupReporter mkEqErr)
329
330 , ("Implicit params", is_ip, False, mkGroupReporter mkIPErr)
331 , ("Irreds", is_irred, False, mkGroupReporter mkIrredErr)
332 , ("Dicts", is_dict, False, mkGroupReporter mkDictErr)
333 ]
334 (bagToList simples)
335 -- TuplePreds should have been expanded away by the constraint
336 -- simplifier, so they shouldn't show up at this point
337 where
338 utterly_wrong_given, utterly_wrong_other, skolem_eq, is_hole, is_dict,
339 is_equality, is_ip, is_irred :: Ct -> PredTree -> Bool
340
341 utterly_wrong_given ct (EqPred _ ty1 ty2)
342 | isGivenCt ct = isRigid ty1 && isRigid ty2
343 utterly_wrong_given _ _ = False
344
345 utterly_wrong_other _ (EqPred _ ty1 ty2) = isRigid ty1 && isRigid ty2
346 utterly_wrong_other _ _ = False
347
348 is_hole ct _ = isHoleCt ct
349
350 skolem_eq _ (EqPred NomEq ty1 ty2) = isRigidOrSkol ty1 && isRigidOrSkol ty2
351 skolem_eq _ _ = False
352
353 is_equality _ (EqPred {}) = True
354 is_equality _ _ = False
355
356 is_dict _ (ClassPred {}) = True
357 is_dict _ _ = False
358
359 is_ip _ (ClassPred cls _) = isIPClass cls
360 is_ip _ _ = False
361
362 is_irred _ (IrredPred {}) = True
363 is_irred _ _ = False
364
365
366 ---------------
367 isRigid, isRigidOrSkol :: Type -> Bool
368 isRigid ty
369 | Just (tc,_) <- tcSplitTyConApp_maybe ty = isDecomposableTyCon tc
370 | Just {} <- tcSplitAppTy_maybe ty = True
371 | isForAllTy ty = True
372 | otherwise = False
373
374 isRigidOrSkol ty
375 | Just tv <- getTyVar_maybe ty = isSkolemTyVar tv
376 | otherwise = isRigid ty
377
378 isTyFun_maybe :: Type -> Maybe TyCon
379 isTyFun_maybe ty = case tcSplitTyConApp_maybe ty of
380 Just (tc,_) | isTypeFamilyTyCon tc -> Just tc
381 _ -> Nothing
382
383
384 --------------------------------------------
385 -- Reporters
386 --------------------------------------------
387
388 type Reporter
389 = ReportErrCtxt -> [Ct] -> TcM ()
390 type ReporterSpec
391 = ( String -- Name
392 , Ct -> PredTree -> Bool -- Pick these ones
393 , Bool -- True <=> suppress subsequent reporters
394 , Reporter) -- The reporter itself
395
396 mkSkolReporter :: Reporter
397 -- Suppress duplicates with the same LHS
398 mkSkolReporter ctxt cts
399 = mapM_ (reportGroup mkEqErr ctxt) (equivClasses cmp_lhs_type cts)
400 where
401 cmp_lhs_type ct1 ct2
402 = case (classifyPredType (ctPred ct1), classifyPredType (ctPred ct2)) of
403 (EqPred eq_rel1 ty1 _, EqPred eq_rel2 ty2 _) ->
404 (eq_rel1 `compare` eq_rel2) `thenCmp` (ty1 `cmpType` ty2)
405 _ -> pprPanic "mkSkolReporter" (ppr ct1 $$ ppr ct2)
406
407 mkHoleReporter :: Reporter
408 -- Reports errors one at a time
409 mkHoleReporter ctxt
410 = mapM_ $ \ct ->
411 do { err <- mkHoleError ctxt ct
412 ; maybeReportHoleError ctxt ct err
413 ; maybeAddDeferredHoleBinding ctxt err ct }
414
415 mkGroupReporter :: (ReportErrCtxt -> [Ct] -> TcM ErrMsg)
416 -- Make error message for a group
417 -> Reporter -- Deal with lots of constraints
418 -- Group together errors from same location,
419 -- and report only the first (to avoid a cascade)
420 mkGroupReporter mk_err ctxt cts
421 = mapM_ (reportGroup mk_err ctxt) (equivClasses cmp_loc cts)
422 where
423 cmp_loc ct1 ct2 = ctLocSpan (ctLoc ct1) `compare` ctLocSpan (ctLoc ct2)
424
425 reportGroup :: (ReportErrCtxt -> [Ct] -> TcM ErrMsg) -> ReportErrCtxt
426 -> [Ct] -> TcM ()
427 reportGroup mk_err ctxt cts
428 = do { err <- mk_err ctxt cts
429 ; maybeReportError ctxt err
430 ; mapM_ (maybeAddDeferredBinding ctxt err) cts }
431 -- Add deferred bindings for all
432 -- But see Note [Always warn with -fdefer-type-errors]
433
434 maybeReportHoleError :: ReportErrCtxt -> Ct -> ErrMsg -> TcM ()
435 maybeReportHoleError ctxt ct err
436 -- When -XPartialTypeSignatures is on, warnings (instead of errors) are
437 -- generated for holes in partial type signatures. Unless
438 -- -fwarn_partial_type_signatures is not on, in which case the messages are
439 -- discarded.
440 | isTypeHoleCt ct
441 = -- For partial type signatures, generate warnings only, and do that
442 -- only if -fwarn_partial_type_signatures is on
443 case cec_type_holes ctxt of
444 HoleError -> reportError err
445 HoleWarn -> reportWarning err
446 HoleDefer -> return ()
447
448 -- Otherwise this is a typed hole in an expression
449 | otherwise
450 = -- If deferring, report a warning only if -fwarn-typed-holds is on
451 case cec_expr_holes ctxt of
452 HoleError -> reportError err
453 HoleWarn -> reportWarning err
454 HoleDefer -> return ()
455
456 maybeReportError :: ReportErrCtxt -> ErrMsg -> TcM ()
457 -- Report the error and/or make a deferred binding for it
458 maybeReportError ctxt err
459 -- See Note [Always warn with -fdefer-type-errors]
460 | cec_defer_type_errors ctxt
461 = reportWarning err
462 | cec_suppress ctxt
463 = return ()
464 | otherwise
465 = reportError err
466
467 addDeferredBinding :: ReportErrCtxt -> ErrMsg -> Ct -> TcM ()
468 -- See Note [Deferring coercion errors to runtime]
469 addDeferredBinding ctxt err ct
470 | CtWanted { ctev_pred = pred, ctev_evar = ev_id } <- ctEvidence ct
471 -- Only add deferred bindings for Wanted constraints
472 , Just ev_binds_var <- cec_binds ctxt -- We have somewhere to put the bindings
473 = do { dflags <- getDynFlags
474 ; let err_msg = pprLocErrMsg err
475 err_fs = mkFastString $ showSDoc dflags $
476 err_msg $$ text "(deferred type error)"
477
478 -- Create the binding
479 ; addTcEvBind ev_binds_var (mkWantedEvBind ev_id (EvDelayedError pred err_fs)) }
480
481 | otherwise -- Do not set any evidence for Given/Derived
482 = return ()
483
484 maybeAddDeferredHoleBinding :: ReportErrCtxt -> ErrMsg -> Ct -> TcM ()
485 maybeAddDeferredHoleBinding ctxt err ct
486 | isExprHoleCt ct
487 , case cec_expr_holes ctxt of
488 HoleDefer -> True
489 HoleWarn -> True
490 HoleError -> False
491 = addDeferredBinding ctxt err ct -- Only add bindings for holes in expressions
492 | otherwise -- not for holes in partial type signatures
493 = return ()
494
495 maybeAddDeferredBinding :: ReportErrCtxt -> ErrMsg -> Ct -> TcM ()
496 maybeAddDeferredBinding ctxt err ct
497 | cec_defer_type_errors ctxt
498 = addDeferredBinding ctxt err ct
499 | otherwise
500 = return ()
501
502 tryReporters :: ReportErrCtxt -> [ReporterSpec] -> [Ct] -> TcM ReportErrCtxt
503 -- Use the first reporter in the list whose predicate says True
504 tryReporters ctxt reporters cts
505 = do { traceTc "tryReporters {" (ppr cts)
506 ; ctxt' <- go ctxt reporters cts
507 ; traceTc "tryReporters }" empty
508 ; return ctxt' }
509 where
510 go ctxt [] cts
511 | null cts = return ctxt
512 | otherwise = pprPanic "tryReporters" (ppr cts)
513
514 go ctxt ((str, pred, suppress_after, reporter) : rs) cts
515 | null yeses = do { traceTc "tryReporters: no" (text str)
516 ; go ctxt rs cts }
517 | otherwise = do { traceTc "tryReporters: yes" (text str <+> ppr yeses)
518 ; reporter ctxt yeses :: TcM ()
519 ; let ctxt' = ctxt { cec_suppress = suppress_after || cec_suppress ctxt }
520 ; go ctxt' rs nos }
521 -- Carry on with the rest, because we must make
522 -- deferred bindings for them if we have
523 -- -fdefer-type-errors
524 -- But suppress their error messages
525 where
526 (yeses, nos) = partition keep_me cts
527 keep_me ct = pred ct (classifyPredType (ctPred ct))
528
529 -- Add the "arising from..." part to a message about bunch of dicts
530 addArising :: CtOrigin -> SDoc -> SDoc
531 addArising orig msg = hang msg 2 (pprArising orig)
532
533 pprWithArising :: [Ct] -> (CtLoc, SDoc)
534 -- Print something like
535 -- (Eq a) arising from a use of x at y
536 -- (Show a) arising from a use of p at q
537 -- Also return a location for the error message
538 -- Works for Wanted/Derived only
539 pprWithArising []
540 = panic "pprWithArising"
541 pprWithArising (ct:cts)
542 | null cts
543 = (loc, addArising (ctLocOrigin loc)
544 (pprTheta [ctPred ct]))
545 | otherwise
546 = (loc, vcat (map ppr_one (ct:cts)))
547 where
548 loc = ctLoc ct
549 ppr_one ct' = hang (parens (pprType (ctPred ct')))
550 2 (pprArisingAt (ctLoc ct'))
551
552 mkErrorMsgFromCt :: ReportErrCtxt -> Ct -> SDoc -> TcM ErrMsg
553 mkErrorMsgFromCt ctxt ct msg
554 = mkErrorMsg ctxt (ctLocEnv (ctLoc ct)) msg
555
556 mkErrorMsg :: ReportErrCtxt -> TcLclEnv -> SDoc -> TcM ErrMsg
557 mkErrorMsg ctxt tcl_env msg
558 = do { err_info <- mkErrInfo (cec_tidy ctxt) (tcl_ctxt tcl_env)
559 ; mkLongErrAt (RealSrcSpan (tcl_loc tcl_env)) msg err_info }
560
561 type UserGiven = ([EvVar], SkolemInfo, Bool, RealSrcSpan)
562
563 getUserGivens :: ReportErrCtxt -> [UserGiven]
564 -- One item for each enclosing implication
565 getUserGivens (CEC {cec_encl = ctxt})
566 = reverse $
567 [ (givens, info, no_eqs, tcl_loc env)
568 | Implic { ic_given = givens, ic_env = env
569 , ic_no_eqs = no_eqs, ic_info = info } <- ctxt
570 , not (null givens) ]
571
572 {-
573 Note [Always warn with -fdefer-type-errors]
574 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
575 When -fdefer-type-errors is on we warn about *all* type errors, even
576 if cec_suppress is on. This can lead to a lot more warnings than you
577 would get errors without -fdefer-type-errors, but if we suppress any of
578 them you might get a runtime error that wasn't warned about at compile
579 time.
580
581 This is an easy design choice to change; just flip the order of the
582 first two equations for maybeReportError
583
584 To be consistent, we should also report multiple warnings from a single
585 location in mkGroupReporter, when -fdefer-type-errors is on. But that
586 is perhaps a bit *over*-consistent! Again, an easy choice to change.
587
588
589 Note [Do not report derived but soluble errors]
590 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
591 The wc_simples include Derived constraints that have not been solved, but are
592 not insoluble (in that case they'd be in wc_insols). We do not want to report
593 these as errors:
594
595 * Superclass constraints. If we have an unsolved [W] Ord a, we'll also have
596 an unsolved [D] Eq a, and we do not want to report that; it's just noise.
597
598 * Functional dependencies. For givens, consider
599 class C a b | a -> b
600 data T a where
601 MkT :: C a d => [d] -> T a
602 f :: C a b => T a -> F Int
603 f (MkT xs) = length xs
604 Then we get a [D] b~d. But there *is* a legitimate call to
605 f, namely f (MkT [True]) :: T Bool, in which b=d. So we should
606 not reject the program.
607
608 For wanteds, something similar
609 data T a where
610 MkT :: C Int b => a -> b -> T a
611 g :: C Int c => c -> ()
612 f :: T a -> ()
613 f (MkT x y) = g x
614 Here we get [G] C Int b, [W] C Int a, hence [D] a~b.
615 But again f (MkT True True) is a legitimate call.
616
617 (We leave the Deriveds in wc_simple until reportErrors, so that we don't lose
618 derived superclasses between iterations of the solver.)
619
620 For functional dependencies, here is a real example,
621 stripped off from libraries/utf8-string/Codec/Binary/UTF8/Generic.hs
622
623 class C a b | a -> b
624 g :: C a b => a -> b -> ()
625 f :: C a b => a -> b -> ()
626 f xa xb =
627 let loop = g xa
628 in loop xb
629
630 We will first try to infer a type for loop, and we will succeed:
631 C a b' => b' -> ()
632 Subsequently, we will type check (loop xb) and all is good. But,
633 recall that we have to solve a final implication constraint:
634 C a b => (C a b' => .... cts from body of loop .... ))
635 And now we have a problem as we will generate an equality b ~ b' and fail to
636 solve it.
637
638
639 ************************************************************************
640 * *
641 Irreducible predicate errors
642 * *
643 ************************************************************************
644 -}
645
646 mkIrredErr :: ReportErrCtxt -> [Ct] -> TcM ErrMsg
647 mkIrredErr ctxt cts
648 = do { (ctxt, binds_msg, _) <- relevantBindings True ctxt ct1
649 ; mkErrorMsgFromCt ctxt ct1 (msg $$ binds_msg) }
650 where
651 (ct1:_) = cts
652 orig = ctLocOrigin (ctLoc ct1)
653 givens = getUserGivens ctxt
654 msg = couldNotDeduce givens (map ctPred cts, orig)
655
656 ----------------
657 mkHoleError :: ReportErrCtxt -> Ct -> TcM ErrMsg
658 mkHoleError ctxt ct@(CHoleCan { cc_occ = occ, cc_hole = hole_sort })
659 = do { let tyvars = varSetElems (tyVarsOfCt ct)
660 tyvars_msg = map loc_msg tyvars
661 msg = vcat [ hang (ptext (sLit "Found hole") <+> quotes (ppr occ))
662 2 (ptext (sLit "with type:") <+> pprType (ctEvPred (ctEvidence ct)))
663 , ppUnless (null tyvars) (ptext (sLit "Where:") <+> vcat tyvars_msg)
664 , hint ]
665 ; (ctxt, binds_doc, _) <- relevantBindings False ctxt ct
666 -- The 'False' means "don't filter the bindings"; see Trac #8191
667 ; mkErrorMsgFromCt ctxt ct (msg $$ binds_doc) }
668 where
669 hint
670 | TypeHole <- hole_sort
671 , HoleError <- cec_type_holes ctxt
672 = ptext (sLit "To use the inferred type, enable PartialTypeSignatures")
673
674 | ExprHole <- hole_sort -- Give hint for, say, f x = _x
675 , lengthFS (occNameFS occ) > 1 -- Don't give this hint for plain "_", which isn't legal Haskell
676 = ptext (sLit "Or perhaps") <+> quotes (ppr occ)
677 <+> ptext (sLit "is mis-spelled, or not in scope")
678
679 | otherwise
680 = empty
681
682 loc_msg tv
683 = case tcTyVarDetails tv of
684 SkolemTv {} -> quotes (ppr tv) <+> skol_msg
685 MetaTv {} -> quotes (ppr tv) <+> ptext (sLit "is an ambiguous type variable")
686 det -> pprTcTyVarDetails det
687 where
688 skol_msg = pprSkol (getSkolemInfo (cec_encl ctxt) tv) (getSrcLoc tv)
689
690 mkHoleError _ ct = pprPanic "mkHoleError" (ppr ct)
691
692 ----------------
693 mkIPErr :: ReportErrCtxt -> [Ct] -> TcM ErrMsg
694 mkIPErr ctxt cts
695 = do { (ctxt, bind_msg, _) <- relevantBindings True ctxt ct1
696 ; mkErrorMsgFromCt ctxt ct1 (msg $$ bind_msg) }
697 where
698 (ct1:_) = cts
699 orig = ctLocOrigin (ctLoc ct1)
700 preds = map ctPred cts
701 givens = getUserGivens ctxt
702 msg | null givens
703 = addArising orig $
704 sep [ ptext (sLit "Unbound implicit parameter") <> plural cts
705 , nest 2 (pprTheta preds) ]
706 | otherwise
707 = couldNotDeduce givens (preds, orig)
708
709 {-
710 ************************************************************************
711 * *
712 Equality errors
713 * *
714 ************************************************************************
715
716 Note [Inaccessible code]
717 ~~~~~~~~~~~~~~~~~~~~~~~~
718 Consider
719 data T a where
720 T1 :: T a
721 T2 :: T Bool
722
723 f :: (a ~ Int) => T a -> Int
724 f T1 = 3
725 f T2 = 4 -- Unreachable code
726
727 Here the second equation is unreachable. The original constraint
728 (a~Int) from the signature gets rewritten by the pattern-match to
729 (Bool~Int), so the danger is that we report the error as coming from
730 the *signature* (Trac #7293). So, for Given errors we replace the
731 env (and hence src-loc) on its CtLoc with that from the immediately
732 enclosing implication.
733 -}
734
735 mkEqErr :: ReportErrCtxt -> [Ct] -> TcM ErrMsg
736 -- Don't have multiple equality errors from the same location
737 -- E.g. (Int,Bool) ~ (Bool,Int) one error will do!
738 mkEqErr ctxt (ct:_) = mkEqErr1 ctxt ct
739 mkEqErr _ [] = panic "mkEqErr"
740
741 mkEqErr1 :: ReportErrCtxt -> Ct -> TcM ErrMsg
742 -- Wanted constraints only!
743 mkEqErr1 ctxt ct
744 | isGiven ev
745 = do { (ctxt, binds_msg, _) <- relevantBindings True ctxt ct
746 ; let (given_loc, given_msg) = mk_given (cec_encl ctxt)
747 ; dflags <- getDynFlags
748 ; mkEqErr_help dflags ctxt (given_msg $$ binds_msg)
749 (ct { cc_ev = ev {ctev_loc = given_loc}}) -- Note [Inaccessible code]
750 Nothing ty1 ty2 }
751
752 | otherwise -- Wanted or derived
753 = do { (ctxt, binds_msg, tidy_orig) <- relevantBindings True ctxt ct
754 ; rdr_env <- getGlobalRdrEnv
755 ; fam_envs <- tcGetFamInstEnvs
756 ; let (is_oriented, wanted_msg) = mk_wanted_extra tidy_orig
757 coercible_msg = case ctEvEqRel ev of
758 NomEq -> empty
759 ReprEq -> mkCoercibleExplanation rdr_env fam_envs ty1 ty2
760 ; dflags <- getDynFlags
761 ; traceTc "mkEqErr1" (ppr ct $$ pprCtOrigin (ctLocOrigin loc) $$ pprCtOrigin tidy_orig)
762 ; mkEqErr_help dflags ctxt (wanted_msg $$ coercible_msg $$ binds_msg)
763 ct is_oriented ty1 ty2 }
764 where
765 ev = ctEvidence ct
766 loc = ctEvLoc ev
767 (ty1, ty2) = getEqPredTys (ctEvPred ev)
768
769 mk_given :: [Implication] -> (CtLoc, SDoc)
770 -- For given constraints we overwrite the env (and hence src-loc)
771 -- with one from the implication. See Note [Inaccessible code]
772 mk_given [] = (loc, empty)
773 mk_given (implic : _) = (setCtLocEnv loc (ic_env implic)
774 , hang (ptext (sLit "Inaccessible code in"))
775 2 (ppr (ic_info implic)))
776
777 -- If the types in the error message are the same as the types
778 -- we are unifying, don't add the extra expected/actual message
779 mk_wanted_extra orig@(TypeEqOrigin {})
780 = mkExpectedActualMsg ty1 ty2 orig
781
782 mk_wanted_extra (KindEqOrigin cty1 cty2 sub_o)
783 = (Nothing, msg1 $$ msg2)
784 where
785 msg1 = hang (ptext (sLit "When matching types"))
786 2 (vcat [ ppr cty1 <+> dcolon <+> ppr (typeKind cty1)
787 , ppr cty2 <+> dcolon <+> ppr (typeKind cty2) ])
788 msg2 = case sub_o of
789 TypeEqOrigin {} -> snd (mkExpectedActualMsg cty1 cty2 sub_o)
790 _ -> empty
791
792 mk_wanted_extra orig@(FunDepOrigin1 {}) = (Nothing, pprArising orig)
793 mk_wanted_extra orig@(FunDepOrigin2 {}) = (Nothing, pprArising orig)
794 mk_wanted_extra orig@(DerivOriginCoerce _ oty1 oty2)
795 = (Nothing, pprArising orig $+$ mkRoleSigs oty1 oty2)
796 mk_wanted_extra orig@(CoercibleOrigin oty1 oty2)
797 -- if the origin types are the same as the final types, don't
798 -- clutter output with repetitive information
799 | not (oty1 `eqType` ty1 && oty2 `eqType` ty2) &&
800 not (oty1 `eqType` ty2 && oty2 `eqType` ty1)
801 = (Nothing, pprArising orig $+$ mkRoleSigs oty1 oty2)
802 | otherwise
803 -- still print role sigs even if types line up
804 = (Nothing, mkRoleSigs oty1 oty2)
805 mk_wanted_extra _ = (Nothing, empty)
806
807 -- | This function tries to reconstruct why a "Coercible ty1 ty2" constraint
808 -- is left over.
809 mkCoercibleExplanation :: GlobalRdrEnv -> FamInstEnvs
810 -> TcType -> TcType -> SDoc
811 mkCoercibleExplanation rdr_env fam_envs ty1 ty2
812 | Just (tc, tys) <- tcSplitTyConApp_maybe ty1
813 , (rep_tc, _, _) <- tcLookupDataFamInst fam_envs tc tys
814 , Just msg <- coercible_msg_for_tycon rep_tc
815 = msg
816 | Just (tc, tys) <- splitTyConApp_maybe ty2
817 , (rep_tc, _, _) <- tcLookupDataFamInst fam_envs tc tys
818 , Just msg <- coercible_msg_for_tycon rep_tc
819 = msg
820 | Just (s1, _) <- tcSplitAppTy_maybe ty1
821 , Just (s2, _) <- tcSplitAppTy_maybe ty2
822 , s1 `eqType` s2
823 , has_unknown_roles s1
824 = hang (text "NB: We cannot know what roles the parameters to" <+>
825 quotes (ppr s1) <+> text "have;")
826 2 (text "we must assume that the role is nominal")
827 | otherwise
828 = empty
829 where
830 coercible_msg_for_tycon tc
831 | isAbstractTyCon tc
832 = Just $ hsep [ text "NB: The type constructor"
833 , quotes (pprSourceTyCon tc)
834 , text "is abstract" ]
835 | isNewTyCon tc
836 , [data_con] <- tyConDataCons tc
837 , let dc_name = dataConName data_con
838 , null (lookupGRE_Name rdr_env dc_name)
839 = Just $ hang (text "The data constructor" <+> quotes (ppr dc_name))
840 2 (sep [ text "of newtype" <+> quotes (pprSourceTyCon tc)
841 , text "is not in scope" ])
842 | otherwise = Nothing
843
844 has_unknown_roles ty
845 | Just (tc, tys) <- tcSplitTyConApp_maybe ty
846 = length tys >= tyConArity tc -- oversaturated tycon
847 | Just (s, _) <- tcSplitAppTy_maybe ty
848 = has_unknown_roles s
849 | isTyVarTy ty
850 = True
851 | otherwise
852 = False
853
854 -- | Make a listing of role signatures for all the parameterised tycons
855 -- used in the provided types
856 mkRoleSigs :: Type -> Type -> SDoc
857 mkRoleSigs ty1 ty2
858 = ppUnless (null role_sigs) $
859 hang (text "Relevant role signatures:")
860 2 (vcat role_sigs)
861 where
862 tcs = nameEnvElts $ tyConsOfType ty1 `plusNameEnv` tyConsOfType ty2
863 role_sigs = mapMaybe ppr_role_sig tcs
864
865 ppr_role_sig tc
866 | null roles -- if there are no parameters, don't bother printing
867 = Nothing
868 | otherwise
869 = Just $ hsep $ [text "type role", ppr tc] ++ map ppr roles
870 where
871 roles = tyConRoles tc
872
873 mkEqErr_help :: DynFlags -> ReportErrCtxt -> SDoc
874 -> Ct
875 -> Maybe SwapFlag -- Nothing <=> not sure
876 -> TcType -> TcType -> TcM ErrMsg
877 mkEqErr_help dflags ctxt extra ct oriented ty1 ty2
878 | Just tv1 <- tcGetTyVar_maybe ty1 = mkTyVarEqErr dflags ctxt extra ct oriented tv1 ty2
879 | Just tv2 <- tcGetTyVar_maybe ty2 = mkTyVarEqErr dflags ctxt extra ct swapped tv2 ty1
880 | otherwise = reportEqErr ctxt extra ct oriented ty1 ty2
881 where
882 swapped = fmap flipSwap oriented
883
884 reportEqErr :: ReportErrCtxt -> SDoc
885 -> Ct
886 -> Maybe SwapFlag -- Nothing <=> not sure
887 -> TcType -> TcType -> TcM ErrMsg
888 reportEqErr ctxt extra1 ct oriented ty1 ty2
889 = do { let extra2 = mkEqInfoMsg ct ty1 ty2
890 ; mkErrorMsgFromCt ctxt ct (vcat [ misMatchOrCND ctxt ct oriented ty1 ty2
891 , extra2, extra1]) }
892
893 mkTyVarEqErr :: DynFlags -> ReportErrCtxt -> SDoc -> Ct
894 -> Maybe SwapFlag -> TcTyVar -> TcType -> TcM ErrMsg
895 -- tv1 and ty2 are already tidied
896 mkTyVarEqErr dflags ctxt extra ct oriented tv1 ty2
897 | isUserSkolem ctxt tv1 -- ty2 won't be a meta-tyvar, or else the thing would
898 -- be oriented the other way round;
899 -- see TcCanonical.canEqTyVarTyVar
900 || isSigTyVar tv1 && not (isTyVarTy ty2)
901 = mkErrorMsgFromCt ctxt ct (vcat [ misMatchOrCND ctxt ct oriented ty1 ty2
902 , extraTyVarInfo ctxt tv1 ty2
903 , extra ])
904
905 -- So tv is a meta tyvar (or started that way before we
906 -- generalised it). So presumably it is an *untouchable*
907 -- meta tyvar or a SigTv, else it'd have been unified
908 | not (k2 `tcIsSubKind` k1) -- Kind error
909 = mkErrorMsgFromCt ctxt ct $ (kindErrorMsg (mkTyVarTy tv1) ty2 $$ extra)
910
911 | OC_Occurs <- occ_check_expand
912 , NomEq <- ctEqRel ct -- reporting occurs check for Coercible is strange
913 = do { let occCheckMsg = hang (text "Occurs check: cannot construct the infinite type:")
914 2 (sep [ppr ty1, char '~', ppr ty2])
915 extra2 = mkEqInfoMsg ct ty1 ty2
916 ; mkErrorMsgFromCt ctxt ct (occCheckMsg $$ extra2 $$ extra) }
917
918 | OC_Forall <- occ_check_expand
919 = do { let msg = vcat [ ptext (sLit "Cannot instantiate unification variable")
920 <+> quotes (ppr tv1)
921 , hang (ptext (sLit "with a type involving foralls:")) 2 (ppr ty2)
922 , nest 2 (ptext (sLit "GHC doesn't yet support impredicative polymorphism")) ]
923 ; mkErrorMsgFromCt ctxt ct msg }
924
925 -- If the immediately-enclosing implication has 'tv' a skolem, and
926 -- we know by now its an InferSkol kind of skolem, then presumably
927 -- it started life as a SigTv, else it'd have been unified, given
928 -- that there's no occurs-check or forall problem
929 | (implic:_) <- cec_encl ctxt
930 , Implic { ic_skols = skols } <- implic
931 , tv1 `elem` skols
932 = mkErrorMsgFromCt ctxt ct (vcat [ misMatchMsg oriented eq_rel ty1 ty2
933 , extraTyVarInfo ctxt tv1 ty2
934 , extra ])
935
936 -- Check for skolem escape
937 | (implic:_) <- cec_encl ctxt -- Get the innermost context
938 , Implic { ic_env = env, ic_skols = skols, ic_info = skol_info } <- implic
939 , let esc_skols = filter (`elemVarSet` (tyVarsOfType ty2)) skols
940 , not (null esc_skols)
941 = do { let msg = misMatchMsg oriented eq_rel ty1 ty2
942 esc_doc = sep [ ptext (sLit "because type variable") <> plural esc_skols
943 <+> pprQuotedList esc_skols
944 , ptext (sLit "would escape") <+>
945 if isSingleton esc_skols then ptext (sLit "its scope")
946 else ptext (sLit "their scope") ]
947 tv_extra = vcat [ nest 2 $ esc_doc
948 , sep [ (if isSingleton esc_skols
949 then ptext (sLit "This (rigid, skolem) type variable is")
950 else ptext (sLit "These (rigid, skolem) type variables are"))
951 <+> ptext (sLit "bound by")
952 , nest 2 $ ppr skol_info
953 , nest 2 $ ptext (sLit "at") <+> ppr (tcl_loc env) ] ]
954 ; mkErrorMsgFromCt ctxt ct (msg $$ tv_extra $$ extra) }
955
956 -- Nastiest case: attempt to unify an untouchable variable
957 | (implic:_) <- cec_encl ctxt -- Get the innermost context
958 , Implic { ic_env = env, ic_given = given, ic_info = skol_info } <- implic
959 = do { let msg = misMatchMsg oriented eq_rel ty1 ty2
960 tclvl_extra
961 = nest 2 $
962 sep [ quotes (ppr tv1) <+> ptext (sLit "is untouchable")
963 , nest 2 $ ptext (sLit "inside the constraints:") <+> pprEvVarTheta given
964 , nest 2 $ ptext (sLit "bound by") <+> ppr skol_info
965 , nest 2 $ ptext (sLit "at") <+> ppr (tcl_loc env) ]
966 tv_extra = extraTyVarInfo ctxt tv1 ty2
967 add_sig = suggestAddSig ctxt ty1 ty2
968 ; mkErrorMsgFromCt ctxt ct (vcat [msg, tclvl_extra, tv_extra, add_sig, extra]) }
969
970 | otherwise
971 = reportEqErr ctxt extra ct oriented (mkTyVarTy tv1) ty2
972 -- This *can* happen (Trac #6123, and test T2627b)
973 -- Consider an ambiguous top-level constraint (a ~ F a)
974 -- Not an occurs check, because F is a type function.
975 where
976 occ_check_expand = occurCheckExpand dflags tv1 ty2
977 k1 = tyVarKind tv1
978 k2 = typeKind ty2
979 ty1 = mkTyVarTy tv1
980 eq_rel = ctEqRel ct
981
982 mkEqInfoMsg :: Ct -> TcType -> TcType -> SDoc
983 -- Report (a) ambiguity if either side is a type function application
984 -- e.g. F a0 ~ Int
985 -- (b) warning about injectivity if both sides are the same
986 -- type function application F a ~ F b
987 -- See Note [Non-injective type functions]
988 mkEqInfoMsg ct ty1 ty2
989 = tyfun_msg $$ ambig_msg
990 where
991 mb_fun1 = isTyFun_maybe ty1
992 mb_fun2 = isTyFun_maybe ty2
993
994 ambig_msg | isJust mb_fun1 || isJust mb_fun2
995 = snd (mkAmbigMsg ct)
996 | otherwise = empty
997
998 tyfun_msg | Just tc1 <- mb_fun1
999 , Just tc2 <- mb_fun2
1000 , tc1 == tc2
1001 = ptext (sLit "NB:") <+> quotes (ppr tc1)
1002 <+> ptext (sLit "is a type function, and may not be injective")
1003 | otherwise = empty
1004
1005 isUserSkolem :: ReportErrCtxt -> TcTyVar -> Bool
1006 -- See Note [Reporting occurs-check errors]
1007 isUserSkolem ctxt tv
1008 = isSkolemTyVar tv && any is_user_skol_tv (cec_encl ctxt)
1009 where
1010 is_user_skol_tv (Implic { ic_skols = sks, ic_info = skol_info })
1011 = tv `elem` sks && is_user_skol_info skol_info
1012
1013 is_user_skol_info (InferSkol {}) = False
1014 is_user_skol_info _ = True
1015
1016 misMatchOrCND :: ReportErrCtxt -> Ct -> Maybe SwapFlag -> TcType -> TcType -> SDoc
1017 -- If oriented then ty1 is actual, ty2 is expected
1018 misMatchOrCND ctxt ct oriented ty1 ty2
1019 | null givens ||
1020 (isRigid ty1 && isRigid ty2) ||
1021 isGivenCt ct
1022 -- If the equality is unconditionally insoluble
1023 -- or there is no context, don't report the context
1024 = misMatchMsg oriented (ctEqRel ct) ty1 ty2
1025 | otherwise
1026 = couldNotDeduce givens ([mkTcEqPred ty1 ty2], orig)
1027 where
1028 givens = [ given | given@(_, _, no_eqs, _) <- getUserGivens ctxt, not no_eqs]
1029 -- Keep only UserGivens that have some equalities
1030 orig = TypeEqOrigin { uo_actual = ty1, uo_expected = ty2 }
1031
1032 couldNotDeduce :: [UserGiven] -> (ThetaType, CtOrigin) -> SDoc
1033 couldNotDeduce givens (wanteds, orig)
1034 = vcat [ addArising orig (ptext (sLit "Could not deduce:") <+> pprTheta wanteds)
1035 , vcat (pp_givens givens)]
1036
1037 pp_givens :: [UserGiven] -> [SDoc]
1038 pp_givens givens
1039 = case givens of
1040 [] -> []
1041 (g:gs) -> ppr_given (ptext (sLit "from the context:")) g
1042 : map (ppr_given (ptext (sLit "or from:"))) gs
1043 where
1044 ppr_given herald (gs, skol_info, _, loc)
1045 = hang (herald <+> pprEvVarTheta gs)
1046 2 (sep [ ptext (sLit "bound by") <+> ppr skol_info
1047 , ptext (sLit "at") <+> ppr loc])
1048
1049 extraTyVarInfo :: ReportErrCtxt -> TcTyVar -> TcType -> SDoc
1050 -- Add on extra info about skolem constants
1051 -- NB: The types themselves are already tidied
1052 extraTyVarInfo ctxt tv1 ty2
1053 = nest 2 (tv_extra tv1 $$ ty_extra ty2)
1054 where
1055 implics = cec_encl ctxt
1056 ty_extra ty = case tcGetTyVar_maybe ty of
1057 Just tv -> tv_extra tv
1058 Nothing -> empty
1059
1060 tv_extra tv | isTcTyVar tv, isSkolemTyVar tv
1061 , let pp_tv = quotes (ppr tv)
1062 = case tcTyVarDetails tv of
1063 SkolemTv {} -> pp_tv <+> pprSkol (getSkolemInfo implics tv) (getSrcLoc tv)
1064 FlatSkol {} -> pp_tv <+> ptext (sLit "is a flattening type variable")
1065 RuntimeUnk {} -> pp_tv <+> ptext (sLit "is an interactive-debugger skolem")
1066 MetaTv {} -> empty
1067
1068 | otherwise -- Normal case
1069 = empty
1070
1071 suggestAddSig :: ReportErrCtxt -> TcType -> TcType -> SDoc
1072 -- See Note [Suggest adding a type signature]
1073 suggestAddSig ctxt ty1 ty2
1074 | null inferred_bndrs
1075 = empty
1076 | [bndr] <- inferred_bndrs
1077 = ptext (sLit "Possible fix: add a type signature for") <+> quotes (ppr bndr)
1078 | otherwise
1079 = ptext (sLit "Possible fix: add type signatures for some or all of") <+> (ppr inferred_bndrs)
1080 where
1081 inferred_bndrs = nub (get_inf ty1 ++ get_inf ty2)
1082 get_inf ty | Just tv <- tcGetTyVar_maybe ty
1083 , isTcTyVar tv, isSkolemTyVar tv
1084 , InferSkol prs <- getSkolemInfo (cec_encl ctxt) tv
1085 = map fst prs
1086 | otherwise
1087 = []
1088
1089 kindErrorMsg :: TcType -> TcType -> SDoc -- Types are already tidy
1090 kindErrorMsg ty1 ty2
1091 = vcat [ ptext (sLit "Kind incompatibility when matching types:")
1092 , nest 2 (vcat [ ppr ty1 <+> dcolon <+> ppr k1
1093 , ppr ty2 <+> dcolon <+> ppr k2 ]) ]
1094 where
1095 k1 = typeKind ty1
1096 k2 = typeKind ty2
1097
1098 --------------------
1099 misMatchMsg :: Maybe SwapFlag -> EqRel -> TcType -> TcType -> SDoc
1100 -- Types are already tidy
1101 -- If oriented then ty1 is actual, ty2 is expected
1102 misMatchMsg oriented eq_rel ty1 ty2
1103 | Just IsSwapped <- oriented
1104 = misMatchMsg (Just NotSwapped) eq_rel ty2 ty1
1105 | Just NotSwapped <- oriented
1106 = sep [ text "Couldn't match" <+> repr1 <+> text "expected" <+>
1107 what <+> quotes (ppr ty2)
1108 , nest (12 + extra_space) $
1109 text "with" <+> repr2 <+> text "actual" <+> what <+> quotes (ppr ty1)
1110 , sameOccExtra ty2 ty1 ]
1111 | otherwise
1112 = sep [ text "Couldn't match" <+> repr1 <+> what <+> quotes (ppr ty1)
1113 , nest (15 + extra_space) $
1114 text "with" <+> repr2 <+> quotes (ppr ty2)
1115 , sameOccExtra ty1 ty2 ]
1116 where
1117 what | isKind ty1 = ptext (sLit "kind")
1118 | otherwise = ptext (sLit "type")
1119
1120 (repr1, repr2, extra_space) = case eq_rel of
1121 NomEq -> (empty, empty, 0)
1122 ReprEq -> (text "representation of", text "that of", 10)
1123
1124 mkExpectedActualMsg :: Type -> Type -> CtOrigin -> (Maybe SwapFlag, SDoc)
1125 -- NotSwapped means (actual, expected), IsSwapped is the reverse
1126 mkExpectedActualMsg ty1 ty2 (TypeEqOrigin { uo_actual = act, uo_expected = exp })
1127 | act `pickyEqType` ty1, exp `pickyEqType` ty2 = (Just NotSwapped, empty)
1128 | exp `pickyEqType` ty1, act `pickyEqType` ty2 = (Just IsSwapped, empty)
1129 | otherwise = (Nothing, msg)
1130 where
1131 msg = vcat [ text "Expected type:" <+> ppr exp
1132 , text " Actual type:" <+> ppr act ]
1133
1134 mkExpectedActualMsg _ _ _ = panic "mkExprectedAcutalMsg"
1135
1136 sameOccExtra :: TcType -> TcType -> SDoc
1137 -- See Note [Disambiguating (X ~ X) errors]
1138 sameOccExtra ty1 ty2
1139 | Just (tc1, _) <- tcSplitTyConApp_maybe ty1
1140 , Just (tc2, _) <- tcSplitTyConApp_maybe ty2
1141 , let n1 = tyConName tc1
1142 n2 = tyConName tc2
1143 same_occ = nameOccName n1 == nameOccName n2
1144 same_pkg = modulePackageKey (nameModule n1) == modulePackageKey (nameModule n2)
1145 , n1 /= n2 -- Different Names
1146 , same_occ -- but same OccName
1147 = ptext (sLit "NB:") <+> (ppr_from same_pkg n1 $$ ppr_from same_pkg n2)
1148 | otherwise
1149 = empty
1150 where
1151 ppr_from same_pkg nm
1152 | isGoodSrcSpan loc
1153 = hang (quotes (ppr nm) <+> ptext (sLit "is defined at"))
1154 2 (ppr loc)
1155 | otherwise -- Imported things have an UnhelpfulSrcSpan
1156 = hang (quotes (ppr nm))
1157 2 (sep [ ptext (sLit "is defined in") <+> quotes (ppr (moduleName mod))
1158 , ppUnless (same_pkg || pkg == mainPackageKey) $
1159 nest 4 $ ptext (sLit "in package") <+> quotes (ppr pkg) ])
1160 where
1161 pkg = modulePackageKey mod
1162 mod = nameModule nm
1163 loc = nameSrcSpan nm
1164
1165 {-
1166 Note [Suggest adding a type signature]
1167 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1168 The OutsideIn algorithm rejects GADT programs that don't have a principal
1169 type, and indeed some that do. Example:
1170 data T a where
1171 MkT :: Int -> T Int
1172
1173 f (MkT n) = n
1174
1175 Does this have type f :: T a -> a, or f :: T a -> Int?
1176 The error that shows up tends to be an attempt to unify an
1177 untouchable type variable. So suggestAddSig sees if the offending
1178 type variable is bound by an *inferred* signature, and suggests
1179 adding a declared signature instead.
1180
1181 This initially came up in Trac #8968, concerning pattern synonyms.
1182
1183 Note [Disambiguating (X ~ X) errors]
1184 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1185 See Trac #8278
1186
1187 Note [Reporting occurs-check errors]
1188 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1189 Given (a ~ [a]), if 'a' is a rigid type variable bound by a user-supplied
1190 type signature, then the best thing is to report that we can't unify
1191 a with [a], because a is a skolem variable. That avoids the confusing
1192 "occur-check" error message.
1193
1194 But nowadays when inferring the type of a function with no type signature,
1195 even if there are errors inside, we still generalise its signature and
1196 carry on. For example
1197 f x = x:x
1198 Here we will infer somethiing like
1199 f :: forall a. a -> [a]
1200 with a suspended error of (a ~ [a]). So 'a' is now a skolem, but not
1201 one bound by the programmer! Here we really should report an occurs check.
1202
1203 So isUserSkolem distinguishes the two.
1204
1205 Note [Non-injective type functions]
1206 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1207 It's very confusing to get a message like
1208 Couldn't match expected type `Depend s'
1209 against inferred type `Depend s1'
1210 so mkTyFunInfoMsg adds:
1211 NB: `Depend' is type function, and hence may not be injective
1212
1213 Warn of loopy local equalities that were dropped.
1214
1215
1216 ************************************************************************
1217 * *
1218 Type-class errors
1219 * *
1220 ************************************************************************
1221 -}
1222
1223 mkDictErr :: ReportErrCtxt -> [Ct] -> TcM ErrMsg
1224 mkDictErr ctxt cts
1225 = ASSERT( not (null cts) )
1226 do { inst_envs <- tcGetInstEnvs
1227 ; let (ct1:_) = cts -- ct1 just for its location
1228 min_cts = elim_superclasses cts
1229 ; lookups <- mapM (lookup_cls_inst inst_envs) min_cts
1230 ; let (no_inst_cts, overlap_cts) = partition is_no_inst lookups
1231
1232 -- Report definite no-instance errors,
1233 -- or (iff there are none) overlap errors
1234 -- But we report only one of them (hence 'head') because they all
1235 -- have the same source-location origin, to try avoid a cascade
1236 -- of error from one location
1237 ; (ctxt, err) <- mk_dict_err ctxt (head (no_inst_cts ++ overlap_cts))
1238 ; mkErrorMsgFromCt ctxt ct1 err }
1239 where
1240 no_givens = null (getUserGivens ctxt)
1241
1242 is_no_inst (ct, (matches, unifiers, _))
1243 = no_givens
1244 && null matches
1245 && (null unifiers || all (not . isAmbiguousTyVar) (varSetElems (tyVarsOfCt ct)))
1246
1247 lookup_cls_inst inst_envs ct
1248 = do { tys_flat <- mapM quickFlattenTy tys
1249 -- Note [Flattening in error message generation]
1250 ; return (ct, lookupInstEnv inst_envs clas tys_flat) }
1251 where
1252 (clas, tys) = getClassPredTys (ctPred ct)
1253
1254
1255 -- When simplifying [W] Ord (Set a), we need
1256 -- [W] Eq a, [W] Ord a
1257 -- but we really only want to report the latter
1258 elim_superclasses cts
1259 = filter (\ct -> any (eqPred (ctPred ct)) min_preds) cts
1260 where
1261 min_preds = mkMinimalBySCs (map ctPred cts)
1262
1263 mk_dict_err :: ReportErrCtxt -> (Ct, ClsInstLookupResult)
1264 -> TcM (ReportErrCtxt, SDoc)
1265 -- Report an overlap error if this class constraint results
1266 -- from an overlap (returning Left clas), otherwise return (Right pred)
1267 mk_dict_err ctxt (ct, (matches, unifiers, safe_haskell))
1268 | null matches -- No matches but perhaps several unifiers
1269 = do { let (is_ambig, ambig_msg) = mkAmbigMsg ct
1270 ; (ctxt, binds_msg, _) <- relevantBindings True ctxt ct
1271 ; traceTc "mk_dict_err" (ppr ct $$ ppr is_ambig $$ ambig_msg)
1272 ; return (ctxt, cannot_resolve_msg is_ambig binds_msg ambig_msg) }
1273
1274 | not safe_haskell -- Some matches => overlap errors
1275 = return (ctxt, overlap_msg)
1276
1277 | otherwise
1278 = return (ctxt, safe_haskell_msg)
1279 where
1280 orig = ctLocOrigin (ctLoc ct)
1281 pred = ctPred ct
1282 (clas, tys) = getClassPredTys pred
1283 ispecs = [ispec | (ispec, _) <- matches]
1284 givens = getUserGivens ctxt
1285 all_tyvars = all isTyVarTy tys
1286
1287 cannot_resolve_msg has_ambig_tvs binds_msg ambig_msg
1288 = vcat [ addArising orig no_inst_msg
1289 , vcat (pp_givens givens)
1290 , ppWhen (has_ambig_tvs && not (null unifiers && null givens))
1291 (vcat [ ambig_msg, binds_msg, potential_msg ])
1292 , show_fixes (add_to_ctxt_fixes has_ambig_tvs ++ drv_fixes) ]
1293
1294 potential_msg
1295 = ppWhen (not (null unifiers) && want_potential orig) $
1296 hang (if isSingleton unifiers
1297 then ptext (sLit "Note: there is a potential instance available:")
1298 else ptext (sLit "Note: there are several potential instances:"))
1299 2 (ppr_insts (sortBy fuzzyClsInstCmp unifiers))
1300
1301 -- Report "potential instances" only when the constraint arises
1302 -- directly from the user's use of an overloaded function
1303 want_potential (TypeEqOrigin {}) = False
1304 want_potential _ = True
1305
1306 add_to_ctxt_fixes has_ambig_tvs
1307 | not has_ambig_tvs && all_tyvars
1308 , (orig:origs) <- usefulContext ctxt pred
1309 = [sep [ ptext (sLit "add") <+> pprParendType pred
1310 <+> ptext (sLit "to the context of")
1311 , nest 2 $ ppr_skol orig $$
1312 vcat [ ptext (sLit "or") <+> ppr_skol orig
1313 | orig <- origs ] ] ]
1314 | otherwise = []
1315
1316 ppr_skol (PatSkol dc _) = ptext (sLit "the data constructor") <+> quotes (ppr dc)
1317 ppr_skol skol_info = ppr skol_info
1318
1319 no_inst_msg
1320 | null givens && null matches
1321 = ptext (sLit "No instance for")
1322 <+> pprParendType pred
1323 $$ if type_has_arrow pred
1324 then nest 2 $ ptext (sLit "(maybe you haven't applied a function to enough arguments?)")
1325 else empty
1326
1327 | otherwise
1328 = ptext (sLit "Could not deduce") <+> pprParendType pred
1329
1330 type_has_arrow (TyVarTy _) = False
1331 type_has_arrow (AppTy t1 t2) = type_has_arrow t1 || type_has_arrow t2
1332 type_has_arrow (TyConApp _ ts) = or $ map type_has_arrow ts
1333 type_has_arrow (FunTy _ _) = True
1334 type_has_arrow (ForAllTy _ t) = type_has_arrow t
1335 type_has_arrow (LitTy _) = False
1336
1337 drv_fixes = case orig of
1338 DerivOrigin -> [drv_fix]
1339 DerivOriginDC {} -> [drv_fix]
1340 DerivOriginCoerce {} -> [drv_fix]
1341 _ -> []
1342
1343 drv_fix = hang (ptext (sLit "use a standalone 'deriving instance' declaration,"))
1344 2 (ptext (sLit "so you can specify the instance context yourself"))
1345
1346 -- Normal overlap error
1347 overlap_msg
1348 = ASSERT( not (null matches) )
1349 vcat [ addArising orig (ptext (sLit "Overlapping instances for")
1350 <+> pprType (mkClassPred clas tys))
1351
1352 , ppUnless (null matching_givens) $
1353 sep [ptext (sLit "Matching givens (or their superclasses):")
1354 , nest 2 (vcat matching_givens)]
1355
1356 , sep [ptext (sLit "Matching instances:"),
1357 nest 2 (vcat [pprInstances ispecs, pprInstances unifiers])]
1358
1359 , ppWhen (null matching_givens && isSingleton matches && null unifiers) $
1360 -- Intuitively, some given matched the wanted in their
1361 -- flattened or rewritten (from given equalities) form
1362 -- but the matcher can't figure that out because the
1363 -- constraints are non-flat and non-rewritten so we
1364 -- simply report back the whole given
1365 -- context. Accelerate Smart.hs showed this problem.
1366 sep [ ptext (sLit "There exists a (perhaps superclass) match:")
1367 , nest 2 (vcat (pp_givens givens))]
1368
1369 , ppWhen (isSingleton matches) $
1370 parens (vcat [ ptext (sLit "The choice depends on the instantiation of") <+>
1371 quotes (pprWithCommas ppr (varSetElems (tyVarsOfTypes tys)))
1372 , ppWhen (null (matching_givens)) $
1373 vcat [ ptext (sLit "To pick the first instance above, use IncoherentInstances")
1374 , ptext (sLit "when compiling the other instance declarations")]
1375 ])]
1376 where
1377 ispecs = [ispec | (ispec, _) <- matches]
1378
1379 givens = getUserGivens ctxt
1380 matching_givens = mapMaybe matchable givens
1381
1382 matchable (evvars,skol_info,_,loc)
1383 = case ev_vars_matching of
1384 [] -> Nothing
1385 _ -> Just $ hang (pprTheta ev_vars_matching)
1386 2 (sep [ ptext (sLit "bound by") <+> ppr skol_info
1387 , ptext (sLit "at") <+> ppr loc])
1388 where ev_vars_matching = filter ev_var_matches (map evVarPred evvars)
1389 ev_var_matches ty = case getClassPredTys_maybe ty of
1390 Just (clas', tys')
1391 | clas' == clas
1392 , Just _ <- tcMatchTys (tyVarsOfTypes tys) tys tys'
1393 -> True
1394 | otherwise
1395 -> any ev_var_matches (immSuperClasses clas' tys')
1396 Nothing -> False
1397
1398 -- Overlap error because of Safe Haskell (first
1399 -- match should be the most specific match)
1400 safe_haskell_msg
1401 = ASSERT( length matches > 1 )
1402 vcat [ addArising orig (ptext (sLit "Unsafe overlapping instances for")
1403 <+> pprType (mkClassPred clas tys))
1404 , sep [ptext (sLit "The matching instance is:"),
1405 nest 2 (pprInstance $ head ispecs)]
1406 , vcat [ ptext $ sLit "It is compiled in a Safe module and as such can only"
1407 , ptext $ sLit "overlap instances from the same module, however it"
1408 , ptext $ sLit "overlaps the following instances from different modules:"
1409 , nest 2 (vcat [pprInstances $ tail ispecs])
1410 ]
1411 ]
1412
1413 usefulContext :: ReportErrCtxt -> TcPredType -> [SkolemInfo]
1414 usefulContext ctxt pred
1415 = go (cec_encl ctxt)
1416 where
1417 pred_tvs = tyVarsOfType pred
1418 go [] = []
1419 go (ic : ics)
1420 | implausible ic = rest
1421 | otherwise = ic_info ic : rest
1422 where
1423 -- Stop when the context binds a variable free in the predicate
1424 rest | any (`elemVarSet` pred_tvs) (ic_skols ic) = []
1425 | otherwise = go ics
1426
1427 implausible ic
1428 | null (ic_skols ic) = True
1429 | implausible_info (ic_info ic) = True
1430 | otherwise = False
1431
1432 implausible_info (SigSkol (InfSigCtxt {}) _) = True
1433 implausible_info _ = False
1434 -- Do not suggest adding constraints to an *inferred* type signature!
1435
1436 show_fixes :: [SDoc] -> SDoc
1437 show_fixes [] = empty
1438 show_fixes (f:fs) = sep [ ptext (sLit "Possible fix:")
1439 , nest 2 (vcat (f : map (ptext (sLit "or") <+>) fs))]
1440
1441 ppr_insts :: [ClsInst] -> SDoc
1442 ppr_insts insts
1443 = pprInstances (take 3 insts) $$ dot_dot_message
1444 where
1445 n_extra = length insts - 3
1446 dot_dot_message
1447 | n_extra <= 0 = empty
1448 | otherwise = ptext (sLit "...plus")
1449 <+> speakNOf n_extra (ptext (sLit "other"))
1450
1451 ----------------------
1452 quickFlattenTy :: TcType -> TcM TcType
1453 -- See Note [Flattening in error message generation]
1454 quickFlattenTy ty | Just ty' <- tcView ty = quickFlattenTy ty'
1455 quickFlattenTy ty@(TyVarTy {}) = return ty
1456 quickFlattenTy ty@(ForAllTy {}) = return ty -- See
1457 quickFlattenTy ty@(LitTy {}) = return ty
1458 -- Don't flatten because of the danger or removing a bound variable
1459 quickFlattenTy (AppTy ty1 ty2) = do { fy1 <- quickFlattenTy ty1
1460 ; fy2 <- quickFlattenTy ty2
1461 ; return (AppTy fy1 fy2) }
1462 quickFlattenTy (FunTy ty1 ty2) = do { fy1 <- quickFlattenTy ty1
1463 ; fy2 <- quickFlattenTy ty2
1464 ; return (FunTy fy1 fy2) }
1465 quickFlattenTy (TyConApp tc tys)
1466 | not (isTypeFamilyTyCon tc)
1467 = do { fys <- mapM quickFlattenTy tys
1468 ; return (TyConApp tc fys) }
1469 | otherwise
1470 = do { let (funtys,resttys) = splitAt (tyConArity tc) tys
1471 -- Ignore the arguments of the type family funtys
1472 ; v <- newMetaTyVar (TauTv False) (typeKind (TyConApp tc funtys))
1473 ; flat_resttys <- mapM quickFlattenTy resttys
1474 ; return (foldl AppTy (mkTyVarTy v) flat_resttys) }
1475
1476 {-
1477 Note [Flattening in error message generation]
1478 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1479 Consider (C (Maybe (F x))), where F is a type function, and we have
1480 instances
1481 C (Maybe Int) and C (Maybe a)
1482 Since (F x) might turn into Int, this is an overlap situation, and
1483 indeed (because of flattening) the main solver will have refrained
1484 from solving. But by the time we get to error message generation, we've
1485 un-flattened the constraint. So we must *re*-flatten it before looking
1486 up in the instance environment, lest we only report one matching
1487 instance when in fact there are two.
1488
1489 Re-flattening is pretty easy, because we don't need to keep track of
1490 evidence. We don't re-use the code in TcCanonical because that's in
1491 the TcS monad, and we are in TcM here.
1492
1493 Note [Quick-flatten polytypes]
1494 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1495 If we see C (Ix a => blah) or C (forall a. blah) we simply refrain from
1496 flattening any further. After all, there can be no instance declarations
1497 that match such things. And flattening under a for-all is problematic
1498 anyway; consider C (forall a. F a)
1499
1500 Note [Suggest -fprint-explicit-kinds]
1501 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1502 It can be terribly confusing to get an error message like (Trac #9171)
1503 Couldn't match expected type ‘GetParam Base (GetParam Base Int)’
1504 with actual type ‘GetParam Base (GetParam Base Int)’
1505 The reason may be that the kinds don't match up. Typically you'll get
1506 more useful information, but not when it's as a result of ambiguity.
1507 This test suggests -fprint-explicit-kinds when all the ambiguous type
1508 variables are kind variables.
1509 -}
1510
1511 mkAmbigMsg :: Ct -> (Bool, SDoc)
1512 mkAmbigMsg ct
1513 | null ambig_tkvs = (False, empty)
1514 | otherwise = (True, msg)
1515 where
1516 ambig_tkv_set = filterVarSet isAmbiguousTyVar (tyVarsOfCt ct)
1517 ambig_tkvs = varSetElems ambig_tkv_set
1518 (ambig_kvs, ambig_tvs) = partition isKindVar ambig_tkvs
1519
1520 msg | any isRuntimeUnkSkol ambig_tkvs -- See Note [Runtime skolems]
1521 = vcat [ ptext (sLit "Cannot resolve unknown runtime type") <> plural ambig_tvs
1522 <+> pprQuotedList ambig_tvs
1523 , ptext (sLit "Use :print or :force to determine these types")]
1524
1525 | not (null ambig_tvs)
1526 = pp_ambig (ptext (sLit "type")) ambig_tvs
1527
1528 | otherwise -- All ambiguous kind variabes; suggest -fprint-explicit-kinds
1529 = vcat [ pp_ambig (ptext (sLit "kind")) ambig_kvs
1530 , sdocWithDynFlags suggest_explicit_kinds ]
1531
1532 pp_ambig what tkvs
1533 = ptext (sLit "The") <+> what <+> ptext (sLit "variable") <> plural tkvs
1534 <+> pprQuotedList tkvs <+> is_or_are tkvs <+> ptext (sLit "ambiguous")
1535
1536 is_or_are [_] = text "is"
1537 is_or_are _ = text "are"
1538
1539 suggest_explicit_kinds dflags -- See Note [Suggest -fprint-explicit-kinds]
1540 | gopt Opt_PrintExplicitKinds dflags = empty
1541 | otherwise = ptext (sLit "Use -fprint-explicit-kinds to see the kind arguments")
1542
1543 pprSkol :: SkolemInfo -> SrcLoc -> SDoc
1544 pprSkol UnkSkol _
1545 = ptext (sLit "is an unknown type variable")
1546 pprSkol skol_info tv_loc
1547 = sep [ ptext (sLit "is a rigid type variable bound by"),
1548 sep [ppr skol_info, ptext (sLit "at") <+> ppr tv_loc]]
1549
1550 getSkolemInfo :: [Implication] -> TcTyVar -> SkolemInfo
1551 -- Get the skolem info for a type variable
1552 -- from the implication constraint that binds it
1553 getSkolemInfo [] tv
1554 = pprPanic "No skolem info:" (ppr tv)
1555
1556 getSkolemInfo (implic:implics) tv
1557 | tv `elem` ic_skols implic = ic_info implic
1558 | otherwise = getSkolemInfo implics tv
1559
1560 -----------------------
1561 -- relevantBindings looks at the value environment and finds values whose
1562 -- types mention any of the offending type variables. It has to be
1563 -- careful to zonk the Id's type first, so it has to be in the monad.
1564 -- We must be careful to pass it a zonked type variable, too.
1565 --
1566 -- We always remove closed top-level bindings, though,
1567 -- since they are never relevant (cf Trac #8233)
1568
1569 relevantBindings :: Bool -- True <=> filter by tyvar; False <=> no filtering
1570 -- See Trac #8191
1571 -> ReportErrCtxt -> Ct
1572 -> TcM (ReportErrCtxt, SDoc, CtOrigin)
1573 -- Also returns the zonked and tidied CtOrigin of the constraint
1574 relevantBindings want_filtering ctxt ct
1575 = do { dflags <- getDynFlags
1576 ; (env1, tidy_orig) <- zonkTidyOrigin (cec_tidy ctxt) (ctLocOrigin loc)
1577 ; let ct_tvs = tyVarsOfCt ct `unionVarSet` extra_tvs
1578
1579 -- For *kind* errors, report the relevant bindings of the
1580 -- enclosing *type* equality, because that's more useful for the programmer
1581 extra_tvs = case tidy_orig of
1582 KindEqOrigin t1 t2 _ -> tyVarsOfTypes [t1,t2]
1583 _ -> emptyVarSet
1584 ; traceTc "relevantBindings" $
1585 vcat [ ppr ct
1586 , pprCtOrigin (ctLocOrigin loc)
1587 , ppr ct_tvs
1588 , ppr [id | TcIdBndr id _ <- tcl_bndrs lcl_env] ]
1589
1590 ; (tidy_env', docs, discards)
1591 <- go env1 ct_tvs (maxRelevantBinds dflags)
1592 emptyVarSet [] False
1593 (tcl_bndrs lcl_env)
1594 -- tcl_bndrs has the innermost bindings first,
1595 -- which are probably the most relevant ones
1596
1597 ; let doc = hang (ptext (sLit "Relevant bindings include"))
1598 2 (vcat docs $$ max_msg)
1599 max_msg | discards
1600 = ptext (sLit "(Some bindings suppressed; use -fmax-relevant-binds=N or -fno-max-relevant-binds)")
1601 | otherwise = empty
1602
1603 ; if null docs
1604 then return (ctxt, empty, tidy_orig)
1605 else return (ctxt { cec_tidy = tidy_env' }, doc, tidy_orig) }
1606 where
1607 loc = ctLoc ct
1608 lcl_env = ctLocEnv loc
1609
1610 run_out :: Maybe Int -> Bool
1611 run_out Nothing = False
1612 run_out (Just n) = n <= 0
1613
1614 dec_max :: Maybe Int -> Maybe Int
1615 dec_max = fmap (\n -> n - 1)
1616
1617 go :: TidyEnv -> TcTyVarSet -> Maybe Int -> TcTyVarSet -> [SDoc]
1618 -> Bool -- True <=> some filtered out due to lack of fuel
1619 -> [TcIdBinder]
1620 -> TcM (TidyEnv, [SDoc], Bool) -- The bool says if we filtered any out
1621 -- because of lack of fuel
1622 go tidy_env _ _ _ docs discards []
1623 = return (tidy_env, reverse docs, discards)
1624 go tidy_env ct_tvs n_left tvs_seen docs discards (TcIdBndr id top_lvl : tc_bndrs)
1625 = do { (tidy_env', tidy_ty) <- zonkTidyTcType tidy_env (idType id)
1626 ; traceTc "relevantBindings 1" (ppr id <+> dcolon <+> ppr tidy_ty)
1627 ; let id_tvs = tyVarsOfType tidy_ty
1628 doc = sep [ pprPrefixOcc id <+> dcolon <+> ppr tidy_ty
1629 , nest 2 (parens (ptext (sLit "bound at")
1630 <+> ppr (getSrcLoc id)))]
1631 new_seen = tvs_seen `unionVarSet` id_tvs
1632
1633 ; if (want_filtering && not opt_PprStyle_Debug
1634 && id_tvs `disjointVarSet` ct_tvs)
1635 -- We want to filter out this binding anyway
1636 -- so discard it silently
1637 then go tidy_env ct_tvs n_left tvs_seen docs discards tc_bndrs
1638
1639 else if isTopLevel top_lvl && not (isNothing n_left)
1640 -- It's a top-level binding and we have not specified
1641 -- -fno-max-relevant-bindings, so discard it silently
1642 then go tidy_env ct_tvs n_left tvs_seen docs discards tc_bndrs
1643
1644 else if run_out n_left && id_tvs `subVarSet` tvs_seen
1645 -- We've run out of n_left fuel and this binding only
1646 -- mentions aleady-seen type variables, so discard it
1647 then go tidy_env ct_tvs n_left tvs_seen docs True tc_bndrs
1648
1649 -- Keep this binding, decrement fuel
1650 else go tidy_env' ct_tvs (dec_max n_left) new_seen (doc:docs) discards tc_bndrs }
1651
1652 -----------------------
1653 warnDefaulting :: [Ct] -> Type -> TcM ()
1654 warnDefaulting wanteds default_ty
1655 = do { warn_default <- woptM Opt_WarnTypeDefaults
1656 ; env0 <- tcInitTidyEnv
1657 ; let tidy_env = tidyFreeTyVars env0 $
1658 foldr (unionVarSet . tyVarsOfCt) emptyVarSet wanteds
1659 tidy_wanteds = map (tidyCt tidy_env) wanteds
1660 (loc, ppr_wanteds) = pprWithArising tidy_wanteds
1661 warn_msg = hang (ptext (sLit "Defaulting the following constraint(s) to type")
1662 <+> quotes (ppr default_ty))
1663 2 ppr_wanteds
1664 ; setCtLoc loc $ warnTc warn_default warn_msg }
1665
1666 {-
1667 Note [Runtime skolems]
1668 ~~~~~~~~~~~~~~~~~~~~~~
1669 We want to give a reasonably helpful error message for ambiguity
1670 arising from *runtime* skolems in the debugger. These
1671 are created by in RtClosureInspect.zonkRTTIType.
1672
1673 ************************************************************************
1674 * *
1675 Error from the canonicaliser
1676 These ones are called *during* constraint simplification
1677 * *
1678 ************************************************************************
1679 -}
1680
1681 solverDepthErrorTcS :: CtLoc -> TcType -> TcM a
1682 solverDepthErrorTcS loc ty
1683 = setCtLoc loc $
1684 do { ty <- zonkTcType ty
1685 ; env0 <- tcInitTidyEnv
1686 ; let tidy_env = tidyFreeTyVars env0 (tyVarsOfType ty)
1687 tidy_ty = tidyType tidy_env ty
1688 msg
1689 = vcat [ text "Reduction stack overflow; size =" <+> ppr depth
1690 , hang (text "When simplifying the following type:")
1691 2 (ppr tidy_ty)
1692 , note ]
1693 ; failWithTcM (tidy_env, msg) }
1694 where
1695 depth = ctLocDepth loc
1696 note = vcat
1697 [ text "Use -freduction-depth=0 to disable this check"
1698 , text "(any upper bound you could choose might fail unpredictably with"
1699 , text " minor updates to GHC, so disabling the check is recommended if"
1700 , text " you're sure that type checking should terminate)" ]