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