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