Use OPTIONS rather than OPTIONS_GHC for pragmas

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

diff --git a/compiler/types/Coercion.lhs b/compiler/types/Coercion.lhs
index 55a282d..ac2173c 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 -w #-}
+-- 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/CodingStyle#Warnings
+-- for details
+

 module Coercion (
         Coercion,
  
 module Coercion (
         Coercion,
  

@@ -19,43 +29,48 @@ 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
+
+       -- CoercionI
+       CoercionI(..),
+       isIdentityCoercion,
+       mkSymCoI, mkTransCoI, 
+       mkTyConAppCoI, mkAppTyCoI, mkFunTyCoI,
+       mkNoteTyCoI, 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
 
 

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

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

@@ -99,17 +114,11 @@ 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)
 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 +126,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)

@@ -166,61 +176,82 @@ 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      
   | 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]
+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
 

@@ -277,7 +308,7 @@ 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.  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 
 -- implement the unsafeCoerce# primitive.
 mkUnsafeCoercion :: Type -> Type -> Coercion
 mkUnsafeCoercion ty1 ty2 

@@ -286,11 +317,32 @@ mkUnsafeCoercion ty1 ty2
 
 -- See note [Newtype coercions] in TyCon
 mkNewTypeCoercion :: Name -> TyCon -> [TyVar] -> Type -> TyCon
 
 -- See note [Newtype coercions] in 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 (TyConApp tycon args) (substTyWith tvs args rhs_ty)
+    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...

@@ -301,14 +353,6 @@ 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

@@ -316,33 +360,34 @@ symCoercionTyCon, transCoercionTyCon, leftCoercionTyCon, rightCoercionTyCon, ins
 -- 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) = 
+    composeCoercionKindsOf (co1:co2:rest)
+      = ASSERT( null rest )

         WARN( not (r1 `coreEqType` a2), text "Strange! Type mismatch in trans coercion, probably a bug")
         WARN( not (r1 `coreEqType` a2), text "Strange! Type mismatch in trans coercion, probably a bug")

-        (a1, r2, rest)
+        (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)
 

@@ -358,25 +403,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

@@ -387,22 +433,117 @@ unsafeCoercionTyConName = mkCoConName FSLIT("CoUnsafe") unsafeCoercionTyConKey u
 
 
 
 
 
 

+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 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
+
+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) ty = 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 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
+
+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 ipn 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 ty1 (ACo co1) ty2 coi2      = ACo $ PredTy $ EqPred co1 (fromCoI coi2 ty2)

 \end{code}
 \end{code}

+