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