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