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

diff --git a/compiler/types/Coercion.lhs b/compiler/types/Coercion.lhs
index 52e4f42..cb85028 100644
--- a/compiler/types/Coercion.lhs
+++ b/compiler/types/Coercion.lhs
@@ -36,7 +36,8 @@ module Coercion (
 import TypeRep
 import Type	  ( Type, Kind, PredType, substTyWith, mkAppTy, mkForAllTy,
                     mkFunTy, splitAppTy_maybe, splitForAllTy_maybe, coreView,
-                    kindView, mkTyConApp, isCoercionKind, isEqPred, mkAppTys
+                    kindView, mkTyConApp, isCoercionKind, isEqPred, mkAppTys,
+                    coreEqType, splitAppTys, isTyVarTy, splitTyConApp_maybe
                   )
 import TyCon      ( TyCon, tyConArity, mkCoercionTyCon, isNewTyCon,
                     newTyConRhs, newTyConCo, 
@@ -59,6 +60,8 @@ import Outputable
 ------------------------------
 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
@@ -105,7 +108,6 @@ 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 (AppTy ty1 ty2) 
@@ -114,6 +116,7 @@ coercionKind (AppTy ty1 ty2)
     (mkAppTy t1 s1, mkAppTy t2 s2)
 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:") 
@@ -162,19 +165,42 @@ mkAppsCoercion   co1 tys = foldl mkAppTy co1 tys
 mkForAllCoercion tv  co  = ASSERT ( isTyVar tv ) mkForAllTy tv co
 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      
   | Just co2 <- splitSymCoercion_maybe co = co2
-  | Just (co1, co2) <- splitAppCoercion_maybe co 
-    -- should make this case better
-  = mkAppCoercion (mkSymCoercion co1) (mkSymCoercion 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
+     -- sym (co1 `trans` co2) --> (sym co2) `trans (sym co2)
   = mkTransCoercion (mkSymCoercion co2) (mkSymCoercion co1)
   | Just (co, ty) <- splitInstCoercion_maybe co
+     -- 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
@@ -182,7 +208,6 @@ mkSymCoercion (TyVarTy tv)
   | isCoVar tv = mkCoercion symCoercionTyCon [TyVarTy tv]
   | otherwise  = TyVarTy tv
 mkSymCoercion co = mkCoercion symCoercionTyCon [co] 
-                   -- this should not happen but does
 
 -- Smart constructors for left and right
 mkLeftCoercion co 
@@ -252,13 +277,21 @@ 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
+-- bottom, which is the 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
+-- 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
 mkNewTypeCoercion :: Name -> TyCon -> [TyVar] -> Type -> TyCon
 mkNewTypeCoercion name tycon tvs rhs_ty 
   = ASSERT (length tvs == tyConArity tycon)
@@ -286,7 +319,7 @@ mkKindingFun f args =
 
 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 = 
@@ -299,7 +332,9 @@ symCoercionTyCon =
 transCoercionTyCon = 
   mkCoercionTyCon transCoercionTyConName 2 (mkKindingFun composeCoercionKindsOf)
   where
-    composeCoercionKindsOf (co1:co2:rest) = (a1, r2, rest)
+    composeCoercionKindsOf (co1:co2:rest) = 
+        WARN( not (r1 `coreEqType` a2), text "Strange! Type mismatch in trans coercion, probably a bug")
+        (a1, r2, rest)
       where
         (a1, r1) = coercionKind co1
         (a2, r2) = coercionKind co2 
@@ -361,7 +396,7 @@ unsafeCoercionTyConName = mkCoConName FSLIT("CoUnsafe") unsafeCoercionTyConKey u
 
 -- 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 
@@ -376,6 +411,5 @@ splitNewTypeRepCo_maybe (TyConApp tc 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
 \end{code}