more aggressive optimization of coercion terms
[ghc.git] / compiler / types / Coercion.lhs
1 T%
2 % (c) The University of Glasgow 2006
3 %
4
5 \begin{code}
6 {-# OPTIONS -fno-warn-incomplete-patterns #-}
7 -- The above warning supression flag is a temporary kludge.
8 -- While working on this module you are encouraged to remove it and fix
9 -- any warnings in the module. See
10 --     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings
11 -- for details
12
13 -- | Module for type coercions, as used in System FC. See 'CoreSyn.Expr' for
14 -- more on System FC and how coercions fit into it.
15 --
16 -- Coercions are represented as types, and their kinds tell what types the 
17 -- coercion works on. The coercion kind constructor is a special TyCon that must always be saturated, like so:
18 --
19 -- > typeKind (symCoercion type) :: TyConApp CoercionTyCon{...} [type, type]
20 module Coercion (
21         -- * Main data type
22         Coercion,
23  
24         mkCoKind, mkReflCoKind, coVarKind,
25         coercionKind, coercionKinds, isIdentityCoercion,
26
27         -- ** Equality predicates
28         isEqPred, mkEqPred, getEqPredTys, isEqPredTy,  
29
30         -- ** Coercion transformations
31         mkCoercion,
32         mkSymCoercion, mkTransCoercion,
33         mkLeftCoercion, mkRightCoercion, mkRightCoercions,
34         mkInstCoercion, mkAppCoercion, mkTyConCoercion, mkFunCoercion,
35         mkForAllCoercion, mkInstsCoercion, mkUnsafeCoercion,
36         mkNewTypeCoercion, mkFamInstCoercion, mkAppsCoercion,
37         mkCsel1Coercion, mkCsel2Coercion, mkCselRCoercion, 
38
39         splitNewTypeRepCo_maybe, instNewTyCon_maybe, decomposeCo,
40
41         unsafeCoercionTyCon, symCoercionTyCon,
42         transCoercionTyCon, leftCoercionTyCon, 
43         rightCoercionTyCon, instCoercionTyCon, -- needed by TysWiredIn
44         csel1CoercionTyCon, csel2CoercionTyCon, cselRCoercionTyCon, 
45
46         -- ** Optimisation
47         optCoercion,
48
49         -- ** Comparison
50         coreEqCoercion,
51
52         -- * CoercionI
53         CoercionI(..),
54         isIdentityCoI,
55         mkSymCoI, mkTransCoI, 
56         mkTyConAppCoI, mkAppTyCoI, mkFunTyCoI,
57         mkForAllTyCoI,
58         fromCoI, fromACo,
59         mkClassPPredCoI, mkIParamPredCoI, mkEqPredCoI
60
61        ) where 
62
63 #include "HsVersions.h"
64
65 import TypeRep
66 import Type
67 import TyCon
68 import Class
69 import Var
70 import Name
71 import PrelNames
72 import Util
73 import BasicTypes
74 import Outputable
75 import FastString
76
77 -- | A 'Coercion' represents a 'Type' something should be coerced to.
78 type Coercion     = Type
79
80 -- | A 'CoercionKind' is always of form @ty1 ~ ty2@ and indicates the
81 -- types that a 'Coercion' will work on.
82 type CoercionKind = Kind
83
84 ------------------------------
85
86 -- | This breaks a 'Coercion' with 'CoercionKind' @T A B C ~ T D E F@ into
87 -- a list of 'Coercion's of kinds @A ~ D@, @B ~ E@ and @E ~ F@. Hence:
88 --
89 -- > decomposeCo 3 c = [right (left (left c)), right (left c), right c]
90 decomposeCo :: Arity -> Coercion -> [Coercion]
91 decomposeCo n co
92   = go n co []
93   where
94     go 0 _  cos = cos
95     go n co cos = go (n-1) (mkLeftCoercion co)
96                            (mkRightCoercion co : cos)
97
98 ------------------------------
99
100 -------------------------------------------------------
101 -- and some coercion kind stuff
102
103 coVarKind :: CoVar -> (Type,Type) 
104 -- c :: t1 ~ t2
105 coVarKind cv = splitCoVarKind (tyVarKind cv)
106
107 -- | Take a 'CoercionKind' apart into the two types it relates: see also 'mkCoKind'.
108 -- Panics if the argument is not a valid 'CoercionKind'
109 splitCoVarKind :: Kind -> (Type, Type)
110 splitCoVarKind co | Just co' <- kindView co = splitCoVarKind co'
111 splitCoVarKind (PredTy (EqPred ty1 ty2))    = (ty1, ty2)
112
113 -- | Makes a 'CoercionKind' from two types: the types whose equality is proven by the relevant 'Coercion'
114 mkCoKind :: Type -> Type -> CoercionKind
115 mkCoKind ty1 ty2 = PredTy (EqPred ty1 ty2)
116
117 -- | (mkCoPredTy s t r) produces the type:   (s~t) => r
118 mkCoPredTy :: Type -> Type -> Type -> Type
119 mkCoPredTy s t r = ForAllTy (mkWildCoVar (mkCoKind s t)) r
120
121 -- | Tests whether a type is just a type equality predicate
122 isEqPredTy :: Type -> Bool
123 isEqPredTy (PredTy pred) = isEqPred pred
124 isEqPredTy _             = False
125
126 -- | Creates a type equality predicate
127 mkEqPred :: (Type, Type) -> PredType
128 mkEqPred (ty1, ty2) = EqPred ty1 ty2
129
130 -- | Splits apart a type equality predicate, if the supplied 'PredType' is one.
131 -- Panics otherwise
132 getEqPredTys :: PredType -> (Type,Type)
133 getEqPredTys (EqPred ty1 ty2) = (ty1, ty2)
134 getEqPredTys other            = pprPanic "getEqPredTys" (ppr other)
135
136 -- | Create a reflexive 'CoercionKind' that asserts that a type can be coerced to itself
137 mkReflCoKind :: Type -> CoercionKind
138 mkReflCoKind ty = mkCoKind ty ty
139
140 -- | If it is the case that
141 --
142 -- > c :: (t1 ~ t2)
143 --
144 -- i.e. the kind of @c@ is a 'CoercionKind' relating @t1@ and @t2@, then @coercionKind c = (t1, t2)@.
145 coercionKind :: Coercion -> (Type, Type)
146 coercionKind ty@(TyVarTy a) | isCoVar a = coVarKind a
147                             | otherwise = (ty, ty)
148 coercionKind (AppTy ty1 ty2) 
149   = let (t1, t2) = coercionKind ty1
150         (s1, s2) = coercionKind ty2 in
151     (mkAppTy t1 s1, mkAppTy t2 s2)
152 coercionKind (TyConApp tc args)
153   | Just (ar, rule) <- isCoercionTyCon_maybe tc 
154     -- CoercionTyCons carry their kinding rule, so we use it here
155   = ASSERT( length args >= ar ) -- Always saturated
156     let (ty1,ty2)    = rule (take ar args)      -- Apply the rule to the right number of args
157         (tys1, tys2) = coercionKinds (drop ar args)
158     in (mkAppTys ty1 tys1, mkAppTys ty2 tys2)
159
160   | otherwise
161   = let (lArgs, rArgs) = coercionKinds args in
162     (TyConApp tc lArgs, TyConApp tc rArgs)
163 coercionKind (FunTy ty1 ty2) 
164   = let (t1, t2) = coercionKind ty1
165         (s1, s2) = coercionKind ty2 in
166     (mkFunTy t1 s1, mkFunTy t2 s2)
167
168 coercionKind (ForAllTy tv ty)
169   | isCoVar tv
170 --     c1 :: s1~s2  c2 :: t1~t2   c3 :: r1~r2
171 --    ----------------------------------------------
172 --    c1~c2 => c3  ::  (s1~t1) => r1 ~ (s2~t2) => r2
173 --      or
174 --    forall (_:c1~c2)
175   = let (c1,c2) = coVarKind tv
176         (s1,s2) = coercionKind c1
177         (t1,t2) = coercionKind c2
178         (r1,r2) = coercionKind ty
179     in
180     (mkCoPredTy s1 t1 r1, mkCoPredTy s2 t2 r2)
181
182   | otherwise
183 --     c1 :: s1~s2  c2 :: t1~t2   c3 :: r1~r2
184 --   ----------------------------------------------
185 --    forall a:k. c :: forall a:k. t1 ~ forall a:k. t2
186   = let (ty1, ty2) = coercionKind ty in
187     (ForAllTy tv ty1, ForAllTy tv ty2)
188
189 coercionKind (PredTy (EqPred c1 c2)) 
190   = pprTrace "coercionKind" (pprEqPred (c1,c2)) $
191     let k1 = coercionKindPredTy c1
192         k2 = coercionKindPredTy c2 in
193     (k1,k2)
194   -- These should not show up in coercions at all
195   -- becuase they are in the form of for-alls
196   where
197     coercionKindPredTy c = let (t1, t2) = coercionKind c in mkCoKind t1 t2
198
199
200
201 coercionKind (PredTy (ClassP cl args)) 
202   = let (lArgs, rArgs) = coercionKinds args in
203     (PredTy (ClassP cl lArgs), PredTy (ClassP cl rArgs))
204 coercionKind (PredTy (IParam name ty))
205   = let (ty1, ty2) = coercionKind ty in
206     (PredTy (IParam name ty1), PredTy (IParam name ty2))
207
208 -- | Apply 'coercionKind' to multiple 'Coercion's
209 coercionKinds :: [Coercion] -> ([Type], [Type])
210 coercionKinds tys = unzip $ map coercionKind tys
211
212 -------------------------------------
213 isIdentityCoercion :: Coercion -> Bool
214 isIdentityCoercion co  
215   = case coercionKind co of
216        (t1,t2) -> t1 `coreEqType` t2
217 \end{code}
218
219 %************************************************************************
220 %*                                                                      *
221             Building coercions
222 %*                                                                      *
223 %************************************************************************
224
225 Coercion kind and type mk's (make saturated TyConApp CoercionTyCon{...} args)
226
227 \begin{code}
228 -- | Make a coercion from the specified coercion 'TyCon' and the 'Type' arguments to
229 -- that coercion. Try to use the @mk*Coercion@ family of functions instead of using this function
230 -- if possible
231 mkCoercion :: TyCon -> [Type] -> Coercion
232 mkCoercion coCon args = ASSERT( tyConArity coCon == length args ) 
233                         TyConApp coCon args
234
235 -- | Apply a 'Coercion' to another 'Coercion', which is presumably a
236 -- 'Coercion' constructor of some kind
237 mkAppCoercion :: Coercion -> Coercion -> Coercion
238 mkAppCoercion co1 co2 = mkAppTy co1 co2
239
240 -- | Applies multiple 'Coercion's to another 'Coercion', from left to right.
241 -- See also 'mkAppCoercion'
242 mkAppsCoercion :: Coercion -> [Coercion] -> Coercion
243 mkAppsCoercion co1 tys = foldl mkAppTy co1 tys
244
245 -- | Apply a type constructor to a list of coercions.
246 mkTyConCoercion :: TyCon -> [Coercion] -> Coercion
247 mkTyConCoercion con cos = mkTyConApp con cos
248
249 -- | Make a function 'Coercion' between two other 'Coercion's
250 mkFunCoercion :: Coercion -> Coercion -> Coercion
251 mkFunCoercion co1 co2 = mkFunTy co1 co2
252
253 -- | Make a 'Coercion' which binds a variable within an inner 'Coercion'
254 mkForAllCoercion :: Var -> Coercion -> Coercion
255 -- note that a TyVar should be used here, not a CoVar (nor a TcTyVar)
256 mkForAllCoercion tv  co  = ASSERT ( isTyVar tv ) mkForAllTy tv co
257
258
259 -------------------------------
260
261 mkSymCoercion :: Coercion -> Coercion
262 -- ^ Create a symmetric version of the given 'Coercion' that asserts equality
263 -- between the same types but in the other "direction", so a kind of @t1 ~ t2@ 
264 -- becomes the kind @t2 ~ t1@.
265 --
266 -- This function attempts to simplify the generated 'Coercion' by removing 
267 -- redundant applications of @sym@. This is done by pushing this new @sym@ 
268 -- down into the 'Coercion' and exploiting the fact that @sym (sym co) = co@.
269 mkSymCoercion co      
270   | Just co' <- coreView co = mkSymCoercion co'
271
272 mkSymCoercion (ForAllTy tv ty)  = ForAllTy tv (mkSymCoercion ty)
273 mkSymCoercion (AppTy co1 co2)   = AppTy (mkSymCoercion co1) (mkSymCoercion co2)
274 mkSymCoercion (FunTy co1 co2)   = FunTy (mkSymCoercion co1) (mkSymCoercion co2)
275
276 mkSymCoercion (TyConApp tc cos) 
277   | not (isCoercionTyCon tc) = mkTyConApp tc (map mkSymCoercion cos)
278
279 mkSymCoercion (TyConApp tc [co]) 
280   | tc `hasKey` symCoercionTyConKey   = co    -- sym (sym co) --> co
281   | tc `hasKey` leftCoercionTyConKey  = mkLeftCoercion (mkSymCoercion co)
282   | tc `hasKey` rightCoercionTyConKey = mkRightCoercion (mkSymCoercion co)
283
284 mkSymCoercion (TyConApp tc [co1,co2]) 
285   | tc `hasKey` transCoercionTyConKey
286      -- sym (co1 `trans` co2) --> (sym co2) `trans (sym co2)
287      -- Note reversal of arguments!
288   = mkTransCoercion (mkSymCoercion co2) (mkSymCoercion co1)
289
290   | tc `hasKey` instCoercionTyConKey
291      -- sym (co @ ty) --> (sym co) @ ty
292      -- Note: sym is not applied to 'ty'
293   = mkInstCoercion (mkSymCoercion co1) co2
294
295 mkSymCoercion (TyConApp tc cos)         -- Other coercion tycons, such as those
296   = mkCoercion symCoercionTyCon [TyConApp tc cos]  -- arising from newtypes
297
298 mkSymCoercion (TyVarTy tv) 
299   | isCoVar tv = mkCoercion symCoercionTyCon [TyVarTy tv]
300   | otherwise  = TyVarTy tv     -- Reflexive
301
302 -------------------------------
303 -- ToDo: we should be cleverer about transitivity
304
305 mkTransCoercion :: Coercion -> Coercion -> Coercion
306 -- ^ Create a new 'Coercion' by exploiting transitivity on the two given 'Coercion's.
307 -- 
308 -- This function attempts to simplify the generated 'Coercion' by exploiting the fact that
309 -- @sym g `trans` g = id@.
310 mkTransCoercion g1 g2   -- sym g `trans` g = id
311   | (t1,_) <- coercionKind g1
312   , (_,t2) <- coercionKind g2
313   , t1 `coreEqType` t2 
314   = t1  
315
316   | otherwise
317   = mkCoercion transCoercionTyCon [g1, g2]
318
319
320 -------------------------------
321 -- Smart constructors for left and right
322
323 mkLeftCoercion :: Coercion -> Coercion
324 -- ^ From an application 'Coercion' build a 'Coercion' that asserts the equality of 
325 -- the "functions" on either side of the type equality. So if @c@ has kind @f x ~ g y@ then:
326 --
327 -- > mkLeftCoercion c :: f ~ g
328 mkLeftCoercion co 
329   | Just (co', _) <- splitAppCoercion_maybe co = co'
330   | otherwise = mkCoercion leftCoercionTyCon [co]
331
332 mkRightCoercion :: Coercion -> Coercion
333 -- ^ From an application 'Coercion' build a 'Coercion' that asserts the equality of 
334 -- the "arguments" on either side of the type equality. So if @c@ has kind @f x ~ g y@ then:
335 --
336 -- > mkLeftCoercion c :: x ~ y
337 mkRightCoercion  co      
338   | Just (_, co2) <- splitAppCoercion_maybe co = co2
339   | otherwise = mkCoercion rightCoercionTyCon [co]
340
341 mkRightCoercions :: Int -> Coercion -> [Coercion]
342 -- ^ As 'mkRightCoercion', but finds the 'Coercion's available on the right side of @n@
343 -- nested application 'Coercion's, manufacturing new left or right cooercions as necessary
344 -- if suffficiently many are not directly available.
345 mkRightCoercions n co
346   = go n co []
347   where
348     go n co acc 
349        | n > 0
350        = case splitAppCoercion_maybe co of
351           Just (co1,co2) -> go (n-1) co1 (co2:acc)
352           Nothing        -> go (n-1) (mkCoercion leftCoercionTyCon [co]) (mkCoercion rightCoercionTyCon [co]:acc)
353        | otherwise
354        = acc
355
356
357 mkCsel1Coercion, mkCsel2Coercion, mkCselRCoercion :: Coercion -> Coercion
358 mkCsel1Coercion co = mkCoercion csel1CoercionTyCon [co]
359 mkCsel2Coercion co = mkCoercion csel2CoercionTyCon [co]
360 mkCselRCoercion co = mkCoercion cselRCoercionTyCon [co]
361
362 -------------------------------
363 mkInstCoercion :: Coercion -> Type -> Coercion
364 -- ^ Instantiates a 'Coercion' with a 'Type' argument. If possible, it immediately performs
365 -- the resulting beta-reduction, otherwise it creates a suspended instantiation.
366 mkInstCoercion co ty
367   | Just (tv,co') <- splitForAllTy_maybe co
368   = substTyWith [tv] [ty] co'   -- (forall a.co) @ ty  -->  co[ty/a]
369   | otherwise
370   = mkCoercion instCoercionTyCon  [co, ty]
371
372 mkInstsCoercion :: Coercion -> [Type] -> Coercion
373 -- ^ As 'mkInstCoercion', but instantiates the coercion with a number of type arguments, left-to-right
374 mkInstsCoercion co tys = foldl mkInstCoercion co tys
375
376 {-
377 splitSymCoercion_maybe :: Coercion -> Maybe Coercion
378 splitSymCoercion_maybe (TyConApp tc [co]) = 
379   if tc `hasKey` symCoercionTyConKey
380   then Just co
381   else Nothing
382 splitSymCoercion_maybe co = Nothing
383 -}
384
385 splitAppCoercion_maybe :: Coercion -> Maybe (Coercion, Coercion)
386 -- ^ Splits a coercion application, being careful *not* to split @left c@ etc.
387 -- This is because those are really syntactic constructs, not applications
388 splitAppCoercion_maybe co  | Just co' <- coreView co = splitAppCoercion_maybe co'
389 splitAppCoercion_maybe (FunTy ty1 ty2)   = Just (TyConApp funTyCon [ty1], ty2)
390 splitAppCoercion_maybe (AppTy ty1 ty2)   = Just (ty1, ty2)
391 splitAppCoercion_maybe (TyConApp tc tys) 
392    | not (isCoercionTyCon tc)
393    = case snocView tys of
394        Just (tys', ty') -> Just (TyConApp tc tys', ty')
395        Nothing          -> Nothing
396 splitAppCoercion_maybe _ = Nothing
397
398 {-
399 splitTransCoercion_maybe :: Coercion -> Maybe (Coercion, Coercion)
400 splitTransCoercion_maybe (TyConApp tc [ty1, ty2]) 
401  = if tc `hasKey` transCoercionTyConKey then
402        Just (ty1, ty2)
403    else
404        Nothing
405 splitTransCoercion_maybe other = Nothing
406
407 splitInstCoercion_maybe :: Coercion -> Maybe (Coercion, Type)
408 splitInstCoercion_maybe (TyConApp tc [ty1, ty2])
409  = if tc `hasKey` instCoercionTyConKey then
410        Just (ty1, ty2)
411     else
412        Nothing
413 splitInstCoercion_maybe other = Nothing
414
415 splitLeftCoercion_maybe :: Coercion -> Maybe Coercion
416 splitLeftCoercion_maybe (TyConApp tc [co])
417  = if tc `hasKey` leftCoercionTyConKey then
418        Just co
419    else
420        Nothing
421 splitLeftCoercion_maybe other = Nothing
422
423 splitRightCoercion_maybe :: Coercion -> Maybe Coercion
424 splitRightCoercion_maybe (TyConApp tc [co])
425  = if tc `hasKey` rightCoercionTyConKey then
426        Just co
427    else
428        Nothing
429 splitRightCoercion_maybe other = Nothing
430 -}
431
432 -- | Manufacture a coercion from this air. Needless to say, this is not usually safe,
433 -- but it is used when we know we are dealing with bottom, which is one case in which 
434 -- it is safe.  This is also used implement the @unsafeCoerce#@ primitive.
435 mkUnsafeCoercion :: Type -> Type -> Coercion
436 mkUnsafeCoercion ty1 ty2 
437   = mkCoercion unsafeCoercionTyCon [ty1, ty2]
438
439
440 -- See note [Newtype coercions] in TyCon
441
442 -- | Create a coercion suitable for the given 'TyCon'. The 'Name' should be that of a
443 -- new coercion 'TyCon', the 'TyVar's the arguments expected by the @newtype@ and the
444 -- type the appropriate right hand side of the @newtype@, with the free variables
445 -- a subset of those 'TyVar's.
446 mkNewTypeCoercion :: Name -> TyCon -> [TyVar] -> Type -> TyCon
447 mkNewTypeCoercion name tycon tvs rhs_ty
448   = mkCoercionTyCon name co_con_arity rule
449   where
450     co_con_arity = length tvs
451
452     rule args = ASSERT( co_con_arity == length args )
453                 (TyConApp tycon args, substTyWith tvs args rhs_ty)
454
455 -- | Create a coercion identifying a @data@, @newtype@ or @type@ representation type
456 -- and its family instance.  It has the form @Co tvs :: F ts ~ R tvs@, where @Co@ is 
457 -- the coercion tycon built here, @F@ the family tycon and @R@ the (derived)
458 -- representation tycon.
459 mkFamInstCoercion :: Name       -- ^ Unique name for the coercion tycon
460                   -> [TyVar]    -- ^ Type parameters of the coercion (@tvs@)
461                   -> TyCon      -- ^ Family tycon (@F@)
462                   -> [Type]     -- ^ Type instance (@ts@)
463                   -> TyCon      -- ^ Representation tycon (@R@)
464                   -> TyCon      -- ^ Coercion tycon (@Co@)
465 mkFamInstCoercion name tvs family instTys rep_tycon
466   = mkCoercionTyCon name coArity rule
467   where
468     coArity = length tvs
469     rule args = (substTyWith tvs args $              -- with sigma = [tys/tvs],
470                    TyConApp family instTys,          --       sigma (F ts)
471                  TyConApp rep_tycon args)            --   ~ R tys
472 \end{code}
473
474
475 %************************************************************************
476 %*                                                                      *
477             Coercion Type Constructors
478 %*                                                                      *
479 %************************************************************************
480
481 Example.  The coercion ((sym c) (sym d) (sym e))
482 will be represented by (TyConApp sym [c, sym d, sym e])
483 If sym c :: p1=q1
484    sym d :: p2=q2
485    sym e :: p3=q3
486 then ((sym c) (sym d) (sym e)) :: (p1 p2 p3)=(q1 q2 q3)
487
488 \begin{code}
489 -- | Coercion type constructors: avoid using these directly and instead use 
490 -- the @mk*Coercion@ and @split*Coercion@ family of functions if possible.
491 --
492 -- Each coercion TyCon is built with the special CoercionTyCon record and
493 -- carries its own kinding rule.  Such CoercionTyCons must be fully applied
494 -- by any TyConApp in which they are applied, however they may also be over
495 -- applied (see example above) and the kinding function must deal with this.
496 symCoercionTyCon, transCoercionTyCon, leftCoercionTyCon, 
497   rightCoercionTyCon, instCoercionTyCon, unsafeCoercionTyCon,
498   csel1CoercionTyCon, csel2CoercionTyCon, cselRCoercionTyCon :: TyCon
499
500 symCoercionTyCon = 
501   mkCoercionTyCon symCoercionTyConName 1 flipCoercionKindOf
502   where
503     flipCoercionKindOf (co:rest) = ASSERT( null rest ) (ty2, ty1)
504         where
505           (ty1, ty2) = coercionKind co
506
507 transCoercionTyCon = 
508   mkCoercionTyCon transCoercionTyConName 2 composeCoercionKindsOf
509   where
510     composeCoercionKindsOf (co1:co2:rest)
511       = ASSERT( null rest )
512         WARN( not (r1 `coreEqType` a2),
513               text "Strange! Type mismatch in trans coercion, probably a bug"
514               $$
515               _err_stuff )
516         (a1, r2)
517       where
518         (a1, r1) = coercionKind co1
519         (a2, r2) = coercionKind co2 
520
521         _err_stuff = vcat [ text "co1:" <+> ppr co1
522                           , text "co1 kind left:"  <+> ppr a1
523                           , text "co1 kind right:" <+> ppr r1
524                           , text "co2:" <+> ppr co2
525                           , text "co2 kind left:"  <+> ppr a2
526                           , text "co2 kind right:" <+> ppr r2 ]
527
528 ---------------------------------------------------
529 leftCoercionTyCon  = mkCoercionTyCon leftCoercionTyConName  1 (fst . decompLR)
530 rightCoercionTyCon = mkCoercionTyCon rightCoercionTyConName 1 (snd . decompLR)
531
532 decompLR :: [Type] -> ((Type,Type), (Type,Type))
533 -- Helper for left and right.  Finds coercion kind of its input and
534 -- returns the left and right projections of the coercion...
535 --
536 -- if c :: t1 s1 ~ t2 s2 then splitCoercionKindOf c = ((t1, t2), (s1, s2))
537 decompLR (co : rest)
538   | (ty1, ty2) <- coercionKind co
539   , Just (ty_fun1, ty_arg1) <- splitAppTy_maybe ty1
540   , Just (ty_fun2, ty_arg2) <- splitAppTy_maybe ty2
541   = ASSERT( null rest) 
542     ((ty_fun1, ty_fun2),(ty_arg1, ty_arg2))
543 decompLR cos 
544   = pprPanic "Coercion.decompLR" 
545              (ppr cos $$ vcat (map (pprEqPred .coercionKind) cos))
546
547 ---------------------------------------------------
548 instCoercionTyCon 
549   =  mkCoercionTyCon instCoercionTyConName 2 instCoercionKind
550   where
551     instantiateCo t s =
552       let Just (tv, ty) = splitForAllTy_maybe t in
553       substTyWith [tv] [s] ty
554
555     instCoercionKind (co1:ty:rest) = ASSERT( null rest )
556                                      (instantiateCo t1 ty, instantiateCo t2 ty)
557       where (t1, t2) = coercionKind co1
558
559 ---------------------------------------------------
560 unsafeCoercionTyCon 
561   = mkCoercionTyCon unsafeCoercionTyConName 2 unsafeCoercionKind
562   where
563    unsafeCoercionKind (ty1:ty2:rest) = ASSERT( null rest ) (ty1,ty2) 
564         
565 ---------------------------------------------------
566 -- The csel* family
567 --   If         co :: (s1~t1 => r1) ~ (s2~t2 => r2)
568 -- Then   csel1 co :: s1 ~ s2
569 --        csel2 co :: t1 ~ t2
570 --        cselR co :: r1 ~ r2
571
572 csel1CoercionTyCon = mkCoercionTyCon csel1CoercionTyConName 1 (fstOf3   . decompCsel)
573 csel2CoercionTyCon = mkCoercionTyCon csel2CoercionTyConName 1 (sndOf3   . decompCsel)
574 cselRCoercionTyCon = mkCoercionTyCon cselRCoercionTyConName 1 (thirdOf3 . decompCsel)
575
576 decompCsel :: [Coercion] -> ((Type,Type), (Type,Type), (Type,Type))
577 decompCsel (co : rest)
578   | (ty1,ty2) <- coercionKind co
579   , Just (cv1, r1) <- splitForAllTy_maybe ty1
580   , Just (cv2, r2) <- splitForAllTy_maybe ty2
581   , (s1,t1) <- ASSERT( isCoVar cv1) coVarKind cv1
582   , (s2,t2) <- ASSERT( isCoVar cv1) coVarKind cv2
583   = ASSERT( null rest )
584     ((s1,s2), (t1,t2), (r1,r2))
585 decompCsel other = pprPanic "decompCsel" (ppr other)
586
587 fstOf3   :: (a,b,c) -> a    
588 sndOf3   :: (a,b,c) -> b    
589 thirdOf3 :: (a,b,c) -> c    
590 fstOf3      (a,_,_) =  a
591 sndOf3      (_,b,_) =  b
592 thirdOf3    (_,_,c) =  c
593
594 --------------------------------------
595 -- Their Names
596
597 transCoercionTyConName, symCoercionTyConName, leftCoercionTyConName, 
598    rightCoercionTyConName, instCoercionTyConName, unsafeCoercionTyConName,
599    csel1CoercionTyConName, csel2CoercionTyConName, cselRCoercionTyConName :: Name
600
601 transCoercionTyConName  = mkCoConName (fsLit "trans") transCoercionTyConKey transCoercionTyCon
602 symCoercionTyConName    = mkCoConName (fsLit "sym") symCoercionTyConKey symCoercionTyCon
603 leftCoercionTyConName   = mkCoConName (fsLit "left") leftCoercionTyConKey leftCoercionTyCon
604 rightCoercionTyConName  = mkCoConName (fsLit "right") rightCoercionTyConKey rightCoercionTyCon
605 instCoercionTyConName   = mkCoConName (fsLit "inst") instCoercionTyConKey instCoercionTyCon
606 csel1CoercionTyConName  = mkCoConName (fsLit "csel1") csel1CoercionTyConKey csel1CoercionTyCon
607 csel2CoercionTyConName  = mkCoConName (fsLit "csel2") csel2CoercionTyConKey csel2CoercionTyCon
608 cselRCoercionTyConName  = mkCoConName (fsLit "cselR") cselRCoercionTyConKey cselRCoercionTyCon
609 unsafeCoercionTyConName = mkCoConName (fsLit "CoUnsafe") unsafeCoercionTyConKey unsafeCoercionTyCon
610
611 mkCoConName :: FastString -> Unique -> TyCon -> Name
612 mkCoConName occ key coCon = mkWiredInName gHC_PRIM (mkTcOccFS occ)
613                             key (ATyCon coCon) BuiltInSyntax
614 \end{code}
615
616
617 %************************************************************************
618 %*                                                                      *
619             Newtypes
620 %*                                                                      *
621 %************************************************************************
622
623 \begin{code}
624 instNewTyCon_maybe :: TyCon -> [Type] -> Maybe (Type, CoercionI)
625 -- ^ If @co :: T ts ~ rep_ty@ then:
626 --
627 -- > instNewTyCon_maybe T ts = Just (rep_ty, co)
628 instNewTyCon_maybe tc tys
629   | Just (tvs, ty, mb_co_tc) <- unwrapNewTyCon_maybe tc
630   = ASSERT( tys `lengthIs` tyConArity tc )
631     Just (substTyWith tvs tys ty, 
632           case mb_co_tc of
633            Nothing    -> IdCo
634            Just co_tc -> ACo (mkTyConApp co_tc tys))
635   | otherwise
636   = Nothing
637
638 -- this is here to avoid module loops
639 splitNewTypeRepCo_maybe :: Type -> Maybe (Type, Coercion)  
640 -- ^ Sometimes we want to look through a @newtype@ and get its associated coercion.
641 -- This function only strips *one layer* of @newtype@ off, so the caller will usually call
642 -- itself recursively. Furthermore, this function should only be applied to types of kind @*@,
643 -- hence the newtype is always saturated. If @co : ty ~ ty'@ then:
644 --
645 -- > splitNewTypeRepCo_maybe ty = Just (ty', co)
646 --
647 -- The function returns @Nothing@ for non-@newtypes@ or fully-transparent @newtype@s.
648 splitNewTypeRepCo_maybe ty 
649   | Just ty' <- coreView ty = splitNewTypeRepCo_maybe ty'
650 splitNewTypeRepCo_maybe (TyConApp tc tys)
651   | Just (ty', coi) <- instNewTyCon_maybe tc tys
652   = case coi of
653         ACo co -> Just (ty', co)
654         IdCo   -> panic "splitNewTypeRepCo_maybe"
655                         -- This case handled by coreView
656 splitNewTypeRepCo_maybe _
657   = Nothing
658
659 -- | Determines syntactic equality of coercions
660 coreEqCoercion :: Coercion -> Coercion -> Bool
661 coreEqCoercion = coreEqType
662 \end{code}
663
664
665 %************************************************************************
666 %*                                                                      *
667             CoercionI and its constructors
668 %*                                                                      *
669 %************************************************************************
670
671 --------------------------------------
672 -- CoercionI smart constructors
673 --      lifted smart constructors of ordinary coercions
674
675 \begin{code}
676 -- | 'CoercionI' represents a /lifted/ ordinary 'Coercion', in that it
677 -- can represent either one of:
678 --
679 -- 1. A proper 'Coercion'
680 --
681 -- 2. The identity coercion
682 data CoercionI = IdCo | ACo Coercion
683
684 instance Outputable CoercionI where
685   ppr IdCo     = ptext (sLit "IdCo")
686   ppr (ACo co) = ppr co
687
688 isIdentityCoI :: CoercionI -> Bool
689 isIdentityCoI IdCo = True
690 isIdentityCoI _    = False
691
692 -- | Tests whether all the given 'CoercionI's represent the identity coercion
693 allIdCoIs :: [CoercionI] -> Bool
694 allIdCoIs = all isIdentityCoI
695
696 -- | For each 'CoercionI' in the input list, return either the 'Coercion' it
697 -- contains or the corresponding 'Type' from the other list
698 zipCoArgs :: [CoercionI] -> [Type] -> [Coercion]
699 zipCoArgs cois tys = zipWith fromCoI cois tys
700
701 -- | Return either the 'Coercion' contained within the 'CoercionI' or the given
702 -- 'Type' if the 'CoercionI' is the identity 'Coercion'
703 fromCoI :: CoercionI -> Type -> Type
704 fromCoI IdCo ty     = ty        -- Identity coercion represented 
705 fromCoI (ACo co) _  = co        --      by the type itself
706
707 -- | Smart constructor for @sym@ on 'CoercionI', see also 'mkSymCoercion'
708 mkSymCoI :: CoercionI -> CoercionI
709 mkSymCoI IdCo = IdCo
710 mkSymCoI (ACo co) = ACo $ mkCoercion symCoercionTyCon [co] 
711                                 -- the smart constructor
712                                 -- is too smart with tyvars
713
714 -- | Smart constructor for @trans@ on 'CoercionI', see also 'mkTransCoercion'
715 mkTransCoI :: CoercionI -> CoercionI -> CoercionI
716 mkTransCoI IdCo aco = aco
717 mkTransCoI aco IdCo = aco
718 mkTransCoI (ACo co1) (ACo co2) = ACo $ mkTransCoercion co1 co2
719
720 -- | Smart constructor for type constructor application on 'CoercionI', see also 'mkAppCoercion'
721 mkTyConAppCoI :: TyCon -> [Type] -> [CoercionI] -> CoercionI
722 mkTyConAppCoI tyCon tys cois
723   | allIdCoIs cois = IdCo
724   | otherwise      = ACo (TyConApp tyCon (zipCoArgs cois tys))
725
726 -- | Smart constructor for honest-to-god 'Coercion' application on 'CoercionI', see also 'mkAppCoercion'
727 mkAppTyCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI
728 mkAppTyCoI _   IdCo _   IdCo = IdCo
729 mkAppTyCoI ty1 coi1 ty2 coi2 =
730         ACo $ AppTy (fromCoI coi1 ty1) (fromCoI coi2 ty2)
731
732 -- | Smart constructor for function-'Coercion's on 'CoercionI', see also 'mkFunCoercion'
733 mkFunTyCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI
734 mkFunTyCoI _   IdCo _   IdCo = IdCo
735 mkFunTyCoI ty1 coi1 ty2 coi2 =
736         ACo $ FunTy (fromCoI coi1 ty1) (fromCoI coi2 ty2)
737
738 -- | Smart constructor for quantified 'Coercion's on 'CoercionI', see also 'mkForAllCoercion'
739 mkForAllTyCoI :: TyVar -> CoercionI -> CoercionI
740 mkForAllTyCoI _ IdCo = IdCo
741 mkForAllTyCoI tv (ACo co) = ACo $ ForAllTy tv co
742
743 -- | Extract a 'Coercion' from a 'CoercionI' if it represents one. If it is the identity coercion,
744 -- panic
745 fromACo :: CoercionI -> Coercion
746 fromACo (ACo co) = co
747
748 -- | Smart constructor for class 'Coercion's on 'CoercionI'. Satisfies:
749 --
750 -- > mkClassPPredCoI cls tys cois :: PredTy (cls tys) ~ PredTy (cls (tys `cast` cois))
751 mkClassPPredCoI :: Class -> [Type] -> [CoercionI] -> CoercionI
752 mkClassPPredCoI cls tys cois 
753   | allIdCoIs cois = IdCo
754   | otherwise      = ACo $ PredTy $ ClassP cls (zipCoArgs cois tys)
755
756 -- | Smart constructor for implicit parameter 'Coercion's on 'CoercionI'. Similar to 'mkClassPPredCoI'
757 mkIParamPredCoI :: (IPName Name) -> CoercionI -> CoercionI 
758 mkIParamPredCoI _   IdCo     = IdCo
759 mkIParamPredCoI ipn (ACo co) = ACo $ PredTy $ IParam ipn co
760
761 -- | Smart constructor for type equality 'Coercion's on 'CoercionI'. Similar to 'mkClassPPredCoI'
762 mkEqPredCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI
763 mkEqPredCoI _    IdCo     _   IdCo      = IdCo
764 mkEqPredCoI ty1  IdCo     _   (ACo co2) = ACo $ PredTy $ EqPred ty1 co2
765 mkEqPredCoI _   (ACo co1) ty2 coi2      = ACo $ PredTy $ EqPred co1 (fromCoI coi2 ty2)
766 \end{code}
767
768 %************************************************************************
769 %*                                                                      *
770                  Optimising coercions                                                                   
771 %*                                                                      *
772 %************************************************************************
773
774 \begin{code}
775 optCoercion :: Coercion -> Coercion
776 optCoercion co
777   = ASSERT2( coercionKind co `eq` coercionKind result, 
778              ppr co $$ ppr result $$ ppr (coercionKind co) $$ ppr (coercionKind result) )
779     result
780   where
781         (s1,t1) `eq` (s2,t2) = s1 `coreEqType` s2 && t1 `coreEqType` t2
782
783         (result,_,_) = go co
784                          -- optimized, changed?, identity?
785         go :: Coercion -> ( Coercion, Bool, Bool )
786         -- traverse coercion term bottom up and return
787         --
788         --    1) equivalent coercion, in optimized form
789         --
790         --    2) whether the output coercion differs from
791         --       the input coercion
792         --
793         --    3) whether the coercion is an identity coercion
794         --
795         -- Performs the following optimizations:
796         --
797         --      sym id          >->     id
798         --      trans id co     >->     co
799         --      trans co id     >->     co
800         --      sym (sym co)    >->     co
801         --      trans g (sym g) >->     id
802         --      trans (sym g) g >->     id
803         --
804         go ty@(TyVarTy a) | isCoVar a = let (ty1,ty2) = coercionKind ty
805                                         in (ty, False, ty1 `coreEqType` ty2)
806                           | otherwise = (ty, False, True)
807         go ty@(AppTy ty1 ty2)
808           = let (ty1', chan1, id1) = go ty1
809                 (ty2', chan2, id2) = go ty2
810             in if chan1 || chan2
811                  then (AppTy ty1' ty2', True,  id1 && id2)
812                  else (ty             , False, id1 && id2)
813         go ty@(TyConApp tc args)
814           | tc == symCoercionTyCon, (ty1:tys) <- args
815           = goSym ty ty1 tys
816           | tc == transCoercionTyCon, [ty1,ty2] <- args
817           = goTrans ty ty1 ty2
818           | tc == leftCoercionTyCon, [ty1] <- args
819           = goLeft ty ty1
820           | tc == rightCoercionTyCon, [ty1] <- args
821           = goRight ty ty1
822           | tc == instCoercionTyCon, [ty1,ty2] <- args
823           = goInst ty ty1 ty2
824           | not (isCoercionTyCon tc)
825           = let (args', chans, ids) = mapAndUnzip3 go args
826             in  if or chans
827                   then (TyConApp tc args', True , and ids)
828                   else (ty               , False, and ids) 
829           | otherwise
830           = (ty, False, False)
831         go ty@(FunTy ty1 ty2)
832           = let (ty1',chan1,id1) = go ty1
833                 (ty2',chan2,id2) = go ty2
834             in  if chan1 || chan2
835                   then (FunTy ty1' ty2', True , id1 && id2)
836                   else (ty             , False, id1 && id2)
837         go ty@(ForAllTy tv ty1)
838           = let (ty1', chan1, id1) = go ty1
839             in if chan1
840                  then (ForAllTy tv ty1', True , id1)
841                  else (ty              , False, id1)
842         go ty@(PredTy (EqPred ty1 ty2))
843           = let (ty1', chan1, id1) = go ty1
844                 (ty2', chan2, id2) = go ty2
845             in if chan1 || chan2
846                  then (PredTy (EqPred ty1' ty2'), True , id1 && id2)
847                  else (ty                       , False, id1 && id2)
848         go ty@(PredTy (ClassP cl args))
849           = let (args', chans, ids) = mapAndUnzip3 go args
850             in  if or chans
851                   then (PredTy (ClassP cl args'), True , and ids)
852                   else (ty                      , False, and ids)
853         go ty@(PredTy (IParam name ty1))
854           = let (ty1', chan1, id1) = go ty1
855             in  if chan1
856                   then (PredTy (IParam name ty1'), True , id1)
857                   else (ty                       , False, id1)
858
859         goSym :: Coercion -> Coercion -> [Coercion] -> ( Coercion, Bool, Bool )
860         --
861         -- pushes the sym constructor inwards, if possible
862         --
863         --   takes original coercion term
864         --                  first argument 
865         --                  rest of arguments
866         goSym ty ty1 tys  
867           = case mkSymCoercion ty1 of
868               (TyConApp tc _ ) | tc == symCoercionTyCon
869                                -> let (tys',chans',ids) = mapAndUnzip3 go (ty1:tys)
870                                   in  if or chans'
871                                         then (TyConApp symCoercionTyCon tys', True , and ids)
872                                         else (ty                            , False, and ids)
873               ty1'             -> let (ty',_   ,id') = go (mkAppsCoercion ty1' tys)
874                                   in  (ty',True,id')
875
876
877         goRight :: Coercion -> Coercion -> ( Coercion, Bool, Bool )
878         --
879         -- reduces the right constructor, if possible
880         --
881         --   takes original coercion term
882         --                  argument 
883         --
884         goRight ty ty1  
885           = case mkRightCoercion ty1 of
886               (TyConApp tc _ ) | tc == rightCoercionTyCon
887                                -> let (ty1',chan1,id1) = go ty1
888                                   in  if chan1
889                                         then (TyConApp rightCoercionTyCon [ty1'], True , id1)
890                                         else (ty                                , False, id1)
891               ty1'             -> let (ty',_   ,id') = go ty1'
892                                   in  (ty',True,id')
893
894         goLeft :: Coercion -> Coercion -> ( Coercion, Bool, Bool )
895         --
896         -- reduces the left constructor, if possible
897         --
898         --   takes original coercion term
899         --                  argument 
900         --
901         goLeft ty ty1  
902           = case mkLeftCoercion ty1 of
903               (TyConApp tc _ ) | tc == leftCoercionTyCon
904                                -> let (ty1',chan1,id1) = go ty1
905                                   in  if chan1
906                                         then (TyConApp leftCoercionTyCon [ty1'], True , id1)
907                                         else (ty                                , False, id1)
908               ty1'             -> let (ty',_   ,id') = go ty1'
909                                   in  (ty',True,id')
910
911         goInst :: Coercion -> Coercion -> Coercion -> ( Coercion, Bool, Bool )
912         --
913         -- reduces the inst constructor, if possible
914         --
915         --   takes original coercion term
916         --                  coercion argument 
917         --                  type argument
918         --
919         goInst ty ty1 ty2
920           = case mkInstCoercion ty1 ty2 of
921               (TyConApp tc _ ) | tc == instCoercionTyCon
922                                -> let (ty1',chan1,id1) = go ty1
923                                   in  if chan1
924                                         then (TyConApp instCoercionTyCon [ty1',ty2], True , id1)
925                                         else (ty                                   , False, id1)
926               ty1'             -> let (ty',_   ,id') = go ty1'
927                                   in  (ty',True,id')
928
929         goTrans :: Coercion -> Coercion -> Coercion -> ( Coercion, Bool, Bool )
930         --
931         --      trans id co     >->     co
932         --      trans co id     >->     co
933         --      trans g (sym g) >->     id
934         --      trans (sym g) g >->     id
935         --
936         goTrans ty ty1 ty2
937           | id1
938           = (ty2', True, id2)
939           | id2
940           = (ty1', True, False)
941           | chan1 || chan2
942           = (TyConApp transCoercionTyCon [ty1',ty2'], True , False)
943           | Just ty' <- mty'
944           = (ty', True, True)
945           | otherwise
946           = (ty, False, False)
947           where (ty1', chan1, id1) = go ty1
948                 (ty2', chan2, id2) = go ty2
949                 mty' = case mkTransCoercion ty1' ty2'
950                          of (TyConApp tc _) | tc == transCoercionTyCon
951                                              -> Nothing
952                             ty'              -> Just ty' 
953 \end{code}