Move the register-inplace special-case stuff into the ghc-prim package

[ghc-hetmet.git] / compiler / types / Coercion.lhs

diff --git a/compiler/types/Coercion.lhs b/compiler/types/Coercion.lhs
index cb85028..3bc5d84 100644 (file)
--- a/compiler/types/Coercion.lhs
+++ b/compiler/types/Coercion.lhs
@@ -1,5 +1,8 @@
+%
+% (c) The University of Glasgow 2006
+%

 
 

- Module for type coercions, as in System FC.
+Module for type coercions, as in System FC.

 
 Coercions are represented as types, and their kinds tell what types the 
 coercion works on. 
 
 Coercions are represented as types, and their kinds tell what types the 
 coercion works on. 

@@ -9,6 +12,13 @@ The coercion kind constructor is a special TyCon that must always be saturated
   typeKind (symCoercion type) :: TyConApp CoercionTyCon{...} [type, type]
 
 \begin{code}
   typeKind (symCoercion type) :: TyConApp CoercionTyCon{...} [type, type]
 
 \begin{code}

+{-# OPTIONS -fno-warn-incomplete-patterns #-}
+-- The above warning supression flag is a temporary kludge.
+-- While working on this module you are encouraged to remove it and fix
+-- any warnings in the module. See
+--     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings
+-- for details
+

 module Coercion (
         Coercion,
  
 module Coercion (
         Coercion,
  

@@ -19,43 +29,51 @@ module Coercion (
        isEqPred, mkEqPred, getEqPredTys, isEqPredTy,  
 
        -- Coercion transformations
        isEqPred, mkEqPred, getEqPredTys, isEqPredTy,  
 
        -- Coercion transformations

+       mkCoercion,

         mkSymCoercion, mkTransCoercion,
         mkSymCoercion, mkTransCoercion,

-        mkLeftCoercion, mkRightCoercion, mkInstCoercion, mkAppCoercion,
+        mkLeftCoercion, mkRightCoercion, mkRightCoercions,
+       mkInstCoercion, mkAppCoercion,

         mkForAllCoercion, mkFunCoercion, mkInstsCoercion, mkUnsafeCoercion,
         mkForAllCoercion, mkFunCoercion, mkInstsCoercion, mkUnsafeCoercion,

-        mkNewTypeCoercion, mkAppsCoercion,
+        mkNewTypeCoercion, mkFamInstCoercion, mkAppsCoercion,

 
 

-        splitNewTypeRepCo_maybe, decomposeCo,
+        splitNewTypeRepCo_maybe, instNewTyCon_maybe, decomposeCo,

 
         unsafeCoercionTyCon, symCoercionTyCon,
         transCoercionTyCon, leftCoercionTyCon, 
 
         unsafeCoercionTyCon, symCoercionTyCon,
         transCoercionTyCon, leftCoercionTyCon, 

-        rightCoercionTyCon, instCoercionTyCon -- needed by TysWiredIn
+        rightCoercionTyCon, instCoercionTyCon, -- needed by TysWiredIn
+
+        -- Comparison
+        coreEqCoercion,
+
+       -- CoercionI
+       CoercionI(..),
+       isIdentityCoercion,
+       mkSymCoI, mkTransCoI, 
+       mkTyConAppCoI, mkAppTyCoI, mkFunTyCoI,
+       mkForAllTyCoI,
+       fromCoI, fromACo,
+       mkClassPPredCoI, mkIParamPredCoI, mkEqPredCoI
+

        ) where 
 
 #include "HsVersions.h"
 
 import TypeRep
        ) where 
 
 #include "HsVersions.h"
 
 import TypeRep

-import Type      ( Type, Kind, PredType, substTyWith, mkAppTy, mkForAllTy,
-                    mkFunTy, splitAppTy_maybe, splitForAllTy_maybe, coreView,
-                    kindView, mkTyConApp, isCoercionKind, isEqPred, mkAppTys,
-                    coreEqType, splitAppTys, isTyVarTy, splitTyConApp_maybe
-                  )
-import TyCon      ( TyCon, tyConArity, mkCoercionTyCon, isNewTyCon,
-                    newTyConRhs, newTyConCo, 
-                    isCoercionTyCon, isCoercionTyCon_maybe )
-import Var       ( Var, TyVar, isTyVar, tyVarKind )
-import Name       ( BuiltInSyntax(..), Name, mkWiredInName, tcName )
-import OccName    ( mkOccNameFS )
-import PrelNames  ( symCoercionTyConKey, 
-                    transCoercionTyConKey, leftCoercionTyConKey,
-                    rightCoercionTyConKey, instCoercionTyConKey, 
-                    unsafeCoercionTyConKey, gHC_PRIM
-                  )
-import Util       ( lengthIs, snocView )
-import Unique     ( hasKey )
-import BasicTypes ( Arity )
+import Type
+import TyCon
+import Class
+import Var
+import Name
+import OccName
+import PrelNames
+import Util
+import Unique
+import BasicTypes

 import Outputable
 import Outputable

+import FastString

 
 

-
+type Coercion     = Type
+type CoercionKind = Kind       -- A CoercionKind is always of form (ty1 :=: ty2)

 
 ------------------------------
 decomposeCo :: Arity -> Coercion -> [Coercion]
 
 ------------------------------
 decomposeCo :: Arity -> Coercion -> [Coercion]

@@ -65,7 +83,7 @@ decomposeCo :: Arity -> Coercion -> [Coercion]
 decomposeCo n co
   = go n co []
   where
 decomposeCo n co
   = go n co []
   where

-    go 0 co cos = cos
+    go 0 _  cos = cos

     go n co cos = go (n-1) (mkLeftCoercion co)
                           (mkRightCoercion co : cos)
 
     go n co cos = go (n-1) (mkLeftCoercion co)
                           (mkRightCoercion co : cos)
 

@@ -74,8 +92,9 @@ decomposeCo n co
 -------------------------------------------------------
 -- and some coercion kind stuff
 
 -------------------------------------------------------
 -- and some coercion kind stuff
 

+isEqPredTy :: Type -> Bool

 isEqPredTy (PredTy pred) = isEqPred pred
 isEqPredTy (PredTy pred) = isEqPred pred

-isEqPredTy other         = False
+isEqPredTy _             = False

 
 mkEqPred :: (Type, Type) -> PredType
 mkEqPred (ty1, ty2) = EqPred ty1 ty2
 
 mkEqPred :: (Type, Type) -> PredType
 mkEqPred (ty1, ty2) = EqPred ty1 ty2

@@ -97,19 +116,13 @@ splitCoercionKind (PredTy (EqPred ty1 ty2))    = (ty1, ty2)
 splitCoercionKind_maybe :: Kind -> Maybe (Type, Type)
 splitCoercionKind_maybe co | Just co' <- kindView co = splitCoercionKind_maybe co'
 splitCoercionKind_maybe (PredTy (EqPred ty1 ty2)) = Just (ty1, ty2)
 splitCoercionKind_maybe :: Kind -> Maybe (Type, Type)
 splitCoercionKind_maybe co | Just co' <- kindView co = splitCoercionKind_maybe co'
 splitCoercionKind_maybe (PredTy (EqPred ty1 ty2)) = Just (ty1, ty2)

-splitCoercionKind_maybe other = Nothing
-
-isCoVar :: Var -> Bool
-isCoVar tv = isTyVar tv && isCoercionKind (tyVarKind tv)
-
-type Coercion     = Type
-type CoercionKind = Kind       -- A CoercionKind is always of form (ty1 :=: ty2)
+splitCoercionKind_maybe _ = Nothing

 
 coercionKind :: Coercion -> (Type, Type)
 --     c :: (t1 :=: t2)
 -- Then (coercionKind c) = (t1,t2)
 
 coercionKind :: Coercion -> (Type, Type)
 --     c :: (t1 :=: t2)
 -- Then (coercionKind c) = (t1,t2)

-coercionKind (TyVarTy a) | isCoVar a = splitCoercionKind (tyVarKind a)
-                         | otherwise = let t = (TyVarTy a) in (t, t)
+coercionKind ty@(TyVarTy a) | isCoVar a = splitCoercionKind (tyVarKind a)
+                            | otherwise = (ty, ty)

 coercionKind (AppTy ty1 ty2) 
   = let (t1, t2) = coercionKind ty1
         (s1, s2) = coercionKind ty2 in
 coercionKind (AppTy ty1 ty2) 
   = let (t1, t2) = coercionKind ty1
         (s1, s2) = coercionKind ty2 in

@@ -117,10 +130,11 @@ coercionKind (AppTy ty1 ty2)
 coercionKind (TyConApp tc args)
   | Just (ar, rule) <- isCoercionTyCon_maybe tc 
     -- CoercionTyCons carry their kinding rule, so we use it here
 coercionKind (TyConApp tc args)
   | Just (ar, rule) <- isCoercionTyCon_maybe tc 
     -- CoercionTyCons carry their kinding rule, so we use it here

-  = if length args >= ar 
-    then splitCoercionKind (rule args)
-    else pprPanic ("arity/arguments mismatch in coercionKind:") 
-             (ppr ar $$ ppr tc <+> ppr args)
+  = ASSERT( length args >= ar )        -- Always saturated
+    let (ty1,ty2)    = rule (take ar args)     -- Apply the rule to the right number of args
+       (tys1, tys2) = coercionKinds (drop ar args)
+    in (mkAppTys ty1 tys1, mkAppTys ty2 tys2)
+

   | otherwise
   = let (lArgs, rArgs) = coercionKinds args in
     (TyConApp tc lArgs, TyConApp tc rArgs)
   | otherwise
   = let (lArgs, rArgs) = coercionKinds args in
     (TyConApp tc lArgs, TyConApp tc rArgs)

@@ -131,7 +145,6 @@ coercionKind (FunTy ty1 ty2)
 coercionKind (ForAllTy tv ty) 
   = let (ty1, ty2) = coercionKind ty in
     (ForAllTy tv ty1, ForAllTy tv ty2)
 coercionKind (ForAllTy tv ty) 
   = let (ty1, ty2) = coercionKind ty in
     (ForAllTy tv ty1, ForAllTy tv ty2)

-coercionKind (NoteTy _ ty) = coercionKind ty

 coercionKind (PredTy (EqPred c1 c2)) 
   = let k1 = coercionKindPredTy c1
         k2 = coercionKindPredTy c2 in
 coercionKind (PredTy (EqPred c1 c2)) 
   = let k1 = coercionKindPredTy c1
         k2 = coercionKindPredTy c2 in

@@ -153,11 +166,14 @@ coercionKinds tys = unzip $ map coercionKind tys
 -- Coercion kind and type mk's
 -- (make saturated TyConApp CoercionTyCon{...} args)
 
 -- Coercion kind and type mk's
 -- (make saturated TyConApp CoercionTyCon{...} args)
 

+mkCoercion :: TyCon -> [Type] -> Coercion

 mkCoercion coCon args = ASSERT( tyConArity coCon == length args ) 
                         TyConApp coCon args
 
 mkAppCoercion, mkFunCoercion, mkTransCoercion, mkInstCoercion :: Coercion -> Coercion -> Coercion
 mkSymCoercion, mkLeftCoercion, mkRightCoercion :: Coercion -> Coercion
 mkCoercion coCon args = ASSERT( tyConArity coCon == length args ) 
                         TyConApp coCon args
 
 mkAppCoercion, mkFunCoercion, mkTransCoercion, mkInstCoercion :: Coercion -> Coercion -> Coercion
 mkSymCoercion, mkLeftCoercion, mkRightCoercion :: Coercion -> Coercion

+mkAppsCoercion, mkInstsCoercion :: Coercion -> [Coercion] -> Coercion
+mkForAllCoercion :: Var -> Coercion -> Coercion

 
 mkAppCoercion    co1 co2 = mkAppTy co1 co2
 mkAppsCoercion   co1 tys = foldl mkAppTy co1 tys
 
 mkAppCoercion    co1 co2 = mkAppTy co1 co2
 mkAppsCoercion   co1 tys = foldl mkAppTy co1 tys

@@ -166,70 +182,94 @@ mkForAllCoercion tv  co  = ASSERT ( isTyVar tv ) mkForAllTy tv co
 mkFunCoercion    co1 co2 = mkFunTy co1 co2
 
 
 mkFunCoercion    co1 co2 = mkFunTy co1 co2
 
 

+-------------------------------

 -- This smart constructor creates a sym'ed version its argument,
 -- but tries to push the sym's down to the leaves.  If we come to
 -- sym tv or sym tycon then we can drop the sym because tv and tycon
 -- are reflexive coercions
 mkSymCoercion co      
 -- This smart constructor creates a sym'ed version its argument,
 -- but tries to push the sym's down to the leaves.  If we come to
 -- sym tv or sym tycon then we can drop the sym because tv and tycon
 -- are reflexive coercions
 mkSymCoercion co      

-  | Just co2 <- splitSymCoercion_maybe co = co2
-     -- sym (sym co) --> co
-  | Just (co1, arg_tys) <- splitTyConApp_maybe co
-  , not (isCoercionTyCon co1) = mkTyConApp co1 (map mkSymCoercion arg_tys)
-     -- we can drop the sym for a TyCon 
-     -- sym (ty [t1, ..., tn]) --> ty [sym t1, ..., sym tn] 
-  | (co1, arg_tys) <- splitAppTys co
-  , isTyVarTy co1 = mkAppTys (maybe_drop co1) (map mkSymCoercion arg_tys)
-     -- sym (tv [t1, ..., tn]) --> tv [sym t1, ..., sym tn]
-     --   if tv type variable
-     -- sym (cv [t1, ..., tn]) --> (sym cv) [sym t1, ..., sym tn]
-     --   if cv is a coercion variable
-     -- fall through if head is a CoercionTyCon
-  | Just (co1, co2) <- splitTransCoercion_maybe co
+  | Just co' <- coreView co = mkSymCoercion co'
+
+mkSymCoercion (ForAllTy tv ty)  = ForAllTy tv (mkSymCoercion ty)
+mkSymCoercion (AppTy co1 co2)  = AppTy (mkSymCoercion co1) (mkSymCoercion co2)
+mkSymCoercion (FunTy co1 co2)  = FunTy (mkSymCoercion co1) (mkSymCoercion co2)
+
+mkSymCoercion (TyConApp tc cos) 
+  | not (isCoercionTyCon tc) = mkTyConApp tc (map mkSymCoercion cos)
+
+mkSymCoercion (TyConApp tc [co]) 
+  | tc `hasKey` symCoercionTyConKey   = co    -- sym (sym co) --> co
+  | tc `hasKey` leftCoercionTyConKey  = mkLeftCoercion (mkSymCoercion co)
+  | tc `hasKey` rightCoercionTyConKey = mkRightCoercion (mkSymCoercion co)
+
+mkSymCoercion (TyConApp tc [co1,co2]) 
+  | tc `hasKey` transCoercionTyConKey

      -- sym (co1 `trans` co2) --> (sym co2) `trans (sym co2)
      -- sym (co1 `trans` co2) --> (sym co2) `trans (sym co2)

+     -- Note reversal of arguments!

   = mkTransCoercion (mkSymCoercion co2) (mkSymCoercion co1)
   = mkTransCoercion (mkSymCoercion co2) (mkSymCoercion co1)

-  | Just (co, ty) <- splitInstCoercion_maybe co
+
+  | tc `hasKey` instCoercionTyConKey

      -- sym (co @ ty) --> (sym co) @ ty
      -- sym (co @ ty) --> (sym co) @ ty

-  = mkInstCoercion (mkSymCoercion co) ty
-  | Just co <- splitLeftCoercion_maybe co
-     -- sym (left co) --> left (sym co)
-  = mkLeftCoercion (mkSymCoercion co)
-  | Just co <- splitRightCoercion_maybe co
-     -- sym (right co) --> right (sym co)
-  = mkRightCoercion (mkSymCoercion co)
-  where
-    maybe_drop (TyVarTy tv) 
-        | isCoVar tv = mkCoercion symCoercionTyCon [TyVarTy tv]
-        | otherwise  = TyVarTy tv
-    maybe_drop other = other
-mkSymCoercion (ForAllTy tv ty) = ForAllTy tv (mkSymCoercion ty)
--- for atomic types and constructors, we can just ignore sym since these
--- are reflexive coercions
+     -- Note: sym is not applied to 'ty'
+  = mkInstCoercion (mkSymCoercion co1) co2
+
+mkSymCoercion (TyConApp tc cos)        -- Other coercion tycons, such as those
+  = mkCoercion symCoercionTyCon [TyConApp tc cos]  -- arising from newtypes
+

 mkSymCoercion (TyVarTy tv) 
   | isCoVar tv = mkCoercion symCoercionTyCon [TyVarTy tv]
 mkSymCoercion (TyVarTy tv) 
   | isCoVar tv = mkCoercion symCoercionTyCon [TyVarTy tv]

-  | otherwise  = TyVarTy tv
-mkSymCoercion co = mkCoercion symCoercionTyCon [co] 
+  | otherwise  = TyVarTy tv    -- Reflexive
+
+-------------------------------
+-- ToDo: we should be cleverer about transitivity
+mkTransCoercion g1 g2  -- sym g `trans` g = id
+  | (t1,_) <- coercionKind g1
+  , (_,t2) <- coercionKind g2
+  , t1 `coreEqType` t2 
+  = t1 
+
+  | otherwise
+  = mkCoercion transCoercionTyCon [g1, g2]
+

 
 

+-------------------------------

 -- Smart constructors for left and right
 mkLeftCoercion co 
   | Just (co', _) <- splitAppCoercion_maybe co = co'
 -- Smart constructors for left and right
 mkLeftCoercion co 
   | Just (co', _) <- splitAppCoercion_maybe co = co'

-  | otherwise                           = mkCoercion leftCoercionTyCon [co]
+  | otherwise = mkCoercion leftCoercionTyCon [co]

 
 mkRightCoercion  co      
 
 mkRightCoercion  co      

-  | Just (co1, co2) <- splitAppCoercion_maybe co = co2
+  | Just (_, co2) <- splitAppCoercion_maybe co = co2

   | otherwise = mkCoercion rightCoercionTyCon [co]
 
   | otherwise = mkCoercion rightCoercionTyCon [co]
 

-mkTransCoercion co1 co2 = mkCoercion transCoercionTyCon [co1, co2]
-
-mkInstCoercion  co ty = mkCoercion instCoercionTyCon  [co, ty]
+mkRightCoercions :: Int -> Coercion -> [Coercion]
+mkRightCoercions n co
+  = go n co []
+  where
+    go n co acc 
+       | n > 0
+       = case splitAppCoercion_maybe co of
+          Just (co1,co2) -> go (n-1) co1 (co2:acc)
+          Nothing        -> go (n-1) (mkCoercion leftCoercionTyCon [co]) (mkCoercion rightCoercionTyCon [co]:acc)
+       | otherwise
+       = acc
+
+mkInstCoercion co ty
+  | Just (tv,co') <- splitForAllTy_maybe co
+  = substTyWith [tv] [ty] co'  -- (forall a.co) @ ty  -->  co[ty/a]
+  | otherwise
+  = mkCoercion instCoercionTyCon  [co, ty]

 
 mkInstsCoercion co tys = foldl mkInstCoercion co tys
 
 
 mkInstsCoercion co tys = foldl mkInstCoercion co tys
 

+{-

 splitSymCoercion_maybe :: Coercion -> Maybe Coercion
 splitSymCoercion_maybe (TyConApp tc [co]) = 
   if tc `hasKey` symCoercionTyConKey
   then Just co
   else Nothing
 splitSymCoercion_maybe co = Nothing
 splitSymCoercion_maybe :: Coercion -> Maybe Coercion
 splitSymCoercion_maybe (TyConApp tc [co]) = 
   if tc `hasKey` symCoercionTyConKey
   then Just co
   else Nothing
 splitSymCoercion_maybe co = Nothing

+-}

 
 splitAppCoercion_maybe :: Coercion -> Maybe (Coercion, Coercion)
 -- Splits a coercion application, being careful *not* to split (left c), etc
 
 splitAppCoercion_maybe :: Coercion -> Maybe (Coercion, Coercion)
 -- Splits a coercion application, being careful *not* to split (left c), etc

@@ -242,8 +282,9 @@ splitAppCoercion_maybe (TyConApp tc tys)
    = case snocView tys of
        Just (tys', ty') -> Just (TyConApp tc tys', ty')
        Nothing          -> Nothing
    = case snocView tys of
        Just (tys', ty') -> Just (TyConApp tc tys', ty')
        Nothing          -> Nothing

-splitAppCoercion_maybe co = Nothing
+splitAppCoercion_maybe _ = Nothing

 
 

+{-

 splitTransCoercion_maybe :: Coercion -> Maybe (Coercion, Coercion)
 splitTransCoercion_maybe (TyConApp tc [ty1, ty2]) 
  = if tc `hasKey` transCoercionTyConKey then
 splitTransCoercion_maybe :: Coercion -> Maybe (Coercion, Coercion)
 splitTransCoercion_maybe (TyConApp tc [ty1, ty2]) 
  = if tc `hasKey` transCoercionTyConKey then

@@ -275,29 +316,44 @@ splitRightCoercion_maybe (TyConApp tc [co])
    else
        Nothing
 splitRightCoercion_maybe other = Nothing
    else
        Nothing
 splitRightCoercion_maybe other = Nothing

+-}

 
 -- Unsafe coercion is not safe, it is used when we know we are dealing with
 
 -- Unsafe coercion is not safe, it is used when we know we are dealing with

--- bottom, which is the one case in which it is safe.  It is also used to 
+-- bottom, which is one case in which it is safe.  It is also used to 

 -- implement the unsafeCoerce# primitive.
 mkUnsafeCoercion :: Type -> Type -> Coercion
 mkUnsafeCoercion ty1 ty2 
   = mkCoercion unsafeCoercionTyCon [ty1, ty2]
 
 
 -- implement the unsafeCoerce# primitive.
 mkUnsafeCoercion :: Type -> Type -> Coercion
 mkUnsafeCoercion ty1 ty2 
   = mkCoercion unsafeCoercionTyCon [ty1, ty2]
 
 

--- Make the coercion associated with a newtype.  If we have
---
---   newtype T a b = MkT (Int, a, b)
---
--- Then (mkNewTypeCoercion CoT T [a,b] (Int, a, b)) creates the coercion
--- CoT, such kinding rule such that
---
---   CoT S U :: (Int, S, U) :=: T S U
+-- See note [Newtype coercions] in TyCon

 mkNewTypeCoercion :: Name -> TyCon -> [TyVar] -> Type -> TyCon
 mkNewTypeCoercion :: Name -> TyCon -> [TyVar] -> Type -> TyCon

-mkNewTypeCoercion name tycon tvs rhs_ty 
-  = ASSERT (length tvs == tyConArity tycon)
-    mkCoercionTyCon name (tyConArity tycon) rule
+mkNewTypeCoercion name tycon tvs rhs_ty
+  = mkCoercionTyCon name co_con_arity rule

   where
   where

-    rule args = mkCoKind (substTyWith tvs args rhs_ty) (TyConApp tycon args)
+    co_con_arity = length tvs
+
+    rule args = ASSERT( co_con_arity == length args )
+               (TyConApp tycon args, substTyWith tvs args rhs_ty)
+
+-- Coercion identifying a data/newtype/synonym representation type and its 
+-- family instance.  It has the form `Co tvs :: F ts :=: R tvs', where `Co' is 
+-- the coercion tycon built here, `F' the family tycon and `R' the (derived)
+-- representation tycon.
+--
+mkFamInstCoercion :: Name      -- unique name for the coercion tycon
+                 -> [TyVar]    -- type parameters of the coercion (`tvs')
+                 -> TyCon      -- family tycon (`F')
+                 -> [Type]     -- type instance (`ts')
+                 -> TyCon      -- representation tycon (`R')
+                 -> TyCon      -- => coercion tycon (`Co')
+mkFamInstCoercion name tvs family instTys rep_tycon
+  = mkCoercionTyCon name coArity rule
+  where
+    coArity = length tvs
+    rule args = (substTyWith tvs args $                     -- with sigma = [tys/tvs],
+                  TyConApp family instTys,          --       sigma (F ts)
+                TyConApp rep_tycon args)            --   :=: R tys

 
 --------------------------------------
 -- Coercion Type Constructors...
 
 --------------------------------------
 -- Coercion Type Constructors...

@@ -308,48 +364,44 @@ mkNewTypeCoercion name tycon tvs rhs_ty
 --    sym d :: p2=q2
 --    sym e :: p3=q3
 -- then ((sym c) (sym d) (sym e)) :: (p1 p2 p3)=(q1 q2 q3)
 --    sym d :: p2=q2
 --    sym e :: p3=q3
 -- then ((sym c) (sym d) (sym e)) :: (p1 p2 p3)=(q1 q2 q3)

---
--- (mkKindingFun f) is given the args [c, sym d, sym e]
-mkKindingFun :: ([Type] -> (Type, Type, [Type])) -> [Type] -> Kind
-mkKindingFun f args = 
-  let (ty1, ty2, rest) = f args in 
-  let (argtys1, argtys2) = unzip (map coercionKind rest) in
-  mkCoKind (mkAppTys ty1 argtys1) (mkAppTys ty2 argtys2)
-        

 
 

-symCoercionTyCon, transCoercionTyCon, leftCoercionTyCon, rightCoercionTyCon, instCoercionTyCon :: TyCon
+symCoercionTyCon, transCoercionTyCon, leftCoercionTyCon, rightCoercionTyCon, instCoercionTyCon, unsafeCoercionTyCon :: TyCon

 -- Each coercion TyCon is built with the special CoercionTyCon record and
 -- carries its own kinding rule.  Such CoercionTyCons must be fully applied
 -- by any TyConApp in which they are applied, however they may also be over
 -- applied (see example above) and the kinding function must deal with this.
 symCoercionTyCon = 
 -- Each coercion TyCon is built with the special CoercionTyCon record and
 -- carries its own kinding rule.  Such CoercionTyCons must be fully applied
 -- by any TyConApp in which they are applied, however they may also be over
 -- applied (see example above) and the kinding function must deal with this.
 symCoercionTyCon = 

-  mkCoercionTyCon symCoercionTyConName 1 (mkKindingFun flipCoercionKindOf)
+  mkCoercionTyCon symCoercionTyConName 1 flipCoercionKindOf

   where
   where

-    flipCoercionKindOf (co:rest) = (ty2, ty1, rest)
+    flipCoercionKindOf (co:rest) = ASSERT( null rest ) (ty2, ty1)

        where
          (ty1, ty2) = coercionKind co
 
 transCoercionTyCon = 
        where
          (ty1, ty2) = coercionKind co
 
 transCoercionTyCon = 

-  mkCoercionTyCon transCoercionTyConName 2 (mkKindingFun composeCoercionKindsOf)
+  mkCoercionTyCon transCoercionTyConName 2 composeCoercionKindsOf

   where
   where

-    composeCoercionKindsOf (co1:co2:rest) = 
-        WARN( not (r1 `coreEqType` a2), text "Strange! Type mismatch in trans coercion, probably a bug")
-        (a1, r2, rest)
+    composeCoercionKindsOf (co1:co2:rest)
+      = ASSERT( null rest )
+        WARN( not (r1 `coreEqType` a2), 
+              text "Strange! Type mismatch in trans coercion, probably a bug"
+              $$
+              ppr r1 <+> text "=/=" <+> ppr a2)
+        (a1, r2)

       where
         (a1, r1) = coercionKind co1
         (a2, r2) = coercionKind co2 
 
 leftCoercionTyCon =
       where
         (a1, r1) = coercionKind co1
         (a2, r2) = coercionKind co2 
 
 leftCoercionTyCon =

-  mkCoercionTyCon leftCoercionTyConName 1 (mkKindingFun leftProjectCoercionKindOf)
+  mkCoercionTyCon leftCoercionTyConName 1 leftProjectCoercionKindOf

   where
   where

-    leftProjectCoercionKindOf (co:rest) = (ty1, ty2, rest)
+    leftProjectCoercionKindOf (co:rest) = ASSERT( null rest ) (ty1, ty2)

       where
         (ty1,ty2) = fst (splitCoercionKindOf co)
 
 rightCoercionTyCon =
       where
         (ty1,ty2) = fst (splitCoercionKindOf co)
 
 rightCoercionTyCon =

-  mkCoercionTyCon rightCoercionTyConName 1 (mkKindingFun rightProjectCoercionKindOf)
+  mkCoercionTyCon rightCoercionTyConName 1 rightProjectCoercionKindOf

   where
   where

-    rightProjectCoercionKindOf (co:rest) = (ty1, ty2, rest)
+    rightProjectCoercionKindOf (co:rest) = ASSERT( null rest ) (ty1, ty2)

       where
         (ty1,ty2) = snd (splitCoercionKindOf co)
 
       where
         (ty1,ty2) = snd (splitCoercionKindOf co)
 

@@ -363,53 +415,157 @@ splitCoercionKindOf co
   , Just (ty_fun1, ty_arg1) <- splitAppTy_maybe ty1
   , Just (ty_fun2, ty_arg2) <- splitAppTy_maybe ty2
   = ((ty_fun1, ty_fun2),(ty_arg1, ty_arg2))
   , Just (ty_fun1, ty_arg1) <- splitAppTy_maybe ty1
   , Just (ty_fun2, ty_arg2) <- splitAppTy_maybe ty2
   = ((ty_fun1, ty_fun2),(ty_arg1, ty_arg2))

+splitCoercionKindOf co 
+  = pprPanic "Coercion.splitCoercionKindOf" 
+             (ppr co $$ ppr (coercionKindPredTy co))

 
 instCoercionTyCon 
 
 instCoercionTyCon 

-  =  mkCoercionTyCon instCoercionTyConName 2 (mkKindingFun instCoercionKind)
+  =  mkCoercionTyCon instCoercionTyConName 2 instCoercionKind

   where
     instantiateCo t s =
       let Just (tv, ty) = splitForAllTy_maybe t in
       substTyWith [tv] [s] ty
 
   where
     instantiateCo t s =
       let Just (tv, ty) = splitForAllTy_maybe t in
       substTyWith [tv] [s] ty
 

-    instCoercionKind (co1:ty:rest) = (instantiateCo t1 ty, instantiateCo t2 ty, rest)
+    instCoercionKind (co1:ty:rest) = ASSERT( null rest )
+                                    (instantiateCo t1 ty, instantiateCo t2 ty)

       where (t1, t2) = coercionKind co1
 
 unsafeCoercionTyCon 
       where (t1, t2) = coercionKind co1
 
 unsafeCoercionTyCon 

-  = mkCoercionTyCon unsafeCoercionTyConName 2 (mkKindingFun unsafeCoercionKind)
+  = mkCoercionTyCon unsafeCoercionTyConName 2 unsafeCoercionKind

   where
   where

-   unsafeCoercionKind (ty1:ty2:rest) = (ty1,ty2,rest) 
+   unsafeCoercionKind (ty1:ty2:rest) = ASSERT( null rest ) (ty1,ty2) 

         
 --------------------------------------
 -- ...and their names
 
         
 --------------------------------------
 -- ...and their names
 

+mkCoConName :: FastString -> Unique -> TyCon -> Name

 mkCoConName occ key coCon = mkWiredInName gHC_PRIM (mkOccNameFS tcName occ)
 mkCoConName occ key coCon = mkWiredInName gHC_PRIM (mkOccNameFS tcName occ)

-                            key Nothing (ATyCon coCon) BuiltInSyntax
+                            key (ATyCon coCon) BuiltInSyntax
+
+transCoercionTyConName, symCoercionTyConName, leftCoercionTyConName, rightCoercionTyConName, instCoercionTyConName, unsafeCoercionTyConName :: Name

 
 

-transCoercionTyConName = mkCoConName FSLIT("trans") transCoercionTyConKey transCoercionTyCon
-symCoercionTyConName   = mkCoConName FSLIT("sym") symCoercionTyConKey symCoercionTyCon
-leftCoercionTyConName  = mkCoConName FSLIT("left") leftCoercionTyConKey leftCoercionTyCon
-rightCoercionTyConName = mkCoConName FSLIT("right") rightCoercionTyConKey rightCoercionTyCon
-instCoercionTyConName  = mkCoConName FSLIT("inst") instCoercionTyConKey instCoercionTyCon
-unsafeCoercionTyConName = mkCoConName FSLIT("CoUnsafe") unsafeCoercionTyConKey unsafeCoercionTyCon
+transCoercionTyConName = mkCoConName (fsLit "trans") transCoercionTyConKey transCoercionTyCon
+symCoercionTyConName   = mkCoConName (fsLit "sym") symCoercionTyConKey symCoercionTyCon
+leftCoercionTyConName  = mkCoConName (fsLit "left") leftCoercionTyConKey leftCoercionTyCon
+rightCoercionTyConName = mkCoConName (fsLit "right") rightCoercionTyConKey rightCoercionTyCon
+instCoercionTyConName  = mkCoConName (fsLit "inst") instCoercionTyConKey instCoercionTyCon
+unsafeCoercionTyConName = mkCoConName (fsLit "CoUnsafe") unsafeCoercionTyConKey unsafeCoercionTyCon

 
 
 
 
 
 

+instNewTyCon_maybe :: TyCon -> [Type] -> Maybe (Type, CoercionI)
+-- instNewTyCon_maybe T ts
+--     = Just (rep_ty, co)     if   co : T ts ~ rep_ty
+instNewTyCon_maybe tc tys
+  | Just (tvs, ty, mb_co_tc) <- unwrapNewTyCon_maybe tc
+  = ASSERT( tys `lengthIs` tyConArity tc )
+    Just (substTyWith tvs tys ty, 
+         case mb_co_tc of
+          Nothing    -> IdCo
+          Just co_tc -> ACo (mkTyConApp co_tc tys))
+  | otherwise
+  = Nothing
+

 -- this is here to avoid module loops
 splitNewTypeRepCo_maybe :: Type -> Maybe (Type, Coercion)  
 -- Sometimes we want to look through a newtype and get its associated coercion
 -- It only strips *one layer* off, so the caller will usually call itself recursively
 -- Only applied to types of kind *, hence the newtype is always saturated
 -- this is here to avoid module loops
 splitNewTypeRepCo_maybe :: Type -> Maybe (Type, Coercion)  
 -- Sometimes we want to look through a newtype and get its associated coercion
 -- It only strips *one layer* off, so the caller will usually call itself recursively
 -- Only applied to types of kind *, hence the newtype is always saturated

+--    splitNewTypeRepCo_maybe ty
+--     = Just (ty', co)  if   co : ty ~ ty'
+-- Returns Nothing for non-newtypes or fully-transparent newtypes

 splitNewTypeRepCo_maybe ty 
   | Just ty' <- coreView ty = splitNewTypeRepCo_maybe ty'
 splitNewTypeRepCo_maybe (TyConApp tc tys)
 splitNewTypeRepCo_maybe ty 
   | Just ty' <- coreView ty = splitNewTypeRepCo_maybe ty'
 splitNewTypeRepCo_maybe (TyConApp tc tys)

-  | isNewTyCon tc 
-  = ASSERT( tys `lengthIs` tyConArity tc )     -- splitNewTypeRepCo_maybe only be applied 
-                                                --     to *types* (of kind *)
-        case newTyConRhs tc of
-         (tvs, rep_ty) -> 
-              ASSERT( length tvs == length tys )
-             Just (substTyWith tvs tys rep_ty, mkTyConApp co_con tys)
-  where
-    co_con = maybe (pprPanic "splitNewTypeRepCo_maybe" (ppr tc)) id (newTyConCo tc)
-splitNewTypeRepCo_maybe other = Nothing
+  | Just (ty', coi) <- instNewTyCon_maybe tc tys
+  = case coi of
+       ACo co -> Just (ty', co)
+       IdCo   -> panic "splitNewTypeRepCo_maybe"
+                       -- This case handled by coreView
+splitNewTypeRepCo_maybe _
+  = Nothing
+
+-------------------------------------
+-- Syntactic equality of coercions
+
+coreEqCoercion :: Coercion -> Coercion -> Bool
+coreEqCoercion = coreEqType

 \end{code}
 \end{code}

+
+
+--------------------------------------
+-- CoercionI smart constructors
+--     lifted smart constructors of ordinary coercions
+
+\begin{code}
+       -- CoercionI is either 
+       --      (a) proper coercion
+       --      (b) the identity coercion
+data CoercionI = IdCo | ACo Coercion
+
+isIdentityCoercion :: CoercionI -> Bool
+isIdentityCoercion IdCo = True
+isIdentityCoercion _    = False
+
+allIdCos :: [CoercionI] -> Bool
+allIdCos = all isIdentityCoercion
+
+zipCoArgs :: [CoercionI] -> [Type] -> [Coercion]
+zipCoArgs cois tys = zipWith fromCoI cois tys
+
+fromCoI :: CoercionI -> Type -> Type
+fromCoI IdCo ty     = ty       -- Identity coercion represented 
+fromCoI (ACo co) _  = co       --      by the type itself
+
+mkSymCoI :: CoercionI -> CoercionI
+mkSymCoI IdCo = IdCo
+mkSymCoI (ACo co) = ACo $ mkCoercion symCoercionTyCon [co] 
+                               -- the smart constructor
+                               -- is too smart with tyvars
+
+mkTransCoI :: CoercionI -> CoercionI -> CoercionI
+mkTransCoI IdCo aco = aco
+mkTransCoI aco IdCo = aco
+mkTransCoI (ACo co1) (ACo co2) = ACo $ mkTransCoercion co1 co2
+
+mkTyConAppCoI :: TyCon -> [Type] -> [CoercionI] -> CoercionI
+mkTyConAppCoI tyCon tys cois
+  | allIdCos cois = IdCo
+  | otherwise    = ACo (TyConApp tyCon (zipCoArgs cois tys))
+
+mkAppTyCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI
+mkAppTyCoI _   IdCo _   IdCo = IdCo
+mkAppTyCoI ty1 coi1 ty2 coi2 =
+       ACo $ AppTy (fromCoI coi1 ty1) (fromCoI coi2 ty2)
+
+mkFunTyCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI
+mkFunTyCoI _   IdCo _   IdCo = IdCo
+mkFunTyCoI ty1 coi1 ty2 coi2 =
+       ACo $ FunTy (fromCoI coi1 ty1) (fromCoI coi2 ty2)
+
+mkForAllTyCoI :: TyVar -> CoercionI -> CoercionI
+mkForAllTyCoI _ IdCo = IdCo
+mkForAllTyCoI tv (ACo co) = ACo $ ForAllTy tv co
+
+fromACo :: CoercionI -> Coercion
+fromACo (ACo co) = co
+
+mkClassPPredCoI :: Class -> [Type] -> [CoercionI] -> CoercionI
+-- mkClassPPredCoI cls tys cois = coi
+--    coi : PredTy (cls tys) ~ predTy (cls (tys `cast` cois))
+mkClassPPredCoI cls tys cois 
+  | allIdCos cois = IdCo
+  | otherwise     = ACo $ PredTy $ ClassP cls (zipCoArgs cois tys)
+
+mkIParamPredCoI :: (IPName Name) -> CoercionI -> CoercionI 
+-- Similar invariant to mkclassPPredCoI
+mkIParamPredCoI _   IdCo     = IdCo
+mkIParamPredCoI ipn (ACo co) = ACo $ PredTy $ IParam ipn co
+
+mkEqPredCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI
+-- Similar invariant to mkclassPPredCoI
+mkEqPredCoI _    IdCo     _   IdCo      = IdCo
+mkEqPredCoI ty1  IdCo     _   (ACo co2) = ACo $ PredTy $ EqPred ty1 co2
+mkEqPredCoI _   (ACo co1) ty2 coi2      = ACo $ PredTy $ EqPred co1 (fromCoI coi2 ty2)
+\end{code}
+