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