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