Implement Partial Type Signatures
[ghc.git] / compiler / typecheck / TcErrors.lhs
1 \begin{code}
2 {-# LANGUAGE CPP, ScopedTypeVariables #-}
3
4 module TcErrors(
5        reportUnsolved, reportAllUnsolved,
6        warnDefaulting,
7
8        solverDepthErrorTcS
9   ) where
10
11 #include "HsVersions.h"
12
13 import TcRnTypes
14 import TcRnMonad
15 import TcMType
16 import TcType
17 import TypeRep
18 import Type
19 import Kind ( isKind )
20 import Unify            ( tcMatchTys )
21 import Module
22 import FamInst          ( FamInstEnvs, tcGetFamInstEnvs, tcLookupDataFamInst )
23 import Inst
24 import InstEnv
25 import TyCon
26 import DataCon
27 import TcEvidence
28 import TysWiredIn       ( coercibleClass )
29 import Name
30 import RdrName          ( lookupGRE_Name )
31 import Id
32 import Var
33 import VarSet
34 import VarEnv
35 import Bag
36 import ErrUtils         ( ErrMsg, makeIntoWarning, pprLocErrMsg, isWarning )
37 import BasicTypes
38 import Util
39 import FastString
40 import Outputable
41 import SrcLoc
42 import DynFlags
43 import StaticFlags      ( opt_PprStyle_Debug )
44 import ListSetOps       ( equivClasses )
45
46 import Control.Monad    ( when )
47 import Data.Maybe
48 import Data.List        ( partition, mapAccumL, zip4, nub, sortBy )
49 \end{code}
50
51 %************************************************************************
52 %*                                                                      *
53 \section{Errors and contexts}
54 %*                                                                      *
55 %************************************************************************
56
57 ToDo: for these error messages, should we note the location as coming
58 from the insts, or just whatever seems to be around in the monad just
59 now?
60
61 Note [Deferring coercion errors to runtime]
62 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
63 While developing, sometimes it is desirable to allow compilation to succeed even
64 if there are type errors in the code. Consider the following case:
65
66   module Main where
67
68   a :: Int
69   a = 'a'
70
71   main = print "b"
72
73 Even though `a` is ill-typed, it is not used in the end, so if all that we're
74 interested in is `main` it is handy to be able to ignore the problems in `a`.
75
76 Since we treat type equalities as evidence, this is relatively simple. Whenever
77 we run into a type mismatch in TcUnify, we normally just emit an error. But it
78 is always safe to defer the mismatch to the main constraint solver. If we do
79 that, `a` will get transformed into
80
81   co :: Int ~ Char
82   co = ...
83
84   a :: Int
85   a = 'a' `cast` co
86
87 The constraint solver would realize that `co` is an insoluble constraint, and
88 emit an error with `reportUnsolved`. But we can also replace the right-hand side
89 of `co` with `error "Deferred type error: Int ~ Char"`. This allows the program
90 to compile, and it will run fine unless we evaluate `a`. This is what
91 `deferErrorsToRuntime` does.
92
93 It does this by keeping track of which errors correspond to which coercion
94 in TcErrors. TcErrors.reportTidyWanteds does not print the errors
95 and does not fail if -fdefer-type-errors is on, so that we can continue
96 compilation. The errors are turned into warnings in `reportUnsolved`.
97
98 \begin{code}
99 reportUnsolved :: WantedConstraints -> TcM (Bag EvBind)
100 reportUnsolved wanted
101   = do { binds_var <- newTcEvBinds
102        ; defer_errors <- goptM Opt_DeferTypeErrors
103        ; defer_holes <- goptM Opt_DeferTypedHoles
104        ; warn_holes <- woptM Opt_WarnTypedHoles
105        ; warn_partial_sigs <- woptM Opt_WarnPartialTypeSignatures
106        ; report_unsolved (Just binds_var) defer_errors defer_holes
107              warn_holes warn_partial_sigs wanted
108        ; getTcEvBinds binds_var }
109
110 reportAllUnsolved :: WantedConstraints -> TcM ()
111 -- Report all unsolved goals, even if -fdefer-type-errors is on
112 -- See Note [Deferring coercion errors to runtime]
113 reportAllUnsolved wanted = do
114     warn_holes <- woptM Opt_WarnTypedHoles
115     warn_partial_sigs <- woptM Opt_WarnPartialTypeSignatures
116     report_unsolved Nothing False False warn_holes warn_partial_sigs wanted
117
118 report_unsolved :: Maybe EvBindsVar  -- cec_binds
119                 -> Bool              -- cec_defer_type_errors
120                 -> Bool              -- cec_defer_holes
121                 -> Bool              -- cec_warn_holes
122                 -> Bool              -- cec_warn_partial_type_signatures
123                 -> WantedConstraints -> TcM ()
124 -- Important precondition:
125 -- WantedConstraints are fully zonked and unflattened, that is,
126 -- zonkWC has already been applied to these constraints.
127 report_unsolved mb_binds_var defer_errors defer_holes warn_holes
128                 warn_partial_sigs wanted
129   | isEmptyWC wanted
130   = return ()
131   | otherwise
132   = do { traceTc "reportUnsolved (before unflattening)" (ppr wanted)
133
134        ; env0 <- tcInitTidyEnv
135
136             -- If we are deferring we are going to need /all/ evidence around,
137             -- including the evidence produced by unflattening (zonkWC)
138        ; let tidy_env = tidyFreeTyVars env0 free_tvs
139              free_tvs = tyVarsOfWC wanted
140              err_ctxt = CEC { cec_encl  = []
141                             , cec_tidy  = tidy_env
142                             , cec_defer_type_errors = defer_errors
143                             , cec_defer_holes = defer_holes
144                             , cec_warn_holes = warn_holes
145                             , cec_warn_partial_type_signatures = warn_partial_sigs
146                             , cec_suppress = False -- See Note [Suppressing error messages]
147                             , cec_binds    = mb_binds_var }
148
149        ; traceTc "reportUnsolved (after unflattening):" $
150          vcat [ pprTvBndrs (varSetElems free_tvs)
151               , ppr wanted ]
152
153        ; reportWanteds err_ctxt wanted }
154
155 --------------------------------------------
156 --      Internal functions
157 --------------------------------------------
158
159 data ReportErrCtxt
160     = CEC { cec_encl :: [Implication]  -- Enclosing implications
161                                        --   (innermost first)
162                                        -- ic_skols and givens are tidied, rest are not
163           , cec_tidy  :: TidyEnv
164           , cec_binds :: Maybe EvBindsVar
165                          -- Nothinng <=> Report all errors, including holes; no bindings
166                          -- Just ev  <=> make some errors (depending on cec_defer)
167                          --              into warnings, and emit evidence bindings
168                          --              into 'ev' for unsolved constraints
169
170           , cec_defer_type_errors :: Bool -- True <=> -fdefer-type-errors
171                                           -- Defer type errors until runtime
172                                           -- Irrelevant if cec_binds = Nothing
173
174           , cec_defer_holes :: Bool     -- True <=> -fdefer-typed-holes
175                                         -- Turn typed holes into runtime errors
176                                         -- Irrelevant if cec_binds = Nothing
177
178           , cec_warn_holes :: Bool  -- True <=> -fwarn-typed-holes
179                                     -- Controls whether typed holes produce warnings
180           , cec_warn_partial_type_signatures :: Bool
181                                     -- True <=> -fwarn-partial-type-signatures
182                                     -- Controls whether holes in partial type
183                                     -- signatures produce warnings
184           , cec_suppress :: Bool    -- True <=> More important errors have occurred,
185                                     --          so create bindings if need be, but
186                                     --          don't issue any more errors/warnings
187                                     -- See Note [Suppressing error messages]
188       }
189 \end{code}
190
191 Note [Suppressing error messages]
192 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
193 The cec_suppress flag says "don't report any errors.  Instead, just create
194 evidence bindings (as usual).  It's used when more important errors have occurred.
195 Specifically (see reportWanteds)
196   * If there are insoluble Givens, then we are in unreachable code and all bets
197     are off.  So don't report any further errors.
198   * If there are any insolubles (eg Int~Bool), here or in a nested implication,
199     then suppress errors from the flat constraints here.  Sometimes the
200     flat-constraint errors are a knock-on effect of the insolubles.
201
202
203 \begin{code}
204 reportImplic :: ReportErrCtxt -> Implication -> TcM ()
205 reportImplic ctxt implic@(Implic { ic_skols = tvs, ic_given = given
206                                  , ic_wanted = wanted, ic_binds = evb
207                                  , ic_insol = ic_insoluble, ic_info = info })
208   | BracketSkol <- info
209   , not ic_insoluble -- For Template Haskell brackets report only
210   = return ()        -- definite errors. The whole thing will be re-checked
211                      -- later when we plug it in, and meanwhile there may
212                      -- certainly be un-satisfied constraints
213
214   | otherwise
215   = reportWanteds ctxt' wanted
216   where
217     (env1, tvs') = mapAccumL tidyTyVarBndr (cec_tidy ctxt) tvs
218     (env2, info') = tidySkolemInfo env1 info
219     implic' = implic { ic_skols = tvs'
220                      , ic_given = map (tidyEvVar env2) given
221                      , ic_info  = info' }
222     ctxt' = ctxt { cec_tidy  = env2
223                  , cec_encl  = implic' : cec_encl ctxt
224                  , cec_binds = case cec_binds ctxt of
225                                  Nothing -> Nothing
226                                  Just {} -> Just evb }
227
228 reportWanteds :: ReportErrCtxt -> WantedConstraints -> TcM ()
229 reportWanteds ctxt wanted@(WC { wc_flat = flats, wc_insol = insols, wc_impl = implics })
230   = do { reportFlats ctxt  (mapBag (tidyCt env) insol_given)
231        ; reportFlats ctxt1 (mapBag (tidyCt env) insol_wanted)
232        ; reportFlats ctxt2 (mapBag (tidyCt env) flats)
233             -- All the Derived ones have been filtered out of flats
234             -- by the constraint solver. This is ok; we don't want
235             -- to report unsolved Derived goals as errors
236             -- See Note [Do not report derived but soluble errors]
237        ; mapBagM_ (reportImplic ctxt1) implics }
238             -- NB ctxt1: don't suppress inner insolubles if there's only a
239             -- wanted insoluble here; but do suppress inner insolubles
240             -- if there's a given insoluble here (= inaccessible code)
241  where
242     (insol_given, insol_wanted) = partitionBag isGivenCt insols
243     env = cec_tidy ctxt
244
245       -- See Note [Suppressing error messages]
246     suppress0 = cec_suppress ctxt
247     suppress1 = suppress0 || not (isEmptyBag insol_given)
248     suppress2 = suppress0 || insolubleWC wanted
249     ctxt1     = ctxt { cec_suppress = suppress1 }
250     ctxt2     = ctxt { cec_suppress = suppress2 }
251
252 reportFlats :: ReportErrCtxt -> Cts -> TcM ()
253 reportFlats ctxt flats    -- Here 'flats' includes insolble goals
254   =  traceTc "reportFlats" (vcat [ ptext (sLit "Flats =") <+> ppr flats
255                                  , ptext (sLit "Suppress =") <+> ppr (cec_suppress ctxt)])
256   >> tryReporters
257       [ -- First deal with things that are utterly wrong
258         -- Like Int ~ Bool (incl nullary TyCons)
259         -- or  Int ~ t a   (AppTy on one side)
260         ("Utterly wrong",  utterly_wrong,   True,  mkGroupReporter mkEqErr)
261       , ("Holes",          is_hole,         False, mkHoleReporter mkHoleError)
262
263         -- Report equalities of form (a~ty).  They are usually
264         -- skolem-equalities, and they cause confusing knock-on
265         -- effects in other errors; see test T4093b.
266       , ("Skolem equalities", skolem_eq,  True,  mkSkolReporter)
267
268         -- Other equalities; also confusing knock on effects
269       , ("Equalities",      is_equality, True,  mkGroupReporter mkEqErr)
270
271       , ("Implicit params", is_ip,       False, mkGroupReporter mkIPErr)
272       , ("Irreds",          is_irred,    False, mkGroupReporter mkIrredErr)
273       , ("Dicts",           is_dict,     False, mkGroupReporter mkDictErr)
274       ]
275       panicReporter ctxt (bagToList flats)
276           -- TuplePreds should have been expanded away by the constraint
277           -- simplifier, so they shouldn't show up at this point
278   where
279     utterly_wrong, skolem_eq, is_hole, is_dict,
280       is_equality, is_ip, is_irred :: Ct -> PredTree -> Bool
281
282     utterly_wrong _ (EqPred ty1 ty2) = isRigid ty1 && isRigid ty2
283     utterly_wrong _ _ = False
284
285     is_hole ct _ = isHoleCt ct
286
287     skolem_eq _ (EqPred ty1 ty2) = isRigidOrSkol ty1 && isRigidOrSkol ty2
288     skolem_eq _ _ = False
289
290     is_equality _ (EqPred {}) = True
291     is_equality _ _           = False
292
293     is_dict _ (ClassPred {}) = True
294     is_dict _ _              = False
295
296     is_ip _ (ClassPred cls _) = isIPClass cls
297     is_ip _ _                 = False
298
299     is_irred _ (IrredPred {}) = True
300     is_irred _ _              = False
301
302
303 ---------------
304 isRigid, isRigidOrSkol :: Type -> Bool
305 isRigid ty
306   | Just (tc,_) <- tcSplitTyConApp_maybe ty = isDecomposableTyCon tc
307   | Just {} <- tcSplitAppTy_maybe ty        = True
308   | isForAllTy ty                           = True
309   | otherwise                               = False
310
311 isRigidOrSkol ty
312   | Just tv <- getTyVar_maybe ty = isSkolemTyVar tv
313   | otherwise                    = isRigid ty
314
315 isTyFun_maybe :: Type -> Maybe TyCon
316 isTyFun_maybe ty = case tcSplitTyConApp_maybe ty of
317                       Just (tc,_) | isTypeFamilyTyCon tc -> Just tc
318                       _ -> Nothing
319
320
321 --------------------------------------------
322 --      Reporters
323 --------------------------------------------
324
325 type Reporter
326   = ReportErrCtxt -> [Ct] -> TcM ()
327 type ReporterSpec
328   = ( String                     -- Name
329     , Ct -> PredTree -> Bool     -- Pick these ones
330     , Bool                       -- True <=> suppress subsequent reporters
331     , Reporter)                  -- The reporter itself
332
333 panicReporter :: Reporter
334 panicReporter _ cts
335   | null cts  = return ()
336   | otherwise =  pprPanic "reportFlats" (ppr cts)
337
338 mkSkolReporter :: Reporter
339 -- Suppress duplicates with the same LHS
340 mkSkolReporter ctxt cts
341   = mapM_ (reportGroup mkEqErr ctxt) (equivClasses cmp_lhs_type cts)
342   where
343     cmp_lhs_type ct1 ct2
344       = case (classifyPredType (ctPred ct1), classifyPredType (ctPred ct2)) of
345            (EqPred ty1 _, EqPred ty2 _) -> ty1 `cmpType` ty2
346            _ -> pprPanic "mkSkolReporter" (ppr ct1 $$ ppr ct2)
347
348 mkHoleReporter :: (ReportErrCtxt -> Ct -> TcM ErrMsg) -> Reporter
349 -- Reports errors one at a time
350 mkHoleReporter mk_err ctxt
351   = mapM_ $ \ct ->
352     do { err <- mk_err ctxt ct
353        ; maybeReportHoleError ctxt err
354        ; maybeAddDeferredHoleBinding ctxt err ct }
355
356 mkGroupReporter :: (ReportErrCtxt -> [Ct] -> TcM ErrMsg)
357                              -- Make error message for a group
358                 -> Reporter  -- Deal with lots of constraints
359 -- Group together errors from same location,
360 -- and report only the first (to avoid a cascade)
361 mkGroupReporter mk_err ctxt cts
362   = mapM_ (reportGroup mk_err ctxt) (equivClasses cmp_loc cts)
363   where
364     cmp_loc ct1 ct2 = ctLocSpan (ctLoc ct1) `compare` ctLocSpan (ctLoc ct2)
365
366 reportGroup :: (ReportErrCtxt -> [Ct] -> TcM ErrMsg) -> ReportErrCtxt
367             -> [Ct] -> TcM ()
368 reportGroup mk_err ctxt cts
369   = do { err <- mk_err ctxt cts
370        ; maybeReportError ctxt err
371        ; mapM_ (maybeAddDeferredBinding ctxt err) cts }
372                -- Add deferred bindings for all
373                -- But see Note [Always warn with -fdefer-type-errors]
374
375 maybeReportHoleError :: ReportErrCtxt -> ErrMsg -> TcM ()
376 maybeReportHoleError ctxt err
377   -- When -XPartialTypeSignatures is on, warnings (instead of errors) are
378   -- generated for holes in partial type signatures. Unless
379   -- -fwarn_partial_type_signatures is not on, in which case the messages are
380   -- discarded.
381   | isWarning err
382   = when (cec_warn_partial_type_signatures ctxt)
383             (reportWarning err)
384   | cec_defer_holes ctxt
385   = when (cec_warn_holes ctxt)
386             (reportWarning (makeIntoWarning err))
387   | otherwise
388   = reportError err
389
390 maybeReportError :: ReportErrCtxt -> ErrMsg -> TcM ()
391 -- Report the error and/or make a deferred binding for it
392 maybeReportError ctxt err
393   -- See Note [Always warn with -fdefer-type-errors]
394   | cec_defer_type_errors ctxt
395   = reportWarning (makeIntoWarning err)
396   | cec_suppress ctxt
397   = return ()
398   | otherwise
399   = reportError err
400
401 addDeferredBinding :: ReportErrCtxt -> ErrMsg -> Ct -> TcM ()
402 -- See Note [Deferring coercion errors to runtime]
403 addDeferredBinding ctxt err ct
404   | CtWanted { ctev_pred = pred, ctev_evar = ev_id } <- ctEvidence ct
405     -- Only add deferred bindings for Wanted constraints
406   , Just ev_binds_var <- cec_binds ctxt  -- We have somewhere to put the bindings
407   = do { dflags <- getDynFlags
408        ; let err_msg = pprLocErrMsg err
409              err_fs  = mkFastString $ showSDoc dflags $
410                        err_msg $$ text "(deferred type error)"
411
412          -- Create the binding
413        ; addTcEvBind ev_binds_var ev_id (EvDelayedError pred err_fs) }
414
415   | otherwise   -- Do not set any evidence for Given/Derived
416   = return ()
417
418 maybeAddDeferredHoleBinding :: ReportErrCtxt -> ErrMsg -> Ct -> TcM ()
419 maybeAddDeferredHoleBinding ctxt err ct
420     | cec_defer_holes ctxt && isTypedHoleCt ct
421     = addDeferredBinding ctxt err ct
422     | otherwise
423     = return ()
424
425 maybeAddDeferredBinding :: ReportErrCtxt -> ErrMsg -> Ct -> TcM ()
426 maybeAddDeferredBinding ctxt err ct
427     | cec_defer_type_errors ctxt
428     = addDeferredBinding ctxt err ct
429     | otherwise
430     = return ()
431
432 tryReporters :: [ReporterSpec] -> Reporter -> Reporter
433 -- Use the first reporter in the list whose predicate says True
434 tryReporters reporters deflt ctxt cts
435   = do { traceTc "tryReporters {" (ppr cts)
436        ; go ctxt reporters cts
437        ; traceTc "tryReporters }" empty }
438   where
439     go ctxt [] cts = deflt ctxt cts
440     go ctxt ((str, pred, suppress_after, reporter) : rs) cts
441       | null yeses  = do { traceTc "tryReporters: no" (text str)
442                          ; go ctxt rs cts }
443       | otherwise   = do { traceTc "tryReporters: yes" (text str <+> ppr yeses)
444                          ; reporter ctxt yeses :: TcM ()
445                          ; let ctxt' = ctxt { cec_suppress = suppress_after || cec_suppress ctxt }
446                          ; go ctxt' rs nos }
447                          -- Carry on with the rest, because we must make
448                          -- deferred bindings for them if we have
449                          -- -fdefer-type-errors
450                          -- But suppress their error messages
451       where
452        (yeses, nos) = partition keep_me cts
453        keep_me ct = pred ct (classifyPredType (ctPred ct))
454
455 -- Add the "arising from..." part to a message about bunch of dicts
456 addArising :: CtOrigin -> SDoc -> SDoc
457 addArising orig msg = hang msg 2 (pprArising orig)
458
459 pprWithArising :: [Ct] -> (CtLoc, SDoc)
460 -- Print something like
461 --    (Eq a) arising from a use of x at y
462 --    (Show a) arising from a use of p at q
463 -- Also return a location for the error message
464 -- Works for Wanted/Derived only
465 pprWithArising []
466   = panic "pprWithArising"
467 pprWithArising (ct:cts)
468   | null cts
469   = (loc, addArising (ctLocOrigin loc)
470                      (pprTheta [ctPred ct]))
471   | otherwise
472   = (loc, vcat (map ppr_one (ct:cts)))
473   where
474     loc = ctLoc ct
475     ppr_one ct' = hang (parens (pprType (ctPred ct')))
476                      2 (pprArisingAt (ctLoc ct'))
477
478 mkErrorMsg :: ReportErrCtxt -> Ct -> SDoc -> TcM ErrMsg
479 mkErrorMsg ctxt ct msg
480   = do { let tcl_env = ctLocEnv (ctLoc ct)
481        ; err_info <- mkErrInfo (cec_tidy ctxt) (tcl_ctxt tcl_env)
482        ; mkLongErrAt (tcl_loc tcl_env) msg err_info }
483
484 type UserGiven = ([EvVar], SkolemInfo, Bool, SrcSpan)
485
486 getUserGivens :: ReportErrCtxt -> [UserGiven]
487 -- One item for each enclosing implication
488 getUserGivens (CEC {cec_encl = ctxt})
489   = reverse $
490     [ (givens, info, no_eqs, tcl_loc env)
491     | Implic { ic_given = givens, ic_env = env
492              , ic_no_eqs = no_eqs, ic_info = info } <- ctxt
493     , not (null givens) ]
494 \end{code}
495
496 Note [Always warn with -fdefer-type-errors]
497 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
498 When -fdefer-type-errors is on we warn about *all* type errors, even
499 if cec_suppress is on.  This can lead to a lot more warnings than you
500 would get errors without -fdefer-type-errors, but if we suppress any of
501 them you might get a runtime error that wasn't warned about at compile
502 time.
503
504 This is an easy design choice to change; just flip the order of the
505 first two equations for maybeReportError
506
507 To be consistent, we should also report multiple warnings from a single
508 location in mkGroupReporter, when -fdefer-type-errors is on.  But that
509 is perhaps a bit *over*-consistent! Again, an easy choice to change.
510
511
512 Note [Do not report derived but soluble errors]
513 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
514 The wc_flats include Derived constraints that have not been solved, but are
515 not insoluble (in that case they'd be in wc_insols).  We do not want to report
516 these as errors:
517
518 * Superclass constraints. If we have an unsolved [W] Ord a, we'll also have
519   an unsolved [D] Eq a, and we do not want to report that; it's just noise.
520
521 * Functional dependencies.  For givens, consider
522       class C a b | a -> b
523       data T a where
524          MkT :: C a d => [d] -> T a
525       f :: C a b => T a -> F Int
526       f (MkT xs) = length xs
527   Then we get a [D] b~d.  But there *is* a legitimate call to
528   f, namely   f (MkT [True]) :: T Bool, in which b=d.  So we should
529   not reject the program.
530
531   For wanteds, something similar
532       data T a where
533         MkT :: C Int b => a -> b -> T a
534       g :: C Int c => c -> ()
535       f :: T a -> ()
536       f (MkT x y) = g x
537   Here we get [G] C Int b, [W] C Int a, hence [D] a~b.
538   But again f (MkT True True) is a legitimate call.
539
540 (We leave the Deriveds in wc_flat until reportErrors, so that we don't lose
541 derived superclasses between iterations of the solver.)
542
543 For functional dependencies, here is a real example,
544 stripped off from libraries/utf8-string/Codec/Binary/UTF8/Generic.hs
545
546   class C a b | a -> b
547   g :: C a b => a -> b -> ()
548   f :: C a b => a -> b -> ()
549   f xa xb =
550       let loop = g xa
551       in loop xb
552
553 We will first try to infer a type for loop, and we will succeed:
554     C a b' => b' -> ()
555 Subsequently, we will type check (loop xb) and all is good. But,
556 recall that we have to solve a final implication constraint:
557     C a b => (C a b' => .... cts from body of loop .... ))
558 And now we have a problem as we will generate an equality b ~ b' and fail to
559 solve it.
560
561
562 %************************************************************************
563 %*                  *
564                 Irreducible predicate errors
565 %*                  *
566 %************************************************************************
567
568 \begin{code}
569 mkIrredErr :: ReportErrCtxt -> [Ct] -> TcM ErrMsg
570 mkIrredErr ctxt cts
571   = do { (ctxt, binds_msg) <- relevantBindings True ctxt ct1
572        ; mkErrorMsg ctxt ct1 (msg $$ binds_msg) }
573   where
574     (ct1:_) = cts
575     orig    = ctLocOrigin (ctLoc ct1)
576     givens  = getUserGivens ctxt
577     msg = couldNotDeduce givens (map ctPred cts, orig)
578
579 ----------------
580 mkHoleError :: ReportErrCtxt -> Ct -> TcM ErrMsg
581 mkHoleError ctxt ct@(CHoleCan { cc_occ = occ })
582   = do { partial_sigs <- xoptM Opt_PartialTypeSignatures
583        ; let tyvars = varSetElems (tyVarsOfCt ct)
584              tyvars_msg = map loc_msg tyvars
585              msg = vcat [ hang (ptext (sLit "Found hole") <+> quotes (ppr occ))
586                              2 (ptext (sLit "with type:") <+> pprType (ctEvPred (ctEvidence ct)))
587                         , ppUnless (null tyvars_msg) (ptext (sLit "Where:") <+> vcat tyvars_msg)
588                         , if in_typesig && not partial_sigs then pts_hint else empty ]
589        ; (ctxt, binds_doc) <- relevantBindings False ctxt ct
590                -- The 'False' means "don't filter the bindings; see Trac #8191
591        ; errMsg <- mkErrorMsg ctxt ct (msg $$ binds_doc)
592        ; if in_typesig && partial_sigs
593            then return $ makeIntoWarning errMsg
594            else return errMsg }
595   where
596     in_typesig = not $ isTypedHoleCt ct
597     pts_hint = ptext (sLit "To use the inferred type, enable PartialTypeSignatures")
598     loc_msg tv
599        = case tcTyVarDetails tv of
600           SkolemTv {} -> quotes (ppr tv) <+> skol_msg
601           MetaTv {}   -> quotes (ppr tv) <+> ptext (sLit "is an ambiguous type variable")
602           det -> pprTcTyVarDetails det
603        where
604           skol_msg = pprSkol (getSkolemInfo (cec_encl ctxt) tv) (getSrcLoc tv)
605
606 mkHoleError _ ct = pprPanic "mkHoleError" (ppr ct)
607
608 ----------------
609 mkIPErr :: ReportErrCtxt -> [Ct] -> TcM ErrMsg
610 mkIPErr ctxt cts
611   = do { (ctxt, bind_msg) <- relevantBindings True ctxt ct1
612        ; mkErrorMsg ctxt ct1 (msg $$ bind_msg) }
613   where
614     (ct1:_) = cts
615     orig    = ctLocOrigin (ctLoc ct1)
616     preds   = map ctPred cts
617     givens  = getUserGivens ctxt
618     msg | null givens
619         = addArising orig $
620           sep [ ptext (sLit "Unbound implicit parameter") <> plural cts
621               , nest 2 (pprTheta preds) ]
622         | otherwise
623         = couldNotDeduce givens (preds, orig)
624 \end{code}
625
626
627 %************************************************************************
628 %*                                                                      *
629                 Equality errors
630 %*                                                                      *
631 %************************************************************************
632
633 Note [Inaccessible code]
634 ~~~~~~~~~~~~~~~~~~~~~~~~
635 Consider
636    data T a where
637      T1 :: T a
638      T2 :: T Bool
639
640    f :: (a ~ Int) => T a -> Int
641    f T1 = 3
642    f T2 = 4   -- Unreachable code
643
644 Here the second equation is unreachable. The original constraint
645 (a~Int) from the signature gets rewritten by the pattern-match to
646 (Bool~Int), so the danger is that we report the error as coming from
647 the *signature* (Trac #7293).  So, for Given errors we replace the
648 env (and hence src-loc) on its CtLoc with that from the immediately
649 enclosing implication.
650
651 \begin{code}
652 mkEqErr :: ReportErrCtxt -> [Ct] -> TcM ErrMsg
653 -- Don't have multiple equality errors from the same location
654 -- E.g.   (Int,Bool) ~ (Bool,Int)   one error will do!
655 mkEqErr ctxt (ct:_) = mkEqErr1 ctxt ct
656 mkEqErr _ [] = panic "mkEqErr"
657
658 mkEqErr1 :: ReportErrCtxt -> Ct -> TcM ErrMsg
659 -- Wanted constraints only!
660 mkEqErr1 ctxt ct
661   | isGiven ev
662   = do { (ctxt, binds_msg) <- relevantBindings True ctxt ct
663        ; let (given_loc, given_msg) = mk_given (cec_encl ctxt)
664        ; dflags <- getDynFlags
665        ; mkEqErr_help dflags ctxt (given_msg $$ binds_msg)
666                       (ct { cc_ev = ev {ctev_loc = given_loc}}) -- Note [Inaccessible code]
667                       Nothing ty1 ty2 }
668
669   | otherwise   -- Wanted or derived
670   = do { (ctxt, binds_msg) <- relevantBindings True ctxt ct
671        ; (env1, tidy_orig) <- zonkTidyOrigin (cec_tidy ctxt) (ctLocOrigin loc)
672        ; let (is_oriented, wanted_msg) = mk_wanted_extra tidy_orig
673        ; dflags <- getDynFlags
674        ; traceTc "mkEqErr1" (ppr ct $$ pprCtOrigin (ctLocOrigin loc) $$ pprCtOrigin tidy_orig) 
675        ; mkEqErr_help dflags (ctxt {cec_tidy = env1})
676                       (wanted_msg $$ binds_msg)
677                       ct is_oriented ty1 ty2 }
678   where
679     ev         = ctEvidence ct
680     loc        = ctEvLoc ev
681     (ty1, ty2) = getEqPredTys (ctEvPred ev)
682
683     mk_given :: [Implication] -> (CtLoc, SDoc)
684     -- For given constraints we overwrite the env (and hence src-loc)
685     -- with one from the implication.  See Note [Inaccessible code]
686     mk_given []           = (loc, empty)
687     mk_given (implic : _) = (setCtLocEnv loc (ic_env implic)
688                             , hang (ptext (sLit "Inaccessible code in"))
689                                  2 (ppr (ic_info implic)))
690
691        -- If the types in the error message are the same as the types
692        -- we are unifying, don't add the extra expected/actual message
693     mk_wanted_extra orig@(TypeEqOrigin {})
694       = mkExpectedActualMsg ty1 ty2 orig
695
696     mk_wanted_extra (KindEqOrigin cty1 cty2 sub_o)
697       = (Nothing, msg1 $$ msg2)
698       where
699         msg1 = hang (ptext (sLit "When matching types"))
700                   2 (vcat [ ppr cty1 <+> dcolon <+> ppr (typeKind cty1)
701                           , ppr cty2 <+> dcolon <+> ppr (typeKind cty2) ])
702         msg2 = case sub_o of
703                  TypeEqOrigin {} -> snd (mkExpectedActualMsg cty1 cty2 sub_o)
704                  _ -> empty
705
706     mk_wanted_extra orig@(FunDepOrigin1 {}) = (Nothing, pprArising orig)
707     mk_wanted_extra orig@(FunDepOrigin2 {}) = (Nothing, pprArising orig)
708     mk_wanted_extra _                       = (Nothing, empty)
709
710 mkEqErr_help :: DynFlags -> ReportErrCtxt -> SDoc
711              -> Ct
712              -> Maybe SwapFlag   -- Nothing <=> not sure
713              -> TcType -> TcType -> TcM ErrMsg
714 mkEqErr_help dflags ctxt extra ct oriented ty1 ty2
715   | Just tv1 <- tcGetTyVar_maybe ty1 = mkTyVarEqErr dflags ctxt extra ct oriented tv1 ty2
716   | Just tv2 <- tcGetTyVar_maybe ty2 = mkTyVarEqErr dflags ctxt extra ct swapped  tv2 ty1
717   | otherwise                        = reportEqErr  ctxt extra ct oriented ty1 ty2
718   where
719     swapped = fmap flipSwap oriented
720
721 reportEqErr :: ReportErrCtxt -> SDoc
722             -> Ct
723             -> Maybe SwapFlag   -- Nothing <=> not sure
724             -> TcType -> TcType -> TcM ErrMsg
725 reportEqErr ctxt extra1 ct oriented ty1 ty2
726   = do { let extra2 = mkEqInfoMsg ct ty1 ty2
727        ; mkErrorMsg ctxt ct (vcat [ misMatchOrCND ctxt ct oriented ty1 ty2
728                                    , extra2, extra1]) }
729
730 mkTyVarEqErr :: DynFlags -> ReportErrCtxt -> SDoc -> Ct
731              -> Maybe SwapFlag -> TcTyVar -> TcType -> TcM ErrMsg
732 -- tv1 and ty2 are already tidied
733 mkTyVarEqErr dflags ctxt extra ct oriented tv1 ty2
734   | isUserSkolem ctxt tv1   -- ty2 won't be a meta-tyvar, or else the thing would
735                             -- be oriented the other way round;
736                             -- see TcCanonical.canEqTyVarTyVar
737   || isSigTyVar tv1 && not (isTyVarTy ty2)
738   = mkErrorMsg ctxt ct (vcat [ misMatchOrCND ctxt ct oriented ty1 ty2
739                              , extraTyVarInfo ctxt tv1 ty2
740                              , extra ])
741
742   -- So tv is a meta tyvar (or started that way before we
743   -- generalised it).  So presumably it is an *untouchable*
744   -- meta tyvar or a SigTv, else it'd have been unified
745   | not (k2 `tcIsSubKind` k1)            -- Kind error
746   = mkErrorMsg ctxt ct $ (kindErrorMsg (mkTyVarTy tv1) ty2 $$ extra)
747
748   | OC_Occurs <- occ_check_expand
749   = do { let occCheckMsg = hang (text "Occurs check: cannot construct the infinite type:")
750                               2 (sep [ppr ty1, char '~', ppr ty2])
751              extra2 = mkEqInfoMsg ct ty1 ty2
752        ; mkErrorMsg ctxt ct (occCheckMsg $$ extra2 $$ extra) }
753
754   | OC_Forall <- occ_check_expand
755   = do { let msg = vcat [ ptext (sLit "Cannot instantiate unification variable")
756                           <+> quotes (ppr tv1)
757                         , hang (ptext (sLit "with a type involving foralls:")) 2 (ppr ty2)
758                         , nest 2 (ptext (sLit "Perhaps you want ImpredicativeTypes")) ]
759        ; mkErrorMsg ctxt ct msg }
760
761   -- If the immediately-enclosing implication has 'tv' a skolem, and
762   -- we know by now its an InferSkol kind of skolem, then presumably
763   -- it started life as a SigTv, else it'd have been unified, given
764   -- that there's no occurs-check or forall problem
765   | (implic:_) <- cec_encl ctxt
766   , Implic { ic_skols = skols } <- implic
767   , tv1 `elem` skols
768   = mkErrorMsg ctxt ct (vcat [ misMatchMsg oriented ty1 ty2
769                              , extraTyVarInfo ctxt tv1 ty2
770                              , extra ])
771
772   -- Check for skolem escape
773   | (implic:_) <- cec_encl ctxt   -- Get the innermost context
774   , Implic { ic_env = env, ic_skols = skols, ic_info = skol_info } <- implic
775   , let esc_skols = filter (`elemVarSet` (tyVarsOfType ty2)) skols
776   , not (null esc_skols)
777   = do { let msg = misMatchMsg oriented ty1 ty2
778              esc_doc = sep [ ptext (sLit "because type variable") <> plural esc_skols
779                              <+> pprQuotedList esc_skols
780                            , ptext (sLit "would escape") <+>
781                              if isSingleton esc_skols then ptext (sLit "its scope")
782                                                       else ptext (sLit "their scope") ]
783              tv_extra = vcat [ nest 2 $ esc_doc
784                              , sep [ (if isSingleton esc_skols
785                                       then ptext (sLit "This (rigid, skolem) type variable is")
786                                       else ptext (sLit "These (rigid, skolem) type variables are"))
787                                <+> ptext (sLit "bound by")
788                              , nest 2 $ ppr skol_info
789                              , nest 2 $ ptext (sLit "at") <+> ppr (tcl_loc env) ] ]
790        ; mkErrorMsg ctxt ct (msg $$ tv_extra $$ extra) }
791
792   -- Nastiest case: attempt to unify an untouchable variable
793   | (implic:_) <- cec_encl ctxt   -- Get the innermost context
794   , Implic { ic_env = env, ic_given = given, ic_info = skol_info } <- implic
795   = do { let msg = misMatchMsg oriented ty1 ty2
796              untch_extra
797                 = nest 2 $
798                   sep [ quotes (ppr tv1) <+> ptext (sLit "is untouchable")
799                       , nest 2 $ ptext (sLit "inside the constraints") <+> pprEvVarTheta given
800                       , nest 2 $ ptext (sLit "bound by") <+> ppr skol_info
801                       , nest 2 $ ptext (sLit "at") <+> ppr (tcl_loc env) ]
802              tv_extra = extraTyVarInfo ctxt tv1 ty2
803              add_sig  = suggestAddSig ctxt ty1 ty2
804        ; mkErrorMsg ctxt ct (vcat [msg, untch_extra, tv_extra, add_sig, extra]) }
805
806   | otherwise
807   = reportEqErr ctxt extra ct oriented (mkTyVarTy tv1) ty2
808         -- This *can* happen (Trac #6123, and test T2627b)
809         -- Consider an ambiguous top-level constraint (a ~ F a)
810         -- Not an occurs check, because F is a type function.
811   where
812     occ_check_expand = occurCheckExpand dflags tv1 ty2
813     k1  = tyVarKind tv1
814     k2  = typeKind ty2
815     ty1 = mkTyVarTy tv1
816
817 mkEqInfoMsg :: Ct -> TcType -> TcType -> SDoc
818 -- Report (a) ambiguity if either side is a type function application
819 --            e.g. F a0 ~ Int
820 --        (b) warning about injectivity if both sides are the same
821 --            type function application   F a ~ F b
822 --            See Note [Non-injective type functions]
823 mkEqInfoMsg ct ty1 ty2
824   = tyfun_msg $$ ambig_msg
825   where
826     mb_fun1 = isTyFun_maybe ty1
827     mb_fun2 = isTyFun_maybe ty2
828
829     ambig_msg | isJust mb_fun1 || isJust mb_fun2
830               = snd (mkAmbigMsg ct)
831               | otherwise = empty
832
833     tyfun_msg | Just tc1 <- mb_fun1
834               , Just tc2 <- mb_fun2
835               , tc1 == tc2
836               = ptext (sLit "NB:") <+> quotes (ppr tc1)
837                 <+> ptext (sLit "is a type function, and may not be injective")
838               | otherwise = empty
839
840 isUserSkolem :: ReportErrCtxt -> TcTyVar -> Bool
841 -- See Note [Reporting occurs-check errors]
842 isUserSkolem ctxt tv
843   = isSkolemTyVar tv && any is_user_skol_tv (cec_encl ctxt)
844   where
845     is_user_skol_tv (Implic { ic_skols = sks, ic_info = skol_info })
846       = tv `elem` sks && is_user_skol_info skol_info
847
848     is_user_skol_info (InferSkol {}) = False
849     is_user_skol_info _ = True
850
851 misMatchOrCND :: ReportErrCtxt -> Ct -> Maybe SwapFlag -> TcType -> TcType -> SDoc
852 -- If oriented then ty1 is actual, ty2 is expected
853 misMatchOrCND ctxt ct oriented ty1 ty2
854   | null givens ||
855     (isRigid ty1 && isRigid ty2) ||
856     isGivenCt ct
857        -- If the equality is unconditionally insoluble
858        -- or there is no context, don't report the context
859   = misMatchMsg oriented ty1 ty2
860   | otherwise
861   = couldNotDeduce givens ([mkTcEqPred ty1 ty2], orig)
862   where
863     givens = [ given | given@(_, _, no_eqs, _) <- getUserGivens ctxt, not no_eqs]
864              -- Keep only UserGivens that have some equalities
865     orig   = TypeEqOrigin { uo_actual = ty1, uo_expected = ty2 }
866
867 couldNotDeduce :: [UserGiven] -> (ThetaType, CtOrigin) -> SDoc
868 couldNotDeduce givens (wanteds, orig)
869   = vcat [ addArising orig (ptext (sLit "Could not deduce") <+> pprTheta wanteds)
870          , vcat (pp_givens givens)]
871
872 pp_givens :: [UserGiven] -> [SDoc]
873 pp_givens givens
874    = case givens of
875          []     -> []
876          (g:gs) ->      ppr_given (ptext (sLit "from the context")) g
877                  : map (ppr_given (ptext (sLit "or from"))) gs
878     where
879        ppr_given herald (gs, skol_info, _, loc)
880            = hang (herald <+> pprEvVarTheta gs)
881                 2 (sep [ ptext (sLit "bound by") <+> ppr skol_info
882                        , ptext (sLit "at") <+> ppr loc])
883
884 extraTyVarInfo :: ReportErrCtxt -> TcTyVar -> TcType -> SDoc
885 -- Add on extra info about skolem constants
886 -- NB: The types themselves are already tidied
887 extraTyVarInfo ctxt tv1 ty2
888   = nest 2 (tv_extra tv1 $$ ty_extra ty2)
889   where
890     implics = cec_encl ctxt
891     ty_extra ty = case tcGetTyVar_maybe ty of
892                     Just tv -> tv_extra tv
893                     Nothing -> empty
894
895     tv_extra tv | isTcTyVar tv, isSkolemTyVar tv
896                 , let pp_tv = quotes (ppr tv)
897                 = case tcTyVarDetails tv of
898                     SkolemTv {}   -> pp_tv <+> pprSkol (getSkolemInfo implics tv) (getSrcLoc tv)
899                     FlatSkol {}   -> pp_tv <+> ptext (sLit "is a flattening type variable")
900                     RuntimeUnk {} -> pp_tv <+> ptext (sLit "is an interactive-debugger skolem")
901                     MetaTv {}     -> empty
902
903                 | otherwise             -- Normal case
904                 = empty
905
906 suggestAddSig :: ReportErrCtxt -> TcType -> TcType -> SDoc
907 -- See Note [Suggest adding a type signature]
908 suggestAddSig ctxt ty1 ty2
909   | null inferred_bndrs
910   = empty
911   | [bndr] <- inferred_bndrs
912   = ptext (sLit "Possible fix: add a type signature for") <+> quotes (ppr bndr)
913   | otherwise
914   = ptext (sLit "Possible fix: add type signatures for some or all of") <+> (ppr inferred_bndrs)
915   where
916     inferred_bndrs = nub (get_inf ty1 ++ get_inf ty2)
917     get_inf ty | Just tv <- tcGetTyVar_maybe ty
918                , isTcTyVar tv, isSkolemTyVar tv
919                , InferSkol prs <- getSkolemInfo (cec_encl ctxt) tv
920                = map fst prs
921                | otherwise
922                = []
923
924 kindErrorMsg :: TcType -> TcType -> SDoc   -- Types are already tidy
925 kindErrorMsg ty1 ty2
926   = vcat [ ptext (sLit "Kind incompatibility when matching types:")
927          , nest 2 (vcat [ ppr ty1 <+> dcolon <+> ppr k1
928                         , ppr ty2 <+> dcolon <+> ppr k2 ]) ]
929   where
930     k1 = typeKind ty1
931     k2 = typeKind ty2
932
933 --------------------
934 misMatchMsg :: Maybe SwapFlag -> TcType -> TcType -> SDoc          -- Types are already tidy
935 -- If oriented then ty1 is actual, ty2 is expected
936 misMatchMsg oriented ty1 ty2
937   | Just IsSwapped <- oriented
938   = misMatchMsg (Just NotSwapped) ty2 ty1
939   | Just NotSwapped <- oriented
940   = sep [ ptext (sLit "Couldn't match expected") <+> what <+> quotes (ppr ty2)
941         , nest 12 $   ptext (sLit "with actual") <+> what <+> quotes (ppr ty1)
942         , sameOccExtra ty2 ty1 ]
943   | otherwise
944   = sep [ ptext (sLit "Couldn't match") <+> what <+> quotes (ppr ty1)
945         , nest 14 $ ptext (sLit "with") <+> quotes (ppr ty2)
946         , sameOccExtra ty1 ty2 ]
947   where
948     what | isKind ty1 = ptext (sLit "kind")
949          | otherwise  = ptext (sLit "type")
950
951 mkExpectedActualMsg :: Type -> Type -> CtOrigin -> (Maybe SwapFlag, SDoc)
952 -- NotSwapped means (actual, expected), IsSwapped is the reverse
953 mkExpectedActualMsg ty1 ty2 (TypeEqOrigin { uo_actual = act, uo_expected = exp })
954   | act `pickyEqType` ty1, exp `pickyEqType` ty2 = (Just NotSwapped,  empty)
955   | exp `pickyEqType` ty1, act `pickyEqType` ty2 = (Just IsSwapped, empty)
956   | otherwise                                    = (Nothing, msg)
957   where
958     msg = vcat [ text "Expected type:" <+> ppr exp
959                , text "  Actual type:" <+> ppr act ]
960
961 mkExpectedActualMsg _ _ _ = panic "mkExprectedAcutalMsg"
962
963 sameOccExtra :: TcType -> TcType -> SDoc
964 -- See Note [Disambiguating (X ~ X) errors]
965 sameOccExtra ty1 ty2
966   | Just (tc1, _) <- tcSplitTyConApp_maybe ty1
967   , Just (tc2, _) <- tcSplitTyConApp_maybe ty2
968   , let n1 = tyConName tc1
969         n2 = tyConName tc2
970         same_occ = nameOccName n1                  == nameOccName n2
971         same_pkg = modulePackageKey (nameModule n1) == modulePackageKey (nameModule n2)
972   , n1 /= n2   -- Different Names
973   , same_occ   -- but same OccName
974   = ptext (sLit "NB:") <+> (ppr_from same_pkg n1 $$ ppr_from same_pkg n2)
975   | otherwise
976   = empty
977   where
978     ppr_from same_pkg nm
979       | isGoodSrcSpan loc
980       = hang (quotes (ppr nm) <+> ptext (sLit "is defined at"))
981            2 (ppr loc)
982       | otherwise  -- Imported things have an UnhelpfulSrcSpan
983       = hang (quotes (ppr nm))
984            2 (sep [ ptext (sLit "is defined in") <+> quotes (ppr (moduleName mod))
985                   , ppUnless (same_pkg || pkg == mainPackageKey) $
986                     nest 4 $ ptext (sLit "in package") <+> quotes (ppr pkg) ])
987        where
988          pkg = modulePackageKey mod
989          mod = nameModule nm
990          loc = nameSrcSpan nm
991 \end{code}
992
993 Note [Suggest adding a type signature]
994 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
995 The OutsideIn algorithm rejects GADT programs that don't have a principal
996 type, and indeed some that do.  Example:
997    data T a where
998      MkT :: Int -> T Int
999
1000    f (MkT n) = n
1001
1002 Does this have type f :: T a -> a, or f :: T a -> Int?
1003 The error that shows up tends to be an attempt to unify an
1004 untouchable type variable.  So suggestAddSig sees if the offending
1005 type variable is bound by an *inferred* signature, and suggests
1006 adding a declared signature instead.
1007
1008 This initially came up in Trac #8968, concerning pattern synonyms.
1009
1010 Note [Disambiguating (X ~ X) errors]
1011 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1012 See Trac #8278
1013
1014 Note [Reporting occurs-check errors]
1015 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1016 Given (a ~ [a]), if 'a' is a rigid type variable bound by a user-supplied
1017 type signature, then the best thing is to report that we can't unify
1018 a with [a], because a is a skolem variable.  That avoids the confusing
1019 "occur-check" error message.
1020
1021 But nowadays when inferring the type of a function with no type signature,
1022 even if there are errors inside, we still generalise its signature and
1023 carry on. For example
1024    f x = x:x
1025 Here we will infer somethiing like
1026    f :: forall a. a -> [a]
1027 with a suspended error of (a ~ [a]).  So 'a' is now a skolem, but not
1028 one bound by the programmer!  Here we really should report an occurs check.
1029
1030 So isUserSkolem distinguishes the two.
1031
1032 Note [Non-injective type functions]
1033 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1034 It's very confusing to get a message like
1035      Couldn't match expected type `Depend s'
1036             against inferred type `Depend s1'
1037 so mkTyFunInfoMsg adds:
1038        NB: `Depend' is type function, and hence may not be injective
1039
1040 Warn of loopy local equalities that were dropped.
1041
1042
1043 %************************************************************************
1044 %*                                                                      *
1045                  Type-class errors
1046 %*                                                                      *
1047 %************************************************************************
1048
1049 \begin{code}
1050 mkDictErr :: ReportErrCtxt -> [Ct] -> TcM ErrMsg
1051 mkDictErr ctxt cts
1052   = ASSERT( not (null cts) )
1053     do { inst_envs <- tcGetInstEnvs
1054        ; fam_envs  <- tcGetFamInstEnvs
1055        ; let (ct1:_) = cts  -- ct1 just for its location
1056              min_cts = elim_superclasses cts
1057        ; lookups   <- mapM (lookup_cls_inst inst_envs) min_cts
1058        ; let (no_inst_cts, overlap_cts) = partition is_no_inst lookups
1059
1060        -- Report definite no-instance errors,
1061        -- or (iff there are none) overlap errors
1062        -- But we report only one of them (hence 'head') because they all
1063        -- have the same source-location origin, to try avoid a cascade
1064        -- of error from one location
1065        ; (ctxt, err) <- mk_dict_err fam_envs ctxt (head (no_inst_cts ++ overlap_cts))
1066        ; mkErrorMsg ctxt ct1 err }
1067   where
1068     no_givens = null (getUserGivens ctxt)
1069
1070     is_no_inst (ct, (matches, unifiers, _))
1071       =  no_givens
1072       && null matches
1073       && (null unifiers || all (not . isAmbiguousTyVar) (varSetElems (tyVarsOfCt ct)))
1074
1075     lookup_cls_inst inst_envs ct
1076       = do { tys_flat <- mapM quickFlattenTy tys
1077                 -- Note [Flattening in error message generation]
1078            ; return (ct, lookupInstEnv inst_envs clas tys_flat) }
1079       where
1080         (clas, tys) = getClassPredTys (ctPred ct)
1081
1082
1083     -- When simplifying [W] Ord (Set a), we need
1084     --    [W] Eq a, [W] Ord a
1085     -- but we really only want to report the latter
1086     elim_superclasses cts
1087       = filter (\ct -> any (eqPred (ctPred ct)) min_preds) cts
1088       where
1089         min_preds = mkMinimalBySCs (map ctPred cts)
1090
1091 mk_dict_err :: FamInstEnvs -> ReportErrCtxt -> (Ct, ClsInstLookupResult)
1092             -> TcM (ReportErrCtxt, SDoc)
1093 -- Report an overlap error if this class constraint results
1094 -- from an overlap (returning Left clas), otherwise return (Right pred)
1095 mk_dict_err fam_envs ctxt (ct, (matches, unifiers, safe_haskell))
1096   | null matches  -- No matches but perhaps several unifiers
1097   = do { let (is_ambig, ambig_msg) = mkAmbigMsg ct
1098        ; (ctxt, binds_msg) <- relevantBindings True ctxt ct
1099        ; traceTc "mk_dict_err" (ppr ct $$ ppr is_ambig $$ ambig_msg)
1100        ; rdr_env <- getGlobalRdrEnv
1101        ; return (ctxt, cannot_resolve_msg rdr_env is_ambig binds_msg ambig_msg) }
1102
1103   | not safe_haskell   -- Some matches => overlap errors
1104   = return (ctxt, overlap_msg)
1105
1106   | otherwise
1107   = return (ctxt, safe_haskell_msg)
1108   where
1109     orig        = ctLocOrigin (ctLoc ct)
1110     pred        = ctPred ct
1111     (clas, tys) = getClassPredTys pred
1112     ispecs      = [ispec | (ispec, _) <- matches]
1113     givens      = getUserGivens ctxt
1114     all_tyvars  = all isTyVarTy tys
1115
1116     cannot_resolve_msg rdr_env has_ambig_tvs binds_msg ambig_msg
1117       = vcat [ addArising orig (no_inst_msg $$ coercible_explanation rdr_env)
1118              , vcat (pp_givens givens)
1119              , ppWhen (has_ambig_tvs && not (null unifiers && null givens))
1120                (vcat [ ambig_msg, binds_msg, potential_msg ])
1121              , show_fixes (add_to_ctxt_fixes has_ambig_tvs ++ drv_fixes) ]
1122
1123     potential_msg
1124       = ppWhen (not (null unifiers) && want_potential orig) $
1125         hang (if isSingleton unifiers
1126               then ptext (sLit "Note: there is a potential instance available:")
1127               else ptext (sLit "Note: there are several potential instances:"))
1128            2 (ppr_insts (sortBy fuzzyClsInstCmp unifiers))
1129
1130     -- Report "potential instances" only when the constraint arises
1131     -- directly from the user's use of an overloaded function
1132     want_potential (TypeEqOrigin {}) = False
1133     want_potential _                 = True
1134
1135     add_to_ctxt_fixes has_ambig_tvs
1136       | not has_ambig_tvs && all_tyvars
1137       , (orig:origs) <- usefulContext ctxt pred 
1138       = [sep [ ptext (sLit "add") <+> pprParendType pred
1139                <+> ptext (sLit "to the context of")
1140              , nest 2 $ ppr_skol orig $$
1141                         vcat [ ptext (sLit "or") <+> ppr_skol orig
1142                              | orig <- origs ] ] ]
1143       | otherwise = []
1144
1145     ppr_skol (PatSkol dc _) = ptext (sLit "the data constructor") <+> quotes (ppr dc)
1146     ppr_skol skol_info      = ppr skol_info
1147
1148     no_inst_msg
1149       | clas == coercibleClass
1150       = let (ty1, ty2) = getEqPredTys pred
1151         in sep [ ptext (sLit "Could not coerce from") <+> quotes (ppr ty1)
1152                , nest 19 (ptext (sLit "to") <+> quotes (ppr ty2)) ]
1153                  -- The nesting makes the types line up
1154       | null givens && null matches
1155       = ptext (sLit "No instance for")
1156         <+> pprParendType pred
1157         $$ if type_has_arrow pred
1158             then nest 2 $ ptext (sLit "(maybe you haven't applied enough arguments to a function?)")
1159             else empty
1160
1161       | otherwise
1162       = ptext (sLit "Could not deduce") <+> pprParendType pred
1163
1164     type_has_arrow (TyVarTy _)      = False
1165     type_has_arrow (AppTy t1 t2)    = type_has_arrow t1 || type_has_arrow t2
1166     type_has_arrow (TyConApp _ ts)  = or $ map type_has_arrow ts
1167     type_has_arrow (FunTy _ _)      = True
1168     type_has_arrow (ForAllTy _ t)   = type_has_arrow t
1169     type_has_arrow (LitTy _)        = False
1170
1171     drv_fixes = case orig of
1172                    DerivOrigin      -> [drv_fix]
1173                    DerivOriginDC {} -> [drv_fix]
1174                    DerivOriginCoerce {} -> [drv_fix]
1175                    _                -> []
1176
1177     drv_fix = hang (ptext (sLit "use a standalone 'deriving instance' declaration,"))
1178                  2 (ptext (sLit "so you can specify the instance context yourself"))
1179
1180     -- Normal overlap error
1181     overlap_msg
1182       = ASSERT( not (null matches) )
1183         vcat [  addArising orig (ptext (sLit "Overlapping instances for")
1184                                 <+> pprType (mkClassPred clas tys))
1185
1186              ,  ppUnless (null matching_givens) $
1187                   sep [ptext (sLit "Matching givens (or their superclasses):")
1188                       , nest 2 (vcat matching_givens)]
1189
1190              ,  sep [ptext (sLit "Matching instances:"),
1191                      nest 2 (vcat [pprInstances ispecs, pprInstances unifiers])]
1192
1193              ,  ppWhen (null matching_givens && isSingleton matches && null unifiers) $
1194                 -- Intuitively, some given matched the wanted in their
1195                 -- flattened or rewritten (from given equalities) form
1196                 -- but the matcher can't figure that out because the
1197                 -- constraints are non-flat and non-rewritten so we
1198                 -- simply report back the whole given
1199                 -- context. Accelerate Smart.hs showed this problem.
1200                   sep [ ptext (sLit "There exists a (perhaps superclass) match:")
1201                       , nest 2 (vcat (pp_givens givens))]
1202
1203              ,  ppWhen (isSingleton matches) $
1204                 parens (vcat [ ptext (sLit "The choice depends on the instantiation of") <+>
1205                                   quotes (pprWithCommas ppr (varSetElems (tyVarsOfTypes tys)))
1206                              , ppWhen (null (matching_givens)) $
1207                                vcat [ ptext (sLit "To pick the first instance above, use IncoherentInstances")
1208                                     , ptext (sLit "when compiling the other instance declarations")]
1209                         ])]
1210         where
1211             ispecs = [ispec | (ispec, _) <- matches]
1212
1213             givens = getUserGivens ctxt
1214             matching_givens = mapMaybe matchable givens
1215
1216             matchable (evvars,skol_info,_,loc)
1217               = case ev_vars_matching of
1218                      [] -> Nothing
1219                      _  -> Just $ hang (pprTheta ev_vars_matching)
1220                                     2 (sep [ ptext (sLit "bound by") <+> ppr skol_info
1221                                            , ptext (sLit "at") <+> ppr loc])
1222                 where ev_vars_matching = filter ev_var_matches (map evVarPred evvars)
1223                       ev_var_matches ty = case getClassPredTys_maybe ty of
1224                          Just (clas', tys')
1225                            | clas' == clas
1226                            , Just _ <- tcMatchTys (tyVarsOfTypes tys) tys tys'
1227                            -> True
1228                            | otherwise
1229                            -> any ev_var_matches (immSuperClasses clas' tys')
1230                          Nothing -> False
1231
1232     -- Overlap error because of Safe Haskell (first
1233     -- match should be the most specific match)
1234     safe_haskell_msg
1235       = ASSERT( length matches > 1 )
1236         vcat [ addArising orig (ptext (sLit "Unsafe overlapping instances for")
1237                         <+> pprType (mkClassPred clas tys))
1238              , sep [ptext (sLit "The matching instance is:"),
1239                     nest 2 (pprInstance $ head ispecs)]
1240              , vcat [ ptext $ sLit "It is compiled in a Safe module and as such can only"
1241                     , ptext $ sLit "overlap instances from the same module, however it"
1242                     , ptext $ sLit "overlaps the following instances from different modules:"
1243                     , nest 2 (vcat [pprInstances $ tail ispecs])
1244                     ]
1245              ]
1246
1247     -- This function tries to reconstruct why a "Coercible ty1 ty2" constraint
1248     -- is left over. Therefore its logic has to stay in sync with
1249     -- getCoericbleInst in TcInteract. See Note [Coercible Instances]
1250     coercible_explanation rdr_env
1251       | clas /= coercibleClass = empty
1252       | Just (tc1,tyArgs1) <- splitTyConApp_maybe ty1,
1253         Just (tc2,tyArgs2) <- splitTyConApp_maybe ty2,
1254         tc1 == tc2
1255       = nest 2 $ vcat $
1256           [ fsep [ hsep [ ptext $ sLit "because the", speakNth n, ptext $ sLit "type argument"]
1257                  , hsep [ ptext $ sLit "of", quotes (ppr tc1), ptext $ sLit "has role Nominal,"]
1258                  , ptext $ sLit "but the arguments"
1259                  , quotes (ppr t1)
1260                  , ptext $ sLit "and"
1261                  , quotes (ppr t2)
1262                  , ptext $ sLit "differ" ]
1263           | (n,Nominal,t1,t2) <- zip4 [1..] (tyConRoles tc1) tyArgs1 tyArgs2
1264           , not (t1 `eqType` t2)
1265           ]
1266       | Just (tc, tys) <- tcSplitTyConApp_maybe ty1
1267       , (rep_tc, _, _) <- tcLookupDataFamInst fam_envs tc tys
1268       , Just msg <- coercible_msg_for_tycon rdr_env rep_tc
1269       = msg
1270       | Just (tc, tys) <- splitTyConApp_maybe ty2
1271       , (rep_tc, _, _) <- tcLookupDataFamInst fam_envs tc tys
1272       , Just msg <- coercible_msg_for_tycon rdr_env rep_tc
1273       = msg
1274       | otherwise
1275       = nest 2 $ sep [ ptext (sLit "because") <+> quotes (ppr ty1)
1276                      , nest 4 (vcat [ ptext (sLit "and") <+> quotes (ppr ty2)
1277                                     , ptext (sLit "are different types.") ]) ]
1278       where
1279         (ty1, ty2) = getEqPredTys pred
1280
1281     coercible_msg_for_tycon rdr_env tc
1282         | isAbstractTyCon tc
1283         = Just $ hsep [ ptext $ sLit "because the type constructor", quotes (pprSourceTyCon tc)
1284                       , ptext $ sLit "is abstract" ]
1285         | isNewTyCon tc
1286         , [data_con] <- tyConDataCons tc
1287         , let dc_name = dataConName data_con
1288         , null (lookupGRE_Name rdr_env dc_name)
1289         = Just $ hang (ptext (sLit "because the data constructor") <+> quotes (ppr dc_name))
1290                     2 (sep [ ptext (sLit "of newtype") <+> quotes (pprSourceTyCon tc)
1291                            , ptext (sLit "is not in scope") ])
1292         | otherwise = Nothing
1293
1294 usefulContext :: ReportErrCtxt -> TcPredType -> [SkolemInfo]
1295 usefulContext ctxt pred
1296   = go (cec_encl ctxt)
1297   where
1298     pred_tvs = tyVarsOfType pred
1299     go [] = []
1300     go (ic : ics)
1301        = case ic_info ic of
1302                -- Do not suggest adding constraints to an *inferred* type signature!
1303            SigSkol (InfSigCtxt {}) _ -> rest
1304            info                      -> info : rest
1305        where
1306           -- Stop when the context binds a variable free in the predicate
1307           rest | any (`elemVarSet` pred_tvs) (ic_skols ic) = []
1308                | otherwise                                 = go ics
1309
1310 show_fixes :: [SDoc] -> SDoc
1311 show_fixes []     = empty
1312 show_fixes (f:fs) = sep [ ptext (sLit "Possible fix:")
1313                         , nest 2 (vcat (f : map (ptext (sLit "or") <+>) fs))]
1314
1315 ppr_insts :: [ClsInst] -> SDoc
1316 ppr_insts insts
1317   = pprInstances (take 3 insts) $$ dot_dot_message
1318   where
1319     n_extra = length insts - 3
1320     dot_dot_message
1321        | n_extra <= 0 = empty
1322        | otherwise    = ptext (sLit "...plus")
1323                         <+> speakNOf n_extra (ptext (sLit "other"))
1324
1325 ----------------------
1326 quickFlattenTy :: TcType -> TcM TcType
1327 -- See Note [Flattening in error message generation]
1328 quickFlattenTy ty | Just ty' <- tcView ty = quickFlattenTy ty'
1329 quickFlattenTy ty@(TyVarTy {})  = return ty
1330 quickFlattenTy ty@(ForAllTy {}) = return ty     -- See
1331 quickFlattenTy ty@(LitTy {})    = return ty
1332   -- Don't flatten because of the danger or removing a bound variable
1333 quickFlattenTy (AppTy ty1 ty2) = do { fy1 <- quickFlattenTy ty1
1334                                     ; fy2 <- quickFlattenTy ty2
1335                                     ; return (AppTy fy1 fy2) }
1336 quickFlattenTy (FunTy ty1 ty2) = do { fy1 <- quickFlattenTy ty1
1337                                     ; fy2 <- quickFlattenTy ty2
1338                                     ; return (FunTy fy1 fy2) }
1339 quickFlattenTy (TyConApp tc tys)
1340     | not (isTypeFamilyTyCon tc)
1341     = do { fys <- mapM quickFlattenTy tys
1342          ; return (TyConApp tc fys) }
1343     | otherwise
1344     = do { let (funtys,resttys) = splitAt (tyConArity tc) tys
1345                 -- Ignore the arguments of the type family funtys
1346          ; v <- newMetaTyVar (TauTv False) (typeKind (TyConApp tc funtys))
1347          ; flat_resttys <- mapM quickFlattenTy resttys
1348          ; return (foldl AppTy (mkTyVarTy v) flat_resttys) }
1349 \end{code}
1350
1351 Note [Flattening in error message generation]
1352 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1353 Consider (C (Maybe (F x))), where F is a type function, and we have
1354 instances
1355                 C (Maybe Int) and C (Maybe a)
1356 Since (F x) might turn into Int, this is an overlap situation, and
1357 indeed (because of flattening) the main solver will have refrained
1358 from solving.  But by the time we get to error message generation, we've
1359 un-flattened the constraint.  So we must *re*-flatten it before looking
1360 up in the instance environment, lest we only report one matching
1361 instance when in fact there are two.
1362
1363 Re-flattening is pretty easy, because we don't need to keep track of
1364 evidence.  We don't re-use the code in TcCanonical because that's in
1365 the TcS monad, and we are in TcM here.
1366
1367 Note [Quick-flatten polytypes]
1368 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1369 If we see C (Ix a => blah) or C (forall a. blah) we simply refrain from
1370 flattening any further.  After all, there can be no instance declarations
1371 that match such things.  And flattening under a for-all is problematic
1372 anyway; consider C (forall a. F a)
1373
1374 Note [Suggest -fprint-explicit-kinds]
1375 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1376 It can be terribly confusing to get an error message like (Trac #9171)
1377     Couldn't match expected type ‘GetParam Base (GetParam Base Int)’
1378                 with actual type ‘GetParam Base (GetParam Base Int)’
1379 The reason may be that the kinds don't match up.  Typically you'll get
1380 more useful information, but not when it's as a result of ambiguity.
1381 This test suggests -fprint-explicit-kinds when all the ambiguous type
1382 variables are kind variables.
1383
1384 \begin{code}
1385 mkAmbigMsg :: Ct -> (Bool, SDoc)
1386 mkAmbigMsg ct
1387   | null ambig_tkvs = (False, empty)
1388   | otherwise       = (True,  msg)
1389   where
1390     ambig_tkv_set = filterVarSet isAmbiguousTyVar (tyVarsOfCt ct)
1391     ambig_tkvs    = varSetElems ambig_tkv_set
1392     (ambig_kvs, ambig_tvs) = partition isKindVar ambig_tkvs
1393
1394     msg | any isRuntimeUnkSkol ambig_tkvs  -- See Note [Runtime skolems]
1395         =  vcat [ ptext (sLit "Cannot resolve unknown runtime type") <> plural ambig_tvs
1396                      <+> pprQuotedList ambig_tvs
1397                 , ptext (sLit "Use :print or :force to determine these types")]
1398
1399         | not (null ambig_tvs)
1400         = pp_ambig (ptext (sLit "type")) ambig_tvs
1401
1402         | otherwise  -- All ambiguous kind variabes; suggest -fprint-explicit-kinds
1403         = vcat [ pp_ambig (ptext (sLit "kind")) ambig_kvs
1404                , sdocWithDynFlags suggest_explicit_kinds ]
1405
1406     pp_ambig what tkvs
1407       = ptext (sLit "The") <+> what <+> ptext (sLit "variable") <> plural tkvs
1408         <+> pprQuotedList tkvs <+> is_or_are tkvs <+> ptext (sLit "ambiguous")
1409
1410     is_or_are [_] = text "is"
1411     is_or_are _   = text "are"
1412
1413     suggest_explicit_kinds dflags  -- See Note [Suggest -fprint-explicit-kinds]
1414       | gopt Opt_PrintExplicitKinds dflags = empty
1415       | otherwise = ptext (sLit "Use -fprint-explicit-kinds to see the kind arguments")
1416
1417 pprSkol :: SkolemInfo -> SrcLoc -> SDoc
1418 pprSkol UnkSkol   _
1419   = ptext (sLit "is an unknown type variable")
1420 pprSkol skol_info tv_loc
1421   = sep [ ptext (sLit "is a rigid type variable bound by"),
1422           sep [ppr skol_info, ptext (sLit "at") <+> ppr tv_loc]]
1423
1424 getSkolemInfo :: [Implication] -> TcTyVar -> SkolemInfo
1425 -- Get the skolem info for a type variable
1426 -- from the implication constraint that binds it
1427 getSkolemInfo [] tv
1428   = pprPanic "No skolem info:" (ppr tv)
1429
1430 getSkolemInfo (implic:implics) tv
1431   | tv `elem` ic_skols implic = ic_info implic
1432   | otherwise                 = getSkolemInfo implics tv
1433
1434 -----------------------
1435 -- relevantBindings looks at the value environment and finds values whose
1436 -- types mention any of the offending type variables.  It has to be
1437 -- careful to zonk the Id's type first, so it has to be in the monad.
1438 -- We must be careful to pass it a zonked type variable, too.
1439 --
1440 -- We always remove closed top-level bindings, though,
1441 -- since they are never relevant (cf Trac #8233)
1442
1443 relevantBindings :: Bool  -- True <=> filter by tyvar; False <=> no filtering
1444                           -- See Trac #8191
1445                  -> ReportErrCtxt -> Ct
1446                  -> TcM (ReportErrCtxt, SDoc)
1447 relevantBindings want_filtering ctxt ct
1448   = do { dflags <- getDynFlags
1449        ; (tidy_env', docs, discards)
1450               <- go (cec_tidy ctxt) (maxRelevantBinds dflags)
1451                     emptyVarSet [] False
1452                     (tcl_bndrs lcl_env)
1453          -- tcl_bndrs has the innermost bindings first,
1454          -- which are probably the most relevant ones
1455
1456        ; traceTc "relevantBindings" (ppr ct $$ ppr [id | TcIdBndr id _ <- tcl_bndrs lcl_env])
1457        ; let doc = hang (ptext (sLit "Relevant bindings include"))
1458                       2 (vcat docs $$ max_msg)
1459              max_msg | discards
1460                      = ptext (sLit "(Some bindings suppressed; use -fmax-relevant-binds=N or -fno-max-relevant-binds)")
1461                      | otherwise = empty
1462
1463        ; if null docs
1464          then return (ctxt, empty)
1465          else do { traceTc "rb" doc
1466                  ; return (ctxt { cec_tidy = tidy_env' }, doc) } }
1467   where
1468     loc       = ctLoc ct
1469     lcl_env   = ctLocEnv loc
1470     ct_tvs    = tyVarsOfCt ct `unionVarSet` extra_tvs
1471
1472     -- For *kind* errors, report the relevant bindings of the
1473     -- enclosing *type* equality, becuase that's more useful for the programmer
1474     extra_tvs = case ctLocOrigin loc of
1475                   KindEqOrigin t1 t2 _ -> tyVarsOfTypes [t1,t2]
1476                   _                    -> emptyVarSet
1477
1478     run_out :: Maybe Int -> Bool
1479     run_out Nothing = False
1480     run_out (Just n) = n <= 0
1481
1482     dec_max :: Maybe Int -> Maybe Int
1483     dec_max = fmap (\n -> n - 1)
1484
1485     go :: TidyEnv -> Maybe Int -> TcTyVarSet -> [SDoc]
1486        -> Bool                          -- True <=> some filtered out due to lack of fuel
1487        -> [TcIdBinder]
1488        -> TcM (TidyEnv, [SDoc], Bool)   -- The bool says if we filtered any out
1489                                         -- because of lack of fuel
1490     go tidy_env _ _ docs discards []
1491        = return (tidy_env, reverse docs, discards)
1492     go tidy_env n_left tvs_seen docs discards (TcIdBndr id top_lvl : tc_bndrs)
1493        = do { (tidy_env', tidy_ty) <- zonkTidyTcType tidy_env (idType id)
1494             ; traceTc "relevantBindings 1" (ppr id <+> dcolon <+> ppr tidy_ty)
1495             ; let id_tvs = tyVarsOfType tidy_ty
1496                   doc = sep [ pprPrefixOcc id <+> dcolon <+> ppr tidy_ty
1497                             , nest 2 (parens (ptext (sLit "bound at")
1498                                  <+> ppr (getSrcLoc id)))]
1499                   new_seen = tvs_seen `unionVarSet` id_tvs
1500
1501             ; if (want_filtering && not opt_PprStyle_Debug 
1502                                  && id_tvs `disjointVarSet` ct_tvs)
1503                        -- We want to filter out this binding anyway
1504                        -- so discard it silently
1505               then go tidy_env n_left tvs_seen docs discards tc_bndrs
1506
1507               else if isTopLevel top_lvl && not (isNothing n_left)
1508                        -- It's a top-level binding and we have not specified
1509                        -- -fno-max-relevant-bindings, so discard it silently
1510               then go tidy_env n_left tvs_seen docs discards tc_bndrs
1511
1512               else if run_out n_left && id_tvs `subVarSet` tvs_seen
1513                        -- We've run out of n_left fuel and this binding only
1514                        -- mentions aleady-seen type variables, so discard it
1515               then go tidy_env n_left tvs_seen docs True tc_bndrs
1516
1517                        -- Keep this binding, decrement fuel
1518               else go tidy_env' (dec_max n_left) new_seen (doc:docs) discards tc_bndrs }
1519
1520 -----------------------
1521 warnDefaulting :: Cts -> Type -> TcM ()
1522 warnDefaulting wanteds default_ty
1523   = do { warn_default <- woptM Opt_WarnTypeDefaults
1524        ; env0 <- tcInitTidyEnv
1525        ; let tidy_env = tidyFreeTyVars env0 $
1526                         tyVarsOfCts wanteds
1527              tidy_wanteds = mapBag (tidyCt tidy_env) wanteds
1528              (loc, ppr_wanteds) = pprWithArising (bagToList tidy_wanteds)
1529              warn_msg  = hang (ptext (sLit "Defaulting the following constraint(s) to type")
1530                                 <+> quotes (ppr default_ty))
1531                             2 ppr_wanteds
1532        ; setCtLoc loc $ warnTc warn_default warn_msg }
1533 \end{code}
1534
1535 Note [Runtime skolems]
1536 ~~~~~~~~~~~~~~~~~~~~~~
1537 We want to give a reasonably helpful error message for ambiguity
1538 arising from *runtime* skolems in the debugger.  These
1539 are created by in RtClosureInspect.zonkRTTIType.
1540
1541 %************************************************************************
1542 %*                                                                      *
1543                  Error from the canonicaliser
1544          These ones are called *during* constraint simplification
1545 %*                                                                      *
1546 %************************************************************************
1547
1548 \begin{code}
1549 solverDepthErrorTcS :: SubGoalCounter -> CtEvidence -> TcM a
1550 solverDepthErrorTcS cnt ev
1551   = setCtLoc loc $
1552     do { pred <- zonkTcType (ctEvPred ev)
1553        ; env0 <- tcInitTidyEnv
1554        ; let tidy_env  = tidyFreeTyVars env0 (tyVarsOfType pred)
1555              tidy_pred = tidyType tidy_env pred
1556        ; failWithTcM (tidy_env, hang (msg cnt) 2 (ppr tidy_pred)) }
1557   where
1558     loc   = ctEvLoc ev
1559     depth = ctLocDepth loc
1560     value = subGoalCounterValue cnt depth
1561     msg CountConstraints =
1562         vcat [ ptext (sLit "Context reduction stack overflow; size =") <+> int value
1563              , ptext (sLit "Use -fcontext-stack=N to increase stack size to N") ]
1564     msg CountTyFunApps =
1565         vcat [ ptext (sLit "Type function application stack overflow; size =") <+> int value
1566              , ptext (sLit "Use -ftype-function-depth=N to increase stack size to N") ]
1567 \end{code}
1568