X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypes%2FCoercion.lhs;h=ca1b1a68154fc88a18206d3dcf7e260e8fd9987e;hp=cb85028ce8add7c56b21664ff880f91476b7fc15;hb=b00b5bc04ff36a551552470060064f0b7d84ca30;hpb=a7bda9e63ce091e4f33b6058a96686d7cde3d40d

diff --git a/compiler/types/Coercion.lhs b/compiler/types/Coercion.lhs
index cb85028..ca1b1a6 100644
--- a/compiler/types/Coercion.lhs
+++ b/compiler/types/Coercion.lhs
@@ -22,7 +22,7 @@ module Coercion (
         mkSymCoercion, mkTransCoercion,
         mkLeftCoercion, mkRightCoercion, mkInstCoercion, mkAppCoercion,
         mkForAllCoercion, mkFunCoercion, mkInstsCoercion, mkUnsafeCoercion,
-        mkNewTypeCoercion, mkAppsCoercion,
+        mkNewTypeCoercion, mkDataInstCoercion, mkAppsCoercion,
 
         splitNewTypeRepCo_maybe, decomposeCo,
 
@@ -39,8 +39,8 @@ import Type	  ( Type, Kind, PredType, substTyWith, mkAppTy, mkForAllTy,
                     kindView, mkTyConApp, isCoercionKind, isEqPred, mkAppTys,
                     coreEqType, splitAppTys, isTyVarTy, splitTyConApp_maybe
                   )
-import TyCon      ( TyCon, tyConArity, mkCoercionTyCon, isNewTyCon,
-                    newTyConRhs, newTyConCo, 
+import TyCon      ( TyCon, tyConArity, mkCoercionTyCon, isClosedNewTyCon,
+                    newTyConRhs, newTyConCo_maybe, 
                     isCoercionTyCon, isCoercionTyCon_maybe )
 import Var	  ( Var, TyVar, isTyVar, tyVarKind )
 import Name       ( BuiltInSyntax(..), Name, mkWiredInName, tcName )
@@ -108,8 +108,8 @@ 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
@@ -117,10 +117,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
-  = 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)
@@ -277,27 +278,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
--- 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]
 
 
--- 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
+-- See note [Newtype coercions] in TyCon
+mkNewTypeCoercion :: Name -> TyCon -> ([TyVar], Type) -> TyCon
+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 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.
 --
---   CoT S U :: (Int, S, U) :=: T S U
-mkNewTypeCoercion :: Name -> TyCon -> [TyVar] -> Type -> TyCon
-mkNewTypeCoercion name tycon tvs rhs_ty 
-  = ASSERT (length tvs == tyConArity tycon)
-    mkCoercionTyCon name (tyConArity tycon) rule
+mkDataInstCoercion :: 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')
+mkDataInstCoercion name tvs family instTys rep_tycon
+  = mkCoercionTyCon name coArity rule
   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...
@@ -308,14 +323,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)
---
--- (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
@@ -323,33 +330,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 = 
-  mkCoercionTyCon symCoercionTyConName 1 (mkKindingFun flipCoercionKindOf)
+  mkCoercionTyCon symCoercionTyConName 1 flipCoercionKindOf
   where
-    flipCoercionKindOf (co:rest) = (ty2, ty1, rest)
+    flipCoercionKindOf (co:rest) = ASSERT( null rest ) (ty2, ty1)
 	where
 	  (ty1, ty2) = coercionKind co
 
 transCoercionTyCon = 
-  mkCoercionTyCon transCoercionTyConName 2 (mkKindingFun composeCoercionKindsOf)
+  mkCoercionTyCon transCoercionTyConName 2 composeCoercionKindsOf
   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")
-        (a1, r2, rest)
+        (a1, r2)
       where
         (a1, r1) = coercionKind co1
         (a2, r2) = coercionKind co2 
 
 leftCoercionTyCon =
-  mkCoercionTyCon leftCoercionTyConName 1 (mkKindingFun leftProjectCoercionKindOf)
+  mkCoercionTyCon leftCoercionTyConName 1 leftProjectCoercionKindOf
   where
-    leftProjectCoercionKindOf (co:rest) = (ty1, ty2, rest)
+    leftProjectCoercionKindOf (co:rest) = ASSERT( null rest ) (ty1, ty2)
       where
         (ty1,ty2) = fst (splitCoercionKindOf co)
 
 rightCoercionTyCon =
-  mkCoercionTyCon rightCoercionTyConName 1 (mkKindingFun rightProjectCoercionKindOf)
+  mkCoercionTyCon rightCoercionTyConName 1 rightProjectCoercionKindOf
   where
-    rightProjectCoercionKindOf (co:rest) = (ty1, ty2, rest)
+    rightProjectCoercionKindOf (co:rest) = ASSERT( null rest ) (ty1, ty2)
       where
         (ty1,ty2) = snd (splitCoercionKindOf co)
 
@@ -365,25 +373,26 @@ splitCoercionKindOf co
   = ((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
 
-    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 
-  = mkCoercionTyCon unsafeCoercionTyConName 2 (mkKindingFun unsafeCoercionKind)
+  = mkCoercionTyCon unsafeCoercionTyConName 2 unsafeCoercionKind
   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)
-                            key Nothing (ATyCon coCon) BuiltInSyntax
+                            key (ATyCon coCon) BuiltInSyntax
 
 transCoercionTyConName = mkCoConName FSLIT("trans") transCoercionTyConKey transCoercionTyCon
 symCoercionTyConName   = mkCoConName FSLIT("sym") symCoercionTyConKey symCoercionTyCon
@@ -402,7 +411,7 @@ splitNewTypeRepCo_maybe :: Type -> Maybe (Type, Coercion)
 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
@@ -410,6 +419,6 @@ splitNewTypeRepCo_maybe (TyConApp tc tys)
               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}