+%
+% (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.
mkSymCoercion, mkTransCoercion,
mkLeftCoercion, mkRightCoercion, mkInstCoercion, mkAppCoercion,
mkForAllCoercion, mkFunCoercion, mkInstsCoercion, mkUnsafeCoercion,
- mkNewTypeCoercion, mkDataInstCoercion, mkAppsCoercion,
+ mkNewTypeCoercion, mkFamInstCoercion, mkAppsCoercion,
splitNewTypeRepCo_maybe, decomposeCo,
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,
+ mkClassPPredCoI, mkIParamPredCoI, mkEqPredCoI,
+
) 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,
- tyVarsOfType, mkTyVarTys
- )
-import TyCon ( TyCon, tyConArity, mkCoercionTyCon, isClosedNewTyCon,
- newTyConRhs, newTyConCo_maybe,
- isCoercionTyCon, isCoercionTyCon_maybe )
-import Var ( Var, TyVar, isTyVar, tyVarKind )
-import VarSet ( elemVarSet )
-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
-
------------------------------
decomposeCo :: Arity -> Coercion -> [Coercion]
-- (decomposeCo 3 c) = [right (left (left c)), right (left c), right c]
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 (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 (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)
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
- -- 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)
+ -- Note reversal of arguments!
= mkTransCoercion (mkSymCoercion co2) (mkSymCoercion co1)
- | Just (co, ty) <- splitInstCoercion_maybe co
+
+ | tc `hasKey` instCoercionTyConKey
-- 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]
- | 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'
- | otherwise = mkCoercion leftCoercionTyCon [co]
+ | otherwise = mkCoercion leftCoercionTyCon [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]
+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
-- 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 co_con_arity (mkKindingFun rule)
+mkNewTypeCoercion name tycon tvs rhs_ty
+ = mkCoercionTyCon name co_con_arity rule
where
- rule args = (TyConApp tycon tys, substTyWith tvs_eta tys rhs_eta, rest)
- where
- tys = take co_con_arity args
- rest = drop co_con_arity args
-
- -- if the rhs_ty is a type application and it has a tail equal to a tail
- -- of the tvs, then we eta-contract the type of the coercion
- rhs_args = let (ty, ty_args) = splitAppTys rhs_ty in ty_args
+ co_con_arity = length tvs
- n_eta_tys = count_eta (reverse rhs_args) (reverse tvs)
+ rule args = ASSERT( co_con_arity == length args )
+ (TyConApp tycon args, substTyWith tvs args rhs_ty)
- count_eta ((TyVarTy tv):rest_ty) (tv':rest_tv)
- | tv == tv' && (not $ any (elemVarSet tv . tyVarsOfType) rest_ty)
- -- if the last types are the same, and not free anywhere else
- -- then eta contract
- = 1 + (count_eta rest_ty rest_tv)
- | otherwise -- don't
- = 0
- count_eta _ _ = 0
-
-
- eqVar (TyVarTy tv) tv' = tv == tv'
- eqVar _ _ = False
-
- co_con_arity = (tyConArity tycon) - n_eta_tys
-
- tvs_eta = (reverse (drop n_eta_tys (reverse tvs)))
-
- rhs_eta
- | (ty, ty_args) <- splitAppTys rhs_ty
- = mkAppTys ty (reverse (drop n_eta_tys (reverse ty_args)))
-
--- 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)
+-- 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.
--
-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 (mkKindingFun rule)
+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 tys $ -- with sigma = [tys/tvs],
+ rule args = (substTyWith tvs args $ -- with sigma = [tys/tvs],
TyConApp family instTys, -- sigma (F ts)
- TyConApp rep_tycon tys, -- :=: R tys
- rest) -- surplus arguments
- where
- tys = take coArity args
- rest = drop coArity args
+ TyConApp rep_tycon args) -- :=: R tys
--------------------------------------
-- Coercion Type Constructors...
-- 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
-- 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)
= ((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
co_con = maybe (pprPanic "splitNewTypeRepCo_maybe" (ppr tc)) id (newTyConCo_maybe tc)
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
+
+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 =
+ 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)
+
+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
+
+fromCoI IdCo ty = ty
+fromCoI (ACo co) ty = 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)
+
+mkIParamPredCoI :: (IPName Name) -> CoercionI -> CoercionI
+mkIParamPredCoI ipn IdCo = IdCo
+mkIParamPredCoI ipn (ACo co) = ACo $ PredTy $ IParam ipn co
+
+mkEqPredCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI
+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}
+
projects / ghc-hetmet.git / blobdiff