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