White-space only

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

diff --git a/compiler/types/Coercion.lhs b/compiler/types/Coercion.lhs
index 8f08d35..1e071eb 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. 

@@ -22,43 +25,46 @@ module Coercion (
         mkSymCoercion, mkTransCoercion,
         mkLeftCoercion, mkRightCoercion, mkInstCoercion, mkAppCoercion,
         mkForAllCoercion, mkFunCoercion, mkInstsCoercion, mkUnsafeCoercion,
         mkSymCoercion, mkTransCoercion,
         mkLeftCoercion, mkRightCoercion, mkInstCoercion, mkAppCoercion,
         mkForAllCoercion, mkFunCoercion, mkInstsCoercion, mkUnsafeCoercion,

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

 
         splitNewTypeRepCo_maybe, decomposeCo,
 
         unsafeCoercionTyCon, symCoercionTyCon,
         transCoercionTyCon, leftCoercionTyCon, 
 
         splitNewTypeRepCo_maybe, decomposeCo,
 
         unsafeCoercionTyCon, symCoercionTyCon,
         transCoercionTyCon, leftCoercionTyCon, 

-        rightCoercionTyCon, instCoercionTyCon -- needed by TysWiredIn
+        rightCoercionTyCon, instCoercionTyCon, -- needed by TysWiredIn
+
+       -- CoercionI
+       CoercionI(..),
+       isIdentityCoercion,
+       mkSymCoI, mkTransCoI, 
+       mkTyConAppCoI, mkAppTyCoI, mkFunTyCoI,
+       mkNoteTyCoI, mkForAllTyCoI,
+       fromCoI,
+       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
-                  )
-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
 
 

-

 ------------------------------
 decomposeCo :: Arity -> Coercion -> [Coercion]
 -- (decomposeCo 3 c) = [right (left (left c)), right (left c), right c]
 ------------------------------
 decomposeCo :: Arity -> Coercion -> [Coercion]
 -- (decomposeCo 3 c) = [right (left (left c)), right (left c), right c]

+-- So this breaks a coercion with kind T A B C :=: T D E F into
+-- a list of coercions of kinds A :=: D, B :=: E and E :=: F

 decomposeCo n co
   = go n co []
   where
 decomposeCo n co
   = go n co []
   where

@@ -96,28 +102,26 @@ splitCoercionKind_maybe co | Just co' <- kindView co = splitCoercionKind_maybe c
 splitCoercionKind_maybe (PredTy (EqPred ty1 ty2)) = Just (ty1, ty2)
 splitCoercionKind_maybe other = Nothing
 
 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)
 
 coercionKind :: Coercion -> (Type, Type)
 --     c :: (t1 :=: t2)
 -- Then (coercionKind c) = (t1,t2)
 type Coercion     = Type
 type CoercionKind = Kind       -- A CoercionKind is always of form (ty1 :=: ty2)
 
 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
     (mkAppTy t1 s1, mkAppTy t2 s2)
 coercionKind (TyConApp tc args)
   | Just (ar, rule) <- isCoercionTyCon_maybe tc 
 coercionKind (AppTy ty1 ty2) 
   = let (t1, t2) = coercionKind ty1
         (s1, s2) = coercionKind ty2 in
     (mkAppTy t1 s1, mkAppTy t2 s2)
 coercionKind (TyConApp tc args)
   | Just (ar, rule) <- isCoercionTyCon_maybe tc 

-  = if length args >= ar 
-    then splitCoercionKind (rule args)
-    else pprPanic ("arity/arguments mismatch in coercionKind:") 
-             (ppr ar $$ ppr tc <+> ppr args)
+    -- CoercionTyCons carry their kinding rule, so we use it here
+  = 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)

@@ -162,40 +166,72 @@ mkAppsCoercion   co1 tys = foldl mkAppTy co1 tys
 mkForAllCoercion tv  co  = ASSERT ( isTyVar tv ) mkForAllTy tv co
 mkFunCoercion    co1 co2 = mkFunTy co1 co2
 
 mkForAllCoercion tv  co  = ASSERT ( isTyVar tv ) mkForAllTy tv co
 mkFunCoercion    co1 co2 = mkFunTy co1 co2
 

-mkSymCoercion co      
-  | Just co2 <- splitSymCoercion_maybe co = co2
-  | Just (co1, co2) <- splitAppCoercion_maybe co 
-    -- should make this case better
-  = mkAppCoercion (mkSymCoercion co1) (mkSymCoercion co2)
-  | Just (co1, co2) <- splitTransCoercion_maybe co
-  = mkTransCoercion (mkSymCoercion co1) (mkSymCoercion co2)
-  | Just (co, ty) <- splitInstCoercion_maybe co
-  = mkInstCoercion (mkSymCoercion co) ty
-  | Just co <- splitLeftCoercion_maybe co
-  = mkLeftCoercion (mkSymCoercion co)
-  | Just co <- splitRightCoercion_maybe co
-  = mkRightCoercion (mkSymCoercion co)
-mkSymCoercion (ForAllTy tv ty) = ForAllTy tv (mkSymCoercion ty)
--- for atomic types and constructors, we can just ignore sym since these
+
+-------------------------------
+-- 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
 -- are reflexive coercions

+mkSymCoercion 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)
+     -- Note reversal of arguments!
+  = mkTransCoercion (mkSymCoercion co2) (mkSymCoercion co1)
+
+  | tc `hasKey` instCoercionTyConKey
+     -- sym (co @ ty) --> (sym co) @ ty
+     -- 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] 
-                   -- this should not happen but does
+  | 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      
   | Just (co1, co2) <- splitAppCoercion_maybe co = co2
   | otherwise = mkCoercion rightCoercionTyCon [co]
 
 
 mkRightCoercion  co      
   | Just (co1, co2) <- splitAppCoercion_maybe co = co2
   | otherwise = mkCoercion rightCoercionTyCon [co]
 

-mkTransCoercion co1 co2 = mkCoercion transCoercionTyCon [co1, co2]
-
-mkInstCoercion  co ty = mkCoercion instCoercionTyCon  [co, ty]
+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
 

@@ -252,19 +288,41 @@ splitRightCoercion_maybe (TyConApp tc [co])
 splitRightCoercion_maybe other = Nothing
 
 -- Unsafe coercion is not safe, it is used when we know we are dealing with
 splitRightCoercion_maybe other = Nothing
 
 -- 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
+-- 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]
 
 
 mkUnsafeCoercion :: Type -> Type -> Coercion
 mkUnsafeCoercion ty1 ty2 
   = mkCoercion unsafeCoercionTyCon [ty1, ty2]
 
 

--- make the coercion associated with a newtype
+-- 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
+    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
   where

-    rule args = mkCoKind (substTyWith tvs args rhs_ty) (TyConApp tycon args)
+    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...

@@ -275,46 +333,41 @@ 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
 -- Each coercion TyCon is built with the special CoercionTyCon record and
 
 symCoercionTyCon, transCoercionTyCon, leftCoercionTyCon, rightCoercionTyCon, instCoercionTyCon :: TyCon
 -- Each coercion TyCon is built with the special CoercionTyCon record and

--- carries its won kinding rule.  Such CoercionTyCons must be fully applied
+-- 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 = 
 -- 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) = (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")
+        (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)
 

@@ -330,25 +383,26 @@ splitCoercionKindOf co
   = ((ty_fun1, ty_fun2),(ty_arg1, ty_arg2))
 
 instCoercionTyCon 
   = ((ty_fun1, ty_fun2),(ty_arg1, ty_arg2))
 
 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
 
 mkCoConName occ key coCon = mkWiredInName gHC_PRIM (mkOccNameFS tcName occ)
         
 --------------------------------------
 -- ...and their names
 
 mkCoConName occ key coCon = mkWiredInName gHC_PRIM (mkOccNameFS tcName occ)

-                            key Nothing (ATyCon coCon) BuiltInSyntax
+                            key (ATyCon coCon) BuiltInSyntax

 
 transCoercionTyConName = mkCoConName FSLIT("trans") transCoercionTyConKey transCoercionTyCon
 symCoercionTyConName   = mkCoConName FSLIT("sym") symCoercionTyConKey symCoercionTyCon
 
 transCoercionTyConName = mkCoConName FSLIT("trans") transCoercionTyConKey transCoercionTyCon
 symCoercionTyConName   = mkCoConName FSLIT("sym") symCoercionTyConKey symCoercionTyCon

@@ -361,13 +415,13 @@ unsafeCoercionTyConName = mkCoConName FSLIT("CoUnsafe") unsafeCoercionTyConKey u
 
 -- this is here to avoid module loops
 splitNewTypeRepCo_maybe :: Type -> Maybe (Type, Coercion)  
 
 -- this is here to avoid module loops
 splitNewTypeRepCo_maybe :: Type -> Maybe (Type, Coercion)  

--- Sometimes we want to look through a recursive newtype, and that's what happens here
+-- 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' <- coreView ty = splitNewTypeRepCo_maybe ty'
 splitNewTypeRepCo_maybe (TyConApp tc tys)
 -- 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' <- coreView ty = splitNewTypeRepCo_maybe ty'
 splitNewTypeRepCo_maybe (TyConApp tc tys)

-  | isNewTyCon tc 
+  | isClosedNewTyCon tc 

   = ASSERT( tys `lengthIs` tyConArity tc )     -- splitNewTypeRepCo_maybe only be applied 
                                                 --     to *types* (of kind *)
         case newTyConRhs tc of
   = ASSERT( tys `lengthIs` tyConArity tc )     -- splitNewTypeRepCo_maybe only be applied 
                                                 --     to *types* (of kind *)
         case newTyConRhs tc of

@@ -375,7 +429,95 @@ splitNewTypeRepCo_maybe (TyConApp tc tys)
               ASSERT( length tvs == length tys )
              Just (substTyWith tvs tys rep_ty, mkTyConApp co_con tys)
   where
               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)
-
+    co_con = maybe (pprPanic "splitNewTypeRepCo_maybe" (ppr tc)) id (newTyConCo_maybe tc)

 splitNewTypeRepCo_maybe other = Nothing
 \end{code}
 splitNewTypeRepCo_maybe other = Nothing
 \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
+
+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 =
+       let (anyAcon,co_args) = f tys cois
+       in if anyAcon
+               then ACo (TyConApp tyCon co_args)
+               else IdCo
+       where
+               f [] [] = (False,[])
+               f (x:xs) (y:ys) = 
+                       let (b,cos) = f xs ys
+                       in case y of
+                               IdCo   -> (b,x:cos)
+                               ACo co -> (True,co:cos)
+
+mkAppTyCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI
+mkAppTyCoI ty1 IdCo ty2 IdCo = IdCo
+mkAppTyCoI ty1 coi1 ty2 coi2 =
+       ACo $ AppTy (fromCoI coi1 ty1) (fromCoI coi2 ty2)
+
+mkFunTyCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI
+mkFunTyCoI ty1 IdCo ty2 IdCo = IdCo
+mkFunTyCoI ty1 coi1 ty2 coi2 =
+       ACo $ FunTy (fromCoI coi1 ty1) (fromCoI coi2 ty2)
+
+mkNoteTyCoI :: TyNote -> CoercionI -> CoercionI
+mkNoteTyCoI _ IdCo = IdCo
+mkNoteTyCoI note (ACo co) = ACo $ NoteTy note co
+
+mkForAllTyCoI :: TyVar -> CoercionI -> CoercionI
+mkForAllTyCoI _ IdCo = IdCo
+mkForAllTyCoI tv (ACo co) = ACo $ ForAllTy tv co
+
+fromCoI IdCo ty     = ty
+fromCoI (ACo co) ty = co
+
+mkClassPPredCoI :: Class -> [Type] -> [CoercionI] -> CoercionI
+mkClassPPredCoI cls tys cois =
+       let (anyAcon,co_args) = f tys cois
+       in if anyAcon
+               then ACo $ PredTy $ ClassP cls co_args
+               else IdCo
+       where
+               f [] [] = (False,[])
+               f (x:xs) (y:ys) = 
+                       let (b,cos) = f xs ys
+                       in case y of
+                               IdCo   -> (b,x:cos)
+                               ACo co -> (True,co:cos)
+
+mkIParamPredCoI :: (IPName Name) -> CoercionI -> CoercionI 
+mkIParamPredCoI ipn IdCo     = IdCo
+mkIParamPredCoI ipn (ACo co) = ACo $ PredTy $ IParam ipn co
+
+mkEqPredCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI
+mkEqPredCoI _    IdCo     _   IdCo      = IdCo
+mkEqPredCoI ty1  IdCo     _   (ACo co2) = ACo $ PredTy $ EqPred ty1 co2
+mkEqPredCoI ty1 (ACo co1) ty2 coi2      = ACo $ PredTy $ EqPred co1 (fromCoI coi2 ty2)
+
+\end{code}
+