%
% (c) The University of Glasgow 2006
%
\begin{code}
module Coercion (
Coercion,
mkCoKind, mkReflCoKind, splitCoercionKind_maybe, splitCoercionKind,
coercionKind, coercionKinds, coercionKindPredTy, isIdentityCoercion,
isEqPred, mkEqPred, getEqPredTys, isEqPredTy,
mkCoercion,
mkSymCoercion, mkTransCoercion,
mkLeftCoercion, mkRightCoercion, mkRightCoercions,
mkInstCoercion, mkAppCoercion, mkTyConCoercion, mkFunCoercion,
mkForAllCoercion, mkInstsCoercion, mkUnsafeCoercion,
mkNewTypeCoercion, mkFamInstCoercion, mkAppsCoercion,
splitNewTypeRepCo_maybe, instNewTyCon_maybe, decomposeCo,
unsafeCoercionTyCon, symCoercionTyCon,
transCoercionTyCon, leftCoercionTyCon,
rightCoercionTyCon, instCoercionTyCon,
coreEqCoercion,
CoercionI(..),
isIdentityCoI,
mkSymCoI, mkTransCoI,
mkTyConAppCoI, mkAppTyCoI, mkFunTyCoI,
mkForAllTyCoI,
fromCoI, fromACo,
mkClassPPredCoI, mkIParamPredCoI, mkEqPredCoI
) where
#include "HsVersions.h"
import TypeRep
import Type
import TyCon
import Class
import Var
import Name
import PrelNames
import Util
import BasicTypes
import Outputable
import FastString
type Coercion = Type
type CoercionKind = Kind
decomposeCo :: Arity -> Coercion -> [Coercion]
decomposeCo n co
= go n co []
where
go 0 _ cos = cos
go n co cos = go (n1) (mkLeftCoercion co)
(mkRightCoercion co : cos)
isEqPredTy :: Type -> Bool
isEqPredTy (PredTy pred) = isEqPred pred
isEqPredTy _ = False
mkEqPred :: (Type, Type) -> PredType
mkEqPred (ty1, ty2) = EqPred ty1 ty2
getEqPredTys :: PredType -> (Type,Type)
getEqPredTys (EqPred ty1 ty2) = (ty1, ty2)
getEqPredTys other = pprPanic "getEqPredTys" (ppr other)
mkCoKind :: Type -> Type -> CoercionKind
mkCoKind ty1 ty2 = PredTy (EqPred ty1 ty2)
mkReflCoKind :: Type -> CoercionKind
mkReflCoKind ty = mkCoKind ty ty
splitCoercionKind :: CoercionKind -> (Type, Type)
splitCoercionKind co | Just co' <- kindView co = splitCoercionKind co'
splitCoercionKind (PredTy (EqPred ty1 ty2)) = (ty1, ty2)
splitCoercionKind_maybe :: Kind -> Maybe (Type, Type)
splitCoercionKind_maybe co | Just co' <- kindView co = splitCoercionKind_maybe co'
splitCoercionKind_maybe (PredTy (EqPred ty1 ty2)) = Just (ty1, ty2)
splitCoercionKind_maybe _ = Nothing
coercionKind :: Coercion -> (Type, Type)
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
(mkAppTy t1 s1, mkAppTy t2 s2)
coercionKind (TyConApp tc args)
| Just (ar, rule) <- isCoercionTyCon_maybe tc
= ASSERT( length args >= ar )
let (ty1,ty2) = rule (take ar 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)
coercionKind (FunTy ty1 ty2)
= let (t1, t2) = coercionKind ty1
(s1, s2) = coercionKind ty2 in
(mkFunTy t1 s1, mkFunTy t2 s2)
coercionKind (ForAllTy tv ty)
= let (ty1, ty2) = coercionKind ty in
(ForAllTy tv ty1, ForAllTy tv ty2)
coercionKind (PredTy (EqPred c1 c2))
= let k1 = coercionKindPredTy c1
k2 = coercionKindPredTy c2 in
(k1,k2)
coercionKind (PredTy (ClassP cl args))
= let (lArgs, rArgs) = coercionKinds args in
(PredTy (ClassP cl lArgs), PredTy (ClassP cl rArgs))
coercionKind (PredTy (IParam name ty))
= let (ty1, ty2) = coercionKind ty in
(PredTy (IParam name ty1), PredTy (IParam name ty2))
coercionKindPredTy :: Coercion -> CoercionKind
coercionKindPredTy c = let (t1, t2) = coercionKind c in mkCoKind t1 t2
coercionKinds :: [Coercion] -> ([Type], [Type])
coercionKinds tys = unzip $ map coercionKind tys
isIdentityCoercion :: Coercion -> Bool
isIdentityCoercion co
= case coercionKind co of
(t1,t2) -> t1 `coreEqType` t2
mkCoercion :: TyCon -> [Type] -> Coercion
mkCoercion coCon args = ASSERT( tyConArity coCon == length args )
TyConApp coCon args
mkAppCoercion :: Coercion -> Coercion -> Coercion
mkAppCoercion co1 co2 = mkAppTy co1 co2
mkAppsCoercion :: Coercion -> [Coercion] -> Coercion
mkAppsCoercion co1 tys = foldl mkAppTy co1 tys
mkTyConCoercion :: TyCon -> [Coercion] -> Coercion
mkTyConCoercion con cos = mkTyConApp con cos
mkFunCoercion :: Coercion -> Coercion -> Coercion
mkFunCoercion co1 co2 = mkFunTy co1 co2
mkForAllCoercion :: Var -> Coercion -> Coercion
mkForAllCoercion tv co = ASSERT ( isTyVar tv ) mkForAllTy tv co
mkSymCoercion :: Coercion -> Coercion
mkSymCoercion 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
| tc `hasKey` leftCoercionTyConKey = mkLeftCoercion (mkSymCoercion co)
| tc `hasKey` rightCoercionTyConKey = mkRightCoercion (mkSymCoercion co)
mkSymCoercion (TyConApp tc [co1,co2])
| tc `hasKey` transCoercionTyConKey
= mkTransCoercion (mkSymCoercion co2) (mkSymCoercion co1)
| tc `hasKey` instCoercionTyConKey
= mkInstCoercion (mkSymCoercion co1) co2
mkSymCoercion (TyConApp tc cos)
= mkCoercion symCoercionTyCon [TyConApp tc cos]
mkSymCoercion (TyVarTy tv)
| isCoVar tv = mkCoercion symCoercionTyCon [TyVarTy tv]
| otherwise = TyVarTy tv
mkTransCoercion :: Coercion -> Coercion -> Coercion
mkTransCoercion g1 g2
| (t1,_) <- coercionKind g1
, (_,t2) <- coercionKind g2
, t1 `coreEqType` t2
= t1
| otherwise
= mkCoercion transCoercionTyCon [g1, g2]
mkLeftCoercion :: Coercion -> Coercion
mkLeftCoercion co
| Just (co', _) <- splitAppCoercion_maybe co = co'
| otherwise = mkCoercion leftCoercionTyCon [co]
mkRightCoercion :: Coercion -> Coercion
mkRightCoercion co
| Just (_, co2) <- splitAppCoercion_maybe co = co2
| otherwise = mkCoercion rightCoercionTyCon [co]
mkRightCoercions :: Int -> Coercion -> [Coercion]
mkRightCoercions n co
= go n co []
where
go n co acc
| n > 0
= case splitAppCoercion_maybe co of
Just (co1,co2) -> go (n1) co1 (co2:acc)
Nothing -> go (n1) (mkCoercion leftCoercionTyCon [co]) (mkCoercion rightCoercionTyCon [co]:acc)
| otherwise
= acc
mkInstCoercion :: Coercion -> Type -> Coercion
mkInstCoercion co ty
| Just (tv,co') <- splitForAllTy_maybe co
= substTyWith [tv] [ty] co'
| otherwise
= mkCoercion instCoercionTyCon [co, ty]
mkInstsCoercion :: Coercion -> [Type] -> Coercion
mkInstsCoercion co tys = foldl mkInstCoercion co tys
splitAppCoercion_maybe :: Coercion -> Maybe (Coercion, Coercion)
splitAppCoercion_maybe co | Just co' <- coreView co = splitAppCoercion_maybe co'
splitAppCoercion_maybe (FunTy ty1 ty2) = Just (TyConApp funTyCon [ty1], ty2)
splitAppCoercion_maybe (AppTy ty1 ty2) = Just (ty1, ty2)
splitAppCoercion_maybe (TyConApp tc tys)
| not (isCoercionTyCon tc)
= case snocView tys of
Just (tys', ty') -> Just (TyConApp tc tys', ty')
Nothing -> Nothing
splitAppCoercion_maybe _ = Nothing
mkUnsafeCoercion :: Type -> Type -> Coercion
mkUnsafeCoercion ty1 ty2
= mkCoercion unsafeCoercionTyCon [ty1, ty2]
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)
mkFamInstCoercion :: Name
-> [TyVar]
-> TyCon
-> [Type]
-> TyCon
-> TyCon
mkFamInstCoercion name tvs family instTys rep_tycon
= mkCoercionTyCon name coArity rule
where
coArity = length tvs
rule args = (substTyWith tvs args $
TyConApp family instTys,
TyConApp rep_tycon args)
symCoercionTyCon, transCoercionTyCon, leftCoercionTyCon, rightCoercionTyCon, instCoercionTyCon, unsafeCoercionTyCon :: TyCon
symCoercionTyCon =
mkCoercionTyCon symCoercionTyConName 1 flipCoercionKindOf
where
flipCoercionKindOf (co:rest) = ASSERT( null rest ) (ty2, ty1)
where
(ty1, ty2) = coercionKind co
transCoercionTyCon =
mkCoercionTyCon transCoercionTyConName 2 composeCoercionKindsOf
where
composeCoercionKindsOf (co1:co2:rest)
= ASSERT( null rest )
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
(a2, r2) = coercionKind co2
leftCoercionTyCon =
mkCoercionTyCon leftCoercionTyConName 1 leftProjectCoercionKindOf
where
leftProjectCoercionKindOf (co:rest) = ASSERT( null rest ) (ty1, ty2)
where
(ty1,ty2) = fst (splitCoercionKindOf co)
rightCoercionTyCon =
mkCoercionTyCon rightCoercionTyConName 1 rightProjectCoercionKindOf
where
rightProjectCoercionKindOf (co:rest) = ASSERT( null rest ) (ty1, ty2)
where
(ty1,ty2) = snd (splitCoercionKindOf co)
splitCoercionKindOf :: Type -> ((Type,Type), (Type,Type))
splitCoercionKindOf co
| Just (ty1, ty2) <- splitCoercionKind_maybe (coercionKindPredTy 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
where
instantiateCo t s =
let Just (tv, ty) = splitForAllTy_maybe t in
substTyWith [tv] [s] ty
instCoercionKind (co1:ty:rest) = ASSERT( null rest )
(instantiateCo t1 ty, instantiateCo t2 ty)
where (t1, t2) = coercionKind co1
unsafeCoercionTyCon
= mkCoercionTyCon unsafeCoercionTyConName 2 unsafeCoercionKind
where
unsafeCoercionKind (ty1:ty2:rest) = ASSERT( null rest ) (ty1,ty2)
mkCoConName :: FastString -> Unique -> TyCon -> Name
mkCoConName occ key coCon = mkWiredInName gHC_PRIM (mkTcOccFS occ)
key (ATyCon coCon) BuiltInSyntax
transCoercionTyConName, symCoercionTyConName, leftCoercionTyConName, rightCoercionTyConName, instCoercionTyConName, unsafeCoercionTyConName :: Name
transCoercionTyConName = mkCoConName (fsLit "trans") transCoercionTyConKey transCoercionTyCon
symCoercionTyConName = mkCoConName (fsLit "sym") symCoercionTyConKey symCoercionTyCon
leftCoercionTyConName = mkCoConName (fsLit "left") leftCoercionTyConKey leftCoercionTyCon
rightCoercionTyConName = mkCoConName (fsLit "right") rightCoercionTyConKey rightCoercionTyCon
instCoercionTyConName = mkCoConName (fsLit "inst") instCoercionTyConKey instCoercionTyCon
unsafeCoercionTyConName = mkCoConName (fsLit "CoUnsafe") unsafeCoercionTyConKey unsafeCoercionTyCon
instNewTyCon_maybe :: TyCon -> [Type] -> Maybe (Type, CoercionI)
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
splitNewTypeRepCo_maybe :: Type -> Maybe (Type, Coercion)
splitNewTypeRepCo_maybe ty
| Just ty' <- coreView ty = splitNewTypeRepCo_maybe ty'
splitNewTypeRepCo_maybe (TyConApp tc tys)
| Just (ty', coi) <- instNewTyCon_maybe tc tys
= case coi of
ACo co -> Just (ty', co)
IdCo -> panic "splitNewTypeRepCo_maybe"
splitNewTypeRepCo_maybe _
= Nothing
coreEqCoercion :: Coercion -> Coercion -> Bool
coreEqCoercion = coreEqType
\end{code}
\begin{code}
data CoercionI = IdCo | ACo Coercion
instance Outputable CoercionI where
ppr IdCo = ptext (sLit "IdCo")
ppr (ACo co) = ppr co
isIdentityCoI :: CoercionI -> Bool
isIdentityCoI IdCo = True
isIdentityCoI _ = False
allIdCoIs :: [CoercionI] -> Bool
allIdCoIs = all isIdentityCoI
zipCoArgs :: [CoercionI] -> [Type] -> [Coercion]
zipCoArgs cois tys = zipWith fromCoI cois tys
fromCoI :: CoercionI -> Type -> Type
fromCoI IdCo ty = ty
fromCoI (ACo co) _ = co
mkSymCoI :: CoercionI -> CoercionI
mkSymCoI IdCo = IdCo
mkSymCoI (ACo co) = ACo $ mkCoercion symCoercionTyCon [co]
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
| allIdCoIs cois = IdCo
| otherwise = ACo (TyConApp tyCon (zipCoArgs cois tys))
mkAppTyCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI
mkAppTyCoI _ IdCo _ IdCo = IdCo
mkAppTyCoI ty1 coi1 ty2 coi2 =
ACo $ AppTy (fromCoI coi1 ty1) (fromCoI coi2 ty2)
mkFunTyCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI
mkFunTyCoI _ IdCo _ IdCo = IdCo
mkFunTyCoI ty1 coi1 ty2 coi2 =
ACo $ FunTy (fromCoI coi1 ty1) (fromCoI coi2 ty2)
mkForAllTyCoI :: TyVar -> CoercionI -> CoercionI
mkForAllTyCoI _ IdCo = IdCo
mkForAllTyCoI tv (ACo co) = ACo $ ForAllTy tv co
fromACo :: CoercionI -> Coercion
fromACo (ACo co) = co
mkClassPPredCoI :: Class -> [Type] -> [CoercionI] -> CoercionI
mkClassPPredCoI cls tys cois
| allIdCoIs cois = IdCo
| otherwise = ACo $ PredTy $ ClassP cls (zipCoArgs cois tys)
mkIParamPredCoI :: (IPName Name) -> CoercionI -> CoercionI
mkIParamPredCoI _ 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 _ (ACo co1) ty2 coi2 = ACo $ PredTy $ EqPred co1 (fromCoI coi2 ty2)
\end{code}