09c0333447cba3771fc63218a67ffe713b0fcc2f
[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 bindings
14   TcEvBinds(..), EvBindsVar(..), 
15   EvBindMap(..), emptyEvBindMap, extendEvBinds, lookupEvBind, evBindMapBinds,
16   EvBind(..), emptyTcEvBinds, isEmptyTcEvBinds, 
17   EvTerm(..), mkEvCast, evVarsOfTerm, 
18   EvLit(..), evTermCoercion,
19   EvCoercible(..), EvCoercibleArg(..), mapEvCoercibleArgM,
20
21   -- TcCoercion
22   TcCoercion(..), LeftOrRight(..), pickLR,
23   mkTcReflCo, mkTcTyConAppCo, mkTcAppCo, mkTcAppCos, mkTcFunCo,
24   mkTcAxInstCo, mkTcUnbranchedAxInstCo, mkTcForAllCo, mkTcForAllCos, 
25   mkTcSymCo, mkTcTransCo, mkTcNthCo, mkTcLRCo, mkTcInstCos,
26   mkTcAxiomRuleCo,
27   tcCoercionKind, coVarsOfTcCo, isEqVar, mkTcCoVarCo, 
28   isTcReflCo, isTcReflCo_maybe, getTcCoVar_maybe,
29   liftTcCoSubstWith
30
31   ) where
32 #include "HsVersions.h"
33
34 import Var
35 import Coercion( LeftOrRight(..), pickLR )
36 import PprCore ()   -- Instance OutputableBndr TyVar
37 import TypeRep  -- Knows type representation
38 import TcType
39 import Type( tyConAppArgN, tyConAppTyCon_maybe, getEqPredTys, coAxNthLHS )
40 import TysPrim( funTyCon )
41 import TyCon
42 import CoAxiom
43 import PrelNames
44 import VarEnv
45 import VarSet
46 import Name
47
48 import Util
49 import Bag
50 import Pair
51 import Control.Applicative
52 import Data.Traversable (traverse, sequenceA)
53 import qualified Data.Data as Data 
54 import Outputable
55 import FastString
56 import Data.IORef( IORef )
57 \end{code}
58
59
60 Note [TcCoercions]
61 ~~~~~~~~~~~~~~~~~~
62 | LCoercions are a hack used by the typechecker. Normally,
63 Coercions have free variables of type (a ~# b): we call these
64 CoVars. However, the type checker passes around equality evidence
65 (boxed up) at type (a ~ b).
66
67 An LCoercion is simply a Coercion whose free variables have the
68 boxed type (a ~ b). After we are done with typechecking the
69 desugarer finds the free variables, unboxes them, and creates a
70 resulting real Coercion with kosher free variables.
71
72 We can use most of the Coercion "smart constructors" to build LCoercions. However,
73 mkCoVarCo will not work! The equivalent is mkTcCoVarCo.
74
75 The data type is similar to Coercion.Coercion, with the following
76 differences
77   * Most important, TcLetCo adds let-bindings for coercions.
78     This is what lets us unify two for-all types and generate
79     equality constraints underneath
80
81   * The kind of a TcCoercion is  t1 ~  t2 
82              of a Coercion   is  t1 ~# t2
83
84   * TcCoercions are essentially all at role Nominal -- the type-checker
85     reasons only about nominal equality, not representational.
86     --> Exception: there can be newtype axioms wrapped up in TcCoercions.
87                    These, of course, are only used in casts, so the desugarer
88                    will still produce the right 'Coercion's.
89
90   * TcAxiomInstCo takes Types, not Coecions as arguments;
91     the generality is required only in the Simplifier
92
93   * UnsafeCo aren't required
94
95   * Reprsentation invariants are weaker:
96      - we are allowed to have type synonyms in TcTyConAppCo
97      - the first arg of a TcAppCo can be a TcTyConAppCo
98     Reason: they'll get established when we desugar to Coercion
99
100 \begin{code}
101 data TcCoercion 
102   = TcRefl TcType
103   | TcTyConAppCo TyCon [TcCoercion]
104   | TcAppCo TcCoercion TcCoercion
105   | TcForAllCo TyVar TcCoercion 
106   | TcInstCo TcCoercion TcType
107   | TcCoVarCo EqVar               -- variable always at role N
108   | TcAxiomInstCo (CoAxiom Branched) Int [TcType] -- Int specifies branch number
109                                                   -- See [CoAxiom Index] in Coercion.lhs
110   -- This is number of types and coercions are expected to macth to CoAxiomRule
111   -- (i.e., the CoAxiomRules are always fully saturated)
112   | TcAxiomRuleCo CoAxiomRule [TcType] [TcCoercion]
113   | TcSymCo TcCoercion
114   | TcTransCo TcCoercion TcCoercion
115   | TcNthCo Int TcCoercion
116   | TcLRCo LeftOrRight TcCoercion
117   | TcCastCo TcCoercion TcCoercion     -- co1 |> co2
118   | TcLetCo TcEvBinds TcCoercion
119   deriving (Data.Data, Data.Typeable)
120
121 isEqVar :: Var -> Bool 
122 -- Is lifted coercion variable (only!)
123 isEqVar v = case tyConAppTyCon_maybe (varType v) of
124                Just tc -> tc `hasKey` eqTyConKey
125                Nothing -> False
126
127 isTcReflCo_maybe :: TcCoercion -> Maybe TcType
128 isTcReflCo_maybe (TcRefl ty) = Just ty
129 isTcReflCo_maybe _           = Nothing
130
131 isTcReflCo :: TcCoercion -> Bool
132 isTcReflCo (TcRefl {}) = True
133 isTcReflCo _           = False
134
135 getTcCoVar_maybe :: TcCoercion -> Maybe CoVar
136 getTcCoVar_maybe (TcCoVarCo v) = Just v
137 getTcCoVar_maybe _             = Nothing
138
139 mkTcReflCo :: TcType -> TcCoercion
140 mkTcReflCo = TcRefl
141
142 mkTcFunCo :: TcCoercion -> TcCoercion -> TcCoercion
143 mkTcFunCo co1 co2 = mkTcTyConAppCo funTyCon [co1, co2]
144
145 mkTcTyConAppCo :: TyCon -> [TcCoercion] -> TcCoercion
146 mkTcTyConAppCo tc cos   -- No need to expand type synonyms
147                         -- See Note [TcCoercions]
148   | Just tys <- traverse isTcReflCo_maybe cos 
149   = TcRefl (mkTyConApp tc tys)    -- See Note [Refl invariant]
150
151   | otherwise = TcTyConAppCo tc cos
152
153 mkTcAxInstCo :: CoAxiom br -> Int -> [TcType] -> TcCoercion
154 mkTcAxInstCo ax ind tys
155   | arity == n_tys = TcAxiomInstCo ax_br ind tys
156   | otherwise      = ASSERT( arity < n_tys )
157                      foldl TcAppCo (TcAxiomInstCo ax_br ind (take arity tys))
158                                    (map TcRefl (drop arity tys))
159   where
160     n_tys = length tys
161     arity = coAxiomArity ax ind
162     ax_br = toBranchedAxiom ax
163
164 mkTcAxiomRuleCo :: CoAxiomRule -> [TcType] -> [TcCoercion] -> TcCoercion
165 mkTcAxiomRuleCo = TcAxiomRuleCo
166
167 mkTcUnbranchedAxInstCo :: CoAxiom Unbranched -> [TcType] -> TcCoercion
168 mkTcUnbranchedAxInstCo ax tys
169   = mkTcAxInstCo ax 0 tys
170
171 mkTcAppCo :: TcCoercion -> TcCoercion -> TcCoercion
172 -- No need to deal with TyConApp on the left; see Note [TcCoercions]
173 mkTcAppCo (TcRefl ty1) (TcRefl ty2)     = TcRefl (mkAppTy ty1 ty2)
174 mkTcAppCo co1 co2                       = TcAppCo co1 co2
175
176 mkTcSymCo :: TcCoercion -> TcCoercion
177 mkTcSymCo co@(TcRefl {})  = co
178 mkTcSymCo    (TcSymCo co) = co
179 mkTcSymCo co              = TcSymCo co
180
181 mkTcTransCo :: TcCoercion -> TcCoercion -> TcCoercion
182 mkTcTransCo (TcRefl _) co = co
183 mkTcTransCo co (TcRefl _) = co
184 mkTcTransCo co1 co2       = TcTransCo co1 co2
185
186 mkTcNthCo :: Int -> TcCoercion -> TcCoercion
187 mkTcNthCo n (TcRefl ty) = TcRefl (tyConAppArgN n ty)
188 mkTcNthCo n co          = TcNthCo n co
189
190 mkTcLRCo :: LeftOrRight -> TcCoercion -> TcCoercion
191 mkTcLRCo lr (TcRefl ty) = TcRefl (pickLR lr (tcSplitAppTy ty))
192 mkTcLRCo lr co          = TcLRCo lr co
193
194 mkTcAppCos :: TcCoercion -> [TcCoercion] -> TcCoercion
195 mkTcAppCos co1 tys = foldl mkTcAppCo co1 tys
196
197 mkTcForAllCo :: Var -> TcCoercion -> TcCoercion
198 -- note that a TyVar should be used here, not a CoVar (nor a TcTyVar)
199 mkTcForAllCo tv (TcRefl ty) = ASSERT( isTyVar tv ) TcRefl (mkForAllTy tv ty)
200 mkTcForAllCo tv  co         = ASSERT( isTyVar tv ) TcForAllCo tv co
201
202 mkTcForAllCos :: [Var] -> TcCoercion -> TcCoercion
203 mkTcForAllCos tvs (TcRefl ty) = ASSERT( all isTyVar tvs ) TcRefl (mkForAllTys tvs ty)
204 mkTcForAllCos tvs co          = ASSERT( all isTyVar tvs ) foldr TcForAllCo co tvs
205
206 mkTcInstCos :: TcCoercion -> [TcType] -> TcCoercion
207 mkTcInstCos (TcRefl ty) tys = TcRefl (applyTys ty tys)
208 mkTcInstCos co tys          = foldl TcInstCo co tys
209
210 mkTcCoVarCo :: EqVar -> TcCoercion
211 -- ipv :: s ~ t  (the boxed equality type)
212 mkTcCoVarCo ipv = TcCoVarCo ipv
213   -- Previously I checked for (ty ~ ty) and generated Refl,
214   -- but in fact ipv may not even (visibly) have a (t1 ~ t2) type, because
215   -- the constraint solver does not substitute in the types of
216   -- evidence variables as it goes.  In any case, the optimisation
217   -- will be done in the later zonking phase
218 \end{code}
219
220 \begin{code}
221 tcCoercionKind :: TcCoercion -> Pair Type
222 tcCoercionKind co = go co 
223   where 
224     go (TcRefl ty)            = Pair ty ty
225     go (TcLetCo _ co)         = go co
226     go (TcCastCo _ co)        = case getEqPredTys (pSnd (go co)) of
227                                    (ty1,ty2) -> Pair ty1 ty2
228     go (TcTyConAppCo tc cos)  = mkTyConApp tc <$> (sequenceA $ map go cos)
229     go (TcAppCo co1 co2)      = mkAppTy <$> go co1 <*> go co2
230     go (TcForAllCo tv co)     = mkForAllTy tv <$> go co
231     go (TcInstCo co ty)       = go_inst co [ty]
232     go (TcCoVarCo cv)         = eqVarKind cv
233     go (TcAxiomInstCo ax ind tys)
234       = let branch = coAxiomNthBranch ax ind
235             tvs    = coAxBranchTyVars branch
236         in Pair (substTyWith tvs tys (coAxNthLHS ax ind)) 
237                 (substTyWith tvs tys (coAxBranchRHS branch))
238     go (TcSymCo co)           = swap (go co)
239     go (TcTransCo co1 co2)    = Pair (pFst (go co1)) (pSnd (go co2))
240     go (TcNthCo d co)         = tyConAppArgN d <$> go co
241     go (TcLRCo lr co)         = (pickLR lr . tcSplitAppTy) <$> go co
242     go (TcAxiomRuleCo ax ts cs) =
243        case coaxrProves ax ts (map tcCoercionKind cs) of
244          Just res -> res
245          Nothing -> panic "tcCoercionKind: malformed TcAxiomRuleCo"
246
247     -- c.f. Coercion.coercionKind
248     go_inst (TcInstCo co ty) tys = go_inst co (ty:tys)
249     go_inst co               tys = (`applyTys` tys) <$> go co
250
251 eqVarKind :: EqVar -> Pair Type
252 eqVarKind cv
253  | Just (tc, [_kind,ty1,ty2]) <- tcSplitTyConApp_maybe (varType cv)
254  = ASSERT(tc `hasKey` eqTyConKey)
255    Pair ty1 ty2
256  | otherwise = pprPanic "eqVarKind, non coercion variable" (ppr cv <+> dcolon <+> ppr (varType cv))
257
258 coVarsOfTcCo :: TcCoercion -> VarSet
259 -- Only works on *zonked* coercions, because of TcLetCo
260 coVarsOfTcCo tc_co
261   = go tc_co
262   where
263     go (TcRefl _)                = emptyVarSet
264     go (TcTyConAppCo _ cos)      = foldr (unionVarSet . go) emptyVarSet cos
265     go (TcAppCo co1 co2)         = go co1 `unionVarSet` go co2
266     go (TcCastCo co1 co2)        = go co1 `unionVarSet` go co2
267     go (TcForAllCo _ co)         = go co
268     go (TcInstCo co _)           = go co
269     go (TcCoVarCo v)             = unitVarSet v
270     go (TcAxiomInstCo {})        = emptyVarSet
271     go (TcSymCo co)              = go co
272     go (TcTransCo co1 co2)       = go co1 `unionVarSet` go co2
273     go (TcNthCo _ co)            = go co
274     go (TcLRCo  _ co)            = go co
275     go (TcLetCo (EvBinds bs) co) = foldrBag (unionVarSet . go_bind) (go co) bs
276                                    `minusVarSet` get_bndrs bs
277     go (TcLetCo {}) = emptyVarSet    -- Harumph. This does legitimately happen in the call
278                                      -- to evVarsOfTerm in the DEBUG check of setEvBind
279     go (TcAxiomRuleCo _ _ cos)   = foldr (unionVarSet . go) emptyVarSet cos
280
281
282     -- We expect only coercion bindings, so use evTermCoercion 
283     go_bind :: EvBind -> VarSet
284     go_bind (EvBind _ tm) = go (evTermCoercion tm)
285
286     get_bndrs :: Bag EvBind -> VarSet
287     get_bndrs = foldrBag (\ (EvBind b _) bs -> extendVarSet bs b) emptyVarSet 
288
289 liftTcCoSubstWith :: [TyVar] -> [TcCoercion] -> TcType -> TcCoercion
290 -- This version can ignore capture; the free varialbes of the 
291 -- TcCoerion are all fresh.  Result is mush simpler code
292 liftTcCoSubstWith tvs cos ty
293   = ASSERT( equalLength tvs cos )
294     go ty
295   where
296     env = zipVarEnv tvs cos
297
298     go ty@(TyVarTy tv)   = case lookupVarEnv env tv of
299                              Just co -> co
300                              Nothing -> mkTcReflCo ty
301     go (AppTy t1 t2)     = mkTcAppCo (go t1) (go t2)
302     go (TyConApp tc tys) = mkTcTyConAppCo tc (map go tys)
303     go ty@(LitTy {})     = mkTcReflCo ty
304     go (ForAllTy tv ty)  = mkTcForAllCo tv (go ty)
305     go (FunTy t1 t2)     = mkTcFunCo (go t1) (go t2)
306 \end{code}
307
308 Pretty printing
309
310 \begin{code}
311 instance Outputable TcCoercion where
312   ppr = pprTcCo
313
314 pprTcCo, pprParendTcCo :: TcCoercion -> SDoc
315 pprTcCo       co = ppr_co TopPrec   co
316 pprParendTcCo co = ppr_co TyConPrec co
317
318 ppr_co :: Prec -> TcCoercion -> SDoc
319 ppr_co _ (TcRefl ty) = angleBrackets (ppr ty)
320
321 ppr_co p co@(TcTyConAppCo tc [_,_])
322   | tc `hasKey` funTyConKey = ppr_fun_co p co
323
324 ppr_co p (TcTyConAppCo tc cos)   = pprTcApp   p ppr_co tc cos
325 ppr_co p (TcLetCo bs co)         = maybeParen p TopPrec $
326                                    sep [ptext (sLit "let") <+> braces (ppr bs), ppr co]
327 ppr_co p (TcAppCo co1 co2)       = maybeParen p TyConPrec $
328                                    pprTcCo co1 <+> ppr_co TyConPrec co2
329 ppr_co p (TcCastCo co1 co2)      = maybeParen p FunPrec $
330                                    ppr_co FunPrec co1 <+> ptext (sLit "|>") <+> ppr_co FunPrec co2
331 ppr_co p co@(TcForAllCo {})      = ppr_forall_co p co
332 ppr_co p (TcInstCo co ty)        = maybeParen p TyConPrec $
333                                    pprParendTcCo co <> ptext (sLit "@") <> pprType ty
334                      
335 ppr_co _ (TcCoVarCo cv)          = parenSymOcc (getOccName cv) (ppr cv)
336
337 ppr_co p (TcAxiomInstCo con ind cos)
338   = pprPrefixApp p (ppr (getName con) <> brackets (ppr ind)) (map (ppr_type TyConPrec) cos)
339
340 ppr_co p (TcTransCo co1 co2) = maybeParen p FunPrec $
341                                ppr_co FunPrec co1
342                                <+> ptext (sLit ";")
343                                <+> ppr_co FunPrec co2
344 ppr_co p (TcSymCo co)         = pprPrefixApp p (ptext (sLit "Sym")) [pprParendTcCo co]
345 ppr_co p (TcNthCo n co)       = pprPrefixApp p (ptext (sLit "Nth:") <+> int n) [pprParendTcCo co]
346 ppr_co p (TcLRCo lr co)       = pprPrefixApp p (ppr lr) [pprParendTcCo co]
347 ppr_co p (TcAxiomRuleCo co ts ps) = maybeParen p TopPrec
348                                   $ ppr_tc_axiom_rule_co co ts ps
349
350 ppr_tc_axiom_rule_co :: CoAxiomRule -> [TcType] -> [TcCoercion] -> SDoc
351 ppr_tc_axiom_rule_co co ts ps = ppr (coaxrName co) <> ppTs ts $$ nest 2 (ppPs ps)
352   where
353   ppTs []   = Outputable.empty
354   ppTs [t]  = ptext (sLit "@") <> ppr_type TopPrec t
355   ppTs ts   = ptext (sLit "@") <>
356                 parens (hsep $ punctuate comma $ map pprType ts)
357
358   ppPs []   = Outputable.empty
359   ppPs [p]  = pprParendTcCo p
360   ppPs (p : ps) = ptext (sLit "(") <+> pprTcCo p $$
361                   vcat [ ptext (sLit ",") <+> pprTcCo q | q <- ps ] $$
362                   ptext (sLit ")")
363
364
365
366
367 ppr_fun_co :: Prec -> TcCoercion -> SDoc
368 ppr_fun_co p co = pprArrowChain p (split co)
369   where
370     split :: TcCoercion -> [SDoc]
371     split (TcTyConAppCo f [arg,res])
372       | f `hasKey` funTyConKey
373       = ppr_co FunPrec arg : split res
374     split co = [ppr_co TopPrec co]
375
376 ppr_forall_co :: Prec -> TcCoercion -> SDoc
377 ppr_forall_co p ty
378   = maybeParen p FunPrec $
379     sep [pprForAll tvs, ppr_co TopPrec rho]
380   where
381     (tvs,  rho) = split1 [] ty
382     split1 tvs (TcForAllCo tv ty) = split1 (tv:tvs) ty
383     split1 tvs ty                 = (reverse tvs, ty)
384 \end{code}
385
386 %************************************************************************
387 %*                                                                      *
388                   HsWrapper
389 %*                                                                      *
390 %************************************************************************
391
392 \begin{code}
393 data HsWrapper
394   = WpHole                      -- The identity coercion
395
396   | WpCompose HsWrapper HsWrapper
397        -- (wrap1 `WpCompose` wrap2)[e] = wrap1[ wrap2[ e ]]
398        --
399        -- Hence  (\a. []) `WpCompose` (\b. []) = (\a b. [])
400        -- But    ([] a)   `WpCompose` ([] b)   = ([] b a)
401
402   | WpCast TcCoercion         -- A cast:  [] `cast` co
403                               -- Guaranteed not the identity coercion
404
405         -- Evidence abstraction and application
406         -- (both dictionaries and coercions)
407   | WpEvLam EvVar               -- \d. []       the 'd' is an evidence variable
408   | WpEvApp EvTerm              -- [] d         the 'd' is evidence for a constraint
409
410         -- Kind and Type abstraction and application
411   | WpTyLam TyVar       -- \a. []  the 'a' is a type/kind variable (not coercion var)
412   | WpTyApp KindOrType  -- [] t    the 't' is a type (not coercion)
413
414
415   | WpLet TcEvBinds             -- Non-empty (or possibly non-empty) evidence bindings,
416                                 -- so that the identity coercion is always exactly WpHole
417   deriving (Data.Data, Data.Typeable)
418
419
420 (<.>) :: HsWrapper -> HsWrapper -> HsWrapper
421 WpHole <.> c = c
422 c <.> WpHole = c
423 c1 <.> c2    = c1 `WpCompose` c2
424
425 mkWpTyApps :: [Type] -> HsWrapper
426 mkWpTyApps tys = mk_co_app_fn WpTyApp tys
427
428 mkWpEvApps :: [EvTerm] -> HsWrapper
429 mkWpEvApps args = mk_co_app_fn WpEvApp args
430
431 mkWpEvVarApps :: [EvVar] -> HsWrapper
432 mkWpEvVarApps vs = mkWpEvApps (map EvId vs)
433
434 mkWpTyLams :: [TyVar] -> HsWrapper
435 mkWpTyLams ids = mk_co_lam_fn WpTyLam ids
436
437 mkWpLams :: [Var] -> HsWrapper
438 mkWpLams ids = mk_co_lam_fn WpEvLam ids
439
440 mkWpLet :: TcEvBinds -> HsWrapper
441 -- This no-op is a quite a common case
442 mkWpLet (EvBinds b) | isEmptyBag b = WpHole
443 mkWpLet ev_binds                   = WpLet ev_binds
444
445 mk_co_lam_fn :: (a -> HsWrapper) -> [a] -> HsWrapper
446 mk_co_lam_fn f as = foldr (\x wrap -> f x <.> wrap) WpHole as
447
448 mk_co_app_fn :: (a -> HsWrapper) -> [a] -> HsWrapper
449 -- For applications, the *first* argument must
450 -- come *last* in the composition sequence
451 mk_co_app_fn f as = foldr (\x wrap -> wrap <.> f x) WpHole as
452
453 idHsWrapper :: HsWrapper
454 idHsWrapper = WpHole
455
456 isIdHsWrapper :: HsWrapper -> Bool
457 isIdHsWrapper WpHole = True
458 isIdHsWrapper _      = False
459 \end{code}
460
461
462 %************************************************************************
463 %*                                                                      *
464                   Evidence bindings
465 %*                                                                      *
466 %************************************************************************
467
468 \begin{code}
469 data TcEvBinds
470   = TcEvBinds           -- Mutable evidence bindings
471        EvBindsVar       -- Mutable because they are updated "later"
472                         --    when an implication constraint is solved
473
474   | EvBinds             -- Immutable after zonking
475        (Bag EvBind)
476
477   deriving( Data.Typeable )
478
479 data EvBindsVar = EvBindsVar (IORef EvBindMap) Unique
480      -- The Unique is only for debug printing
481
482 instance Data.Data TcEvBinds where
483   -- Placeholder; we can't travers into TcEvBinds
484   toConstr _   = abstractConstr "TcEvBinds"
485   gunfold _ _  = error "gunfold"
486   dataTypeOf _ = Data.mkNoRepType "TcEvBinds"
487
488 -----------------
489 newtype EvBindMap 
490   = EvBindMap { 
491        ev_bind_varenv :: VarEnv EvBind
492     }       -- Map from evidence variables to evidence terms
493
494 emptyEvBindMap :: EvBindMap
495 emptyEvBindMap = EvBindMap { ev_bind_varenv = emptyVarEnv }
496
497 extendEvBinds :: EvBindMap -> EvVar -> EvTerm -> EvBindMap
498 extendEvBinds bs v t 
499   = EvBindMap { ev_bind_varenv = extendVarEnv (ev_bind_varenv bs) v (EvBind v t) }
500
501 lookupEvBind :: EvBindMap -> EvVar -> Maybe EvBind
502 lookupEvBind bs = lookupVarEnv (ev_bind_varenv bs)
503
504 evBindMapBinds :: EvBindMap -> Bag EvBind
505 evBindMapBinds bs 
506   = foldVarEnv consBag emptyBag (ev_bind_varenv bs)
507
508 -----------------
509 -- All evidence is bound by EvBinds; no side effects
510 data EvBind = EvBind EvVar EvTerm
511
512 data EvTerm
513   = EvId EvId                    -- Any sort of evidence Id, including coercions
514
515   | EvCoercion TcCoercion        -- (Boxed) coercion bindings 
516                                  -- See Note [Coercion evidence terms]
517
518   | EvCast EvTerm TcCoercion     -- d |> co
519
520   | EvDFunApp DFunId             -- Dictionary instance application
521        [Type] [EvTerm]
522
523   | EvTupleSel EvTerm  Int       -- n'th component of the tuple, 0-indexed
524
525   | EvTupleMk [EvTerm]           -- tuple built from this stuff
526
527   | EvDelayedError Type FastString  -- Used with Opt_DeferTypeErrors
528                                -- See Note [Deferring coercion errors to runtime]
529                                -- in TcSimplify
530
531   | EvSuperClass EvTerm Int      -- n'th superclass. Used for both equalities and
532                                  -- dictionaries, even though the former have no
533                                  -- selector Id.  We count up from _0_
534
535   | EvLit EvLit                  -- Dictionary for class "SingI" for type lits.
536                                  -- Note [SingI and EvLit]
537
538   | EvCoercible EvCoercible      -- Dictionary for "Coercible a b"
539                                  -- Note [Coercible Instances]
540
541   deriving( Data.Data, Data.Typeable)
542
543
544 data EvLit
545   = EvNum Integer
546   | EvStr FastString
547     deriving( Data.Data, Data.Typeable)
548
549 data EvCoercible
550   = EvCoercibleRefl Type
551   | EvCoercibleTyCon TyCon [EvCoercibleArg EvTerm]
552   | EvCoercibleNewType LeftOrRight TyCon [Type] EvTerm
553     deriving( Data.Data, Data.Typeable)
554
555 data EvCoercibleArg a
556   = EvCoercibleArgN Type
557   | EvCoercibleArgR a
558   | EvCoercibleArgP Type Type
559     deriving( Data.Data, Data.Typeable)
560
561 mapEvCoercibleArgM :: Monad m => (a -> m b) -> EvCoercibleArg a -> m (EvCoercibleArg b)
562 mapEvCoercibleArgM _ (EvCoercibleArgN t)     = return (EvCoercibleArgN t)
563 mapEvCoercibleArgM f (EvCoercibleArgR v)     = do { v' <- f v; return (EvCoercibleArgR v') }
564 mapEvCoercibleArgM _ (EvCoercibleArgP t1 t2) = return (EvCoercibleArgP t1 t2)
565 \end{code}
566
567 Note [Coercion evidence terms]
568 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
569 A "coercion evidence term" takes one of these forms
570    co_tm ::= EvId v           where v :: t1 ~ t2
571            | EvCoercion co
572            | EvCast co_tm co
573
574 We do quite often need to get a TcCoercion from an EvTerm; see
575 'evTermCoercion'.
576
577 INVARIANT: The evidence for any constraint with type (t1~t2) is 
578 a coercion evidence term.  Consider for example
579     [G] d :: F Int a
580 If we have
581     ax7 a :: F Int a ~ (a ~ Bool)
582 then we do NOT generate the constraint
583     [G} (d |> ax7 a) :: a ~ Bool
584 because that does not satisfy the invariant (d is not a coercion variable).  
585 Instead we make a binding
586     g1 :: a~Bool = g |> ax7 a
587 and the constraint
588     [G] g1 :: a~Bool
589 See Trac [7238] and Note [Bind new Givens immediately] in TcSMonad
590
591 Note [EvBinds/EvTerm]
592 ~~~~~~~~~~~~~~~~~~~~~
593 How evidence is created and updated. Bindings for dictionaries,
594 and coercions and implicit parameters are carried around in TcEvBinds
595 which during constraint generation and simplification is always of the
596 form (TcEvBinds ref). After constraint simplification is finished it
597 will be transformed to t an (EvBinds ev_bag).
598
599 Evidence for coercions *SHOULD* be filled in using the TcEvBinds
600 However, all EvVars that correspond to *wanted* coercion terms in
601 an EvBind must be mutable variables so that they can be readily
602 inlined (by zonking) after constraint simplification is finished.
603
604 Conclusion: a new wanted coercion variable should be made mutable.
605 [Notice though that evidence variables that bind coercion terms
606  from super classes will be "given" and hence rigid]
607
608
609 Note [SingI and EvLit]
610 ~~~~~~~~~~~~~~~~~~~~~~
611 A part of the type-level literals implementation is the class "SingI",
612 which provides a "smart" constructor for defining singleton values.
613 Here is the key stuff from GHC.TypeLits
614
615   class SingI n where
616     sing :: Sing n
617
618   data family Sing (n::k)
619   newtype instance Sing (n :: Nat)    = SNat Integer
620   newtype instance Sing (s :: Symbol) = SSym String
621
622 Conceptually, this class has infinitely many instances:
623
624   instance Sing 0       where sing = SNat 0
625   instance Sing 1       where sing = SNat 1
626   instance Sing 2       where sing = SNat 2
627   instance Sing "hello" where sing = SSym "hello"
628   ...
629
630 In practice, we solve "SingI" predicates in the type-checker because we can't
631 have infinately many instances.  The evidence (aka "dictionary")
632 for "SingI (n :: Nat)" is of the form "EvLit (EvNum n)".
633
634 We make the following assumptions about dictionaries in GHC:
635   1. The "dictionary" for classes with a single method---like SingI---is
636      a newtype for the type of the method, so using a evidence amounts
637      to a coercion, and
638   2. Newtypes use the same representation as their definition types.
639
640 So, the evidence for "SingI" is just a value of the representation type,
641 wrapped in two newtype constructors: one to make it into a "Sing" value,
642 and another to make it into "SingI" evidence.
643
644
645 \begin{code}
646 mkEvCast :: EvTerm -> TcCoercion -> EvTerm
647 mkEvCast ev lco
648   | isTcReflCo lco = ev
649   | otherwise      = EvCast ev lco
650
651 emptyTcEvBinds :: TcEvBinds
652 emptyTcEvBinds = EvBinds emptyBag
653
654 isEmptyTcEvBinds :: TcEvBinds -> Bool
655 isEmptyTcEvBinds (EvBinds b)    = isEmptyBag b
656 isEmptyTcEvBinds (TcEvBinds {}) = panic "isEmptyTcEvBinds"
657
658
659 evTermCoercion :: EvTerm -> TcCoercion
660 -- Applied only to EvTerms of type (s~t)
661 -- See Note [Coercion evidence terms]
662 evTermCoercion (EvId v)        = mkTcCoVarCo v
663 evTermCoercion (EvCoercion co) = co
664 evTermCoercion (EvCast tm co)  = TcCastCo (evTermCoercion tm) co
665 evTermCoercion tm = pprPanic "evTermCoercion" (ppr tm)
666
667 evVarsOfTerm :: EvTerm -> VarSet
668 evVarsOfTerm (EvId v)             = unitVarSet v
669 evVarsOfTerm (EvCoercion co)      = coVarsOfTcCo co
670 evVarsOfTerm (EvDFunApp _ _ evs)  = evVarsOfTerms evs
671 evVarsOfTerm (EvTupleSel v _)     = evVarsOfTerm v
672 evVarsOfTerm (EvSuperClass v _)   = evVarsOfTerm v
673 evVarsOfTerm (EvCast tm co)       = evVarsOfTerm tm `unionVarSet` coVarsOfTcCo co
674 evVarsOfTerm (EvTupleMk evs)      = evVarsOfTerms evs
675 evVarsOfTerm (EvDelayedError _ _) = emptyVarSet
676 evVarsOfTerm (EvLit _)            = emptyVarSet
677 evVarsOfTerm (EvCoercible evnt)   = evVarsOfEvCoercible evnt
678
679 evVarsOfEvCoercible :: EvCoercible -> VarSet
680 evVarsOfEvCoercible (EvCoercibleRefl _)          = emptyVarSet
681 evVarsOfEvCoercible (EvCoercibleTyCon _ evs)     = evVarsOfTerms [v | EvCoercibleArgR v <- evs ]
682 evVarsOfEvCoercible (EvCoercibleNewType _ _ _ v) = evVarsOfTerm v
683
684 evVarsOfTerms :: [EvTerm] -> VarSet
685 evVarsOfTerms = foldr (unionVarSet . evVarsOfTerm) emptyVarSet 
686 \end{code}
687
688
689 %************************************************************************
690 %*                                                                      *
691                   Pretty printing
692 %*                                                                      *
693 %************************************************************************
694
695 \begin{code}
696 instance Outputable HsWrapper where
697   ppr co_fn = pprHsWrapper (ptext (sLit "<>")) co_fn
698
699 pprHsWrapper :: SDoc -> HsWrapper -> SDoc
700 -- In debug mode, print the wrapper
701 -- otherwise just print what's inside
702 pprHsWrapper doc wrap
703   = getPprStyle (\ s -> if debugStyle s then (help (add_parens doc) wrap False) else doc)
704   where
705     help :: (Bool -> SDoc) -> HsWrapper -> Bool -> SDoc
706     -- True  <=> appears in function application position
707     -- False <=> appears as body of let or lambda
708     help it WpHole             = it
709     help it (WpCompose f1 f2)  = help (help it f2) f1
710     help it (WpCast co)   = add_parens $ sep [it False, nest 2 (ptext (sLit "|>")
711                                               <+> pprParendTcCo co)]
712     help it (WpEvApp id)  = no_parens  $ sep [it True, nest 2 (ppr id)]
713     help it (WpTyApp ty)  = no_parens  $ sep [it True, ptext (sLit "@") <+> pprParendType ty]
714     help it (WpEvLam id)  = add_parens $ sep [ ptext (sLit "\\") <> pp_bndr id, it False]
715     help it (WpTyLam tv)  = add_parens $ sep [ptext (sLit "/\\") <> pp_bndr tv, it False]
716     help it (WpLet binds) = add_parens $ sep [ptext (sLit "let") <+> braces (ppr binds), it False]
717
718     pp_bndr v = pprBndr LambdaBind v <> dot
719
720     add_parens, no_parens :: SDoc -> Bool -> SDoc
721     add_parens d True  = parens d
722     add_parens d False = d
723     no_parens d _ = d
724
725 instance Outputable TcEvBinds where
726   ppr (TcEvBinds v) = ppr v
727   ppr (EvBinds bs)  = ptext (sLit "EvBinds") <> braces (vcat (map ppr (bagToList bs)))
728
729 instance Outputable EvBindsVar where
730   ppr (EvBindsVar _ u) = ptext (sLit "EvBindsVar") <> angleBrackets (ppr u)
731
732 instance Outputable EvBind where
733   ppr (EvBind v e)   = sep [ ppr v, nest 2 $ equals <+> ppr e ]
734    -- We cheat a bit and pretend EqVars are CoVars for the purposes of pretty printing
735
736 instance Outputable EvTerm where
737   ppr (EvId v)           = ppr v
738   ppr (EvCast v co)      = ppr v <+> (ptext (sLit "`cast`")) <+> pprParendTcCo co
739   ppr (EvCoercion co)    = ptext (sLit "CO") <+> ppr co
740   ppr (EvTupleSel v n)   = ptext (sLit "tupsel") <> parens (ppr (v,n))
741   ppr (EvTupleMk vs)     = ptext (sLit "tupmk") <+> ppr vs
742   ppr (EvSuperClass d n) = ptext (sLit "sc") <> parens (ppr (d,n))
743   ppr (EvDFunApp df tys ts) = ppr df <+> sep [ char '@' <> ppr tys, ppr ts ]
744   ppr (EvLit l)          = ppr l
745   ppr (EvCoercible co)   = ptext (sLit "Coercible") <+> ppr co
746   ppr (EvDelayedError ty msg) =     ptext (sLit "error") 
747                                 <+> sep [ char '@' <> ppr ty, ppr msg ]
748
749 instance Outputable EvLit where
750   ppr (EvNum n) = integer n
751   ppr (EvStr s) = text (show s)
752
753 instance Outputable EvCoercible where
754   ppr (EvCoercibleRefl ty) = ppr ty
755   ppr (EvCoercibleTyCon tyCon evs) = ppr tyCon <+> hsep (map ppr evs)
756   ppr (EvCoercibleNewType CLeft tyCon tys v) = ppr (tyCon `mkTyConApp` tys) <+> char ';' <+> ppr v
757   ppr (EvCoercibleNewType CRight tyCon tys v) =ppr v <+> char ';' <+> ppr (tyCon `mkTyConApp` tys)
758
759 instance Outputable a => Outputable (EvCoercibleArg a) where
760   ppr (EvCoercibleArgN t)     = ptext (sLit "N:") <+> ppr t
761   ppr (EvCoercibleArgR v)     = ptext (sLit "R:") <+> ppr v
762   ppr (EvCoercibleArgP t1 t2) = ptext (sLit "P:") <+> parens (ppr (t1,t2))
763 \end{code}
764