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