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