b74a8af8b7bb518cff572a8c52aab1ac49fd9149
[ghc.git] / compiler / types / Coercion.lhs
1 %
2 % (c) The University of Glasgow 2006
3 %
4
5 Module for type coercions, as in System FC.
6
7 Coercions are represented as types, and their kinds tell what types the 
8 coercion works on. 
9
10 The coercion kind constructor is a special TyCon that must always be saturated
11
12   typeKind (symCoercion type) :: TyConApp CoercionTyCon{...} [type, type]
13
14 \begin{code}
15 {-# OPTIONS -fno-warn-incomplete-patterns #-}
16 -- The above warning supression flag is a temporary kludge.
17 -- While working on this module you are encouraged to remove it and fix
18 -- any warnings in the module. See
19 --     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings
20 -- for details
21
22 module Coercion (
23         Coercion,
24  
25         mkCoKind, mkReflCoKind, splitCoercionKind_maybe, splitCoercionKind,
26         coercionKind, coercionKinds, coercionKindPredTy,
27
28         -- Equality predicates
29         isEqPred, mkEqPred, getEqPredTys, isEqPredTy,  
30
31         -- Coercion transformations
32         mkCoercion,
33         mkSymCoercion, mkTransCoercion,
34         mkLeftCoercion, mkRightCoercion, mkRightCoercions,
35         mkInstCoercion, mkAppCoercion,
36         mkForAllCoercion, mkFunCoercion, mkInstsCoercion, mkUnsafeCoercion,
37         mkNewTypeCoercion, mkFamInstCoercion, mkAppsCoercion,
38
39         splitNewTypeRepCo_maybe, instNewTyCon_maybe, decomposeCo,
40
41         unsafeCoercionTyCon, symCoercionTyCon,
42         transCoercionTyCon, leftCoercionTyCon, 
43         rightCoercionTyCon, instCoercionTyCon, -- needed by TysWiredIn
44
45         -- CoercionI
46         CoercionI(..),
47         isIdentityCoercion,
48         mkSymCoI, mkTransCoI, 
49         mkTyConAppCoI, mkAppTyCoI, mkFunTyCoI,
50         mkNoteTyCoI, mkForAllTyCoI,
51         fromCoI, fromACo,
52         mkClassPPredCoI, mkIParamPredCoI, mkEqPredCoI
53
54        ) where 
55
56 #include "HsVersions.h"
57
58 import TypeRep
59 import Type
60 import TyCon
61 import Class
62 import Var
63 import Name
64 import OccName
65 import PrelNames
66 import Util
67 import Unique
68 import BasicTypes
69 import Outputable
70
71
72 type Coercion     = Type
73 type CoercionKind = Kind        -- A CoercionKind is always of form (ty1 :=: ty2)
74
75 ------------------------------
76 decomposeCo :: Arity -> Coercion -> [Coercion]
77 -- (decomposeCo 3 c) = [right (left (left c)), right (left c), right c]
78 -- So this breaks a coercion with kind T A B C :=: T D E F into
79 -- a list of coercions of kinds A :=: D, B :=: E and E :=: F
80 decomposeCo n co
81   = go n co []
82   where
83     go 0 _  cos = cos
84     go n co cos = go (n-1) (mkLeftCoercion co)
85                            (mkRightCoercion co : cos)
86
87 ------------------------------
88
89 -------------------------------------------------------
90 -- and some coercion kind stuff
91
92 isEqPredTy :: Type -> Bool
93 isEqPredTy (PredTy pred) = isEqPred pred
94 isEqPredTy _             = False
95
96 mkEqPred :: (Type, Type) -> PredType
97 mkEqPred (ty1, ty2) = EqPred ty1 ty2
98
99 getEqPredTys :: PredType -> (Type,Type)
100 getEqPredTys (EqPred ty1 ty2) = (ty1, ty2)
101 getEqPredTys other            = pprPanic "getEqPredTys" (ppr other)
102
103 mkCoKind :: Type -> Type -> CoercionKind
104 mkCoKind ty1 ty2 = PredTy (EqPred ty1 ty2)
105
106 mkReflCoKind :: Type -> CoercionKind
107 mkReflCoKind ty = mkCoKind ty ty
108
109 splitCoercionKind :: CoercionKind -> (Type, Type)
110 splitCoercionKind co | Just co' <- kindView co = splitCoercionKind co'
111 splitCoercionKind (PredTy (EqPred ty1 ty2))    = (ty1, ty2)
112
113 splitCoercionKind_maybe :: Kind -> Maybe (Type, Type)
114 splitCoercionKind_maybe co | Just co' <- kindView co = splitCoercionKind_maybe co'
115 splitCoercionKind_maybe (PredTy (EqPred ty1 ty2)) = Just (ty1, ty2)
116 splitCoercionKind_maybe _ = Nothing
117
118 coercionKind :: Coercion -> (Type, Type)
119 --      c :: (t1 :=: t2)
120 -- Then (coercionKind c) = (t1,t2)
121 coercionKind ty@(TyVarTy a) | isCoVar a = splitCoercionKind (tyVarKind a)
122                             | otherwise = (ty, ty)
123 coercionKind (AppTy ty1 ty2) 
124   = let (t1, t2) = coercionKind ty1
125         (s1, s2) = coercionKind ty2 in
126     (mkAppTy t1 s1, mkAppTy t2 s2)
127 coercionKind (TyConApp tc args)
128   | Just (ar, rule) <- isCoercionTyCon_maybe tc 
129     -- CoercionTyCons carry their kinding rule, so we use it here
130   = ASSERT( length args >= ar ) -- Always saturated
131     let (ty1,ty2)    = rule (take ar args)      -- Apply the rule to the right number of args
132         (tys1, tys2) = coercionKinds (drop ar args)
133     in (mkAppTys ty1 tys1, mkAppTys ty2 tys2)
134
135   | otherwise
136   = let (lArgs, rArgs) = coercionKinds args in
137     (TyConApp tc lArgs, TyConApp tc rArgs)
138 coercionKind (FunTy ty1 ty2) 
139   = let (t1, t2) = coercionKind ty1
140         (s1, s2) = coercionKind ty2 in
141     (mkFunTy t1 s1, mkFunTy t2 s2)
142 coercionKind (ForAllTy tv ty) 
143   = let (ty1, ty2) = coercionKind ty in
144     (ForAllTy tv ty1, ForAllTy tv ty2)
145 coercionKind (NoteTy _ ty) = coercionKind ty
146 coercionKind (PredTy (EqPred c1 c2)) 
147   = let k1 = coercionKindPredTy c1
148         k2 = coercionKindPredTy c2 in
149     (k1,k2)
150 coercionKind (PredTy (ClassP cl args)) 
151   = let (lArgs, rArgs) = coercionKinds args in
152     (PredTy (ClassP cl lArgs), PredTy (ClassP cl rArgs))
153 coercionKind (PredTy (IParam name ty))
154   = let (ty1, ty2) = coercionKind ty in
155     (PredTy (IParam name ty1), PredTy (IParam name ty2))
156
157 coercionKindPredTy :: Coercion -> CoercionKind
158 coercionKindPredTy c = let (t1, t2) = coercionKind c in mkCoKind t1 t2
159
160 coercionKinds :: [Coercion] -> ([Type], [Type])
161 coercionKinds tys = unzip $ map coercionKind tys
162
163 -------------------------------------
164 -- Coercion kind and type mk's
165 -- (make saturated TyConApp CoercionTyCon{...} args)
166
167 mkCoercion :: TyCon -> [Type] -> Coercion
168 mkCoercion coCon args = ASSERT( tyConArity coCon == length args ) 
169                         TyConApp coCon args
170
171 mkAppCoercion, mkFunCoercion, mkTransCoercion, mkInstCoercion :: Coercion -> Coercion -> Coercion
172 mkSymCoercion, mkLeftCoercion, mkRightCoercion :: Coercion -> Coercion
173 mkAppsCoercion, mkInstsCoercion :: Coercion -> [Coercion] -> Coercion
174 mkForAllCoercion :: Var -> Coercion -> Coercion
175
176 mkAppCoercion    co1 co2 = mkAppTy co1 co2
177 mkAppsCoercion   co1 tys = foldl mkAppTy co1 tys
178 -- note that a TyVar should be used here, not a CoVar (nor a TcTyVar)
179 mkForAllCoercion tv  co  = ASSERT ( isTyVar tv ) mkForAllTy tv co
180 mkFunCoercion    co1 co2 = mkFunTy co1 co2
181
182
183 -------------------------------
184 -- This smart constructor creates a sym'ed version its argument,
185 -- but tries to push the sym's down to the leaves.  If we come to
186 -- sym tv or sym tycon then we can drop the sym because tv and tycon
187 -- are reflexive coercions
188 mkSymCoercion co      
189   | Just co' <- coreView co = mkSymCoercion co'
190
191 mkSymCoercion (ForAllTy tv ty)  = ForAllTy tv (mkSymCoercion ty)
192 mkSymCoercion (AppTy co1 co2)   = AppTy (mkSymCoercion co1) (mkSymCoercion co2)
193 mkSymCoercion (FunTy co1 co2)   = FunTy (mkSymCoercion co1) (mkSymCoercion co2)
194
195 mkSymCoercion (TyConApp tc cos) 
196   | not (isCoercionTyCon tc) = mkTyConApp tc (map mkSymCoercion cos)
197
198 mkSymCoercion (TyConApp tc [co]) 
199   | tc `hasKey` symCoercionTyConKey   = co    -- sym (sym co) --> co
200   | tc `hasKey` leftCoercionTyConKey  = mkLeftCoercion (mkSymCoercion co)
201   | tc `hasKey` rightCoercionTyConKey = mkRightCoercion (mkSymCoercion co)
202
203 mkSymCoercion (TyConApp tc [co1,co2]) 
204   | tc `hasKey` transCoercionTyConKey
205      -- sym (co1 `trans` co2) --> (sym co2) `trans (sym co2)
206      -- Note reversal of arguments!
207   = mkTransCoercion (mkSymCoercion co2) (mkSymCoercion co1)
208
209   | tc `hasKey` instCoercionTyConKey
210      -- sym (co @ ty) --> (sym co) @ ty
211      -- Note: sym is not applied to 'ty'
212   = mkInstCoercion (mkSymCoercion co1) co2
213
214 mkSymCoercion (TyConApp tc cos)         -- Other coercion tycons, such as those
215   = mkCoercion symCoercionTyCon [TyConApp tc cos]  -- arising from newtypes
216
217 mkSymCoercion (TyVarTy tv) 
218   | isCoVar tv = mkCoercion symCoercionTyCon [TyVarTy tv]
219   | otherwise  = TyVarTy tv     -- Reflexive
220
221 -------------------------------
222 -- ToDo: we should be cleverer about transitivity
223 mkTransCoercion g1 g2   -- sym g `trans` g = id
224   | (t1,_) <- coercionKind g1
225   , (_,t2) <- coercionKind g2
226   , t1 `coreEqType` t2 
227   = t1  
228
229   | otherwise
230   = mkCoercion transCoercionTyCon [g1, g2]
231
232
233 -------------------------------
234 -- Smart constructors for left and right
235 mkLeftCoercion co 
236   | Just (co', _) <- splitAppCoercion_maybe co = co'
237   | otherwise = mkCoercion leftCoercionTyCon [co]
238
239 mkRightCoercion  co      
240   | Just (_, co2) <- splitAppCoercion_maybe co = co2
241   | otherwise = mkCoercion rightCoercionTyCon [co]
242
243 mkRightCoercions :: Int -> Coercion -> [Coercion]
244 mkRightCoercions n co
245   = go n co []
246   where
247     go n co acc 
248        | n > 0
249        = case splitAppCoercion_maybe co of
250           Just (co1,co2) -> go (n-1) co1 (co2:acc)
251           Nothing        -> go (n-1) (mkCoercion leftCoercionTyCon [co]) (mkCoercion rightCoercionTyCon [co]:acc)
252        | otherwise
253        = acc
254
255 mkInstCoercion co ty
256   | Just (tv,co') <- splitForAllTy_maybe co
257   = substTyWith [tv] [ty] co'   -- (forall a.co) @ ty  -->  co[ty/a]
258   | otherwise
259   = mkCoercion instCoercionTyCon  [co, ty]
260
261 mkInstsCoercion co tys = foldl mkInstCoercion co tys
262
263 {-
264 splitSymCoercion_maybe :: Coercion -> Maybe Coercion
265 splitSymCoercion_maybe (TyConApp tc [co]) = 
266   if tc `hasKey` symCoercionTyConKey
267   then Just co
268   else Nothing
269 splitSymCoercion_maybe co = Nothing
270 -}
271
272 splitAppCoercion_maybe :: Coercion -> Maybe (Coercion, Coercion)
273 -- Splits a coercion application, being careful *not* to split (left c), etc
274 -- which are really sytactic constructs, not applications
275 splitAppCoercion_maybe co  | Just co' <- coreView co = splitAppCoercion_maybe co'
276 splitAppCoercion_maybe (FunTy ty1 ty2)   = Just (TyConApp funTyCon [ty1], ty2)
277 splitAppCoercion_maybe (AppTy ty1 ty2)   = Just (ty1, ty2)
278 splitAppCoercion_maybe (TyConApp tc tys) 
279    | not (isCoercionTyCon tc)
280    = case snocView tys of
281        Just (tys', ty') -> Just (TyConApp tc tys', ty')
282        Nothing          -> Nothing
283 splitAppCoercion_maybe _ = Nothing
284
285 {-
286 splitTransCoercion_maybe :: Coercion -> Maybe (Coercion, Coercion)
287 splitTransCoercion_maybe (TyConApp tc [ty1, ty2]) 
288  = if tc `hasKey` transCoercionTyConKey then
289        Just (ty1, ty2)
290    else
291        Nothing
292 splitTransCoercion_maybe other = Nothing
293
294 splitInstCoercion_maybe :: Coercion -> Maybe (Coercion, Type)
295 splitInstCoercion_maybe (TyConApp tc [ty1, ty2])
296  = if tc `hasKey` instCoercionTyConKey then
297        Just (ty1, ty2)
298     else
299        Nothing
300 splitInstCoercion_maybe other = Nothing
301
302 splitLeftCoercion_maybe :: Coercion -> Maybe Coercion
303 splitLeftCoercion_maybe (TyConApp tc [co])
304  = if tc `hasKey` leftCoercionTyConKey then
305        Just co
306    else
307        Nothing
308 splitLeftCoercion_maybe other = Nothing
309
310 splitRightCoercion_maybe :: Coercion -> Maybe Coercion
311 splitRightCoercion_maybe (TyConApp tc [co])
312  = if tc `hasKey` rightCoercionTyConKey then
313        Just co
314    else
315        Nothing
316 splitRightCoercion_maybe other = Nothing
317 -}
318
319 -- Unsafe coercion is not safe, it is used when we know we are dealing with
320 -- bottom, which is one case in which it is safe.  It is also used to 
321 -- implement the unsafeCoerce# primitive.
322 mkUnsafeCoercion :: Type -> Type -> Coercion
323 mkUnsafeCoercion ty1 ty2 
324   = mkCoercion unsafeCoercionTyCon [ty1, ty2]
325
326
327 -- See note [Newtype coercions] in TyCon
328 mkNewTypeCoercion :: Name -> TyCon -> [TyVar] -> Type -> TyCon
329 mkNewTypeCoercion name tycon tvs rhs_ty
330   = mkCoercionTyCon name co_con_arity rule
331   where
332     co_con_arity = length tvs
333
334     rule args = ASSERT( co_con_arity == length args )
335                 (TyConApp tycon args, substTyWith tvs args rhs_ty)
336
337 -- Coercion identifying a data/newtype/synonym representation type and its 
338 -- family instance.  It has the form `Co tvs :: F ts :=: R tvs', where `Co' is 
339 -- the coercion tycon built here, `F' the family tycon and `R' the (derived)
340 -- representation tycon.
341 --
342 mkFamInstCoercion :: Name       -- unique name for the coercion tycon
343                   -> [TyVar]    -- type parameters of the coercion (`tvs')
344                   -> TyCon      -- family tycon (`F')
345                   -> [Type]     -- type instance (`ts')
346                   -> TyCon      -- representation tycon (`R')
347                   -> TyCon      -- => coercion tycon (`Co')
348 mkFamInstCoercion name tvs family instTys rep_tycon
349   = mkCoercionTyCon name coArity rule
350   where
351     coArity = length tvs
352     rule args = (substTyWith tvs args $              -- with sigma = [tys/tvs],
353                    TyConApp family instTys,          --       sigma (F ts)
354                  TyConApp rep_tycon args)            --   :=: R tys
355
356 --------------------------------------
357 -- Coercion Type Constructors...
358
359 -- Example.  The coercion ((sym c) (sym d) (sym e))
360 -- will be represented by (TyConApp sym [c, sym d, sym e])
361 -- If sym c :: p1=q1
362 --    sym d :: p2=q2
363 --    sym e :: p3=q3
364 -- then ((sym c) (sym d) (sym e)) :: (p1 p2 p3)=(q1 q2 q3)
365
366 symCoercionTyCon, transCoercionTyCon, leftCoercionTyCon, rightCoercionTyCon, instCoercionTyCon, unsafeCoercionTyCon :: TyCon
367 -- Each coercion TyCon is built with the special CoercionTyCon record and
368 -- carries its own kinding rule.  Such CoercionTyCons must be fully applied
369 -- by any TyConApp in which they are applied, however they may also be over
370 -- applied (see example above) and the kinding function must deal with this.
371 symCoercionTyCon = 
372   mkCoercionTyCon symCoercionTyConName 1 flipCoercionKindOf
373   where
374     flipCoercionKindOf (co:rest) = ASSERT( null rest ) (ty2, ty1)
375         where
376           (ty1, ty2) = coercionKind co
377
378 transCoercionTyCon = 
379   mkCoercionTyCon transCoercionTyConName 2 composeCoercionKindsOf
380   where
381     composeCoercionKindsOf (co1:co2:rest)
382       = ASSERT( null rest )
383         WARN( not (r1 `coreEqType` a2), 
384               text "Strange! Type mismatch in trans coercion, probably a bug"
385               $$
386               ppr r1 <+> text "=/=" <+> ppr a2)
387         (a1, r2)
388       where
389         (a1, r1) = coercionKind co1
390         (a2, r2) = coercionKind co2 
391
392 leftCoercionTyCon =
393   mkCoercionTyCon leftCoercionTyConName 1 leftProjectCoercionKindOf
394   where
395     leftProjectCoercionKindOf (co:rest) = ASSERT( null rest ) (ty1, ty2)
396       where
397         (ty1,ty2) = fst (splitCoercionKindOf co)
398
399 rightCoercionTyCon =
400   mkCoercionTyCon rightCoercionTyConName 1 rightProjectCoercionKindOf
401   where
402     rightProjectCoercionKindOf (co:rest) = ASSERT( null rest ) (ty1, ty2)
403       where
404         (ty1,ty2) = snd (splitCoercionKindOf co)
405
406 splitCoercionKindOf :: Type -> ((Type,Type), (Type,Type))
407 -- Helper for left and right.  Finds coercion kind of its input and
408 -- returns the left and right projections of the coercion...
409 --
410 -- if c :: t1 s1 :=: t2 s2 then splitCoercionKindOf c = ((t1, t2), (s1, s2))
411 splitCoercionKindOf co
412   | Just (ty1, ty2) <- splitCoercionKind_maybe (coercionKindPredTy co)
413   , Just (ty_fun1, ty_arg1) <- splitAppTy_maybe ty1
414   , Just (ty_fun2, ty_arg2) <- splitAppTy_maybe ty2
415   = ((ty_fun1, ty_fun2),(ty_arg1, ty_arg2))
416 splitCoercionKindOf co 
417   = pprPanic "Coercion.splitCoercionKindOf" 
418              (ppr co $$ ppr (coercionKindPredTy co))
419
420 instCoercionTyCon 
421   =  mkCoercionTyCon instCoercionTyConName 2 instCoercionKind
422   where
423     instantiateCo t s =
424       let Just (tv, ty) = splitForAllTy_maybe t in
425       substTyWith [tv] [s] ty
426
427     instCoercionKind (co1:ty:rest) = ASSERT( null rest )
428                                      (instantiateCo t1 ty, instantiateCo t2 ty)
429       where (t1, t2) = coercionKind co1
430
431 unsafeCoercionTyCon 
432   = mkCoercionTyCon unsafeCoercionTyConName 2 unsafeCoercionKind
433   where
434    unsafeCoercionKind (ty1:ty2:rest) = ASSERT( null rest ) (ty1,ty2) 
435         
436 --------------------------------------
437 -- ...and their names
438
439 mkCoConName :: FS.FastString -> Unique -> TyCon -> Name
440 mkCoConName occ key coCon = mkWiredInName gHC_PRIM (mkOccNameFS tcName occ)
441                             key (ATyCon coCon) BuiltInSyntax
442
443 transCoercionTyConName, symCoercionTyConName, leftCoercionTyConName, rightCoercionTyConName, instCoercionTyConName, unsafeCoercionTyConName :: Name
444
445 transCoercionTyConName = mkCoConName FSLIT("trans") transCoercionTyConKey transCoercionTyCon
446 symCoercionTyConName   = mkCoConName FSLIT("sym") symCoercionTyConKey symCoercionTyCon
447 leftCoercionTyConName  = mkCoConName FSLIT("left") leftCoercionTyConKey leftCoercionTyCon
448 rightCoercionTyConName = mkCoConName FSLIT("right") rightCoercionTyConKey rightCoercionTyCon
449 instCoercionTyConName  = mkCoConName FSLIT("inst") instCoercionTyConKey instCoercionTyCon
450 unsafeCoercionTyConName = mkCoConName FSLIT("CoUnsafe") unsafeCoercionTyConKey unsafeCoercionTyCon
451
452
453
454 instNewTyCon_maybe :: TyCon -> [Type] -> Maybe (Type, CoercionI)
455 -- instNewTyCon_maybe T ts
456 --      = Just (rep_ty, co)     if   co : T ts ~ rep_ty
457 instNewTyCon_maybe tc tys
458   | Just (tvs, ty, mb_co_tc) <- unwrapNewTyCon_maybe tc
459   = ASSERT( tys `lengthIs` tyConArity tc )
460     Just (substTyWith tvs tys ty, 
461           case mb_co_tc of
462            Nothing    -> IdCo
463            Just co_tc -> ACo (mkTyConApp co_tc tys))
464   | otherwise
465   = Nothing
466
467 -- this is here to avoid module loops
468 splitNewTypeRepCo_maybe :: Type -> Maybe (Type, Coercion)  
469 -- Sometimes we want to look through a newtype and get its associated coercion
470 -- It only strips *one layer* off, so the caller will usually call itself recursively
471 -- Only applied to types of kind *, hence the newtype is always saturated
472 --    splitNewTypeRepCo_maybe ty
473 --      = Just (ty', co)  if   co : ty ~ ty'
474 -- Returns Nothing for non-newtypes or fully-transparent newtypes
475 splitNewTypeRepCo_maybe ty 
476   | Just ty' <- coreView ty = splitNewTypeRepCo_maybe ty'
477 splitNewTypeRepCo_maybe (TyConApp tc tys)
478   | Just (ty', coi) <- instNewTyCon_maybe tc tys
479   = case coi of
480         ACo co -> Just (ty', co)
481         IdCo   -> panic "splitNewTypeRepCo_maybe"
482                         -- This case handled by coreView
483 splitNewTypeRepCo_maybe _
484   = Nothing
485 \end{code}
486
487
488 --------------------------------------
489 -- CoercionI smart constructors
490 --      lifted smart constructors of ordinary coercions
491
492 \begin{code}
493         -- CoercionI is either 
494         --      (a) proper coercion
495         --      (b) the identity coercion
496 data CoercionI = IdCo | ACo Coercion
497
498 isIdentityCoercion :: CoercionI -> Bool
499 isIdentityCoercion IdCo = True
500 isIdentityCoercion _    = False
501
502 allIdCos :: [CoercionI] -> Bool
503 allIdCos = all isIdentityCoercion
504
505 zipCoArgs :: [CoercionI] -> [Type] -> [Coercion]
506 zipCoArgs cois tys = zipWith fromCoI cois tys
507
508 fromCoI :: CoercionI -> Type -> Type
509 fromCoI IdCo ty     = ty        -- Identity coercion represented 
510 fromCoI (ACo co) _  = co        --      by the type itself
511
512 mkSymCoI :: CoercionI -> CoercionI
513 mkSymCoI IdCo = IdCo
514 mkSymCoI (ACo co) = ACo $ mkCoercion symCoercionTyCon [co] 
515                                 -- the smart constructor
516                                 -- is too smart with tyvars
517
518 mkTransCoI :: CoercionI -> CoercionI -> CoercionI
519 mkTransCoI IdCo aco = aco
520 mkTransCoI aco IdCo = aco
521 mkTransCoI (ACo co1) (ACo co2) = ACo $ mkTransCoercion co1 co2
522
523 mkTyConAppCoI :: TyCon -> [Type] -> [CoercionI] -> CoercionI
524 mkTyConAppCoI tyCon tys cois
525   | allIdCos cois = IdCo
526   | otherwise     = ACo (TyConApp tyCon (zipCoArgs cois tys))
527
528 mkAppTyCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI
529 mkAppTyCoI _   IdCo _   IdCo = IdCo
530 mkAppTyCoI ty1 coi1 ty2 coi2 =
531         ACo $ AppTy (fromCoI coi1 ty1) (fromCoI coi2 ty2)
532
533 mkFunTyCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI
534 mkFunTyCoI _   IdCo _   IdCo = IdCo
535 mkFunTyCoI ty1 coi1 ty2 coi2 =
536         ACo $ FunTy (fromCoI coi1 ty1) (fromCoI coi2 ty2)
537
538 mkNoteTyCoI :: TyNote -> CoercionI -> CoercionI
539 mkNoteTyCoI _ IdCo = IdCo
540 mkNoteTyCoI note (ACo co) = ACo $ NoteTy note co
541
542 mkForAllTyCoI :: TyVar -> CoercionI -> CoercionI
543 mkForAllTyCoI _ IdCo = IdCo
544 mkForAllTyCoI tv (ACo co) = ACo $ ForAllTy tv co
545
546 fromACo :: CoercionI -> Coercion
547 fromACo (ACo co) = co
548
549 mkClassPPredCoI :: Class -> [Type] -> [CoercionI] -> CoercionI
550 -- mkClassPPredCoI cls tys cois = coi
551 --    coi : PredTy (cls tys) ~ predTy (cls (tys `cast` cois))
552 mkClassPPredCoI cls tys cois 
553   | allIdCos cois = IdCo
554   | otherwise     = ACo $ PredTy $ ClassP cls (zipCoArgs cois tys)
555
556 mkIParamPredCoI :: (IPName Name) -> CoercionI -> CoercionI 
557 -- Similar invariant to mkclassPPredCoI
558 mkIParamPredCoI _   IdCo     = IdCo
559 mkIParamPredCoI ipn (ACo co) = ACo $ PredTy $ IParam ipn co
560
561 mkEqPredCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI
562 -- Similar invariant to mkclassPPredCoI
563 mkEqPredCoI _    IdCo     _   IdCo      = IdCo
564 mkEqPredCoI ty1  IdCo     _   (ACo co2) = ACo $ PredTy $ EqPred ty1 co2
565 mkEqPredCoI _   (ACo co1) ty2 coi2      = ACo $ PredTy $ EqPred co1 (fromCoI coi2 ty2)
566 \end{code}
567