Track type variable scope more carefully.
[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 {-
364 Note [Suppressing error messages]
365 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
366 The cec_suppress flag says "don't report any errors". Instead, just create
367 evidence bindings (as usual). It's used when more important errors have occurred.
368
369 Specifically (see reportWanteds)
370 * If there are insoluble Givens, then we are in unreachable code and all bets
371 are off. So don't report any further errors.
372 * If there are any insolubles (eg Int~Bool), here or in a nested implication,
373 then suppress errors from the simple constraints here. Sometimes the
374 simple-constraint errors are a knock-on effect of the insolubles.
375 -}
376
377 reportImplic :: ReportErrCtxt -> Implication -> TcM ()
378 reportImplic ctxt implic@(Implic { ic_skols = tvs, ic_telescope = m_telescope
379 , ic_given = given
380 , ic_wanted = wanted, ic_binds = evb
381 , ic_status = status, ic_info = info
382 , ic_env = tcl_env, ic_tclvl = tc_lvl })
383 | BracketSkol <- info
384 , not insoluble
385 = return () -- For Template Haskell brackets report only
386 -- definite errors. The whole thing will be re-checked
387 -- later when we plug it in, and meanwhile there may
388 -- certainly be un-satisfied constraints
389
390 | otherwise
391 = do { traceTc "reportImplic" (ppr implic')
392 ; reportWanteds ctxt' tc_lvl wanted
393 ; when (cec_warn_redundant ctxt) $
394 warnRedundantConstraints ctxt' tcl_env info' dead_givens
395 ; when bad_telescope $ reportBadTelescope ctxt tcl_env m_telescope tvs }
396 where
397 insoluble = isInsolubleStatus status
398 (env1, tvs') = mapAccumL tidyTyCoVarBndr (cec_tidy ctxt) tvs
399 info' = tidySkolemInfo env1 info
400 implic' = implic { ic_skols = tvs'
401 , ic_given = map (tidyEvVar env1) given
402 , ic_info = info' }
403 ctxt1 | NoEvBindsVar{} <- evb = noDeferredBindings ctxt
404 | termEvidenceAllowed info = ctxt
405 | otherwise = noDeferredBindings ctxt
406 -- If we go inside an implication that has no term
407 -- evidence (i.e. unifying under a forall), we can't defer
408 -- type errors. You could imagine using the /enclosing/
409 -- bindings (in cec_binds), but that may not have enough stuff
410 -- in scope for the bindings to be well typed. So we just
411 -- switch off deferred type errors altogether. See Trac #14605.
412
413 ctxt' = ctxt1 { cec_tidy = env1
414 , cec_encl = implic' : cec_encl ctxt
415
416 , cec_suppress = insoluble || cec_suppress ctxt
417 -- Suppress inessential errors if there
418 -- are insolubles anywhere in the
419 -- tree rooted here, or we've come across
420 -- a suppress-worthy constraint higher up (Trac #11541)
421
422 , cec_binds = evb }
423
424 dead_givens = case status of
425 IC_Solved { ics_dead = dead } -> dead
426 _ -> []
427
428 bad_telescope = case status of
429 IC_BadTelescope -> True
430 _ -> False
431
432 warnRedundantConstraints :: ReportErrCtxt -> TcLclEnv -> SkolemInfo -> [EvVar] -> TcM ()
433 -- See Note [Tracking redundant constraints] in TcSimplify
434 warnRedundantConstraints ctxt env info ev_vars
435 | null redundant_evs
436 = return ()
437
438 | SigSkol {} <- info
439 = setLclEnv env $ -- We want to add "In the type signature for f"
440 -- to the error context, which is a bit tiresome
441 addErrCtxt (text "In" <+> ppr info) $
442 do { env <- getLclEnv
443 ; msg <- mkErrorReport ctxt env (important doc)
444 ; reportWarning (Reason Opt_WarnRedundantConstraints) msg }
445
446 | otherwise -- But for InstSkol there already *is* a surrounding
447 -- "In the instance declaration for Eq [a]" context
448 -- and we don't want to say it twice. Seems a bit ad-hoc
449 = do { msg <- mkErrorReport ctxt env (important doc)
450 ; reportWarning (Reason Opt_WarnRedundantConstraints) msg }
451 where
452 doc = text "Redundant constraint" <> plural redundant_evs <> colon
453 <+> pprEvVarTheta redundant_evs
454
455 redundant_evs = case info of -- See Note [Redundant constraints in instance decls]
456 InstSkol -> filterOut improving ev_vars
457 _ -> ev_vars
458
459 improving ev_var = any isImprovementPred $
460 transSuperClasses (idType ev_var)
461
462 reportBadTelescope :: ReportErrCtxt -> TcLclEnv -> Maybe SDoc -> [TcTyVar] -> TcM ()
463 reportBadTelescope ctxt env (Just telescope) skols
464 = do { msg <- mkErrorReport ctxt env (important doc)
465 ; reportError msg }
466 where
467 doc = hang (text "These kind and type variables:" <+> telescope $$
468 text "are out of dependency order. Perhaps try this ordering:")
469 2 (pprTyVars sorted_tvs)
470
471 sorted_tvs = toposortTyVars skols
472
473 reportBadTelescope _ _ Nothing skols
474 = pprPanic "reportBadTelescope" (ppr skols)
475
476 {- Note [Redundant constraints in instance decls]
477 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
478 For instance declarations, we don't report unused givens if
479 they can give rise to improvement. Example (Trac #10100):
480 class Add a b ab | a b -> ab, a ab -> b
481 instance Add Zero b b
482 instance Add a b ab => Add (Succ a) b (Succ ab)
483 The context (Add a b ab) for the instance is clearly unused in terms
484 of evidence, since the dictionary has no fields. But it is still
485 needed! With the context, a wanted constraint
486 Add (Succ Zero) beta (Succ Zero)
487 we will reduce to (Add Zero beta Zero), and thence we get beta := Zero.
488 But without the context we won't find beta := Zero.
489
490 This only matters in instance declarations..
491 -}
492
493 reportWanteds :: ReportErrCtxt -> TcLevel -> WantedConstraints -> TcM ()
494 reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_impl = implics })
495 = do { traceTc "reportWanteds" (vcat [ text "Simples =" <+> ppr simples
496 , text "Suppress =" <+> ppr (cec_suppress ctxt)])
497 ; traceTc "rw2" (ppr tidy_cts)
498
499 -- First deal with things that are utterly wrong
500 -- Like Int ~ Bool (incl nullary TyCons)
501 -- or Int ~ t a (AppTy on one side)
502 -- These /ones/ are not suppressed by the incoming context
503 ; let ctxt_for_insols = ctxt { cec_suppress = False }
504 ; (ctxt1, cts1) <- tryReporters ctxt_for_insols report1 tidy_cts
505
506 -- Now all the other constraints. We suppress errors here if
507 -- any of the first batch failed, or if the enclosing context
508 -- says to suppress
509 ; let ctxt2 = ctxt { cec_suppress = cec_suppress ctxt || cec_suppress ctxt1 }
510 ; (_, leftovers) <- tryReporters ctxt2 report2 cts1
511 ; MASSERT2( null leftovers, ppr leftovers )
512
513 -- All the Derived ones have been filtered out of simples
514 -- by the constraint solver. This is ok; we don't want
515 -- to report unsolved Derived goals as errors
516 -- See Note [Do not report derived but soluble errors]
517
518 ; mapBagM_ (reportImplic ctxt2) implics }
519 -- NB ctxt1: don't suppress inner insolubles if there's only a
520 -- wanted insoluble here; but do suppress inner insolubles
521 -- if there's a *given* insoluble here (= inaccessible code)
522 where
523 env = cec_tidy ctxt
524 tidy_cts = bagToList (mapBag (tidyCt env) simples)
525
526 -- report1: ones that should *not* be suppresed by
527 -- an insoluble somewhere else in the tree
528 -- It's crucial that anything that is considered insoluble
529 -- (see TcRnTypes.insolubleWantedCt) is caught here, otherwise
530 -- we might suppress its error message, and proceed on past
531 -- type checking to get a Lint error later
532 report1 = [ ("custom_error", is_user_type_error,True, mkUserTypeErrorReporter)
533 , given_eq_spec
534 , ("insoluble2", utterly_wrong, True, mkGroupReporter mkEqErr)
535 , ("skolem eq1", very_wrong, True, mkSkolReporter)
536 , ("skolem eq2", skolem_eq, True, mkSkolReporter)
537 , ("non-tv eq", non_tv_eq, True, mkSkolReporter)
538 , ("Out of scope", is_out_of_scope,True, mkHoleReporter tidy_cts)
539 , ("Holes", is_hole, False, mkHoleReporter tidy_cts)
540
541 -- The only remaining equalities are alpha ~ ty,
542 -- where alpha is untouchable; and representational equalities
543 -- Prefer homogeneous equalities over hetero, because the
544 -- former might be holding up the latter.
545 -- See Note [Equalities with incompatible kinds] in TcCanonical
546 , ("Homo eqs", is_homo_equality, True, mkGroupReporter mkEqErr)
547 , ("Other eqs", is_equality, False, mkGroupReporter mkEqErr) ]
548
549 -- report2: we suppress these if there are insolubles elsewhere in the tree
550 report2 = [ ("Implicit params", is_ip, False, mkGroupReporter mkIPErr)
551 , ("Irreds", is_irred, False, mkGroupReporter mkIrredErr)
552 , ("Dicts", is_dict, False, mkGroupReporter mkDictErr) ]
553
554 -- rigid_nom_eq, rigid_nom_tv_eq,
555 is_hole, is_dict,
556 is_equality, is_ip, is_irred :: Ct -> PredTree -> Bool
557
558 is_given_eq ct pred
559 | EqPred {} <- pred = arisesFromGivens ct
560 | otherwise = False
561 -- I think all given residuals are equalities
562
563 -- Things like (Int ~N Bool)
564 utterly_wrong _ (EqPred NomEq ty1 ty2) = isRigidTy ty1 && isRigidTy ty2
565 utterly_wrong _ _ = False
566
567 -- Things like (a ~N Int)
568 very_wrong _ (EqPred NomEq ty1 ty2) = isSkolemTy tc_lvl ty1 && isRigidTy ty2
569 very_wrong _ _ = False
570
571 -- Things like (a ~N b) or (a ~N F Bool)
572 skolem_eq _ (EqPred NomEq ty1 _) = isSkolemTy tc_lvl ty1
573 skolem_eq _ _ = False
574
575 -- Things like (F a ~N Int)
576 non_tv_eq _ (EqPred NomEq ty1 _) = not (isTyVarTy ty1)
577 non_tv_eq _ _ = False
578
579 is_out_of_scope ct _ = isOutOfScopeCt ct
580 is_hole ct _ = isHoleCt ct
581
582 is_user_type_error ct _ = isUserTypeErrorCt ct
583
584 is_homo_equality _ (EqPred _ ty1 ty2) = typeKind ty1 `tcEqType` typeKind ty2
585 is_homo_equality _ _ = False
586
587 is_equality _ (EqPred {}) = True
588 is_equality _ _ = False
589
590 is_dict _ (ClassPred {}) = True
591 is_dict _ _ = False
592
593 is_ip _ (ClassPred cls _) = isIPClass cls
594 is_ip _ _ = False
595
596 is_irred _ (IrredPred {}) = True
597 is_irred _ _ = False
598
599 given_eq_spec = case find_gadt_match (cec_encl ctxt) of
600 Just imp -> ("insoluble1a", is_given_eq, True, mkGivenErrorReporter imp)
601 Nothing -> ("insoluble1b", is_given_eq, False, ignoreErrorReporter)
602 -- False means don't suppress subsequent errors
603 -- Reason: we don't report all given errors
604 -- (see mkGivenErrorReporter), and we should only suppress
605 -- subsequent errors if we actually report this one!
606 -- Trac #13446 is an example
607
608 find_gadt_match [] = Nothing
609 find_gadt_match (implic : implics)
610 | PatSkol {} <- ic_info implic
611 , not (ic_no_eqs implic)
612 = Just implic
613 | otherwise
614 = find_gadt_match implics
615
616 ---------------
617 isSkolemTy :: TcLevel -> Type -> Bool
618 -- The type is a skolem tyvar
619 isSkolemTy tc_lvl ty
620 | Just tv <- getTyVar_maybe ty
621 = isSkolemTyVar tv
622 || (isSigTyVar tv && isTouchableMetaTyVar tc_lvl tv)
623 -- The last case is for touchable SigTvs
624 -- we postpone untouchables to a latter test (too obscure)
625
626 | otherwise
627 = False
628
629 isTyFun_maybe :: Type -> Maybe TyCon
630 isTyFun_maybe ty = case tcSplitTyConApp_maybe ty of
631 Just (tc,_) | isTypeFamilyTyCon tc -> Just tc
632 _ -> Nothing
633
634 --------------------------------------------
635 -- Reporters
636 --------------------------------------------
637
638 type Reporter
639 = ReportErrCtxt -> [Ct] -> TcM ()
640 type ReporterSpec
641 = ( String -- Name
642 , Ct -> PredTree -> Bool -- Pick these ones
643 , Bool -- True <=> suppress subsequent reporters
644 , Reporter) -- The reporter itself
645
646 mkSkolReporter :: Reporter
647 -- Suppress duplicates with either the same LHS, or same location
648 mkSkolReporter ctxt cts
649 = mapM_ (reportGroup mkEqErr ctxt) (group cts)
650 where
651 group [] = []
652 group (ct:cts) = (ct : yeses) : group noes
653 where
654 (yeses, noes) = partition (group_with ct) cts
655
656 group_with ct1 ct2
657 | EQ <- cmp_loc ct1 ct2 = True
658 | eq_lhs_type ct1 ct2 = True
659 | otherwise = False
660
661 mkHoleReporter :: [Ct] -> Reporter
662 -- Reports errors one at a time
663 mkHoleReporter tidy_simples ctxt
664 = mapM_ $ \ct -> do { err <- mkHoleError tidy_simples ctxt ct
665 ; maybeReportHoleError ctxt ct err
666 ; maybeAddDeferredHoleBinding ctxt err ct }
667
668 mkUserTypeErrorReporter :: Reporter
669 mkUserTypeErrorReporter ctxt
670 = mapM_ $ \ct -> do { err <- mkUserTypeError ctxt ct
671 ; maybeReportError ctxt err
672 ; addDeferredBinding ctxt err ct }
673
674 mkUserTypeError :: ReportErrCtxt -> Ct -> TcM ErrMsg
675 mkUserTypeError ctxt ct = mkErrorMsgFromCt ctxt ct
676 $ important
677 $ pprUserTypeErrorTy
678 $ case getUserTypeErrorMsg ct of
679 Just msg -> msg
680 Nothing -> pprPanic "mkUserTypeError" (ppr ct)
681
682
683 mkGivenErrorReporter :: Implication -> Reporter
684 -- See Note [Given errors]
685 mkGivenErrorReporter implic ctxt cts
686 = do { (ctxt, binds_msg, ct) <- relevantBindings True ctxt ct
687 ; dflags <- getDynFlags
688 ; let ct' = setCtLoc ct (setCtLocEnv (ctLoc ct) (ic_env implic))
689 -- For given constraints we overwrite the env (and hence src-loc)
690 -- with one from the implication. See Note [Inaccessible code]
691
692 inaccessible_msg = hang (text "Inaccessible code in")
693 2 (ppr (ic_info implic))
694 report = important inaccessible_msg `mappend`
695 relevant_bindings binds_msg
696
697 ; err <- mkEqErr_help dflags ctxt report ct'
698 Nothing ty1 ty2
699
700 ; traceTc "mkGivenErrorReporter" (ppr ct)
701 ; maybeReportError ctxt err }
702 where
703 (ct : _ ) = cts -- Never empty
704 (ty1, ty2) = getEqPredTys (ctPred ct)
705
706 ignoreErrorReporter :: Reporter
707 -- Discard Given errors that don't come from
708 -- a pattern match; maybe we should warn instead?
709 ignoreErrorReporter ctxt cts
710 = do { traceTc "mkGivenErrorReporter no" (ppr cts $$ ppr (cec_encl ctxt))
711 ; return () }
712
713
714 {- Note [Given errors]
715 ~~~~~~~~~~~~~~~~~~~~~~
716 Given constraints represent things for which we have (or will have)
717 evidence, so they aren't errors. But if a Given constraint is
718 insoluble, this code is inaccessible, and we might want to at least
719 warn about that. A classic case is
720
721 data T a where
722 T1 :: T Int
723 T2 :: T a
724 T3 :: T Bool
725
726 f :: T Int -> Bool
727 f T1 = ...
728 f T2 = ...
729 f T3 = ... -- We want to report this case as inaccessible
730
731 We'd like to point out that the T3 match is inaccessible. It
732 will have a Given constraint [G] Int ~ Bool.
733
734 But we don't want to report ALL insoluble Given constraints. See Trac
735 #12466 for a long discussion. For example, if we aren't careful
736 we'll complain about
737 f :: ((Int ~ Bool) => a -> a) -> Int
738 which arguably is OK. It's more debatable for
739 g :: (Int ~ Bool) => Int -> Int
740 but it's tricky to distinguish these cases so we don't report
741 either.
742
743 The bottom line is this: find_gadt_match looks for an enclosing
744 pattern match which binds some equality constraints. If we
745 find one, we report the insoluble Given.
746 -}
747
748 mkGroupReporter :: (ReportErrCtxt -> [Ct] -> TcM ErrMsg)
749 -- Make error message for a group
750 -> Reporter -- Deal with lots of constraints
751 -- Group together errors from same location,
752 -- and report only the first (to avoid a cascade)
753 mkGroupReporter mk_err ctxt cts
754 = mapM_ (reportGroup mk_err ctxt . toList) (equivClasses cmp_loc cts)
755
756 eq_lhs_type :: Ct -> Ct -> Bool
757 eq_lhs_type ct1 ct2
758 = case (classifyPredType (ctPred ct1), classifyPredType (ctPred ct2)) of
759 (EqPred eq_rel1 ty1 _, EqPred eq_rel2 ty2 _) ->
760 (eq_rel1 == eq_rel2) && (ty1 `eqType` ty2)
761 _ -> pprPanic "mkSkolReporter" (ppr ct1 $$ ppr ct2)
762
763 cmp_loc :: Ct -> Ct -> Ordering
764 cmp_loc ct1 ct2 = ctLocSpan (ctLoc ct1) `compare` ctLocSpan (ctLoc ct2)
765
766 reportGroup :: (ReportErrCtxt -> [Ct] -> TcM ErrMsg) -> ReportErrCtxt
767 -> [Ct] -> TcM ()
768 reportGroup mk_err ctxt cts =
769 case partition isMonadFailInstanceMissing cts of
770 -- Only warn about missing MonadFail constraint when
771 -- there are no other missing constraints!
772 (monadFailCts, []) ->
773 do { err <- mk_err ctxt monadFailCts
774 ; reportWarning (Reason Opt_WarnMissingMonadFailInstances) err }
775
776 (_, cts') -> do { err <- mk_err ctxt cts'
777 ; maybeReportError ctxt err
778 -- But see Note [Always warn with -fdefer-type-errors]
779 ; traceTc "reportGroup" (ppr cts')
780 ; mapM_ (addDeferredBinding ctxt err) cts' }
781 -- Add deferred bindings for all
782 -- Redundant if we are going to abort compilation,
783 -- but that's hard to know for sure, and if we don't
784 -- abort, we need bindings for all (e.g. Trac #12156)
785 where
786 isMonadFailInstanceMissing ct =
787 case ctLocOrigin (ctLoc ct) of
788 FailablePattern _pat -> True
789 _otherwise -> False
790
791 maybeReportHoleError :: ReportErrCtxt -> Ct -> ErrMsg -> TcM ()
792 maybeReportHoleError ctxt ct err
793 -- When -XPartialTypeSignatures is on, warnings (instead of errors) are
794 -- generated for holes in partial type signatures.
795 -- Unless -fwarn_partial_type_signatures is not on,
796 -- in which case the messages are discarded.
797 | isTypeHoleCt ct
798 = -- For partial type signatures, generate warnings only, and do that
799 -- only if -fwarn_partial_type_signatures is on
800 case cec_type_holes ctxt of
801 HoleError -> reportError err
802 HoleWarn -> reportWarning (Reason Opt_WarnPartialTypeSignatures) err
803 HoleDefer -> return ()
804
805 -- Always report an error for out-of-scope variables
806 -- Unless -fdefer-out-of-scope-variables is on,
807 -- in which case the messages are discarded.
808 -- See Trac #12170, #12406
809 | isOutOfScopeCt ct
810 = -- If deferring, report a warning only if -Wout-of-scope-variables is on
811 case cec_out_of_scope_holes ctxt of
812 HoleError -> reportError err
813 HoleWarn ->
814 reportWarning (Reason Opt_WarnDeferredOutOfScopeVariables) err
815 HoleDefer -> return ()
816
817 -- Otherwise this is a typed hole in an expression,
818 -- but not for an out-of-scope variable
819 | otherwise
820 = -- If deferring, report a warning only if -Wtyped-holes is on
821 case cec_expr_holes ctxt of
822 HoleError -> reportError err
823 HoleWarn -> reportWarning (Reason Opt_WarnTypedHoles) err
824 HoleDefer -> return ()
825
826 maybeReportError :: ReportErrCtxt -> ErrMsg -> TcM ()
827 -- Report the error and/or make a deferred binding for it
828 maybeReportError ctxt err
829 | cec_suppress ctxt -- Some worse error has occurred;
830 = return () -- so suppress this error/warning
831
832 | otherwise
833 = case cec_defer_type_errors ctxt of
834 TypeDefer -> return ()
835 TypeWarn reason -> reportWarning reason err
836 TypeError -> reportError err
837
838 addDeferredBinding :: ReportErrCtxt -> ErrMsg -> Ct -> TcM ()
839 -- See Note [Deferring coercion errors to runtime]
840 addDeferredBinding ctxt err ct
841 | deferringAnyBindings ctxt
842 , CtWanted { ctev_pred = pred, ctev_dest = dest } <- ctEvidence ct
843 -- Only add deferred bindings for Wanted constraints
844 = do { dflags <- getDynFlags
845 ; let err_msg = pprLocErrMsg err
846 err_fs = mkFastString $ showSDoc dflags $
847 err_msg $$ text "(deferred type error)"
848 err_tm = evDelayedError pred err_fs
849 ev_binds_var = cec_binds ctxt
850
851 ; case dest of
852 EvVarDest evar
853 -> addTcEvBind ev_binds_var $ mkWantedEvBind evar (EvExpr err_tm)
854 HoleDest hole
855 -> do { -- See Note [Deferred errors for coercion holes]
856 let co_var = coHoleCoVar hole
857 ; addTcEvBind ev_binds_var $ mkWantedEvBind co_var (EvExpr err_tm)
858 ; fillCoercionHole hole (mkTcCoVarCo co_var) }}
859
860 | otherwise -- Do not set any evidence for Given/Derived
861 = return ()
862
863 maybeAddDeferredHoleBinding :: ReportErrCtxt -> ErrMsg -> Ct -> TcM ()
864 maybeAddDeferredHoleBinding ctxt err ct
865 | isExprHoleCt ct
866 = addDeferredBinding ctxt err ct -- Only add bindings for holes in expressions
867 | otherwise -- not for holes in partial type signatures
868 = return ()
869
870 tryReporters :: ReportErrCtxt -> [ReporterSpec] -> [Ct] -> TcM (ReportErrCtxt, [Ct])
871 -- Use the first reporter in the list whose predicate says True
872 tryReporters ctxt reporters cts
873 = do { let (vis_cts, invis_cts) = partition (isVisibleOrigin . ctOrigin) cts
874 ; traceTc "tryReporters {" (ppr vis_cts $$ ppr invis_cts)
875 ; (ctxt', cts') <- go ctxt reporters vis_cts invis_cts
876 ; traceTc "tryReporters }" (ppr cts')
877 ; return (ctxt', cts') }
878 where
879 go ctxt [] vis_cts invis_cts
880 = return (ctxt, vis_cts ++ invis_cts)
881
882 go ctxt (r : rs) vis_cts invis_cts
883 -- always look at *visible* Origins before invisible ones
884 -- this is the whole point of isVisibleOrigin
885 = do { (ctxt', vis_cts') <- tryReporter ctxt r vis_cts
886 ; (ctxt'', invis_cts') <- tryReporter ctxt' r invis_cts
887 ; go ctxt'' rs vis_cts' invis_cts' }
888 -- Carry on with the rest, because we must make
889 -- deferred bindings for them if we have -fdefer-type-errors
890 -- But suppress their error messages
891
892 tryReporter :: ReportErrCtxt -> ReporterSpec -> [Ct] -> TcM (ReportErrCtxt, [Ct])
893 tryReporter ctxt (str, keep_me, suppress_after, reporter) cts
894 | null yeses = return (ctxt, cts)
895 | otherwise = do { traceTc "tryReporter{ " (text str <+> ppr yeses)
896 ; reporter ctxt yeses
897 ; let ctxt' = ctxt { cec_suppress = suppress_after || cec_suppress ctxt }
898 ; traceTc "tryReporter end }" (text str <+> ppr (cec_suppress ctxt) <+> ppr suppress_after)
899 ; return (ctxt', nos) }
900 where
901 (yeses, nos) = partition (\ct -> keep_me ct (classifyPredType (ctPred ct))) cts
902
903
904 pprArising :: CtOrigin -> SDoc
905 -- Used for the main, top-level error message
906 -- We've done special processing for TypeEq, KindEq, Given
907 pprArising (TypeEqOrigin {}) = empty
908 pprArising (KindEqOrigin {}) = empty
909 pprArising (GivenOrigin {}) = empty
910 pprArising orig = pprCtOrigin orig
911
912 -- Add the "arising from..." part to a message about bunch of dicts
913 addArising :: CtOrigin -> SDoc -> SDoc
914 addArising orig msg = hang msg 2 (pprArising orig)
915
916 pprWithArising :: [Ct] -> (CtLoc, SDoc)
917 -- Print something like
918 -- (Eq a) arising from a use of x at y
919 -- (Show a) arising from a use of p at q
920 -- Also return a location for the error message
921 -- Works for Wanted/Derived only
922 pprWithArising []
923 = panic "pprWithArising"
924 pprWithArising (ct:cts)
925 | null cts
926 = (loc, addArising (ctLocOrigin loc)
927 (pprTheta [ctPred ct]))
928 | otherwise
929 = (loc, vcat (map ppr_one (ct:cts)))
930 where
931 loc = ctLoc ct
932 ppr_one ct' = hang (parens (pprType (ctPred ct')))
933 2 (pprCtLoc (ctLoc ct'))
934
935 mkErrorMsgFromCt :: ReportErrCtxt -> Ct -> Report -> TcM ErrMsg
936 mkErrorMsgFromCt ctxt ct report
937 = mkErrorReport ctxt (ctLocEnv (ctLoc ct)) report
938
939 mkErrorReport :: ReportErrCtxt -> TcLclEnv -> Report -> TcM ErrMsg
940 mkErrorReport ctxt tcl_env (Report important relevant_bindings valid_subs)
941 = do { context <- mkErrInfo (cec_tidy ctxt) (tcl_ctxt tcl_env)
942 ; mkErrDocAt (RealSrcSpan (tcl_loc tcl_env))
943 (errDoc important [context] (relevant_bindings ++ valid_subs))
944 }
945
946 type UserGiven = Implication
947
948 getUserGivens :: ReportErrCtxt -> [UserGiven]
949 -- One item for each enclosing implication
950 getUserGivens (CEC {cec_encl = implics}) = getUserGivensFromImplics implics
951
952 getUserGivensFromImplics :: [Implication] -> [UserGiven]
953 getUserGivensFromImplics implics
954 = reverse (filterOut (null . ic_given) implics)
955
956 {-
957 Note [Always warn with -fdefer-type-errors]
958 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
959 When -fdefer-type-errors is on we warn about *all* type errors, even
960 if cec_suppress is on. This can lead to a lot more warnings than you
961 would get errors without -fdefer-type-errors, but if we suppress any of
962 them you might get a runtime error that wasn't warned about at compile
963 time.
964
965 This is an easy design choice to change; just flip the order of the
966 first two equations for maybeReportError
967
968 To be consistent, we should also report multiple warnings from a single
969 location in mkGroupReporter, when -fdefer-type-errors is on. But that
970 is perhaps a bit *over*-consistent! Again, an easy choice to change.
971
972 With #10283, you can now opt out of deferred type error warnings.
973
974 Note [Deferred errors for coercion holes]
975 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
976 Suppose we need to defer a type error where the destination for the evidence
977 is a coercion hole. We can't just put the error in the hole, because we can't
978 make an erroneous coercion. (Remember that coercions are erased for runtime.)
979 Instead, we invent a new EvVar, bind it to an error and then make a coercion
980 from that EvVar, filling the hole with that coercion. Because coercions'
981 types are unlifted, the error is guaranteed to be hit before we get to the
982 coercion.
983
984 Note [Do not report derived but soluble errors]
985 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
986 The wc_simples include Derived constraints that have not been solved,
987 but are not insoluble (in that case they'd be reported by 'report1').
988 We do not want to report these as errors:
989
990 * Superclass constraints. If we have an unsolved [W] Ord a, we'll also have
991 an unsolved [D] Eq a, and we do not want to report that; it's just noise.
992
993 * Functional dependencies. For givens, consider
994 class C a b | a -> b
995 data T a where
996 MkT :: C a d => [d] -> T a
997 f :: C a b => T a -> F Int
998 f (MkT xs) = length xs
999 Then we get a [D] b~d. But there *is* a legitimate call to
1000 f, namely f (MkT [True]) :: T Bool, in which b=d. So we should
1001 not reject the program.
1002
1003 For wanteds, something similar
1004 data T a where
1005 MkT :: C Int b => a -> b -> T a
1006 g :: C Int c => c -> ()
1007 f :: T a -> ()
1008 f (MkT x y) = g x
1009 Here we get [G] C Int b, [W] C Int a, hence [D] a~b.
1010 But again f (MkT True True) is a legitimate call.
1011
1012 (We leave the Deriveds in wc_simple until reportErrors, so that we don't lose
1013 derived superclasses between iterations of the solver.)
1014
1015 For functional dependencies, here is a real example,
1016 stripped off from libraries/utf8-string/Codec/Binary/UTF8/Generic.hs
1017
1018 class C a b | a -> b
1019 g :: C a b => a -> b -> ()
1020 f :: C a b => a -> b -> ()
1021 f xa xb =
1022 let loop = g xa
1023 in loop xb
1024
1025 We will first try to infer a type for loop, and we will succeed:
1026 C a b' => b' -> ()
1027 Subsequently, we will type check (loop xb) and all is good. But,
1028 recall that we have to solve a final implication constraint:
1029 C a b => (C a b' => .... cts from body of loop .... ))
1030 And now we have a problem as we will generate an equality b ~ b' and fail to
1031 solve it.
1032
1033
1034 ************************************************************************
1035 * *
1036 Irreducible predicate errors
1037 * *
1038 ************************************************************************
1039 -}
1040
1041 mkIrredErr :: ReportErrCtxt -> [Ct] -> TcM ErrMsg
1042 mkIrredErr ctxt cts
1043 = do { (ctxt, binds_msg, ct1) <- relevantBindings True ctxt ct1
1044 ; let orig = ctOrigin ct1
1045 msg = couldNotDeduce (getUserGivens ctxt) (map ctPred cts, orig)
1046 ; mkErrorMsgFromCt ctxt ct1 $
1047 important msg `mappend` relevant_bindings binds_msg }
1048 where
1049 (ct1:_) = cts
1050
1051 ----------------
1052 mkHoleError :: [Ct] -> ReportErrCtxt -> Ct -> TcM ErrMsg
1053 mkHoleError _ _ ct@(CHoleCan { cc_hole = ExprHole (OutOfScope occ rdr_env0) })
1054 -- Out-of-scope variables, like 'a', where 'a' isn't bound; suggest possible
1055 -- in-scope variables in the message, and note inaccessible exact matches
1056 = do { dflags <- getDynFlags
1057 ; imp_info <- getImports
1058 ; let suggs_msg = unknownNameSuggestions dflags rdr_env0
1059 (tcl_rdr lcl_env) imp_info rdr
1060 ; rdr_env <- getGlobalRdrEnv
1061 ; splice_locs <- getTopLevelSpliceLocs
1062 ; let match_msgs = mk_match_msgs rdr_env splice_locs
1063 ; mkErrDocAt (RealSrcSpan err_loc) $
1064 errDoc [out_of_scope_msg] [] (match_msgs ++ [suggs_msg]) }
1065
1066 where
1067 rdr = mkRdrUnqual occ
1068 ct_loc = ctLoc ct
1069 lcl_env = ctLocEnv ct_loc
1070 err_loc = tcl_loc lcl_env
1071 hole_ty = ctEvPred (ctEvidence ct)
1072 boring_type = isTyVarTy hole_ty
1073
1074 out_of_scope_msg -- Print v :: ty only if the type has structure
1075 | boring_type = hang herald 2 (ppr occ)
1076 | otherwise = hang herald 2 (pp_with_type occ hole_ty)
1077
1078 herald | isDataOcc occ = text "Data constructor not in scope:"
1079 | otherwise = text "Variable not in scope:"
1080
1081 -- Indicate if the out-of-scope variable exactly (and unambiguously) matches
1082 -- a top-level binding in a later inter-splice group; see Note [OutOfScope
1083 -- exact matches]
1084 mk_match_msgs rdr_env splice_locs
1085 = let gres = filter isLocalGRE (lookupGlobalRdrEnv rdr_env occ)
1086 in case gres of
1087 [gre]
1088 | RealSrcSpan bind_loc <- greSrcSpan gre
1089 -- Find splice between the unbound variable and the match; use
1090 -- lookupLE, not lookupLT, since match could be in the splice
1091 , Just th_loc <- Set.lookupLE bind_loc splice_locs
1092 , err_loc < th_loc
1093 -> [mk_bind_scope_msg bind_loc th_loc]
1094 _ -> []
1095
1096 mk_bind_scope_msg bind_loc th_loc
1097 | is_th_bind
1098 = hang (quotes (ppr occ) <+> parens (text "splice on" <+> th_rng))
1099 2 (text "is not in scope before line" <+> int th_start_ln)
1100 | otherwise
1101 = hang (quotes (ppr occ) <+> bind_rng <+> text "is not in scope")
1102 2 (text "before the splice on" <+> th_rng)
1103 where
1104 bind_rng = parens (text "line" <+> int bind_ln)
1105 th_rng
1106 | th_start_ln == th_end_ln = single
1107 | otherwise = multi
1108 single = text "line" <+> int th_start_ln
1109 multi = text "lines" <+> int th_start_ln <> text "-" <> int th_end_ln
1110 bind_ln = srcSpanStartLine bind_loc
1111 th_start_ln = srcSpanStartLine th_loc
1112 th_end_ln = srcSpanEndLine th_loc
1113 is_th_bind = th_loc `containsSpan` bind_loc
1114
1115 mkHoleError tidy_simples ctxt ct@(CHoleCan { cc_hole = hole })
1116 -- Explicit holes, like "_" or "_f"
1117 = do { (ctxt, binds_msg, ct) <- relevantBindings False ctxt ct
1118 -- The 'False' means "don't filter the bindings"; see Trac #8191
1119
1120 ; show_hole_constraints <- goptM Opt_ShowHoleConstraints
1121 ; let constraints_msg
1122 | isExprHoleCt ct, show_hole_constraints
1123 = givenConstraintsMsg ctxt
1124 | otherwise = empty
1125
1126 ; no_show_valid_substitutions <- goptM Opt_NoShowValidSubstitutions
1127 ; sub_msg <- if no_show_valid_substitutions then return empty
1128 else validSubstitutions tidy_simples ctxt ct
1129 ; mkErrorMsgFromCt ctxt ct $
1130 important hole_msg `mappend`
1131 relevant_bindings (binds_msg $$ constraints_msg) `mappend`
1132 valid_substitutions sub_msg}
1133
1134 where
1135 occ = holeOcc hole
1136 hole_ty = ctEvPred (ctEvidence ct)
1137 hole_kind = typeKind hole_ty
1138 tyvars = tyCoVarsOfTypeList hole_ty
1139
1140 hole_msg = case hole of
1141 ExprHole {} -> vcat [ hang (text "Found hole:")
1142 2 (pp_with_type occ hole_ty)
1143 , tyvars_msg, expr_hole_hint ]
1144 TypeHole {} -> vcat [ hang (text "Found type wildcard" <+>
1145 quotes (ppr occ))
1146 2 (text "standing for" <+>
1147 quotes pp_hole_type_with_kind)
1148 , tyvars_msg, type_hole_hint ]
1149
1150 pp_hole_type_with_kind
1151 | isLiftedTypeKind hole_kind = pprType hole_ty
1152 | otherwise = pprType hole_ty <+> dcolon <+> pprKind hole_kind
1153
1154 tyvars_msg = ppUnless (null tyvars) $
1155 text "Where:" <+> (vcat (map loc_msg other_tvs)
1156 $$ pprSkols ctxt skol_tvs)
1157 where
1158 (skol_tvs, other_tvs) = partition is_skol tyvars
1159 is_skol tv = isTcTyVar tv && isSkolemTyVar tv
1160 -- Coercion variables can be free in the
1161 -- hole, via kind casts
1162
1163 type_hole_hint
1164 | HoleError <- cec_type_holes ctxt
1165 = text "To use the inferred type, enable PartialTypeSignatures"
1166 | otherwise
1167 = empty
1168
1169 expr_hole_hint -- Give hint for, say, f x = _x
1170 | lengthFS (occNameFS occ) > 1 -- Don't give this hint for plain "_"
1171 = text "Or perhaps" <+> quotes (ppr occ)
1172 <+> text "is mis-spelled, or not in scope"
1173 | otherwise
1174 = empty
1175
1176 loc_msg tv
1177 | isTyVar tv
1178 = case tcTyVarDetails tv of
1179 MetaTv {} -> quotes (ppr tv) <+> text "is an ambiguous type variable"
1180 _ -> empty -- Skolems dealt with already
1181 | otherwise -- A coercion variable can be free in the hole type
1182 = sdocWithDynFlags $ \dflags ->
1183 if gopt Opt_PrintExplicitCoercions dflags
1184 then quotes (ppr tv) <+> text "is a coercion variable"
1185 else empty
1186
1187 mkHoleError _ _ ct = pprPanic "mkHoleError" (ppr ct)
1188
1189 -- HoleFit is the type we use for a fit in valid substitutions. It contains the
1190 -- element that was checked, the Id of that element as found by `tcLookup`,
1191 -- and the refinement level of the fit, which is the number of extra argument
1192 -- holes that this fit uses (e.g. if hfRefLvl is 2, the fit is for `Id _ _`).
1193 data HoleFit = HoleFit { hfEl :: GlobalRdrElt -- The element that was checked.
1194 , hfId :: Id -- the elements id in the TcM.
1195 , hfRefLvl :: Int } -- The number of holes in this fit
1196
1197 -- We define an Eq and Ord instance to be able to build a graph.
1198 instance Eq HoleFit where
1199 (==) = (==) `on` hfId
1200
1201 -- We compare HoleFits by their gre_name instead of their Id, since we don't
1202 -- want our tests to be affected by the non-determinism of `nonDetCmpVar`,
1203 -- which is used to compare Ids. When comparing, we want HoleFits with a lower
1204 -- refinement level to come first.
1205 instance Ord HoleFit where
1206 compare a b = cmp a b
1207 where cmp = if (hfRefLvl a) == (hfRefLvl b)
1208 then compare `on` (gre_name . hfEl)
1209 else compare `on` hfRefLvl
1210
1211 instance Outputable HoleFit where
1212 ppr = pprHoleFit False
1213
1214 -- For pretty printing hole fits, we display the name and type of the fit,
1215 -- with added '_' to represent any extra arguments in case of a non-zero
1216 -- refinement level.
1217 pprHoleFit :: Bool -> HoleFit -> SDoc
1218 pprHoleFit showProv hf =
1219 if showProv then sep [idAndTy, nest 2 provenance] else idAndTy
1220 where name = gre_name (hfEl hf)
1221 ty = varType (hfId hf)
1222 holeVs = hsep $ replicate (hfRefLvl hf) $ text "_"
1223 idAndTy = (pprPrefixOcc name <+> holeVs <+> dcolon <+> pprType ty)
1224 provenance = parens $ pprNameProvenance (hfEl hf)
1225
1226
1227 -- See Note [Valid substitutions include ...]
1228 validSubstitutions :: [Ct] -> ReportErrCtxt -> Ct -> TcM SDoc
1229 validSubstitutions simples (CEC {cec_encl = implics}) ct | isExprHoleCt ct =
1230 do { rdr_env <- getGlobalRdrEnv
1231 ; maxVSubs <- maxValidSubstitutions <$> getDynFlags
1232 ; showProvenance <- not <$> goptM Opt_UnclutterValidSubstitutions
1233 ; graphSortSubs <- not <$> goptM Opt_NoSortValidSubstitutions
1234 ; refLevel <- refLevelSubstitutions <$> getDynFlags
1235 ; traceTc "findingValidSubstitutionsFor { " $ ppr ct
1236 ; traceTc "hole_lvl is:" $ ppr hole_lvl
1237 ; traceTc "implics are: " $ ppr implics
1238 ; traceTc "simples are: " $ ppr simples
1239 ; (searchDiscards, subs) <-
1240 findSubs graphSortSubs maxVSubs rdr_env 0 (wrapped_hole_ty, [])
1241 ; (vDiscards, sortedSubs) <-
1242 sortSubs graphSortSubs maxVSubs searchDiscards subs
1243 ; let vMsg = ppUnless (null subs) $
1244 hang (text "Valid substitutions include") 2 $
1245 (vcat (map (pprHoleFit showProvenance) sortedSubs)
1246 $$ ppWhen vDiscards subsDiscardMsg)
1247 ; refMsg <- if refLevel >= (Just 0) then
1248 do { maxRSubs <- maxRefSubstitutions <$> getDynFlags
1249 -- We can use from just, since we know that Nothing >= _ is False.
1250 ; let refLvls = [1..(fromJust refLevel)]
1251 -- We make a new refinement type for each level of refinement, where
1252 -- the level of refinement indicates number of additional arguments
1253 -- to allow.
1254 ; ref_tys <- mapM (\l -> mkRefTy l >>= return . (,) l) refLvls
1255 ; traceTc "ref_tys are" $ ppr ref_tys
1256 ; refDs <-
1257 mapM (uncurry $ findSubs graphSortSubs maxRSubs rdr_env) ref_tys
1258 ; (rDiscards, sortedRSubs) <-
1259 sortSubs graphSortSubs maxRSubs (any fst refDs) $
1260 concatMap snd refDs
1261 ; return $
1262 ppUnless (null sortedRSubs) $
1263 hang (text "Valid refinement substitutions include") 2 $
1264 (vcat (map (pprHoleFit showProvenance) sortedRSubs)
1265 $$ ppWhen rDiscards refSubsDiscardMsg) }
1266 else return empty
1267 ; traceTc "findingValidSubstitutionsFor }" empty
1268 ; return (vMsg $$ refMsg)}
1269 where
1270 hole_loc = ctEvLoc $ ctEvidence ct
1271 hole_lvl = ctLocLevel $ hole_loc
1272
1273 -- We make a refinement type by adding a new type variable in front
1274 -- of the type of t h hole, going from e.g. [Integer] -> Integer
1275 -- to t_a1/m[tau:1] -> [Integer] -> Integer. This allows the simplifier
1276 -- to unify the new type variable with any type, allowing us
1277 -- to suggest a "refinement substitution", like `(foldl1 _)` instead
1278 -- of only concrete substitutions like `sum`.
1279 mkRefTy :: Int -> TcM (TcType, [TcType])
1280 mkRefTy refLvl = (\v -> (wrapHoleWithArgs v, v)) <$> newTyVarTys
1281 where newTyVarTys = replicateM refLvl newOpenFlexiTyVarTy
1282 wrapHoleWithArgs args = (wrap_ty . mkFunTys args) hole_ty
1283
1284
1285 sortSubs :: Bool -- Whether we should sort the subs or not
1286 -- by subsumption or not
1287 -> Maybe Int -- How many we should output, if limited.
1288 -> Bool -- Whether there were any discards in the
1289 -- initial search
1290 -> [HoleFit] -- The subs to sort
1291 -> TcM (Bool, [HoleFit])
1292 -- If we don't want to sort by the subsumption graph, we just sort it
1293 -- such that local fits come before global fits, since local fits are
1294 -- probably more relevant to the user.
1295 sortSubs False _ discards subs = return (discards, sortedFits)
1296 where (lclFits, gblFits) = partition (gre_lcl . hfEl) subs
1297 sortedFits = lclFits ++ gblFits
1298 -- We sort the fits first, to prevent the order of
1299 -- suggestions being effected when identifiers are moved
1300 -- around in modules. We use (<*>) to expose the
1301 -- parallelism, in case it becomes useful later.
1302 sortSubs _ limit _ subs = possiblyDiscard limit <$>
1303 ((++) <$> sortByGraph (sort lclFits)
1304 <*> sortByGraph (sort gblFits))
1305 where (lclFits, gblFits) = partition (gre_lcl . hfEl) subs
1306
1307
1308 findSubs :: Bool -- Whether we should sort the subs or not
1309 -> Maybe Int -- How many we should output, if limited
1310 -> GlobalRdrEnv -- The elements to check whether fit
1311 -> Int -- The refinement level of the hole
1312 -> (TcType, [TcType]) -- The type to check for fits and ref vars
1313 -> TcM (Bool, [HoleFit])
1314 -- We don't check if no output is desired.
1315 findSubs _ (Just 0) _ _ _ = return (False, [])
1316 findSubs sortSubs maxSubs rdr_env refLvl ht@(hole_ty, _) =
1317 do { traceTc "checkingSubstitutionsFor {" $ ppr $ hole_ty
1318 ; let limit = if sortSubs then Nothing else maxSubs
1319 ; (discards, subs) <- setTcLevel hole_lvl $
1320 go limit ht refLvl $
1321 globalRdrEnvElts rdr_env
1322 ; traceTc "}" empty
1323 ; return (discards, subs) }
1324 -- We extract the type of the hole from the constraint.
1325 hole_ty :: TcPredType
1326 hole_ty = ctPred ct
1327 hole_fvs = tyCoFVsOfType hole_ty
1328
1329 -- For checking, we wrap the type of the hole with all the givens
1330 -- from all the implications in the context.
1331 wrap_ty :: TcType -> TcSigmaType
1332 wrap_ty ty = foldl' wrapTypeWithImplication ty implics
1333
1334 wrapped_hole_ty :: TcSigmaType
1335 wrapped_hole_ty = wrap_ty hole_ty
1336
1337 -- We rearrange the elements to make locals appear at the top of the list
1338 -- since they're most likely to be relevant to the user.
1339 localsFirst :: [HoleFit] -> [HoleFit]
1340 localsFirst elts = lcl ++ gbl
1341 where (lcl, gbl) = partition (gre_lcl . hfEl) elts
1342
1343
1344 -- These are the constraints whose every free unification variable is
1345 -- mentioned in the type of the hole.
1346 relevantCts :: [Ct]
1347 relevantCts = if isEmptyVarSet hole_fv then []
1348 else filter isRelevant simples
1349 where hole_fv :: VarSet
1350 hole_fv = fvVarSet hole_fvs
1351 ctFreeVarSet :: Ct -> VarSet
1352 ctFreeVarSet = fvVarSet . tyCoFVsOfType . ctPred
1353 allFVMentioned :: Ct -> Bool
1354 allFVMentioned ct = ctFreeVarSet ct `subVarSet` hole_fv
1355 -- We filter out those constraints that have no variables (since
1356 -- they won't be solved by finding a type for the type variable
1357 -- representing the hole) and also other holes, since we're not
1358 -- trying to find substitutions for many holes at once.
1359 isRelevant ct = not (isEmptyVarSet (ctFreeVarSet ct))
1360 && allFVMentioned ct
1361 && not (isHoleCt ct)
1362
1363
1364 -- This creates a substitution with new fresh type variables for all the
1365 -- free variables mentioned in the type of hole and in the relevant
1366 -- constraints. Note that since we only pick constraints such that all their
1367 -- free variables are mentioned by the hole, the free variables of the hole
1368 -- are all the free variables of the constraints as well.
1369 getHoleCloningSubst :: TcType -> TcM TCvSubst
1370 getHoleCloningSubst hole_ty = mkTvSubstPrs <$> getClonedVars
1371 where cloneFV :: TyVar -> TcM (TyVar, Type)
1372 cloneFV fv = ((,) fv) <$> pushTcLevelM_ (newFlexiTyVarTy (varType fv))
1373 -- The subsumption check pushes the level, so as to be sure that
1374 -- its invocation of the solver doesn't unify type variables floating
1375 -- about that are unrelated to the subsumption check. However, these
1376 -- cloned variables in the hole type *should* be unified, so we make
1377 -- sure to bump the level before creating them
1378
1379 getClonedVars :: TcM [(TyVar, Type)]
1380 getClonedVars = mapM cloneFV (fvVarList $ tyCoFVsOfType hole_ty)
1381
1382 -- This applies the given substitution to the given constraint.
1383 applySubToCt :: TCvSubst -> Ct -> Ct
1384 applySubToCt sub ct = ct {cc_ev = ev {ctev_pred = subbedPredType} }
1385 where subbedPredType = substTy sub $ ctPred ct
1386 ev = ctEvidence ct
1387
1388 -- The real work happens here, where we invoke the type checker
1389 -- to check whether we the given type fits into the hole!
1390 -- To check: Clone all relevant cts and the hole
1391 -- then solve the subsumption check AND check that all other
1392 -- the other constraints were solved.
1393 fitsHole :: (TcType, [TcType]) -> Type -> TcM Bool
1394 fitsHole (hole_ty, vars) typ =
1395 do { traceTc "checkingFitOf {" $ ppr typ
1396 ; cloneSub <- getHoleCloningSubst hole_ty
1397 ; let cHoleTy = substTy cloneSub hole_ty
1398 cCts = map (applySubToCt cloneSub) relevantCts
1399 cVars = map (substTy cloneSub) vars
1400
1401 ; absFits <- tcCheckHoleFit (listToBag cCts) cHoleTy typ
1402 ; traceTc "}" empty
1403 -- We'd like to avoid refinement suggestions like `id _ _` or
1404 -- `head _ _`, and only suggest refinements where our all phantom
1405 -- variables got unified during the checking. This can be disabled
1406 -- with the `-fabstract-refinement-substitutions` flag.
1407 ; if absFits && (not . null) vars then
1408 goptM Opt_AbstractRefSubstitutions `orM`
1409 allM isFilledMetaTyVar (fvVarList $ tyCoFVsOfTypes cVars)
1410 else return absFits }
1411
1412 -- Based on the flags, we might possibly discard some or all the
1413 -- fits we've found.
1414 possiblyDiscard :: Maybe Int -> [HoleFit] -> (Bool, [HoleFit])
1415 possiblyDiscard (Just max) fits = (fits `lengthExceeds` max, take max fits)
1416 possiblyDiscard Nothing fits = (False, fits)
1417
1418 -- Based on a suggestion by phadej on #ghc, we can sort the found fits
1419 -- by constructing a subsumption graph, and then do a topological sort of
1420 -- the graph. This makes the most specific types appear first, which are
1421 -- probably those most relevant. This takes a lot of work (but results in
1422 -- much more useful output), and can be disabled by
1423 -- '-fno-sort-valid-substitutions'.
1424 sortByGraph :: [HoleFit] -> TcM [HoleFit]
1425 sortByGraph fits = go [] fits
1426 where hfType :: HoleFit -> TcSigmaType
1427 hfType = varType . hfId
1428
1429 go :: [(HoleFit, [HoleFit])] -> [HoleFit] -> TcM [HoleFit]
1430 go sofar [] = do { traceTc "subsumptionGraph was" $ ppr sofar
1431 ; return $ localsFirst topSorted }
1432 where toV (hf, adjs) = (hf, hfId hf, map hfId adjs)
1433 (graph, fromV, _) = graphFromEdges $ map toV sofar
1434 topSorted = map ((\(h,_,_) -> h) . fromV) $ topSort graph
1435 go sofar (id:ids) =
1436 do { adjs <- filterM (tcSubsumes (hfType id) . hfType) fits
1437 ; go ((id, adjs):sofar) ids }
1438
1439 -- Kickoff the checking of the elements.
1440 go :: Maybe Int -> (TcType, [TcType]) -> Int
1441 -> [GlobalRdrElt] -> TcM (Bool, [HoleFit])
1442 go = go_ []
1443
1444 -- We iterate over the elements, checking each one in turn for whether it
1445 -- fits, and adding it to the results if it does.
1446 go_ :: [HoleFit] -- What we've found so far.
1447 -> Maybe Int -- How many we're allowed to find, if limited
1448 -> (TcType, [TcType]) -- The type to check, and refinement variables.
1449 -> Int -- The refinement level of the hole we're checking
1450 -> [GlobalRdrElt] -- The elements we've yet to check.
1451 -> TcM (Bool, [HoleFit])
1452 go_ subs _ _ _ [] = return (False, reverse subs)
1453 go_ subs (Just 0) _ _ _ = return (True, reverse subs)
1454 go_ subs maxleft t r (el:elts) =
1455 do { traceTc "lookingUp" $ ppr el
1456 ; maybeThing <- lookup (gre_name el)
1457 ; case maybeThing of
1458 Just id -> do { fits <- fitsHole t (varType id)
1459 ; if fits then keep_it (HoleFit el id r)
1460 else discard_it }
1461 _ -> discard_it }
1462 where discard_it = go_ subs maxleft t r elts
1463 keep_it fit = go_ (fit:subs) ((\n -> n - 1) <$> maxleft) t r elts
1464 lookup name =
1465 do { thing <- tcLookup name
1466 ; case thing of
1467 ATcId {tct_id = id} -> return $ Just id
1468 AGlobal (AnId id) -> return $ Just id
1469 AGlobal (AConLike (RealDataCon con)) ->
1470 return $ Just (dataConWrapId con)
1471 _ -> return Nothing }
1472
1473
1474 -- We don't (as of yet) handle holes in types, only in expressions.
1475 validSubstitutions _ _ _ = return empty
1476
1477
1478 -- See Note [Constraints include ...]
1479 givenConstraintsMsg :: ReportErrCtxt -> SDoc
1480 givenConstraintsMsg ctxt =
1481 let constraints :: [(Type, RealSrcSpan)]
1482 constraints =
1483 do { Implic{ ic_given = given, ic_env = env } <- cec_encl ctxt
1484 ; constraint <- given
1485 ; return (varType constraint, tcl_loc env) }
1486
1487 pprConstraint (constraint, loc) =
1488 ppr constraint <+> nest 2 (parens (text "from" <+> ppr loc))
1489
1490 in ppUnless (null constraints) $
1491 hang (text "Constraints include")
1492 2 (vcat $ map pprConstraint constraints)
1493
1494 pp_with_type :: OccName -> Type -> SDoc
1495 pp_with_type occ ty = hang (pprPrefixOcc occ) 2 (dcolon <+> pprType ty)
1496
1497 ----------------
1498 mkIPErr :: ReportErrCtxt -> [Ct] -> TcM ErrMsg
1499 mkIPErr ctxt cts
1500 = do { (ctxt, binds_msg, ct1) <- relevantBindings True ctxt ct1
1501 ; let orig = ctOrigin ct1
1502 preds = map ctPred cts
1503 givens = getUserGivens ctxt
1504 msg | null givens
1505 = addArising orig $
1506 sep [ text "Unbound implicit parameter" <> plural cts
1507 , nest 2 (pprParendTheta preds) ]
1508 | otherwise
1509 = couldNotDeduce givens (preds, orig)
1510
1511 ; mkErrorMsgFromCt ctxt ct1 $
1512 important msg `mappend` relevant_bindings binds_msg }
1513 where
1514 (ct1:_) = cts
1515
1516 {-
1517 Note [Valid substitutions include ...]
1518 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1519 `validSubstitutions` returns the "Valid substitutions include ..." message.
1520 For example, look at the following definitions in a file called test.hs:
1521
1522 import Data.List (inits)
1523
1524 f :: [String]
1525 f = _ "hello, world"
1526
1527 The hole in `f` would generate the message:
1528
1529 • Found hole: _ :: [Char] -> [String]
1530 • In the expression: _
1531 In the expression: _ "hello, world"
1532 In an equation for ‘f’: f = _ "hello, world"
1533 • Relevant bindings include f :: [String] (bound at test.hs:6:1)
1534 Valid substitutions include
1535 lines :: String -> [String]
1536 (imported from ‘Prelude’ at test.hs:1:8-11
1537 (and originally defined in ‘base-4.11.0.0:Data.OldList’))
1538 words :: String -> [String]
1539 (imported from ‘Prelude’ at test.hs:1:8-11
1540 (and originally defined in ‘base-4.11.0.0:Data.OldList’))
1541 read :: forall a. Read a => String -> a
1542 (imported from ‘Prelude’ at test.hs:1:8-11
1543 (and originally defined in ‘Text.Read’))
1544 inits :: forall a. [a] -> [[a]]
1545 (imported from ‘Data.List’ at test.hs:3:19-23
1546 (and originally defined in ‘base-4.11.0.0:Data.OldList’))
1547 repeat :: forall a. a -> [a]
1548 (imported from ‘Prelude’ at test.hs:1:8-11
1549 (and originally defined in ‘GHC.List’))
1550 mempty :: forall a. Monoid a => a
1551 (imported from ‘Prelude’ at test.hs:1:8-11
1552 (and originally defined in ‘GHC.Base’))
1553 return :: forall (m :: * -> *). Monad m => forall a. a -> m a
1554 (imported from ‘Prelude’ at test.hs:1:8-11
1555 (and originally defined in ‘GHC.Base’))
1556 pure :: forall (f :: * -> *). Applicative f => forall a. a -> f a
1557 (imported from ‘Prelude’ at test.hs:1:8-11
1558 (and originally defined in ‘GHC.Base’))
1559 fail :: forall (m :: * -> *). Monad m => forall a. String -> m a
1560 (imported from ‘Prelude’ at test.hs:1:8-11
1561 (and originally defined in ‘GHC.Base’))
1562 error :: forall (a :: TYPE r). GHC.Stack.Types.HasCallStack => [Char] -> a
1563 (imported from ‘Prelude’ at test.hs:1:8-11
1564 (and originally defined in ‘GHC.Err’))
1565 errorWithoutStackTrace :: forall (a :: TYPE r). [Char] -> a
1566 (imported from ‘Prelude’ at test.hs:1:8-11
1567 (and originally defined in ‘GHC.Err’))
1568 undefined :: forall (a :: TYPE r). GHC.Stack.Types.HasCallStack => a
1569 (imported from ‘Prelude’ at test.hs:1:8-11
1570 (and originally defined in ‘GHC.Err’))
1571
1572
1573 Valid substitutions are found by checking top level identifiers in scope for
1574 whether their type is subsumed by the type of the hole. Additionally, as
1575 highlighted by Trac #14273, we also need to check whether all relevant
1576 constraints are solved by choosing an identifier of that type as well. This is
1577 to make sure we don't suggest a substitution which does not fulfill the
1578 constraints imposed on the hole (even though it has a type that would otherwise
1579 fit the hole). The relevant constraints are those whose free unification
1580 variables are all mentioned by the type of the hole. Since checking for
1581 subsumption results in the side effect of type variables being unified by the
1582 simplifier, we need to take care to clone the variables in the hole and relevant
1583 constraints before checking whether an identifier fits into the hole, to avoid
1584 affecting the hole and later checks. When outputting, take the fits found for
1585 the hole and build a subsumption graph, where fit a and fit b are connected if
1586 a subsumes b. We then sort the graph topologically, and output the suggestions
1587 in that order. This is done in order to display "more relevant" suggestions
1588 first where the most specific suggestions (i.e. the ones that are subsumed by
1589 the other suggestions) appear first. This puts suggestions such as `error` and
1590 `undefined` last, as seen in the example above.
1591
1592 When the flag `-frefinement-level-substitutions=n` where `n > 0` is passed, we
1593 also look for valid refinement substitutions, i.e. substitutions that are valid,
1594 but adds more holes. Consider the following:
1595
1596 f :: [Integer] -> Integer
1597 f = _
1598
1599 Here the valid substitutions suggested will be (with the
1600 `-funclutter-valid-substitutions` flag set):
1601
1602 Valid substitutions include
1603 f :: [Integer] -> Integer
1604 product :: forall (t :: * -> *).
1605 Foldable t => forall a. Num a => t a -> a
1606 sum :: forall (t :: * -> *).
1607 Foldable t => forall a. Num a => t a -> a
1608 maximum :: forall (t :: * -> *).
1609 Foldable t => forall a. Ord a => t a -> a
1610 minimum :: forall (t :: * -> *).
1611 Foldable t => forall a. Ord a => t a -> a
1612 head :: forall a. [a] -> a
1613 (Some substitutions suppressed;
1614 use -fmax-valid-substitutions=N or -fno-max-valid-substitutions)
1615
1616 When the `-frefinement-level-substitutions=1` flag is given, we additionally
1617 compute and report valid refinement substitutions:
1618
1619 Valid refinement substitutions include
1620 foldl1 _ :: forall (t :: * -> *).
1621 Foldable t => forall a. (a -> a -> a) -> t a -> a
1622 foldr1 _ :: forall (t :: * -> *).
1623 Foldable t => forall a. (a -> a -> a) -> t a -> a
1624 head _ :: forall a. [a] -> a
1625 last _ :: forall a. [a] -> a
1626 error _ :: forall (a :: TYPE r).
1627 GHC.Stack.Types.HasCallStack => [Char] -> a
1628 errorWithoutStackTrace _ :: forall (a :: TYPE r). [Char] -> a
1629 (Some refinement substitutions suppressed;
1630 use -fmax-refinement-substitutions=N or -fno-max-refinement-substitutions)
1631
1632 Which are substitutions with holes in them. This allows e.g. beginners to
1633 discover the fold functions and similar.
1634
1635 We find these refinement suggestions by considering substitutions that don't
1636 fit the type of the hole, but ones that would fit if given an additional
1637 argument. We do this by creating a new type variable with `newOpenFlexiTyVarTy`
1638 (e.g. `t_a1/m[tau:1]`), and then considering substitutions of the type
1639 `t_a1/m[tau:1] -> v` where `v` is the type of the hole. Since the simplifier is
1640 free to unify this new type variable with any type (and it is cloned before each
1641 check to avoid side-effects), we can now discover any identifiers that would fit
1642 if given another identifier of a suitable type. This is then generalized so that
1643 we can consider any number of additional arguments by setting the
1644 `-frefinement-level-substitutions` flag to any number, and then considering
1645 substitutions like e.g. `foldl _ _` with two additional arguments.
1646
1647 Note [Constraints include ...]
1648 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1649 'givenConstraintsMsg' returns the "Constraints include ..." message enabled by
1650 -fshow-hole-constraints. For example, the following hole:
1651
1652 foo :: (Eq a, Show a) => a -> String
1653 foo x = _
1654
1655 would generate the message:
1656
1657 Constraints include
1658 Eq a (from foo.hs:1:1-36)
1659 Show a (from foo.hs:1:1-36)
1660
1661 Constraints are displayed in order from innermost (closest to the hole) to
1662 outermost. There's currently no filtering or elimination of duplicates.
1663
1664
1665 Note [OutOfScope exact matches]
1666 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1667 When constructing an out-of-scope error message, we not only generate a list of
1668 possible in-scope alternatives but also search for an exact, unambiguous match
1669 in a later inter-splice group. If we find such a match, we report its presence
1670 (and indirectly, its scope) in the message. For example, if a module A contains
1671 the following declarations,
1672
1673 foo :: Int
1674 foo = x
1675
1676 $(return []) -- Empty top-level splice
1677
1678 x :: Int
1679 x = 23
1680
1681 we will issue an error similar to
1682
1683 A.hs:6:7: error:
1684 • Variable not in scope: x :: Int
1685 • ‘x’ (line 11) is not in scope before the splice on line 8
1686
1687 By providing information about the match, we hope to clarify why declaring a
1688 variable after a top-level splice but using it before the splice generates an
1689 out-of-scope error (a situation which is often confusing to Haskell newcomers).
1690
1691 Note that if we find multiple exact matches to the out-of-scope variable
1692 (hereafter referred to as x), we report nothing. Such matches can only be
1693 duplicate record fields, as the presence of any other duplicate top-level
1694 declarations would have already halted compilation. But if these record fields
1695 are declared in a later inter-splice group, then so too are their corresponding
1696 types. Thus, these types must not occur in the inter-splice group containing x
1697 (any unknown types would have already been reported), and so the matches to the
1698 record fields are most likely coincidental.
1699
1700 One oddity of the exact match portion of the error message is that we specify
1701 where the match to x is NOT in scope. Why not simply state where the match IS
1702 in scope? It most cases, this would be just as easy and perhaps a little
1703 clearer for the user. But now consider the following example:
1704
1705 {-# LANGUAGE TemplateHaskell #-}
1706
1707 module A where
1708
1709 import Language.Haskell.TH
1710 import Language.Haskell.TH.Syntax
1711
1712 foo = x
1713
1714 $(do -------------------------------------------------
1715 ds <- [d| ok1 = x
1716 |]
1717 addTopDecls ds
1718 return [])
1719
1720 bar = $(do
1721 ds <- [d| x = 23
1722 ok2 = x
1723 |]
1724 addTopDecls ds
1725 litE $ stringL "hello")
1726
1727 $(return []) -----------------------------------------
1728
1729 ok3 = x
1730
1731 Here, x is out-of-scope in the declaration of foo, and so we report
1732
1733 A.hs:8:7: error:
1734 • Variable not in scope: x
1735 • ‘x’ (line 16) is not in scope before the splice on lines 10-14
1736
1737 If we instead reported where x IS in scope, we would have to state that it is in
1738 scope after the second top-level splice as well as among all the top-level
1739 declarations added by both calls to addTopDecls. But doing so would not only
1740 add complexity to the code but also overwhelm the user with unneeded
1741 information.
1742
1743 The logic which determines where x is not in scope is straightforward: it simply
1744 finds the last top-level splice which occurs after x but before (or at) the
1745 match to x (assuming such a splice exists). In most cases, the check that the
1746 splice occurs after x acts only as a sanity check. For example, when the match
1747 to x is a non-TH top-level declaration and a splice S occurs before the match,
1748 then x must precede S; otherwise, it would be in scope. But when dealing with
1749 addTopDecls, this check serves a practical purpose. Consider the following
1750 declarations:
1751
1752 $(do
1753 ds <- [d| ok = x
1754 x = 23
1755 |]
1756 addTopDecls ds
1757 return [])
1758
1759 foo = x
1760
1761 In this case, x is not in scope in the declaration for foo. Since x occurs
1762 AFTER the splice containing the match, the logic does not find any splices after
1763 x but before or at its match, and so we report nothing about x's scope. If we
1764 had not checked whether x occurs before the splice, we would have instead
1765 reported that x is not in scope before the splice. While correct, such an error
1766 message is more likely to confuse than to enlighten.
1767 -}
1768
1769 {-
1770 ************************************************************************
1771 * *
1772 Equality errors
1773 * *
1774 ************************************************************************
1775
1776 Note [Inaccessible code]
1777 ~~~~~~~~~~~~~~~~~~~~~~~~
1778 Consider
1779 data T a where
1780 T1 :: T a
1781 T2 :: T Bool
1782
1783 f :: (a ~ Int) => T a -> Int
1784 f T1 = 3
1785 f T2 = 4 -- Unreachable code
1786
1787 Here the second equation is unreachable. The original constraint
1788 (a~Int) from the signature gets rewritten by the pattern-match to
1789 (Bool~Int), so the danger is that we report the error as coming from
1790 the *signature* (Trac #7293). So, for Given errors we replace the
1791 env (and hence src-loc) on its CtLoc with that from the immediately
1792 enclosing implication.
1793
1794 Note [Error messages for untouchables]
1795 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1796 Consider (Trac #9109)
1797 data G a where { GBool :: G Bool }
1798 foo x = case x of GBool -> True
1799
1800 Here we can't solve (t ~ Bool), where t is the untouchable result
1801 meta-var 't', because of the (a ~ Bool) from the pattern match.
1802 So we infer the type
1803 f :: forall a t. G a -> t
1804 making the meta-var 't' into a skolem. So when we come to report
1805 the unsolved (t ~ Bool), t won't look like an untouchable meta-var
1806 any more. So we don't assert that it is.
1807 -}
1808
1809 -- Don't have multiple equality errors from the same location
1810 -- E.g. (Int,Bool) ~ (Bool,Int) one error will do!
1811 mkEqErr :: ReportErrCtxt -> [Ct] -> TcM ErrMsg
1812 mkEqErr ctxt (ct:_) = mkEqErr1 ctxt ct
1813 mkEqErr _ [] = panic "mkEqErr"
1814
1815 mkEqErr1 :: ReportErrCtxt -> Ct -> TcM ErrMsg
1816 mkEqErr1 ctxt ct -- Wanted or derived;
1817 -- givens handled in mkGivenErrorReporter
1818 = do { (ctxt, binds_msg, ct) <- relevantBindings True ctxt ct
1819 ; rdr_env <- getGlobalRdrEnv
1820 ; fam_envs <- tcGetFamInstEnvs
1821 ; exp_syns <- goptM Opt_PrintExpandedSynonyms
1822 ; let (keep_going, is_oriented, wanted_msg)
1823 = mk_wanted_extra (ctLoc ct) exp_syns
1824 coercible_msg = case ctEqRel ct of
1825 NomEq -> empty
1826 ReprEq -> mkCoercibleExplanation rdr_env fam_envs ty1 ty2
1827 ; dflags <- getDynFlags
1828 ; traceTc "mkEqErr1" (ppr ct $$ pprCtOrigin (ctOrigin ct) $$ ppr keep_going)
1829 ; let report = mconcat [important wanted_msg, important coercible_msg,
1830 relevant_bindings binds_msg]
1831 ; if keep_going
1832 then mkEqErr_help dflags ctxt report ct is_oriented ty1 ty2
1833 else mkErrorMsgFromCt ctxt ct report }
1834 where
1835 (ty1, ty2) = getEqPredTys (ctPred ct)
1836
1837 -- If the types in the error message are the same as the types
1838 -- we are unifying, don't add the extra expected/actual message
1839 mk_wanted_extra :: CtLoc -> Bool -> (Bool, Maybe SwapFlag, SDoc)
1840 mk_wanted_extra loc expandSyns
1841 = case ctLocOrigin loc of
1842 orig@TypeEqOrigin {} -> mkExpectedActualMsg ty1 ty2 orig
1843 t_or_k expandSyns
1844 where
1845 t_or_k = ctLocTypeOrKind_maybe loc
1846
1847 KindEqOrigin cty1 mb_cty2 sub_o sub_t_or_k
1848 -> (True, Nothing, msg1 $$ msg2)
1849 where
1850 sub_what = case sub_t_or_k of Just KindLevel -> text "kinds"
1851 _ -> text "types"
1852 msg1 = sdocWithDynFlags $ \dflags ->
1853 case mb_cty2 of
1854 Just cty2
1855 | gopt Opt_PrintExplicitCoercions dflags
1856 || not (cty1 `pickyEqType` cty2)
1857 -> hang (text "When matching" <+> sub_what)
1858 2 (vcat [ ppr cty1 <+> dcolon <+>
1859 ppr (typeKind cty1)
1860 , ppr cty2 <+> dcolon <+>
1861 ppr (typeKind cty2) ])
1862 _ -> text "When matching the kind of" <+> quotes (ppr cty1)
1863 msg2 = case sub_o of
1864 TypeEqOrigin {}
1865 | Just cty2 <- mb_cty2 ->
1866 thdOf3 (mkExpectedActualMsg cty1 cty2 sub_o sub_t_or_k
1867 expandSyns)
1868 _ -> empty
1869 _ -> (True, Nothing, empty)
1870
1871 -- | This function tries to reconstruct why a "Coercible ty1 ty2" constraint
1872 -- is left over.
1873 mkCoercibleExplanation :: GlobalRdrEnv -> FamInstEnvs
1874 -> TcType -> TcType -> SDoc
1875 mkCoercibleExplanation rdr_env fam_envs ty1 ty2
1876 | Just (tc, tys) <- tcSplitTyConApp_maybe ty1
1877 , (rep_tc, _, _) <- tcLookupDataFamInst fam_envs tc tys
1878 , Just msg <- coercible_msg_for_tycon rep_tc
1879 = msg
1880 | Just (tc, tys) <- splitTyConApp_maybe ty2
1881 , (rep_tc, _, _) <- tcLookupDataFamInst fam_envs tc tys
1882 , Just msg <- coercible_msg_for_tycon rep_tc
1883 = msg
1884 | Just (s1, _) <- tcSplitAppTy_maybe ty1
1885 , Just (s2, _) <- tcSplitAppTy_maybe ty2
1886 , s1 `eqType` s2
1887 , has_unknown_roles s1
1888 = hang (text "NB: We cannot know what roles the parameters to" <+>
1889 quotes (ppr s1) <+> text "have;")
1890 2 (text "we must assume that the role is nominal")
1891 | otherwise
1892 = empty
1893 where
1894 coercible_msg_for_tycon tc
1895 | isAbstractTyCon tc
1896 = Just $ hsep [ text "NB: The type constructor"
1897 , quotes (pprSourceTyCon tc)
1898 , text "is abstract" ]
1899 | isNewTyCon tc
1900 , [data_con] <- tyConDataCons tc
1901 , let dc_name = dataConName data_con
1902 , isNothing (lookupGRE_Name rdr_env dc_name)
1903 = Just $ hang (text "The data constructor" <+> quotes (ppr dc_name))
1904 2 (sep [ text "of newtype" <+> quotes (pprSourceTyCon tc)
1905 , text "is not in scope" ])
1906 | otherwise = Nothing
1907
1908 has_unknown_roles ty
1909 | Just (tc, tys) <- tcSplitTyConApp_maybe ty
1910 = tys `lengthAtLeast` tyConArity tc -- oversaturated tycon
1911 | Just (s, _) <- tcSplitAppTy_maybe ty
1912 = has_unknown_roles s
1913 | isTyVarTy ty
1914 = True
1915 | otherwise
1916 = False
1917
1918 {-
1919 -- | Make a listing of role signatures for all the parameterised tycons
1920 -- used in the provided types
1921
1922
1923 -- SLPJ Jun 15: I could not convince myself that these hints were really
1924 -- useful. Maybe they are, but I think we need more work to make them
1925 -- actually helpful.
1926 mkRoleSigs :: Type -> Type -> SDoc
1927 mkRoleSigs ty1 ty2
1928 = ppUnless (null role_sigs) $
1929 hang (text "Relevant role signatures:")
1930 2 (vcat role_sigs)
1931 where
1932 tcs = nameEnvElts $ tyConsOfType ty1 `plusNameEnv` tyConsOfType ty2
1933 role_sigs = mapMaybe ppr_role_sig tcs
1934
1935 ppr_role_sig tc
1936 | null roles -- if there are no parameters, don't bother printing
1937 = Nothing
1938 | isBuiltInSyntax (tyConName tc) -- don't print roles for (->), etc.
1939 = Nothing
1940 | otherwise
1941 = Just $ hsep $ [text "type role", ppr tc] ++ map ppr roles
1942 where
1943 roles = tyConRoles tc
1944 -}
1945
1946 mkEqErr_help :: DynFlags -> ReportErrCtxt -> Report
1947 -> Ct
1948 -> Maybe SwapFlag -- Nothing <=> not sure
1949 -> TcType -> TcType -> TcM ErrMsg
1950 mkEqErr_help dflags ctxt report ct oriented ty1 ty2
1951 | Just (tv1, co1) <- tcGetCastedTyVar_maybe ty1
1952 = mkTyVarEqErr dflags ctxt report ct oriented tv1 co1 ty2
1953 | Just (tv2, co2) <- tcGetCastedTyVar_maybe ty2
1954 = mkTyVarEqErr dflags ctxt report ct swapped tv2 co2 ty1
1955 | otherwise
1956 = reportEqErr ctxt report ct oriented ty1 ty2
1957 where
1958 swapped = fmap flipSwap oriented
1959
1960 reportEqErr :: ReportErrCtxt -> Report
1961 -> Ct
1962 -> Maybe SwapFlag -- Nothing <=> not sure
1963 -> TcType -> TcType -> TcM ErrMsg
1964 reportEqErr ctxt report ct oriented ty1 ty2
1965 = mkErrorMsgFromCt ctxt ct (mconcat [misMatch, report, eqInfo])
1966 where misMatch = important $ misMatchOrCND ctxt ct oriented ty1 ty2
1967 eqInfo = important $ mkEqInfoMsg ct ty1 ty2
1968
1969 mkTyVarEqErr, mkTyVarEqErr'
1970 :: DynFlags -> ReportErrCtxt -> Report -> Ct
1971 -> Maybe SwapFlag -> TcTyVar -> TcCoercionN -> TcType -> TcM ErrMsg
1972 -- tv1 and ty2 are already tidied
1973 mkTyVarEqErr dflags ctxt report ct oriented tv1 co1 ty2
1974 = do { traceTc "mkTyVarEqErr" (ppr ct $$ ppr tv1 $$ ppr co1 $$ ppr ty2)
1975 ; mkTyVarEqErr' dflags ctxt report ct oriented tv1 co1 ty2 }
1976
1977 mkTyVarEqErr' dflags ctxt report ct oriented tv1 co1 ty2
1978 | not insoluble_occurs_check -- See Note [Occurs check wins]
1979 , isUserSkolem ctxt tv1 -- ty2 won't be a meta-tyvar, or else the thing would
1980 -- be oriented the other way round;
1981 -- see TcCanonical.canEqTyVarTyVar
1982 || isSigTyVar tv1 && not (isTyVarTy ty2)
1983 || ctEqRel ct == ReprEq
1984 -- the cases below don't really apply to ReprEq (except occurs check)
1985 = mkErrorMsgFromCt ctxt ct $ mconcat
1986 [ important $ misMatchOrCND ctxt ct oriented ty1 ty2
1987 , important $ extraTyVarEqInfo ctxt tv1 ty2
1988 , report
1989 ]
1990
1991 | OC_Occurs <- occ_check_expand
1992 -- We report an "occurs check" even for a ~ F t a, where F is a type
1993 -- function; it's not insoluble (because in principle F could reduce)
1994 -- but we have certainly been unable to solve it
1995 -- See Note [Occurs check error] in TcCanonical
1996 = do { let main_msg = addArising (ctOrigin ct) $
1997 hang (text "Occurs check: cannot construct the infinite" <+> what <> colon)
1998 2 (sep [ppr ty1, char '~', ppr ty2])
1999
2000 extra2 = important $ mkEqInfoMsg ct ty1 ty2
2001
2002 interesting_tyvars = filter (not . noFreeVarsOfType . tyVarKind) $
2003 filter isTyVar $
2004 fvVarList $
2005 tyCoFVsOfType ty1 `unionFV` tyCoFVsOfType ty2
2006 extra3 = relevant_bindings $
2007 ppWhen (not (null interesting_tyvars)) $
2008 hang (text "Type variable kinds:") 2 $
2009 vcat (map (tyvar_binding . tidyTyVarOcc (cec_tidy ctxt))
2010 interesting_tyvars)
2011
2012 tyvar_binding tv = ppr tv <+> dcolon <+> ppr (tyVarKind tv)
2013 ; mkErrorMsgFromCt ctxt ct $
2014 mconcat [important main_msg, extra2, extra3, report] }
2015
2016 | OC_Bad <- occ_check_expand
2017 = do { let msg = vcat [ text "Cannot instantiate unification variable"
2018 <+> quotes (ppr tv1)
2019 , hang (text "with a" <+> what <+> text "involving foralls:") 2 (ppr ty2)
2020 , nest 2 (text "GHC doesn't yet support impredicative polymorphism") ]
2021 -- Unlike the other reports, this discards the old 'report_important'
2022 -- instead of augmenting it. This is because the details are not likely
2023 -- to be helpful since this is just an unimplemented feature.
2024 ; mkErrorMsgFromCt ctxt ct $ report { report_important = [msg] } }
2025
2026 -- check for heterogeneous equality next; see Note [Equalities with incompatible kinds]
2027 -- in TcCanonical
2028 | not (k1 `tcEqType` k2)
2029 = do { let main_msg = addArising (ctOrigin ct) $
2030 vcat [ hang (text "Kind mismatch: cannot unify" <+>
2031 parens (ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1)) <+>
2032 text "with:")
2033 2 (sep [ppr ty2, dcolon, ppr k2])
2034 , text "Their kinds differ." ]
2035 cast_msg
2036 | isTcReflexiveCo co1 = empty
2037 | otherwise = text "NB:" <+> ppr tv1 <+>
2038 text "was casted to have kind" <+>
2039 quotes (ppr k1)
2040
2041 ; mkErrorMsgFromCt ctxt ct (mconcat [important main_msg, important cast_msg, report]) }
2042
2043 -- If the immediately-enclosing implication has 'tv' a skolem, and
2044 -- we know by now its an InferSkol kind of skolem, then presumably
2045 -- it started life as a SigTv, else it'd have been unified, given
2046 -- that there's no occurs-check or forall problem
2047 | (implic:_) <- cec_encl ctxt
2048 , Implic { ic_skols = skols } <- implic
2049 , tv1 `elem` skols
2050 = mkErrorMsgFromCt ctxt ct $ mconcat
2051 [ important $ misMatchMsg ct oriented ty1 ty2
2052 , important $ extraTyVarEqInfo ctxt tv1 ty2
2053 , report
2054 ]
2055
2056 -- Check for skolem escape
2057 | (implic:_) <- cec_encl ctxt -- Get the innermost context
2058 , Implic { ic_env = env, ic_skols = skols, ic_info = skol_info } <- implic
2059 , let esc_skols = filter (`elemVarSet` (tyCoVarsOfType ty2)) skols
2060 , not (null esc_skols)
2061 = do { let msg = important $ misMatchMsg ct oriented ty1 ty2
2062 esc_doc = sep [ text "because" <+> what <+> text "variable" <> plural esc_skols
2063 <+> pprQuotedList esc_skols
2064 , text "would escape" <+>
2065 if isSingleton esc_skols then text "its scope"
2066 else text "their scope" ]
2067 tv_extra = important $
2068 vcat [ nest 2 $ esc_doc
2069 , sep [ (if isSingleton esc_skols
2070 then text "This (rigid, skolem)" <+>
2071 what <+> text "variable is"
2072 else text "These (rigid, skolem)" <+>
2073 what <+> text "variables are")
2074 <+> text "bound by"
2075 , nest 2 $ ppr skol_info
2076 , nest 2 $ text "at" <+> ppr (tcl_loc env) ] ]
2077 ; mkErrorMsgFromCt ctxt ct (mconcat [msg, tv_extra, report]) }
2078
2079 -- Nastiest case: attempt to unify an untouchable variable
2080 -- So tv is a meta tyvar (or started that way before we
2081 -- generalised it). So presumably it is an *untouchable*
2082 -- meta tyvar or a SigTv, else it'd have been unified
2083 -- See Note [Error messages for untouchables]
2084 | (implic:_) <- cec_encl ctxt -- Get the innermost context
2085 , Implic { ic_env = env, ic_given = given
2086 , ic_tclvl = lvl, ic_info = skol_info } <- implic
2087 = ASSERT2( not (isTouchableMetaTyVar lvl tv1)
2088 , ppr tv1 $$ ppr lvl ) -- See Note [Error messages for untouchables]
2089 do { let msg = important $ misMatchMsg ct oriented ty1 ty2
2090 tclvl_extra = important $
2091 nest 2 $
2092 sep [ quotes (ppr tv1) <+> text "is untouchable"
2093 , nest 2 $ text "inside the constraints:" <+> pprEvVarTheta given
2094 , nest 2 $ text "bound by" <+> ppr skol_info
2095 , nest 2 $ text "at" <+> ppr (tcl_loc env) ]
2096 tv_extra = important $ extraTyVarEqInfo ctxt tv1 ty2
2097 add_sig = important $ suggestAddSig ctxt ty1 ty2
2098 ; mkErrorMsgFromCt ctxt ct $ mconcat
2099 [msg, tclvl_extra, tv_extra, add_sig, report] }
2100
2101 | otherwise
2102 = reportEqErr ctxt report ct oriented (mkTyVarTy tv1) ty2
2103 -- This *can* happen (Trac #6123, and test T2627b)
2104 -- Consider an ambiguous top-level constraint (a ~ F a)
2105 -- Not an occurs check, because F is a type function.
2106 where
2107 Pair _ k1 = tcCoercionKind co1
2108 k2 = typeKind ty2
2109
2110 ty1 = mkTyVarTy tv1
2111 occ_check_expand = occCheckForErrors dflags tv1 ty2
2112 insoluble_occurs_check = isInsolubleOccursCheck (ctEqRel ct) tv1 ty2
2113
2114 what = case ctLocTypeOrKind_maybe (ctLoc ct) of
2115 Just KindLevel -> text "kind"
2116 _ -> text "type"
2117
2118 mkEqInfoMsg :: Ct -> TcType -> TcType -> SDoc
2119 -- Report (a) ambiguity if either side is a type function application
2120 -- e.g. F a0 ~ Int
2121 -- (b) warning about injectivity if both sides are the same
2122 -- type function application F a ~ F b
2123 -- See Note [Non-injective type functions]
2124 -- (c) warning about -fprint-explicit-kinds if that might be helpful
2125 mkEqInfoMsg ct ty1 ty2
2126 = tyfun_msg $$ ambig_msg $$ invis_msg
2127 where
2128 mb_fun1 = isTyFun_maybe ty1
2129 mb_fun2 = isTyFun_maybe ty2
2130
2131 ambig_msg | isJust mb_fun1 || isJust mb_fun2
2132 = snd (mkAmbigMsg False ct)
2133 | otherwise = empty
2134
2135 -- better to check the exp/act types in the CtOrigin than the actual
2136 -- mismatched types for suggestion about -fprint-explicit-kinds
2137 (act_ty, exp_ty) = case ctOrigin ct of
2138 TypeEqOrigin { uo_actual = act
2139 , uo_expected = exp } -> (act, exp)
2140 _ -> (ty1, ty2)
2141
2142 invis_msg | Just vis <- tcEqTypeVis act_ty exp_ty
2143 , not vis
2144 = ppSuggestExplicitKinds
2145 | otherwise
2146 = empty
2147
2148 tyfun_msg | Just tc1 <- mb_fun1
2149 , Just tc2 <- mb_fun2
2150 , tc1 == tc2
2151 , not (isInjectiveTyCon tc1 Nominal)
2152 = text "NB:" <+> quotes (ppr tc1)
2153 <+> text "is a non-injective type family"
2154 | otherwise = empty
2155
2156 isUserSkolem :: ReportErrCtxt -> TcTyVar -> Bool
2157 -- See Note [Reporting occurs-check errors]
2158 isUserSkolem ctxt tv
2159 = isSkolemTyVar tv && any is_user_skol_tv (cec_encl ctxt)
2160 where
2161 is_user_skol_tv (Implic { ic_skols = sks, ic_info = skol_info })
2162 = tv `elem` sks && is_user_skol_info skol_info
2163
2164 is_user_skol_info (InferSkol {}) = False
2165 is_user_skol_info _ = True
2166
2167 misMatchOrCND :: ReportErrCtxt -> Ct
2168 -> Maybe SwapFlag -> TcType -> TcType -> SDoc
2169 -- If oriented then ty1 is actual, ty2 is expected
2170 misMatchOrCND ctxt ct oriented ty1 ty2
2171 | null givens ||
2172 (isRigidTy ty1 && isRigidTy ty2) ||
2173 isGivenCt ct
2174 -- If the equality is unconditionally insoluble
2175 -- or there is no context, don't report the context
2176 = misMatchMsg ct oriented ty1 ty2
2177 | otherwise
2178 = couldNotDeduce givens ([eq_pred], orig)
2179 where
2180 ev = ctEvidence ct
2181 eq_pred = ctEvPred ev
2182 orig = ctEvOrigin ev
2183 givens = [ given | given <- getUserGivens ctxt, not (ic_no_eqs given)]
2184 -- Keep only UserGivens that have some equalities
2185
2186 couldNotDeduce :: [UserGiven] -> (ThetaType, CtOrigin) -> SDoc
2187 couldNotDeduce givens (wanteds, orig)
2188 = vcat [ addArising orig (text "Could not deduce:" <+> pprTheta wanteds)
2189 , vcat (pp_givens givens)]
2190
2191 pp_givens :: [UserGiven] -> [SDoc]
2192 pp_givens givens
2193 = case givens of
2194 [] -> []
2195 (g:gs) -> ppr_given (text "from the context:") g
2196 : map (ppr_given (text "or from:")) gs
2197 where
2198 ppr_given herald (Implic { ic_given = gs, ic_info = skol_info
2199 , ic_env = env })
2200 = hang (herald <+> pprEvVarTheta gs)
2201 2 (sep [ text "bound by" <+> ppr skol_info
2202 , text "at" <+> ppr (tcl_loc env) ])
2203
2204 extraTyVarEqInfo :: ReportErrCtxt -> TcTyVar -> TcType -> SDoc
2205 -- Add on extra info about skolem constants
2206 -- NB: The types themselves are already tidied
2207 extraTyVarEqInfo ctxt tv1 ty2
2208 = extraTyVarInfo ctxt tv1 $$ ty_extra ty2
2209 where
2210 ty_extra ty = case tcGetTyVar_maybe ty of
2211 Just tv -> extraTyVarInfo ctxt tv
2212 Nothing -> empty
2213
2214 extraTyVarInfo :: ReportErrCtxt -> TcTyVar -> SDoc
2215 extraTyVarInfo ctxt tv
2216 = ASSERT2( isTyVar tv, ppr tv )
2217 case tcTyVarDetails tv of
2218 SkolemTv {} -> pprSkols ctxt [tv]
2219 RuntimeUnk {} -> quotes (ppr tv) <+> text "is an interactive-debugger skolem"
2220 MetaTv {} -> empty
2221
2222 suggestAddSig :: ReportErrCtxt -> TcType -> TcType -> SDoc
2223 -- See Note [Suggest adding a type signature]
2224 suggestAddSig ctxt ty1 ty2
2225 | null inferred_bndrs
2226 = empty
2227 | [bndr] <- inferred_bndrs
2228 = text "Possible fix: add a type signature for" <+> quotes (ppr bndr)
2229 | otherwise
2230 = text "Possible fix: add type signatures for some or all of" <+> (ppr inferred_bndrs)
2231 where
2232 inferred_bndrs = nub (get_inf ty1 ++ get_inf ty2)
2233 get_inf ty | Just tv <- tcGetTyVar_maybe ty
2234 , isSkolemTyVar tv
2235 , (implic, _) : _ <- getSkolemInfo (cec_encl ctxt) [tv]
2236 , InferSkol prs <- ic_info implic
2237 = map fst prs
2238 | otherwise
2239 = []
2240
2241 --------------------
2242 misMatchMsg :: Ct -> Maybe SwapFlag -> TcType -> TcType -> SDoc
2243 -- Types are already tidy
2244 -- If oriented then ty1 is actual, ty2 is expected
2245 misMatchMsg ct oriented ty1 ty2
2246 | Just NotSwapped <- oriented
2247 = misMatchMsg ct (Just IsSwapped) ty2 ty1
2248
2249 -- These next two cases are when we're about to report, e.g., that
2250 -- 'LiftedRep doesn't match 'VoidRep. Much better just to say
2251 -- lifted vs. unlifted
2252 | Just (tc1, []) <- splitTyConApp_maybe ty1
2253 , tc1 `hasKey` liftedRepDataConKey
2254 = lifted_vs_unlifted
2255
2256 | Just (tc2, []) <- splitTyConApp_maybe ty2
2257 , tc2 `hasKey` liftedRepDataConKey
2258 = lifted_vs_unlifted
2259
2260 | otherwise -- So now we have Nothing or (Just IsSwapped)
2261 -- For some reason we treat Nothing like IsSwapped
2262 = addArising orig $
2263 sep [ text herald1 <+> quotes (ppr ty1)
2264 , nest padding $
2265 text herald2 <+> quotes (ppr ty2)
2266 , sameOccExtra ty2 ty1 ]
2267 where
2268 herald1 = conc [ "Couldn't match"
2269 , if is_repr then "representation of" else ""
2270 , if is_oriented then "expected" else ""
2271 , what ]
2272 herald2 = conc [ "with"
2273 , if is_repr then "that of" else ""
2274 , if is_oriented then ("actual " ++ what) else "" ]
2275 padding = length herald1 - length herald2
2276
2277 is_repr = case ctEqRel ct of { ReprEq -> True; NomEq -> False }
2278 is_oriented = isJust oriented
2279
2280 orig = ctOrigin ct
2281 what = case ctLocTypeOrKind_maybe (ctLoc ct) of
2282 Just KindLevel -> "kind"
2283 _ -> "type"
2284
2285 conc :: [String] -> String
2286 conc = foldr1 add_space
2287
2288 add_space :: String -> String -> String
2289 add_space s1 s2 | null s1 = s2
2290 | null s2 = s1
2291 | otherwise = s1 ++ (' ' : s2)
2292
2293 lifted_vs_unlifted
2294 = addArising orig $
2295 text "Couldn't match a lifted type with an unlifted type"
2296
2297 mkExpectedActualMsg :: Type -> Type -> CtOrigin -> Maybe TypeOrKind -> Bool
2298 -> (Bool, Maybe SwapFlag, SDoc)
2299 -- NotSwapped means (actual, expected), IsSwapped is the reverse
2300 -- First return val is whether or not to print a herald above this msg
2301 mkExpectedActualMsg ty1 ty2 (TypeEqOrigin { uo_actual = act
2302 , uo_expected = exp
2303 , uo_thing = maybe_thing })
2304 m_level printExpanded
2305 | KindLevel <- level, occurs_check_error = (True, Nothing, empty)
2306 | isUnliftedTypeKind act, isLiftedTypeKind exp = (False, Nothing, msg2)
2307 | isLiftedTypeKind act, isUnliftedTypeKind exp = (False, Nothing, msg3)
2308 | isLiftedTypeKind exp && not (isConstraintKind exp)
2309 = (False, Nothing, msg4)
2310 | Just msg <- num_args_msg = (False, Nothing, msg $$ msg1)
2311 | KindLevel <- level, Just th <- maybe_thing = (False, Nothing, msg5 th)
2312 | act `pickyEqType` ty1, exp `pickyEqType` ty2 = (True, Just NotSwapped, empty)
2313 | exp `pickyEqType` ty1, act `pickyEqType` ty2 = (True, Just IsSwapped, empty)
2314 | otherwise = (True, Nothing, msg1)
2315 where
2316 level = m_level `orElse` TypeLevel
2317
2318 occurs_check_error
2319 | Just act_tv <- tcGetTyVar_maybe act
2320 , act_tv `elemVarSet` tyCoVarsOfType exp
2321 = True
2322 | Just exp_tv <- tcGetTyVar_maybe exp
2323 , exp_tv `elemVarSet` tyCoVarsOfType act
2324 = True
2325 | otherwise
2326 = False
2327
2328 sort = case level of
2329 TypeLevel -> text "type"
2330 KindLevel -> text "kind"
2331
2332 msg1 = case level of
2333 KindLevel
2334 | Just th <- maybe_thing
2335 -> msg5 th
2336
2337 _ | not (act `pickyEqType` exp)
2338 -> vcat [ text "Expected" <+> sort <> colon <+> ppr exp
2339 , text " Actual" <+> sort <> colon <+> ppr act
2340 , if printExpanded then expandedTys else empty ]
2341
2342 | otherwise
2343 -> empty
2344
2345 thing_msg = case maybe_thing of
2346 Just thing -> \_ -> quotes thing <+> text "is"
2347 Nothing -> \vowel -> text "got a" <>
2348 if vowel then char 'n' else empty
2349 msg2 = sep [ text "Expecting a lifted type, but"
2350 , thing_msg True, text "unlifted" ]
2351 msg3 = sep [ text "Expecting an unlifted type, but"
2352 , thing_msg False, text "lifted" ]
2353 msg4 = maybe_num_args_msg $$
2354 sep [ text "Expected a type, but"
2355 , maybe (text "found something with kind")
2356 (\thing -> quotes thing <+> text "has kind")
2357 maybe_thing
2358 , quotes (pprWithTYPE act) ]
2359
2360 msg5 th = hang (text "Expected" <+> kind_desc <> comma)
2361 2 (text "but" <+> quotes th <+> text "has kind" <+>
2362 quotes (ppr act))
2363 where
2364 kind_desc | isConstraintKind exp = text "a constraint"
2365
2366 -- TYPE t0
2367 | Just (tc, [arg]) <- tcSplitTyConApp_maybe exp
2368 , tc `hasKey` tYPETyConKey
2369 , tcIsTyVarTy arg = sdocWithDynFlags $ \dflags ->
2370 if gopt Opt_PrintExplicitRuntimeReps dflags
2371 then text "kind" <+> quotes (ppr exp)
2372 else text "a type"
2373
2374 | otherwise = text "kind" <+> quotes (ppr exp)
2375
2376 num_args_msg = case level of
2377 KindLevel
2378 | not (isMetaTyVarTy exp) && not (isMetaTyVarTy act)
2379 -- if one is a meta-tyvar, then it's possible that the user
2380 -- has asked for something impredicative, and we couldn't unify.
2381 -- Don't bother with counting arguments.
2382 -> let n_act = count_args act
2383 n_exp = count_args exp in
2384 case n_act - n_exp of
2385 n | n > 0 -- we don't know how many args there are, so don't
2386 -- recommend removing args that aren't
2387 , Just thing <- maybe_thing
2388 -> Just $ text "Expecting" <+> speakN (abs n) <+>
2389 more <+> quotes thing
2390 where
2391 more
2392 | n == 1 = text "more argument to"
2393 | otherwise = text "more arguments to" -- n > 1
2394 _ -> Nothing
2395
2396 _ -> Nothing
2397
2398 maybe_num_args_msg = case num_args_msg of
2399 Nothing -> empty
2400 Just m -> m
2401
2402 count_args ty = count isVisibleBinder $ fst $ splitPiTys ty
2403
2404 expandedTys =
2405 ppUnless (expTy1 `pickyEqType` exp && expTy2 `pickyEqType` act) $ vcat
2406 [ text "Type synonyms expanded:"
2407 , text "Expected type:" <+> ppr expTy1
2408 , text " Actual type:" <+> ppr expTy2
2409 ]
2410
2411 (expTy1, expTy2) = expandSynonymsToMatch exp act
2412
2413 mkExpectedActualMsg _ _ _ _ _ = panic "mkExpectedAcutalMsg"
2414
2415 {- Note [Insoluble occurs check wins]
2416 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2417 Consider [G] a ~ [a], [W] a ~ [a] (Trac #13674). The Given is insoluble
2418 so we don't use it for rewriting. The Wanted is also insoluble, and
2419 we don't solve it from the Given. It's very confusing to say
2420 Cannot solve a ~ [a] from given constraints a ~ [a]
2421
2422 And indeed even thinking about the Givens is silly; [W] a ~ [a] is
2423 just as insoluble as Int ~ Bool.
2424
2425 Conclusion: if there's an insoluble occurs check (isInsolubleOccursCheck)
2426 then report it first.
2427
2428 (NB: there are potentially-soluble ones, like (a ~ F a b), and we don't
2429 want to be as draconian with them.)
2430
2431 Note [Expanding type synonyms to make types similar]
2432 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2433
2434 In type error messages, if -fprint-expanded-types is used, we want to expand
2435 type synonyms to make expected and found types as similar as possible, but we
2436 shouldn't expand types too much to make type messages even more verbose and
2437 harder to understand. The whole point here is to make the difference in expected
2438 and found types clearer.
2439
2440 `expandSynonymsToMatch` does this, it takes two types, and expands type synonyms
2441 only as much as necessary. Given two types t1 and t2:
2442
2443 * If they're already same, it just returns the types.
2444
2445 * If they're in form `C1 t1_1 .. t1_n` and `C2 t2_1 .. t2_m` (C1 and C2 are
2446 type constructors), it expands C1 and C2 if they're different type synonyms.
2447 Then it recursively does the same thing on expanded types. If C1 and C2 are
2448 same, then it applies the same procedure to arguments of C1 and arguments of
2449 C2 to make them as similar as possible.
2450
2451 Most important thing here is to keep number of synonym expansions at
2452 minimum. For example, if t1 is `T (T3, T5, Int)` and t2 is `T (T5, T3,
2453 Bool)` where T5 = T4, T4 = T3, ..., T1 = X, it returns `T (T3, T3, Int)` and
2454 `T (T3, T3, Bool)`.
2455
2456 * Otherwise types don't have same shapes and so the difference is clearly
2457 visible. It doesn't do any expansions and show these types.
2458
2459 Note that we only expand top-layer type synonyms. Only when top-layer
2460 constructors are the same we start expanding inner type synonyms.
2461
2462 Suppose top-layer type synonyms of t1 and t2 can expand N and M times,
2463 respectively. If their type-synonym-expanded forms will meet at some point (i.e.
2464 will have same shapes according to `sameShapes` function), it's possible to find
2465 where they meet in O(N+M) top-layer type synonym expansions and O(min(N,M))
2466 comparisons. We first collect all the top-layer expansions of t1 and t2 in two
2467 lists, then drop the prefix of the longer list so that they have same lengths.
2468 Then we search through both lists in parallel, and return the first pair of
2469 types that have same shapes. Inner types of these two types with same shapes
2470 are then expanded using the same algorithm.
2471
2472 In case they don't meet, we return the last pair of types in the lists, which
2473 has top-layer type synonyms completely expanded. (in this case the inner types
2474 are not expanded at all, as the current form already shows the type error)
2475 -}
2476
2477 -- | Expand type synonyms in given types only enough to make them as similar as
2478 -- possible. Returned types are the same in terms of used type synonyms.
2479 --
2480 -- To expand all synonyms, see 'Type.expandTypeSynonyms'.
2481 --
2482 -- See `ExpandSynsFail` tests in tests testsuite/tests/typecheck/should_fail for
2483 -- some examples of how this should work.
2484 expandSynonymsToMatch :: Type -> Type -> (Type, Type)
2485 expandSynonymsToMatch ty1 ty2 = (ty1_ret, ty2_ret)
2486 where
2487 (ty1_ret, ty2_ret) = go ty1 ty2
2488
2489 -- | Returns (type synonym expanded version of first type,
2490 -- type synonym expanded version of second type)
2491 go :: Type -> Type -> (Type, Type)
2492 go t1 t2
2493 | t1 `pickyEqType` t2 =
2494 -- Types are same, nothing to do
2495 (t1, t2)
2496
2497 go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
2498 | tc1 == tc2 =
2499 -- Type constructors are same. They may be synonyms, but we don't
2500 -- expand further.
2501 let (tys1', tys2') =
2502 unzip (zipWith (\ty1 ty2 -> go ty1 ty2) tys1 tys2)
2503 in (TyConApp tc1 tys1', TyConApp tc2 tys2')
2504
2505 go (AppTy t1_1 t1_2) (AppTy t2_1 t2_2) =
2506 let (t1_1', t2_1') = go t1_1 t2_1
2507 (t1_2', t2_2') = go t1_2 t2_2
2508 in (mkAppTy t1_1' t1_2', mkAppTy t2_1' t2_2')
2509
2510 go (FunTy t1_1 t1_2) (FunTy t2_1 t2_2) =
2511 let (t1_1', t2_1') = go t1_1 t2_1
2512 (t1_2', t2_2') = go t1_2 t2_2
2513 in (mkFunTy t1_1' t1_2', mkFunTy t2_1' t2_2')
2514
2515 go (ForAllTy b1 t1) (ForAllTy b2 t2) =
2516 -- NOTE: We may have a bug here, but we just can't reproduce it easily.
2517 -- See D1016 comments for details and our attempts at producing a test
2518 -- case. Short version: We probably need RnEnv2 to really get this right.
2519 let (t1', t2') = go t1 t2
2520 in (ForAllTy b1 t1', ForAllTy b2 t2')
2521
2522 go (CastTy ty1 _) ty2 = go ty1 ty2
2523 go ty1 (CastTy ty2 _) = go ty1 ty2
2524
2525 go t1 t2 =
2526 -- See Note [Expanding type synonyms to make types similar] for how this
2527 -- works
2528 let
2529 t1_exp_tys = t1 : tyExpansions t1
2530 t2_exp_tys = t2 : tyExpansions t2
2531 t1_exps = length t1_exp_tys
2532 t2_exps = length t2_exp_tys
2533 dif = abs (t1_exps - t2_exps)
2534 in
2535 followExpansions $
2536 zipEqual "expandSynonymsToMatch.go"
2537 (if t1_exps > t2_exps then drop dif t1_exp_tys else t1_exp_tys)
2538 (if t2_exps > t1_exps then drop dif t2_exp_tys else t2_exp_tys)
2539
2540 -- | Expand the top layer type synonyms repeatedly, collect expansions in a
2541 -- list. The list does not include the original type.
2542 --
2543 -- Example, if you have:
2544 --
2545 -- type T10 = T9
2546 -- type T9 = T8
2547 -- ...
2548 -- type T0 = Int
2549 --
2550 -- `tyExpansions T10` returns [T9, T8, T7, ... Int]
2551 --
2552 -- This only expands the top layer, so if you have:
2553 --
2554 -- type M a = Maybe a
2555 --
2556 -- `tyExpansions (M T10)` returns [Maybe T10] (T10 is not expanded)
2557 tyExpansions :: Type -> [Type]
2558 tyExpansions = unfoldr (\t -> (\x -> (x, x)) `fmap` tcView t)
2559
2560 -- | Drop the type pairs until types in a pair look alike (i.e. the outer
2561 -- constructors are the same).
2562 followExpansions :: [(Type, Type)] -> (Type, Type)
2563 followExpansions [] = pprPanic "followExpansions" empty
2564 followExpansions [(t1, t2)]
2565 | sameShapes t1 t2 = go t1 t2 -- expand subtrees
2566 | otherwise = (t1, t2) -- the difference is already visible
2567 followExpansions ((t1, t2) : tss)
2568 -- Traverse subtrees when the outer shapes are the same
2569 | sameShapes t1 t2 = go t1 t2
2570 -- Otherwise follow the expansions until they look alike
2571 | otherwise = followExpansions tss
2572
2573 sameShapes :: Type -> Type -> Bool
2574 sameShapes AppTy{} AppTy{} = True
2575 sameShapes (TyConApp tc1 _) (TyConApp tc2 _) = tc1 == tc2
2576 sameShapes (FunTy {}) (FunTy {}) = True
2577 sameShapes (ForAllTy {}) (ForAllTy {}) = True
2578 sameShapes (CastTy ty1 _) ty2 = sameShapes ty1 ty2
2579 sameShapes ty1 (CastTy ty2 _) = sameShapes ty1 ty2
2580 sameShapes _ _ = False
2581
2582 sameOccExtra :: TcType -> TcType -> SDoc
2583 -- See Note [Disambiguating (X ~ X) errors]
2584 sameOccExtra ty1 ty2
2585 | Just (tc1, _) <- tcSplitTyConApp_maybe ty1
2586 , Just (tc2, _) <- tcSplitTyConApp_maybe ty2
2587 , let n1 = tyConName tc1
2588 n2 = tyConName tc2
2589 same_occ = nameOccName n1 == nameOccName n2
2590 same_pkg = moduleUnitId (nameModule n1) == moduleUnitId (nameModule n2)
2591 , n1 /= n2 -- Different Names
2592 , same_occ -- but same OccName
2593 = text "NB:" <+> (ppr_from same_pkg n1 $$ ppr_from same_pkg n2)
2594 | otherwise
2595 = empty
2596 where
2597 ppr_from same_pkg nm
2598 | isGoodSrcSpan loc
2599 = hang (quotes (ppr nm) <+> text "is defined at")
2600 2 (ppr loc)
2601 | otherwise -- Imported things have an UnhelpfulSrcSpan
2602 = hang (quotes (ppr nm))
2603 2 (sep [ text "is defined in" <+> quotes (ppr (moduleName mod))
2604 , ppUnless (same_pkg || pkg == mainUnitId) $
2605 nest 4 $ text "in package" <+> quotes (ppr pkg) ])
2606 where
2607 pkg = moduleUnitId mod
2608 mod = nameModule nm
2609 loc = nameSrcSpan nm
2610
2611 {-
2612 Note [Suggest adding a type signature]
2613 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2614 The OutsideIn algorithm rejects GADT programs that don't have a principal
2615 type, and indeed some that do. Example:
2616 data T a where
2617 MkT :: Int -> T Int
2618
2619 f (MkT n) = n
2620
2621 Does this have type f :: T a -> a, or f :: T a -> Int?
2622 The error that shows up tends to be an attempt to unify an
2623 untouchable type variable. So suggestAddSig sees if the offending
2624 type variable is bound by an *inferred* signature, and suggests
2625 adding a declared signature instead.
2626
2627 This initially came up in Trac #8968, concerning pattern synonyms.
2628
2629 Note [Disambiguating (X ~ X) errors]
2630 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2631 See Trac #8278
2632
2633 Note [Reporting occurs-check errors]
2634 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2635 Given (a ~ [a]), if 'a' is a rigid type variable bound by a user-supplied
2636 type signature, then the best thing is to report that we can't unify
2637 a with [a], because a is a skolem variable. That avoids the confusing
2638 "occur-check" error message.
2639
2640 But nowadays when inferring the type of a function with no type signature,
2641 even if there are errors inside, we still generalise its signature and
2642 carry on. For example
2643 f x = x:x
2644 Here we will infer something like
2645 f :: forall a. a -> [a]
2646 with a deferred error of (a ~ [a]). So in the deferred unsolved constraint
2647 'a' is now a skolem, but not one bound by the programmer in the context!
2648 Here we really should report an occurs check.
2649
2650 So isUserSkolem distinguishes the two.
2651
2652 Note [Non-injective type functions]
2653 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2654 It's very confusing to get a message like
2655 Couldn't match expected type `Depend s'
2656 against inferred type `Depend s1'
2657 so mkTyFunInfoMsg adds:
2658 NB: `Depend' is type function, and hence may not be injective
2659
2660 Warn of loopy local equalities that were dropped.
2661
2662
2663 ************************************************************************
2664 * *
2665 Type-class errors
2666 * *
2667 ************************************************************************
2668 -}
2669
2670 mkDictErr :: ReportErrCtxt -> [Ct] -> TcM ErrMsg
2671 mkDictErr ctxt cts
2672 = ASSERT( not (null cts) )
2673 do { inst_envs <- tcGetInstEnvs
2674 ; let (ct1:_) = cts -- ct1 just for its location
2675 min_cts = elim_superclasses cts
2676 lookups = map (lookup_cls_inst inst_envs) min_cts
2677 (no_inst_cts, overlap_cts) = partition is_no_inst lookups
2678
2679 -- Report definite no-instance errors,
2680 -- or (iff there are none) overlap errors
2681 -- But we report only one of them (hence 'head') because they all
2682 -- have the same source-location origin, to try avoid a cascade
2683 -- of error from one location
2684 ; (ctxt, err) <- mk_dict_err ctxt (head (no_inst_cts ++ overlap_cts))
2685 ; mkErrorMsgFromCt ctxt ct1 (important err) }
2686 where
2687 no_givens = null (getUserGivens ctxt)
2688
2689 is_no_inst (ct, (matches, unifiers, _))
2690 = no_givens
2691 && null matches
2692 && (null unifiers || all (not . isAmbiguousTyVar) (tyCoVarsOfCtList ct))
2693
2694 lookup_cls_inst inst_envs ct
2695 -- Note [Flattening in error message generation]
2696 = (ct, lookupInstEnv True inst_envs clas (flattenTys emptyInScopeSet tys))
2697 where
2698 (clas, tys) = getClassPredTys (ctPred ct)
2699
2700
2701 -- When simplifying [W] Ord (Set a), we need
2702 -- [W] Eq a, [W] Ord a
2703 -- but we really only want to report the latter
2704 elim_superclasses cts = mkMinimalBySCs ctPred cts
2705
2706 mk_dict_err :: ReportErrCtxt -> (Ct, ClsInstLookupResult)
2707 -> TcM (ReportErrCtxt, SDoc)
2708 -- Report an overlap error if this class constraint results
2709 -- from an overlap (returning Left clas), otherwise return (Right pred)
2710 mk_dict_err ctxt@(CEC {cec_encl = implics}) (ct, (matches, unifiers, unsafe_overlapped))
2711 | null matches -- No matches but perhaps several unifiers
2712 = do { (ctxt, binds_msg, ct) <- relevantBindings True ctxt ct
2713 ; candidate_insts <- get_candidate_instances
2714 ; return (ctxt, cannot_resolve_msg ct candidate_insts binds_msg) }
2715
2716 | null unsafe_overlapped -- Some matches => overlap errors
2717 = return (ctxt, overlap_msg)
2718
2719 | otherwise
2720 = return (ctxt, safe_haskell_msg)
2721 where
2722 orig = ctOrigin ct
2723 pred = ctPred ct
2724 (clas, tys) = getClassPredTys pred
2725 ispecs = [ispec | (ispec, _) <- matches]
2726 unsafe_ispecs = [ispec | (ispec, _) <- unsafe_overlapped]
2727 useful_givens = discardProvCtxtGivens orig (getUserGivensFromImplics implics)
2728 -- useful_givens are the enclosing implications with non-empty givens,
2729 -- modulo the horrid discardProvCtxtGivens
2730
2731 get_candidate_instances :: TcM [ClsInst]
2732 -- See Note [Report candidate instances]
2733 get_candidate_instances
2734 | [ty] <- tys -- Only try for single-parameter classes
2735 = do { instEnvs <- tcGetInstEnvs
2736 ; return (filter (is_candidate_inst ty)
2737 (classInstances instEnvs clas)) }
2738 | otherwise = return []
2739
2740 is_candidate_inst ty inst -- See Note [Report candidate instances]
2741 | [other_ty] <- is_tys inst
2742 , Just (tc1, _) <- tcSplitTyConApp_maybe ty
2743 , Just (tc2, _) <- tcSplitTyConApp_maybe other_ty
2744 = let n1 = tyConName tc1
2745 n2 = tyConName tc2
2746 different_names = n1 /= n2
2747 same_occ_names = nameOccName n1 == nameOccName n2
2748 in different_names && same_occ_names
2749 | otherwise = False
2750
2751 cannot_resolve_msg :: Ct -> [ClsInst] -> SDoc -> SDoc
2752 cannot_resolve_msg ct candidate_insts binds_msg
2753 = vcat [ no_inst_msg
2754 , nest 2 extra_note
2755 , vcat (pp_givens useful_givens)
2756 , mb_patsyn_prov `orElse` empty
2757 , ppWhen (has_ambig_tvs && not (null unifiers && null useful_givens))
2758 (vcat [ ppUnless lead_with_ambig ambig_msg, binds_msg, potential_msg ])
2759
2760 , ppWhen (isNothing mb_patsyn_prov) $
2761 -- Don't suggest fixes for the provided context of a pattern
2762 -- synonym; the right fix is to bind more in the pattern
2763 show_fixes (ctxtFixes has_ambig_tvs pred implics
2764 ++ drv_fixes)
2765 , ppWhen (not (null candidate_insts))
2766 (hang (text "There are instances for similar types:")
2767 2 (vcat (map ppr candidate_insts))) ]
2768 -- See Note [Report candidate instances]
2769 where
2770 orig = ctOrigin ct
2771 -- See Note [Highlighting ambiguous type variables]
2772 lead_with_ambig = has_ambig_tvs && not (any isRuntimeUnkSkol ambig_tvs)
2773 && not (null unifiers) && null useful_givens
2774
2775 (has_ambig_tvs, ambig_msg) = mkAmbigMsg lead_with_ambig ct
2776 ambig_tvs = uncurry (++) (getAmbigTkvs ct)
2777
2778 no_inst_msg
2779 | lead_with_ambig
2780 = ambig_msg <+> pprArising orig
2781 $$ text "prevents the constraint" <+> quotes (pprParendType pred)
2782 <+> text "from being solved."
2783
2784 | null useful_givens
2785 = addArising orig $ text "No instance for"
2786 <+> pprParendType pred
2787
2788 | otherwise
2789 = addArising orig $ text "Could not deduce"
2790 <+> pprParendType pred
2791
2792 potential_msg
2793 = ppWhen (not (null unifiers) && want_potential orig) $
2794 sdocWithDynFlags $ \dflags ->
2795 getPprStyle $ \sty ->
2796 pprPotentials dflags sty potential_hdr unifiers
2797
2798 potential_hdr
2799 = vcat [ ppWhen lead_with_ambig $
2800 text "Probable fix: use a type annotation to specify what"
2801 <+> pprQuotedList ambig_tvs <+> text "should be."
2802 , text "These potential instance" <> plural unifiers
2803 <+> text "exist:"]
2804
2805 mb_patsyn_prov :: Maybe SDoc
2806 mb_patsyn_prov
2807 | not lead_with_ambig
2808 , ProvCtxtOrigin PSB{ psb_def = L _ pat } <- orig
2809 = Just (vcat [ text "In other words, a successful match on the pattern"
2810 , nest 2 $ ppr pat
2811 , text "does not provide the constraint" <+> pprParendType pred ])
2812 | otherwise = Nothing
2813
2814 -- Report "potential instances" only when the constraint arises
2815 -- directly from the user's use of an overloaded function
2816 want_potential (TypeEqOrigin {}) = False
2817 want_potential _ = True
2818
2819 extra_note | any isFunTy (filterOutInvisibleTypes (classTyCon clas) tys)
2820 = text "(maybe you haven't applied a function to enough arguments?)"
2821 | className clas == typeableClassName -- Avoid mysterious "No instance for (Typeable T)
2822 , [_,ty] <- tys -- Look for (Typeable (k->*) (T k))
2823 , Just (tc,_) <- tcSplitTyConApp_maybe ty
2824 , not (isTypeFamilyTyCon tc)
2825 = hang (text "GHC can't yet do polykinded")
2826 2 (text "Typeable" <+>
2827 parens (ppr ty <+> dcolon <+> ppr (typeKind ty)))
2828 | otherwise
2829 = empty
2830
2831 drv_fixes = case orig of
2832 DerivClauseOrigin -> [drv_fix False]
2833 StandAloneDerivOrigin -> [drv_fix True]
2834 DerivOriginDC _ _ standalone -> [drv_fix standalone]
2835 DerivOriginCoerce _ _ _ standalone -> [drv_fix standalone]
2836 _ -> []
2837
2838 drv_fix standalone_wildcard
2839 | standalone_wildcard
2840 = text "fill in the wildcard constraint yourself"
2841 | otherwise
2842 = hang (text "use a standalone 'deriving instance' declaration,")
2843 2 (text "so you can specify the instance context yourself")
2844
2845 -- Normal overlap error
2846 overlap_msg
2847 = ASSERT( not (null matches) )
2848 vcat [ addArising orig (text "Overlapping instances for"
2849 <+> pprType (mkClassPred clas tys))
2850
2851 , ppUnless (null matching_givens) $
2852 sep [text "Matching givens (or their superclasses):"
2853 , nest 2 (vcat matching_givens)]
2854
2855 , sdocWithDynFlags $ \dflags ->
2856 getPprStyle $ \sty ->
2857 pprPotentials dflags sty (text "Matching instances:") $
2858 ispecs ++ unifiers
2859
2860 , ppWhen (null matching_givens && isSingleton matches && null unifiers) $
2861 -- Intuitively, some given matched the wanted in their
2862 -- flattened or rewritten (from given equalities) form
2863 -- but the matcher can't figure that out because the
2864 -- constraints are non-flat and non-rewritten so we
2865 -- simply report back the whole given
2866 -- context. Accelerate Smart.hs showed this problem.
2867 sep [ text "There exists a (perhaps superclass) match:"
2868 , nest 2 (vcat (pp_givens useful_givens))]
2869
2870 , ppWhen (isSingleton matches) $
2871 parens (vcat [ text "The choice depends on the instantiation of" <+>
2872 quotes (pprWithCommas ppr (tyCoVarsOfTypesList tys))
2873 , ppWhen (null (matching_givens)) $
2874 vcat [ text "To pick the first instance above, use IncoherentInstances"
2875 , text "when compiling the other instance declarations"]
2876 ])]
2877
2878 matching_givens = mapMaybe matchable useful_givens
2879
2880 matchable (Implic { ic_given = evvars, ic_info = skol_info, ic_env = env })
2881 = case ev_vars_matching of
2882 [] -> Nothing
2883 _ -> Just $ hang (pprTheta ev_vars_matching)
2884 2 (sep [ text "bound by" <+> ppr skol_info
2885 , text "at" <+> ppr (tcl_loc env) ])
2886 where ev_vars_matching = filter ev_var_matches (map evVarPred evvars)
2887 ev_var_matches ty = case getClassPredTys_maybe ty of
2888 Just (clas', tys')
2889 | clas' == clas
2890 , Just _ <- tcMatchTys tys tys'
2891 -> True
2892 | otherwise
2893 -> any ev_var_matches (immSuperClasses clas' tys')
2894 Nothing -> False
2895
2896 -- Overlap error because of Safe Haskell (first
2897 -- match should be the most specific match)
2898 safe_haskell_msg
2899 = ASSERT( matches `lengthIs` 1 && not (null unsafe_ispecs) )
2900 vcat [ addArising orig (text "Unsafe overlapping instances for"
2901 <+> pprType (mkClassPred clas tys))
2902 , sep [text "The matching instance is:",
2903 nest 2 (pprInstance $ head ispecs)]
2904 , vcat [ text "It is compiled in a Safe module and as such can only"
2905 , text "overlap instances from the same module, however it"
2906 , text "overlaps the following instances from different" <+>
2907 text "modules:"
2908 , nest 2 (vcat [pprInstances $ unsafe_ispecs])
2909 ]
2910 ]
2911
2912
2913 ctxtFixes :: Bool -> PredType -> [Implication] -> [SDoc]
2914 ctxtFixes has_ambig_tvs pred implics
2915 | not has_ambig_tvs
2916 , isTyVarClassPred pred
2917 , (skol:skols) <- usefulContext implics pred
2918 , let what | null skols
2919 , SigSkol (PatSynCtxt {}) _ _ <- skol
2920 = text "\"required\""
2921 | otherwise
2922 = empty
2923 = [sep [ text "add" <+> pprParendType pred
2924 <+> text "to the" <+> what <+> text "context of"
2925 , nest 2 $ ppr_skol skol $$
2926 vcat [ text "or" <+> ppr_skol skol
2927 | skol <- skols ] ] ]
2928 | otherwise = []
2929 where
2930 ppr_skol (PatSkol (RealDataCon dc) _) = text "the data constructor" <+> quotes (ppr dc)
2931 ppr_skol (PatSkol (PatSynCon ps) _) = text "the pattern synonym" <+> quotes (ppr ps)
2932 ppr_skol skol_info = ppr skol_info
2933
2934 discardProvCtxtGivens :: CtOrigin -> [UserGiven] -> [UserGiven]
2935 discardProvCtxtGivens orig givens -- See Note [discardProvCtxtGivens]
2936 | ProvCtxtOrigin (PSB {psb_id = L _ name}) <- orig
2937 = filterOut (discard name) givens
2938 | otherwise
2939 = givens
2940 where
2941 discard n (Implic { ic_info = SigSkol (PatSynCtxt n') _ _ }) = n == n'
2942 discard _ _ = False
2943
2944 usefulContext :: [Implication] -> PredType -> [SkolemInfo]
2945 -- usefulContext picks out the implications whose context
2946 -- the programmer might plausibly augment to solve 'pred'
2947 usefulContext implics pred
2948 = go implics
2949 where
2950 pred_tvs = tyCoVarsOfType pred
2951 go [] = []
2952 go (ic : ics)
2953 | implausible ic = rest
2954 | otherwise = ic_info ic : rest
2955 where
2956 -- Stop when the context binds a variable free in the predicate
2957 rest | any (`elemVarSet` pred_tvs) (ic_skols ic) = []
2958 | otherwise = go ics
2959
2960 implausible ic
2961 | null (ic_skols ic) = True
2962 | implausible_info (ic_info ic) = True
2963 | otherwise = False
2964
2965 implausible_info (SigSkol (InfSigCtxt {}) _ _) = True
2966 implausible_info _ = False
2967 -- Do not suggest adding constraints to an *inferred* type signature
2968
2969 {- Note [Report candidate instances]
2970 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2971 If we have an unsolved (Num Int), where `Int` is not the Prelude Int,
2972 but comes from some other module, then it may be helpful to point out
2973 that there are some similarly named instances elsewhere. So we get
2974 something like
2975 No instance for (Num Int) arising from the literal ‘3’
2976 There are instances for similar types:
2977 instance Num GHC.Types.Int -- Defined in ‘GHC.Num’
2978 Discussion in Trac #9611.
2979
2980 Note [Highlighting ambiguous type variables]
2981 ~-------------------------------------------
2982 When we encounter ambiguous type variables (i.e. type variables
2983 that remain metavariables after type inference), we need a few more
2984 conditions before we can reason that *ambiguity* prevents constraints
2985 from being solved:
2986 - We can't have any givens, as encountering a typeclass error
2987 with given constraints just means we couldn't deduce
2988 a solution satisfying those constraints and as such couldn't
2989 bind the type variable to a known type.
2990 - If we don't have any unifiers, we don't even have potential
2991 instances from which an ambiguity could arise.
2992 - Lastly, I don't want to mess with error reporting for
2993 unknown runtime types so we just fall back to the old message there.
2994 Once these conditions are satisfied, we can safely say that ambiguity prevents
2995 the constraint from being solved.
2996
2997 Note [discardProvCtxtGivens]
2998 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
2999 In most situations we call all enclosing implications "useful". There is one
3000 exception, and that is when the constraint that causes the error is from the
3001 "provided" context of a pattern synonym declaration:
3002
3003 pattern Pat :: (Num a, Eq a) => Show a => a -> Maybe a
3004 -- required => provided => type
3005 pattern Pat x <- (Just x, 4)
3006
3007 When checking the pattern RHS we must check that it does actually bind all
3008 the claimed "provided" constraints; in this case, does the pattern (Just x, 4)
3009 bind the (Show a) constraint. Answer: no!
3010
3011 But the implication we generate for this will look like
3012 forall a. (Num a, Eq a) => [W] Show a
3013 because when checking the pattern we must make the required
3014 constraints available, since they are needed to match the pattern (in
3015 this case the literal '4' needs (Num a, Eq a)).
3016
3017 BUT we don't want to suggest adding (Show a) to the "required" constraints
3018 of the pattern synonym, thus:
3019 pattern Pat :: (Num a, Eq a, Show a) => Show a => a -> Maybe a
3020 It would then typecheck but it's silly. We want the /pattern/ to bind
3021 the alleged "provided" constraints, Show a.
3022
3023 So we suppress that Implication in discardProvCtxtGivens. It's
3024 painfully ad-hoc but the truth is that adding it to the "required"
3025 constraints would work. Suprressing it solves two problems. First,
3026 we never tell the user that we could not deduce a "provided"
3027 constraint from the "required" context. Second, we never give a
3028 possible fix that suggests to add a "provided" constraint to the
3029 "required" context.
3030
3031 For example, without this distinction the above code gives a bad error
3032 message (showing both problems):
3033
3034 error: Could not deduce (Show a) ... from the context: (Eq a)
3035 ... Possible fix: add (Show a) to the context of
3036 the signature for pattern synonym `Pat' ...
3037
3038 -}
3039
3040 show_fixes :: [SDoc] -> SDoc
3041 show_fixes [] = empty
3042 show_fixes (f:fs) = sep [ text "Possible fix:"
3043 , nest 2 (vcat (f : map (text "or" <+>) fs))]
3044
3045 pprPotentials :: DynFlags -> PprStyle -> SDoc -> [ClsInst] -> SDoc
3046 -- See Note [Displaying potential instances]
3047 pprPotentials dflags sty herald insts
3048 | null insts
3049 = empty
3050
3051 | null show_these
3052 = hang herald
3053 2 (vcat [ not_in_scope_msg empty
3054 , flag_hint ])
3055
3056 | otherwise
3057 = hang herald
3058 2 (vcat [ pprInstances show_these
3059 , ppWhen (n_in_scope_hidden > 0) $
3060 text "...plus"
3061 <+> speakNOf n_in_scope_hidden (text "other")
3062 , not_in_scope_msg (text "...plus")
3063 , flag_hint ])
3064 where
3065 n_show = 3 :: Int
3066 show_potentials = gopt Opt_PrintPotentialInstances dflags
3067
3068 (in_scope, not_in_scope) = partition inst_in_scope insts
3069 sorted = sortBy fuzzyClsInstCmp in_scope
3070 show_these | show_potentials = sorted
3071 | otherwise = take n_show sorted
3072 n_in_scope_hidden = length sorted - length show_these
3073
3074 -- "in scope" means that all the type constructors
3075 -- are lexically in scope; these instances are likely
3076 -- to be more useful
3077 inst_in_scope :: ClsInst -> Bool
3078 inst_in_scope cls_inst = nameSetAll name_in_scope $
3079 orphNamesOfTypes (is_tys cls_inst)
3080
3081 name_in_scope name
3082 | isBuiltInSyntax name
3083 = True -- E.g. (->)
3084 | Just mod <- nameModule_maybe name
3085 = qual_in_scope (qualName sty mod (nameOccName name))
3086 | otherwise
3087 = True
3088
3089 qual_in_scope :: QualifyName -> Bool
3090 qual_in_scope NameUnqual = True
3091 qual_in_scope (NameQual {}) = True
3092 qual_in_scope _ = False
3093
3094 not_in_scope_msg herald
3095 | null not_in_scope
3096 = empty
3097 | otherwise
3098 = hang (herald <+> speakNOf (length not_in_scope) (text "instance")
3099 <+> text "involving out-of-scope types")
3100 2 (ppWhen show_potentials (pprInstances not_in_scope))
3101
3102 flag_hint = ppUnless (show_potentials || equalLength show_these insts) $
3103 text "(use -fprint-potential-instances to see them all)"
3104
3105 {- Note [Displaying potential instances]
3106 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
3107 When showing a list of instances for
3108 - overlapping instances (show ones that match)
3109 - no such instance (show ones that could match)
3110 we want to give it a bit of structure. Here's the plan
3111
3112 * Say that an instance is "in scope" if all of the
3113 type constructors it mentions are lexically in scope.
3114 These are the ones most likely to be useful to the programmer.
3115
3116 * Show at most n_show in-scope instances,
3117 and summarise the rest ("plus 3 others")
3118
3119 * Summarise the not-in-scope instances ("plus 4 not in scope")
3120
3121 * Add the flag -fshow-potential-instances which replaces the
3122 summary with the full list
3123 -}
3124
3125 {-
3126 Note [Flattening in error message generation]
3127 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
3128 Consider (C (Maybe (F x))), where F is a type function, and we have
3129 instances
3130 C (Maybe Int) and C (Maybe a)
3131 Since (F x) might turn into Int, this is an overlap situation, and
3132 indeed (because of flattening) the main solver will have refrained
3133 from solving. But by the time we get to error message generation, we've
3134 un-flattened the constraint. So we must *re*-flatten it before looking
3135 up in the instance environment, lest we only report one matching
3136 instance when in fact there are two.
3137
3138 Re-flattening is pretty easy, because we don't need to keep track of
3139 evidence. We don't re-use the code in TcCanonical because that's in
3140 the TcS monad, and we are in TcM here.
3141
3142 Note [Suggest -fprint-explicit-kinds]
3143 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
3144 It can be terribly confusing to get an error message like (Trac #9171)
3145 Couldn't match expected type ‘GetParam Base (GetParam Base Int)’
3146 with actual type ‘GetParam Base (GetParam Base Int)’
3147 The reason may be that the kinds don't match up. Typically you'll get
3148 more useful information, but not when it's as a result of ambiguity.
3149 This test suggests -fprint-explicit-kinds when all the ambiguous type
3150 variables are kind variables.
3151 -}
3152
3153 mkAmbigMsg :: Bool -- True when message has to be at beginning of sentence
3154 -> Ct -> (Bool, SDoc)
3155 mkAmbigMsg prepend_msg ct
3156 | null ambig_kvs && null ambig_tvs = (False, empty)
3157 | otherwise = (True, msg)
3158 where
3159 (ambig_kvs, ambig_tvs) = getAmbigTkvs ct
3160
3161 msg | any isRuntimeUnkSkol ambig_kvs -- See Note [Runtime skolems]
3162 || any isRuntimeUnkSkol ambig_tvs
3163 = vcat [ text "Cannot resolve unknown runtime type"
3164 <> plural ambig_tvs <+> pprQuotedList ambig_tvs
3165 , text "Use :print or :force to determine these types"]
3166
3167 | not (null ambig_tvs)
3168 = pp_ambig (text "type") ambig_tvs
3169
3170 | otherwise -- All ambiguous kind variabes; suggest -fprint-explicit-kinds
3171 -- See Note [Suggest -fprint-explicit-kinds]
3172 = vcat [ pp_ambig (text "kind") ambig_kvs
3173 , ppSuggestExplicitKinds ]
3174
3175 pp_ambig what tkvs
3176 | prepend_msg -- "Ambiguous type variable 't0'"
3177 = text "Ambiguous" <+> what <+> text "variable"
3178 <> plural tkvs <+> pprQuotedList tkvs
3179
3180 | otherwise -- "The type variable 't0' is ambiguous"
3181 = text "The" <+> what <+> text "variable" <> plural tkvs
3182 <+> pprQuotedList tkvs <+> is_or_are tkvs <+> text "ambiguous"
3183
3184 is_or_are [_] = text "is"
3185 is_or_are _ = text "are"
3186
3187 pprSkols :: ReportErrCtxt -> [TcTyVar] -> SDoc
3188 pprSkols ctxt tvs
3189 = vcat (map pp_one (getSkolemInfo (cec_encl ctxt) tvs))
3190 where
3191 pp_one (Implic { ic_info = skol_info }, tvs)
3192 | UnkSkol <- skol_info
3193 = hang (pprQuotedList tvs)
3194 2 (is_or_are tvs "an" "unknown")
3195 | otherwise
3196 = vcat [ hang (pprQuotedList tvs)
3197 2 (is_or_are tvs "a" "rigid" <+> text "bound by")
3198 , nest 2 (pprSkolInfo skol_info)
3199 , nest 2 (text "at" <+> ppr (foldr1 combineSrcSpans (map getSrcSpan tvs))) ]
3200
3201 is_or_are [_] article adjective = text "is" <+> text article <+> text adjective
3202 <+> text "type variable"
3203 is_or_are _ _ adjective = text "are" <+> text adjective
3204 <+> text "type variables"
3205
3206 getAmbigTkvs :: Ct -> ([Var],[Var])
3207 getAmbigTkvs ct
3208 = partition (`elemVarSet` dep_tkv_set) ambig_tkvs
3209 where
3210 tkvs = tyCoVarsOfCtList ct
3211 ambig_tkvs = filter isAmbiguousTyVar tkvs
3212 dep_tkv_set = tyCoVarsOfTypes (map tyVarKind tkvs)
3213
3214 getSkolemInfo :: [Implication] -> [TcTyVar]
3215 -> [(Implication, [TcTyVar])]
3216 -- Get the skolem info for some type variables
3217 -- from the implication constraints that bind them
3218 --
3219 -- In the returned (implic, tvs) pairs, the 'tvs' part is non-empty
3220 getSkolemInfo _ []
3221 = []
3222
3223 getSkolemInfo [] tvs
3224 = pprPanic "No skolem info:" (ppr tvs)
3225
3226 getSkolemInfo (implic:implics) tvs
3227 | null tvs_here = getSkolemInfo implics tvs
3228 | otherwise = (implic, tvs_here) : getSkolemInfo implics tvs_other
3229 where
3230 (tvs_here, tvs_other) = partition (`elem` ic_skols implic) tvs
3231
3232 -----------------------
3233 -- relevantBindings looks at the value environment and finds values whose
3234 -- types mention any of the offending type variables. It has to be
3235 -- careful to zonk the Id's type first, so it has to be in the monad.
3236 -- We must be careful to pass it a zonked type variable, too.
3237 --
3238 -- We always remove closed top-level bindings, though,
3239 -- since they are never relevant (cf Trac #8233)
3240
3241 relevantBindings :: Bool -- True <=> filter by tyvar; False <=> no filtering
3242 -- See Trac #8191
3243 -> ReportErrCtxt -> Ct
3244 -> TcM (ReportErrCtxt, SDoc, Ct)
3245 -- Also returns the zonked and tidied CtOrigin of the constraint
3246 relevantBindings want_filtering ctxt ct
3247 = do { dflags <- getDynFlags
3248 ; (env1, tidy_orig) <- zonkTidyOrigin (cec_tidy ctxt) (ctLocOrigin loc)
3249 ; let ct_tvs = tyCoVarsOfCt ct `unionVarSet` extra_tvs
3250
3251 -- For *kind* errors, report the relevant bindings of the
3252 -- enclosing *type* equality, because that's more useful for the programmer
3253 extra_tvs = case tidy_orig of
3254 KindEqOrigin t1 m_t2 _ _ -> tyCoVarsOfTypes $
3255 t1 : maybeToList m_t2
3256 _ -> emptyVarSet
3257 ; traceTc "relevantBindings" $
3258 vcat [ ppr ct
3259 , pprCtOrigin (ctLocOrigin loc)
3260 , ppr ct_tvs
3261 , pprWithCommas id [ ppr id <+> dcolon <+> ppr (idType id)
3262 | TcIdBndr id _ <- tcl_bndrs lcl_env ]
3263 , pprWithCommas id
3264 [ ppr id | TcIdBndr_ExpType id _ _ <- tcl_bndrs lcl_env ] ]
3265
3266 ; (tidy_env', docs, discards)
3267 <- go dflags env1 ct_tvs (maxRelevantBinds dflags)
3268 emptyVarSet [] False
3269 (remove_shadowing $ tcl_bndrs lcl_env)
3270 -- tcl_bndrs has the innermost bindings first,
3271 -- which are probably the most relevant ones
3272
3273 ; let doc = ppUnless (null docs) $
3274 hang (text "Relevant bindings include")
3275 2 (vcat docs $$ ppWhen discards discardMsg)
3276
3277 -- Put a zonked, tidied CtOrigin into the Ct
3278 loc' = setCtLocOrigin loc tidy_orig
3279 ct' = setCtLoc ct loc'
3280 ctxt' = ctxt { cec_tidy = tidy_env' }
3281
3282 ; return (ctxt', doc, ct') }
3283 where
3284 ev = ctEvidence ct
3285 loc = ctEvLoc ev
3286 lcl_env = ctLocEnv loc
3287
3288 run_out :: Maybe Int -> Bool
3289 run_out Nothing = False
3290 run_out (Just n) = n <= 0
3291
3292 dec_max :: Maybe Int -> Maybe Int
3293 dec_max = fmap (\n -> n - 1)
3294
3295 ---- fixes #12177
3296 ---- builds up a list of bindings whose OccName has not been seen before
3297 remove_shadowing :: [TcBinder] -> [TcBinder]
3298 remove_shadowing bindings = reverse $ fst $ foldl
3299 (\(bindingAcc, seenNames) binding ->
3300 if (occName binding) `elemOccSet` seenNames -- if we've seen it
3301 then (bindingAcc, seenNames) -- skip it
3302 else (binding:bindingAcc, extendOccSet seenNames (occName binding)))
3303 ([], emptyOccSet) bindings
3304
3305 go :: DynFlags -> TidyEnv -> TcTyVarSet -> Maybe Int -> TcTyVarSet -> [SDoc]
3306 -> Bool -- True <=> some filtered out due to lack of fuel
3307 -> [TcBinder]
3308 -> TcM (TidyEnv, [SDoc], Bool) -- The bool says if we filtered any out
3309 -- because of lack of fuel
3310 go _ tidy_env _ _ _ docs discards []
3311 = return (tidy_env, reverse docs, discards)
3312 go dflags tidy_env ct_tvs n_left tvs_seen docs discards (tc_bndr : tc_bndrs)
3313 = case tc_bndr of
3314 TcTvBndr {} -> discard_it
3315 TcIdBndr id top_lvl -> go2 (idName id) (idType id) top_lvl
3316 TcIdBndr_ExpType name et top_lvl ->
3317 do { mb_ty <- readExpType_maybe et
3318 -- et really should be filled in by now. But there's a chance
3319 -- it hasn't, if, say, we're reporting a kind error en route to
3320 -- checking a term. See test indexed-types/should_fail/T8129
3321 -- Or we are reporting errors from the ambiguity check on
3322 -- a local type signature
3323 ; case mb_ty of
3324 Just ty -> go2 name ty top_lvl
3325 Nothing -> discard_it -- No info; discard
3326 }
3327 where
3328 discard_it = go dflags tidy_env ct_tvs n_left tvs_seen docs
3329 discards tc_bndrs
3330 go2 id_name id_type top_lvl
3331 = do { (tidy_env', tidy_ty) <- zonkTidyTcType tidy_env id_type
3332 ; traceTc "relevantBindings 1" (ppr id_name <+> dcolon <+> ppr tidy_ty)
3333 ; let id_tvs = tyCoVarsOfType tidy_ty
3334 doc = sep [ pprPrefixOcc id_name <+> dcolon <+> ppr tidy_ty
3335 , nest 2 (parens (text "bound at"
3336 <+> ppr (getSrcLoc id_name)))]
3337 new_seen = tvs_seen `unionVarSet` id_tvs
3338
3339 ; if (want_filtering && not (hasPprDebug dflags)
3340 && id_tvs `disjointVarSet` ct_tvs)
3341 -- We want to filter out this binding anyway
3342 -- so discard it silently
3343 then discard_it
3344
3345 else if isTopLevel top_lvl && not (isNothing n_left)
3346 -- It's a top-level binding and we have not specified
3347 -- -fno-max-relevant-bindings, so discard it silently
3348 then discard_it
3349
3350 else if run_out n_left && id_tvs `subVarSet` tvs_seen
3351 -- We've run out of n_left fuel and this binding only
3352 -- mentions already-seen type variables, so discard it
3353 then go dflags tidy_env ct_tvs n_left tvs_seen docs
3354 True -- Record that we have now discarded something
3355 tc_bndrs
3356
3357 -- Keep this binding, decrement fuel
3358 else go dflags tidy_env' ct_tvs (dec_max n_left) new_seen
3359 (doc:docs) discards tc_bndrs }
3360
3361 discardMsg :: SDoc
3362 discardMsg = text "(Some bindings suppressed;" <+>
3363 text "use -fmax-relevant-binds=N or -fno-max-relevant-binds)"
3364
3365 subsDiscardMsg :: SDoc
3366 subsDiscardMsg =
3367 text "(Some substitutions suppressed;" <+>
3368 text "use -fmax-valid-substitutions=N or -fno-max-valid-substitutions)"
3369
3370 refSubsDiscardMsg :: SDoc
3371 refSubsDiscardMsg =
3372 text "(Some refinement substitutions suppressed;" <+>
3373 text "use -fmax-refinement-substitutions=N" <+>
3374 text "or -fno-max-refinement-substitutions)"
3375
3376 -----------------------
3377 warnDefaulting :: [Ct] -> Type -> TcM ()
3378 warnDefaulting wanteds default_ty
3379 = do { warn_default <- woptM Opt_WarnTypeDefaults
3380 ; env0 <- tcInitTidyEnv
3381 ; let tidy_env = tidyFreeTyCoVars env0 $
3382 tyCoVarsOfCtsList (listToBag wanteds)
3383 tidy_wanteds = map (tidyCt tidy_env) wanteds
3384 (loc, ppr_wanteds) = pprWithArising tidy_wanteds
3385 warn_msg =
3386 hang (hsep [ text "Defaulting the following"
3387 , text "constraint" <> plural tidy_wanteds
3388 , text "to type"
3389 , quotes (ppr default_ty) ])
3390 2
3391 ppr_wanteds
3392 ; setCtLocM loc $ warnTc (Reason Opt_WarnTypeDefaults) warn_default warn_msg }
3393
3394 {-
3395 Note [Runtime skolems]
3396 ~~~~~~~~~~~~~~~~~~~~~~
3397 We want to give a reasonably helpful error message for ambiguity
3398 arising from *runtime* skolems in the debugger. These
3399 are created by in RtClosureInspect.zonkRTTIType.
3400
3401 ************************************************************************
3402 * *
3403 Error from the canonicaliser
3404 These ones are called *during* constraint simplification
3405 * *
3406 ************************************************************************
3407 -}
3408
3409 solverDepthErrorTcS :: CtLoc -> TcType -> TcM a
3410 solverDepthErrorTcS loc ty
3411 = setCtLocM loc $
3412 do { ty <- zonkTcType ty
3413 ; env0 <- tcInitTidyEnv
3414 ; let tidy_env = tidyFreeTyCoVars env0 (tyCoVarsOfTypeList ty)
3415 tidy_ty = tidyType tidy_env ty
3416 msg
3417 = vcat [ text "Reduction stack overflow; size =" <+> ppr depth
3418 , hang (text "When simplifying the following type:")
3419 2 (ppr tidy_ty)
3420 , note ]
3421 ; failWithTcM (tidy_env, msg) }
3422 where
3423 depth = ctLocDepth loc
3424 note = vcat
3425 [ text "Use -freduction-depth=0 to disable this check"
3426 , text "(any upper bound you could choose might fail unpredictably with"
3427 , text " minor updates to GHC, so disabling the check is recommended if"
3428 , text " you're sure that type checking should terminate)" ]