Tidy up error suppression
[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, pprNameProvenance
40 , GlobalRdrElt (..), globalRdrEnvElts )
41 import PrelNames ( typeableClassName, hasKey, liftedRepDataConKey, tYPETyConKey )
42 import Id
43 import Var
44 import VarSet
45 import VarEnv
46 import NameSet
47 import Bag
48 import ErrUtils ( ErrMsg, errDoc, pprLocErrMsg )
49 import BasicTypes
50 import ConLike ( ConLike(..))
51 import Util
52 import TcEnv (tcLookup)
53 import {-# SOURCE #-} TcSimplify ( tcCheckHoleFit, tcSubsumes )
54 import FastString
55 import Outputable
56 import SrcLoc
57 import DynFlags
58 import ListSetOps ( equivClasses )
59 import Maybes
60 import Pair
61 import qualified GHC.LanguageExtensions as LangExt
62 import FV ( fvVarList, fvVarSet, unionFV )
63
64 import Control.Monad ( when, filterM, replicateM )
65 import Data.Foldable ( toList )
66 import Data.List ( partition, mapAccumL, nub
67 , sortBy, sort, unfoldr, foldl' )
68 import qualified Data.Set as Set
69 import Data.Graph ( graphFromEdges, topSort )
70 import Data.Function ( on )
71
72 import Data.Semigroup ( Semigroup )
73 import qualified Data.Semigroup as Semigroup
74
75
76 {-
77 ************************************************************************
78 * *
79 \section{Errors and contexts}
80 * *
81 ************************************************************************
82
83 ToDo: for these error messages, should we note the location as coming
84 from the insts, or just whatever seems to be around in the monad just
85 now?
86
87 Note [Deferring coercion errors to runtime]
88 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
89 While developing, sometimes it is desirable to allow compilation to succeed even
90 if there are type errors in the code. Consider the following case:
91
92 module Main where
93
94 a :: Int
95 a = 'a'
96
97 main = print "b"
98
99 Even though `a` is ill-typed, it is not used in the end, so if all that we're
100 interested in is `main` it is handy to be able to ignore the problems in `a`.
101
102 Since we treat type equalities as evidence, this is relatively simple. Whenever
103 we run into a type mismatch in TcUnify, we normally just emit an error. But it
104 is always safe to defer the mismatch to the main constraint solver. If we do
105 that, `a` will get transformed into
106
107 co :: Int ~ Char
108 co = ...
109
110 a :: Int
111 a = 'a' `cast` co
112
113 The constraint solver would realize that `co` is an insoluble constraint, and
114 emit an error with `reportUnsolved`. But we can also replace the right-hand side
115 of `co` with `error "Deferred type error: Int ~ Char"`. This allows the program
116 to compile, and it will run fine unless we evaluate `a`. This is what
117 `deferErrorsToRuntime` does.
118
119 It does this by keeping track of which errors correspond to which coercion
120 in TcErrors. TcErrors.reportTidyWanteds does not print the errors
121 and does not fail if -fdefer-type-errors is on, so that we can continue
122 compilation. The errors are turned into warnings in `reportUnsolved`.
123 -}
124
125 -- | Report unsolved goals as errors or warnings. We may also turn some into
126 -- deferred run-time errors if `-fdefer-type-errors` is on.
127 reportUnsolved :: WantedConstraints -> TcM (Bag EvBind)
128 reportUnsolved wanted
129 = do { binds_var <- newTcEvBinds
130 ; defer_errors <- goptM Opt_DeferTypeErrors
131 ; warn_errors <- woptM Opt_WarnDeferredTypeErrors -- implement #10283
132 ; let type_errors | not defer_errors = TypeError
133 | warn_errors = TypeWarn (Reason Opt_WarnDeferredTypeErrors)
134 | otherwise = TypeDefer
135
136 ; defer_holes <- goptM Opt_DeferTypedHoles
137 ; warn_holes <- woptM Opt_WarnTypedHoles
138 ; let expr_holes | not defer_holes = HoleError
139 | warn_holes = HoleWarn
140 | otherwise = HoleDefer
141
142 ; partial_sigs <- xoptM LangExt.PartialTypeSignatures
143 ; warn_partial_sigs <- woptM Opt_WarnPartialTypeSignatures
144 ; let type_holes | not partial_sigs = HoleError
145 | warn_partial_sigs = HoleWarn
146 | otherwise = HoleDefer
147
148 ; defer_out_of_scope <- goptM Opt_DeferOutOfScopeVariables
149 ; warn_out_of_scope <- woptM Opt_WarnDeferredOutOfScopeVariables
150 ; let out_of_scope_holes | not defer_out_of_scope = HoleError
151 | warn_out_of_scope = HoleWarn
152 | otherwise = HoleDefer
153
154 ; report_unsolved binds_var type_errors expr_holes
155 type_holes out_of_scope_holes wanted
156
157 ; ev_binds <- getTcEvBindsMap binds_var
158 ; return (evBindMapBinds ev_binds)}
159
160 -- | Report *all* unsolved goals as errors, even if -fdefer-type-errors is on
161 -- However, do not make any evidence bindings, because we don't
162 -- have any convenient place to put them.
163 -- See Note [Deferring coercion errors to runtime]
164 -- Used by solveEqualities for kind equalities
165 -- (see Note [Fail fast on kind errors] in TcSimplify]
166 -- and for simplifyDefault.
167 reportAllUnsolved :: WantedConstraints -> TcM ()
168 reportAllUnsolved wanted
169 = do { ev_binds <- newNoTcEvBinds
170 ; report_unsolved ev_binds TypeError
171 HoleError HoleError HoleError wanted }
172
173 -- | Report all unsolved goals as warnings (but without deferring any errors to
174 -- run-time). See Note [Safe Haskell Overlapping Instances Implementation] in
175 -- TcSimplify
176 warnAllUnsolved :: WantedConstraints -> TcM ()
177 warnAllUnsolved wanted
178 = do { ev_binds <- newTcEvBinds
179 ; report_unsolved ev_binds (TypeWarn NoReason)
180 HoleWarn HoleWarn HoleWarn wanted }
181
182 -- | Report unsolved goals as errors or warnings.
183 report_unsolved :: EvBindsVar -- cec_binds
184 -> TypeErrorChoice -- Deferred type errors
185 -> HoleChoice -- Expression holes
186 -> HoleChoice -- Type holes
187 -> HoleChoice -- Out of scope holes
188 -> WantedConstraints -> TcM ()
189 report_unsolved mb_binds_var type_errors expr_holes
190 type_holes out_of_scope_holes wanted
191 | isEmptyWC wanted
192 = return ()
193 | otherwise
194 = do { traceTc "reportUnsolved warning/error settings:" $
195 vcat [ text "type errors:" <+> ppr type_errors
196 , text "expr holes:" <+> ppr expr_holes
197 , text "type holes:" <+> ppr type_holes
198 , text "scope holes:" <+> ppr out_of_scope_holes ]
199 ; traceTc "reportUnsolved (before zonking and tidying)" (ppr wanted)
200
201 ; wanted <- zonkWC wanted -- Zonk to reveal all information
202 ; env0 <- tcInitTidyEnv
203 -- If we are deferring we are going to need /all/ evidence around,
204 -- including the evidence produced by unflattening (zonkWC)
205 ; let tidy_env = tidyFreeTyCoVars env0 free_tvs
206 free_tvs = tyCoVarsOfWCList wanted
207
208 ; traceTc "reportUnsolved (after zonking):" $
209 vcat [ text "Free tyvars:" <+> pprTyVars free_tvs
210 , text "Tidy env:" <+> ppr tidy_env
211 , text "Wanted:" <+> ppr wanted ]
212
213 ; warn_redundant <- woptM Opt_WarnRedundantConstraints
214 ; let err_ctxt = CEC { cec_encl = []
215 , cec_tidy = tidy_env
216 , cec_defer_type_errors = type_errors
217 , cec_expr_holes = expr_holes
218 , cec_type_holes = type_holes
219 , cec_out_of_scope_holes = out_of_scope_holes
220 , cec_suppress = False -- See Note [Suppressing error messages]
221 , cec_warn_redundant = warn_redundant
222 , cec_binds = mb_binds_var }
223
224 ; tc_lvl <- getTcLevel
225 ; reportWanteds err_ctxt tc_lvl wanted }
226
227 --------------------------------------------
228 -- Internal functions
229 --------------------------------------------
230
231 -- | An error Report collects messages categorised by their importance.
232 -- See Note [Error report] for details.
233 data Report
234 = Report { report_important :: [SDoc]
235 , report_relevant_bindings :: [SDoc]
236 , report_valid_substitutions :: [SDoc]
237 }
238
239 instance Outputable Report where -- Debugging only
240 ppr (Report { report_important = imp
241 , report_relevant_bindings = rel
242 , report_valid_substitutions = val })
243 = vcat [ text "important:" <+> vcat imp
244 , text "relevant:" <+> vcat rel
245 , text "valid:" <+> vcat val ]
246
247 {- Note [Error report]
248 The idea is that error msgs are divided into three parts: the main msg, the
249 context block (\"In the second argument of ...\"), and the relevant bindings
250 block, which are displayed in that order, with a mark to divide them. The
251 idea is that the main msg ('report_important') varies depending on the error
252 in question, but context and relevant bindings are always the same, which
253 should simplify visual parsing.
254
255 The context is added when the Report is passed off to 'mkErrorReport'.
256 Unfortunately, unlike the context, the relevant bindings are added in
257 multiple places so they have to be in the Report.
258 -}
259
260 instance Semigroup Report where
261 Report a1 b1 c1 <> Report a2 b2 c2 = Report (a1 ++ a2) (b1 ++ b2) (c1 ++ c2)
262
263 instance Monoid Report where
264 mempty = Report [] [] []
265 mappend = (Semigroup.<>)
266
267 -- | Put a doc into the important msgs block.
268 important :: SDoc -> Report
269 important doc = mempty { report_important = [doc] }
270
271 -- | Put a doc into the relevant bindings block.
272 relevant_bindings :: SDoc -> Report
273 relevant_bindings doc = mempty { report_relevant_bindings = [doc] }
274
275 -- | Put a doc into the valid substitutions block.
276 valid_substitutions :: SDoc -> Report
277 valid_substitutions docs = mempty { report_valid_substitutions = [docs] }
278
279 data TypeErrorChoice -- What to do for type errors found by the type checker
280 = TypeError -- A type error aborts compilation with an error message
281 | TypeWarn WarnReason
282 -- A type error is deferred to runtime, plus a compile-time warning
283 -- The WarnReason should usually be (Reason Opt_WarnDeferredTypeErrors)
284 -- but it isn't for the Safe Haskell Overlapping Instances warnings
285 -- see warnAllUnsolved
286 | TypeDefer -- A type error is deferred to runtime; no error or warning at compile time
287
288 data HoleChoice
289 = HoleError -- A hole is a compile-time error
290 | HoleWarn -- Defer to runtime, emit a compile-time warning
291 | HoleDefer -- Defer to runtime, no warning
292
293 instance Outputable HoleChoice where
294 ppr HoleError = text "HoleError"
295 ppr HoleWarn = text "HoleWarn"
296 ppr HoleDefer = text "HoleDefer"
297
298 instance Outputable TypeErrorChoice where
299 ppr TypeError = text "TypeError"
300 ppr (TypeWarn reason) = text "TypeWarn" <+> ppr reason
301 ppr TypeDefer = text "TypeDefer"
302
303 data ReportErrCtxt
304 = CEC { cec_encl :: [Implication] -- Enclosing implications
305 -- (innermost first)
306 -- ic_skols and givens are tidied, rest are not
307 , cec_tidy :: TidyEnv
308
309 , cec_binds :: EvBindsVar -- Make some errors (depending on cec_defer)
310 -- into warnings, and emit evidence bindings
311 -- into 'cec_binds' for unsolved constraints
312
313 , cec_defer_type_errors :: TypeErrorChoice -- Defer type errors until runtime
314
315 -- cec_expr_holes is a union of:
316 -- cec_type_holes - a set of typed holes: '_', '_a', '_foo'
317 -- cec_out_of_scope_holes - a set of variables which are
318 -- out of scope: 'x', 'y', 'bar'
319 , cec_expr_holes :: HoleChoice -- Holes in expressions
320 , cec_type_holes :: HoleChoice -- Holes in types
321 , cec_out_of_scope_holes :: HoleChoice -- Out of scope holes
322
323 , cec_warn_redundant :: Bool -- True <=> -Wredundant-constraints
324
325 , cec_suppress :: Bool -- True <=> More important errors have occurred,
326 -- so create bindings if need be, but
327 -- don't issue any more errors/warnings
328 -- See Note [Suppressing error messages]
329 }
330
331 instance Outputable ReportErrCtxt where
332 ppr (CEC { cec_binds = bvar
333 , cec_defer_type_errors = dte
334 , cec_expr_holes = eh
335 , cec_type_holes = th
336 , cec_out_of_scope_holes = osh
337 , cec_warn_redundant = wr
338 , cec_suppress = sup })
339 = text "CEC" <+> braces (vcat
340 [ text "cec_binds" <+> equals <+> ppr bvar
341 , text "cec_defer_type_errors" <+> equals <+> ppr dte
342 , text "cec_expr_holes" <+> equals <+> ppr eh
343 , text "cec_type_holes" <+> equals <+> ppr th
344 , text "cec_out_of_scope_holes" <+> equals <+> ppr osh
345 , text "cec_warn_redundant" <+> equals <+> ppr wr
346 , text "cec_suppress" <+> equals <+> ppr sup ])
347
348 -- | Returns True <=> the ReportErrCtxt indicates that something is deferred
349 deferringAnyBindings :: ReportErrCtxt -> Bool
350 -- Don't check cec_type_holes, as these don't cause bindings to be deferred
351 deferringAnyBindings (CEC { cec_defer_type_errors = TypeError
352 , cec_expr_holes = HoleError
353 , cec_out_of_scope_holes = HoleError }) = False
354 deferringAnyBindings _ = True
355
356 -- | Transforms a 'ReportErrCtxt' into one that does not defer any bindings
357 -- at all.
358 noDeferredBindings :: ReportErrCtxt -> ReportErrCtxt
359 noDeferredBindings ctxt = ctxt { cec_defer_type_errors = TypeError
360 , cec_expr_holes = HoleError
361 , cec_out_of_scope_holes = HoleError }
362
363 {- Note [Suppressing error messages]
364 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
365 The cec_suppress flag says "don't report any errors". Instead, just create
366 evidence bindings (as usual). It's used when more important errors have occurred.
367
368 Specifically (see reportWanteds)
369 * If there are insoluble Givens, then we are in unreachable code and all bets
370 are off. So don't report any further errors.
371 * If there are any insolubles (eg Int~Bool), here or in a nested implication,
372 then suppress errors from the simple constraints here. Sometimes the
373 simple-constraint errors are a knock-on effect of the insolubles.
374
375 This suppression behaviour is controlled by the Bool flag in
376 ReportErrorSpec, as used in reportWanteds.
377
378 But we need to take care: flags can turn errors into warnings, and we
379 don't want those warnings to suppress subsequent errors (including
380 suppressing the essential addTcEvBind for them: Trac #15152). So in
381 tryReporter we use askNoErrs to see if any error messages were
382 /actually/ produced; if not, we don't switch on suppression.
383
384 A consequence is that warnings never suppress warnings, so turning an
385 error into a warning may allow subsequent warnings to appear that were
386 previously suppressed. (e.g. partial-sigs/should_fail/T14584)
387 -}
388
389 reportImplic :: ReportErrCtxt -> Implication -> TcM ()
390 reportImplic ctxt implic@(Implic { ic_skols = tvs, ic_telescope = m_telescope
391 , ic_given = given
392 , ic_wanted = wanted, ic_binds = evb
393 , ic_status = status, ic_info = info
394 , ic_env = tcl_env, ic_tclvl = tc_lvl })
395 | BracketSkol <- info
396 , not insoluble
397 = return () -- For Template Haskell brackets report only
398 -- definite errors. The whole thing will be re-checked
399 -- later when we plug it in, and meanwhile there may
400 -- certainly be un-satisfied constraints
401
402 | otherwise
403 = do { traceTc "reportImplic" (ppr implic')
404 ; reportWanteds ctxt' tc_lvl wanted
405 ; when (cec_warn_redundant ctxt) $
406 warnRedundantConstraints ctxt' tcl_env info' dead_givens
407 ; when bad_telescope $ reportBadTelescope ctxt tcl_env m_telescope tvs }
408 where
409 insoluble = isInsolubleStatus status
410 (env1, tvs') = mapAccumL tidyTyCoVarBndr (cec_tidy ctxt) tvs
411 info' = tidySkolemInfo env1 info
412 implic' = implic { ic_skols = tvs'
413 , ic_given = map (tidyEvVar env1) given
414 , ic_info = info' }
415 ctxt1 | NoEvBindsVar{} <- evb = noDeferredBindings ctxt
416 | termEvidenceAllowed info = ctxt
417 | otherwise = noDeferredBindings ctxt
418 -- If we go inside an implication that has no term
419 -- evidence (i.e. unifying under a forall), we can't defer
420 -- type errors. You could imagine using the /enclosing/
421 -- bindings (in cec_binds), but that may not have enough stuff
422 -- in scope for the bindings to be well typed. So we just
423 -- switch off deferred type errors altogether. See Trac #14605.
424
425 ctxt' = ctxt1 { cec_tidy = env1
426 , cec_encl = implic' : cec_encl ctxt
427
428 , cec_suppress = insoluble || cec_suppress ctxt
429 -- Suppress inessential errors if there
430 -- are insolubles anywhere in the
431 -- tree rooted here, or we've come across
432 -- a suppress-worthy constraint higher up (Trac #11541)
433
434 , cec_binds = evb }
435
436 dead_givens = case status of
437 IC_Solved { ics_dead = dead } -> dead
438 _ -> []
439
440 bad_telescope = case status of
441 IC_BadTelescope -> True
442 _ -> False
443
444 warnRedundantConstraints :: ReportErrCtxt -> TcLclEnv -> SkolemInfo -> [EvVar] -> TcM ()
445 -- See Note [Tracking redundant constraints] in TcSimplify
446 warnRedundantConstraints ctxt env info ev_vars
447 | null redundant_evs
448 = return ()
449
450 | SigSkol {} <- info
451 = setLclEnv env $ -- We want to add "In the type signature for f"
452 -- to the error context, which is a bit tiresome
453 addErrCtxt (text "In" <+> ppr info) $
454 do { env <- getLclEnv
455 ; msg <- mkErrorReport ctxt env (important doc)
456 ; reportWarning (Reason Opt_WarnRedundantConstraints) msg }
457
458 | otherwise -- But for InstSkol there already *is* a surrounding
459 -- "In the instance declaration for Eq [a]" context
460 -- and we don't want to say it twice. Seems a bit ad-hoc
461 = do { msg <- mkErrorReport ctxt env (important doc)
462 ; reportWarning (Reason Opt_WarnRedundantConstraints) msg }
463 where
464 doc = text "Redundant constraint" <> plural redundant_evs <> colon
465 <+> pprEvVarTheta redundant_evs
466
467 redundant_evs = case info of -- See Note [Redundant constraints in instance decls]
468 InstSkol -> filterOut improving ev_vars
469 _ -> ev_vars
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 ; maybeReportError ctxt 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 (EvExpr 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 (EvExpr 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 ; no_show_valid_substitutions <- goptM Opt_NoShowValidSubstitutions
1149 ; sub_msg <- if no_show_valid_substitutions then return empty
1150 else validSubstitutions tidy_simples ctxt ct
1151 ; mkErrorMsgFromCt ctxt ct $
1152 important hole_msg `mappend`
1153 relevant_bindings (binds_msg $$ constraints_msg) `mappend`
1154 valid_substitutions sub_msg}
1155
1156 where
1157 occ = holeOcc hole
1158 hole_ty = ctEvPred (ctEvidence ct)
1159 hole_kind = typeKind hole_ty
1160 tyvars = tyCoVarsOfTypeList hole_ty
1161
1162 hole_msg = case hole of
1163 ExprHole {} -> vcat [ hang (text "Found hole:")
1164 2 (pp_with_type occ hole_ty)
1165 , tyvars_msg, expr_hole_hint ]
1166 TypeHole {} -> vcat [ hang (text "Found type wildcard" <+>
1167 quotes (ppr occ))
1168 2 (text "standing for" <+>
1169 quotes pp_hole_type_with_kind)
1170 , tyvars_msg, type_hole_hint ]
1171
1172 pp_hole_type_with_kind
1173 | isLiftedTypeKind hole_kind = pprType hole_ty
1174 | otherwise = pprType hole_ty <+> dcolon <+> pprKind hole_kind
1175
1176 tyvars_msg = ppUnless (null tyvars) $
1177 text "Where:" <+> (vcat (map loc_msg other_tvs)
1178 $$ pprSkols ctxt skol_tvs)
1179 where
1180 (skol_tvs, other_tvs) = partition is_skol tyvars
1181 is_skol tv = isTcTyVar tv && isSkolemTyVar tv
1182 -- Coercion variables can be free in the
1183 -- hole, via kind casts
1184
1185 type_hole_hint
1186 | HoleError <- cec_type_holes ctxt
1187 = text "To use the inferred type, enable PartialTypeSignatures"
1188 | otherwise
1189 = empty
1190
1191 expr_hole_hint -- Give hint for, say, f x = _x
1192 | lengthFS (occNameFS occ) > 1 -- Don't give this hint for plain "_"
1193 = text "Or perhaps" <+> quotes (ppr occ)
1194 <+> text "is mis-spelled, or not in scope"
1195 | otherwise
1196 = empty
1197
1198 loc_msg tv
1199 | isTyVar tv
1200 = case tcTyVarDetails tv of
1201 MetaTv {} -> quotes (ppr tv) <+> text "is an ambiguous type variable"
1202 _ -> empty -- Skolems dealt with already
1203 | otherwise -- A coercion variable can be free in the hole type
1204 = sdocWithDynFlags $ \dflags ->
1205 if gopt Opt_PrintExplicitCoercions dflags
1206 then quotes (ppr tv) <+> text "is a coercion variable"
1207 else empty
1208
1209 mkHoleError _ _ ct = pprPanic "mkHoleError" (ppr ct)
1210
1211 -- HoleFit is the type we use for a fit in valid substitutions. It contains the
1212 -- element that was checked, the Id of that element as found by `tcLookup`,
1213 -- and the refinement level of the fit, which is the number of extra argument
1214 -- holes that this fit uses (e.g. if hfRefLvl is 2, the fit is for `Id _ _`).
1215 data HoleFit = HoleFit { hfEl :: GlobalRdrElt -- The element that was checked.
1216 , hfId :: Id -- the elements id in the TcM.
1217 , hfRefLvl :: Int } -- The number of holes in this fit
1218
1219 -- We define an Eq and Ord instance to be able to build a graph.
1220 instance Eq HoleFit where
1221 (==) = (==) `on` hfId
1222
1223 -- We compare HoleFits by their gre_name instead of their Id, since we don't
1224 -- want our tests to be affected by the non-determinism of `nonDetCmpVar`,
1225 -- which is used to compare Ids. When comparing, we want HoleFits with a lower
1226 -- refinement level to come first.
1227 instance Ord HoleFit where
1228 compare a b = cmp a b
1229 where cmp = if (hfRefLvl a) == (hfRefLvl b)
1230 then compare `on` (gre_name . hfEl)
1231 else compare `on` hfRefLvl
1232
1233 instance Outputable HoleFit where
1234 ppr = pprHoleFit False
1235
1236 -- For pretty printing hole fits, we display the name and type of the fit,
1237 -- with added '_' to represent any extra arguments in case of a non-zero
1238 -- refinement level.
1239 pprHoleFit :: Bool -> HoleFit -> SDoc
1240 pprHoleFit showProv hf =
1241 if showProv then sep [idAndTy, nest 2 provenance] else idAndTy
1242 where name = gre_name (hfEl hf)
1243 ty = varType (hfId hf)
1244 holeVs = hsep $ replicate (hfRefLvl hf) $ text "_"
1245 idAndTy = (pprPrefixOcc name <+> holeVs <+> dcolon <+> pprType ty)
1246 provenance = parens $ pprNameProvenance (hfEl hf)
1247
1248
1249 -- See Note [Valid substitutions include ...]
1250 validSubstitutions :: [Ct] -> ReportErrCtxt -> Ct -> TcM SDoc
1251 validSubstitutions simples (CEC {cec_encl = implics}) ct | isExprHoleCt ct =
1252 do { rdr_env <- getGlobalRdrEnv
1253 ; maxVSubs <- maxValidSubstitutions <$> getDynFlags
1254 ; showProvenance <- not <$> goptM Opt_UnclutterValidSubstitutions
1255 ; graphSortSubs <- not <$> goptM Opt_NoSortValidSubstitutions
1256 ; refLevel <- refLevelSubstitutions <$> getDynFlags
1257 ; traceTc "findingValidSubstitutionsFor { " $ ppr ct
1258 ; traceTc "hole_lvl is:" $ ppr hole_lvl
1259 ; traceTc "implics are: " $ ppr implics
1260 ; traceTc "simples are: " $ ppr simples
1261 ; (searchDiscards, subs) <-
1262 findSubs graphSortSubs maxVSubs rdr_env 0 (wrapped_hole_ty, [])
1263 ; (vDiscards, sortedSubs) <-
1264 sortSubs graphSortSubs maxVSubs searchDiscards subs
1265 ; let vMsg = ppUnless (null subs) $
1266 hang (text "Valid substitutions include") 2 $
1267 (vcat (map (pprHoleFit showProvenance) sortedSubs)
1268 $$ ppWhen vDiscards subsDiscardMsg)
1269 ; refMsg <- if refLevel >= (Just 0) then
1270 do { maxRSubs <- maxRefSubstitutions <$> getDynFlags
1271 -- We can use from just, since we know that Nothing >= _ is False.
1272 ; let refLvls = [1..(fromJust refLevel)]
1273 -- We make a new refinement type for each level of refinement, where
1274 -- the level of refinement indicates number of additional arguments
1275 -- to allow.
1276 ; ref_tys <- mapM (\l -> mkRefTy l >>= return . (,) l) refLvls
1277 ; traceTc "ref_tys are" $ ppr ref_tys
1278 ; refDs <-
1279 mapM (uncurry $ findSubs graphSortSubs maxRSubs rdr_env) ref_tys
1280 ; (rDiscards, sortedRSubs) <-
1281 sortSubs graphSortSubs maxRSubs (any fst refDs) $
1282 concatMap snd refDs
1283 ; return $
1284 ppUnless (null sortedRSubs) $
1285 hang (text "Valid refinement substitutions include") 2 $
1286 (vcat (map (pprHoleFit showProvenance) sortedRSubs)
1287 $$ ppWhen rDiscards refSubsDiscardMsg) }
1288 else return empty
1289 ; traceTc "findingValidSubstitutionsFor }" empty
1290 ; return (vMsg $$ refMsg)}
1291 where
1292 hole_loc = ctEvLoc $ ctEvidence ct
1293 hole_lvl = ctLocLevel $ hole_loc
1294
1295 -- We make a refinement type by adding a new type variable in front
1296 -- of the type of t h hole, going from e.g. [Integer] -> Integer
1297 -- to t_a1/m[tau:1] -> [Integer] -> Integer. This allows the simplifier
1298 -- to unify the new type variable with any type, allowing us
1299 -- to suggest a "refinement substitution", like `(foldl1 _)` instead
1300 -- of only concrete substitutions like `sum`.
1301 mkRefTy :: Int -> TcM (TcType, [TcType])
1302 mkRefTy refLvl = (\v -> (wrapHoleWithArgs v, v)) <$> newTyVarTys
1303 where newTyVarTys = replicateM refLvl newOpenFlexiTyVarTy
1304 wrapHoleWithArgs args = (wrap_ty . mkFunTys args) hole_ty
1305
1306
1307 sortSubs :: Bool -- Whether we should sort the subs or not
1308 -- by subsumption or not
1309 -> Maybe Int -- How many we should output, if limited.
1310 -> Bool -- Whether there were any discards in the
1311 -- initial search
1312 -> [HoleFit] -- The subs to sort
1313 -> TcM (Bool, [HoleFit])
1314 -- If we don't want to sort by the subsumption graph, we just sort it
1315 -- such that local fits come before global fits, since local fits are
1316 -- probably more relevant to the user.
1317 sortSubs False _ discards subs = return (discards, sortedFits)
1318 where (lclFits, gblFits) = partition (gre_lcl . hfEl) subs
1319 sortedFits = lclFits ++ gblFits
1320 -- We sort the fits first, to prevent the order of
1321 -- suggestions being effected when identifiers are moved
1322 -- around in modules. We use (<*>) to expose the
1323 -- parallelism, in case it becomes useful later.
1324 sortSubs _ limit _ subs = possiblyDiscard limit <$>
1325 ((++) <$> sortByGraph (sort lclFits)
1326 <*> sortByGraph (sort gblFits))
1327 where (lclFits, gblFits) = partition (gre_lcl . hfEl) subs
1328
1329
1330 findSubs :: Bool -- Whether we should sort the subs or not
1331 -> Maybe Int -- How many we should output, if limited
1332 -> GlobalRdrEnv -- The elements to check whether fit
1333 -> Int -- The refinement level of the hole
1334 -> (TcType, [TcType]) -- The type to check for fits and ref vars
1335 -> TcM (Bool, [HoleFit])
1336 -- We don't check if no output is desired.
1337 findSubs _ (Just 0) _ _ _ = return (False, [])
1338 findSubs sortSubs maxSubs rdr_env refLvl ht@(hole_ty, _) =
1339 do { traceTc "checkingSubstitutionsFor {" $ ppr $ hole_ty
1340 ; let limit = if sortSubs then Nothing else maxSubs
1341 ; (discards, subs) <- setTcLevel hole_lvl $
1342 go limit ht refLvl $
1343 globalRdrEnvElts rdr_env
1344 ; traceTc "}" empty
1345 ; return (discards, subs) }
1346 -- We extract the type of the hole from the constraint.
1347 hole_ty :: TcPredType
1348 hole_ty = ctPred ct
1349 hole_fvs = tyCoFVsOfType hole_ty
1350
1351 -- For checking, we wrap the type of the hole with all the givens
1352 -- from all the implications in the context.
1353 wrap_ty :: TcType -> TcSigmaType
1354 wrap_ty ty = foldl' wrapTypeWithImplication ty implics
1355
1356 wrapped_hole_ty :: TcSigmaType
1357 wrapped_hole_ty = wrap_ty hole_ty
1358
1359 -- We rearrange the elements to make locals appear at the top of the list
1360 -- since they're most likely to be relevant to the user.
1361 localsFirst :: [HoleFit] -> [HoleFit]
1362 localsFirst elts = lcl ++ gbl
1363 where (lcl, gbl) = partition (gre_lcl . hfEl) elts
1364
1365
1366 -- These are the constraints whose every free unification variable is
1367 -- mentioned in the type of the hole.
1368 relevantCts :: [Ct]
1369 relevantCts = if isEmptyVarSet hole_fv then []
1370 else filter isRelevant simples
1371 where hole_fv :: VarSet
1372 hole_fv = fvVarSet hole_fvs
1373 ctFreeVarSet :: Ct -> VarSet
1374 ctFreeVarSet = fvVarSet . tyCoFVsOfType . ctPred
1375 allFVMentioned :: Ct -> Bool
1376 allFVMentioned ct = ctFreeVarSet ct `subVarSet` hole_fv
1377 -- We filter out those constraints that have no variables (since
1378 -- they won't be solved by finding a type for the type variable
1379 -- representing the hole) and also other holes, since we're not
1380 -- trying to find substitutions for many holes at once.
1381 isRelevant ct = not (isEmptyVarSet (ctFreeVarSet ct))
1382 && allFVMentioned ct
1383 && not (isHoleCt ct)
1384
1385
1386 -- This creates a substitution with new fresh type variables for all the
1387 -- free variables mentioned in the type of hole and in the relevant
1388 -- constraints. Note that since we only pick constraints such that all their
1389 -- free variables are mentioned by the hole, the free variables of the hole
1390 -- are all the free variables of the constraints as well.
1391 getHoleCloningSubst :: TcType -> TcM TCvSubst
1392 getHoleCloningSubst hole_ty = mkTvSubstPrs <$> getClonedVars
1393 where cloneFV :: TyVar -> TcM (TyVar, Type)
1394 cloneFV fv = ((,) fv) <$> pushTcLevelM_ (newFlexiTyVarTy (varType fv))
1395 -- The subsumption check pushes the level, so as to be sure that
1396 -- its invocation of the solver doesn't unify type variables floating
1397 -- about that are unrelated to the subsumption check. However, these
1398 -- cloned variables in the hole type *should* be unified, so we make
1399 -- sure to bump the level before creating them
1400
1401 getClonedVars :: TcM [(TyVar, Type)]
1402 getClonedVars = mapM cloneFV (fvVarList $ tyCoFVsOfType hole_ty)
1403
1404 -- This applies the given substitution to the given constraint.
1405 applySubToCt :: TCvSubst -> Ct -> Ct
1406 applySubToCt sub ct = ct {cc_ev = ev {ctev_pred = subbedPredType} }
1407 where subbedPredType = substTy sub $ ctPred ct
1408 ev = ctEvidence ct
1409
1410 -- The real work happens here, where we invoke the type checker
1411 -- to check whether we the given type fits into the hole!
1412 -- To check: Clone all relevant cts and the hole
1413 -- then solve the subsumption check AND check that all other
1414 -- the other constraints were solved.
1415 fitsHole :: (TcType, [TcType]) -> Type -> TcM Bool
1416 fitsHole (hole_ty, vars) typ =
1417 do { traceTc "checkingFitOf {" $ ppr typ
1418 ; cloneSub <- getHoleCloningSubst hole_ty
1419 ; let cHoleTy = substTy cloneSub hole_ty
1420 cCts = map (applySubToCt cloneSub) relevantCts
1421 cVars = map (substTy cloneSub) vars
1422
1423 ; absFits <- tcCheckHoleFit (listToBag cCts) cHoleTy typ
1424 ; traceTc "}" empty
1425 -- We'd like to avoid refinement suggestions like `id _ _` or
1426 -- `head _ _`, and only suggest refinements where our all phantom
1427 -- variables got unified during the checking. This can be disabled
1428 -- with the `-fabstract-refinement-substitutions` flag.
1429 ; if absFits && (not . null) vars then
1430 goptM Opt_AbstractRefSubstitutions `orM`
1431 allM isFilledMetaTyVar (fvVarList $ tyCoFVsOfTypes cVars)
1432 else return absFits }
1433
1434 -- Based on the flags, we might possibly discard some or all the
1435 -- fits we've found.
1436 possiblyDiscard :: Maybe Int -> [HoleFit] -> (Bool, [HoleFit])
1437 possiblyDiscard (Just max) fits = (fits `lengthExceeds` max, take max fits)
1438 possiblyDiscard Nothing fits = (False, fits)
1439
1440 -- Based on a suggestion by phadej on #ghc, we can sort the found fits
1441 -- by constructing a subsumption graph, and then do a topological sort of
1442 -- the graph. This makes the most specific types appear first, which are
1443 -- probably those most relevant. This takes a lot of work (but results in
1444 -- much more useful output), and can be disabled by
1445 -- '-fno-sort-valid-substitutions'.
1446 sortByGraph :: [HoleFit] -> TcM [HoleFit]
1447 sortByGraph fits = go [] fits
1448 where hfType :: HoleFit -> TcSigmaType
1449 hfType = varType . hfId
1450
1451 go :: [(HoleFit, [HoleFit])] -> [HoleFit] -> TcM [HoleFit]
1452 go sofar [] = do { traceTc "subsumptionGraph was" $ ppr sofar
1453 ; return $ localsFirst topSorted }
1454 where toV (hf, adjs) = (hf, hfId hf, map hfId adjs)
1455 (graph, fromV, _) = graphFromEdges $ map toV sofar
1456 topSorted = map ((\(h,_,_) -> h) . fromV) $ topSort graph
1457 go sofar (id:ids) =
1458 do { adjs <- filterM (tcSubsumes (hfType id) . hfType) fits
1459 ; go ((id, adjs):sofar) ids }
1460
1461 -- Kickoff the checking of the elements.
1462 go :: Maybe Int -> (TcType, [TcType]) -> Int
1463 -> [GlobalRdrElt] -> TcM (Bool, [HoleFit])
1464 go = go_ []
1465
1466 -- We iterate over the elements, checking each one in turn for whether it
1467 -- fits, and adding it to the results if it does.
1468 go_ :: [HoleFit] -- What we've found so far.
1469 -> Maybe Int -- How many we're allowed to find, if limited
1470 -> (TcType, [TcType]) -- The type to check, and refinement variables.
1471 -> Int -- The refinement level of the hole we're checking
1472 -> [GlobalRdrElt] -- The elements we've yet to check.
1473 -> TcM (Bool, [HoleFit])
1474 go_ subs _ _ _ [] = return (False, reverse subs)
1475 go_ subs (Just 0) _ _ _ = return (True, reverse subs)
1476 go_ subs maxleft t r (el:elts) =
1477 do { traceTc "lookingUp" $ ppr el
1478 ; maybeThing <- lookup (gre_name el)
1479 ; case maybeThing of
1480 Just id -> do { fits <- fitsHole t (varType id)
1481 ; if fits then keep_it (HoleFit el id r)
1482 else discard_it }
1483 _ -> discard_it }
1484 where discard_it = go_ subs maxleft t r elts
1485 keep_it fit = go_ (fit:subs) ((\n -> n - 1) <$> maxleft) t r elts
1486 lookup name =
1487 do { thing <- tcLookup name
1488 ; case thing of
1489 ATcId {tct_id = id} -> return $ Just id
1490 AGlobal (AnId id) -> return $ Just id
1491 AGlobal (AConLike (RealDataCon con)) ->
1492 return $ Just (dataConWrapId con)
1493 _ -> return Nothing }
1494
1495
1496 -- We don't (as of yet) handle holes in types, only in expressions.
1497 validSubstitutions _ _ _ = return empty
1498
1499
1500 -- See Note [Constraints include ...]
1501 givenConstraintsMsg :: ReportErrCtxt -> SDoc
1502 givenConstraintsMsg ctxt =
1503 let constraints :: [(Type, RealSrcSpan)]
1504 constraints =
1505 do { Implic{ ic_given = given, ic_env = env } <- cec_encl ctxt
1506 ; constraint <- given
1507 ; return (varType constraint, tcl_loc env) }
1508
1509 pprConstraint (constraint, loc) =
1510 ppr constraint <+> nest 2 (parens (text "from" <+> ppr loc))
1511
1512 in ppUnless (null constraints) $
1513 hang (text "Constraints include")
1514 2 (vcat $ map pprConstraint constraints)
1515
1516 pp_with_type :: OccName -> Type -> SDoc
1517 pp_with_type occ ty = hang (pprPrefixOcc occ) 2 (dcolon <+> pprType ty)
1518
1519 ----------------
1520 mkIPErr :: ReportErrCtxt -> [Ct] -> TcM ErrMsg
1521 mkIPErr ctxt cts
1522 = do { (ctxt, binds_msg, ct1) <- relevantBindings True ctxt ct1
1523 ; let orig = ctOrigin ct1
1524 preds = map ctPred cts
1525 givens = getUserGivens ctxt
1526 msg | null givens
1527 = addArising orig $
1528 sep [ text "Unbound implicit parameter" <> plural cts
1529 , nest 2 (pprParendTheta preds) ]
1530 | otherwise
1531 = couldNotDeduce givens (preds, orig)
1532
1533 ; mkErrorMsgFromCt ctxt ct1 $
1534 important msg `mappend` relevant_bindings binds_msg }
1535 where
1536 (ct1:_) = cts
1537
1538 {-
1539 Note [Valid substitutions include ...]
1540 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1541 `validSubstitutions` returns the "Valid substitutions include ..." message.
1542 For example, look at the following definitions in a file called test.hs:
1543
1544 import Data.List (inits)
1545
1546 f :: [String]
1547 f = _ "hello, world"
1548
1549 The hole in `f` would generate the message:
1550
1551 • Found hole: _ :: [Char] -> [String]
1552 • In the expression: _
1553 In the expression: _ "hello, world"
1554 In an equation for ‘f’: f = _ "hello, world"
1555 • Relevant bindings include f :: [String] (bound at test.hs:6:1)
1556 Valid substitutions include
1557 lines :: String -> [String]
1558 (imported from ‘Prelude’ at test.hs:1:8-11
1559 (and originally defined in ‘base-4.11.0.0:Data.OldList’))
1560 words :: String -> [String]
1561 (imported from ‘Prelude’ at test.hs:1:8-11
1562 (and originally defined in ‘base-4.11.0.0:Data.OldList’))
1563 read :: forall a. Read a => String -> a
1564 (imported from ‘Prelude’ at test.hs:1:8-11
1565 (and originally defined in ‘Text.Read’))
1566 inits :: forall a. [a] -> [[a]]
1567 (imported from ‘Data.List’ at test.hs:3:19-23
1568 (and originally defined in ‘base-4.11.0.0:Data.OldList’))
1569 repeat :: forall a. a -> [a]
1570 (imported from ‘Prelude’ at test.hs:1:8-11
1571 (and originally defined in ‘GHC.List’))
1572 mempty :: forall a. Monoid a => a
1573 (imported from ‘Prelude’ at test.hs:1:8-11
1574 (and originally defined in ‘GHC.Base’))
1575 return :: forall (m :: * -> *). Monad m => forall a. a -> m a
1576 (imported from ‘Prelude’ at test.hs:1:8-11
1577 (and originally defined in ‘GHC.Base’))
1578 pure :: forall (f :: * -> *). Applicative f => forall a. a -> f a
1579 (imported from ‘Prelude’ at test.hs:1:8-11
1580 (and originally defined in ‘GHC.Base’))
1581 fail :: forall (m :: * -> *). Monad m => forall a. String -> m a
1582 (imported from ‘Prelude’ at test.hs:1:8-11
1583 (and originally defined in ‘GHC.Base’))
1584 error :: forall (a :: TYPE r). GHC.Stack.Types.HasCallStack => [Char] -> a
1585 (imported from ‘Prelude’ at test.hs:1:8-11
1586 (and originally defined in ‘GHC.Err’))
1587 errorWithoutStackTrace :: forall (a :: TYPE r). [Char] -> a
1588 (imported from ‘Prelude’ at test.hs:1:8-11
1589 (and originally defined in ‘GHC.Err’))
1590 undefined :: forall (a :: TYPE r). GHC.Stack.Types.HasCallStack => a
1591 (imported from ‘Prelude’ at test.hs:1:8-11
1592 (and originally defined in ‘GHC.Err’))
1593
1594
1595 Valid substitutions are found by checking top level identifiers in scope for
1596 whether their type is subsumed by the type of the hole. Additionally, as
1597 highlighted by Trac #14273, we also need to check whether all relevant
1598 constraints are solved by choosing an identifier of that type as well. This is
1599 to make sure we don't suggest a substitution which does not fulfill the
1600 constraints imposed on the hole (even though it has a type that would otherwise
1601 fit the hole). The relevant constraints are those whose free unification
1602 variables are all mentioned by the type of the hole. Since checking for
1603 subsumption results in the side effect of type variables being unified by the
1604 simplifier, we need to take care to clone the variables in the hole and relevant
1605 constraints before checking whether an identifier fits into the hole, to avoid
1606 affecting the hole and later checks. When outputting, take the fits found for
1607 the hole and build a subsumption graph, where fit a and fit b are connected if
1608 a subsumes b. We then sort the graph topologically, and output the suggestions
1609 in that order. This is done in order to display "more relevant" suggestions
1610 first where the most specific suggestions (i.e. the ones that are subsumed by
1611 the other suggestions) appear first. This puts suggestions such as `error` and
1612 `undefined` last, as seen in the example above.
1613
1614 When the flag `-frefinement-level-substitutions=n` where `n > 0` is passed, we
1615 also look for valid refinement substitutions, i.e. substitutions that are valid,
1616 but adds more holes. Consider the following:
1617
1618 f :: [Integer] -> Integer
1619 f = _
1620
1621 Here the valid substitutions suggested will be (with the
1622 `-funclutter-valid-substitutions` flag set):
1623
1624 Valid substitutions include
1625 f :: [Integer] -> Integer
1626 product :: forall (t :: * -> *).
1627 Foldable t => forall a. Num a => t a -> a
1628 sum :: forall (t :: * -> *).
1629 Foldable t => forall a. Num a => t a -> a
1630 maximum :: forall (t :: * -> *).
1631 Foldable t => forall a. Ord a => t a -> a
1632 minimum :: forall (t :: * -> *).
1633 Foldable t => forall a. Ord a => t a -> a
1634 head :: forall a. [a] -> a
1635 (Some substitutions suppressed;
1636 use -fmax-valid-substitutions=N or -fno-max-valid-substitutions)
1637
1638 When the `-frefinement-level-substitutions=1` flag is given, we additionally
1639 compute and report valid refinement substitutions:
1640
1641 Valid refinement substitutions include
1642 foldl1 _ :: forall (t :: * -> *).
1643 Foldable t => forall a. (a -> a -> a) -> t a -> a
1644 foldr1 _ :: forall (t :: * -> *).
1645 Foldable t => forall a. (a -> a -> a) -> t a -> a
1646 head _ :: forall a. [a] -> a
1647 last _ :: forall a. [a] -> a
1648 error _ :: forall (a :: TYPE r).
1649 GHC.Stack.Types.HasCallStack => [Char] -> a
1650 errorWithoutStackTrace _ :: forall (a :: TYPE r). [Char] -> a
1651 (Some refinement substitutions suppressed;
1652 use -fmax-refinement-substitutions=N or -fno-max-refinement-substitutions)
1653
1654 Which are substitutions with holes in them. This allows e.g. beginners to
1655 discover the fold functions and similar.
1656
1657 We find these refinement suggestions by considering substitutions that don't
1658 fit the type of the hole, but ones that would fit if given an additional
1659 argument. We do this by creating a new type variable with `newOpenFlexiTyVarTy`
1660 (e.g. `t_a1/m[tau:1]`), and then considering substitutions of the type
1661 `t_a1/m[tau:1] -> v` where `v` is the type of the hole. Since the simplifier is
1662 free to unify this new type variable with any type (and it is cloned before each
1663 check to avoid side-effects), we can now discover any identifiers that would fit
1664 if given another identifier of a suitable type. This is then generalized so that
1665 we can consider any number of additional arguments by setting the
1666 `-frefinement-level-substitutions` flag to any number, and then considering
1667 substitutions like e.g. `foldl _ _` with two additional arguments.
1668
1669 Note [Constraints include ...]
1670 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1671 'givenConstraintsMsg' returns the "Constraints include ..." message enabled by
1672 -fshow-hole-constraints. For example, the following hole:
1673
1674 foo :: (Eq a, Show a) => a -> String
1675 foo x = _
1676
1677 would generate the message:
1678
1679 Constraints include
1680 Eq a (from foo.hs:1:1-36)
1681 Show a (from foo.hs:1:1-36)
1682
1683 Constraints are displayed in order from innermost (closest to the hole) to
1684 outermost. There's currently no filtering or elimination of duplicates.
1685
1686
1687 Note [OutOfScope exact matches]
1688 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1689 When constructing an out-of-scope error message, we not only generate a list of
1690 possible in-scope alternatives but also search for an exact, unambiguous match
1691 in a later inter-splice group. If we find such a match, we report its presence
1692 (and indirectly, its scope) in the message. For example, if a module A contains
1693 the following declarations,
1694
1695 foo :: Int
1696 foo = x
1697
1698 $(return []) -- Empty top-level splice
1699
1700 x :: Int
1701 x = 23
1702
1703 we will issue an error similar to
1704
1705 A.hs:6:7: error:
1706 • Variable not in scope: x :: Int
1707 • ‘x’ (line 11) is not in scope before the splice on line 8
1708
1709 By providing information about the match, we hope to clarify why declaring a
1710 variable after a top-level splice but using it before the splice generates an
1711 out-of-scope error (a situation which is often confusing to Haskell newcomers).
1712
1713 Note that if we find multiple exact matches to the out-of-scope variable
1714 (hereafter referred to as x), we report nothing. Such matches can only be
1715 duplicate record fields, as the presence of any other duplicate top-level
1716 declarations would have already halted compilation. But if these record fields
1717 are declared in a later inter-splice group, then so too are their corresponding
1718 types. Thus, these types must not occur in the inter-splice group containing x
1719 (any unknown types would have already been reported), and so the matches to the
1720 record fields are most likely coincidental.
1721
1722 One oddity of the exact match portion of the error message is that we specify
1723 where the match to x is NOT in scope. Why not simply state where the match IS
1724 in scope? It most cases, this would be just as easy and perhaps a little
1725 clearer for the user. But now consider the following example:
1726
1727 {-# LANGUAGE TemplateHaskell #-}
1728
1729 module A where
1730
1731 import Language.Haskell.TH
1732 import Language.Haskell.TH.Syntax
1733
1734 foo = x
1735
1736 $(do -------------------------------------------------
1737 ds <- [d| ok1 = x
1738 |]
1739 addTopDecls ds
1740 return [])
1741
1742 bar = $(do
1743 ds <- [d| x = 23
1744 ok2 = x
1745 |]
1746 addTopDecls ds
1747 litE $ stringL "hello")
1748
1749 $(return []) -----------------------------------------
1750
1751 ok3 = x
1752
1753 Here, x is out-of-scope in the declaration of foo, and so we report
1754
1755 A.hs:8:7: error:
1756 • Variable not in scope: x
1757 • ‘x’ (line 16) is not in scope before the splice on lines 10-14
1758
1759 If we instead reported where x IS in scope, we would have to state that it is in
1760 scope after the second top-level splice as well as among all the top-level
1761 declarations added by both calls to addTopDecls. But doing so would not only
1762 add complexity to the code but also overwhelm the user with unneeded
1763 information.
1764
1765 The logic which determines where x is not in scope is straightforward: it simply
1766 finds the last top-level splice which occurs after x but before (or at) the
1767 match to x (assuming such a splice exists). In most cases, the check that the
1768 splice occurs after x acts only as a sanity check. For example, when the match
1769 to x is a non-TH top-level declaration and a splice S occurs before the match,
1770 then x must precede S; otherwise, it would be in scope. But when dealing with
1771 addTopDecls, this check serves a practical purpose. Consider the following
1772 declarations:
1773
1774 $(do
1775 ds <- [d| ok = x
1776 x = 23
1777 |]
1778 addTopDecls ds
1779 return [])
1780
1781 foo = x
1782
1783 In this case, x is not in scope in the declaration for foo. Since x occurs
1784 AFTER the splice containing the match, the logic does not find any splices after
1785 x but before or at its match, and so we report nothing about x's scope. If we
1786 had not checked whether x occurs before the splice, we would have instead
1787 reported that x is not in scope before the splice. While correct, such an error
1788 message is more likely to confuse than to enlighten.
1789 -}
1790
1791 {-
1792 ************************************************************************
1793 * *
1794 Equality errors
1795 * *
1796 ************************************************************************
1797
1798 Note [Inaccessible code]
1799 ~~~~~~~~~~~~~~~~~~~~~~~~
1800 Consider
1801 data T a where
1802 T1 :: T a
1803 T2 :: T Bool
1804
1805 f :: (a ~ Int) => T a -> Int
1806 f T1 = 3
1807 f T2 = 4 -- Unreachable code
1808
1809 Here the second equation is unreachable. The original constraint
1810 (a~Int) from the signature gets rewritten by the pattern-match to
1811 (Bool~Int), so the danger is that we report the error as coming from
1812 the *signature* (Trac #7293). So, for Given errors we replace the
1813 env (and hence src-loc) on its CtLoc with that from the immediately
1814 enclosing implication.
1815
1816 Note [Error messages for untouchables]
1817 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1818 Consider (Trac #9109)
1819 data G a where { GBool :: G Bool }
1820 foo x = case x of GBool -> True
1821
1822 Here we can't solve (t ~ Bool), where t is the untouchable result
1823 meta-var 't', because of the (a ~ Bool) from the pattern match.
1824 So we infer the type
1825 f :: forall a t. G a -> t
1826 making the meta-var 't' into a skolem. So when we come to report
1827 the unsolved (t ~ Bool), t won't look like an untouchable meta-var
1828 any more. So we don't assert that it is.
1829 -}
1830
1831 -- Don't have multiple equality errors from the same location
1832 -- E.g. (Int,Bool) ~ (Bool,Int) one error will do!
1833 mkEqErr :: ReportErrCtxt -> [Ct] -> TcM ErrMsg
1834 mkEqErr ctxt (ct:_) = mkEqErr1 ctxt ct
1835 mkEqErr _ [] = panic "mkEqErr"
1836
1837 mkEqErr1 :: ReportErrCtxt -> Ct -> TcM ErrMsg
1838 mkEqErr1 ctxt ct -- Wanted or derived;
1839 -- givens handled in mkGivenErrorReporter
1840 = do { (ctxt, binds_msg, ct) <- relevantBindings True ctxt ct
1841 ; rdr_env <- getGlobalRdrEnv
1842 ; fam_envs <- tcGetFamInstEnvs
1843 ; exp_syns <- goptM Opt_PrintExpandedSynonyms
1844 ; let (keep_going, is_oriented, wanted_msg)
1845 = mk_wanted_extra (ctLoc ct) exp_syns
1846 coercible_msg = case ctEqRel ct of
1847 NomEq -> empty
1848 ReprEq -> mkCoercibleExplanation rdr_env fam_envs ty1 ty2
1849 ; dflags <- getDynFlags
1850 ; traceTc "mkEqErr1" (ppr ct $$ pprCtOrigin (ctOrigin ct) $$ ppr keep_going)
1851 ; let report = mconcat [important wanted_msg, important coercible_msg,
1852 relevant_bindings binds_msg]
1853 ; if keep_going
1854 then mkEqErr_help dflags ctxt report ct is_oriented ty1 ty2
1855 else mkErrorMsgFromCt ctxt ct report }
1856 where
1857 (ty1, ty2) = getEqPredTys (ctPred ct)
1858
1859 -- If the types in the error message are the same as the types
1860 -- we are unifying, don't add the extra expected/actual message
1861 mk_wanted_extra :: CtLoc -> Bool -> (Bool, Maybe SwapFlag, SDoc)
1862 mk_wanted_extra loc expandSyns
1863 = case ctLocOrigin loc of
1864 orig@TypeEqOrigin {} -> mkExpectedActualMsg ty1 ty2 orig
1865 t_or_k expandSyns
1866 where
1867 t_or_k = ctLocTypeOrKind_maybe loc
1868
1869 KindEqOrigin cty1 mb_cty2 sub_o sub_t_or_k
1870 -> (True, Nothing, msg1 $$ msg2)
1871 where
1872 sub_what = case sub_t_or_k of Just KindLevel -> text "kinds"
1873 _ -> text "types"
1874 msg1 = sdocWithDynFlags $ \dflags ->
1875 case mb_cty2 of
1876 Just cty2
1877 | gopt Opt_PrintExplicitCoercions dflags
1878 || not (cty1 `pickyEqType` cty2)
1879 -> hang (text "When matching" <+> sub_what)
1880 2 (vcat [ ppr cty1 <+> dcolon <+>
1881 ppr (typeKind cty1)
1882 , ppr cty2 <+> dcolon <+>
1883 ppr (typeKind cty2) ])
1884 _ -> text "When matching the kind of" <+> quotes (ppr cty1)
1885 msg2 = case sub_o of
1886 TypeEqOrigin {}
1887 | Just cty2 <- mb_cty2 ->
1888 thdOf3 (mkExpectedActualMsg cty1 cty2 sub_o sub_t_or_k
1889 expandSyns)
1890 _ -> empty
1891 _ -> (True, Nothing, empty)
1892
1893 -- | This function tries to reconstruct why a "Coercible ty1 ty2" constraint
1894 -- is left over.
1895 mkCoercibleExplanation :: GlobalRdrEnv -> FamInstEnvs
1896 -> TcType -> TcType -> SDoc
1897 mkCoercibleExplanation rdr_env fam_envs ty1 ty2
1898 | Just (tc, tys) <- tcSplitTyConApp_maybe ty1
1899 , (rep_tc, _, _) <- tcLookupDataFamInst fam_envs tc tys
1900 , Just msg <- coercible_msg_for_tycon rep_tc
1901 = msg
1902 | Just (tc, tys) <- splitTyConApp_maybe ty2
1903 , (rep_tc, _, _) <- tcLookupDataFamInst fam_envs tc tys
1904 , Just msg <- coercible_msg_for_tycon rep_tc
1905 = msg
1906 | Just (s1, _) <- tcSplitAppTy_maybe ty1
1907 , Just (s2, _) <- tcSplitAppTy_maybe ty2
1908 , s1 `eqType` s2
1909 , has_unknown_roles s1
1910 = hang (text "NB: We cannot know what roles the parameters to" <+>
1911 quotes (ppr s1) <+> text "have;")
1912 2 (text "we must assume that the role is nominal")
1913 | otherwise
1914 = empty
1915 where
1916 coercible_msg_for_tycon tc
1917 | isAbstractTyCon tc
1918 = Just $ hsep [ text "NB: The type constructor"
1919 , quotes (pprSourceTyCon tc)
1920 , text "is abstract" ]
1921 | isNewTyCon tc
1922 , [data_con] <- tyConDataCons tc
1923 , let dc_name = dataConName data_con
1924 , isNothing (lookupGRE_Name rdr_env dc_name)
1925 = Just $ hang (text "The data constructor" <+> quotes (ppr dc_name))
1926 2 (sep [ text "of newtype" <+> quotes (pprSourceTyCon tc)
1927 , text "is not in scope" ])
1928 | otherwise = Nothing
1929
1930 has_unknown_roles ty
1931 | Just (tc, tys) <- tcSplitTyConApp_maybe ty
1932 = tys `lengthAtLeast` tyConArity tc -- oversaturated tycon
1933 | Just (s, _) <- tcSplitAppTy_maybe ty
1934 = has_unknown_roles s
1935 | isTyVarTy ty
1936 = True
1937 | otherwise
1938 = False
1939
1940 {-
1941 -- | Make a listing of role signatures for all the parameterised tycons
1942 -- used in the provided types
1943
1944
1945 -- SLPJ Jun 15: I could not convince myself that these hints were really
1946 -- useful. Maybe they are, but I think we need more work to make them
1947 -- actually helpful.
1948 mkRoleSigs :: Type -> Type -> SDoc
1949 mkRoleSigs ty1 ty2
1950 = ppUnless (null role_sigs) $
1951 hang (text "Relevant role signatures:")
1952 2 (vcat role_sigs)
1953 where
1954 tcs = nameEnvElts $ tyConsOfType ty1 `plusNameEnv` tyConsOfType ty2
1955 role_sigs = mapMaybe ppr_role_sig tcs
1956
1957 ppr_role_sig tc
1958 | null roles -- if there are no parameters, don't bother printing
1959 = Nothing
1960 | isBuiltInSyntax (tyConName tc) -- don't print roles for (->), etc.
1961 = Nothing
1962 | otherwise
1963 = Just $ hsep $ [text "type role", ppr tc] ++ map ppr roles
1964 where
1965 roles = tyConRoles tc
1966 -}
1967
1968 mkEqErr_help :: DynFlags -> ReportErrCtxt -> Report
1969 -> Ct
1970 -> Maybe SwapFlag -- Nothing <=> not sure
1971 -> TcType -> TcType -> TcM ErrMsg
1972 mkEqErr_help dflags ctxt report ct oriented ty1 ty2
1973 | Just (tv1, co1) <- tcGetCastedTyVar_maybe ty1
1974 = mkTyVarEqErr dflags ctxt report ct oriented tv1 co1 ty2
1975 | Just (tv2, co2) <- tcGetCastedTyVar_maybe ty2
1976 = mkTyVarEqErr dflags ctxt report ct swapped tv2 co2 ty1
1977 | otherwise
1978 = reportEqErr ctxt report ct oriented ty1 ty2
1979 where
1980 swapped = fmap flipSwap oriented
1981
1982 reportEqErr :: ReportErrCtxt -> Report
1983 -> Ct
1984 -> Maybe SwapFlag -- Nothing <=> not sure
1985 -> TcType -> TcType -> TcM ErrMsg
1986 reportEqErr ctxt report ct oriented ty1 ty2
1987 = mkErrorMsgFromCt ctxt ct (mconcat [misMatch, report, eqInfo])
1988 where misMatch = important $ misMatchOrCND ctxt ct oriented ty1 ty2
1989 eqInfo = important $ mkEqInfoMsg ct ty1 ty2
1990
1991 mkTyVarEqErr, mkTyVarEqErr'
1992 :: DynFlags -> ReportErrCtxt -> Report -> Ct
1993 -> Maybe SwapFlag -> TcTyVar -> TcCoercionN -> TcType -> TcM ErrMsg
1994 -- tv1 and ty2 are already tidied
1995 mkTyVarEqErr dflags ctxt report ct oriented tv1 co1 ty2
1996 = do { traceTc "mkTyVarEqErr" (ppr ct $$ ppr tv1 $$ ppr co1 $$ ppr ty2)
1997 ; mkTyVarEqErr' dflags ctxt report ct oriented tv1 co1 ty2 }
1998
1999 mkTyVarEqErr' dflags ctxt report ct oriented tv1 co1 ty2
2000 | not insoluble_occurs_check -- See Note [Occurs check wins]
2001 , isUserSkolem ctxt tv1 -- ty2 won't be a meta-tyvar, or else the thing would
2002 -- be oriented the other way round;
2003 -- see TcCanonical.canEqTyVarTyVar
2004 || isSigTyVar tv1 && not (isTyVarTy ty2)
2005 || ctEqRel ct == ReprEq
2006 -- the cases below don't really apply to ReprEq (except occurs check)
2007 = mkErrorMsgFromCt ctxt ct $ mconcat
2008 [ important $ misMatchOrCND ctxt ct oriented ty1 ty2
2009 , important $ extraTyVarEqInfo ctxt tv1 ty2
2010 , report
2011 ]
2012
2013 | OC_Occurs <- occ_check_expand
2014 -- We report an "occurs check" even for a ~ F t a, where F is a type
2015 -- function; it's not insoluble (because in principle F could reduce)
2016 -- but we have certainly been unable to solve it
2017 -- See Note [Occurs check error] in TcCanonical
2018 = do { let main_msg = addArising (ctOrigin ct) $
2019 hang (text "Occurs check: cannot construct the infinite" <+> what <> colon)
2020 2 (sep [ppr ty1, char '~', ppr ty2])
2021
2022 extra2 = important $ mkEqInfoMsg ct ty1 ty2
2023
2024 interesting_tyvars = filter (not . noFreeVarsOfType . tyVarKind) $
2025 filter isTyVar $
2026 fvVarList $
2027 tyCoFVsOfType ty1 `unionFV` tyCoFVsOfType ty2
2028 extra3 = relevant_bindings $
2029 ppWhen (not (null interesting_tyvars)) $
2030 hang (text "Type variable kinds:") 2 $
2031 vcat (map (tyvar_binding . tidyTyVarOcc (cec_tidy ctxt))
2032 interesting_tyvars)
2033
2034 tyvar_binding tv = ppr tv <+> dcolon <+> ppr (tyVarKind tv)
2035 ; mkErrorMsgFromCt ctxt ct $
2036 mconcat [important main_msg, extra2, extra3, report] }
2037
2038 | OC_Bad <- occ_check_expand
2039 = do { let msg = vcat [ text "Cannot instantiate unification variable"
2040 <+> quotes (ppr tv1)
2041 , hang (text "with a" <+> what <+> text "involving foralls:") 2 (ppr ty2)
2042 , nest 2 (text "GHC doesn't yet support impredicative polymorphism") ]
2043 -- Unlike the other reports, this discards the old 'report_important'
2044 -- instead of augmenting it. This is because the details are not likely
2045 -- to be helpful since this is just an unimplemented feature.
2046 ; mkErrorMsgFromCt ctxt ct $ report { report_important = [msg] } }
2047
2048 -- check for heterogeneous equality next; see Note [Equalities with incompatible kinds]
2049 -- in TcCanonical
2050 | not (k1 `tcEqType` k2)
2051 = do { let main_msg = addArising (ctOrigin ct) $
2052 vcat [ hang (text "Kind mismatch: cannot unify" <+>
2053 parens (ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1)) <+>
2054 text "with:")
2055 2 (sep [ppr ty2, dcolon, ppr k2])
2056 , text "Their kinds differ." ]
2057 cast_msg
2058 | isTcReflexiveCo co1 = empty
2059 | otherwise = text "NB:" <+> ppr tv1 <+>
2060 text "was casted to have kind" <+>
2061 quotes (ppr k1)
2062
2063 ; mkErrorMsgFromCt ctxt ct (mconcat [important main_msg, important cast_msg, report]) }
2064
2065 -- If the immediately-enclosing implication has 'tv' a skolem, and
2066 -- we know by now its an InferSkol kind of skolem, then presumably
2067 -- it started life as a SigTv, else it'd have been unified, given
2068 -- that there's no occurs-check or forall problem
2069 | (implic:_) <- cec_encl ctxt
2070 , Implic { ic_skols = skols } <- implic
2071 , tv1 `elem` skols
2072 = mkErrorMsgFromCt ctxt ct $ mconcat
2073 [ important $ misMatchMsg ct oriented ty1 ty2
2074 , important $ extraTyVarEqInfo ctxt tv1 ty2
2075 , report
2076 ]
2077
2078 -- Check for skolem escape
2079 | (implic:_) <- cec_encl ctxt -- Get the innermost context
2080 , Implic { ic_env = env, ic_skols = skols, ic_info = skol_info } <- implic
2081 , let esc_skols = filter (`elemVarSet` (tyCoVarsOfType ty2)) skols
2082 , not (null esc_skols)
2083 = do { let msg = important $ misMatchMsg ct oriented ty1 ty2
2084 esc_doc = sep [ text "because" <+> what <+> text "variable" <> plural esc_skols
2085 <+> pprQuotedList esc_skols
2086 , text "would escape" <+>
2087 if isSingleton esc_skols then text "its scope"
2088 else text "their scope" ]
2089 tv_extra = important $
2090 vcat [ nest 2 $ esc_doc
2091 , sep [ (if isSingleton esc_skols
2092 then text "This (rigid, skolem)" <+>
2093 what <+> text "variable is"
2094 else text "These (rigid, skolem)" <+>
2095 what <+> text "variables are")
2096 <+> text "bound by"
2097 , nest 2 $ ppr skol_info
2098 , nest 2 $ text "at" <+> ppr (tcl_loc env) ] ]
2099 ; mkErrorMsgFromCt ctxt ct (mconcat [msg, tv_extra, report]) }
2100
2101 -- Nastiest case: attempt to unify an untouchable variable
2102 -- So tv is a meta tyvar (or started that way before we
2103 -- generalised it). So presumably it is an *untouchable*
2104 -- meta tyvar or a SigTv, else it'd have been unified
2105 -- See Note [Error messages for untouchables]
2106 | (implic:_) <- cec_encl ctxt -- Get the innermost context
2107 , Implic { ic_env = env, ic_given = given
2108 , ic_tclvl = lvl, ic_info = skol_info } <- implic
2109 = ASSERT2( not (isTouchableMetaTyVar lvl tv1)
2110 , ppr tv1 $$ ppr lvl ) -- See Note [Error messages for untouchables]
2111 do { let msg = important $ misMatchMsg ct oriented ty1 ty2
2112 tclvl_extra = important $
2113 nest 2 $
2114 sep [ quotes (ppr tv1) <+> text "is untouchable"
2115 , nest 2 $ text "inside the constraints:" <+> pprEvVarTheta given
2116 , nest 2 $ text "bound by" <+> ppr skol_info
2117 , nest 2 $ text "at" <+> ppr (tcl_loc env) ]
2118 tv_extra = important $ extraTyVarEqInfo ctxt tv1 ty2
2119 add_sig = important $ suggestAddSig ctxt ty1 ty2
2120 ; mkErrorMsgFromCt ctxt ct $ mconcat
2121 [msg, tclvl_extra, tv_extra, add_sig, report] }
2122
2123 | otherwise
2124 = reportEqErr ctxt report ct oriented (mkTyVarTy tv1) ty2
2125 -- This *can* happen (Trac #6123, and test T2627b)
2126 -- Consider an ambiguous top-level constraint (a ~ F a)
2127 -- Not an occurs check, because F is a type function.
2128 where
2129 Pair _ k1 = tcCoercionKind co1
2130 k2 = typeKind ty2
2131
2132 ty1 = mkTyVarTy tv1
2133 occ_check_expand = occCheckForErrors dflags tv1 ty2
2134 insoluble_occurs_check = isInsolubleOccursCheck (ctEqRel ct) tv1 ty2
2135
2136 what = case ctLocTypeOrKind_maybe (ctLoc ct) of
2137 Just KindLevel -> text "kind"
2138 _ -> text "type"
2139
2140 mkEqInfoMsg :: Ct -> TcType -> TcType -> SDoc
2141 -- Report (a) ambiguity if either side is a type function application
2142 -- e.g. F a0 ~ Int
2143 -- (b) warning about injectivity if both sides are the same
2144 -- type function application F a ~ F b
2145 -- See Note [Non-injective type functions]
2146 -- (c) warning about -fprint-explicit-kinds if that might be helpful
2147 mkEqInfoMsg ct ty1 ty2
2148 = tyfun_msg $$ ambig_msg $$ invis_msg
2149 where
2150 mb_fun1 = isTyFun_maybe ty1
2151 mb_fun2 = isTyFun_maybe ty2
2152
2153 ambig_msg | isJust mb_fun1 || isJust mb_fun2
2154 = snd (mkAmbigMsg False ct)
2155 | otherwise = empty
2156
2157 -- better to check the exp/act types in the CtOrigin than the actual
2158 -- mismatched types for suggestion about -fprint-explicit-kinds
2159 (act_ty, exp_ty) = case ctOrigin ct of
2160 TypeEqOrigin { uo_actual = act
2161 , uo_expected = exp } -> (act, exp)
2162 _ -> (ty1, ty2)
2163
2164 invis_msg | Just vis <- tcEqTypeVis act_ty exp_ty
2165 , not vis
2166 = ppSuggestExplicitKinds
2167 | otherwise
2168 = empty
2169
2170 tyfun_msg | Just tc1 <- mb_fun1
2171 , Just tc2 <- mb_fun2
2172 , tc1 == tc2
2173 , not (isInjectiveTyCon tc1 Nominal)
2174 = text "NB:" <+> quotes (ppr tc1)
2175 <+> text "is a non-injective type family"
2176 | otherwise = empty
2177
2178 isUserSkolem :: ReportErrCtxt -> TcTyVar -> Bool
2179 -- See Note [Reporting occurs-check errors]
2180 isUserSkolem ctxt tv
2181 = isSkolemTyVar tv && any is_user_skol_tv (cec_encl ctxt)
2182 where
2183 is_user_skol_tv (Implic { ic_skols = sks, ic_info = skol_info })
2184 = tv `elem` sks && is_user_skol_info skol_info
2185
2186 is_user_skol_info (InferSkol {}) = False
2187 is_user_skol_info _ = True
2188
2189 misMatchOrCND :: ReportErrCtxt -> Ct
2190 -> Maybe SwapFlag -> TcType -> TcType -> SDoc
2191 -- If oriented then ty1 is actual, ty2 is expected
2192 misMatchOrCND ctxt ct oriented ty1 ty2
2193 | null givens ||
2194 (isRigidTy ty1 && isRigidTy ty2) ||
2195 isGivenCt ct
2196 -- If the equality is unconditionally insoluble
2197 -- or there is no context, don't report the context
2198 = misMatchMsg ct oriented ty1 ty2
2199 | otherwise
2200 = couldNotDeduce givens ([eq_pred], orig)
2201 where
2202 ev = ctEvidence ct
2203 eq_pred = ctEvPred ev
2204 orig = ctEvOrigin ev
2205 givens = [ given | given <- getUserGivens ctxt, not (ic_no_eqs given)]
2206 -- Keep only UserGivens that have some equalities
2207
2208 couldNotDeduce :: [UserGiven] -> (ThetaType, CtOrigin) -> SDoc
2209 couldNotDeduce givens (wanteds, orig)
2210 = vcat [ addArising orig (text "Could not deduce:" <+> pprTheta wanteds)
2211 , vcat (pp_givens givens)]
2212
2213 pp_givens :: [UserGiven] -> [SDoc]
2214 pp_givens givens
2215 = case givens of
2216 [] -> []
2217 (g:gs) -> ppr_given (text "from the context:") g
2218 : map (ppr_given (text "or from:")) gs
2219 where
2220 ppr_given herald (Implic { ic_given = gs, ic_info = skol_info
2221 , ic_env = env })
2222 = hang (herald <+> pprEvVarTheta gs)
2223 2 (sep [ text "bound by" <+> ppr skol_info
2224 , text "at" <+> ppr (tcl_loc env) ])
2225
2226 extraTyVarEqInfo :: ReportErrCtxt -> TcTyVar -> TcType -> SDoc
2227 -- Add on extra info about skolem constants
2228 -- NB: The types themselves are already tidied
2229 extraTyVarEqInfo ctxt tv1 ty2
2230 = extraTyVarInfo ctxt tv1 $$ ty_extra ty2
2231 where
2232 ty_extra ty = case tcGetTyVar_maybe ty of
2233 Just tv -> extraTyVarInfo ctxt tv
2234 Nothing -> empty
2235
2236 extraTyVarInfo :: ReportErrCtxt -> TcTyVar -> SDoc
2237 extraTyVarInfo ctxt tv
2238 = ASSERT2( isTyVar tv, ppr tv )
2239 case tcTyVarDetails tv of
2240 SkolemTv {} -> pprSkols ctxt [tv]
2241 RuntimeUnk {} -> quotes (ppr tv) <+> text "is an interactive-debugger skolem"
2242 MetaTv {} -> empty
2243
2244 suggestAddSig :: ReportErrCtxt -> TcType -> TcType -> SDoc
2245 -- See Note [Suggest adding a type signature]
2246 suggestAddSig ctxt ty1 ty2
2247 | null inferred_bndrs
2248 = empty
2249 | [bndr] <- inferred_bndrs
2250 = text "Possible fix: add a type signature for" <+> quotes (ppr bndr)
2251 | otherwise
2252 = text "Possible fix: add type signatures for some or all of" <+> (ppr inferred_bndrs)
2253 where
2254 inferred_bndrs = nub (get_inf ty1 ++ get_inf ty2)
2255 get_inf ty | Just tv <- tcGetTyVar_maybe ty
2256 , isSkolemTyVar tv
2257 , (implic, _) : _ <- getSkolemInfo (cec_encl ctxt) [tv]
2258 , InferSkol prs <- ic_info implic
2259 = map fst prs
2260 | otherwise
2261 = []
2262
2263 --------------------
2264 misMatchMsg :: Ct -> Maybe SwapFlag -> TcType -> TcType -> SDoc
2265 -- Types are already tidy
2266 -- If oriented then ty1 is actual, ty2 is expected
2267 misMatchMsg ct oriented ty1 ty2
2268 | Just NotSwapped <- oriented
2269 = misMatchMsg ct (Just IsSwapped) ty2 ty1
2270
2271 -- These next two cases are when we're about to report, e.g., that
2272 -- 'LiftedRep doesn't match 'VoidRep. Much better just to say
2273 -- lifted vs. unlifted
2274 | Just (tc1, []) <- splitTyConApp_maybe ty1
2275 , tc1 `hasKey` liftedRepDataConKey
2276 = lifted_vs_unlifted
2277
2278 | Just (tc2, []) <- splitTyConApp_maybe ty2
2279 , tc2 `hasKey` liftedRepDataConKey
2280 = lifted_vs_unlifted
2281
2282 | otherwise -- So now we have Nothing or (Just IsSwapped)
2283 -- For some reason we treat Nothing like IsSwapped
2284 = addArising orig $
2285 sep [ text herald1 <+> quotes (ppr ty1)
2286 , nest padding $
2287 text herald2 <+> quotes (ppr ty2)
2288 , sameOccExtra ty2 ty1 ]
2289 where
2290 herald1 = conc [ "Couldn't match"
2291 , if is_repr then "representation of" else ""
2292 , if is_oriented then "expected" else ""
2293 , what ]
2294 herald2 = conc [ "with"
2295 , if is_repr then "that of" else ""
2296 , if is_oriented then ("actual " ++ what) else "" ]
2297 padding = length herald1 - length herald2
2298
2299 is_repr = case ctEqRel ct of { ReprEq -> True; NomEq -> False }
2300 is_oriented = isJust oriented
2301
2302 orig = ctOrigin ct
2303 what = case ctLocTypeOrKind_maybe (ctLoc ct) of
2304 Just KindLevel -> "kind"
2305 _ -> "type"
2306
2307 conc :: [String] -> String
2308 conc = foldr1 add_space
2309
2310 add_space :: String -> String -> String
2311 add_space s1 s2 | null s1 = s2
2312 | null s2 = s1
2313 | otherwise = s1 ++ (' ' : s2)
2314
2315 lifted_vs_unlifted
2316 = addArising orig $
2317 text "Couldn't match a lifted type with an unlifted type"
2318
2319 mkExpectedActualMsg :: Type -> Type -> CtOrigin -> Maybe TypeOrKind -> Bool
2320 -> (Bool, Maybe SwapFlag, SDoc)
2321 -- NotSwapped means (actual, expected), IsSwapped is the reverse
2322 -- First return val is whether or not to print a herald above this msg
2323 mkExpectedActualMsg ty1 ty2 (TypeEqOrigin { uo_actual = act
2324 , uo_expected = exp
2325 , uo_thing = maybe_thing })
2326 m_level printExpanded
2327 | KindLevel <- level, occurs_check_error = (True, Nothing, empty)
2328 | isUnliftedTypeKind act, isLiftedTypeKind exp = (False, Nothing, msg2)
2329 | isLiftedTypeKind act, isUnliftedTypeKind exp = (False, Nothing, msg3)
2330 | isLiftedTypeKind exp && not (isConstraintKind exp)
2331 = (False, Nothing, msg4)
2332 | Just msg <- num_args_msg = (False, Nothing, msg $$ msg1)
2333 | KindLevel <- level, Just th <- maybe_thing = (False, Nothing, msg5 th)
2334 | act `pickyEqType` ty1, exp `pickyEqType` ty2 = (True, Just NotSwapped, empty)
2335 | exp `pickyEqType` ty1, act `pickyEqType` ty2 = (True, Just IsSwapped, empty)
2336 | otherwise = (True, Nothing, msg1)
2337 where
2338 level = m_level `orElse` TypeLevel
2339
2340 occurs_check_error
2341 | Just act_tv <- tcGetTyVar_maybe act
2342 , act_tv `elemVarSet` tyCoVarsOfType exp
2343 = True
2344 | Just exp_tv <- tcGetTyVar_maybe exp
2345 , exp_tv `elemVarSet` tyCoVarsOfType act
2346 = True
2347 | otherwise
2348 = False
2349
2350 sort = case level of
2351 TypeLevel -> text "type"
2352 KindLevel -> text "kind"
2353
2354 msg1 = case level of
2355 KindLevel
2356 | Just th <- maybe_thing
2357 -> msg5 th
2358
2359 _ | not (act `pickyEqType` exp)
2360 -> vcat [ text "Expected" <+> sort <> colon <+> ppr exp
2361 , text " Actual" <+> sort <> colon <+> ppr act
2362 , if printExpanded then expandedTys else empty ]
2363
2364 | otherwise
2365 -> empty
2366
2367 thing_msg = case maybe_thing of
2368 Just thing -> \_ -> quotes thing <+> text "is"
2369 Nothing -> \vowel -> text "got a" <>
2370 if vowel then char 'n' else empty
2371 msg2 = sep [ text "Expecting a lifted type, but"
2372 , thing_msg True, text "unlifted" ]
2373 msg3 = sep [ text "Expecting an unlifted type, but"
2374 , thing_msg False, text "lifted" ]
2375 msg4 = maybe_num_args_msg $$
2376 sep [ text "Expected a type, but"
2377 , maybe (text "found something with kind")
2378 (\thing -> quotes thing <+> text "has kind")
2379 maybe_thing
2380 , quotes (pprWithTYPE act) ]
2381
2382 msg5 th = hang (text "Expected" <+> kind_desc <> comma)
2383 2 (text "but" <+> quotes th <+> text "has kind" <+>
2384 quotes (ppr act))
2385 where
2386 kind_desc | isConstraintKind exp = text "a constraint"
2387
2388 -- TYPE t0
2389 | Just (tc, [arg]) <- tcSplitTyConApp_maybe exp
2390 , tc `hasKey` tYPETyConKey
2391 , tcIsTyVarTy arg = sdocWithDynFlags $ \dflags ->
2392 if gopt Opt_PrintExplicitRuntimeReps dflags
2393 then text "kind" <+> quotes (ppr exp)
2394 else text "a type"
2395
2396 | otherwise = text "kind" <+> quotes (ppr exp)
2397
2398 num_args_msg = case level of
2399 KindLevel
2400 | not (isMetaTyVarTy exp) && not (isMetaTyVarTy act)
2401 -- if one is a meta-tyvar, then it's possible that the user
2402 -- has asked for something impredicative, and we couldn't unify.
2403 -- Don't bother with counting arguments.
2404 -> let n_act = count_args act
2405 n_exp = count_args exp in
2406 case n_act - n_exp of
2407 n | n > 0 -- we don't know how many args there are, so don't
2408 -- recommend removing args that aren't
2409 , Just thing <- maybe_thing
2410 -> Just $ text "Expecting" <+> speakN (abs n) <+>
2411 more <+> quotes thing
2412 where
2413 more
2414 | n == 1 = text "more argument to"
2415 | otherwise = text "more arguments to" -- n > 1
2416 _ -> Nothing
2417
2418 _ -> Nothing
2419
2420 maybe_num_args_msg = case num_args_msg of
2421 Nothing -> empty
2422 Just m -> m
2423
2424 count_args ty = count isVisibleBinder $ fst $ splitPiTys ty
2425
2426 expandedTys =
2427 ppUnless (expTy1 `pickyEqType` exp && expTy2 `pickyEqType` act) $ vcat
2428 [ text "Type synonyms expanded:"
2429 , text "Expected type:" <+> ppr expTy1
2430 , text " Actual type:" <+> ppr expTy2
2431 ]
2432
2433 (expTy1, expTy2) = expandSynonymsToMatch exp act
2434
2435 mkExpectedActualMsg _ _ _ _ _ = panic "mkExpectedAcutalMsg"
2436
2437 {- Note [Insoluble occurs check wins]
2438 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2439 Consider [G] a ~ [a], [W] a ~ [a] (Trac #13674). The Given is insoluble
2440 so we don't use it for rewriting. The Wanted is also insoluble, and
2441 we don't solve it from the Given. It's very confusing to say
2442 Cannot solve a ~ [a] from given constraints a ~ [a]
2443
2444 And indeed even thinking about the Givens is silly; [W] a ~ [a] is
2445 just as insoluble as Int ~ Bool.
2446
2447 Conclusion: if there's an insoluble occurs check (isInsolubleOccursCheck)
2448 then report it first.
2449
2450 (NB: there are potentially-soluble ones, like (a ~ F a b), and we don't
2451 want to be as draconian with them.)
2452
2453 Note [Expanding type synonyms to make types similar]
2454 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2455
2456 In type error messages, if -fprint-expanded-types is used, we want to expand
2457 type synonyms to make expected and found types as similar as possible, but we
2458 shouldn't expand types too much to make type messages even more verbose and
2459 harder to understand. The whole point here is to make the difference in expected
2460 and found types clearer.
2461
2462 `expandSynonymsToMatch` does this, it takes two types, and expands type synonyms
2463 only as much as necessary. Given two types t1 and t2:
2464
2465 * If they're already same, it just returns the types.
2466
2467 * If they're in form `C1 t1_1 .. t1_n` and `C2 t2_1 .. t2_m` (C1 and C2 are
2468 type constructors), it expands C1 and C2 if they're different type synonyms.
2469 Then it recursively does the same thing on expanded types. If C1 and C2 are
2470 same, then it applies the same procedure to arguments of C1 and arguments of
2471 C2 to make them as similar as possible.
2472
2473 Most important thing here is to keep number of synonym expansions at
2474 minimum. For example, if t1 is `T (T3, T5, Int)` and t2 is `T (T5, T3,
2475 Bool)` where T5 = T4, T4 = T3, ..., T1 = X, it returns `T (T3, T3, Int)` and
2476 `T (T3, T3, Bool)`.
2477
2478 * Otherwise types don't have same shapes and so the difference is clearly
2479 visible. It doesn't do any expansions and show these types.
2480
2481 Note that we only expand top-layer type synonyms. Only when top-layer
2482 constructors are the same we start expanding inner type synonyms.
2483
2484 Suppose top-layer type synonyms of t1 and t2 can expand N and M times,
2485 respectively. If their type-synonym-expanded forms will meet at some point (i.e.
2486 will have same shapes according to `sameShapes` function), it's possible to find
2487 where they meet in O(N+M) top-layer type synonym expansions and O(min(N,M))
2488 comparisons. We first collect all the top-layer expansions of t1 and t2 in two
2489 lists, then drop the prefix of the longer list so that they have same lengths.
2490 Then we search through both lists in parallel, and return the first pair of
2491 types that have same shapes. Inner types of these two types with same shapes
2492 are then expanded using the same algorithm.
2493
2494 In case they don't meet, we return the last pair of types in the lists, which
2495 has top-layer type synonyms completely expanded. (in this case the inner types
2496 are not expanded at all, as the current form already shows the type error)
2497 -}
2498
2499 -- | Expand type synonyms in given types only enough to make them as similar as
2500 -- possible. Returned types are the same in terms of used type synonyms.
2501 --
2502 -- To expand all synonyms, see 'Type.expandTypeSynonyms'.
2503 --
2504 -- See `ExpandSynsFail` tests in tests testsuite/tests/typecheck/should_fail for
2505 -- some examples of how this should work.
2506 expandSynonymsToMatch :: Type -> Type -> (Type, Type)
2507 expandSynonymsToMatch ty1 ty2 = (ty1_ret, ty2_ret)
2508 where
2509 (ty1_ret, ty2_ret) = go ty1 ty2
2510
2511 -- | Returns (type synonym expanded version of first type,
2512 -- type synonym expanded version of second type)
2513 go :: Type -> Type -> (Type, Type)
2514 go t1 t2
2515 | t1 `pickyEqType` t2 =
2516 -- Types are same, nothing to do
2517 (t1, t2)
2518
2519 go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
2520 | tc1 == tc2 =
2521 -- Type constructors are same. They may be synonyms, but we don't
2522 -- expand further.
2523 let (tys1', tys2') =
2524 unzip (zipWith (\ty1 ty2 -> go ty1 ty2) tys1 tys2)
2525 in (TyConApp tc1 tys1', TyConApp tc2 tys2')
2526
2527 go (AppTy t1_1 t1_2) (AppTy t2_1 t2_2) =
2528 let (t1_1', t2_1') = go t1_1 t2_1
2529 (t1_2', t2_2') = go t1_2 t2_2
2530 in (mkAppTy t1_1' t1_2', mkAppTy t2_1' t2_2')
2531
2532 go (FunTy t1_1 t1_2) (FunTy t2_1 t2_2) =
2533 let (t1_1', t2_1') = go t1_1 t2_1
2534 (t1_2', t2_2') = go t1_2 t2_2
2535 in (mkFunTy t1_1' t1_2', mkFunTy t2_1' t2_2')
2536
2537 go (ForAllTy b1 t1) (ForAllTy b2 t2) =
2538 -- NOTE: We may have a bug here, but we just can't reproduce it easily.
2539 -- See D1016 comments for details and our attempts at producing a test
2540 -- case. Short version: We probably need RnEnv2 to really get this right.
2541 let (t1', t2') = go t1 t2
2542 in (ForAllTy b1 t1', ForAllTy b2 t2')
2543
2544 go (CastTy ty1 _) ty2 = go ty1 ty2
2545 go ty1 (CastTy ty2 _) = go ty1 ty2
2546
2547 go t1 t2 =
2548 -- See Note [Expanding type synonyms to make types similar] for how this
2549 -- works
2550 let
2551 t1_exp_tys = t1 : tyExpansions t1
2552 t2_exp_tys = t2 : tyExpansions t2
2553 t1_exps = length t1_exp_tys
2554 t2_exps = length t2_exp_tys
2555 dif = abs (t1_exps - t2_exps)
2556 in
2557 followExpansions $
2558 zipEqual "expandSynonymsToMatch.go"
2559 (if t1_exps > t2_exps then drop dif t1_exp_tys else t1_exp_tys)
2560 (if t2_exps > t1_exps then drop dif t2_exp_tys else t2_exp_tys)
2561
2562 -- | Expand the top layer type synonyms repeatedly, collect expansions in a
2563 -- list. The list does not include the original type.
2564 --
2565 -- Example, if you have:
2566 --
2567 -- type T10 = T9
2568 -- type T9 = T8
2569 -- ...
2570 -- type T0 = Int
2571 --
2572 -- `tyExpansions T10` returns [T9, T8, T7, ... Int]
2573 --
2574 -- This only expands the top layer, so if you have:
2575 --
2576 -- type M a = Maybe a
2577 --
2578 -- `tyExpansions (M T10)` returns [Maybe T10] (T10 is not expanded)
2579 tyExpansions :: Type -> [Type]
2580 tyExpansions = unfoldr (\t -> (\x -> (x, x)) `fmap` tcView t)
2581
2582 -- | Drop the type pairs until types in a pair look alike (i.e. the outer
2583 -- constructors are the same).
2584 followExpansions :: [(Type, Type)] -> (Type, Type)
2585 followExpansions [] = pprPanic "followExpansions" empty
2586 followExpansions [(t1, t2)]
2587 | sameShapes t1 t2 = go t1 t2 -- expand subtrees
2588 | otherwise = (t1, t2) -- the difference is already visible
2589 followExpansions ((t1, t2) : tss)
2590 -- Traverse subtrees when the outer shapes are the same
2591 | sameShapes t1 t2 = go t1 t2
2592 -- Otherwise follow the expansions until they look alike
2593 | otherwise = followExpansions tss
2594
2595 sameShapes :: Type -> Type -> Bool
2596 sameShapes AppTy{} AppTy{} = True
2597 sameShapes (TyConApp tc1 _) (TyConApp tc2 _) = tc1 == tc2
2598 sameShapes (FunTy {}) (FunTy {}) = True
2599 sameShapes (ForAllTy {}) (ForAllTy {}) = True
2600 sameShapes (CastTy ty1 _) ty2 = sameShapes ty1 ty2
2601 sameShapes ty1 (CastTy ty2 _) = sameShapes ty1 ty2
2602 sameShapes _ _ = False
2603
2604 sameOccExtra :: TcType -> TcType -> SDoc
2605 -- See Note [Disambiguating (X ~ X) errors]
2606 sameOccExtra ty1 ty2
2607 | Just (tc1, _) <- tcSplitTyConApp_maybe ty1
2608 , Just (tc2, _) <- tcSplitTyConApp_maybe ty2
2609 , let n1 = tyConName tc1
2610 n2 = tyConName tc2
2611 same_occ = nameOccName n1 == nameOccName n2
2612 same_pkg = moduleUnitId (nameModule n1) == moduleUnitId (nameModule n2)
2613 , n1 /= n2 -- Different Names
2614 , same_occ -- but same OccName
2615 = text "NB:" <+> (ppr_from same_pkg n1 $$ ppr_from same_pkg n2)
2616 | otherwise
2617 = empty
2618 where
2619 ppr_from same_pkg nm
2620 | isGoodSrcSpan loc
2621 = hang (quotes (ppr nm) <+> text "is defined at")
2622 2 (ppr loc)
2623 | otherwise -- Imported things have an UnhelpfulSrcSpan
2624 = hang (quotes (ppr nm))
2625 2 (sep [ text "is defined in" <+> quotes (ppr (moduleName mod))
2626 , ppUnless (same_pkg || pkg == mainUnitId) $
2627 nest 4 $ text "in package" <+> quotes (ppr pkg) ])
2628 where
2629 pkg = moduleUnitId mod
2630 mod = nameModule nm
2631 loc = nameSrcSpan nm
2632
2633 {-
2634 Note [Suggest adding a type signature]
2635 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2636 The OutsideIn algorithm rejects GADT programs that don't have a principal
2637 type, and indeed some that do. Example:
2638 data T a where
2639 MkT :: Int -> T Int
2640
2641 f (MkT n) = n
2642
2643 Does this have type f :: T a -> a, or f :: T a -> Int?
2644 The error that shows up tends to be an attempt to unify an
2645 untouchable type variable. So suggestAddSig sees if the offending
2646 type variable is bound by an *inferred* signature, and suggests
2647 adding a declared signature instead.
2648
2649 This initially came up in Trac #8968, concerning pattern synonyms.
2650
2651 Note [Disambiguating (X ~ X) errors]
2652 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2653 See Trac #8278
2654
2655 Note [Reporting occurs-check errors]
2656 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2657 Given (a ~ [a]), if 'a' is a rigid type variable bound by a user-supplied
2658 type signature, then the best thing is to report that we can't unify
2659 a with [a], because a is a skolem variable. That avoids the confusing
2660 "occur-check" error message.
2661
2662 But nowadays when inferring the type of a function with no type signature,
2663 even if there are errors inside, we still generalise its signature and
2664 carry on. For example
2665 f x = x:x
2666 Here we will infer something like
2667 f :: forall a. a -> [a]
2668 with a deferred error of (a ~ [a]). So in the deferred unsolved constraint
2669 'a' is now a skolem, but not one bound by the programmer in the context!
2670 Here we really should report an occurs check.
2671
2672 So isUserSkolem distinguishes the two.
2673
2674 Note [Non-injective type functions]
2675 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2676 It's very confusing to get a message like
2677 Couldn't match expected type `Depend s'
2678 against inferred type `Depend s1'
2679 so mkTyFunInfoMsg adds:
2680 NB: `Depend' is type function, and hence may not be injective
2681
2682 Warn of loopy local equalities that were dropped.
2683
2684
2685 ************************************************************************
2686 * *
2687 Type-class errors
2688 * *
2689 ************************************************************************
2690 -}
2691
2692 mkDictErr :: ReportErrCtxt -> [Ct] -> TcM ErrMsg
2693 mkDictErr ctxt cts
2694 = ASSERT( not (null cts) )
2695 do { inst_envs <- tcGetInstEnvs
2696 ; let (ct1:_) = cts -- ct1 just for its location
2697 min_cts = elim_superclasses cts
2698 lookups = map (lookup_cls_inst inst_envs) min_cts
2699 (no_inst_cts, overlap_cts) = partition is_no_inst lookups
2700
2701 -- Report definite no-instance errors,
2702 -- or (iff there are none) overlap errors
2703 -- But we report only one of them (hence 'head') because they all
2704 -- have the same source-location origin, to try avoid a cascade
2705 -- of error from one location
2706 ; (ctxt, err) <- mk_dict_err ctxt (head (no_inst_cts ++ overlap_cts))
2707 ; mkErrorMsgFromCt ctxt ct1 (important err) }
2708 where
2709 no_givens = null (getUserGivens ctxt)
2710
2711 is_no_inst (ct, (matches, unifiers, _))
2712 = no_givens
2713 && null matches
2714 && (null unifiers || all (not . isAmbiguousTyVar) (tyCoVarsOfCtList ct))
2715
2716 lookup_cls_inst inst_envs ct
2717 -- Note [Flattening in error message generation]
2718 = (ct, lookupInstEnv True inst_envs clas (flattenTys emptyInScopeSet tys))
2719 where
2720 (clas, tys) = getClassPredTys (ctPred ct)
2721
2722
2723 -- When simplifying [W] Ord (Set a), we need
2724 -- [W] Eq a, [W] Ord a
2725 -- but we really only want to report the latter
2726 elim_superclasses cts = mkMinimalBySCs ctPred cts
2727
2728 mk_dict_err :: ReportErrCtxt -> (Ct, ClsInstLookupResult)
2729 -> TcM (ReportErrCtxt, SDoc)
2730 -- Report an overlap error if this class constraint results
2731 -- from an overlap (returning Left clas), otherwise return (Right pred)
2732 mk_dict_err ctxt@(CEC {cec_encl = implics}) (ct, (matches, unifiers, unsafe_overlapped))
2733 | null matches -- No matches but perhaps several unifiers
2734 = do { (ctxt, binds_msg, ct) <- relevantBindings True ctxt ct
2735 ; candidate_insts <- get_candidate_instances
2736 ; return (ctxt, cannot_resolve_msg ct candidate_insts binds_msg) }
2737
2738 | null unsafe_overlapped -- Some matches => overlap errors
2739 = return (ctxt, overlap_msg)
2740
2741 | otherwise
2742 = return (ctxt, safe_haskell_msg)
2743 where
2744 orig = ctOrigin ct
2745 pred = ctPred ct
2746 (clas, tys) = getClassPredTys pred
2747 ispecs = [ispec | (ispec, _) <- matches]
2748 unsafe_ispecs = [ispec | (ispec, _) <- unsafe_overlapped]
2749 useful_givens = discardProvCtxtGivens orig (getUserGivensFromImplics implics)
2750 -- useful_givens are the enclosing implications with non-empty givens,
2751 -- modulo the horrid discardProvCtxtGivens
2752
2753 get_candidate_instances :: TcM [ClsInst]
2754 -- See Note [Report candidate instances]
2755 get_candidate_instances
2756 | [ty] <- tys -- Only try for single-parameter classes
2757 = do { instEnvs <- tcGetInstEnvs
2758 ; return (filter (is_candidate_inst ty)
2759 (classInstances instEnvs clas)) }
2760 | otherwise = return []
2761
2762 is_candidate_inst ty inst -- See Note [Report candidate instances]
2763 | [other_ty] <- is_tys inst
2764 , Just (tc1, _) <- tcSplitTyConApp_maybe ty
2765 , Just (tc2, _) <- tcSplitTyConApp_maybe other_ty
2766 = let n1 = tyConName tc1
2767 n2 = tyConName tc2
2768 different_names = n1 /= n2
2769 same_occ_names = nameOccName n1 == nameOccName n2
2770 in different_names && same_occ_names
2771 | otherwise = False
2772
2773 cannot_resolve_msg :: Ct -> [ClsInst] -> SDoc -> SDoc
2774 cannot_resolve_msg ct candidate_insts binds_msg
2775 = vcat [ no_inst_msg
2776 , nest 2 extra_note
2777 , vcat (pp_givens useful_givens)
2778 , mb_patsyn_prov `orElse` empty
2779 , ppWhen (has_ambig_tvs && not (null unifiers && null useful_givens))
2780 (vcat [ ppUnless lead_with_ambig ambig_msg, binds_msg, potential_msg ])
2781
2782 , ppWhen (isNothing mb_patsyn_prov) $
2783 -- Don't suggest fixes for the provided context of a pattern
2784 -- synonym; the right fix is to bind more in the pattern
2785 show_fixes (ctxtFixes has_ambig_tvs pred implics
2786 ++ drv_fixes)
2787 , ppWhen (not (null candidate_insts))
2788 (hang (text "There are instances for similar types:")
2789 2 (vcat (map ppr candidate_insts))) ]
2790 -- See Note [Report candidate instances]
2791 where
2792 orig = ctOrigin ct
2793 -- See Note [Highlighting ambiguous type variables]
2794 lead_with_ambig = has_ambig_tvs && not (any isRuntimeUnkSkol ambig_tvs)
2795 && not (null unifiers) && null useful_givens
2796
2797 (has_ambig_tvs, ambig_msg) = mkAmbigMsg lead_with_ambig ct
2798 ambig_tvs = uncurry (++) (getAmbigTkvs ct)
2799
2800 no_inst_msg
2801 | lead_with_ambig
2802 = ambig_msg <+> pprArising orig
2803 $$ text "prevents the constraint" <+> quotes (pprParendType pred)
2804 <+> text "from being solved."
2805
2806 | null useful_givens
2807 = addArising orig $ text "No instance for"
2808 <+> pprParendType pred
2809
2810 | otherwise
2811 = addArising orig $ text "Could not deduce"
2812 <+> pprParendType pred
2813
2814 potential_msg
2815 = ppWhen (not (null unifiers) && want_potential orig) $
2816 sdocWithDynFlags $ \dflags ->
2817 getPprStyle $ \sty ->
2818 pprPotentials dflags sty potential_hdr unifiers
2819
2820 potential_hdr
2821 = vcat [ ppWhen lead_with_ambig $
2822 text "Probable fix: use a type annotation to specify what"
2823 <+> pprQuotedList ambig_tvs <+> text "should be."
2824 , text "These potential instance" <> plural unifiers
2825 <+> text "exist:"]
2826
2827 mb_patsyn_prov :: Maybe SDoc
2828 mb_patsyn_prov
2829 | not lead_with_ambig
2830 , ProvCtxtOrigin PSB{ psb_def = L _ pat } <- orig
2831 = Just (vcat [ text "In other words, a successful match on the pattern"
2832 , nest 2 $ ppr pat
2833 , text "does not provide the constraint" <+> pprParendType pred ])
2834 | otherwise = Nothing
2835
2836 -- Report "potential instances" only when the constraint arises
2837 -- directly from the user's use of an overloaded function
2838 want_potential (TypeEqOrigin {}) = False
2839 want_potential _ = True
2840
2841 extra_note | any isFunTy (filterOutInvisibleTypes (classTyCon clas) tys)
2842 = text "(maybe you haven't applied a function to enough arguments?)"
2843 | className clas == typeableClassName -- Avoid mysterious "No instance for (Typeable T)
2844 , [_,ty] <- tys -- Look for (Typeable (k->*) (T k))
2845 , Just (tc,_) <- tcSplitTyConApp_maybe ty
2846 , not (isTypeFamilyTyCon tc)
2847 = hang (text "GHC can't yet do polykinded")
2848 2 (text "Typeable" <+>
2849 parens (ppr ty <+> dcolon <+> ppr (typeKind ty)))
2850 | otherwise
2851 = empty
2852
2853 drv_fixes = case orig of
2854 DerivClauseOrigin -> [drv_fix False]
2855 StandAloneDerivOrigin -> [drv_fix True]
2856 DerivOriginDC _ _ standalone -> [drv_fix standalone]
2857 DerivOriginCoerce _ _ _ standalone -> [drv_fix standalone]
2858 _ -> []
2859
2860 drv_fix standalone_wildcard
2861 | standalone_wildcard
2862 = text "fill in the wildcard constraint yourself"
2863 | otherwise
2864 = hang (text "use a standalone 'deriving instance' declaration,")
2865 2 (text "so you can specify the instance context yourself")
2866
2867 -- Normal overlap error
2868 overlap_msg
2869 = ASSERT( not (null matches) )
2870 vcat [ addArising orig (text "Overlapping instances for"
2871 <+> pprType (mkClassPred clas tys))
2872
2873 , ppUnless (null matching_givens) $
2874 sep [text "Matching givens (or their superclasses):"
2875 , nest 2 (vcat matching_givens)]
2876
2877 , sdocWithDynFlags $ \dflags ->
2878 getPprStyle $ \sty ->
2879 pprPotentials dflags sty (text "Matching instances:") $
2880 ispecs ++ unifiers
2881
2882 , ppWhen (null matching_givens && isSingleton matches && null unifiers) $
2883 -- Intuitively, some given matched the wanted in their
2884 -- flattened or rewritten (from given equalities) form
2885 -- but the matcher can't figure that out because the
2886 -- constraints are non-flat and non-rewritten so we
2887 -- simply report back the whole given
2888 -- context. Accelerate Smart.hs showed this problem.
2889 sep [ text "There exists a (perhaps superclass) match:"
2890 , nest 2 (vcat (pp_givens useful_givens))]
2891
2892 , ppWhen (isSingleton matches) $
2893 parens (vcat [ text "The choice depends on the instantiation of" <+>
2894 quotes (pprWithCommas ppr (tyCoVarsOfTypesList tys))
2895 , ppWhen (null (matching_givens)) $
2896 vcat [ text "To pick the first instance above, use IncoherentInstances"
2897 , text "when compiling the other instance declarations"]
2898 ])]
2899
2900 matching_givens = mapMaybe matchable useful_givens
2901
2902 matchable (Implic { ic_given = evvars, ic_info = skol_info, ic_env = env })
2903 = case ev_vars_matching of
2904 [] -> Nothing
2905 _ -> Just $ hang (pprTheta ev_vars_matching)
2906 2 (sep [ text "bound by" <+> ppr skol_info
2907 , text "at" <+> ppr (tcl_loc env) ])
2908 where ev_vars_matching = filter ev_var_matches (map evVarPred evvars)
2909 ev_var_matches ty = case getClassPredTys_maybe ty of
2910 Just (clas', tys')
2911 | clas' == clas
2912 , Just _ <- tcMatchTys tys tys'
2913 -> True
2914 | otherwise
2915 -> any ev_var_matches (immSuperClasses clas' tys')
2916 Nothing -> False
2917
2918 -- Overlap error because of Safe Haskell (first
2919 -- match should be the most specific match)
2920 safe_haskell_msg
2921 = ASSERT( matches `lengthIs` 1 && not (null unsafe_ispecs) )
2922 vcat [ addArising orig (text "Unsafe overlapping instances for"
2923 <+> pprType (mkClassPred clas tys))
2924 , sep [text "The matching instance is:",
2925 nest 2 (pprInstance $ head ispecs)]
2926 , vcat [ text "It is compiled in a Safe module and as such can only"
2927 , text "overlap instances from the same module, however it"
2928 , text "overlaps the following instances from different" <+>
2929 text "modules:"
2930 , nest 2 (vcat [pprInstances $ unsafe_ispecs])
2931 ]
2932 ]
2933
2934
2935 ctxtFixes :: Bool -> PredType -> [Implication] -> [SDoc]
2936 ctxtFixes has_ambig_tvs pred implics
2937 | not has_ambig_tvs
2938 , isTyVarClassPred pred
2939 , (skol:skols) <- usefulContext implics pred
2940 , let what | null skols
2941 , SigSkol (PatSynCtxt {}) _ _ <- skol
2942 = text "\"required\""
2943 | otherwise
2944 = empty
2945 = [sep [ text "add" <+> pprParendType pred
2946 <+> text "to the" <+> what <+> text "context of"
2947 , nest 2 $ ppr_skol skol $$
2948 vcat [ text "or" <+> ppr_skol skol
2949 | skol <- skols ] ] ]
2950 | otherwise = []
2951 where
2952 ppr_skol (PatSkol (RealDataCon dc) _) = text "the data constructor" <+> quotes (ppr dc)
2953 ppr_skol (PatSkol (PatSynCon ps) _) = text "the pattern synonym" <+> quotes (ppr ps)
2954 ppr_skol skol_info = ppr skol_info
2955
2956 discardProvCtxtGivens :: CtOrigin -> [UserGiven] -> [UserGiven]
2957 discardProvCtxtGivens orig givens -- See Note [discardProvCtxtGivens]
2958 | ProvCtxtOrigin (PSB {psb_id = L _ name}) <- orig
2959 = filterOut (discard name) givens
2960 | otherwise
2961 = givens
2962 where
2963 discard n (Implic { ic_info = SigSkol (PatSynCtxt n') _ _ }) = n == n'
2964 discard _ _ = False
2965
2966 usefulContext :: [Implication] -> PredType -> [SkolemInfo]
2967 -- usefulContext picks out the implications whose context
2968 -- the programmer might plausibly augment to solve 'pred'
2969 usefulContext implics pred
2970 = go implics
2971 where
2972 pred_tvs = tyCoVarsOfType pred
2973 go [] = []
2974 go (ic : ics)
2975 | implausible ic = rest
2976 | otherwise = ic_info ic : rest
2977 where
2978 -- Stop when the context binds a variable free in the predicate
2979 rest | any (`elemVarSet` pred_tvs) (ic_skols ic) = []
2980 | otherwise = go ics
2981
2982 implausible ic
2983 | null (ic_skols ic) = True
2984 | implausible_info (ic_info ic) = True
2985 | otherwise = False
2986
2987 implausible_info (SigSkol (InfSigCtxt {}) _ _) = True
2988 implausible_info _ = False
2989 -- Do not suggest adding constraints to an *inferred* type signature
2990
2991 {- Note [Report candidate instances]
2992 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2993 If we have an unsolved (Num Int), where `Int` is not the Prelude Int,
2994 but comes from some other module, then it may be helpful to point out
2995 that there are some similarly named instances elsewhere. So we get
2996 something like
2997 No instance for (Num Int) arising from the literal ‘3’
2998 There are instances for similar types:
2999 instance Num GHC.Types.Int -- Defined in ‘GHC.Num’
3000 Discussion in Trac #9611.
3001
3002 Note [Highlighting ambiguous type variables]
3003 ~-------------------------------------------
3004 When we encounter ambiguous type variables (i.e. type variables
3005 that remain metavariables after type inference), we need a few more
3006 conditions before we can reason that *ambiguity* prevents constraints
3007 from being solved:
3008 - We can't have any givens, as encountering a typeclass error
3009 with given constraints just means we couldn't deduce
3010 a solution satisfying those constraints and as such couldn't
3011 bind the type variable to a known type.
3012 - If we don't have any unifiers, we don't even have potential
3013 instances from which an ambiguity could arise.
3014 - Lastly, I don't want to mess with error reporting for
3015 unknown runtime types so we just fall back to the old message there.
3016 Once these conditions are satisfied, we can safely say that ambiguity prevents
3017 the constraint from being solved.
3018
3019 Note [discardProvCtxtGivens]
3020 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
3021 In most situations we call all enclosing implications "useful". There is one
3022 exception, and that is when the constraint that causes the error is from the
3023 "provided" context of a pattern synonym declaration:
3024
3025 pattern Pat :: (Num a, Eq a) => Show a => a -> Maybe a
3026 -- required => provided => type
3027 pattern Pat x <- (Just x, 4)
3028
3029 When checking the pattern RHS we must check that it does actually bind all
3030 the claimed "provided" constraints; in this case, does the pattern (Just x, 4)
3031 bind the (Show a) constraint. Answer: no!
3032
3033 But the implication we generate for this will look like
3034 forall a. (Num a, Eq a) => [W] Show a
3035 because when checking the pattern we must make the required
3036 constraints available, since they are needed to match the pattern (in
3037 this case the literal '4' needs (Num a, Eq a)).
3038
3039 BUT we don't want to suggest adding (Show a) to the "required" constraints
3040 of the pattern synonym, thus:
3041 pattern Pat :: (Num a, Eq a, Show a) => Show a => a -> Maybe a
3042 It would then typecheck but it's silly. We want the /pattern/ to bind
3043 the alleged "provided" constraints, Show a.
3044
3045 So we suppress that Implication in discardProvCtxtGivens. It's
3046 painfully ad-hoc but the truth is that adding it to the "required"
3047 constraints would work. Suprressing it solves two problems. First,
3048 we never tell the user that we could not deduce a "provided"
3049 constraint from the "required" context. Second, we never give a
3050 possible fix that suggests to add a "provided" constraint to the
3051 "required" context.
3052
3053 For example, without this distinction the above code gives a bad error
3054 message (showing both problems):
3055
3056 error: Could not deduce (Show a) ... from the context: (Eq a)
3057 ... Possible fix: add (Show a) to the context of
3058 the signature for pattern synonym `Pat' ...
3059
3060 -}
3061
3062 show_fixes :: [SDoc] -> SDoc
3063 show_fixes [] = empty
3064 show_fixes (f:fs) = sep [ text "Possible fix:"
3065 , nest 2 (vcat (f : map (text "or" <+>) fs))]
3066
3067 pprPotentials :: DynFlags -> PprStyle -> SDoc -> [ClsInst] -> SDoc
3068 -- See Note [Displaying potential instances]
3069 pprPotentials dflags sty herald insts
3070 | null insts
3071 = empty
3072
3073 | null show_these
3074 = hang herald
3075 2 (vcat [ not_in_scope_msg empty
3076 , flag_hint ])
3077
3078 | otherwise
3079 = hang herald
3080 2 (vcat [ pprInstances show_these
3081 , ppWhen (n_in_scope_hidden > 0) $
3082 text "...plus"
3083 <+> speakNOf n_in_scope_hidden (text "other")
3084 , not_in_scope_msg (text "...plus")
3085 , flag_hint ])
3086 where
3087 n_show = 3 :: Int
3088 show_potentials = gopt Opt_PrintPotentialInstances dflags
3089
3090 (in_scope, not_in_scope) = partition inst_in_scope insts
3091 sorted = sortBy fuzzyClsInstCmp in_scope
3092 show_these | show_potentials = sorted
3093 | otherwise = take n_show sorted
3094 n_in_scope_hidden = length sorted - length show_these
3095
3096 -- "in scope" means that all the type constructors
3097 -- are lexically in scope; these instances are likely
3098 -- to be more useful
3099 inst_in_scope :: ClsInst -> Bool
3100 inst_in_scope cls_inst = nameSetAll name_in_scope $
3101 orphNamesOfTypes (is_tys cls_inst)
3102
3103 name_in_scope name
3104 | isBuiltInSyntax name
3105 = True -- E.g. (->)
3106 | Just mod <- nameModule_maybe name
3107 = qual_in_scope (qualName sty mod (nameOccName name))
3108 | otherwise
3109 = True
3110
3111 qual_in_scope :: QualifyName -> Bool
3112 qual_in_scope NameUnqual = True
3113 qual_in_scope (NameQual {}) = True
3114 qual_in_scope _ = False
3115
3116 not_in_scope_msg herald
3117 | null not_in_scope
3118 = empty
3119 | otherwise
3120 = hang (herald <+> speakNOf (length not_in_scope) (text "instance")
3121 <+> text "involving out-of-scope types")
3122 2 (ppWhen show_potentials (pprInstances not_in_scope))
3123
3124 flag_hint = ppUnless (show_potentials || equalLength show_these insts) $
3125 text "(use -fprint-potential-instances to see them all)"
3126
3127 {- Note [Displaying potential instances]
3128 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
3129 When showing a list of instances for
3130 - overlapping instances (show ones that match)
3131 - no such instance (show ones that could match)
3132 we want to give it a bit of structure. Here's the plan
3133
3134 * Say that an instance is "in scope" if all of the
3135 type constructors it mentions are lexically in scope.
3136 These are the ones most likely to be useful to the programmer.
3137
3138 * Show at most n_show in-scope instances,
3139 and summarise the rest ("plus 3 others")
3140
3141 * Summarise the not-in-scope instances ("plus 4 not in scope")
3142
3143 * Add the flag -fshow-potential-instances which replaces the
3144 summary with the full list
3145 -}
3146
3147 {-
3148 Note [Flattening in error message generation]
3149 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
3150 Consider (C (Maybe (F x))), where F is a type function, and we have
3151 instances
3152 C (Maybe Int) and C (Maybe a)
3153 Since (F x) might turn into Int, this is an overlap situation, and
3154 indeed (because of flattening) the main solver will have refrained
3155 from solving. But by the time we get to error message generation, we've
3156 un-flattened the constraint. So we must *re*-flatten it before looking
3157 up in the instance environment, lest we only report one matching
3158 instance when in fact there are two.
3159
3160 Re-flattening is pretty easy, because we don't need to keep track of
3161 evidence. We don't re-use the code in TcCanonical because that's in
3162 the TcS monad, and we are in TcM here.
3163
3164 Note [Suggest -fprint-explicit-kinds]
3165 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
3166 It can be terribly confusing to get an error message like (Trac #9171)
3167 Couldn't match expected type ‘GetParam Base (GetParam Base Int)’
3168 with actual type ‘GetParam Base (GetParam Base Int)’
3169 The reason may be that the kinds don't match up. Typically you'll get
3170 more useful information, but not when it's as a result of ambiguity.
3171 This test suggests -fprint-explicit-kinds when all the ambiguous type
3172 variables are kind variables.
3173 -}
3174
3175 mkAmbigMsg :: Bool -- True when message has to be at beginning of sentence
3176 -> Ct -> (Bool, SDoc)
3177 mkAmbigMsg prepend_msg ct
3178 | null ambig_kvs && null ambig_tvs = (False, empty)
3179 | otherwise = (True, msg)
3180 where
3181 (ambig_kvs, ambig_tvs) = getAmbigTkvs ct
3182
3183 msg | any isRuntimeUnkSkol ambig_kvs -- See Note [Runtime skolems]
3184 || any isRuntimeUnkSkol ambig_tvs
3185 = vcat [ text "Cannot resolve unknown runtime type"
3186 <> plural ambig_tvs <+> pprQuotedList ambig_tvs
3187 , text "Use :print or :force to determine these types"]
3188
3189 | not (null ambig_tvs)
3190 = pp_ambig (text "type") ambig_tvs
3191
3192 | otherwise -- All ambiguous kind variabes; suggest -fprint-explicit-kinds
3193 -- See Note [Suggest -fprint-explicit-kinds]
3194 = vcat [ pp_ambig (text "kind") ambig_kvs
3195 , ppSuggestExplicitKinds ]
3196
3197 pp_ambig what tkvs
3198 | prepend_msg -- "Ambiguous type variable 't0'"
3199 = text "Ambiguous" <+> what <+> text "variable"
3200 <> plural tkvs <+> pprQuotedList tkvs
3201
3202 | otherwise -- "The type variable 't0' is ambiguous"
3203 = text "The" <+> what <+> text "variable" <> plural tkvs
3204 <+> pprQuotedList tkvs <+> is_or_are tkvs <+> text "ambiguous"
3205
3206 is_or_are [_] = text "is"
3207 is_or_are _ = text "are"
3208
3209 pprSkols :: ReportErrCtxt -> [TcTyVar] -> SDoc
3210 pprSkols ctxt tvs
3211 = vcat (map pp_one (getSkolemInfo (cec_encl ctxt) tvs))
3212 where
3213 pp_one (Implic { ic_info = skol_info }, tvs)
3214 | UnkSkol <- skol_info
3215 = hang (pprQuotedList tvs)
3216 2 (is_or_are tvs "an" "unknown")
3217 | otherwise
3218 = vcat [ hang (pprQuotedList tvs)
3219 2 (is_or_are tvs "a" "rigid" <+> text "bound by")
3220 , nest 2 (pprSkolInfo skol_info)
3221 , nest 2 (text "at" <+> ppr (foldr1 combineSrcSpans (map getSrcSpan tvs))) ]
3222
3223 is_or_are [_] article adjective = text "is" <+> text article <+> text adjective
3224 <+> text "type variable"
3225 is_or_are _ _ adjective = text "are" <+> text adjective
3226 <+> text "type variables"
3227
3228 getAmbigTkvs :: Ct -> ([Var],[Var])
3229 getAmbigTkvs ct
3230 = partition (`elemVarSet` dep_tkv_set) ambig_tkvs
3231 where
3232 tkvs = tyCoVarsOfCtList ct
3233 ambig_tkvs = filter isAmbiguousTyVar tkvs
3234 dep_tkv_set = tyCoVarsOfTypes (map tyVarKind tkvs)
3235
3236 getSkolemInfo :: [Implication] -> [TcTyVar]
3237 -> [(Implication, [TcTyVar])]
3238 -- Get the skolem info for some type variables
3239 -- from the implication constraints that bind them
3240 --
3241 -- In the returned (implic, tvs) pairs, the 'tvs' part is non-empty
3242 getSkolemInfo _ []
3243 = []
3244
3245 getSkolemInfo [] tvs
3246 = pprPanic "No skolem info:" (ppr tvs)
3247
3248 getSkolemInfo (implic:implics) tvs
3249 | null tvs_here = getSkolemInfo implics tvs
3250 | otherwise = (implic, tvs_here) : getSkolemInfo implics tvs_other
3251 where
3252 (tvs_here, tvs_other) = partition (`elem` ic_skols implic) tvs
3253
3254 -----------------------
3255 -- relevantBindings looks at the value environment and finds values whose
3256 -- types mention any of the offending type variables. It has to be
3257 -- careful to zonk the Id's type first, so it has to be in the monad.
3258 -- We must be careful to pass it a zonked type variable, too.
3259 --
3260 -- We always remove closed top-level bindings, though,
3261 -- since they are never relevant (cf Trac #8233)
3262
3263 relevantBindings :: Bool -- True <=> filter by tyvar; False <=> no filtering
3264 -- See Trac #8191
3265 -> ReportErrCtxt -> Ct
3266 -> TcM (ReportErrCtxt, SDoc, Ct)
3267 -- Also returns the zonked and tidied CtOrigin of the constraint
3268 relevantBindings want_filtering ctxt ct
3269 = do { dflags <- getDynFlags
3270 ; (env1, tidy_orig) <- zonkTidyOrigin (cec_tidy ctxt) (ctLocOrigin loc)
3271 ; let ct_tvs = tyCoVarsOfCt ct `unionVarSet` extra_tvs
3272
3273 -- For *kind* errors, report the relevant bindings of the
3274 -- enclosing *type* equality, because that's more useful for the programmer
3275 extra_tvs = case tidy_orig of
3276 KindEqOrigin t1 m_t2 _ _ -> tyCoVarsOfTypes $
3277 t1 : maybeToList m_t2
3278 _ -> emptyVarSet
3279 ; traceTc "relevantBindings" $
3280 vcat [ ppr ct
3281 , pprCtOrigin (ctLocOrigin loc)
3282 , ppr ct_tvs
3283 , pprWithCommas id [ ppr id <+> dcolon <+> ppr (idType id)
3284 | TcIdBndr id _ <- tcl_bndrs lcl_env ]
3285 , pprWithCommas id
3286 [ ppr id | TcIdBndr_ExpType id _ _ <- tcl_bndrs lcl_env ] ]
3287
3288 ; (tidy_env', docs, discards)
3289 <- go dflags env1 ct_tvs (maxRelevantBinds dflags)
3290 emptyVarSet [] False
3291 (remove_shadowing $ tcl_bndrs lcl_env)
3292 -- tcl_bndrs has the innermost bindings first,
3293 -- which are probably the most relevant ones
3294
3295 ; let doc = ppUnless (null docs) $
3296 hang (text "Relevant bindings include")
3297 2 (vcat docs $$ ppWhen discards discardMsg)
3298
3299 -- Put a zonked, tidied CtOrigin into the Ct
3300 loc' = setCtLocOrigin loc tidy_orig
3301 ct' = setCtLoc ct loc'
3302 ctxt' = ctxt { cec_tidy = tidy_env' }
3303
3304 ; return (ctxt', doc, ct') }
3305 where
3306 ev = ctEvidence ct
3307 loc = ctEvLoc ev
3308 lcl_env = ctLocEnv loc
3309
3310 run_out :: Maybe Int -> Bool
3311 run_out Nothing = False
3312 run_out (Just n) = n <= 0
3313
3314 dec_max :: Maybe Int -> Maybe Int
3315 dec_max = fmap (\n -> n - 1)
3316
3317 ---- fixes #12177
3318 ---- builds up a list of bindings whose OccName has not been seen before
3319 remove_shadowing :: [TcBinder] -> [TcBinder]
3320 remove_shadowing bindings = reverse $ fst $ foldl
3321 (\(bindingAcc, seenNames) binding ->
3322 if (occName binding) `elemOccSet` seenNames -- if we've seen it
3323 then (bindingAcc, seenNames) -- skip it
3324 else (binding:bindingAcc, extendOccSet seenNames (occName binding)))
3325 ([], emptyOccSet) bindings
3326
3327 go :: DynFlags -> TidyEnv -> TcTyVarSet -> Maybe Int -> TcTyVarSet -> [SDoc]
3328 -> Bool -- True <=> some filtered out due to lack of fuel
3329 -> [TcBinder]
3330 -> TcM (TidyEnv, [SDoc], Bool) -- The bool says if we filtered any out
3331 -- because of lack of fuel
3332 go _ tidy_env _ _ _ docs discards []
3333 = return (tidy_env, reverse docs, discards)
3334 go dflags tidy_env ct_tvs n_left tvs_seen docs discards (tc_bndr : tc_bndrs)
3335 = case tc_bndr of
3336 TcTvBndr {} -> discard_it
3337 TcIdBndr id top_lvl -> go2 (idName id) (idType id) top_lvl
3338 TcIdBndr_ExpType name et top_lvl ->
3339 do { mb_ty <- readExpType_maybe et
3340 -- et really should be filled in by now. But there's a chance
3341 -- it hasn't, if, say, we're reporting a kind error en route to
3342 -- checking a term. See test indexed-types/should_fail/T8129
3343 -- Or we are reporting errors from the ambiguity check on
3344 -- a local type signature
3345 ; case mb_ty of
3346 Just ty -> go2 name ty top_lvl
3347 Nothing -> discard_it -- No info; discard
3348 }
3349 where
3350 discard_it = go dflags tidy_env ct_tvs n_left tvs_seen docs
3351 discards tc_bndrs
3352 go2 id_name id_type top_lvl
3353 = do { (tidy_env', tidy_ty) <- zonkTidyTcType tidy_env id_type
3354 ; traceTc "relevantBindings 1" (ppr id_name <+> dcolon <+> ppr tidy_ty)
3355 ; let id_tvs = tyCoVarsOfType tidy_ty
3356 doc = sep [ pprPrefixOcc id_name <+> dcolon <+> ppr tidy_ty
3357 , nest 2 (parens (text "bound at"
3358 <+> ppr (getSrcLoc id_name)))]
3359 new_seen = tvs_seen `unionVarSet` id_tvs
3360
3361 ; if (want_filtering && not (hasPprDebug dflags)
3362 && id_tvs `disjointVarSet` ct_tvs)
3363 -- We want to filter out this binding anyway
3364 -- so discard it silently
3365 then discard_it
3366
3367 else if isTopLevel top_lvl && not (isNothing n_left)
3368 -- It's a top-level binding and we have not specified
3369 -- -fno-max-relevant-bindings, so discard it silently
3370 then discard_it
3371
3372 else if run_out n_left && id_tvs `subVarSet` tvs_seen
3373 -- We've run out of n_left fuel and this binding only
3374 -- mentions already-seen type variables, so discard it
3375 then go dflags tidy_env ct_tvs n_left tvs_seen docs
3376 True -- Record that we have now discarded something
3377 tc_bndrs
3378
3379 -- Keep this binding, decrement fuel
3380 else go dflags tidy_env' ct_tvs (dec_max n_left) new_seen
3381 (doc:docs) discards tc_bndrs }
3382
3383 discardMsg :: SDoc
3384 discardMsg = text "(Some bindings suppressed;" <+>
3385 text "use -fmax-relevant-binds=N or -fno-max-relevant-binds)"
3386
3387 subsDiscardMsg :: SDoc
3388 subsDiscardMsg =
3389 text "(Some substitutions suppressed;" <+>
3390 text "use -fmax-valid-substitutions=N or -fno-max-valid-substitutions)"
3391
3392 refSubsDiscardMsg :: SDoc
3393 refSubsDiscardMsg =
3394 text "(Some refinement substitutions suppressed;" <+>
3395 text "use -fmax-refinement-substitutions=N" <+>
3396 text "or -fno-max-refinement-substitutions)"
3397
3398 -----------------------
3399 warnDefaulting :: [Ct] -> Type -> TcM ()
3400 warnDefaulting wanteds default_ty
3401 = do { warn_default <- woptM Opt_WarnTypeDefaults
3402 ; env0 <- tcInitTidyEnv
3403 ; let tidy_env = tidyFreeTyCoVars env0 $
3404 tyCoVarsOfCtsList (listToBag wanteds)
3405 tidy_wanteds = map (tidyCt tidy_env) wanteds
3406 (loc, ppr_wanteds) = pprWithArising tidy_wanteds
3407 warn_msg =
3408 hang (hsep [ text "Defaulting the following"
3409 , text "constraint" <> plural tidy_wanteds
3410 , text "to type"
3411 , quotes (ppr default_ty) ])
3412 2
3413 ppr_wanteds
3414 ; setCtLocM loc $ warnTc (Reason Opt_WarnTypeDefaults) warn_default warn_msg }
3415
3416 {-
3417 Note [Runtime skolems]
3418 ~~~~~~~~~~~~~~~~~~~~~~
3419 We want to give a reasonably helpful error message for ambiguity
3420 arising from *runtime* skolems in the debugger. These
3421 are created by in RtClosureInspect.zonkRTTIType.
3422
3423 ************************************************************************
3424 * *
3425 Error from the canonicaliser
3426 These ones are called *during* constraint simplification
3427 * *
3428 ************************************************************************
3429 -}
3430
3431 solverDepthErrorTcS :: CtLoc -> TcType -> TcM a
3432 solverDepthErrorTcS loc ty
3433 = setCtLocM loc $
3434 do { ty <- zonkTcType ty
3435 ; env0 <- tcInitTidyEnv
3436 ; let tidy_env = tidyFreeTyCoVars env0 (tyCoVarsOfTypeList ty)
3437 tidy_ty = tidyType tidy_env ty
3438 msg
3439 = vcat [ text "Reduction stack overflow; size =" <+> ppr depth
3440 , hang (text "When simplifying the following type:")
3441 2 (ppr tidy_ty)
3442 , note ]
3443 ; failWithTcM (tidy_env, msg) }
3444 where
3445 depth = ctLocDepth loc
3446 note = vcat
3447 [ text "Use -freduction-depth=0 to disable this check"
3448 , text "(any upper bound you could choose might fail unpredictably with"
3449 , text " minor updates to GHC, so disabling the check is recommended if"
3450 , text " you're sure that type checking should terminate)" ]