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