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