X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypes%2FCoercion.lhs;h=05f1601431b92bc4cd94ec71659d1188e1800250;hb=19b44dcc5e5b9f92735fa99aa45dfaa94777177c;hp=98b5a0721b59ae03c0c8af44ad4a228fd9a2de17;hpb=701797c3f724090508e06ded276723edfa431ab4;p=ghc-hetmet.git

diff --git a/compiler/types/Coercion.lhs b/compiler/types/Coercion.lhs
index 98b5a07..05f1601 100644
--- a/compiler/types/Coercion.lhs
+++ b/compiler/types/Coercion.lhs
@@ -12,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}
+{-# 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/Commentary/CodingStyle#Warnings
+-- for details
+
 module Coercion (
         Coercion,
  
@@ -22,12 +29,14 @@ module Coercion (
 	isEqPred, mkEqPred, getEqPredTys, isEqPredTy,  
 
 	-- Coercion transformations
+	mkCoercion,
         mkSymCoercion, mkTransCoercion,
-        mkLeftCoercion, mkRightCoercion, mkInstCoercion, mkAppCoercion,
+        mkLeftCoercion, mkRightCoercion, mkRightCoercions,
+	mkInstCoercion, mkAppCoercion,
         mkForAllCoercion, mkFunCoercion, mkInstsCoercion, mkUnsafeCoercion,
         mkNewTypeCoercion, mkFamInstCoercion, mkAppsCoercion,
 
-        splitNewTypeRepCo_maybe, decomposeCo,
+        splitNewTypeRepCo_maybe, instNewTyCon_maybe, decomposeCo,
 
         unsafeCoercionTyCon, symCoercionTyCon,
         transCoercionTyCon, leftCoercionTyCon, 
@@ -39,8 +48,8 @@ module Coercion (
 	mkSymCoI, mkTransCoI, 
 	mkTyConAppCoI, mkAppTyCoI, mkFunTyCoI,
 	mkNoteTyCoI, mkForAllTyCoI,
-	fromCoI,
-	mkClassPPredCoI, mkIParamPredCoI, mkEqPredCoI,
+	fromCoI, fromACo,
+	mkClassPPredCoI, mkIParamPredCoI, mkEqPredCoI
 
        ) where 
 
@@ -60,6 +69,9 @@ import BasicTypes
 import Outputable
 
 
+type Coercion     = Type
+type CoercionKind = Kind	-- A CoercionKind is always of form (ty1 :=: ty2)
+
 ------------------------------
 decomposeCo :: Arity -> Coercion -> [Coercion]
 -- (decomposeCo 3 c) = [right (left (left c)), right (left c), right c]
@@ -102,9 +114,6 @@ splitCoercionKind_maybe co | Just co' <- kindView co = splitCoercionKind_maybe c
 splitCoercionKind_maybe (PredTy (EqPred ty1 ty2)) = Just (ty1, ty2)
 splitCoercionKind_maybe other = Nothing
 
-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)
@@ -227,6 +236,17 @@ mkRightCoercion  co
   | Just (co1, co2) <- splitAppCoercion_maybe co = co2
   | otherwise = mkCoercion rightCoercionTyCon [co]
 
+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]
@@ -351,7 +371,10 @@ transCoercionTyCon =
   where
     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"
+              $$
+              ppr r1 <+> text "=/=" <+> ppr a2)
         (a1, r2)
       where
         (a1, r1) = coercionKind co1
@@ -381,6 +404,9 @@ splitCoercionKindOf co
   , Just (ty_fun1, ty_arg1) <- splitAppTy_maybe ty1
   , Just (ty_fun2, ty_arg2) <- splitAppTy_maybe ty2
   = ((ty_fun1, ty_fun2),(ty_arg1, ty_arg2))
+splitCoercionKindOf co 
+  = pprPanic "Coercion.splitCoercionKindOf" 
+             (ppr co $$ ppr (coercionKindPredTy co))
 
 instCoercionTyCon 
   =  mkCoercionTyCon instCoercionTyConName 2 instCoercionKind
@@ -413,24 +439,37 @@ 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
+--    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)
-  | isClosedNewTyCon 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_maybe 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}
 
 
@@ -438,18 +477,26 @@ splitNewTypeRepCo_maybe other = Nothing
 -- 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
+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] 
@@ -462,18 +509,9 @@ 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)
+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
@@ -493,31 +531,25 @@ mkForAllTyCoI :: TyVar -> CoercionI -> CoercionI
 mkForAllTyCoI _ IdCo = IdCo
 mkForAllTyCoI tv (ACo co) = ACo $ ForAllTy tv co
 
-fromCoI IdCo ty     = ty
-fromCoI (ACo co) ty = co
+fromACo :: CoercionI -> Coercion
+fromACo (ACo co) = 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)
+-- 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}