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