A (final) re-engineering of the new typechecker

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

diff --git a/compiler/types/Coercion.lhs b/compiler/types/Coercion.lhs
index dcd10fc..faab463 100644 (file)
--- a/compiler/types/Coercion.lhs
+++ b/compiler/types/Coercion.lhs
@@ -44,8 +44,9 @@ module Coercion (
         mkForAllCoercion, mkInstsCoercion, mkUnsafeCoercion,
         mkNewTypeCoercion, mkFamInstCoercion, mkAppsCoercion,
         mkCsel1Coercion, mkCsel2Coercion, mkCselRCoercion, 
-                       
-        mkCoVarCoercion, 
+
+       mkClassPPredCo, mkIParamPredCo, mkEqPredCo, 
+        mkCoVarCoercion, mkCoPredCo, 
 
 
         unsafeCoercionTyCon, symCoercionTyCon,
@@ -68,7 +69,7 @@ module Coercion (
        mkTyConAppCoI, mkAppTyCoI, mkFunTyCoI,
        mkForAllTyCoI,
        fromCoI, 
-       mkClassPPredCoI, mkIParamPredCoI, mkEqPredCoI
+       mkClassPPredCoI, mkIParamPredCoI, mkEqPredCoI, mkCoPredCoI 
 
        ) where 
 
@@ -80,6 +81,7 @@ import TyCon
 import Class
 import Var
 import VarEnv
+import VarSet
 import Name
 import PrelNames
 import Util
@@ -276,7 +278,15 @@ mkCoKind ty1 ty2 = PredTy (EqPred ty1 ty2)
 
 -- | (mkCoPredTy s t r) produces the type:   (s~t) => r
 mkCoPredTy :: Type -> Type -> Type -> Type
-mkCoPredTy s t r = ForAllTy (mkWildCoVar (mkCoKind s t)) r
+mkCoPredTy s t r = ASSERT( not (co_var `elemVarSet` tyVarsOfType r) )
+                   ForAllTy co_var r
+  where
+    co_var = mkWildCoVar (mkCoKind s t)
+
+mkCoPredCo :: Coercion -> Coercion -> Coercion -> Coercion 
+-- Creates a coercion between (s1~t1) => r1  and (s2~t2) => r2 
+mkCoPredCo = mkCoPredTy 
+
 
 splitCoPredTy_maybe :: Type -> Maybe (Type, Type, Type)
 splitCoPredTy_maybe ty
@@ -343,7 +353,7 @@ mkTyConCoercion con cos = mkTyConApp con cos
 
 -- | Make a function 'Coercion' between two other 'Coercion's
 mkFunCoercion :: Coercion -> Coercion -> Coercion
-mkFunCoercion co1 co2 = mkFunTy co1 co2
+mkFunCoercion co1 co2 = mkFunTy co1 co2 -- NB: Handles correctly the forall for eqpreds!
 
 -- | Make a 'Coercion' which binds a variable within an inner 'Coercion'
 mkForAllCoercion :: Var -> Coercion -> Coercion
@@ -440,6 +450,18 @@ mkFamInstCoercion name tvs family inst_tys rep_tycon
     desc = CoAxiom { co_ax_tvs = tvs
                    , co_ax_lhs = mkTyConApp family inst_tys 
                    , co_ax_rhs = mkTyConApp rep_tycon (mkTyVarTys tvs) }
+
+
+mkClassPPredCo :: Class -> [Coercion] -> Coercion
+mkClassPPredCo cls = (PredTy . ClassP cls)
+
+mkIParamPredCo :: (IPName Name) -> Coercion -> Coercion
+mkIParamPredCo ipn = (PredTy . IParam ipn)
+
+mkEqPredCo :: Coercion -> Coercion -> Coercion 
+mkEqPredCo co1 co2 = PredTy (EqPred co1 co2)
+
+
 \end{code}
 
 
@@ -676,6 +698,11 @@ mkIParamPredCoI ipn = liftCoI (PredTy . IParam ipn)
 -- | Smart constructor for type equality 'Coercion's on 'CoercionI'. Similar to 'mkClassPPredCoI'
 mkEqPredCoI :: CoercionI -> CoercionI -> CoercionI
 mkEqPredCoI = liftCoI2 (\t1 t2 -> PredTy (EqPred t1 t2))
+
+mkCoPredCoI :: CoercionI -> CoercionI -> CoercionI -> CoercionI 
+mkCoPredCoI coi1 coi2 coi3 =   mkFunTyCoI (mkEqPredCoI coi1 coi2) coi3
+
+
 \end{code}
 
 %************************************************************************
@@ -720,7 +747,8 @@ predKind (IParam {}) = liftedTypeKind       -- always represented by lifted types
 --
 -- > c :: (t1 ~ t2)
 --
--- i.e. the kind of @c@ is a 'CoercionKind' relating @t1@ and @t2@, then @coercionKind c = (t1, t2)@.
+-- i.e. the kind of @c@ is a 'CoercionKind' relating @t1@ and @t2@, 
+-- then @coercionKind c = (t1, t2)@.
 coercionKind :: Coercion -> (Type, Type)
 coercionKind ty@(TyVarTy a) | isCoVar a = coVarKind a
                             | otherwise = (ty, ty)
@@ -822,5 +850,8 @@ coTyConAppKind (CoAxiom { co_ax_tvs = tvs
   = (substTyWith tvs tys1 lhs_ty, substTyWith tvs tys2 rhs_ty)
   where
     (tys1, tys2) = coercionKinds cos
-coTyConAppKind desc cos = pprPanic "coTyConAppKind" (ppr desc $$ ppr cos)
+coTyConAppKind desc cos = pprTrace "coTyConAppKind" (ppr desc $$ braces (vcat 
+                             [ ppr co <+> dcolon <+> pprEqPred (coercionKind co)
+                             | co <- cos ])) $
+                          coercionKind (head cos)
 \end{code}