No deferred type errors under a forall
[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 GhcPrelude
13
14 import TcRnTypes
15 import TcRnMonad
16 import TcMType
17 import TcUnify( occCheckForErrors, OccCheckResult(..) )
18 import TcEnv( tcInitTidyEnv )
19 import TcType
20 import RnUnbound ( unknownNameSuggestions )
21 import Type
22 import TyCoRep
23 import Kind
24 import Unify ( tcMatchTys )
25 import Module
26 import FamInst
27 import FamInstEnv ( flattenTys )
28 import Inst
29 import InstEnv
30 import TyCon
31 import Class
32 import DataCon
33 import TcEvidence
34 import HsExpr ( UnboundVar(..) )
35 import HsBinds ( PatSynBind(..) )
36 import Name
37 import RdrName ( lookupGlobalRdrEnv, lookupGRE_Name, GlobalRdrEnv
38 , mkRdrUnqual, isLocalGRE, greSrcSpan, pprNameProvenance
39 , GlobalRdrElt (..), globalRdrEnvElts )
40 import PrelNames ( typeableClassName, hasKey, liftedRepDataConKey )
41 import Id
42 import Var
43 import VarSet
44 import VarEnv
45 import NameSet
46 import Bag
47 import ErrUtils ( ErrMsg, errDoc, pprLocErrMsg )
48 import BasicTypes
49 import ConLike ( ConLike(..))
50 import Util
51 import TcEnv (tcLookupIdMaybe)
52 import {-# SOURCE #-} TcSimplify ( tcSubsumes )
53 import FastString
54 import Outputable
55 import SrcLoc
56 import DynFlags
57 import ListSetOps ( equivClasses )
58 import Maybes
59 import Pair
60 import qualified GHC.LanguageExtensions as LangExt
61 import FV ( fvVarList, unionFV )
62
63 import Control.Monad ( when )
64 import Data.Foldable ( toList )
65 import Data.List ( partition, mapAccumL, nub, sortBy, unfoldr, foldl')
66 import qualified Data.Set as Set
67
68 import Data.Semigroup ( Semigroup )
69 import qualified Data.Semigroup as Semigroup
70
71
72 {-
73 ************************************************************************
74 * *
75 \section{Errors and contexts}
76 * *
77 ************************************************************************
78
79 ToDo: for these error messages, should we note the location as coming
80 from the insts, or just whatever seems to be around in the monad just
81 now?
82
83 Note [Deferring coercion errors to runtime]
84 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
85 While developing, sometimes it is desirable to allow compilation to succeed even
86 if there are type errors in the code. Consider the following case:
87
88 module Main where
89
90 a :: Int
91 a = 'a'
92
93 main = print "b"
94
95 Even though `a` is ill-typed, it is not used in the end, so if all that we're
96 interested in is `main` it is handy to be able to ignore the problems in `a`.
97
98 Since we treat type equalities as evidence, this is relatively simple. Whenever
99 we run into a type mismatch in TcUnify, we normally just emit an error. But it
100 is always safe to defer the mismatch to the main constraint solver. If we do
101 that, `a` will get transformed into
102
103 co :: Int ~ Char
104 co = ...
105
106 a :: Int
107 a = 'a' `cast` co
108
109 The constraint solver would realize that `co` is an insoluble constraint, and
110 emit an error with `reportUnsolved`. But we can also replace the right-hand side
111 of `co` with `error "Deferred type error: Int ~ Char"`. This allows the program
112 to compile, and it will run fine unless we evaluate `a`. This is what
113 `deferErrorsToRuntime` does.
114
115 It does this by keeping track of which errors correspond to which coercion
116 in TcErrors. TcErrors.reportTidyWanteds does not print the errors
117 and does not fail if -fdefer-type-errors is on, so that we can continue
118 compilation. The errors are turned into warnings in `reportUnsolved`.
119 -}
120
121 -- | Report unsolved goals as errors or warnings. We may also turn some into
122 -- deferred run-time errors if `-fdefer-type-errors` is on.
123 reportUnsolved :: WantedConstraints -> TcM (Bag EvBind)
124 reportUnsolved wanted
125 = do { binds_var <- newTcEvBinds
126 ; defer_errors <- goptM Opt_DeferTypeErrors
127 ; warn_errors <- woptM Opt_WarnDeferredTypeErrors -- implement #10283
128 ; let type_errors | not defer_errors = TypeError
129 | warn_errors = TypeWarn
130 | otherwise = TypeDefer
131
132 ; defer_holes <- goptM Opt_DeferTypedHoles
133 ; warn_holes <- woptM Opt_WarnTypedHoles
134 ; let expr_holes | not defer_holes = HoleError
135 | warn_holes = HoleWarn
136 | otherwise = HoleDefer
137
138 ; partial_sigs <- xoptM LangExt.PartialTypeSignatures
139 ; warn_partial_sigs <- woptM Opt_WarnPartialTypeSignatures
140 ; let type_holes | not partial_sigs = HoleError
141 | warn_partial_sigs = HoleWarn
142 | otherwise = HoleDefer
143
144 ; defer_out_of_scope <- goptM Opt_DeferOutOfScopeVariables
145 ; warn_out_of_scope <- woptM Opt_WarnDeferredOutOfScopeVariables
146 ; let out_of_scope_holes | not defer_out_of_scope = HoleError
147 | warn_out_of_scope = HoleWarn
148 | otherwise = HoleDefer
149
150 ; report_unsolved binds_var False type_errors expr_holes
151 type_holes out_of_scope_holes wanted
152
153 ; ev_binds <- getTcEvBindsMap binds_var
154 ; return (evBindMapBinds ev_binds)}
155
156 -- | Report *all* unsolved goals as errors, even if -fdefer-type-errors is on
157 -- However, do not make any evidence bindings, because we don't
158 -- have any convenient place to put them.
159 -- See Note [Deferring coercion errors to runtime]
160 -- Used by solveEqualities for kind equalities
161 -- (see Note [Fail fast on kind errors] in TcSimplify]
162 -- and for simplifyDefault.
163 reportAllUnsolved :: WantedConstraints -> TcM ()
164 reportAllUnsolved wanted
165 = do { ev_binds <- newTcEvBinds
166 ; report_unsolved ev_binds False TypeError
167 HoleError HoleError HoleError wanted }
168
169 -- | Report all unsolved goals as warnings (but without deferring any errors to
170 -- run-time). See Note [Safe Haskell Overlapping Instances Implementation] in
171 -- TcSimplify
172 warnAllUnsolved :: WantedConstraints -> TcM ()
173 warnAllUnsolved wanted
174 = do { ev_binds <- newTcEvBinds
175 ; report_unsolved ev_binds True TypeWarn
176 HoleWarn HoleWarn HoleWarn wanted }
177
178 -- | Report unsolved goals as errors or warnings.
179 report_unsolved :: EvBindsVar -- cec_binds
180 -> Bool -- Errors as warnings
181 -> TypeErrorChoice -- Deferred type errors
182 -> HoleChoice -- Expression holes
183 -> HoleChoice -- Type holes
184 -> HoleChoice -- Out of scope holes
185 -> WantedConstraints -> TcM ()
186 report_unsolved mb_binds_var err_as_warn type_errors expr_holes
187 type_holes out_of_scope_holes wanted
188 | isEmptyWC wanted
189 = return ()
190 | otherwise
191 = do { traceTc "reportUnsolved (before zonking and tidying)" (ppr wanted)
192
193 ; wanted <- zonkWC wanted -- Zonk to reveal all information
194 ; env0 <- tcInitTidyEnv
195 -- If we are deferring we are going to need /all/ evidence around,
196 -- including the evidence produced by unflattening (zonkWC)
197 ; let tidy_env = tidyFreeTyCoVars env0 free_tvs
198 free_tvs = tyCoVarsOfWCList wanted
199
200 ; traceTc "reportUnsolved (after zonking):" $
201 vcat [ text "Free tyvars:" <+> pprTyVars free_tvs
202 , text "Tidy env:" <+> ppr tidy_env
203 , text "Wanted:" <+> ppr wanted ]
204
205 ; warn_redundant <- woptM Opt_WarnRedundantConstraints
206 ; let err_ctxt = CEC { cec_encl = []
207 , cec_tidy = tidy_env
208 , cec_defer_type_errors = type_errors
209 , cec_errors_as_warns = err_as_warn
210 , cec_expr_holes = expr_holes
211 , cec_type_holes = type_holes
212 , cec_out_of_scope_holes = out_of_scope_holes
213 , cec_suppress = False -- See Note [Suppressing error messages]
214 , cec_warn_redundant = warn_redundant
215 , cec_binds = mb_binds_var }
216
217 ; tc_lvl <- getTcLevel
218 ; reportWanteds err_ctxt tc_lvl wanted }
219
220 --------------------------------------------
221 -- Internal functions
222 --------------------------------------------
223
224 -- | An error Report collects messages categorised by their importance.
225 -- See Note [Error report] for details.
226 data Report
227 = Report { report_important :: [SDoc]
228 , report_relevant_bindings :: [SDoc]
229 , report_valid_substitutions :: [SDoc]
230 }
231
232 instance Outputable Report where -- Debugging only
233 ppr (Report { report_important = imp
234 , report_relevant_bindings = rel
235 , report_valid_substitutions = val })
236 = vcat [ text "important:" <+> vcat imp
237 , text "relevant:" <+> vcat rel
238 , text "valid:" <+> vcat val ]
239
240 {- Note [Error report]
241 The idea is that error msgs are divided into three parts: the main msg, the
242 context block (\"In the second argument of ...\"), and the relevant bindings
243 block, which are displayed in that order, with a mark to divide them. The
244 idea is that the main msg ('report_important') varies depending on the error
245 in question, but context and relevant bindings are always the same, which
246 should simplify visual parsing.
247
248 The context is added when the Report is passed off to 'mkErrorReport'.
249 Unfortunately, unlike the context, the relevant bindings are added in
250 multiple places so they have to be in the Report.
251 -}
252
253 instance Semigroup Report where
254 Report a1 b1 c1 <> Report a2 b2 c2 = Report (a1 ++ a2) (b1 ++ b2) (c1 ++ c2)
255
256 instance Monoid Report where
257 mempty = Report [] [] []
258 mappend = (Semigroup.<>)
259
260 -- | Put a doc into the important msgs block.
261 important :: SDoc -> Report
262 important doc = mempty { report_important = [doc] }
263
264 -- | Put a doc into the relevant bindings block.
265 relevant_bindings :: SDoc -> Report
266 relevant_bindings doc = mempty { report_relevant_bindings = [doc] }
267
268 -- | Put a doc into the valid substitutions block.
269 valid_substitutions :: SDoc -> Report
270 valid_substitutions docs = mempty { report_valid_substitutions = [docs] }
271
272 data TypeErrorChoice -- What to do for type errors found by the type checker
273 = TypeError -- A type error aborts compilation with an error message
274 | TypeWarn -- A type error is deferred to runtime, plus a compile-time warning
275 | TypeDefer -- A type error is deferred to runtime; no error or warning at compile time
276
277 data HoleChoice
278 = HoleError -- A hole is a compile-time error
279 | HoleWarn -- Defer to runtime, emit a compile-time warning
280 | HoleDefer -- Defer to runtime, no warning
281
282 instance Outputable HoleChoice where
283 ppr HoleError = text "HoleError"
284 ppr HoleWarn = text "HoleWarn"
285 ppr HoleDefer = text "HoleDefer"
286
287 instance Outputable TypeErrorChoice where
288 ppr TypeError = text "TypeError"
289 ppr TypeWarn = text "TypeWarn"
290 ppr TypeDefer = text "TypeDefer"
291
292 data ReportErrCtxt
293 = CEC { cec_encl :: [Implication] -- Enclosing implications
294 -- (innermost first)
295 -- ic_skols and givens are tidied, rest are not
296 , cec_tidy :: TidyEnv
297
298 , cec_binds :: EvBindsVar -- Make some errors (depending on cec_defer)
299 -- into warnings, and emit evidence bindings
300 -- into 'cec_binds' for unsolved constraints
301
302 , cec_errors_as_warns :: Bool -- Turn all errors into warnings
303 -- (except for Holes, which are
304 -- controlled by cec_type_holes and
305 -- cec_expr_holes)
306 , cec_defer_type_errors :: TypeErrorChoice -- Defer type errors until runtime
307
308 -- cec_expr_holes is a union of:
309 -- cec_type_holes - a set of typed holes: '_', '_a', '_foo'
310 -- cec_out_of_scope_holes - a set of variables which are
311 -- out of scope: 'x', 'y', 'bar'
312 , cec_expr_holes :: HoleChoice -- Holes in expressions
313 , cec_type_holes :: HoleChoice -- Holes in types
314 , cec_out_of_scope_holes :: HoleChoice -- Out of scope holes
315
316 , cec_warn_redundant :: Bool -- True <=> -Wredundant-constraints
317
318 , cec_suppress :: Bool -- True <=> More important errors have occurred,
319 -- so create bindings if need be, but
320 -- don't issue any more errors/warnings
321 -- See Note [Suppressing error messages]
322 }
323
324 instance Outputable ReportErrCtxt where
325 ppr (CEC { cec_binds = bvar
326 , cec_errors_as_warns = ew
327 , cec_defer_type_errors = dte
328 , cec_expr_holes = eh
329 , cec_type_holes = th
330 , cec_out_of_scope_holes = osh
331 , cec_warn_redundant = wr
332 , cec_suppress = sup })
333 = text "CEC" <+> braces (vcat
334 [ text "cec_binds" <+> equals <+> ppr bvar
335 , text "cec_errors_as_warns" <+> equals <+> ppr ew
336 , text "cec_defer_type_errors" <+> equals <+> ppr dte
337 , text "cec_expr_holes" <+> equals <+> ppr eh
338 , text "cec_type_holes" <+> equals <+> ppr th
339 , text "cec_out_of_scope_holes" <+> equals <+> ppr osh
340 , text "cec_warn_redundant" <+> equals <+> ppr wr
341 , text "cec_suppress" <+> equals <+> ppr sup ])
342
343 {-
344 Note [Suppressing error messages]
345 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
346 The cec_suppress flag says "don't report any errors". Instead, just create
347 evidence bindings (as usual). It's used when more important errors have occurred.
348
349 Specifically (see reportWanteds)
350 * If there are insoluble Givens, then we are in unreachable code and all bets
351 are off. So don't report any further errors.
352 * If there are any insolubles (eg Int~Bool), here or in a nested implication,
353 then suppress errors from the simple constraints here. Sometimes the
354 simple-constraint errors are a knock-on effect of the insolubles.
355 -}
356
357 reportImplic :: ReportErrCtxt -> Implication -> TcM ()
358 reportImplic ctxt implic@(Implic { ic_skols = tvs, ic_given = given
359 , ic_wanted = wanted, ic_binds = evb
360 , ic_status = status, ic_info = info
361 , ic_env = tcl_env, ic_tclvl = tc_lvl })
362 | BracketSkol <- info
363 , not insoluble
364 = return () -- For Template Haskell brackets report only
365 -- definite errors. The whole thing will be re-checked
366 -- later when we plug it in, and meanwhile there may
367 -- certainly be un-satisfied constraints
368
369 | otherwise
370 = do { traceTc "reportImplic" (ppr implic')
371 ; reportWanteds ctxt' tc_lvl wanted
372 ; when (cec_warn_redundant ctxt) $
373 warnRedundantConstraints ctxt' tcl_env info' dead_givens }
374 where
375 insoluble = isInsolubleStatus status
376 (env1, tvs') = mapAccumL tidyTyCoVarBndr (cec_tidy ctxt) tvs
377 info' = tidySkolemInfo env1 info
378 implic' = implic { ic_skols = tvs'
379 , ic_given = map (tidyEvVar env1) given
380 , ic_info = info' }
381 ctxt1 | termEvidenceAllowed info = ctxt
382 | otherwise = ctxt { cec_defer_type_errors = TypeError }
383 -- If we go inside an implication that has no term
384 -- evidence (i.e. unifying under a forall), we can't defer
385 -- type errors. You could imagine using the /enclosing/
386 -- bindings (in cec_binds), but that may not have enough stuff
387 -- in scope for the bindings to be well typed. So we just
388 -- switch off deferred type errors altogether. See Trac #14605.
389
390 ctxt' = ctxt1 { cec_tidy = env1
391 , cec_encl = implic' : cec_encl ctxt
392
393 , cec_suppress = insoluble || cec_suppress ctxt
394 -- Suppress inessential errors if there
395 -- are insolubles anywhere in the
396 -- tree rooted here, or we've come across
397 -- a suppress-worthy constraint higher up (Trac #11541)
398
399 , cec_binds = evb }
400
401 dead_givens = case status of
402 IC_Solved { ics_dead = dead } -> dead
403 _ -> []
404
405 warnRedundantConstraints :: ReportErrCtxt -> TcLclEnv -> SkolemInfo -> [EvVar] -> TcM ()
406 -- See Note [Tracking redundant constraints] in TcSimplify
407 warnRedundantConstraints ctxt env info ev_vars
408 | null redundant_evs
409 = return ()
410
411 | SigSkol {} <- info
412 = setLclEnv env $ -- We want to add "In the type signature for f"
413 -- to the error context, which is a bit tiresome
414 addErrCtxt (text "In" <+> ppr info) $
415 do { env <- getLclEnv
416 ; msg <- mkErrorReport ctxt env (important doc)
417 ; reportWarning (Reason Opt_WarnRedundantConstraints) msg }
418
419 | otherwise -- But for InstSkol there already *is* a surrounding
420 -- "In the instance declaration for Eq [a]" context
421 -- and we don't want to say it twice. Seems a bit ad-hoc
422 = do { msg <- mkErrorReport ctxt env (important doc)
423 ; reportWarning (Reason Opt_WarnRedundantConstraints) msg }
424 where
425 doc = text "Redundant constraint" <> plural redundant_evs <> colon
426 <+> pprEvVarTheta redundant_evs
427
428 redundant_evs = case info of -- See Note [Redundant constraints in instance decls]
429 InstSkol -> filterOut improving ev_vars
430 _ -> ev_vars
431
432 improving ev_var = any isImprovementPred $
433 transSuperClasses (idType ev_var)
434
435 {- Note [Redundant constraints in instance decls]
436 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
437 For instance declarations, we don't report unused givens if
438 they can give rise to improvement. Example (Trac #10100):
439 class Add a b ab | a b -> ab, a ab -> b
440 instance Add Zero b b
441 instance Add a b ab => Add (Succ a) b (Succ ab)
442 The context (Add a b ab) for the instance is clearly unused in terms
443 of evidence, since the dictionary has no fields. But it is still
444 needed! With the context, a wanted constraint
445 Add (Succ Zero) beta (Succ Zero)
446 we will reduce to (Add Zero beta Zero), and thence we get beta := Zero.
447 But without the context we won't find beta := Zero.
448
449 This only matters in instance declarations..
450 -}
451
452 reportWanteds :: ReportErrCtxt -> TcLevel -> WantedConstraints -> TcM ()
453 reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_impl = implics })
454 = do { traceTc "reportWanteds" (vcat [ text "Simples =" <+> ppr simples
455 , text "Suppress =" <+> ppr (cec_suppress ctxt)])
456 ; let tidy_cts = bagToList (mapBag (tidyCt env) simples)
457 ; traceTc "rw2" (ppr tidy_cts)
458
459 -- First deal with things that are utterly wrong
460 -- Like Int ~ Bool (incl nullary TyCons)
461 -- or Int ~ t a (AppTy on one side)
462 -- These /ones/ are not suppressed by the incoming context
463 ; let ctxt_for_insols = ctxt { cec_suppress = False }
464 ; (ctxt1, cts1) <- tryReporters ctxt_for_insols report1 tidy_cts
465
466 -- Now all the other constraints. We suppress errors here if
467 -- any of the first batch failed, or if the enclosing context
468 -- says to suppress
469 ; let ctxt2 = ctxt { cec_suppress = cec_suppress ctxt || cec_suppress ctxt1 }
470 ; (_, leftovers) <- tryReporters ctxt2 report2 cts1
471 ; MASSERT2( null leftovers, ppr leftovers )
472
473 -- All the Derived ones have been filtered out of simples
474 -- by the constraint solver. This is ok; we don't want
475 -- to report unsolved Derived goals as errors
476 -- See Note [Do not report derived but soluble errors]
477
478 ; mapBagM_ (reportImplic ctxt2) implics }
479 -- NB ctxt1: don't suppress inner insolubles if there's only a
480 -- wanted insoluble here; but do suppress inner insolubles
481 -- if there's a *given* insoluble here (= inaccessible code)
482 where
483 env = cec_tidy ctxt
484
485 -- report1: ones that should *not* be suppresed by
486 -- an insoluble somewhere else in the tree
487 -- It's crucial that anything that is considered insoluble
488 -- (see TcRnTypes.insolubleWantedCt) is caught here, otherwise
489 -- we might suppress its error message, and proceed on past
490 -- type checking to get a Lint error later
491 report1 = [ ("custom_error", is_user_type_error,True, mkUserTypeErrorReporter)
492 , given_eq_spec
493 , ("insoluble2", utterly_wrong, True, mkGroupReporter mkEqErr)
494 , ("skolem eq1", very_wrong, True, mkSkolReporter)
495 , ("skolem eq2", skolem_eq, True, mkSkolReporter)
496 , ("non-tv eq", non_tv_eq, True, mkSkolReporter)
497 , ("Out of scope", is_out_of_scope, True, mkHoleReporter)
498 , ("Holes", is_hole, False, mkHoleReporter)
499
500 -- The only remaining equalities are alpha ~ ty,
501 -- where alpha is untouchable; and representational equalities
502 -- Prefer homogeneous equalities over hetero, because the
503 -- former might be holding up the latter.
504 -- See Note [Equalities with incompatible kinds] in TcCanonical
505 , ("Homo eqs", is_homo_equality, True, mkGroupReporter mkEqErr)
506 , ("Other eqs", is_equality, False, mkGroupReporter mkEqErr) ]
507
508 -- report2: we suppress these if there are insolubles elsewhere in the tree
509 report2 = [ ("Implicit params", is_ip, False, mkGroupReporter mkIPErr)
510 , ("Irreds", is_irred, False, mkGroupReporter mkIrredErr)
511 , ("Dicts", is_dict, False, mkGroupReporter mkDictErr) ]
512
513 -- rigid_nom_eq, rigid_nom_tv_eq,
514 is_hole, is_dict,
515 is_equality, is_ip, is_irred :: Ct -> PredTree -> Bool
516
517 is_given_eq ct pred
518 | EqPred {} <- pred = arisesFromGivens ct
519 | otherwise = False
520 -- I think all given residuals are equalities
521
522 -- Things like (Int ~N Bool)
523 utterly_wrong _ (EqPred NomEq ty1 ty2) = isRigidTy ty1 && isRigidTy ty2
524 utterly_wrong _ _ = False
525
526 -- Things like (a ~N Int)
527 very_wrong _ (EqPred NomEq ty1 ty2) = isSkolemTy tc_lvl ty1 && isRigidTy ty2
528 very_wrong _ _ = False
529
530 -- Things like (a ~N b) or (a ~N F Bool)
531 skolem_eq _ (EqPred NomEq ty1 _) = isSkolemTy tc_lvl ty1
532 skolem_eq _ _ = False
533
534 -- Things like (F a ~N Int)
535 non_tv_eq _ (EqPred NomEq ty1 _) = not (isTyVarTy ty1)
536 non_tv_eq _ _ = False
537
538 is_out_of_scope ct _ = isOutOfScopeCt ct
539 is_hole ct _ = isHoleCt ct
540
541 is_user_type_error ct _ = isUserTypeErrorCt ct
542
543 is_homo_equality _ (EqPred _ ty1 ty2) = typeKind ty1 `tcEqType` typeKind ty2
544 is_homo_equality _ _ = False
545
546 is_equality _ (EqPred {}) = True
547 is_equality _ _ = False
548
549 is_dict _ (ClassPred {}) = True
550 is_dict _ _ = False
551
552 is_ip _ (ClassPred cls _) = isIPClass cls
553 is_ip _ _ = False
554
555 is_irred _ (IrredPred {}) = True
556 is_irred _ _ = False
557
558 given_eq_spec = case find_gadt_match (cec_encl ctxt) of
559 Just imp -> ("insoluble1a", is_given_eq, True, mkGivenErrorReporter imp)
560 Nothing -> ("insoluble1b", is_given_eq, False, ignoreErrorReporter)
561 -- False means don't suppress subsequent errors
562 -- Reason: we don't report all given errors
563 -- (see mkGivenErrorReporter), and we should only suppress
564 -- subsequent errors if we actually report this one!
565 -- Trac #13446 is an example
566
567 find_gadt_match [] = Nothing
568 find_gadt_match (implic : implics)
569 | PatSkol {} <- ic_info implic
570 , not (ic_no_eqs implic)
571 = Just implic
572 | otherwise
573 = find_gadt_match implics
574
575 ---------------
576 isSkolemTy :: TcLevel -> Type -> Bool
577 -- The type is a skolem tyvar
578 isSkolemTy tc_lvl ty
579 | Just tv <- getTyVar_maybe ty
580 = isSkolemTyVar tv
581 || (isSigTyVar tv && isTouchableMetaTyVar tc_lvl tv)
582 -- The last case is for touchable SigTvs
583 -- we postpone untouchables to a latter test (too obscure)
584
585 | otherwise
586 = False
587
588 isTyFun_maybe :: Type -> Maybe TyCon
589 isTyFun_maybe ty = case tcSplitTyConApp_maybe ty of
590 Just (tc,_) | isTypeFamilyTyCon tc -> Just tc
591 _ -> Nothing
592
593 --------------------------------------------
594 -- Reporters
595 --------------------------------------------
596
597 type Reporter
598 = ReportErrCtxt -> [Ct] -> TcM ()
599 type ReporterSpec
600 = ( String -- Name
601 , Ct -> PredTree -> Bool -- Pick these ones
602 , Bool -- True <=> suppress subsequent reporters
603 , Reporter) -- The reporter itself
604
605 mkSkolReporter :: Reporter
606 -- Suppress duplicates with either the same LHS, or same location
607 mkSkolReporter ctxt cts
608 = mapM_ (reportGroup mkEqErr ctxt) (group cts)
609 where
610 group [] = []
611 group (ct:cts) = (ct : yeses) : group noes
612 where
613 (yeses, noes) = partition (group_with ct) cts
614
615 group_with ct1 ct2
616 | EQ <- cmp_loc ct1 ct2 = True
617 | eq_lhs_type ct1 ct2 = True
618 | otherwise = False
619
620 mkHoleReporter :: Reporter
621 -- Reports errors one at a time
622 mkHoleReporter ctxt
623 = mapM_ $ \ct -> do { err <- mkHoleError ctxt ct
624 ; maybeReportHoleError ctxt ct err
625 ; maybeAddDeferredHoleBinding ctxt err ct }
626
627 mkUserTypeErrorReporter :: Reporter
628 mkUserTypeErrorReporter ctxt
629 = mapM_ $ \ct -> do { err <- mkUserTypeError ctxt ct
630 ; maybeReportError ctxt err
631 ; addDeferredBinding ctxt err ct }
632
633 mkUserTypeError :: ReportErrCtxt -> Ct -> TcM ErrMsg
634 mkUserTypeError ctxt ct = mkErrorMsgFromCt ctxt ct
635 $ important
636 $ pprUserTypeErrorTy
637 $ case getUserTypeErrorMsg ct of
638 Just msg -> msg
639 Nothing -> pprPanic "mkUserTypeError" (ppr ct)
640
641
642 mkGivenErrorReporter :: Implication -> Reporter
643 -- See Note [Given errors]
644 mkGivenErrorReporter implic ctxt cts
645 = do { (ctxt, binds_msg, ct) <- relevantBindings True ctxt ct
646 ; dflags <- getDynFlags
647 ; let ct' = setCtLoc ct (setCtLocEnv (ctLoc ct) (ic_env implic))
648 -- For given constraints we overwrite the env (and hence src-loc)
649 -- with one from the implication. See Note [Inaccessible code]
650
651 inaccessible_msg = hang (text "Inaccessible code in")
652 2 (ppr (ic_info implic))
653 report = important inaccessible_msg `mappend`
654 relevant_bindings binds_msg
655
656 ; err <- mkEqErr_help dflags ctxt report ct'
657 Nothing ty1 ty2
658
659 ; traceTc "mkGivenErrorReporter" (ppr ct)
660 ; maybeReportError ctxt err }
661 where
662 (ct : _ ) = cts -- Never empty
663 (ty1, ty2) = getEqPredTys (ctPred ct)
664
665 ignoreErrorReporter :: Reporter
666 -- Discard Given errors that don't come from
667 -- a pattern match; maybe we should warn instead?
668 ignoreErrorReporter ctxt cts
669 = do { traceTc "mkGivenErrorReporter no" (ppr cts $$ ppr (cec_encl ctxt))
670 ; return () }
671
672
673 {- Note [Given errors]
674 ~~~~~~~~~~~~~~~~~~~~~~
675 Given constraints represent things for which we have (or will have)
676 evidence, so they aren't errors. But if a Given constraint is
677 insoluble, this code is inaccessible, and we might want to at least
678 warn about that. A classic case is
679
680 data T a where
681 T1 :: T Int
682 T2 :: T a
683 T3 :: T Bool
684
685 f :: T Int -> Bool
686 f T1 = ...
687 f T2 = ...
688 f T3 = ... -- We want to report this case as inaccessible
689
690 We'd like to point out that the T3 match is inaccessible. It
691 will have a Given constraint [G] Int ~ Bool.
692
693 But we don't want to report ALL insoluble Given constraints. See Trac
694 #12466 for a long discussion. For example, if we aren't careful
695 we'll complain about
696 f :: ((Int ~ Bool) => a -> a) -> Int
697 which arguably is OK. It's more debatable for
698 g :: (Int ~ Bool) => Int -> Int
699 but it's tricky to distinguish these cases to we don't report
700 either.
701
702 The bottom line is this: find_gadt_match looks for an enclosing
703 pattern match which binds some equality constraints. If we
704 find one, we report the insoluble Given.
705 -}
706
707 mkGroupReporter :: (ReportErrCtxt -> [Ct] -> TcM ErrMsg)
708 -- Make error message for a group
709 -> Reporter -- Deal with lots of constraints
710 -- Group together errors from same location,
711 -- and report only the first (to avoid a cascade)
712 mkGroupReporter mk_err ctxt cts
713 = mapM_ (reportGroup mk_err ctxt . toList) (equivClasses cmp_loc cts)
714
715 eq_lhs_type :: Ct -> Ct -> Bool
716 eq_lhs_type ct1 ct2
717 = case (classifyPredType (ctPred ct1), classifyPredType (ctPred ct2)) of
718 (EqPred eq_rel1 ty1 _, EqPred eq_rel2 ty2 _) ->
719 (eq_rel1 == eq_rel2) && (ty1 `eqType` ty2)
720 _ -> pprPanic "mkSkolReporter" (ppr ct1 $$ ppr ct2)
721
722 cmp_loc :: Ct -> Ct -> Ordering
723 cmp_loc ct1 ct2 = ctLocSpan (ctLoc ct1) `compare` ctLocSpan (ctLoc ct2)
724
725 reportGroup :: (ReportErrCtxt -> [Ct] -> TcM ErrMsg) -> ReportErrCtxt
726 -> [Ct] -> TcM ()
727 reportGroup mk_err ctxt cts =
728 case partition isMonadFailInstanceMissing cts of
729 -- Only warn about missing MonadFail constraint when
730 -- there are no other missing constraints!
731 (monadFailCts, []) ->
732 do { err <- mk_err ctxt monadFailCts
733 ; reportWarning (Reason Opt_WarnMissingMonadFailInstances) err }
734
735 (_, cts') -> do { err <- mk_err ctxt cts'
736 ; maybeReportError ctxt err
737 -- But see Note [Always warn with -fdefer-type-errors]
738 ; traceTc "reportGroup" (ppr cts')
739 ; mapM_ (addDeferredBinding ctxt err) cts' }
740 -- Add deferred bindings for all
741 -- Redundant if we are going to abort compilation,
742 -- but that's hard to know for sure, and if we don't
743 -- abort, we need bindings for all (e.g. Trac #12156)
744 where
745 isMonadFailInstanceMissing ct =
746 case ctLocOrigin (ctLoc ct) of
747 FailablePattern _pat -> True
748 _otherwise -> False
749
750 maybeReportHoleError :: ReportErrCtxt -> Ct -> ErrMsg -> TcM ()
751 maybeReportHoleError ctxt ct err
752 -- When -XPartialTypeSignatures is on, warnings (instead of errors) are
753 -- generated for holes in partial type signatures.
754 -- Unless -fwarn_partial_type_signatures is not on,
755 -- in which case the messages are discarded.
756 | isTypeHoleCt ct
757 = -- For partial type signatures, generate warnings only, and do that
758 -- only if -fwarn_partial_type_signatures is on
759 case cec_type_holes ctxt of
760 HoleError -> reportError err
761 HoleWarn -> reportWarning (Reason Opt_WarnPartialTypeSignatures) err
762 HoleDefer -> return ()
763
764 -- Always report an error for out-of-scope variables
765 -- Unless -fdefer-out-of-scope-variables is on,
766 -- in which case the messages are discarded.
767 -- See Trac #12170, #12406
768 | isOutOfScopeCt ct
769 = -- If deferring, report a warning only if -Wout-of-scope-variables is on
770 case cec_out_of_scope_holes ctxt of
771 HoleError -> reportError err
772 HoleWarn ->
773 reportWarning (Reason Opt_WarnDeferredOutOfScopeVariables) err
774 HoleDefer -> return ()
775
776 -- Otherwise this is a typed hole in an expression,
777 -- but not for an out-of-scope variable
778 | otherwise
779 = -- If deferring, report a warning only if -Wtyped-holes is on
780 case cec_expr_holes ctxt of
781 HoleError -> reportError err
782 HoleWarn -> reportWarning (Reason Opt_WarnTypedHoles) err
783 HoleDefer -> return ()
784
785 maybeReportError :: ReportErrCtxt -> ErrMsg -> TcM ()
786 -- Report the error and/or make a deferred binding for it
787 maybeReportError ctxt err
788 | cec_suppress ctxt -- Some worse error has occurred;
789 = return () -- so suppress this error/warning
790
791 | cec_errors_as_warns ctxt
792 = reportWarning NoReason err
793
794 | otherwise
795 = case cec_defer_type_errors ctxt of
796 TypeDefer -> return ()
797 TypeWarn -> reportWarning (Reason Opt_WarnDeferredTypeErrors) err
798 TypeError -> reportError err
799
800 addDeferredBinding :: ReportErrCtxt -> ErrMsg -> Ct -> TcM ()
801 -- See Note [Deferring coercion errors to runtime]
802 addDeferredBinding ctxt err ct
803 | CtWanted { ctev_pred = pred, ctev_dest = dest } <- ctEvidence ct
804 -- Only add deferred bindings for Wanted constraints
805 = do { dflags <- getDynFlags
806 ; let err_msg = pprLocErrMsg err
807 err_fs = mkFastString $ showSDoc dflags $
808 err_msg $$ text "(deferred type error)"
809 err_tm = EvDelayedError pred err_fs
810 ev_binds_var = cec_binds ctxt
811
812 ; case dest of
813 EvVarDest evar
814 -> addTcEvBind ev_binds_var $ mkWantedEvBind evar err_tm
815 HoleDest hole
816 -> do { -- See Note [Deferred errors for coercion holes]
817 let co_var = coHoleCoVar hole
818 ; addTcEvBind ev_binds_var $ mkWantedEvBind co_var err_tm
819 ; fillCoercionHole hole (mkTcCoVarCo co_var) }}
820
821 | otherwise -- Do not set any evidence for Given/Derived
822 = return ()
823
824 maybeAddDeferredHoleBinding :: ReportErrCtxt -> ErrMsg -> Ct -> TcM ()
825 maybeAddDeferredHoleBinding ctxt err ct
826 | isExprHoleCt ct
827 = addDeferredBinding ctxt err ct -- Only add bindings for holes in expressions
828 | otherwise -- not for holes in partial type signatures
829 = return ()
830
831 tryReporters :: ReportErrCtxt -> [ReporterSpec] -> [Ct] -> TcM (ReportErrCtxt, [Ct])
832 -- Use the first reporter in the list whose predicate says True
833 tryReporters ctxt reporters cts
834 = do { let (vis_cts, invis_cts) = partition (isVisibleOrigin . ctOrigin) cts
835 ; traceTc "tryReporters {" (ppr vis_cts $$ ppr invis_cts)
836 ; (ctxt', cts') <- go ctxt reporters vis_cts invis_cts
837 ; traceTc "tryReporters }" (ppr cts')
838 ; return (ctxt', cts') }
839 where
840 go ctxt [] vis_cts invis_cts
841 = return (ctxt, vis_cts ++ invis_cts)
842
843 go ctxt (r : rs) vis_cts invis_cts
844 -- always look at *visible* Origins before invisible ones
845 -- this is the whole point of isVisibleOrigin
846 = do { (ctxt', vis_cts') <- tryReporter ctxt r vis_cts
847 ; (ctxt'', invis_cts') <- tryReporter ctxt' r invis_cts
848 ; go ctxt'' rs vis_cts' invis_cts' }
849 -- Carry on with the rest, because we must make
850 -- deferred bindings for them if we have -fdefer-type-errors
851 -- But suppress their error messages
852
853 tryReporter :: ReportErrCtxt -> ReporterSpec -> [Ct] -> TcM (ReportErrCtxt, [Ct])
854 tryReporter ctxt (str, keep_me, suppress_after, reporter) cts
855 | null yeses = return (ctxt, cts)
856 | otherwise = do { traceTc "tryReporter{ " (text str <+> ppr yeses)
857 ; reporter ctxt yeses
858 ; let ctxt' = ctxt { cec_suppress = suppress_after || cec_suppress ctxt }
859 ; traceTc "tryReporter end }" (text str <+> ppr (cec_suppress ctxt) <+> ppr suppress_after)
860 ; return (ctxt', nos) }
861 where
862 (yeses, nos) = partition (\ct -> keep_me ct (classifyPredType (ctPred ct))) cts
863
864
865 pprArising :: CtOrigin -> SDoc
866 -- Used for the main, top-level error message
867 -- We've done special processing for TypeEq, KindEq, Given
868 pprArising (TypeEqOrigin {}) = empty
869 pprArising (KindEqOrigin {}) = empty
870 pprArising (GivenOrigin {}) = empty
871 pprArising orig = pprCtOrigin orig
872
873 -- Add the "arising from..." part to a message about bunch of dicts
874 addArising :: CtOrigin -> SDoc -> SDoc
875 addArising orig msg = hang msg 2 (pprArising orig)
876
877 pprWithArising :: [Ct] -> (CtLoc, SDoc)
878 -- Print something like
879 -- (Eq a) arising from a use of x at y
880 -- (Show a) arising from a use of p at q
881 -- Also return a location for the error message
882 -- Works for Wanted/Derived only
883 pprWithArising []
884 = panic "pprWithArising"
885 pprWithArising (ct:cts)
886 | null cts
887 = (loc, addArising (ctLocOrigin loc)
888 (pprTheta [ctPred ct]))
889 | otherwise
890 = (loc, vcat (map ppr_one (ct:cts)))
891 where
892 loc = ctLoc ct
893 ppr_one ct' = hang (parens (pprType (ctPred ct')))
894 2 (pprCtLoc (ctLoc ct'))
895
896 mkErrorMsgFromCt :: ReportErrCtxt -> Ct -> Report -> TcM ErrMsg
897 mkErrorMsgFromCt ctxt ct report
898 = mkErrorReport ctxt (ctLocEnv (ctLoc ct)) report
899
900 mkErrorReport :: ReportErrCtxt -> TcLclEnv -> Report -> TcM ErrMsg
901 mkErrorReport ctxt tcl_env (Report important relevant_bindings valid_subs)
902 = do { context <- mkErrInfo (cec_tidy ctxt) (tcl_ctxt tcl_env)
903 ; mkErrDocAt (RealSrcSpan (tcl_loc tcl_env))
904 (errDoc important [context] (relevant_bindings ++ valid_subs))
905 }
906
907 type UserGiven = Implication
908
909 getUserGivens :: ReportErrCtxt -> [UserGiven]
910 -- One item for each enclosing implication
911 getUserGivens (CEC {cec_encl = implics}) = getUserGivensFromImplics implics
912
913 getUserGivensFromImplics :: [Implication] -> [UserGiven]
914 getUserGivensFromImplics implics
915 = reverse (filterOut (null . ic_given) implics)
916
917 {-
918 Note [Always warn with -fdefer-type-errors]
919 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
920 When -fdefer-type-errors is on we warn about *all* type errors, even
921 if cec_suppress is on. This can lead to a lot more warnings than you
922 would get errors without -fdefer-type-errors, but if we suppress any of
923 them you might get a runtime error that wasn't warned about at compile
924 time.
925
926 This is an easy design choice to change; just flip the order of the
927 first two equations for maybeReportError
928
929 To be consistent, we should also report multiple warnings from a single
930 location in mkGroupReporter, when -fdefer-type-errors is on. But that
931 is perhaps a bit *over*-consistent! Again, an easy choice to change.
932
933 With #10283, you can now opt out of deferred type error warnings.
934
935 Note [Deferred errors for coercion holes]
936 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
937 Suppose we need to defer a type error where the destination for the evidence
938 is a coercion hole. We can't just put the error in the hole, because we can't
939 make an erroneous coercion. (Remember that coercions are erased for runtime.)
940 Instead, we invent a new EvVar, bind it to an error and then make a coercion
941 from that EvVar, filling the hole with that coercion. Because coercions'
942 types are unlifted, the error is guaranteed to be hit before we get to the
943 coercion.
944
945 Note [Do not report derived but soluble errors]
946 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
947 The wc_simples include Derived constraints that have not been solved,
948 but are not insoluble (in that case they'd be reported by 'report1').
949 We do not want to report these as errors:
950
951 * Superclass constraints. If we have an unsolved [W] Ord a, we'll also have
952 an unsolved [D] Eq a, and we do not want to report that; it's just noise.
953
954 * Functional dependencies. For givens, consider
955 class C a b | a -> b
956 data T a where
957 MkT :: C a d => [d] -> T a
958 f :: C a b => T a -> F Int
959 f (MkT xs) = length xs
960 Then we get a [D] b~d. But there *is* a legitimate call to
961 f, namely f (MkT [True]) :: T Bool, in which b=d. So we should
962 not reject the program.
963
964 For wanteds, something similar
965 data T a where
966 MkT :: C Int b => a -> b -> T a
967 g :: C Int c => c -> ()
968 f :: T a -> ()
969 f (MkT x y) = g x
970 Here we get [G] C Int b, [W] C Int a, hence [D] a~b.
971 But again f (MkT True True) is a legitimate call.
972
973 (We leave the Deriveds in wc_simple until reportErrors, so that we don't lose
974 derived superclasses between iterations of the solver.)
975
976 For functional dependencies, here is a real example,
977 stripped off from libraries/utf8-string/Codec/Binary/UTF8/Generic.hs
978
979 class C a b | a -> b
980 g :: C a b => a -> b -> ()
981 f :: C a b => a -> b -> ()
982 f xa xb =
983 let loop = g xa
984 in loop xb
985
986 We will first try to infer a type for loop, and we will succeed:
987 C a b' => b' -> ()
988 Subsequently, we will type check (loop xb) and all is good. But,
989 recall that we have to solve a final implication constraint:
990 C a b => (C a b' => .... cts from body of loop .... ))
991 And now we have a problem as we will generate an equality b ~ b' and fail to
992 solve it.
993
994
995 ************************************************************************
996 * *
997 Irreducible predicate errors
998 * *
999 ************************************************************************
1000 -}
1001
1002 mkIrredErr :: ReportErrCtxt -> [Ct] -> TcM ErrMsg
1003 mkIrredErr ctxt cts
1004 = do { (ctxt, binds_msg, ct1) <- relevantBindings True ctxt ct1
1005 ; let orig = ctOrigin ct1
1006 msg = couldNotDeduce (getUserGivens ctxt) (map ctPred cts, orig)
1007 ; mkErrorMsgFromCt ctxt ct1 $
1008 important msg `mappend` relevant_bindings binds_msg }
1009 where
1010 (ct1:_) = cts
1011
1012 ----------------
1013 mkHoleError :: ReportErrCtxt -> Ct -> TcM ErrMsg
1014 mkHoleError _ctxt ct@(CHoleCan { cc_hole = ExprHole (OutOfScope occ rdr_env0) })
1015 -- Out-of-scope variables, like 'a', where 'a' isn't bound; suggest possible
1016 -- in-scope variables in the message, and note inaccessible exact matches
1017 = do { dflags <- getDynFlags
1018 ; imp_info <- getImports
1019 ; let suggs_msg = unknownNameSuggestions dflags rdr_env0
1020 (tcl_rdr lcl_env) imp_info rdr
1021 ; rdr_env <- getGlobalRdrEnv
1022 ; splice_locs <- getTopLevelSpliceLocs
1023 ; let match_msgs = mk_match_msgs rdr_env splice_locs
1024 ; mkErrDocAt (RealSrcSpan err_loc) $
1025 errDoc [out_of_scope_msg] [] (match_msgs ++ [suggs_msg]) }
1026
1027 where
1028 rdr = mkRdrUnqual occ
1029 ct_loc = ctLoc ct
1030 lcl_env = ctLocEnv ct_loc
1031 err_loc = tcl_loc lcl_env
1032 hole_ty = ctEvPred (ctEvidence ct)
1033 boring_type = isTyVarTy hole_ty
1034
1035 out_of_scope_msg -- Print v :: ty only if the type has structure
1036 | boring_type = hang herald 2 (ppr occ)
1037 | otherwise = hang herald 2 (pp_with_type occ hole_ty)
1038
1039 herald | isDataOcc occ = text "Data constructor not in scope:"
1040 | otherwise = text "Variable not in scope:"
1041
1042 -- Indicate if the out-of-scope variable exactly (and unambiguously) matches
1043 -- a top-level binding in a later inter-splice group; see Note [OutOfScope
1044 -- exact matches]
1045 mk_match_msgs rdr_env splice_locs
1046 = let gres = filter isLocalGRE (lookupGlobalRdrEnv rdr_env occ)
1047 in case gres of
1048 [gre]
1049 | RealSrcSpan bind_loc <- greSrcSpan gre
1050 -- Find splice between the unbound variable and the match; use
1051 -- lookupLE, not lookupLT, since match could be in the splice
1052 , Just th_loc <- Set.lookupLE bind_loc splice_locs
1053 , err_loc < th_loc
1054 -> [mk_bind_scope_msg bind_loc th_loc]
1055 _ -> []
1056
1057 mk_bind_scope_msg bind_loc th_loc
1058 | is_th_bind
1059 = hang (quotes (ppr occ) <+> parens (text "splice on" <+> th_rng))
1060 2 (text "is not in scope before line" <+> int th_start_ln)
1061 | otherwise
1062 = hang (quotes (ppr occ) <+> bind_rng <+> text "is not in scope")
1063 2 (text "before the splice on" <+> th_rng)
1064 where
1065 bind_rng = parens (text "line" <+> int bind_ln)
1066 th_rng
1067 | th_start_ln == th_end_ln = single
1068 | otherwise = multi
1069 single = text "line" <+> int th_start_ln
1070 multi = text "lines" <+> int th_start_ln <> text "-" <> int th_end_ln
1071 bind_ln = srcSpanStartLine bind_loc
1072 th_start_ln = srcSpanStartLine th_loc
1073 th_end_ln = srcSpanEndLine th_loc
1074 is_th_bind = th_loc `containsSpan` bind_loc
1075
1076 mkHoleError ctxt ct@(CHoleCan { cc_hole = hole })
1077 -- Explicit holes, like "_" or "_f"
1078 = do { (ctxt, binds_msg, ct) <- relevantBindings False ctxt ct
1079 -- The 'False' means "don't filter the bindings"; see Trac #8191
1080
1081 ; show_hole_constraints <- goptM Opt_ShowHoleConstraints
1082 ; let constraints_msg
1083 | isExprHoleCt ct, show_hole_constraints
1084 = givenConstraintsMsg ctxt
1085 | otherwise = empty
1086
1087 ; sub_msg <- validSubstitutions ctxt ct
1088 ; mkErrorMsgFromCt ctxt ct $
1089 important hole_msg `mappend`
1090 relevant_bindings (binds_msg $$ constraints_msg) `mappend`
1091 valid_substitutions sub_msg}
1092
1093 where
1094 occ = holeOcc hole
1095 hole_ty = ctEvPred (ctEvidence ct)
1096 hole_kind = typeKind hole_ty
1097 tyvars = tyCoVarsOfTypeList hole_ty
1098
1099 hole_msg = case hole of
1100 ExprHole {} -> vcat [ hang (text "Found hole:")
1101 2 (pp_with_type occ hole_ty)
1102 , tyvars_msg, expr_hole_hint ]
1103 TypeHole {} -> vcat [ hang (text "Found type wildcard" <+>
1104 quotes (ppr occ))
1105 2 (text "standing for" <+>
1106 quotes pp_hole_type_with_kind)
1107 , tyvars_msg, type_hole_hint ]
1108
1109 pp_hole_type_with_kind
1110 | isLiftedTypeKind hole_kind = pprType hole_ty
1111 | otherwise = pprType hole_ty <+> dcolon <+> pprKind hole_kind
1112
1113 tyvars_msg = ppUnless (null tyvars) $
1114 text "Where:" <+> (vcat (map loc_msg other_tvs)
1115 $$ pprSkols ctxt skol_tvs)
1116 where
1117 (skol_tvs, other_tvs) = partition is_skol tyvars
1118 is_skol tv = isTcTyVar tv && isSkolemTyVar tv
1119 -- Coercion variables can be free in the
1120 -- hole, via kind casts
1121
1122 type_hole_hint
1123 | HoleError <- cec_type_holes ctxt
1124 = text "To use the inferred type, enable PartialTypeSignatures"
1125 | otherwise
1126 = empty
1127
1128 expr_hole_hint -- Give hint for, say, f x = _x
1129 | lengthFS (occNameFS occ) > 1 -- Don't give this hint for plain "_"
1130 = text "Or perhaps" <+> quotes (ppr occ)
1131 <+> text "is mis-spelled, or not in scope"
1132 | otherwise
1133 = empty
1134
1135 loc_msg tv
1136 | isTyVar tv
1137 = case tcTyVarDetails tv of
1138 MetaTv {} -> quotes (ppr tv) <+> text "is an ambiguous type variable"
1139 _ -> empty -- Skolems dealt with already
1140 | otherwise -- A coercion variable can be free in the hole type
1141 = sdocWithDynFlags $ \dflags ->
1142 if gopt Opt_PrintExplicitCoercions dflags
1143 then quotes (ppr tv) <+> text "is a coercion variable"
1144 else empty
1145
1146 mkHoleError _ ct = pprPanic "mkHoleError" (ppr ct)
1147
1148
1149 -- See Note [Valid substitutions include ...]
1150 validSubstitutions :: ReportErrCtxt -> Ct -> TcM SDoc
1151 validSubstitutions (CEC {cec_encl = implics}) ct | isExprHoleCt ct =
1152 do { rdr_env <- getGlobalRdrEnv
1153 ; dflags <- getDynFlags
1154 ; traceTc "findingValidSubstitutionsFor {" $ ppr wrapped_hole_ty
1155 ; (discards, substitutions) <-
1156 setTcLevel hole_lvl $
1157 go (maxValidSubstitutions dflags) $
1158 localsFirst $ globalRdrEnvElts rdr_env
1159 ; traceTc "}" empty
1160 ; return $ ppUnless (null substitutions) $
1161 hang (text "Valid substitutions include")
1162 2 (vcat (map (ppr_sub rdr_env) substitutions)
1163 $$ ppWhen discards subsDiscardMsg) }
1164 where
1165 -- We extract the type of the hole from the constraint.
1166 hole_ty :: TcPredType
1167 hole_ty = ctEvPred (ctEvidence ct)
1168 hole_loc = ctEvLoc $ ctEvidence ct
1169 hole_env = ctLocEnv $ hole_loc
1170 hole_lvl = ctLocLevel $ hole_loc
1171
1172
1173 -- For checking, we wrap the type of the hole with all the givens
1174 -- from all the implications in the context.
1175 wrapped_hole_ty :: TcSigmaType
1176 wrapped_hole_ty = foldl' wrapType hole_ty implics
1177
1178
1179 -- We rearrange the elements to make locals appear at the top of the list,
1180 -- since they're most likely to be relevant to the user
1181 localsFirst :: [GlobalRdrElt] -> [GlobalRdrElt]
1182 localsFirst elts = lcl ++ gbl
1183 where (lcl, gbl) = partition gre_lcl elts
1184
1185 is_id_bind :: TcBinder -> Bool
1186 is_id_bind (TcIdBndr {}) = True
1187 is_id_bind (TcIdBndr_ExpType {}) = True
1188 is_id_bind (TcTvBndr {}) = False
1189
1190 -- The set of relevant bindings. We use it to make sure we don't repeat
1191 -- ids from the relevant bindings again in the suggestions.
1192 relBindSet :: OccSet
1193 relBindSet = mkOccSet [ occName b | b <- tcl_bndrs hole_env
1194 , is_id_bind b ]
1195
1196 -- We skip elements that are already in the "Relevant Bindings Include"
1197 -- part of the error message, as given by the relBindSet.
1198 shouldBeSkipped :: GlobalRdrElt -> Bool
1199 shouldBeSkipped el = (occName $ gre_name el) `elemOccSet` relBindSet
1200
1201 -- For pretty printing, we look up the name and type of the substitution
1202 -- we found.
1203 ppr_sub :: GlobalRdrEnv -> Id -> SDoc
1204 ppr_sub rdr_env id = case lookupGRE_Name rdr_env (idName id) of
1205 Just elt -> sep [ idAndTy, nest 2 (parens $ pprNameProvenance elt)]
1206 _ -> idAndTy
1207 where name = idName id
1208 ty = varType id
1209 idAndTy = (pprPrefixOcc name <+> dcolon <+> pprType ty)
1210
1211 -- The real work happens here, where we invoke the typechecker to check
1212 -- whether we the given type fits into the hole!
1213 substituteable :: Id -> TcM Bool
1214 substituteable id = wrapped_hole_ty `tcSubsumes` ty
1215 where ty = varType id
1216
1217 -- Kickoff the checking of the elements. The first argument
1218 -- is a counter, so that we stop after finding functions up to the
1219 -- limit the user gives us.
1220 go :: Maybe Int -> [GlobalRdrElt] -> TcM (Bool, [Id])
1221 go = go_ []
1222
1223 -- We iterate over the elements, checking each one in turn. If we've
1224 -- already found -fmax-valid-substitutions=n elements, we look no further.
1225 go_ :: [Id] -> Maybe Int -> [GlobalRdrElt] -> TcM (Bool, [Id])
1226 go_ subs _ [] = return (False, reverse subs)
1227 go_ subs (Just 0) _ = return (True, reverse subs)
1228 go_ subs maxleft (el:elts) =
1229 if shouldBeSkipped el then discard_it
1230 else do { maybeId <- tcLookupIdMaybe (gre_name el)
1231 ; case maybeId of
1232 Just id -> do { canSub <- substituteable id
1233 ; if canSub then (keep_it id) else discard_it }
1234 _ -> discard_it
1235 }
1236 where discard_it = go_ subs maxleft elts
1237 keep_it id = go_ (id:subs) ((\n -> n - 1) <$> maxleft) elts
1238
1239
1240 -- We don't (as of yet) handle holes in types, only in expressions.
1241 validSubstitutions _ _ = return empty
1242
1243
1244 -- See Note [Constraints include ...]
1245 givenConstraintsMsg :: ReportErrCtxt -> SDoc
1246 givenConstraintsMsg ctxt =
1247 let constraints :: [(Type, RealSrcSpan)]
1248 constraints =
1249 do { Implic{ ic_given = given, ic_env = env } <- cec_encl ctxt
1250 ; constraint <- given
1251 ; return (varType constraint, tcl_loc env) }
1252
1253 pprConstraint (constraint, loc) =
1254 ppr constraint <+> nest 2 (parens (text "from" <+> ppr loc))
1255
1256 in ppUnless (null constraints) $
1257 hang (text "Constraints include")
1258 2 (vcat $ map pprConstraint constraints)
1259
1260 pp_with_type :: OccName -> Type -> SDoc
1261 pp_with_type occ ty = hang (pprPrefixOcc occ) 2 (dcolon <+> pprType ty)
1262
1263 ----------------
1264 mkIPErr :: ReportErrCtxt -> [Ct] -> TcM ErrMsg
1265 mkIPErr ctxt cts
1266 = do { (ctxt, binds_msg, ct1) <- relevantBindings True ctxt ct1
1267 ; let orig = ctOrigin ct1
1268 preds = map ctPred cts
1269 givens = getUserGivens ctxt
1270 msg | null givens
1271 = addArising orig $
1272 sep [ text "Unbound implicit parameter" <> plural cts
1273 , nest 2 (pprParendTheta preds) ]
1274 | otherwise
1275 = couldNotDeduce givens (preds, orig)
1276
1277 ; mkErrorMsgFromCt ctxt ct1 $
1278 important msg `mappend` relevant_bindings binds_msg }
1279 where
1280 (ct1:_) = cts
1281
1282 {-
1283 Note [Valid substitutions include ...]
1284 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1285 `validSubstitutions` returns the "Valid substitutions include ..." message.
1286 For example, look at the following definitions in a file called test.hs:
1287
1288 import Data.List (inits)
1289
1290 f :: [String]
1291 f = _ "hello, world"
1292
1293 The hole in `f` would generate the message:
1294
1295 Valid substitutions include
1296 inits :: forall a. [a] -> [[a]]
1297 (imported from ‘Data.List’ at tp.hs:3:19-23
1298 (and originally defined in ‘base-4.10.0.0:Data.OldList’))
1299 fail :: forall (m :: * -> *). Monad m => forall a. String -> m a
1300 (imported from ‘Prelude’ at tp.hs:1:8-9
1301 (and originally defined in ‘GHC.Base’))
1302 mempty :: forall a. Monoid a => a
1303 (imported from ‘Prelude’ at tp.hs:1:8-9
1304 (and originally defined in ‘GHC.Base’))
1305 pure :: forall (f :: * -> *). Applicative f => forall a. a -> f a
1306 (imported from ‘Prelude’ at tp.hs:1:8-9
1307 (and originally defined in ‘GHC.Base’))
1308 return :: forall (m :: * -> *). Monad m => forall a. a -> m a
1309 (imported from ‘Prelude’ at tp.hs:1:8-9
1310 (and originally defined in ‘GHC.Base’))
1311 read :: forall a. Read a => String -> a
1312 (imported from ‘Prelude’ at tp.hs:1:8-9
1313 (and originally defined in ‘Text.Read’))
1314 lines :: String -> [String]
1315 (imported from ‘Prelude’ at tp.hs:1:8-9
1316 (and originally defined in ‘base-4.10.0.0:Data.OldList’))
1317 words :: String -> [String]
1318 (imported from ‘Prelude’ at tp.hs:1:8-9
1319 (and originally defined in ‘base-4.10.0.0:Data.OldList’))
1320 error :: forall (a :: TYPE r). GHC.Stack.Types.HasCallStack => [Char] -> a
1321 (imported from ‘Prelude’ at tp.hs:1:8-9
1322 (and originally defined in ‘GHC.Err’))
1323 errorWithoutStackTrace :: forall (a :: TYPE r). [Char] -> a
1324 (imported from ‘Prelude’ at tp.hs:1:8-9
1325 (and originally defined in ‘GHC.Err’))
1326 undefined :: forall (a :: TYPE r). GHC.Stack.Types.HasCallStack => a
1327 (imported from ‘Prelude’ at tp.hs:1:8-9
1328 (and originally defined in ‘GHC.Err’))
1329 repeat :: forall a. a -> [a]
1330 (imported from ‘Prelude’ at tp.hs:1:8-9
1331 (and originally defined in ‘GHC.List’))
1332
1333 Valid substitutions are found by checking top level ids in scope, and checking
1334 whether their type subsumes the type of the hole. We remove ids that are
1335 local bindings, since they are already included in the relevant bindings
1336 section of the hole error message.
1337
1338 Note [Constraints include ...]
1339 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1340 'givenConstraintsMsg' returns the "Constraints include ..." message enabled by
1341 -fshow-hole-constraints. For example, the following hole:
1342
1343 foo :: (Eq a, Show a) => a -> String
1344 foo x = _
1345
1346 would generate the message:
1347
1348 Constraints include
1349 Eq a (from foo.hs:1:1-36)
1350 Show a (from foo.hs:1:1-36)
1351
1352 Constraints are displayed in order from innermost (closest to the hole) to
1353 outermost. There's currently no filtering or elimination of duplicates.
1354
1355
1356 Note [OutOfScope exact matches]
1357 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1358 When constructing an out-of-scope error message, we not only generate a list of
1359 possible in-scope alternatives but also search for an exact, unambiguous match
1360 in a later inter-splice group. If we find such a match, we report its presence
1361 (and indirectly, its scope) in the message. For example, if a module A contains
1362 the following declarations,
1363
1364 foo :: Int
1365 foo = x
1366
1367 $(return []) -- Empty top-level splice
1368
1369 x :: Int
1370 x = 23
1371
1372 we will issue an error similar to
1373
1374 A.hs:6:7: error:
1375 • Variable not in scope: x :: Int
1376 • ‘x’ (line 11) is not in scope before the splice on line 8
1377
1378 By providing information about the match, we hope to clarify why declaring a
1379 variable after a top-level splice but using it before the splice generates an
1380 out-of-scope error (a situation which is often confusing to Haskell newcomers).
1381
1382 Note that if we find multiple exact matches to the out-of-scope variable
1383 (hereafter referred to as x), we report nothing. Such matches can only be
1384 duplicate record fields, as the presence of any other duplicate top-level
1385 declarations would have already halted compilation. But if these record fields
1386 are declared in a later inter-splice group, then so too are their corresponding
1387 types. Thus, these types must not occur in the inter-splice group containing x
1388 (any unknown types would have already been reported), and so the matches to the
1389 record fields are most likely coincidental.
1390
1391 One oddity of the exact match portion of the error message is that we specify
1392 where the match to x is NOT in scope. Why not simply state where the match IS
1393 in scope? It most cases, this would be just as easy and perhaps a little
1394 clearer for the user. But now consider the following example:
1395
1396 {-# LANGUAGE TemplateHaskell #-}
1397
1398 module A where
1399
1400 import Language.Haskell.TH
1401 import Language.Haskell.TH.Syntax
1402
1403 foo = x
1404
1405 $(do -------------------------------------------------
1406 ds <- [d| ok1 = x
1407 |]
1408 addTopDecls ds
1409 return [])
1410
1411 bar = $(do
1412 ds <- [d| x = 23
1413 ok2 = x
1414 |]
1415 addTopDecls ds
1416 litE $ stringL "hello")
1417
1418 $(return []) -----------------------------------------
1419
1420 ok3 = x
1421
1422 Here, x is out-of-scope in the declaration of foo, and so we report
1423
1424 A.hs:8:7: error:
1425 • Variable not in scope: x
1426 • ‘x’ (line 16) is not in scope before the splice on lines 10-14
1427
1428 If we instead reported where x IS in scope, we would have to state that it is in
1429 scope after the second top-level splice as well as among all the top-level
1430 declarations added by both calls to addTopDecls. But doing so would not only
1431 add complexity to the code but also overwhelm the user with unneeded
1432 information.
1433
1434 The logic which determines where x is not in scope is straightforward: it simply
1435 finds the last top-level splice which occurs after x but before (or at) the
1436 match to x (assuming such a splice exists). In most cases, the check that the
1437 splice occurs after x acts only as a sanity check. For example, when the match
1438 to x is a non-TH top-level declaration and a splice S occurs before the match,
1439 then x must precede S; otherwise, it would be in scope. But when dealing with
1440 addTopDecls, this check serves a practical purpose. Consider the following
1441 declarations:
1442
1443 $(do
1444 ds <- [d| ok = x
1445 x = 23
1446 |]
1447 addTopDecls ds
1448 return [])
1449
1450 foo = x
1451
1452 In this case, x is not in scope in the declaration for foo. Since x occurs
1453 AFTER the splice containing the match, the logic does not find any splices after
1454 x but before or at its match, and so we report nothing about x's scope. If we
1455 had not checked whether x occurs before the splice, we would have instead
1456 reported that x is not in scope before the splice. While correct, such an error
1457 message is more likely to confuse than to enlighten.
1458 -}
1459
1460 {-
1461 ************************************************************************
1462 * *
1463 Equality errors
1464 * *
1465 ************************************************************************
1466
1467 Note [Inaccessible code]
1468 ~~~~~~~~~~~~~~~~~~~~~~~~
1469 Consider
1470 data T a where
1471 T1 :: T a
1472 T2 :: T Bool
1473
1474 f :: (a ~ Int) => T a -> Int
1475 f T1 = 3
1476 f T2 = 4 -- Unreachable code
1477
1478 Here the second equation is unreachable. The original constraint
1479 (a~Int) from the signature gets rewritten by the pattern-match to
1480 (Bool~Int), so the danger is that we report the error as coming from
1481 the *signature* (Trac #7293). So, for Given errors we replace the
1482 env (and hence src-loc) on its CtLoc with that from the immediately
1483 enclosing implication.
1484
1485 Note [Error messages for untouchables]
1486 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1487 Consider (Trac #9109)
1488 data G a where { GBool :: G Bool }
1489 foo x = case x of GBool -> True
1490
1491 Here we can't solve (t ~ Bool), where t is the untouchable result
1492 meta-var 't', because of the (a ~ Bool) from the pattern match.
1493 So we infer the type
1494 f :: forall a t. G a -> t
1495 making the meta-var 't' into a skolem. So when we come to report
1496 the unsolved (t ~ Bool), t won't look like an untouchable meta-var
1497 any more. So we don't assert that it is.
1498 -}
1499
1500 -- Don't have multiple equality errors from the same location
1501 -- E.g. (Int,Bool) ~ (Bool,Int) one error will do!
1502 mkEqErr :: ReportErrCtxt -> [Ct] -> TcM ErrMsg
1503 mkEqErr ctxt (ct:_) = mkEqErr1 ctxt ct
1504 mkEqErr _ [] = panic "mkEqErr"
1505
1506 mkEqErr1 :: ReportErrCtxt -> Ct -> TcM ErrMsg
1507 mkEqErr1 ctxt ct -- Wanted or derived;
1508 -- givens handled in mkGivenErrorReporter
1509 = do { (ctxt, binds_msg, ct) <- relevantBindings True ctxt ct
1510 ; rdr_env <- getGlobalRdrEnv
1511 ; fam_envs <- tcGetFamInstEnvs
1512 ; exp_syns <- goptM Opt_PrintExpandedSynonyms
1513 ; let (keep_going, is_oriented, wanted_msg)
1514 = mk_wanted_extra (ctLoc ct) exp_syns
1515 coercible_msg = case ctEqRel ct of
1516 NomEq -> empty
1517 ReprEq -> mkCoercibleExplanation rdr_env fam_envs ty1 ty2
1518 ; dflags <- getDynFlags
1519 ; traceTc "mkEqErr1" (ppr ct $$ pprCtOrigin (ctOrigin ct) $$ ppr keep_going)
1520 ; let report = mconcat [important wanted_msg, important coercible_msg,
1521 relevant_bindings binds_msg]
1522 ; if keep_going
1523 then mkEqErr_help dflags ctxt report ct is_oriented ty1 ty2
1524 else mkErrorMsgFromCt ctxt ct report }
1525 where
1526 (ty1, ty2) = getEqPredTys (ctPred ct)
1527
1528 -- If the types in the error message are the same as the types
1529 -- we are unifying, don't add the extra expected/actual message
1530 mk_wanted_extra :: CtLoc -> Bool -> (Bool, Maybe SwapFlag, SDoc)
1531 mk_wanted_extra loc expandSyns
1532 = case ctLocOrigin loc of
1533 orig@TypeEqOrigin {} -> mkExpectedActualMsg ty1 ty2 orig
1534 t_or_k expandSyns
1535 where
1536 t_or_k = ctLocTypeOrKind_maybe loc
1537
1538 KindEqOrigin cty1 mb_cty2 sub_o sub_t_or_k
1539 -> (True, Nothing, msg1 $$ msg2)
1540 where
1541 sub_what = case sub_t_or_k of Just KindLevel -> text "kinds"
1542 _ -> text "types"
1543 msg1 = sdocWithDynFlags $ \dflags ->
1544 case mb_cty2 of
1545 Just cty2
1546 | gopt Opt_PrintExplicitCoercions dflags
1547 || not (cty1 `pickyEqType` cty2)
1548 -> hang (text "When matching" <+> sub_what)
1549 2 (vcat [ ppr cty1 <+> dcolon <+>
1550 ppr (typeKind cty1)
1551 , ppr cty2 <+> dcolon <+>
1552 ppr (typeKind cty2) ])
1553 _ -> text "When matching the kind of" <+> quotes (ppr cty1)
1554 msg2 = case sub_o of
1555 TypeEqOrigin {}
1556 | Just cty2 <- mb_cty2 ->
1557 thdOf3 (mkExpectedActualMsg cty1 cty2 sub_o sub_t_or_k
1558 expandSyns)
1559 _ -> empty
1560 _ -> (True, Nothing, empty)
1561
1562 -- | This function tries to reconstruct why a "Coercible ty1 ty2" constraint
1563 -- is left over.
1564 mkCoercibleExplanation :: GlobalRdrEnv -> FamInstEnvs
1565 -> TcType -> TcType -> SDoc
1566 mkCoercibleExplanation rdr_env fam_envs ty1 ty2
1567 | Just (tc, tys) <- tcSplitTyConApp_maybe ty1
1568 , (rep_tc, _, _) <- tcLookupDataFamInst fam_envs tc tys
1569 , Just msg <- coercible_msg_for_tycon rep_tc
1570 = msg
1571 | Just (tc, tys) <- splitTyConApp_maybe ty2
1572 , (rep_tc, _, _) <- tcLookupDataFamInst fam_envs tc tys
1573 , Just msg <- coercible_msg_for_tycon rep_tc
1574 = msg
1575 | Just (s1, _) <- tcSplitAppTy_maybe ty1
1576 , Just (s2, _) <- tcSplitAppTy_maybe ty2
1577 , s1 `eqType` s2
1578 , has_unknown_roles s1
1579 = hang (text "NB: We cannot know what roles the parameters to" <+>
1580 quotes (ppr s1) <+> text "have;")
1581 2 (text "we must assume that the role is nominal")
1582 | otherwise
1583 = empty
1584 where
1585 coercible_msg_for_tycon tc
1586 | isAbstractTyCon tc
1587 = Just $ hsep [ text "NB: The type constructor"
1588 , quotes (pprSourceTyCon tc)
1589 , text "is abstract" ]
1590 | isNewTyCon tc
1591 , [data_con] <- tyConDataCons tc
1592 , let dc_name = dataConName data_con
1593 , isNothing (lookupGRE_Name rdr_env dc_name)
1594 = Just $ hang (text "The data constructor" <+> quotes (ppr dc_name))
1595 2 (sep [ text "of newtype" <+> quotes (pprSourceTyCon tc)
1596 , text "is not in scope" ])
1597 | otherwise = Nothing
1598
1599 has_unknown_roles ty
1600 | Just (tc, tys) <- tcSplitTyConApp_maybe ty
1601 = tys `lengthAtLeast` tyConArity tc -- oversaturated tycon
1602 | Just (s, _) <- tcSplitAppTy_maybe ty
1603 = has_unknown_roles s
1604 | isTyVarTy ty
1605 = True
1606 | otherwise
1607 = False
1608
1609 {-
1610 -- | Make a listing of role signatures for all the parameterised tycons
1611 -- used in the provided types
1612
1613
1614 -- SLPJ Jun 15: I could not convince myself that these hints were really
1615 -- useful. Maybe they are, but I think we need more work to make them
1616 -- actually helpful.
1617 mkRoleSigs :: Type -> Type -> SDoc
1618 mkRoleSigs ty1 ty2
1619 = ppUnless (null role_sigs) $
1620 hang (text "Relevant role signatures:")
1621 2 (vcat role_sigs)
1622 where
1623 tcs = nameEnvElts $ tyConsOfType ty1 `plusNameEnv` tyConsOfType ty2
1624 role_sigs = mapMaybe ppr_role_sig tcs
1625
1626 ppr_role_sig tc
1627 | null roles -- if there are no parameters, don't bother printing
1628 = Nothing
1629 | isBuiltInSyntax (tyConName tc) -- don't print roles for (->), etc.
1630 = Nothing
1631 | otherwise
1632 = Just $ hsep $ [text "type role", ppr tc] ++ map ppr roles
1633 where
1634 roles = tyConRoles tc
1635 -}
1636
1637 mkEqErr_help :: DynFlags -> ReportErrCtxt -> Report
1638 -> Ct
1639 -> Maybe SwapFlag -- Nothing <=> not sure
1640 -> TcType -> TcType -> TcM ErrMsg
1641 mkEqErr_help dflags ctxt report ct oriented ty1 ty2
1642 | Just (tv1, co1) <- tcGetCastedTyVar_maybe ty1
1643 = mkTyVarEqErr dflags ctxt report ct oriented tv1 co1 ty2
1644 | Just (tv2, co2) <- tcGetCastedTyVar_maybe ty2
1645 = mkTyVarEqErr dflags ctxt report ct swapped tv2 co2 ty1
1646 | otherwise
1647 = reportEqErr ctxt report ct oriented ty1 ty2
1648 where
1649 swapped = fmap flipSwap oriented
1650
1651 reportEqErr :: ReportErrCtxt -> Report
1652 -> Ct
1653 -> Maybe SwapFlag -- Nothing <=> not sure
1654 -> TcType -> TcType -> TcM ErrMsg
1655 reportEqErr ctxt report ct oriented ty1 ty2
1656 = mkErrorMsgFromCt ctxt ct (mconcat [misMatch, report, eqInfo])
1657 where misMatch = important $ misMatchOrCND ctxt ct oriented ty1 ty2
1658 eqInfo = important $ mkEqInfoMsg ct ty1 ty2
1659
1660 mkTyVarEqErr, mkTyVarEqErr'
1661 :: DynFlags -> ReportErrCtxt -> Report -> Ct
1662 -> Maybe SwapFlag -> TcTyVar -> TcCoercionN -> TcType -> TcM ErrMsg
1663 -- tv1 and ty2 are already tidied
1664 mkTyVarEqErr dflags ctxt report ct oriented tv1 co1 ty2
1665 = do { traceTc "mkTyVarEqErr" (ppr ct $$ ppr tv1 $$ ppr co1 $$ ppr ty2)
1666 ; mkTyVarEqErr' dflags ctxt report ct oriented tv1 co1 ty2 }
1667
1668 mkTyVarEqErr' dflags ctxt report ct oriented tv1 co1 ty2
1669 | not insoluble_occurs_check -- See Note [Occurs check wins]
1670 , isUserSkolem ctxt tv1 -- ty2 won't be a meta-tyvar, or else the thing would
1671 -- be oriented the other way round;
1672 -- see TcCanonical.canEqTyVarTyVar
1673 || isSigTyVar tv1 && not (isTyVarTy ty2)
1674 || ctEqRel ct == ReprEq
1675 -- the cases below don't really apply to ReprEq (except occurs check)
1676 = mkErrorMsgFromCt ctxt ct $ mconcat
1677 [ important $ misMatchOrCND ctxt ct oriented ty1 ty2
1678 , important $ extraTyVarEqInfo ctxt tv1 ty2
1679 , report
1680 ]
1681
1682 | OC_Occurs <- occ_check_expand
1683 -- We report an "occurs check" even for a ~ F t a, where F is a type
1684 -- function; it's not insoluble (because in principle F could reduce)
1685 -- but we have certainly been unable to solve it
1686 -- See Note [Occurs check error] in TcCanonical
1687 = do { let main_msg = addArising (ctOrigin ct) $
1688 hang (text "Occurs check: cannot construct the infinite" <+> what <> colon)
1689 2 (sep [ppr ty1, char '~', ppr ty2])
1690
1691 extra2 = important $ mkEqInfoMsg ct ty1 ty2
1692
1693 interesting_tyvars = filter (not . noFreeVarsOfType . tyVarKind) $
1694 filter isTyVar $
1695 fvVarList $
1696 tyCoFVsOfType ty1 `unionFV` tyCoFVsOfType ty2
1697 extra3 = relevant_bindings $
1698 ppWhen (not (null interesting_tyvars)) $
1699 hang (text "Type variable kinds:") 2 $
1700 vcat (map (tyvar_binding . tidyTyVarOcc (cec_tidy ctxt))
1701 interesting_tyvars)
1702
1703 tyvar_binding tv = ppr tv <+> dcolon <+> ppr (tyVarKind tv)
1704 ; mkErrorMsgFromCt ctxt ct $
1705 mconcat [important main_msg, extra2, extra3, report] }
1706
1707 | OC_Bad <- occ_check_expand
1708 = do { let msg = vcat [ text "Cannot instantiate unification variable"
1709 <+> quotes (ppr tv1)
1710 , hang (text "with a" <+> what <+> text "involving foralls:") 2 (ppr ty2)
1711 , nest 2 (text "GHC doesn't yet support impredicative polymorphism") ]
1712 -- Unlike the other reports, this discards the old 'report_important'
1713 -- instead of augmenting it. This is because the details are not likely
1714 -- to be helpful since this is just an unimplemented feature.
1715 ; mkErrorMsgFromCt ctxt ct $ report { report_important = [msg] } }
1716
1717 -- check for heterogeneous equality next; see Note [Equalities with incompatible kinds]
1718 -- in TcCanonical
1719 | not (k1 `tcEqType` k2)
1720 = do { let main_msg = addArising (ctOrigin ct) $
1721 vcat [ hang (text "Kind mismatch: cannot unify" <+>
1722 parens (ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1)) <+>
1723 text "with:")
1724 2 (sep [ppr ty2, dcolon, ppr k2])
1725 , text "Their kinds differ." ]
1726 cast_msg
1727 | isTcReflexiveCo co1 = empty
1728 | otherwise = text "NB:" <+> ppr tv1 <+>
1729 text "was casted to have kind" <+>
1730 quotes (ppr k1)
1731
1732 ; mkErrorMsgFromCt ctxt ct (mconcat [important main_msg, important cast_msg, report]) }
1733
1734 -- If the immediately-enclosing implication has 'tv' a skolem, and
1735 -- we know by now its an InferSkol kind of skolem, then presumably
1736 -- it started life as a SigTv, else it'd have been unified, given
1737 -- that there's no occurs-check or forall problem
1738 | (implic:_) <- cec_encl ctxt
1739 , Implic { ic_skols = skols } <- implic
1740 , tv1 `elem` skols
1741 = mkErrorMsgFromCt ctxt ct $ mconcat
1742 [ important $ misMatchMsg ct oriented ty1 ty2
1743 , important $ extraTyVarEqInfo ctxt tv1 ty2
1744 , report
1745 ]
1746
1747 -- Check for skolem escape
1748 | (implic:_) <- cec_encl ctxt -- Get the innermost context
1749 , Implic { ic_env = env, ic_skols = skols, ic_info = skol_info } <- implic
1750 , let esc_skols = filter (`elemVarSet` (tyCoVarsOfType ty2)) skols
1751 , not (null esc_skols)
1752 = do { let msg = important $ misMatchMsg ct oriented ty1 ty2
1753 esc_doc = sep [ text "because" <+> what <+> text "variable" <> plural esc_skols
1754 <+> pprQuotedList esc_skols
1755 , text "would escape" <+>
1756 if isSingleton esc_skols then text "its scope"
1757 else text "their scope" ]
1758 tv_extra = important $
1759 vcat [ nest 2 $ esc_doc
1760 , sep [ (if isSingleton esc_skols
1761 then text "This (rigid, skolem)" <+>
1762 what <+> text "variable is"
1763 else text "These (rigid, skolem)" <+>
1764 what <+> text "variables are")
1765 <+> text "bound by"
1766 , nest 2 $ ppr skol_info
1767 , nest 2 $ text "at" <+> ppr (tcl_loc env) ] ]
1768 ; mkErrorMsgFromCt ctxt ct (mconcat [msg, tv_extra, report]) }
1769
1770 -- Nastiest case: attempt to unify an untouchable variable
1771 -- So tv is a meta tyvar (or started that way before we
1772 -- generalised it). So presumably it is an *untouchable*
1773 -- meta tyvar or a SigTv, else it'd have been unified
1774 -- See Note [Error messages for untouchables]
1775 | (implic:_) <- cec_encl ctxt -- Get the innermost context
1776 , Implic { ic_env = env, ic_given = given
1777 , ic_tclvl = lvl, ic_info = skol_info } <- implic
1778 = ASSERT2( not (isTouchableMetaTyVar lvl tv1)
1779 , ppr tv1 $$ ppr lvl ) -- See Note [Error messages for untouchables]
1780 do { let msg = important $ misMatchMsg ct oriented ty1 ty2
1781 tclvl_extra = important $
1782 nest 2 $
1783 sep [ quotes (ppr tv1) <+> text "is untouchable"
1784 , nest 2 $ text "inside the constraints:" <+> pprEvVarTheta given
1785 , nest 2 $ text "bound by" <+> ppr skol_info
1786 , nest 2 $ text "at" <+> ppr (tcl_loc env) ]
1787 tv_extra = important $ extraTyVarEqInfo ctxt tv1 ty2
1788 add_sig = important $ suggestAddSig ctxt ty1 ty2
1789 ; mkErrorMsgFromCt ctxt ct $ mconcat
1790 [msg, tclvl_extra, tv_extra, add_sig, report] }
1791
1792 | otherwise
1793 = reportEqErr ctxt report ct oriented (mkTyVarTy tv1) ty2
1794 -- This *can* happen (Trac #6123, and test T2627b)
1795 -- Consider an ambiguous top-level constraint (a ~ F a)
1796 -- Not an occurs check, because F is a type function.
1797 where
1798 Pair _ k1 = tcCoercionKind co1
1799 k2 = typeKind ty2
1800
1801 ty1 = mkTyVarTy tv1
1802 occ_check_expand = occCheckForErrors dflags tv1 ty2
1803 insoluble_occurs_check = isInsolubleOccursCheck (ctEqRel ct) tv1 ty2
1804
1805 what = case ctLocTypeOrKind_maybe (ctLoc ct) of
1806 Just KindLevel -> text "kind"
1807 _ -> text "type"
1808
1809 mkEqInfoMsg :: Ct -> TcType -> TcType -> SDoc
1810 -- Report (a) ambiguity if either side is a type function application
1811 -- e.g. F a0 ~ Int
1812 -- (b) warning about injectivity if both sides are the same
1813 -- type function application F a ~ F b
1814 -- See Note [Non-injective type functions]
1815 -- (c) warning about -fprint-explicit-kinds if that might be helpful
1816 mkEqInfoMsg ct ty1 ty2
1817 = tyfun_msg $$ ambig_msg $$ invis_msg
1818 where
1819 mb_fun1 = isTyFun_maybe ty1
1820 mb_fun2 = isTyFun_maybe ty2
1821
1822 ambig_msg | isJust mb_fun1 || isJust mb_fun2
1823 = snd (mkAmbigMsg False ct)
1824 | otherwise = empty
1825
1826 -- better to check the exp/act types in the CtOrigin than the actual
1827 -- mismatched types for suggestion about -fprint-explicit-kinds
1828 (act_ty, exp_ty) = case ctOrigin ct of
1829 TypeEqOrigin { uo_actual = act
1830 , uo_expected = exp } -> (act, exp)
1831 _ -> (ty1, ty2)
1832
1833 invis_msg | Just vis <- tcEqTypeVis act_ty exp_ty
1834 , not vis
1835 = ppSuggestExplicitKinds
1836 | otherwise
1837 = empty
1838
1839 tyfun_msg | Just tc1 <- mb_fun1
1840 , Just tc2 <- mb_fun2
1841 , tc1 == tc2
1842 , not (isInjectiveTyCon tc1 Nominal)
1843 = text "NB:" <+> quotes (ppr tc1)
1844 <+> text "is a non-injective type family"
1845 | otherwise = empty
1846
1847 isUserSkolem :: ReportErrCtxt -> TcTyVar -> Bool
1848 -- See Note [Reporting occurs-check errors]
1849 isUserSkolem ctxt tv
1850 = isSkolemTyVar tv && any is_user_skol_tv (cec_encl ctxt)
1851 where
1852 is_user_skol_tv (Implic { ic_skols = sks, ic_info = skol_info })
1853 = tv `elem` sks && is_user_skol_info skol_info
1854
1855 is_user_skol_info (InferSkol {}) = False
1856 is_user_skol_info _ = True
1857
1858 misMatchOrCND :: ReportErrCtxt -> Ct
1859 -> Maybe SwapFlag -> TcType -> TcType -> SDoc
1860 -- If oriented then ty1 is actual, ty2 is expected
1861 misMatchOrCND ctxt ct oriented ty1 ty2
1862 | null givens ||
1863 (isRigidTy ty1 && isRigidTy ty2) ||
1864 isGivenCt ct
1865 -- If the equality is unconditionally insoluble
1866 -- or there is no context, don't report the context
1867 = misMatchMsg ct oriented ty1 ty2
1868 | otherwise
1869 = couldNotDeduce givens ([eq_pred], orig)
1870 where
1871 ev = ctEvidence ct
1872 eq_pred = ctEvPred ev
1873 orig = ctEvOrigin ev
1874 givens = [ given | given <- getUserGivens ctxt, not (ic_no_eqs given)]
1875 -- Keep only UserGivens that have some equalities
1876
1877 couldNotDeduce :: [UserGiven] -> (ThetaType, CtOrigin) -> SDoc
1878 couldNotDeduce givens (wanteds, orig)
1879 = vcat [ addArising orig (text "Could not deduce:" <+> pprTheta wanteds)
1880 , vcat (pp_givens givens)]
1881
1882 pp_givens :: [UserGiven] -> [SDoc]
1883 pp_givens givens
1884 = case givens of
1885 [] -> []
1886 (g:gs) -> ppr_given (text "from the context:") g
1887 : map (ppr_given (text "or from:")) gs
1888 where
1889 ppr_given herald (Implic { ic_given = gs, ic_info = skol_info
1890 , ic_env = env })
1891 = hang (herald <+> pprEvVarTheta gs)
1892 2 (sep [ text "bound by" <+> ppr skol_info
1893 , text "at" <+> ppr (tcl_loc env) ])
1894
1895 extraTyVarEqInfo :: ReportErrCtxt -> TcTyVar -> TcType -> SDoc
1896 -- Add on extra info about skolem constants
1897 -- NB: The types themselves are already tidied
1898 extraTyVarEqInfo ctxt tv1 ty2
1899 = extraTyVarInfo ctxt tv1 $$ ty_extra ty2
1900 where
1901 ty_extra ty = case tcGetTyVar_maybe ty of
1902 Just tv -> extraTyVarInfo ctxt tv
1903 Nothing -> empty
1904
1905 extraTyVarInfo :: ReportErrCtxt -> TcTyVar -> SDoc
1906 extraTyVarInfo ctxt tv
1907 = ASSERT2( isTyVar tv, ppr tv )
1908 case tcTyVarDetails tv of
1909 SkolemTv {} -> pprSkols ctxt [tv]
1910 RuntimeUnk {} -> quotes (ppr tv) <+> text "is an interactive-debugger skolem"
1911 MetaTv {} -> empty
1912
1913 suggestAddSig :: ReportErrCtxt -> TcType -> TcType -> SDoc
1914 -- See Note [Suggest adding a type signature]
1915 suggestAddSig ctxt ty1 ty2
1916 | null inferred_bndrs
1917 = empty
1918 | [bndr] <- inferred_bndrs
1919 = text "Possible fix: add a type signature for" <+> quotes (ppr bndr)
1920 | otherwise
1921 = text "Possible fix: add type signatures for some or all of" <+> (ppr inferred_bndrs)
1922 where
1923 inferred_bndrs = nub (get_inf ty1 ++ get_inf ty2)
1924 get_inf ty | Just tv <- tcGetTyVar_maybe ty
1925 , isSkolemTyVar tv
1926 , (implic, _) : _ <- getSkolemInfo (cec_encl ctxt) [tv]
1927 , InferSkol prs <- ic_info implic
1928 = map fst prs
1929 | otherwise
1930 = []
1931
1932 --------------------
1933 misMatchMsg :: Ct -> Maybe SwapFlag -> TcType -> TcType -> SDoc
1934 -- Types are already tidy
1935 -- If oriented then ty1 is actual, ty2 is expected
1936 misMatchMsg ct oriented ty1 ty2
1937 | Just NotSwapped <- oriented
1938 = misMatchMsg ct (Just IsSwapped) ty2 ty1
1939
1940 -- These next two cases are when we're about to report, e.g., that
1941 -- 'LiftedRep doesn't match 'VoidRep. Much better just to say
1942 -- lifted vs. unlifted
1943 | Just (tc1, []) <- splitTyConApp_maybe ty1
1944 , tc1 `hasKey` liftedRepDataConKey
1945 = lifted_vs_unlifted
1946
1947 | Just (tc2, []) <- splitTyConApp_maybe ty2
1948 , tc2 `hasKey` liftedRepDataConKey
1949 = lifted_vs_unlifted
1950
1951 | otherwise -- So now we have Nothing or (Just IsSwapped)
1952 -- For some reason we treat Nothing like IsSwapped
1953 = addArising orig $
1954 sep [ text herald1 <+> quotes (ppr ty1)
1955 , nest padding $
1956 text herald2 <+> quotes (ppr ty2)
1957 , sameOccExtra ty2 ty1 ]
1958 where
1959 herald1 = conc [ "Couldn't match"
1960 , if is_repr then "representation of" else ""
1961 , if is_oriented then "expected" else ""
1962 , what ]
1963 herald2 = conc [ "with"
1964 , if is_repr then "that of" else ""
1965 , if is_oriented then ("actual " ++ what) else "" ]
1966 padding = length herald1 - length herald2
1967
1968 is_repr = case ctEqRel ct of { ReprEq -> True; NomEq -> False }
1969 is_oriented = isJust oriented
1970
1971 orig = ctOrigin ct
1972 what = case ctLocTypeOrKind_maybe (ctLoc ct) of
1973 Just KindLevel -> "kind"
1974 _ -> "type"
1975
1976 conc :: [String] -> String
1977 conc = foldr1 add_space
1978
1979 add_space :: String -> String -> String
1980 add_space s1 s2 | null s1 = s2
1981 | null s2 = s1
1982 | otherwise = s1 ++ (' ' : s2)
1983
1984 lifted_vs_unlifted
1985 = addArising orig $
1986 text "Couldn't match a lifted type with an unlifted type"
1987
1988 mkExpectedActualMsg :: Type -> Type -> CtOrigin -> Maybe TypeOrKind -> Bool
1989 -> (Bool, Maybe SwapFlag, SDoc)
1990 -- NotSwapped means (actual, expected), IsSwapped is the reverse
1991 -- First return val is whether or not to print a herald above this msg
1992 mkExpectedActualMsg ty1 ty2 (TypeEqOrigin { uo_actual = act
1993 , uo_expected = exp
1994 , uo_thing = maybe_thing })
1995 m_level printExpanded
1996 | KindLevel <- level, occurs_check_error = (True, Nothing, empty)
1997 | isUnliftedTypeKind act, isLiftedTypeKind exp = (False, Nothing, msg2)
1998 | isLiftedTypeKind act, isUnliftedTypeKind exp = (False, Nothing, msg3)
1999 | isLiftedTypeKind exp && not (isConstraintKind exp)
2000 = (False, Nothing, msg4)
2001 | Just msg <- num_args_msg = (False, Nothing, msg $$ msg1)
2002 | KindLevel <- level, Just th <- maybe_thing = (False, Nothing, msg5 th)
2003 | act `pickyEqType` ty1, exp `pickyEqType` ty2 = (True, Just NotSwapped, empty)
2004 | exp `pickyEqType` ty1, act `pickyEqType` ty2 = (True, Just IsSwapped, empty)
2005 | otherwise = (True, Nothing, msg1)
2006 where
2007 level = m_level `orElse` TypeLevel
2008
2009 occurs_check_error
2010 | Just act_tv <- tcGetTyVar_maybe act
2011 , act_tv `elemVarSet` tyCoVarsOfType exp
2012 = True
2013 | Just exp_tv <- tcGetTyVar_maybe exp
2014 , exp_tv `elemVarSet` tyCoVarsOfType act
2015 = True
2016 | otherwise
2017 = False
2018
2019 sort = case level of
2020 TypeLevel -> text "type"
2021 KindLevel -> text "kind"
2022
2023 msg1 = case level of
2024 KindLevel
2025 | Just th <- maybe_thing
2026 -> msg5 th
2027
2028 _ | not (act `pickyEqType` exp)
2029 -> vcat [ text "Expected" <+> sort <> colon <+> ppr exp
2030 , text " Actual" <+> sort <> colon <+> ppr act
2031 , if printExpanded then expandedTys else empty ]
2032
2033 | otherwise
2034 -> empty
2035
2036 thing_msg = case maybe_thing of
2037 Just thing -> \_ -> quotes thing <+> text "is"
2038 Nothing -> \vowel -> text "got a" <>
2039 if vowel then char 'n' else empty
2040 msg2 = sep [ text "Expecting a lifted type, but"
2041 , thing_msg True, text "unlifted" ]
2042 msg3 = sep [ text "Expecting an unlifted type, but"
2043 , thing_msg False, text "lifted" ]
2044 msg4 = maybe_num_args_msg $$
2045 sep [ text "Expected a type, but"
2046 , maybe (text "found something with kind")
2047 (\thing -> quotes thing <+> text "has kind")
2048 maybe_thing
2049 , quotes (ppr act) ]
2050
2051 msg5 th = hang (text "Expected" <+> kind_desc <> comma)
2052 2 (text "but" <+> quotes th <+> text "has kind" <+>
2053 quotes (ppr act))
2054 where
2055 kind_desc | isConstraintKind exp = text "a constraint"
2056 | otherwise = text "kind" <+> quotes (ppr exp)
2057
2058 num_args_msg = case level of
2059 KindLevel
2060 | not (isMetaTyVarTy exp) && not (isMetaTyVarTy act)
2061 -- if one is a meta-tyvar, then it's possible that the user
2062 -- has asked for something impredicative, and we couldn't unify.
2063 -- Don't bother with counting arguments.
2064 -> let n_act = count_args act
2065 n_exp = count_args exp in
2066 case n_act - n_exp of
2067 n | n > 0 -- we don't know how many args there are, so don't
2068 -- recommend removing args that aren't
2069 , Just thing <- maybe_thing
2070 -> Just $ text "Expecting" <+> speakN (abs n) <+>
2071 more <+> quotes thing
2072 where
2073 more
2074 | n == 1 = text "more argument to"
2075 | otherwise = text "more arguments to" -- n > 1
2076 _ -> Nothing
2077
2078 _ -> Nothing
2079
2080 maybe_num_args_msg = case num_args_msg of
2081 Nothing -> empty
2082 Just m -> m
2083
2084 count_args ty = count isVisibleBinder $ fst $ splitPiTys ty
2085
2086 expandedTys =
2087 ppUnless (expTy1 `pickyEqType` exp && expTy2 `pickyEqType` act) $ vcat
2088 [ text "Type synonyms expanded:"
2089 , text "Expected type:" <+> ppr expTy1
2090 , text " Actual type:" <+> ppr expTy2
2091 ]
2092
2093 (expTy1, expTy2) = expandSynonymsToMatch exp act
2094
2095 mkExpectedActualMsg _ _ _ _ _ = panic "mkExpectedAcutalMsg"
2096
2097 {- Note [Insoluble occurs check wins]
2098 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2099 Consider [G] a ~ [a], [W] a ~ [a] (Trac #13674). The Given is insoluble
2100 so we don't use it for rewriting. The Wanted is also insoluble, and
2101 we don't solve it from the Given. It's very confusing to say
2102 Cannot solve a ~ [a] from given constraints a ~ [a]
2103
2104 And indeed even thinking about the Givens is silly; [W] a ~ [a] is
2105 just as insoluble as Int ~ Bool.
2106
2107 Conclusion: if there's an insoluble occurs check (isInsolubleOccursCheck)
2108 then report it first.
2109
2110 (NB: there are potentially-soluble ones, like (a ~ F a b), and we don't
2111 want to be as draconian with them.)
2112
2113 Note [Expanding type synonyms to make types similar]
2114 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2115
2116 In type error messages, if -fprint-expanded-types is used, we want to expand
2117 type synonyms to make expected and found types as similar as possible, but we
2118 shouldn't expand types too much to make type messages even more verbose and
2119 harder to understand. The whole point here is to make the difference in expected
2120 and found types clearer.
2121
2122 `expandSynonymsToMatch` does this, it takes two types, and expands type synonyms
2123 only as much as necessary. Given two types t1 and t2:
2124
2125 * If they're already same, it just returns the types.
2126
2127 * If they're in form `C1 t1_1 .. t1_n` and `C2 t2_1 .. t2_m` (C1 and C2 are
2128 type constructors), it expands C1 and C2 if they're different type synonyms.
2129 Then it recursively does the same thing on expanded types. If C1 and C2 are
2130 same, then it applies the same procedure to arguments of C1 and arguments of
2131 C2 to make them as similar as possible.
2132
2133 Most important thing here is to keep number of synonym expansions at
2134 minimum. For example, if t1 is `T (T3, T5, Int)` and t2 is `T (T5, T3,
2135 Bool)` where T5 = T4, T4 = T3, ..., T1 = X, it returns `T (T3, T3, Int)` and
2136 `T (T3, T3, Bool)`.
2137
2138 * Otherwise types don't have same shapes and so the difference is clearly
2139 visible. It doesn't do any expansions and show these types.
2140
2141 Note that we only expand top-layer type synonyms. Only when top-layer
2142 constructors are the same we start expanding inner type synonyms.
2143
2144 Suppose top-layer type synonyms of t1 and t2 can expand N and M times,
2145 respectively. If their type-synonym-expanded forms will meet at some point (i.e.
2146 will have same shapes according to `sameShapes` function), it's possible to find
2147 where they meet in O(N+M) top-layer type synonym expansions and O(min(N,M))
2148 comparisons. We first collect all the top-layer expansions of t1 and t2 in two
2149 lists, then drop the prefix of the longer list so that they have same lengths.
2150 Then we search through both lists in parallel, and return the first pair of
2151 types that have same shapes. Inner types of these two types with same shapes
2152 are then expanded using the same algorithm.
2153
2154 In case they don't meet, we return the last pair of types in the lists, which
2155 has top-layer type synonyms completely expanded. (in this case the inner types
2156 are not expanded at all, as the current form already shows the type error)
2157 -}
2158
2159 -- | Expand type synonyms in given types only enough to make them as similar as
2160 -- possible. Returned types are the same in terms of used type synonyms.
2161 --
2162 -- To expand all synonyms, see 'Type.expandTypeSynonyms'.
2163 --
2164 -- See `ExpandSynsFail` tests in tests testsuite/tests/typecheck/should_fail for
2165 -- some examples of how this should work.
2166 expandSynonymsToMatch :: Type -> Type -> (Type, Type)
2167 expandSynonymsToMatch ty1 ty2 = (ty1_ret, ty2_ret)
2168 where
2169 (ty1_ret, ty2_ret) = go ty1 ty2
2170
2171 -- | Returns (type synonym expanded version of first type,
2172 -- type synonym expanded version of second type)
2173 go :: Type -> Type -> (Type, Type)
2174 go t1 t2
2175 | t1 `pickyEqType` t2 =
2176 -- Types are same, nothing to do
2177 (t1, t2)
2178
2179 go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
2180 | tc1 == tc2 =
2181 -- Type constructors are same. They may be synonyms, but we don't
2182 -- expand further.
2183 let (tys1', tys2') =
2184 unzip (zipWith (\ty1 ty2 -> go ty1 ty2) tys1 tys2)
2185 in (TyConApp tc1 tys1', TyConApp tc2 tys2')
2186
2187 go (AppTy t1_1 t1_2) (AppTy t2_1 t2_2) =
2188 let (t1_1', t2_1') = go t1_1 t2_1
2189 (t1_2', t2_2') = go t1_2 t2_2
2190 in (mkAppTy t1_1' t1_2', mkAppTy t2_1' t2_2')
2191
2192 go (FunTy t1_1 t1_2) (FunTy t2_1 t2_2) =
2193 let (t1_1', t2_1') = go t1_1 t2_1
2194 (t1_2', t2_2') = go t1_2 t2_2
2195 in (mkFunTy t1_1' t1_2', mkFunTy t2_1' t2_2')
2196
2197 go (ForAllTy b1 t1) (ForAllTy b2 t2) =
2198 -- NOTE: We may have a bug here, but we just can't reproduce it easily.
2199 -- See D1016 comments for details and our attempts at producing a test
2200 -- case. Short version: We probably need RnEnv2 to really get this right.
2201 let (t1', t2') = go t1 t2
2202 in (ForAllTy b1 t1', ForAllTy b2 t2')
2203
2204 go (CastTy ty1 _) ty2 = go ty1 ty2
2205 go ty1 (CastTy ty2 _) = go ty1 ty2
2206
2207 go t1 t2 =
2208 -- See Note [Expanding type synonyms to make types similar] for how this
2209 -- works
2210 let
2211 t1_exp_tys = t1 : tyExpansions t1
2212 t2_exp_tys = t2 : tyExpansions t2
2213 t1_exps = length t1_exp_tys
2214 t2_exps = length t2_exp_tys
2215 dif = abs (t1_exps - t2_exps)
2216 in
2217 followExpansions $
2218 zipEqual "expandSynonymsToMatch.go"
2219 (if t1_exps > t2_exps then drop dif t1_exp_tys else t1_exp_tys)
2220 (if t2_exps > t1_exps then drop dif t2_exp_tys else t2_exp_tys)
2221
2222 -- | Expand the top layer type synonyms repeatedly, collect expansions in a
2223 -- list. The list does not include the original type.
2224 --
2225 -- Example, if you have:
2226 --
2227 -- type T10 = T9
2228 -- type T9 = T8
2229 -- ...
2230 -- type T0 = Int
2231 --
2232 -- `tyExpansions T10` returns [T9, T8, T7, ... Int]
2233 --
2234 -- This only expands the top layer, so if you have:
2235 --
2236 -- type M a = Maybe a
2237 --
2238 -- `tyExpansions (M T10)` returns [Maybe T10] (T10 is not expanded)
2239 tyExpansions :: Type -> [Type]
2240 tyExpansions = unfoldr (\t -> (\x -> (x, x)) `fmap` tcView t)
2241
2242 -- | Drop the type pairs until types in a pair look alike (i.e. the outer
2243 -- constructors are the same).
2244 followExpansions :: [(Type, Type)] -> (Type, Type)
2245 followExpansions [] = pprPanic "followExpansions" empty
2246 followExpansions [(t1, t2)]
2247 | sameShapes t1 t2 = go t1 t2 -- expand subtrees
2248 | otherwise = (t1, t2) -- the difference is already visible
2249 followExpansions ((t1, t2) : tss)
2250 -- Traverse subtrees when the outer shapes are the same
2251 | sameShapes t1 t2 = go t1 t2
2252 -- Otherwise follow the expansions until they look alike
2253 | otherwise = followExpansions tss
2254
2255 sameShapes :: Type -> Type -> Bool
2256 sameShapes AppTy{} AppTy{} = True
2257 sameShapes (TyConApp tc1 _) (TyConApp tc2 _) = tc1 == tc2
2258 sameShapes (FunTy {}) (FunTy {}) = True
2259 sameShapes (ForAllTy {}) (ForAllTy {}) = True
2260 sameShapes (CastTy ty1 _) ty2 = sameShapes ty1 ty2
2261 sameShapes ty1 (CastTy ty2 _) = sameShapes ty1 ty2
2262 sameShapes _ _ = False
2263
2264 sameOccExtra :: TcType -> TcType -> SDoc
2265 -- See Note [Disambiguating (X ~ X) errors]
2266 sameOccExtra ty1 ty2
2267 | Just (tc1, _) <- tcSplitTyConApp_maybe ty1
2268 , Just (tc2, _) <- tcSplitTyConApp_maybe ty2
2269 , let n1 = tyConName tc1
2270 n2 = tyConName tc2
2271 same_occ = nameOccName n1 == nameOccName n2
2272 same_pkg = moduleUnitId (nameModule n1) == moduleUnitId (nameModule n2)
2273 , n1 /= n2 -- Different Names
2274 , same_occ -- but same OccName
2275 = text "NB:" <+> (ppr_from same_pkg n1 $$ ppr_from same_pkg n2)
2276 | otherwise
2277 = empty
2278 where
2279 ppr_from same_pkg nm
2280 | isGoodSrcSpan loc
2281 = hang (quotes (ppr nm) <+> text "is defined at")
2282 2 (ppr loc)
2283 | otherwise -- Imported things have an UnhelpfulSrcSpan
2284 = hang (quotes (ppr nm))
2285 2 (sep [ text "is defined in" <+> quotes (ppr (moduleName mod))
2286 , ppUnless (same_pkg || pkg == mainUnitId) $
2287 nest 4 $ text "in package" <+> quotes (ppr pkg) ])
2288 where
2289 pkg = moduleUnitId mod
2290 mod = nameModule nm
2291 loc = nameSrcSpan nm
2292
2293 {-
2294 Note [Suggest adding a type signature]
2295 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2296 The OutsideIn algorithm rejects GADT programs that don't have a principal
2297 type, and indeed some that do. Example:
2298 data T a where
2299 MkT :: Int -> T Int
2300
2301 f (MkT n) = n
2302
2303 Does this have type f :: T a -> a, or f :: T a -> Int?
2304 The error that shows up tends to be an attempt to unify an
2305 untouchable type variable. So suggestAddSig sees if the offending
2306 type variable is bound by an *inferred* signature, and suggests
2307 adding a declared signature instead.
2308
2309 This initially came up in Trac #8968, concerning pattern synonyms.
2310
2311 Note [Disambiguating (X ~ X) errors]
2312 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2313 See Trac #8278
2314
2315 Note [Reporting occurs-check errors]
2316 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2317 Given (a ~ [a]), if 'a' is a rigid type variable bound by a user-supplied
2318 type signature, then the best thing is to report that we can't unify
2319 a with [a], because a is a skolem variable. That avoids the confusing
2320 "occur-check" error message.
2321
2322 But nowadays when inferring the type of a function with no type signature,
2323 even if there are errors inside, we still generalise its signature and
2324 carry on. For example
2325 f x = x:x
2326 Here we will infer something like
2327 f :: forall a. a -> [a]
2328 with a deferred error of (a ~ [a]). So in the deferred unsolved constraint
2329 'a' is now a skolem, but not one bound by the programmer in the context!
2330 Here we really should report an occurs check.
2331
2332 So isUserSkolem distinguishes the two.
2333
2334 Note [Non-injective type functions]
2335 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2336 It's very confusing to get a message like
2337 Couldn't match expected type `Depend s'
2338 against inferred type `Depend s1'
2339 so mkTyFunInfoMsg adds:
2340 NB: `Depend' is type function, and hence may not be injective
2341
2342 Warn of loopy local equalities that were dropped.
2343
2344
2345 ************************************************************************
2346 * *
2347 Type-class errors
2348 * *
2349 ************************************************************************
2350 -}
2351
2352 mkDictErr :: ReportErrCtxt -> [Ct] -> TcM ErrMsg
2353 mkDictErr ctxt cts
2354 = ASSERT( not (null cts) )
2355 do { inst_envs <- tcGetInstEnvs
2356 ; let (ct1:_) = cts -- ct1 just for its location
2357 min_cts = elim_superclasses cts
2358 lookups = map (lookup_cls_inst inst_envs) min_cts
2359 (no_inst_cts, overlap_cts) = partition is_no_inst lookups
2360
2361 -- Report definite no-instance errors,
2362 -- or (iff there are none) overlap errors
2363 -- But we report only one of them (hence 'head') because they all
2364 -- have the same source-location origin, to try avoid a cascade
2365 -- of error from one location
2366 ; (ctxt, err) <- mk_dict_err ctxt (head (no_inst_cts ++ overlap_cts))
2367 ; mkErrorMsgFromCt ctxt ct1 (important err) }
2368 where
2369 no_givens = null (getUserGivens ctxt)
2370
2371 is_no_inst (ct, (matches, unifiers, _))
2372 = no_givens
2373 && null matches
2374 && (null unifiers || all (not . isAmbiguousTyVar) (tyCoVarsOfCtList ct))
2375
2376 lookup_cls_inst inst_envs ct
2377 -- Note [Flattening in error message generation]
2378 = (ct, lookupInstEnv True inst_envs clas (flattenTys emptyInScopeSet tys))
2379 where
2380 (clas, tys) = getClassPredTys (ctPred ct)
2381
2382
2383 -- When simplifying [W] Ord (Set a), we need
2384 -- [W] Eq a, [W] Ord a
2385 -- but we really only want to report the latter
2386 elim_superclasses cts = mkMinimalBySCs ctPred cts
2387
2388 mk_dict_err :: ReportErrCtxt -> (Ct, ClsInstLookupResult)
2389 -> TcM (ReportErrCtxt, SDoc)
2390 -- Report an overlap error if this class constraint results
2391 -- from an overlap (returning Left clas), otherwise return (Right pred)
2392 mk_dict_err ctxt@(CEC {cec_encl = implics}) (ct, (matches, unifiers, unsafe_overlapped))
2393 | null matches -- No matches but perhaps several unifiers
2394 = do { (ctxt, binds_msg, ct) <- relevantBindings True ctxt ct
2395 ; candidate_insts <- get_candidate_instances
2396 ; return (ctxt, cannot_resolve_msg ct candidate_insts binds_msg) }
2397
2398 | null unsafe_overlapped -- Some matches => overlap errors
2399 = return (ctxt, overlap_msg)
2400
2401 | otherwise
2402 = return (ctxt, safe_haskell_msg)
2403 where
2404 orig = ctOrigin ct
2405 pred = ctPred ct
2406 (clas, tys) = getClassPredTys pred
2407 ispecs = [ispec | (ispec, _) <- matches]
2408 unsafe_ispecs = [ispec | (ispec, _) <- unsafe_overlapped]
2409 useful_givens = discardProvCtxtGivens orig (getUserGivensFromImplics implics)
2410 -- useful_givens are the enclosing implications with non-empty givens,
2411 -- modulo the horrid discardProvCtxtGivens
2412
2413 get_candidate_instances :: TcM [ClsInst]
2414 -- See Note [Report candidate instances]
2415 get_candidate_instances
2416 | [ty] <- tys -- Only try for single-parameter classes
2417 = do { instEnvs <- tcGetInstEnvs
2418 ; return (filter (is_candidate_inst ty)
2419 (classInstances instEnvs clas)) }
2420 | otherwise = return []
2421
2422 is_candidate_inst ty inst -- See Note [Report candidate instances]
2423 | [other_ty] <- is_tys inst
2424 , Just (tc1, _) <- tcSplitTyConApp_maybe ty
2425 , Just (tc2, _) <- tcSplitTyConApp_maybe other_ty
2426 = let n1 = tyConName tc1
2427 n2 = tyConName tc2
2428 different_names = n1 /= n2
2429 same_occ_names = nameOccName n1 == nameOccName n2
2430 in different_names && same_occ_names
2431 | otherwise = False
2432
2433 cannot_resolve_msg :: Ct -> [ClsInst] -> SDoc -> SDoc
2434 cannot_resolve_msg ct candidate_insts binds_msg
2435 = vcat [ no_inst_msg
2436 , nest 2 extra_note
2437 , vcat (pp_givens useful_givens)
2438 , mb_patsyn_prov `orElse` empty
2439 , ppWhen (has_ambig_tvs && not (null unifiers && null useful_givens))
2440 (vcat [ ppUnless lead_with_ambig ambig_msg, binds_msg, potential_msg ])
2441
2442 , ppWhen (isNothing mb_patsyn_prov) $
2443 -- Don't suggest fixes for the provided context of a pattern
2444 -- synonym; the right fix is to bind more in the pattern
2445 show_fixes (ctxtFixes has_ambig_tvs pred implics
2446 ++ drv_fixes)
2447 , ppWhen (not (null candidate_insts))
2448 (hang (text "There are instances for similar types:")
2449 2 (vcat (map ppr candidate_insts))) ]
2450 -- See Note [Report candidate instances]
2451 where
2452 orig = ctOrigin ct
2453 -- See Note [Highlighting ambiguous type variables]
2454 lead_with_ambig = has_ambig_tvs && not (any isRuntimeUnkSkol ambig_tvs)
2455 && not (null unifiers) && null useful_givens
2456
2457 (has_ambig_tvs, ambig_msg) = mkAmbigMsg lead_with_ambig ct
2458 ambig_tvs = uncurry (++) (getAmbigTkvs ct)
2459
2460 no_inst_msg
2461 | lead_with_ambig
2462 = ambig_msg <+> pprArising orig
2463 $$ text "prevents the constraint" <+> quotes (pprParendType pred)
2464 <+> text "from being solved."
2465
2466 | null useful_givens
2467 = addArising orig $ text "No instance for"
2468 <+> pprParendType pred
2469
2470 | otherwise
2471 = addArising orig $ text "Could not deduce"
2472 <+> pprParendType pred
2473
2474 potential_msg
2475 = ppWhen (not (null unifiers) && want_potential orig) $
2476 sdocWithDynFlags $ \dflags ->
2477 getPprStyle $ \sty ->
2478 pprPotentials dflags sty potential_hdr unifiers
2479
2480 potential_hdr
2481 = vcat [ ppWhen lead_with_ambig $
2482 text "Probable fix: use a type annotation to specify what"
2483 <+> pprQuotedList ambig_tvs <+> text "should be."
2484 , text "These potential instance" <> plural unifiers
2485 <+> text "exist:"]
2486
2487 mb_patsyn_prov :: Maybe SDoc
2488 mb_patsyn_prov
2489 | not lead_with_ambig
2490 , ProvCtxtOrigin PSB{ psb_def = L _ pat } <- orig
2491 = Just (vcat [ text "In other words, a successful match on the pattern"
2492 , nest 2 $ ppr pat
2493 , text "does not provide the constraint" <+> pprParendType pred ])
2494 | otherwise = Nothing
2495
2496 -- Report "potential instances" only when the constraint arises
2497 -- directly from the user's use of an overloaded function
2498 want_potential (TypeEqOrigin {}) = False
2499 want_potential _ = True
2500
2501 extra_note | any isFunTy (filterOutInvisibleTypes (classTyCon clas) tys)
2502 = text "(maybe you haven't applied a function to enough arguments?)"
2503 | className clas == typeableClassName -- Avoid mysterious "No instance for (Typeable T)
2504 , [_,ty] <- tys -- Look for (Typeable (k->*) (T k))
2505 , Just (tc,_) <- tcSplitTyConApp_maybe ty
2506 , not (isTypeFamilyTyCon tc)
2507 = hang (text "GHC can't yet do polykinded")
2508 2 (text "Typeable" <+>
2509 parens (ppr ty <+> dcolon <+> ppr (typeKind ty)))
2510 | otherwise
2511 = empty
2512
2513 drv_fixes = case orig of
2514 DerivOrigin -> [drv_fix]
2515 DerivOriginDC {} -> [drv_fix]
2516 DerivOriginCoerce {} -> [drv_fix]
2517 _ -> []
2518
2519 drv_fix = hang (text "use a standalone 'deriving instance' declaration,")
2520 2 (text "so you can specify the instance context yourself")
2521
2522 -- Normal overlap error
2523 overlap_msg
2524 = ASSERT( not (null matches) )
2525 vcat [ addArising orig (text "Overlapping instances for"
2526 <+> pprType (mkClassPred clas tys))
2527
2528 , ppUnless (null matching_givens) $
2529 sep [text "Matching givens (or their superclasses):"
2530 , nest 2 (vcat matching_givens)]
2531
2532 , sdocWithDynFlags $ \dflags ->
2533 getPprStyle $ \sty ->
2534 pprPotentials dflags sty (text "Matching instances:") $
2535 ispecs ++ unifiers
2536
2537 , ppWhen (null matching_givens && isSingleton matches && null unifiers) $
2538 -- Intuitively, some given matched the wanted in their
2539 -- flattened or rewritten (from given equalities) form
2540 -- but the matcher can't figure that out because the
2541 -- constraints are non-flat and non-rewritten so we
2542 -- simply report back the whole given
2543 -- context. Accelerate Smart.hs showed this problem.
2544 sep [ text "There exists a (perhaps superclass) match:"
2545 , nest 2 (vcat (pp_givens useful_givens))]
2546
2547 , ppWhen (isSingleton matches) $
2548 parens (vcat [ text "The choice depends on the instantiation of" <+>
2549 quotes (pprWithCommas ppr (tyCoVarsOfTypesList tys))
2550 , ppWhen (null (matching_givens)) $
2551 vcat [ text "To pick the first instance above, use IncoherentInstances"
2552 , text "when compiling the other instance declarations"]
2553 ])]
2554
2555 matching_givens = mapMaybe matchable useful_givens
2556
2557 matchable (Implic { ic_given = evvars, ic_info = skol_info, ic_env = env })
2558 = case ev_vars_matching of
2559 [] -> Nothing
2560 _ -> Just $ hang (pprTheta ev_vars_matching)
2561 2 (sep [ text "bound by" <+> ppr skol_info
2562 , text "at" <+> ppr (tcl_loc env) ])
2563 where ev_vars_matching = filter ev_var_matches (map evVarPred evvars)
2564 ev_var_matches ty = case getClassPredTys_maybe ty of
2565 Just (clas', tys')
2566 | clas' == clas
2567 , Just _ <- tcMatchTys tys tys'
2568 -> True
2569 | otherwise
2570 -> any ev_var_matches (immSuperClasses clas' tys')
2571 Nothing -> False
2572
2573 -- Overlap error because of Safe Haskell (first
2574 -- match should be the most specific match)
2575 safe_haskell_msg
2576 = ASSERT( matches `lengthIs` 1 && not (null unsafe_ispecs) )
2577 vcat [ addArising orig (text "Unsafe overlapping instances for"
2578 <+> pprType (mkClassPred clas tys))
2579 , sep [text "The matching instance is:",
2580 nest 2 (pprInstance $ head ispecs)]
2581 , vcat [ text "It is compiled in a Safe module and as such can only"
2582 , text "overlap instances from the same module, however it"
2583 , text "overlaps the following instances from different" <+>
2584 text "modules:"
2585 , nest 2 (vcat [pprInstances $ unsafe_ispecs])
2586 ]
2587 ]
2588
2589
2590 ctxtFixes :: Bool -> PredType -> [Implication] -> [SDoc]
2591 ctxtFixes has_ambig_tvs pred implics
2592 | not has_ambig_tvs
2593 , isTyVarClassPred pred
2594 , (skol:skols) <- usefulContext implics pred
2595 , let what | null skols
2596 , SigSkol (PatSynCtxt {}) _ _ <- skol
2597 = text "\"required\""
2598 | otherwise
2599 = empty
2600 = [sep [ text "add" <+> pprParendType pred
2601 <+> text "to the" <+> what <+> text "context of"
2602 , nest 2 $ ppr_skol skol $$
2603 vcat [ text "or" <+> ppr_skol skol
2604 | skol <- skols ] ] ]
2605 | otherwise = []
2606 where
2607 ppr_skol (PatSkol (RealDataCon dc) _) = text "the data constructor" <+> quotes (ppr dc)
2608 ppr_skol (PatSkol (PatSynCon ps) _) = text "the pattern synonym" <+> quotes (ppr ps)
2609 ppr_skol skol_info = ppr skol_info
2610
2611 discardProvCtxtGivens :: CtOrigin -> [UserGiven] -> [UserGiven]
2612 discardProvCtxtGivens orig givens -- See Note [discardProvCtxtGivens]
2613 | ProvCtxtOrigin (PSB {psb_id = L _ name}) <- orig
2614 = filterOut (discard name) givens
2615 | otherwise
2616 = givens
2617 where
2618 discard n (Implic { ic_info = SigSkol (PatSynCtxt n') _ _ }) = n == n'
2619 discard _ _ = False
2620
2621 usefulContext :: [Implication] -> PredType -> [SkolemInfo]
2622 -- usefulContext picks out the implications whose context
2623 -- the programmer might plausibly augment to solve 'pred'
2624 usefulContext implics pred
2625 = go implics
2626 where
2627 pred_tvs = tyCoVarsOfType pred
2628 go [] = []
2629 go (ic : ics)
2630 | implausible ic = rest
2631 | otherwise = ic_info ic : rest
2632 where
2633 -- Stop when the context binds a variable free in the predicate
2634 rest | any (`elemVarSet` pred_tvs) (ic_skols ic) = []
2635 | otherwise = go ics
2636
2637 implausible ic
2638 | null (ic_skols ic) = True
2639 | implausible_info (ic_info ic) = True
2640 | otherwise = False
2641
2642 implausible_info (SigSkol (InfSigCtxt {}) _ _) = True
2643 implausible_info _ = False
2644 -- Do not suggest adding constraints to an *inferred* type signature
2645
2646 {- Note [Report candidate instances]
2647 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2648 If we have an unsolved (Num Int), where `Int` is not the Prelude Int,
2649 but comes from some other module, then it may be helpful to point out
2650 that there are some similarly named instances elsewhere. So we get
2651 something like
2652 No instance for (Num Int) arising from the literal ‘3’
2653 There are instances for similar types:
2654 instance Num GHC.Types.Int -- Defined in ‘GHC.Num’
2655 Discussion in Trac #9611.
2656
2657 Note [Highlighting ambiguous type variables]
2658 ~-------------------------------------------
2659 When we encounter ambiguous type variables (i.e. type variables
2660 that remain metavariables after type inference), we need a few more
2661 conditions before we can reason that *ambiguity* prevents constraints
2662 from being solved:
2663 - We can't have any givens, as encountering a typeclass error
2664 with given constraints just means we couldn't deduce
2665 a solution satisfying those constraints and as such couldn't
2666 bind the type variable to a known type.
2667 - If we don't have any unifiers, we don't even have potential
2668 instances from which an ambiguity could arise.
2669 - Lastly, I don't want to mess with error reporting for
2670 unknown runtime types so we just fall back to the old message there.
2671 Once these conditions are satisfied, we can safely say that ambiguity prevents
2672 the constraint from being solved.
2673
2674 Note [discardProvCtxtGivens]
2675 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
2676 In most situations we call all enclosing implications "useful". There is one
2677 exception, and that is when the constraint that causes the error is from the
2678 "provided" context of a pattern synonym declaration:
2679
2680 pattern Pat :: (Num a, Eq a) => Show a => a -> Maybe a
2681 -- required => provided => type
2682 pattern Pat x <- (Just x, 4)
2683
2684 When checking the pattern RHS we must check that it does actually bind all
2685 the claimed "provided" constraints; in this case, does the pattern (Just x, 4)
2686 bind the (Show a) constraint. Answer: no!
2687
2688 But the implication we generate for this will look like
2689 forall a. (Num a, Eq a) => [W] Show a
2690 because when checking the pattern we must make the required
2691 constraints available, since they are needed to match the pattern (in
2692 this case the literal '4' needs (Num a, Eq a)).
2693
2694 BUT we don't want to suggest adding (Show a) to the "required" constraints
2695 of the pattern synonym, thus:
2696 pattern Pat :: (Num a, Eq a, Show a) => Show a => a -> Maybe a
2697 It would then typecheck but it's silly. We want the /pattern/ to bind
2698 the alleged "provided" constraints, Show a.
2699
2700 So we suppress that Implication in discardProvCtxtGivens. It's
2701 painfully ad-hoc but the truth is that adding it to the "required"
2702 constraints would work. Suprressing it solves two problems. First,
2703 we never tell the user that we could not deduce a "provided"
2704 constraint from the "required" context. Second, we never give a
2705 possible fix that suggests to add a "provided" constraint to the
2706 "required" context.
2707
2708 For example, without this distinction the above code gives a bad error
2709 message (showing both problems):
2710
2711 error: Could not deduce (Show a) ... from the context: (Eq a)
2712 ... Possible fix: add (Show a) to the context of
2713 the signature for pattern synonym `Pat' ...
2714
2715 -}
2716
2717 show_fixes :: [SDoc] -> SDoc
2718 show_fixes [] = empty
2719 show_fixes (f:fs) = sep [ text "Possible fix:"
2720 , nest 2 (vcat (f : map (text "or" <+>) fs))]
2721
2722 pprPotentials :: DynFlags -> PprStyle -> SDoc -> [ClsInst] -> SDoc
2723 -- See Note [Displaying potential instances]
2724 pprPotentials dflags sty herald insts
2725 | null insts
2726 = empty
2727
2728 | null show_these
2729 = hang herald
2730 2 (vcat [ not_in_scope_msg empty
2731 , flag_hint ])
2732
2733 | otherwise
2734 = hang herald
2735 2 (vcat [ pprInstances show_these
2736 , ppWhen (n_in_scope_hidden > 0) $
2737 text "...plus"
2738 <+> speakNOf n_in_scope_hidden (text "other")
2739 , not_in_scope_msg (text "...plus")
2740 , flag_hint ])
2741 where
2742 n_show = 3 :: Int
2743 show_potentials = gopt Opt_PrintPotentialInstances dflags
2744
2745 (in_scope, not_in_scope) = partition inst_in_scope insts
2746 sorted = sortBy fuzzyClsInstCmp in_scope
2747 show_these | show_potentials = sorted
2748 | otherwise = take n_show sorted
2749 n_in_scope_hidden = length sorted - length show_these
2750
2751 -- "in scope" means that all the type constructors
2752 -- are lexically in scope; these instances are likely
2753 -- to be more useful
2754 inst_in_scope :: ClsInst -> Bool
2755 inst_in_scope cls_inst = nameSetAll name_in_scope $
2756 orphNamesOfTypes (is_tys cls_inst)
2757
2758 name_in_scope name
2759 | isBuiltInSyntax name
2760 = True -- E.g. (->)
2761 | Just mod <- nameModule_maybe name
2762 = qual_in_scope (qualName sty mod (nameOccName name))
2763 | otherwise
2764 = True
2765
2766 qual_in_scope :: QualifyName -> Bool
2767 qual_in_scope NameUnqual = True
2768 qual_in_scope (NameQual {}) = True
2769 qual_in_scope _ = False
2770
2771 not_in_scope_msg herald
2772 | null not_in_scope
2773 = empty
2774 | otherwise
2775 = hang (herald <+> speakNOf (length not_in_scope) (text "instance")
2776 <+> text "involving out-of-scope types")
2777 2 (ppWhen show_potentials (pprInstances not_in_scope))
2778
2779 flag_hint = ppUnless (show_potentials || equalLength show_these insts) $
2780 text "(use -fprint-potential-instances to see them all)"
2781
2782 {- Note [Displaying potential instances]
2783 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2784 When showing a list of instances for
2785 - overlapping instances (show ones that match)
2786 - no such instance (show ones that could match)
2787 we want to give it a bit of structure. Here's the plan
2788
2789 * Say that an instance is "in scope" if all of the
2790 type constructors it mentions are lexically in scope.
2791 These are the ones most likely to be useful to the programmer.
2792
2793 * Show at most n_show in-scope instances,
2794 and summarise the rest ("plus 3 others")
2795
2796 * Summarise the not-in-scope instances ("plus 4 not in scope")
2797
2798 * Add the flag -fshow-potential-instances which replaces the
2799 summary with the full list
2800 -}
2801
2802 {-
2803 Note [Flattening in error message generation]
2804 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2805 Consider (C (Maybe (F x))), where F is a type function, and we have
2806 instances
2807 C (Maybe Int) and C (Maybe a)
2808 Since (F x) might turn into Int, this is an overlap situation, and
2809 indeed (because of flattening) the main solver will have refrained
2810 from solving. But by the time we get to error message generation, we've
2811 un-flattened the constraint. So we must *re*-flatten it before looking
2812 up in the instance environment, lest we only report one matching
2813 instance when in fact there are two.
2814
2815 Re-flattening is pretty easy, because we don't need to keep track of
2816 evidence. We don't re-use the code in TcCanonical because that's in
2817 the TcS monad, and we are in TcM here.
2818
2819 Note [Suggest -fprint-explicit-kinds]
2820 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2821 It can be terribly confusing to get an error message like (Trac #9171)
2822 Couldn't match expected type ‘GetParam Base (GetParam Base Int)’
2823 with actual type ‘GetParam Base (GetParam Base Int)’
2824 The reason may be that the kinds don't match up. Typically you'll get
2825 more useful information, but not when it's as a result of ambiguity.
2826 This test suggests -fprint-explicit-kinds when all the ambiguous type
2827 variables are kind variables.
2828 -}
2829
2830 mkAmbigMsg :: Bool -- True when message has to be at beginning of sentence
2831 -> Ct -> (Bool, SDoc)
2832 mkAmbigMsg prepend_msg ct
2833 | null ambig_kvs && null ambig_tvs = (False, empty)
2834 | otherwise = (True, msg)
2835 where
2836 (ambig_kvs, ambig_tvs) = getAmbigTkvs ct
2837
2838 msg | any isRuntimeUnkSkol ambig_kvs -- See Note [Runtime skolems]
2839 || any isRuntimeUnkSkol ambig_tvs
2840 = vcat [ text "Cannot resolve unknown runtime type"
2841 <> plural ambig_tvs <+> pprQuotedList ambig_tvs
2842 , text "Use :print or :force to determine these types"]
2843
2844 | not (null ambig_tvs)
2845 = pp_ambig (text "type") ambig_tvs
2846
2847 | otherwise -- All ambiguous kind variabes; suggest -fprint-explicit-kinds
2848 -- See Note [Suggest -fprint-explicit-kinds]
2849 = vcat [ pp_ambig (text "kind") ambig_kvs
2850 , ppSuggestExplicitKinds ]
2851
2852 pp_ambig what tkvs
2853 | prepend_msg -- "Ambiguous type variable 't0'"
2854 = text "Ambiguous" <+> what <+> text "variable"
2855 <> plural tkvs <+> pprQuotedList tkvs
2856
2857 | otherwise -- "The type variable 't0' is ambiguous"
2858 = text "The" <+> what <+> text "variable" <> plural tkvs
2859 <+> pprQuotedList tkvs <+> is_or_are tkvs <+> text "ambiguous"
2860
2861 is_or_are [_] = text "is"
2862 is_or_are _ = text "are"
2863
2864 pprSkols :: ReportErrCtxt -> [TcTyVar] -> SDoc
2865 pprSkols ctxt tvs
2866 = vcat (map pp_one (getSkolemInfo (cec_encl ctxt) tvs))
2867 where
2868 pp_one (Implic { ic_info = skol_info }, tvs)
2869 | UnkSkol <- skol_info
2870 = hang (pprQuotedList tvs)
2871 2 (is_or_are tvs "an" "unknown")
2872 | otherwise
2873 = vcat [ hang (pprQuotedList tvs)
2874 2 (is_or_are tvs "a" "rigid" <+> text "bound by")
2875 , nest 2 (pprSkolInfo skol_info)
2876 , nest 2 (text "at" <+> ppr (foldr1 combineSrcSpans (map getSrcSpan tvs))) ]
2877
2878 is_or_are [_] article adjective = text "is" <+> text article <+> text adjective
2879 <+> text "type variable"
2880 is_or_are _ _ adjective = text "are" <+> text adjective
2881 <+> text "type variables"
2882
2883 getAmbigTkvs :: Ct -> ([Var],[Var])
2884 getAmbigTkvs ct
2885 = partition (`elemVarSet` dep_tkv_set) ambig_tkvs
2886 where
2887 tkvs = tyCoVarsOfCtList ct
2888 ambig_tkvs = filter isAmbiguousTyVar tkvs
2889 dep_tkv_set = tyCoVarsOfTypes (map tyVarKind tkvs)
2890
2891 getSkolemInfo :: [Implication] -> [TcTyVar]
2892 -> [(Implication, [TcTyVar])]
2893 -- Get the skolem info for some type variables
2894 -- from the implication constraints that bind them
2895 --
2896 -- In the returned (implic, tvs) pairs, the 'tvs' part is non-empty
2897 getSkolemInfo _ []
2898 = []
2899
2900 getSkolemInfo [] tvs
2901 = pprPanic "No skolem info:" (ppr tvs)
2902
2903 getSkolemInfo (implic:implics) tvs
2904 | null tvs_here = getSkolemInfo implics tvs
2905 | otherwise = (implic, tvs_here) : getSkolemInfo implics tvs_other
2906 where
2907 (tvs_here, tvs_other) = partition (`elem` ic_skols implic) tvs
2908
2909 -----------------------
2910 -- relevantBindings looks at the value environment and finds values whose
2911 -- types mention any of the offending type variables. It has to be
2912 -- careful to zonk the Id's type first, so it has to be in the monad.
2913 -- We must be careful to pass it a zonked type variable, too.
2914 --
2915 -- We always remove closed top-level bindings, though,
2916 -- since they are never relevant (cf Trac #8233)
2917
2918 relevantBindings :: Bool -- True <=> filter by tyvar; False <=> no filtering
2919 -- See Trac #8191
2920 -> ReportErrCtxt -> Ct
2921 -> TcM (ReportErrCtxt, SDoc, Ct)
2922 -- Also returns the zonked and tidied CtOrigin of the constraint
2923 relevantBindings want_filtering ctxt ct
2924 = do { dflags <- getDynFlags
2925 ; (env1, tidy_orig) <- zonkTidyOrigin (cec_tidy ctxt) (ctLocOrigin loc)
2926 ; let ct_tvs = tyCoVarsOfCt ct `unionVarSet` extra_tvs
2927
2928 -- For *kind* errors, report the relevant bindings of the
2929 -- enclosing *type* equality, because that's more useful for the programmer
2930 extra_tvs = case tidy_orig of
2931 KindEqOrigin t1 m_t2 _ _ -> tyCoVarsOfTypes $
2932 t1 : maybeToList m_t2
2933 _ -> emptyVarSet
2934 ; traceTc "relevantBindings" $
2935 vcat [ ppr ct
2936 , pprCtOrigin (ctLocOrigin loc)
2937 , ppr ct_tvs
2938 , pprWithCommas id [ ppr id <+> dcolon <+> ppr (idType id)
2939 | TcIdBndr id _ <- tcl_bndrs lcl_env ]
2940 , pprWithCommas id
2941 [ ppr id | TcIdBndr_ExpType id _ _ <- tcl_bndrs lcl_env ] ]
2942
2943 ; (tidy_env', docs, discards)
2944 <- go dflags env1 ct_tvs (maxRelevantBinds dflags)
2945 emptyVarSet [] False
2946 (remove_shadowing $ tcl_bndrs lcl_env)
2947 -- tcl_bndrs has the innermost bindings first,
2948 -- which are probably the most relevant ones
2949
2950 ; let doc = ppUnless (null docs) $
2951 hang (text "Relevant bindings include")
2952 2 (vcat docs $$ ppWhen discards discardMsg)
2953
2954 -- Put a zonked, tidied CtOrigin into the Ct
2955 loc' = setCtLocOrigin loc tidy_orig
2956 ct' = setCtLoc ct loc'
2957 ctxt' = ctxt { cec_tidy = tidy_env' }
2958
2959 ; return (ctxt', doc, ct') }
2960 where
2961 ev = ctEvidence ct
2962 loc = ctEvLoc ev
2963 lcl_env = ctLocEnv loc
2964
2965 run_out :: Maybe Int -> Bool
2966 run_out Nothing = False
2967 run_out (Just n) = n <= 0
2968
2969 dec_max :: Maybe Int -> Maybe Int
2970 dec_max = fmap (\n -> n - 1)
2971
2972 ---- fixes #12177
2973 ---- builds up a list of bindings whose OccName has not been seen before
2974 remove_shadowing :: [TcBinder] -> [TcBinder]
2975 remove_shadowing bindings = reverse $ fst $ foldl
2976 (\(bindingAcc, seenNames) binding ->
2977 if (occName binding) `elemOccSet` seenNames -- if we've seen it
2978 then (bindingAcc, seenNames) -- skip it
2979 else (binding:bindingAcc, extendOccSet seenNames (occName binding)))
2980 ([], emptyOccSet) bindings
2981
2982 go :: DynFlags -> TidyEnv -> TcTyVarSet -> Maybe Int -> TcTyVarSet -> [SDoc]
2983 -> Bool -- True <=> some filtered out due to lack of fuel
2984 -> [TcBinder]
2985 -> TcM (TidyEnv, [SDoc], Bool) -- The bool says if we filtered any out
2986 -- because of lack of fuel
2987 go _ tidy_env _ _ _ docs discards []
2988 = return (tidy_env, reverse docs, discards)
2989 go dflags tidy_env ct_tvs n_left tvs_seen docs discards (tc_bndr : tc_bndrs)
2990 = case tc_bndr of
2991 TcTvBndr {} -> discard_it
2992 TcIdBndr id top_lvl -> go2 (idName id) (idType id) top_lvl
2993 TcIdBndr_ExpType name et top_lvl ->
2994 do { mb_ty <- readExpType_maybe et
2995 -- et really should be filled in by now. But there's a chance
2996 -- it hasn't, if, say, we're reporting a kind error en route to
2997 -- checking a term. See test indexed-types/should_fail/T8129
2998 -- Or we are reporting errors from the ambiguity check on
2999 -- a local type signature
3000 ; case mb_ty of
3001 Just ty -> go2 name ty top_lvl
3002 Nothing -> discard_it -- No info; discard
3003 }
3004 where
3005 discard_it = go dflags tidy_env ct_tvs n_left tvs_seen docs
3006 discards tc_bndrs
3007 go2 id_name id_type top_lvl
3008 = do { (tidy_env', tidy_ty) <- zonkTidyTcType tidy_env id_type
3009 ; traceTc "relevantBindings 1" (ppr id_name <+> dcolon <+> ppr tidy_ty)
3010 ; let id_tvs = tyCoVarsOfType tidy_ty
3011 doc = sep [ pprPrefixOcc id_name <+> dcolon <+> ppr tidy_ty
3012 , nest 2 (parens (text "bound at"
3013 <+> ppr (getSrcLoc id_name)))]
3014 new_seen = tvs_seen `unionVarSet` id_tvs
3015
3016 ; if (want_filtering && not (hasPprDebug dflags)
3017 && id_tvs `disjointVarSet` ct_tvs)
3018 -- We want to filter out this binding anyway
3019 -- so discard it silently
3020 then discard_it
3021
3022 else if isTopLevel top_lvl && not (isNothing n_left)
3023 -- It's a top-level binding and we have not specified
3024 -- -fno-max-relevant-bindings, so discard it silently
3025 then discard_it
3026
3027 else if run_out n_left && id_tvs `subVarSet` tvs_seen
3028 -- We've run out of n_left fuel and this binding only
3029 -- mentions already-seen type variables, so discard it
3030 then go dflags tidy_env ct_tvs n_left tvs_seen docs
3031 True -- Record that we have now discarded something
3032 tc_bndrs
3033
3034 -- Keep this binding, decrement fuel
3035 else go dflags tidy_env' ct_tvs (dec_max n_left) new_seen
3036 (doc:docs) discards tc_bndrs }
3037
3038 discardMsg :: SDoc
3039 discardMsg = text "(Some bindings suppressed;" <+>
3040 text "use -fmax-relevant-binds=N or -fno-max-relevant-binds)"
3041
3042 subsDiscardMsg :: SDoc
3043 subsDiscardMsg =
3044 text "(Some substitutions suppressed;" <+>
3045 text "use -fmax-valid-substitutions=N or -fno-max-valid-substitutions)"
3046
3047 -----------------------
3048 warnDefaulting :: [Ct] -> Type -> TcM ()
3049 warnDefaulting wanteds default_ty
3050 = do { warn_default <- woptM Opt_WarnTypeDefaults
3051 ; env0 <- tcInitTidyEnv
3052 ; let tidy_env = tidyFreeTyCoVars env0 $
3053 tyCoVarsOfCtsList (listToBag wanteds)
3054 tidy_wanteds = map (tidyCt tidy_env) wanteds
3055 (loc, ppr_wanteds) = pprWithArising tidy_wanteds
3056 warn_msg =
3057 hang (hsep [ text "Defaulting the following"
3058 , text "constraint" <> plural tidy_wanteds
3059 , text "to type"
3060 , quotes (ppr default_ty) ])
3061 2
3062 ppr_wanteds
3063 ; setCtLocM loc $ warnTc (Reason Opt_WarnTypeDefaults) warn_default warn_msg }
3064
3065 {-
3066 Note [Runtime skolems]
3067 ~~~~~~~~~~~~~~~~~~~~~~
3068 We want to give a reasonably helpful error message for ambiguity
3069 arising from *runtime* skolems in the debugger. These
3070 are created by in RtClosureInspect.zonkRTTIType.
3071
3072 ************************************************************************
3073 * *
3074 Error from the canonicaliser
3075 These ones are called *during* constraint simplification
3076 * *
3077 ************************************************************************
3078 -}
3079
3080 solverDepthErrorTcS :: CtLoc -> TcType -> TcM a
3081 solverDepthErrorTcS loc ty
3082 = setCtLocM loc $
3083 do { ty <- zonkTcType ty
3084 ; env0 <- tcInitTidyEnv
3085 ; let tidy_env = tidyFreeTyCoVars env0 (tyCoVarsOfTypeList ty)
3086 tidy_ty = tidyType tidy_env ty
3087 msg
3088 = vcat [ text "Reduction stack overflow; size =" <+> ppr depth
3089 , hang (text "When simplifying the following type:")
3090 2 (ppr tidy_ty)
3091 , note ]
3092 ; failWithTcM (tidy_env, msg) }
3093 where
3094 depth = ctLocDepth loc
3095 note = vcat
3096 [ text "Use -freduction-depth=0 to disable this check"
3097 , text "(any upper bound you could choose might fail unpredictably with"
3098 , text " minor updates to GHC, so disabling the check is recommended if"
3099 , text " you're sure that type checking should terminate)" ]