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