%
% (c) The University of Glasgow 2006
%
\begin{code}
module Coercion (
Coercion, Kind,
typeKind,
kindFunResult, kindAppResult, synTyConResKind,
splitKindFunTys, splitKindFunTysN, splitKindFunTy_maybe,
isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind,
isUbxTupleKind, isArgTypeKind, isKind, isTySuperKind,
isCoSuperKind, isSuperKind, isCoercionKind,
mkArrowKind, mkArrowKinds,
isSubArgTypeKind, isSubOpenTypeKind, isSubKind, defaultKind, eqKind,
isSubKindCon,
mkCoKind, mkCoPredTy, coVarKind, coVarKind_maybe,
coercionKind, coercionKinds, isIdentityCoercion,
isEqPred, mkEqPred, getEqPredTys, isEqPredTy,
mkCoercion,
mkSymCoercion, mkTransCoercion,
mkLeftCoercion, mkRightCoercion,
mkInstCoercion, mkAppCoercion, mkTyConCoercion, mkFunCoercion,
mkForAllCoercion, mkInstsCoercion, mkUnsafeCoercion,
mkNewTypeCoercion, mkFamInstCoercion, mkAppsCoercion,
mkCsel1Coercion, mkCsel2Coercion, mkCselRCoercion,
mkClassPPredCo, mkIParamPredCo, mkEqPredCo,
mkCoVarCoercion, mkCoPredCo,
unsafeCoercionTyCon, symCoercionTyCon,
transCoercionTyCon, leftCoercionTyCon,
rightCoercionTyCon, instCoercionTyCon,
csel1CoercionTyCon, csel2CoercionTyCon, cselRCoercionTyCon,
decompLR_maybe, decompCsel_maybe, decompInst_maybe,
splitCoPredTy_maybe,
splitNewTypeRepCo_maybe, instNewTyCon_maybe, decomposeCo,
coreEqCoercion, coreEqCoercion2,
CoercionI(..),
isIdentityCoI,
mkSymCoI, mkTransCoI,
mkTyConAppCoI, mkAppTyCoI, mkFunTyCoI,
mkForAllTyCoI,
fromCoI,
mkClassPPredCoI, mkIParamPredCoI, mkEqPredCoI, mkCoPredCoI
) where
#include "HsVersions.h"
import TypeRep
import Type
import TyCon
import Class
import Var
import VarEnv
import VarSet
import Name
import PrelNames
import Util
import BasicTypes
import Outputable
import FastString
\end{code}
%************************************************************************
%* *
Functions over Kinds
%* *
%************************************************************************
\begin{code}
kindFunResult :: Kind -> Kind
kindFunResult k = funResultTy k
kindAppResult :: Kind -> [arg] -> Kind
kindAppResult k [] = k
kindAppResult k (_:as) = kindAppResult (kindFunResult k) as
splitKindFunTys :: Kind -> ([Kind],Kind)
splitKindFunTys k = splitFunTys k
splitKindFunTy_maybe :: Kind -> Maybe (Kind,Kind)
splitKindFunTy_maybe = splitFunTy_maybe
splitKindFunTysN :: Int -> Kind -> ([Kind],Kind)
splitKindFunTysN k = splitFunTysN k
synTyConResKind :: TyCon -> Kind
synTyConResKind tycon = kindAppResult (tyConKind tycon) (tyConTyVars tycon)
isUbxTupleKind, isOpenTypeKind, isArgTypeKind, isUnliftedTypeKind :: Kind -> Bool
isOpenTypeKindCon, isUbxTupleKindCon, isArgTypeKindCon,
isUnliftedTypeKindCon, isSubArgTypeKindCon :: TyCon -> Bool
isOpenTypeKindCon tc = tyConUnique tc == openTypeKindTyConKey
isOpenTypeKind (TyConApp tc _) = isOpenTypeKindCon tc
isOpenTypeKind _ = False
isUbxTupleKindCon tc = tyConUnique tc == ubxTupleKindTyConKey
isUbxTupleKind (TyConApp tc _) = isUbxTupleKindCon tc
isUbxTupleKind _ = False
isArgTypeKindCon tc = tyConUnique tc == argTypeKindTyConKey
isArgTypeKind (TyConApp tc _) = isArgTypeKindCon tc
isArgTypeKind _ = False
isUnliftedTypeKindCon tc = tyConUnique tc == unliftedTypeKindTyConKey
isUnliftedTypeKind (TyConApp tc _) = isUnliftedTypeKindCon tc
isUnliftedTypeKind _ = False
isSubOpenTypeKind :: Kind -> Bool
isSubOpenTypeKind (FunTy k1 k2) = ASSERT2 ( isKind k1, text "isSubOpenTypeKind" <+> ppr k1 <+> text "::" <+> ppr (typeKind k1) )
ASSERT2 ( isKind k2, text "isSubOpenTypeKind" <+> ppr k2 <+> text "::" <+> ppr (typeKind k2) )
False
isSubOpenTypeKind (TyConApp kc []) = ASSERT( isKind (TyConApp kc []) ) True
isSubOpenTypeKind other = ASSERT( isKind other ) False
isSubArgTypeKindCon kc
| isUnliftedTypeKindCon kc = True
| isLiftedTypeKindCon kc = True
| isArgTypeKindCon kc = True
| otherwise = False
isSubArgTypeKind :: Kind -> Bool
isSubArgTypeKind (TyConApp kc []) = isSubArgTypeKindCon kc
isSubArgTypeKind _ = False
isSuperKind :: Type -> Bool
isSuperKind (TyConApp (skc) []) = isSuperKindTyCon skc
isSuperKind _ = False
isKind :: Kind -> Bool
isKind k = isSuperKind (typeKind k)
isSubKind :: Kind -> Kind -> Bool
isSubKind (TyConApp kc1 []) (TyConApp kc2 []) = kc1 `isSubKindCon` kc2
isSubKind (FunTy a1 r1) (FunTy a2 r2) = (a2 `isSubKind` a1) && (r1 `isSubKind` r2)
isSubKind (PredTy (EqPred ty1 ty2)) (PredTy (EqPred ty1' ty2'))
= ty1 `tcEqType` ty1' && ty2 `tcEqType` ty2'
isSubKind _ _ = False
eqKind :: Kind -> Kind -> Bool
eqKind = tcEqType
isSubKindCon :: TyCon -> TyCon -> Bool
isSubKindCon kc1 kc2
| isLiftedTypeKindCon kc1 && isLiftedTypeKindCon kc2 = True
| isUnliftedTypeKindCon kc1 && isUnliftedTypeKindCon kc2 = True
| isUbxTupleKindCon kc1 && isUbxTupleKindCon kc2 = True
| isOpenTypeKindCon kc2 = True
| isArgTypeKindCon kc2 && isSubArgTypeKindCon kc1 = True
| otherwise = False
defaultKind :: Kind -> Kind
defaultKind k
| isSubOpenTypeKind k = liftedTypeKind
| isSubArgTypeKind k = liftedTypeKind
| otherwise = k
\end{code}
%************************************************************************
%* *
Coercions
%* *
%************************************************************************
\begin{code}
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)
coVarKind :: CoVar -> (Type,Type)
coVarKind cv = case coVarKind_maybe cv of
Just ts -> ts
Nothing -> pprPanic "coVarKind" (ppr cv $$ ppr (tyVarKind cv))
coVarKind_maybe :: CoVar -> Maybe (Type,Type)
coVarKind_maybe cv = splitCoKind_maybe (tyVarKind cv)
splitCoKind_maybe :: Kind -> Maybe (Type, Type)
splitCoKind_maybe co | Just co' <- kindView co = splitCoKind_maybe co'
splitCoKind_maybe (PredTy (EqPred ty1 ty2)) = Just (ty1, ty2)
splitCoKind_maybe _ = Nothing
mkCoKind :: Type -> Type -> CoercionKind
mkCoKind ty1 ty2 = PredTy (EqPred ty1 ty2)
mkCoPredTy :: Type -> Type -> Type -> Type
mkCoPredTy s t r = ASSERT( not (co_var `elemVarSet` tyVarsOfType r) )
ForAllTy co_var r
where
co_var = mkWildCoVar (mkCoKind s t)
mkCoPredCo :: Coercion -> Coercion -> Coercion -> Coercion
mkCoPredCo = mkCoPredTy
splitCoPredTy_maybe :: Type -> Maybe (Type, Type, Type)
splitCoPredTy_maybe ty
| Just (cv,r) <- splitForAllTy_maybe ty
, isCoVar cv
, Just (s,t) <- coVarKind_maybe cv
= Just (s,t,r)
| otherwise
= Nothing
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)
isIdentityCoercion :: Coercion -> Bool
isIdentityCoercion co
= case coercionKind co of
(t1,t2) -> t1 `coreEqType` t2
\end{code}
%************************************************************************
%* *
Building coercions
%* *
%************************************************************************
Coercion kind and type mk's (make saturated TyConApp CoercionTyCon{...} args)
\begin{code}
mkCoercion :: TyCon -> [Type] -> Coercion
mkCoercion coCon args = ASSERT( tyConArity coCon == length args )
TyConApp coCon args
mkCoVarCoercion :: CoVar -> Coercion
mkCoVarCoercion cv = mkTyVarTy cv
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 ( isTyCoVar tv ) mkForAllTy tv co
mkSymCoercion :: Coercion -> Coercion
mkSymCoercion g = mkCoercion symCoercionTyCon [g]
mkTransCoercion :: Coercion -> Coercion -> Coercion
mkTransCoercion g1 g2 = mkCoercion transCoercionTyCon [g1, g2]
mkLeftCoercion :: Coercion -> Coercion
mkLeftCoercion co = mkCoercion leftCoercionTyCon [co]
mkRightCoercion :: Coercion -> Coercion
mkRightCoercion co = mkCoercion rightCoercionTyCon [co]
mkCsel1Coercion, mkCsel2Coercion, mkCselRCoercion :: Coercion -> Coercion
mkCsel1Coercion co = mkCoercion csel1CoercionTyCon [co]
mkCsel2Coercion co = mkCoercion csel2CoercionTyCon [co]
mkCselRCoercion co = mkCoercion cselRCoercionTyCon [co]
mkInstCoercion :: Coercion -> Type -> Coercion
mkInstCoercion co ty = mkCoercion instCoercionTyCon [co, ty]
mkInstsCoercion :: Coercion -> [Type] -> Coercion
mkInstsCoercion co tys = foldl mkInstCoercion co tys
mkUnsafeCoercion :: Type -> Type -> Coercion
mkUnsafeCoercion (TyConApp tc1 tys1) (TyConApp tc2 tys2)
| tc1 == tc2
= TyConApp tc1 (zipWith mkUnsafeCoercion tys1 tys2)
mkUnsafeCoercion (FunTy a1 r1) (FunTy a2 r2)
= FunTy (mkUnsafeCoercion a1 a2) (mkUnsafeCoercion r1 r2)
mkUnsafeCoercion ty1 ty2
| ty1 `coreEqType` ty2 = ty1
| otherwise = mkCoercion unsafeCoercionTyCon [ty1, ty2]
mkNewTypeCoercion :: Name -> TyCon -> [TyVar] -> Type -> TyCon
mkNewTypeCoercion name tycon tvs rhs_ty
= mkCoercionTyCon name arity desc
where
arity = length tvs
desc = CoAxiom { co_ax_tvs = tvs
, co_ax_lhs = mkTyConApp tycon (mkTyVarTys tvs)
, co_ax_rhs = rhs_ty }
mkFamInstCoercion :: Name
-> [TyVar]
-> TyCon
-> [Type]
-> TyCon
-> TyCon
mkFamInstCoercion name tvs family inst_tys rep_tycon
= mkCoercionTyCon name arity desc
where
arity = length tvs
desc = CoAxiom { co_ax_tvs = tvs
, co_ax_lhs = mkTyConApp family inst_tys
, co_ax_rhs = mkTyConApp rep_tycon (mkTyVarTys tvs) }
mkClassPPredCo :: Class -> [Coercion] -> Coercion
mkClassPPredCo cls = (PredTy . ClassP cls)
mkIParamPredCo :: (IPName Name) -> Coercion -> Coercion
mkIParamPredCo ipn = (PredTy . IParam ipn)
mkEqPredCo :: Coercion -> Coercion -> Coercion
mkEqPredCo co1 co2 = PredTy (EqPred co1 co2)
\end{code}
%************************************************************************
%* *
Coercion Type Constructors
%* *
%************************************************************************
Example. The coercion ((sym c) (sym d) (sym e))
will be represented by (TyConApp sym [c, sym d, sym e])
If sym c :: p1=q1
sym d :: p2=q2
sym e :: p3=q3
then ((sym c) (sym d) (sym e)) :: (p1 p2 p3)=(q1 q2 q3)
\begin{code}
symCoercionTyCon, transCoercionTyCon, leftCoercionTyCon,
rightCoercionTyCon, instCoercionTyCon, unsafeCoercionTyCon,
csel1CoercionTyCon, csel2CoercionTyCon, cselRCoercionTyCon :: TyCon
symCoercionTyCon = mkCoercionTyCon symCoercionTyConName 1 CoSym
transCoercionTyCon = mkCoercionTyCon transCoercionTyConName 2 CoTrans
leftCoercionTyCon = mkCoercionTyCon leftCoercionTyConName 1 CoLeft
rightCoercionTyCon = mkCoercionTyCon rightCoercionTyConName 1 CoRight
instCoercionTyCon = mkCoercionTyCon instCoercionTyConName 2 CoInst
csel1CoercionTyCon = mkCoercionTyCon csel1CoercionTyConName 1 CoCsel1
csel2CoercionTyCon = mkCoercionTyCon csel2CoercionTyConName 1 CoCsel2
cselRCoercionTyCon = mkCoercionTyCon cselRCoercionTyConName 1 CoCselR
unsafeCoercionTyCon = mkCoercionTyCon unsafeCoercionTyConName 2 CoUnsafe
transCoercionTyConName, symCoercionTyConName, leftCoercionTyConName,
rightCoercionTyConName, instCoercionTyConName, unsafeCoercionTyConName,
csel1CoercionTyConName, csel2CoercionTyConName, cselRCoercionTyConName :: 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
csel1CoercionTyConName = mkCoConName (fsLit "csel1") csel1CoercionTyConKey csel1CoercionTyCon
csel2CoercionTyConName = mkCoConName (fsLit "csel2") csel2CoercionTyConKey csel2CoercionTyCon
cselRCoercionTyConName = mkCoConName (fsLit "cselR") cselRCoercionTyConKey cselRCoercionTyCon
unsafeCoercionTyConName = mkCoConName (fsLit "CoUnsafe") unsafeCoercionTyConKey unsafeCoercionTyCon
mkCoConName :: FastString -> Unique -> TyCon -> Name
mkCoConName occ key coCon = mkWiredInName gHC_PRIM (mkTcOccFS occ)
key (ATyCon coCon) BuiltInSyntax
\end{code}
\begin{code}
decompLR_maybe :: (Type,Type) -> Maybe ((Type,Type), (Type,Type))
decompLR_maybe (ty1,ty2)
| Just (ty_fun1, ty_arg1) <- splitAppTy_maybe ty1
, Just (ty_fun2, ty_arg2) <- splitAppTy_maybe ty2
= Just ((ty_fun1, ty_fun2),(ty_arg1, ty_arg2))
decompLR_maybe _ = Nothing
decompInst_maybe :: (Type, Type) -> Maybe ((TyVar,TyVar), (Type,Type))
decompInst_maybe (ty1, ty2)
| Just (tv1,r1) <- splitForAllTy_maybe ty1
, Just (tv2,r2) <- splitForAllTy_maybe ty2
= Just ((tv1,tv2), (r1,r2))
decompInst_maybe _ = Nothing
decompCsel_maybe :: (Type, Type) -> Maybe ((Type,Type), (Type,Type), (Type,Type))
decompCsel_maybe (ty1, ty2)
| Just (s1, t1, r1) <- splitCoPredTy_maybe ty1
, Just (s2, t2, r2) <- splitCoPredTy_maybe ty2
= Just ((s1,s2), (t1,t2), (r1,r2))
decompCsel_maybe _ = Nothing
\end{code}
%************************************************************************
%* *
Newtypes
%* *
%************************************************************************
\begin{code}
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 (mkTyConApp tc tys)
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
coreEqCoercion2 :: RnEnv2 -> Coercion -> Coercion -> Bool
coreEqCoercion2 = coreEqType2
\end{code}
%************************************************************************
%* *
CoercionI and its constructors
%* *
%************************************************************************
--------------------------------------
-- CoercionI smart constructors
-- lifted smart constructors of ordinary coercions
\begin{code}
data CoercionI = IdCo Type | ACo Coercion
liftCoI :: (Type -> Type) -> CoercionI -> CoercionI
liftCoI f (IdCo ty) = IdCo (f ty)
liftCoI f (ACo ty) = ACo (f ty)
liftCoI2 :: (Type -> Type -> Type) -> CoercionI -> CoercionI -> CoercionI
liftCoI2 f (IdCo ty1) (IdCo ty2) = IdCo (f ty1 ty2)
liftCoI2 f coi1 coi2 = ACo (f (fromCoI coi1) (fromCoI coi2))
liftCoIs :: ([Type] -> Type) -> [CoercionI] -> CoercionI
liftCoIs f cois = go_id [] cois
where
go_id rev_tys [] = IdCo (f (reverse rev_tys))
go_id rev_tys (IdCo ty : cois) = go_id (ty:rev_tys) cois
go_id rev_tys (ACo co : cois) = go_aco (co:rev_tys) cois
go_aco rev_tys [] = ACo (f (reverse rev_tys))
go_aco rev_tys (IdCo ty : cois) = go_aco (ty:rev_tys) cois
go_aco rev_tys (ACo co : cois) = go_aco (co:rev_tys) cois
instance Outputable CoercionI where
ppr (IdCo _) = ptext (sLit "IdCo")
ppr (ACo co) = ppr co
isIdentityCoI :: CoercionI -> Bool
isIdentityCoI (IdCo _) = True
isIdentityCoI (ACo _) = False
fromCoI :: CoercionI -> Type
fromCoI (IdCo ty) = ty
fromCoI (ACo co) = co
mkSymCoI :: CoercionI -> CoercionI
mkSymCoI (IdCo ty) = IdCo ty
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 -> [CoercionI] -> CoercionI
mkTyConAppCoI tyCon cois = liftCoIs (mkTyConApp tyCon) cois
mkAppTyCoI :: CoercionI -> CoercionI -> CoercionI
mkAppTyCoI = liftCoI2 mkAppTy
mkFunTyCoI :: CoercionI -> CoercionI -> CoercionI
mkFunTyCoI = liftCoI2 mkFunTy
mkForAllTyCoI :: TyVar -> CoercionI -> CoercionI
mkForAllTyCoI tv = liftCoI (ForAllTy tv)
mkClassPPredCoI :: Class -> [CoercionI] -> CoercionI
mkClassPPredCoI cls = liftCoIs (PredTy . ClassP cls)
mkIParamPredCoI :: (IPName Name) -> CoercionI -> CoercionI
mkIParamPredCoI ipn = liftCoI (PredTy . IParam ipn)
mkEqPredCoI :: CoercionI -> CoercionI -> CoercionI
mkEqPredCoI = liftCoI2 (\t1 t2 -> PredTy (EqPred t1 t2))
mkCoPredCoI :: CoercionI -> CoercionI -> CoercionI -> CoercionI
mkCoPredCoI coi1 coi2 coi3 = mkFunTyCoI (mkEqPredCoI coi1 coi2) coi3
\end{code}
%************************************************************************
%* *
The kind of a type, and of a coercion
%* *
%************************************************************************
\begin{code}
typeKind :: Type -> Kind
typeKind ty@(TyConApp tc tys)
| isCoercionTyCon tc = typeKind (fst (coercionKind ty))
| otherwise = kindAppResult (tyConKind tc) tys
typeKind (PredTy pred) = predKind pred
typeKind (AppTy fun _) = kindFunResult (typeKind fun)
typeKind (ForAllTy _ ty) = typeKind ty
typeKind (TyVarTy tyvar) = tyVarKind tyvar
typeKind (FunTy _arg res)
| isTySuperKind k = k
| otherwise = ASSERT( isSubOpenTypeKind k) liftedTypeKind
where
k = typeKind res
predKind :: PredType -> Kind
predKind (EqPred {}) = coSuperKind
predKind (ClassP {}) = liftedTypeKind
predKind (IParam {}) = liftedTypeKind
coercionKind :: Coercion -> (Type, Type)
coercionKind ty@(TyVarTy a) | isCoVar a = coVarKind a
| otherwise = (ty, ty)
coercionKind (AppTy ty1 ty2)
= let (s1, t1) = coercionKind ty1
(s2, t2) = coercionKind ty2 in
(mkAppTy s1 s2, mkAppTy t1 t2)
coercionKind co@(TyConApp tc args)
| Just (ar, desc) <- isCoercionTyCon_maybe tc
= WARN( not (length args >= ar), ppr co )
(let (ty1, ty2) = coTyConAppKind desc (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)
| isCoVar tv
= let (c1,c2) = coVarKind tv
(s1,s2) = coercionKind c1
(t1,t2) = coercionKind c2
(r1,r2) = coercionKind ty
in
(mkCoPredTy s1 t1 r1, mkCoPredTy s2 t2 r2)
| otherwise
= let (ty1, ty2) = coercionKind ty in
(ForAllTy tv ty1, ForAllTy tv ty2)
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))
coercionKind (PredTy (EqPred c1 c2))
= pprTrace "coercionKind" (pprEqPred (c1,c2)) $
let k1 = coercionKindPredTy c1
k2 = coercionKindPredTy c2 in
(k1,k2)
where
coercionKindPredTy c = let (t1, t2) = coercionKind c in mkCoKind t1 t2
coercionKinds :: [Coercion] -> ([Type], [Type])
coercionKinds tys = unzip $ map coercionKind tys
coTyConAppKind
:: CoTyConDesc
-> [Type]
-> (Type, Type)
coTyConAppKind CoUnsafe (ty1:ty2:_)
= (ty1,ty2)
coTyConAppKind CoSym (co:_)
| (ty1,ty2) <- coercionKind co = (ty2,ty1)
coTyConAppKind CoTrans (co1:co2:_)
= (fst (coercionKind co1), snd (coercionKind co2))
coTyConAppKind CoLeft (co:_)
| Just (res,_) <- decompLR_maybe (coercionKind co) = res
coTyConAppKind CoRight (co:_)
| Just (_,res) <- decompLR_maybe (coercionKind co) = res
coTyConAppKind CoCsel1 (co:_)
| Just (res,_,_) <- decompCsel_maybe (coercionKind co) = res
coTyConAppKind CoCsel2 (co:_)
| Just (_,res,_) <- decompCsel_maybe (coercionKind co) = res
coTyConAppKind CoCselR (co:_)
| Just (_,_,res) <- decompCsel_maybe (coercionKind co) = res
coTyConAppKind CoInst (co:ty:_)
| Just ((tv1,tv2), (ty1,ty2)) <- decompInst_maybe (coercionKind co)
= (substTyWith [tv1] [ty] ty1, substTyWith [tv2] [ty] ty2)
coTyConAppKind (CoAxiom { co_ax_tvs = tvs
, co_ax_lhs = lhs_ty, co_ax_rhs = rhs_ty }) cos
= (substTyWith tvs tys1 lhs_ty, substTyWith tvs tys2 rhs_ty)
where
(tys1, tys2) = coercionKinds cos
coTyConAppKind desc cos = pprTrace "coTyConAppKind" (ppr desc $$ braces (vcat
[ ppr co <+> dcolon <+> pprEqPred (coercionKind co)
| co <- cos ])) $
coercionKind (head cos)
\end{code}