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