Add a missing newline in the ghci :h text; spotted by Alexander McPhail
[ghc.git] / compiler / typecheck / TcEvidence.lhs
1 %
2 % (c) The University of Glasgow 2006
3 %
4
5 \begin{code}
6 module TcEvidence (
7
8   -- HsWrapper
9   HsWrapper(..), 
10   (<.>), mkWpTyApps, mkWpEvApps, mkWpEvVarApps, mkWpTyLams, mkWpLams, mkWpLet, 
11   idHsWrapper, isIdHsWrapper, pprHsWrapper,
12
13   -- Evidence bindin
14   TcEvBinds(..), EvBindsVar(..), 
15   EvBindMap(..), emptyEvBindMap, extendEvBinds, lookupEvBind, evBindMapBinds,
16
17   EvBind(..), emptyTcEvBinds, isEmptyTcEvBinds, 
18
19   EvTerm(..), mkEvCast, evVarsOfTerm, mkEvKindCast,
20
21   -- TcCoercion
22   TcCoercion(..), 
23   mkTcReflCo, mkTcTyConAppCo, mkTcAppCo, mkTcAppCos, mkTcFunCo,
24   mkTcAxInstCo, mkTcForAllCo, mkTcForAllCos, 
25   mkTcSymCo, mkTcTransCo, mkTcNthCo, mkTcInstCos,
26   tcCoercionKind, coVarsOfTcCo, isEqVar, mkTcCoVarCo, 
27   isTcReflCo, isTcReflCo_maybe, getTcCoVar_maybe,
28   liftTcCoSubstWith
29
30   ) where
31 #include "HsVersions.h"
32
33 import Var
34
35 import PprCore ()   -- Instance OutputableBndr TyVar
36 import TypeRep  -- Knows type representation
37 import TcType
38 import Type( tyConAppArgN, getEqPredTys_maybe, tyConAppTyCon_maybe )
39 import TysPrim( funTyCon )
40 import TyCon
41 import PrelNames
42 import VarEnv
43 import VarSet
44 import Name
45
46 import Util
47 import Bag
48 import Pair
49 import Control.Applicative
50 import Data.Traversable (traverse, sequenceA)
51 import qualified Data.Data as Data 
52 import Outputable
53 import FastString
54 import Data.IORef( IORef )
55 \end{code}
56
57
58 Note [TcCoercions]
59 ~~~~~~~~~~~~~~~~~~
60 | LCoercions are a hack used by the typechecker. Normally,
61 Coercions have free variables of type (a ~# b): we call these
62 CoVars. However, the type checker passes around equality evidence
63 (boxed up) at type (a ~ b).
64
65 An LCoercion is simply a Coercion whose free variables have the
66 boxed type (a ~ b). After we are done with typechecking the
67 desugarer finds the free variables, unboxes them, and creates a
68 resulting real Coercion with kosher free variables.
69
70 We can use most of the Coercion "smart constructors" to build LCoercions. However,
71 mkCoVarCo will not work! The equivalent is mkTcCoVarCo.
72
73 The data type is similar to Coercion.Coercion, with the following
74 differences
75   * Most important, TcLetCo adds let-bindings for coercions.
76     This is what lets us unify two for-all types and generate
77     equality constraints underneath
78
79   * The kind of a TcCoercion is  t1 ~  t2 
80              of a Coercion   is  t1 ~# t2
81
82   * TcAxiomInstCo takes Types, not Coecions as arguments;
83     the generality is required only in the Simplifier
84
85   * UnsafeCo aren't required
86
87   * Reprsentation invariants are weaker:
88      - we are allowed to have type synonyms in TcTyConAppCo
89      - the first arg of a TcAppCo can be a TcTyConAppCo
90     Reason: they'll get established when we desugar to Coercion
91
92 \begin{code}
93 data TcCoercion 
94   = TcRefl TcType
95   | TcTyConAppCo TyCon [TcCoercion]
96   | TcAppCo TcCoercion TcCoercion
97   | TcForAllCo TyVar TcCoercion 
98   | TcInstCo TcCoercion TcType
99   | TcCoVarCo EqVar
100   | TcAxiomInstCo CoAxiom [TcType]
101   | TcSymCo TcCoercion
102   | TcTransCo TcCoercion TcCoercion
103   | TcNthCo Int TcCoercion
104   | TcLetCo TcEvBinds TcCoercion
105   deriving (Data.Data, Data.Typeable)
106
107 isEqVar :: Var -> Bool 
108 -- Is lifted coercion variable (only!)
109 isEqVar v = case tyConAppTyCon_maybe (varType v) of
110                Just tc -> tc `hasKey` eqTyConKey
111                Nothing -> False
112
113 isTcReflCo_maybe :: TcCoercion -> Maybe TcType
114 isTcReflCo_maybe (TcRefl ty) = Just ty
115 isTcReflCo_maybe _             = Nothing
116
117 isTcReflCo :: TcCoercion -> Bool
118 isTcReflCo (TcRefl {}) = True
119 isTcReflCo _           = False
120
121 getTcCoVar_maybe :: TcCoercion -> Maybe CoVar
122 getTcCoVar_maybe (TcCoVarCo v) = Just v
123 getTcCoVar_maybe _             = Nothing
124
125 mkTcReflCo :: TcType -> TcCoercion
126 mkTcReflCo = TcRefl
127
128 mkTcFunCo :: TcCoercion -> TcCoercion -> TcCoercion
129 mkTcFunCo co1 co2 = mkTcTyConAppCo funTyCon [co1, co2]
130
131 mkTcTyConAppCo :: TyCon -> [TcCoercion] -> TcCoercion
132 mkTcTyConAppCo tc cos   -- No need to expand type synonyms
133                         -- See Note [TcCoercions]
134   | Just tys <- traverse isTcReflCo_maybe cos 
135   = TcRefl (mkTyConApp tc tys)    -- See Note [Refl invariant]
136
137   | otherwise = TcTyConAppCo tc cos
138
139 mkTcAxInstCo :: CoAxiom -> [TcType] -> TcCoercion
140 mkTcAxInstCo ax tys
141   | arity == n_tys = TcAxiomInstCo ax tys
142   | otherwise      = ASSERT( arity < n_tys )
143                      foldl TcAppCo (TcAxiomInstCo ax (take arity tys))
144                                    (map TcRefl (drop arity tys))
145   where
146     n_tys = length tys
147     arity = coAxiomArity ax
148
149 mkTcAppCo :: TcCoercion -> TcCoercion -> TcCoercion
150 -- No need to deal with TyConApp on the left; see Note [TcCoercions]
151 mkTcAppCo (TcRefl ty1) (TcRefl ty2)     = TcRefl (mkAppTy ty1 ty2)
152 mkTcAppCo co1 co2                       = TcAppCo co1 co2
153
154 mkTcSymCo :: TcCoercion -> TcCoercion
155 mkTcSymCo co@(TcRefl {})  = co
156 mkTcSymCo    (TcSymCo co) = co
157 mkTcSymCo co              = TcSymCo co
158
159 mkTcTransCo :: TcCoercion -> TcCoercion -> TcCoercion
160 mkTcTransCo (TcRefl _) co = co
161 mkTcTransCo co (TcRefl _) = co
162 mkTcTransCo co1 co2       = TcTransCo co1 co2
163
164 mkTcNthCo :: Int -> TcCoercion -> TcCoercion
165 mkTcNthCo n (TcRefl ty) = TcRefl (tyConAppArgN n ty)
166 mkTcNthCo n co          = TcNthCo n co
167
168 mkTcAppCos :: TcCoercion -> [TcCoercion] -> TcCoercion
169 mkTcAppCos co1 tys = foldl mkTcAppCo co1 tys
170
171 mkTcForAllCo :: Var -> TcCoercion -> TcCoercion
172 -- note that a TyVar should be used here, not a CoVar (nor a TcTyVar)
173 mkTcForAllCo tv (TcRefl ty) = ASSERT( isTyVar tv ) TcRefl (mkForAllTy tv ty)
174 mkTcForAllCo tv  co         = ASSERT( isTyVar tv ) TcForAllCo tv co
175
176 mkTcForAllCos :: [Var] -> TcCoercion -> TcCoercion
177 mkTcForAllCos tvs (TcRefl ty) = ASSERT( all isTyVar tvs ) TcRefl (mkForAllTys tvs ty)
178 mkTcForAllCos tvs co          = ASSERT( all isTyVar tvs ) foldr TcForAllCo co tvs
179
180 mkTcInstCos :: TcCoercion -> [TcType] -> TcCoercion
181 mkTcInstCos (TcRefl ty) tys = TcRefl (applyTys ty tys)
182 mkTcInstCos co tys          = foldl TcInstCo co tys
183
184 mkTcCoVarCo :: EqVar -> TcCoercion
185 -- ipv :: s ~ t  (the boxed equality type)
186 mkTcCoVarCo ipv
187   | ty1 `eqType` ty2 = TcRefl ty1
188   | otherwise        = TcCoVarCo ipv
189   where
190     (ty1, ty2) = case getEqPredTys_maybe (varType ipv) of
191         Nothing  -> pprPanic "mkCoVarLCo" (ppr ipv)
192         Just tys -> tys
193 \end{code}
194
195 \begin{code}
196 tcCoercionKind :: TcCoercion -> Pair Type
197 tcCoercionKind co = go co 
198   where 
199     go (TcRefl ty)            = Pair ty ty
200     go (TcLetCo _ co)         = go co
201     go (TcTyConAppCo tc cos)  = mkTyConApp tc <$> (sequenceA $ map go cos)
202     go (TcAppCo co1 co2)      = mkAppTy <$> go co1 <*> go co2
203     go (TcForAllCo tv co)     = mkForAllTy tv <$> go co
204     go (TcInstCo co ty)       = go_inst co [ty]
205     go (TcCoVarCo cv)         = eqVarKind cv
206     go (TcAxiomInstCo ax tys) = Pair (substTyWith (co_ax_tvs ax) tys (co_ax_lhs ax)) 
207                                      (substTyWith (co_ax_tvs ax) tys (co_ax_rhs ax))
208     go (TcSymCo co)           = swap $ go co
209     go (TcTransCo co1 co2)    = Pair (pFst $ go co1) (pSnd $ go co2)
210     go (TcNthCo d co)         = tyConAppArgN d <$> go co
211
212     -- c.f. Coercion.coercionKind
213     go_inst (TcInstCo co ty) tys = go_inst co (ty:tys)
214     go_inst co               tys = (`applyTys` tys) <$> go co
215
216 eqVarKind :: EqVar -> Pair Type
217 eqVarKind cv
218  | Just (tc, [_kind,ty1,ty2]) <- tcSplitTyConApp_maybe (varType cv)
219  = ASSERT (tc `hasKey` eqTyConKey)
220    Pair ty1 ty2
221  | otherwise = panic "eqVarKind, non coercion variable"
222
223 coVarsOfTcCo :: TcCoercion -> VarSet
224 -- Only works on *zonked* coercions, because of TcLetCo
225 coVarsOfTcCo tc_co
226   = go tc_co
227   where
228     go (TcRefl _)                = emptyVarSet
229     go (TcTyConAppCo _ cos)      = foldr (unionVarSet . go) emptyVarSet cos
230     go (TcAppCo co1 co2)         = go co1 `unionVarSet` go co2
231     go (TcForAllCo _ co)         = go co
232     go (TcInstCo co _)           = go co
233     go (TcCoVarCo v)             = unitVarSet v
234     go (TcAxiomInstCo {})        = emptyVarSet
235     go (TcSymCo co)              = go co
236     go (TcTransCo co1 co2)       = go co1 `unionVarSet` go co2
237     go (TcNthCo _ co)            = go co
238     go (TcLetCo (EvBinds bs) co) = foldrBag (unionVarSet . go_bind) (go co) bs
239                                    `minusVarSet` get_bndrs bs
240     go (TcLetCo {}) = pprPanic "coVarsOfTcCo called on non-zonked TcCoercion" (ppr tc_co)
241
242     -- We expect only coercion bindings
243     go_bind :: EvBind -> VarSet
244     go_bind (EvBind _ (EvCoercion co)) = go co
245     go_bind (EvBind _ (EvId v))        = unitVarSet v
246     go_bind other = pprPanic "coVarsOfTcCo:Bind" (ppr other)
247
248     get_bndrs :: Bag EvBind -> VarSet
249     get_bndrs = foldrBag (\ (EvBind b _) bs -> extendVarSet bs b) emptyVarSet 
250
251 liftTcCoSubstWith :: [TyVar] -> [TcCoercion] -> TcType -> TcCoercion
252 -- This version can ignore capture; the free varialbes of the 
253 -- TcCoerion are all fresh.  Result is mush simpler code
254 liftTcCoSubstWith tvs cos ty
255   = ASSERT( equalLength tvs cos )
256     go ty
257   where
258     env = zipVarEnv tvs cos
259
260     go ty@(TyVarTy tv)   = case lookupVarEnv env tv of
261                              Just co -> co
262                              Nothing -> mkTcReflCo ty
263     go (AppTy t1 t2)     = mkTcAppCo (go t1) (go t2)
264     go (TyConApp tc tys) = mkTcTyConAppCo tc (map go tys)
265     go (ForAllTy tv ty)  = mkTcForAllCo tv (go ty)
266     go (FunTy t1 t2)     = mkTcFunCo (go t1) (go t2)
267 \end{code}
268
269 Pretty printing
270
271 \begin{code}
272 instance Outputable TcCoercion where
273   ppr = pprTcCo
274
275 pprTcCo, pprParendTcCo :: TcCoercion -> SDoc
276 pprTcCo       co = ppr_co TopPrec   co
277 pprParendTcCo co = ppr_co TyConPrec co
278
279 ppr_co :: Prec -> TcCoercion -> SDoc
280 ppr_co _ (TcRefl ty) = angleBrackets (ppr ty)
281
282 ppr_co p co@(TcTyConAppCo tc [_,_])
283   | tc `hasKey` funTyConKey = ppr_fun_co p co
284
285 ppr_co p (TcTyConAppCo tc cos)   = pprTcApp   p ppr_co tc cos
286 ppr_co p (TcLetCo bs co)         = maybeParen p TopPrec $
287                                    sep [ptext (sLit "let") <+> braces (ppr bs), ppr co]
288 ppr_co p (TcAppCo co1 co2)       = maybeParen p TyConPrec $
289                                    pprTcCo co1 <+> ppr_co TyConPrec co2
290 ppr_co p co@(TcForAllCo {})      = ppr_forall_co p co
291 ppr_co p (TcInstCo co ty)        = maybeParen p TyConPrec $
292                                    pprParendTcCo co <> ptext (sLit "@") <> pprType ty
293                      
294 ppr_co _ (TcCoVarCo cv)          = parenSymOcc (getOccName cv) (ppr cv)
295 ppr_co p (TcAxiomInstCo con cos) = pprTypeNameApp p ppr_type (getName con) cos
296
297 ppr_co p (TcTransCo co1 co2) = maybeParen p FunPrec $
298                                ppr_co FunPrec co1
299                                <+> ptext (sLit ";")
300                                <+> ppr_co FunPrec co2
301 ppr_co p (TcSymCo co)         = pprPrefixApp p (ptext (sLit "Sym")) [pprParendTcCo co]
302 ppr_co p (TcNthCo n co)       = pprPrefixApp p (ptext (sLit "Nth:") <+> int n) [pprParendTcCo co]
303
304 ppr_fun_co :: Prec -> TcCoercion -> SDoc
305 ppr_fun_co p co = pprArrowChain p (split co)
306   where
307     split :: TcCoercion -> [SDoc]
308     split (TcTyConAppCo f [arg,res])
309       | f `hasKey` funTyConKey
310       = ppr_co FunPrec arg : split res
311     split co = [ppr_co TopPrec co]
312
313 ppr_forall_co :: Prec -> TcCoercion -> SDoc
314 ppr_forall_co p ty
315   = maybeParen p FunPrec $
316     sep [pprForAll tvs, ppr_co TopPrec rho]
317   where
318     (tvs,  rho) = split1 [] ty
319     split1 tvs (TcForAllCo tv ty) = split1 (tv:tvs) ty
320     split1 tvs ty                 = (reverse tvs, ty)
321 \end{code}
322
323 %************************************************************************
324 %*                                                                      *
325                   HsWrapper
326 %*                                                                      *
327 %************************************************************************
328
329 \begin{code}
330 data HsWrapper
331   = WpHole                      -- The identity coercion
332
333   | WpCompose HsWrapper HsWrapper
334        -- (wrap1 `WpCompose` wrap2)[e] = wrap1[ wrap2[ e ]]
335        --
336        -- Hence  (\a. []) `WpCompose` (\b. []) = (\a b. [])
337        -- But    ([] a)   `WpCompose` ([] b)   = ([] b a)
338
339   | WpCast TcCoercion         -- A cast:  [] `cast` co
340                               -- Guaranteed not the identity coercion
341
342         -- Evidence abstraction and application
343         -- (both dictionaries and coercions)
344   | WpEvLam EvVar               -- \d. []       the 'd' is an evidence variable
345   | WpEvApp EvTerm              -- [] d         the 'd' is evidence for a constraint
346
347         -- Kind and Type abstraction and application
348   | WpTyLam TyVar       -- \a. []  the 'a' is a type/kind variable (not coercion var)
349   | WpTyApp KindOrType  -- [] t    the 't' is a type (not coercion)
350
351
352   | WpLet TcEvBinds             -- Non-empty (or possibly non-empty) evidence bindings,
353                                 -- so that the identity coercion is always exactly WpHole
354   deriving (Data.Data, Data.Typeable)
355
356
357 (<.>) :: HsWrapper -> HsWrapper -> HsWrapper
358 WpHole <.> c = c
359 c <.> WpHole = c
360 c1 <.> c2    = c1 `WpCompose` c2
361
362 mkWpTyApps :: [Type] -> HsWrapper
363 mkWpTyApps tys = mk_co_app_fn WpTyApp tys
364
365 mkWpEvApps :: [EvTerm] -> HsWrapper
366 mkWpEvApps args = mk_co_app_fn WpEvApp args
367
368 mkWpEvVarApps :: [EvVar] -> HsWrapper
369 mkWpEvVarApps vs = mkWpEvApps (map EvId vs)
370
371 mkWpTyLams :: [TyVar] -> HsWrapper
372 mkWpTyLams ids = mk_co_lam_fn WpTyLam ids
373
374 mkWpLams :: [Var] -> HsWrapper
375 mkWpLams ids = mk_co_lam_fn WpEvLam ids
376
377 mkWpLet :: TcEvBinds -> HsWrapper
378 -- This no-op is a quite a common case
379 mkWpLet (EvBinds b) | isEmptyBag b = WpHole
380 mkWpLet ev_binds                   = WpLet ev_binds
381
382 mk_co_lam_fn :: (a -> HsWrapper) -> [a] -> HsWrapper
383 mk_co_lam_fn f as = foldr (\x wrap -> f x <.> wrap) WpHole as
384
385 mk_co_app_fn :: (a -> HsWrapper) -> [a] -> HsWrapper
386 -- For applications, the *first* argument must
387 -- come *last* in the composition sequence
388 mk_co_app_fn f as = foldr (\x wrap -> wrap <.> f x) WpHole as
389
390 idHsWrapper :: HsWrapper
391 idHsWrapper = WpHole
392
393 isIdHsWrapper :: HsWrapper -> Bool
394 isIdHsWrapper WpHole = True
395 isIdHsWrapper _      = False
396 \end{code}
397
398
399 %************************************************************************
400 %*                                                                      *
401                   Evidence bindings
402 %*                                                                      *
403 %************************************************************************
404
405 \begin{code}
406 data TcEvBinds
407   = TcEvBinds           -- Mutable evidence bindings
408        EvBindsVar       -- Mutable because they are updated "later"
409                         --    when an implication constraint is solved
410
411   | EvBinds             -- Immutable after zonking
412        (Bag EvBind)
413
414   deriving( Data.Typeable )
415
416 data EvBindsVar = EvBindsVar (IORef EvBindMap) Unique
417      -- The Unique is only for debug printing
418
419 instance Data.Data TcEvBinds where
420   -- Placeholder; we can't travers into TcEvBinds
421   toConstr _   = abstractConstr "TcEvBinds"
422   gunfold _ _  = error "gunfold"
423   dataTypeOf _ = Data.mkNoRepType "TcEvBinds"
424
425 -----------------
426 newtype EvBindMap 
427   = EvBindMap { 
428        ev_bind_varenv :: VarEnv EvBind
429     }       -- Map from evidence variables to evidence terms
430
431 emptyEvBindMap :: EvBindMap
432 emptyEvBindMap = EvBindMap { ev_bind_varenv = emptyVarEnv }
433
434 extendEvBinds :: EvBindMap -> EvVar -> EvTerm -> EvBindMap
435 extendEvBinds bs v t 
436   = EvBindMap { ev_bind_varenv = extendVarEnv (ev_bind_varenv bs) v (EvBind v t) }
437
438 lookupEvBind :: EvBindMap -> EvVar -> Maybe EvBind
439 lookupEvBind bs = lookupVarEnv (ev_bind_varenv bs)
440
441 evBindMapBinds :: EvBindMap -> Bag EvBind
442 evBindMapBinds bs 
443   = foldVarEnv consBag emptyBag (ev_bind_varenv bs)
444
445 -----------------
446 -- All evidence is bound by EvBinds; no side effects
447 data EvBind = EvBind EvVar EvTerm
448
449 data EvTerm
450   = EvId EvId                    -- Term-level variable-to-variable bindings
451                                  -- (no coercion variables! they come via EvCoercion)
452
453   | EvCoercion TcCoercion        -- (Boxed) coercion bindings
454
455   | EvCast EvVar TcCoercion      -- d |> co
456
457   | EvDFunApp DFunId             -- Dictionary instance application
458        [Type] [EvVar]
459
460   | EvTupleSel EvId  Int         -- n'th component of the tuple
461
462   | EvTupleMk [EvId]             -- tuple built from this stuff
463
464   | EvDelayedError Type FastString  -- Used with Opt_DeferTypeErrors
465                                -- See Note [Deferring coercion errors to runtime]
466                                -- in TcSimplify
467
468   | EvSuperClass DictId Int      -- n'th superclass. Used for both equalities and
469                                  -- dictionaries, even though the former have no
470                                  -- selector Id.  We count up from _0_
471   | EvKindCast EvVar TcCoercion  -- See Note [EvKindCast]
472            
473   deriving( Data.Data, Data.Typeable)
474 \end{code}
475
476 Note [EvKindCast] 
477 ~~~~~~~~~~~~~~~~~ 
478
479 EvKindCast g kco is produced when we have a constraint (g : s1 ~ s2) 
480 but the kinds of s1 and s2 (k1 and k2 respectively) don't match but 
481 are rather equal by a coercion. You may think that this coercion will
482 always turn out to be ReflCo, so why is this needed? Because sometimes
483 we will want to defer kind errors until the runtime and in these cases
484 that coercion will be an 'error' term, which we want to evaluate rather
485 than silently forget about!
486
487 The relevant (and only) place where such a coercion is produced in 
488 the simplifier is in emit_kind_constraint in TcCanonical.
489
490
491 Note [EvBinds/EvTerm]
492 ~~~~~~~~~~~~~~~~~~~~~
493 How evidence is created and updated. Bindings for dictionaries,
494 and coercions and implicit parameters are carried around in TcEvBinds
495 which during constraint generation and simplification is always of the
496 form (TcEvBinds ref). After constraint simplification is finished it
497 will be transformed to t an (EvBinds ev_bag).
498
499 Evidence for coercions *SHOULD* be filled in using the TcEvBinds
500 However, all EvVars that correspond to *wanted* coercion terms in
501 an EvBind must be mutable variables so that they can be readily
502 inlined (by zonking) after constraint simplification is finished.
503
504 Conclusion: a new wanted coercion variable should be made mutable.
505 [Notice though that evidence variables that bind coercion terms
506  from super classes will be "given" and hence rigid]
507
508
509 \begin{code}
510 mkEvCast :: EvVar -> TcCoercion -> EvTerm
511 mkEvCast ev lco
512   | isTcReflCo lco = EvId ev
513   | otherwise      = EvCast ev lco
514
515 mkEvKindCast :: EvVar -> TcCoercion -> EvTerm
516 mkEvKindCast ev lco
517   | isTcReflCo lco = EvId ev
518   | otherwise      = EvKindCast ev lco
519
520 emptyTcEvBinds :: TcEvBinds
521 emptyTcEvBinds = EvBinds emptyBag
522
523 isEmptyTcEvBinds :: TcEvBinds -> Bool
524 isEmptyTcEvBinds (EvBinds b)    = isEmptyBag b
525 isEmptyTcEvBinds (TcEvBinds {}) = panic "isEmptyTcEvBinds"
526
527
528 evVarsOfTerm :: EvTerm -> [EvVar]
529 evVarsOfTerm (EvId v) = [v]
530 evVarsOfTerm (EvCoercion co)      = varSetElems (coVarsOfTcCo co)
531 evVarsOfTerm (EvDFunApp _ _ evs)  = evs
532 evVarsOfTerm (EvTupleSel v _)     = [v]
533 evVarsOfTerm (EvSuperClass v _)   = [v]
534 evVarsOfTerm (EvCast v co)        = v : varSetElems (coVarsOfTcCo co)
535 evVarsOfTerm (EvTupleMk evs)      = evs
536 evVarsOfTerm (EvDelayedError _ _) = []
537 evVarsOfTerm (EvKindCast v co)   = v : varSetElems (coVarsOfTcCo co)
538 \end{code}
539
540
541 %************************************************************************
542 %*                                                                      *
543                   Pretty printing
544 %*                                                                      *
545 %************************************************************************
546
547 \begin{code}
548 instance Outputable HsWrapper where
549   ppr co_fn = pprHsWrapper (ptext (sLit "<>")) co_fn
550
551 pprHsWrapper :: SDoc -> HsWrapper -> SDoc
552 -- In debug mode, print the wrapper
553 -- otherwise just print what's inside
554 pprHsWrapper doc wrap
555   = getPprStyle (\ s -> if debugStyle s then (help (add_parens doc) wrap False) else doc)
556   where
557     help :: (Bool -> SDoc) -> HsWrapper -> Bool -> SDoc
558     -- True  <=> appears in function application position
559     -- False <=> appears as body of let or lambda
560     help it WpHole             = it
561     help it (WpCompose f1 f2)  = help (help it f2) f1
562     help it (WpCast co)   = add_parens $ sep [it False, nest 2 (ptext (sLit "|>")
563                                               <+> pprParendTcCo co)]
564     help it (WpEvApp id)  = no_parens  $ sep [it True, nest 2 (ppr id)]
565     help it (WpTyApp ty)  = no_parens  $ sep [it True, ptext (sLit "@") <+> pprParendType ty]
566     help it (WpEvLam id)  = add_parens $ sep [ ptext (sLit "\\") <> pp_bndr id, it False]
567     help it (WpTyLam tv)  = add_parens $ sep [ptext (sLit "/\\") <> pp_bndr tv, it False]
568     help it (WpLet binds) = add_parens $ sep [ptext (sLit "let") <+> braces (ppr binds), it False]
569
570     pp_bndr v = pprBndr LambdaBind v <> dot
571
572     add_parens, no_parens :: SDoc -> Bool -> SDoc
573     add_parens d True  = parens d
574     add_parens d False = d
575     no_parens d _ = d
576
577 instance Outputable TcEvBinds where
578   ppr (TcEvBinds v) = ppr v
579   ppr (EvBinds bs)  = ptext (sLit "EvBinds") <> braces (vcat (map ppr (bagToList bs)))
580
581 instance Outputable EvBindsVar where
582   ppr (EvBindsVar _ u) = ptext (sLit "EvBindsVar") <> angleBrackets (ppr u)
583
584 instance Outputable EvBind where
585   ppr (EvBind v e)   = sep [ ppr v, nest 2 $ equals <+> ppr e ]
586    -- We cheat a bit and pretend EqVars are CoVars for the purposes of pretty printing
587
588 instance Outputable EvTerm where
589   ppr (EvId v)           = ppr v
590   ppr (EvCast v co)      = ppr v <+> (ptext (sLit "`cast`")) <+> pprParendTcCo co
591   ppr (EvKindCast v co)  = ppr v <+> (ptext (sLit "`kind-cast`")) <+> pprParendTcCo co
592   ppr (EvCoercion co)    = ptext (sLit "CO") <+> ppr co
593   ppr (EvTupleSel v n)   = ptext (sLit "tupsel") <> parens (ppr (v,n))
594   ppr (EvTupleMk vs)     = ptext (sLit "tupmk") <+> ppr vs
595   ppr (EvSuperClass d n) = ptext (sLit "sc") <> parens (ppr (d,n))
596   ppr (EvDFunApp df tys ts) = ppr df <+> sep [ char '@' <> ppr tys, ppr ts ]
597   ppr (EvDelayedError ty msg) =     ptext (sLit "error") 
598                                 <+> sep [ char '@' <> ppr ty, ppr msg ]
599 \end{code}
600