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