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