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