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