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