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