module Coercion (
Coercion(..), Var, CoVar,
LeftOrRight(..), pickLR,
Role(..), ltRole,
coVarKind, coVarRole,
coercionType, coercionKind, coercionKinds, isReflCo,
isReflCo_maybe, coercionRole, coercionKindRole,
mkCoercionType,
mkReflCo, mkCoVarCo,
mkAxInstCo, mkUnbranchedAxInstCo, mkAxInstLHS, mkAxInstRHS,
mkUnbranchedAxInstRHS,
mkPiCo, mkPiCos, mkCoCast,
mkSymCo, mkTransCo, mkNthCo, mkNthCoRole, mkLRCo,
mkInstCo, mkAppCo, mkAppCoFlexible, mkTyConAppCo, mkFunCo,
mkForAllCo, mkUnsafeCo, mkUnivCo, mkSubCo, mkPhantomCo,
mkNewTypeCo, downgradeRole,
mkAxiomRuleCo,
instNewTyCon_maybe,
NormaliseStepper, NormaliseStepResult(..), composeSteppers,
modifyStepResultCo, unwrapNewTypeStepper,
topNormaliseNewType_maybe, topNormaliseTypeX_maybe,
decomposeCo, getCoVar_maybe,
splitAppCo_maybe,
splitForAllCo_maybe,
nthRole, tyConRolesX,
setNominalRole_maybe,
mkCoVar, isCoVar, isCoVarType, coVarName, setCoVarName, setCoVarUnique,
tyCoVarsOfCo, tyCoVarsOfCos, coVarsOfCo, coercionSize,
CvSubstEnv, emptyCvSubstEnv,
CvSubst(..), emptyCvSubst, Coercion.lookupTyVar, lookupCoVar,
isEmptyCvSubst, zapCvSubstEnv, getCvInScope,
substCo, substCos, substCoVar, substCoVars,
substCoWithTy, substCoWithTys,
cvTvSubst, tvCvSubst, mkCvSubst, zipOpenCvSubst,
substTy, extendTvSubst,
extendCvSubstAndInScope, extendTvSubstAndInScope,
substTyVarBndr, substCoVarBndr,
liftCoMatch, liftCoSubstTyVar, liftCoSubstWith,
coreEqCoercion, coreEqCoercion2,
seqCo,
pprCo, pprParendCo,
pprCoAxiom, pprCoAxBranch, pprCoAxBranchHdr,
tidyCo, tidyCos,
applyCo,
) where
#include "HsVersions.h"
import Unify ( MatchEnv(..), matchList )
import TypeRep
import qualified Type
import Type hiding( substTy, substTyVarBndr, extendTvSubst )
import TyCon
import CoAxiom
import Var
import VarEnv
import VarSet
import Binary
import Maybes ( orElse )
import Name ( Name, NamedThing(..), nameUnique, nameModule, getSrcSpan )
import OccName ( parenSymOcc )
import Util
import BasicTypes
import Outputable
import Unique
import Pair
import SrcLoc
import PrelNames ( funTyConKey, eqPrimTyConKey, eqReprPrimTyConKey )
#if __GLASGOW_HASKELL__ < 709
import Control.Applicative hiding ( empty )
import Data.Traversable (traverse, sequenceA)
#endif
import FastString
import ListSetOps
import qualified Data.Data as Data hiding ( TyCon )
import Control.Arrow ( first )
data Coercion
=
Refl Role Type
| TyConAppCo Role TyCon [Coercion]
| AppCo Coercion Coercion
| ForAllCo TyVar Coercion
| CoVarCo CoVar
| AxiomInstCo (CoAxiom Branched) BranchIndex [Coercion]
| UnivCo FastString Role Type Type
| SymCo Coercion
| TransCo Coercion Coercion
| AxiomRuleCo CoAxiomRule [Type] [Coercion]
| NthCo Int Coercion
| LRCo LeftOrRight Coercion
| InstCo Coercion Type
| SubCo Coercion
deriving (Data.Data, Data.Typeable)
data LeftOrRight = CLeft | CRight
deriving( Eq, Data.Data, Data.Typeable )
instance Binary LeftOrRight where
put_ bh CLeft = putByte bh 0
put_ bh CRight = putByte bh 1
get bh = do { h <- getByte bh
; case h of
0 -> return CLeft
_ -> return CRight }
pickLR :: LeftOrRight -> (a,a) -> a
pickLR CLeft (l,_) = l
pickLR CRight (_,r) = r
coVarName :: CoVar -> Name
coVarName = varName
setCoVarUnique :: CoVar -> Unique -> CoVar
setCoVarUnique = setVarUnique
setCoVarName :: CoVar -> Name -> CoVar
setCoVarName = setVarName
isCoVar :: Var -> Bool
isCoVar v = isCoVarType (varType v)
isCoVarType :: Type -> Bool
isCoVarType ty
= case splitTyConApp_maybe ty of
Just (tc,tys) -> (tc `hasKey` eqPrimTyConKey || tc `hasKey` eqReprPrimTyConKey)
&& tys `lengthAtLeast` 2
Nothing -> False
tyCoVarsOfCo :: Coercion -> VarSet
tyCoVarsOfCo (Refl _ ty) = tyVarsOfType ty
tyCoVarsOfCo (TyConAppCo _ _ cos) = tyCoVarsOfCos cos
tyCoVarsOfCo (AppCo co1 co2) = tyCoVarsOfCo co1 `unionVarSet` tyCoVarsOfCo co2
tyCoVarsOfCo (ForAllCo tv co) = tyCoVarsOfCo co `delVarSet` tv
tyCoVarsOfCo (CoVarCo v) = unitVarSet v
tyCoVarsOfCo (AxiomInstCo _ _ cos) = tyCoVarsOfCos cos
tyCoVarsOfCo (UnivCo _ _ ty1 ty2) = tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2
tyCoVarsOfCo (SymCo co) = tyCoVarsOfCo co
tyCoVarsOfCo (TransCo co1 co2) = tyCoVarsOfCo co1 `unionVarSet` tyCoVarsOfCo co2
tyCoVarsOfCo (NthCo _ co) = tyCoVarsOfCo co
tyCoVarsOfCo (LRCo _ co) = tyCoVarsOfCo co
tyCoVarsOfCo (InstCo co ty) = tyCoVarsOfCo co `unionVarSet` tyVarsOfType ty
tyCoVarsOfCo (SubCo co) = tyCoVarsOfCo co
tyCoVarsOfCo (AxiomRuleCo _ ts cs) = tyVarsOfTypes ts `unionVarSet` tyCoVarsOfCos cs
tyCoVarsOfCos :: [Coercion] -> VarSet
tyCoVarsOfCos = mapUnionVarSet tyCoVarsOfCo
coVarsOfCo :: Coercion -> VarSet
coVarsOfCo (Refl _ _) = emptyVarSet
coVarsOfCo (TyConAppCo _ _ cos) = coVarsOfCos cos
coVarsOfCo (AppCo co1 co2) = coVarsOfCo co1 `unionVarSet` coVarsOfCo co2
coVarsOfCo (ForAllCo _ co) = coVarsOfCo co
coVarsOfCo (CoVarCo v) = unitVarSet v
coVarsOfCo (AxiomInstCo _ _ cos) = coVarsOfCos cos
coVarsOfCo (UnivCo _ _ _ _) = emptyVarSet
coVarsOfCo (SymCo co) = coVarsOfCo co
coVarsOfCo (TransCo co1 co2) = coVarsOfCo co1 `unionVarSet` coVarsOfCo co2
coVarsOfCo (NthCo _ co) = coVarsOfCo co
coVarsOfCo (LRCo _ co) = coVarsOfCo co
coVarsOfCo (InstCo co _) = coVarsOfCo co
coVarsOfCo (SubCo co) = coVarsOfCo co
coVarsOfCo (AxiomRuleCo _ _ cos) = coVarsOfCos cos
coVarsOfCos :: [Coercion] -> VarSet
coVarsOfCos = mapUnionVarSet coVarsOfCo
coercionSize :: Coercion -> Int
coercionSize (Refl _ ty) = typeSize ty
coercionSize (TyConAppCo _ _ cos) = 1 + sum (map coercionSize cos)
coercionSize (AppCo co1 co2) = coercionSize co1 + coercionSize co2
coercionSize (ForAllCo _ co) = 1 + coercionSize co
coercionSize (CoVarCo _) = 1
coercionSize (AxiomInstCo _ _ cos) = 1 + sum (map coercionSize cos)
coercionSize (UnivCo _ _ ty1 ty2) = typeSize ty1 + typeSize ty2
coercionSize (SymCo co) = 1 + coercionSize co
coercionSize (TransCo co1 co2) = 1 + coercionSize co1 + coercionSize co2
coercionSize (NthCo _ co) = 1 + coercionSize co
coercionSize (LRCo _ co) = 1 + coercionSize co
coercionSize (InstCo co ty) = 1 + coercionSize co + typeSize ty
coercionSize (SubCo co) = 1 + coercionSize co
coercionSize (AxiomRuleCo _ tys cos) = 1 + sum (map typeSize tys)
+ sum (map coercionSize cos)
tidyCo :: TidyEnv -> Coercion -> Coercion
tidyCo env@(_, subst) co
= go co
where
go (Refl r ty) = Refl r (tidyType env ty)
go (TyConAppCo r tc cos) = let args = map go cos
in args `seqList` TyConAppCo r tc args
go (AppCo co1 co2) = (AppCo $! go co1) $! go co2
go (ForAllCo tv co) = ForAllCo tvp $! (tidyCo envp co)
where
(envp, tvp) = tidyTyVarBndr env tv
go (CoVarCo cv) = case lookupVarEnv subst cv of
Nothing -> CoVarCo cv
Just cv' -> CoVarCo cv'
go (AxiomInstCo con ind cos) = let args = tidyCos env cos
in args `seqList` AxiomInstCo con ind args
go (UnivCo s r ty1 ty2) = (UnivCo s r $! tidyType env ty1) $! tidyType env ty2
go (SymCo co) = SymCo $! go co
go (TransCo co1 co2) = (TransCo $! go co1) $! go co2
go (NthCo d co) = NthCo d $! go co
go (LRCo lr co) = LRCo lr $! go co
go (InstCo co ty) = (InstCo $! go co) $! tidyType env ty
go (SubCo co) = SubCo $! go co
go (AxiomRuleCo ax tys cos) = let tys1 = map (tidyType env) tys
cos1 = tidyCos env cos
in tys1 `seqList` cos1 `seqList`
AxiomRuleCo ax tys1 cos1
tidyCos :: TidyEnv -> [Coercion] -> [Coercion]
tidyCos env = map (tidyCo env)
instance Outputable Coercion where
ppr = pprCo
pprCo, pprParendCo :: Coercion -> SDoc
pprCo co = ppr_co TopPrec co
pprParendCo co = ppr_co TyConPrec co
ppr_co :: TyPrec -> Coercion -> SDoc
ppr_co _ (Refl r ty) = angleBrackets (ppr ty) <> ppr_role r
ppr_co p co@(TyConAppCo _ tc [_,_])
| tc `hasKey` funTyConKey = ppr_fun_co p co
ppr_co _ (TyConAppCo r tc cos) = pprTcApp TyConPrec ppr_co tc cos <> ppr_role r
ppr_co p (AppCo co1 co2) = maybeParen p TyConPrec $
pprCo co1 <+> ppr_co TyConPrec co2
ppr_co p co@(ForAllCo {}) = ppr_forall_co p co
ppr_co _ (CoVarCo cv) = parenSymOcc (getOccName cv) (ppr cv)
ppr_co p (AxiomInstCo con index cos)
= pprPrefixApp p (ppr (getName con) <> brackets (ppr index))
(map (ppr_co TyConPrec) cos)
ppr_co p co@(TransCo {}) = maybeParen p FunPrec $
case trans_co_list co [] of
[] -> panic "ppr_co"
(co:cos) -> sep ( ppr_co FunPrec co
: [ char ';' <+> ppr_co FunPrec co | co <- cos])
ppr_co p (InstCo co ty) = maybeParen p TyConPrec $
pprParendCo co <> ptext (sLit "@") <> pprType ty
ppr_co p (UnivCo s r ty1 ty2) = pprPrefixApp p (ptext (sLit "UnivCo") <+> ftext s <+> ppr r)
[pprParendType ty1, pprParendType ty2]
ppr_co p (SymCo co) = pprPrefixApp p (ptext (sLit "Sym")) [pprParendCo co]
ppr_co p (NthCo n co) = pprPrefixApp p (ptext (sLit "Nth:") <> int n) [pprParendCo co]
ppr_co p (LRCo sel co) = pprPrefixApp p (ppr sel) [pprParendCo co]
ppr_co p (SubCo co) = pprPrefixApp p (ptext (sLit "Sub")) [pprParendCo co]
ppr_co p (AxiomRuleCo co ts cs) = maybeParen p TopPrec $
ppr_axiom_rule_co co ts cs
ppr_axiom_rule_co :: CoAxiomRule -> [Type] -> [Coercion] -> SDoc
ppr_axiom_rule_co co ts ps = ppr (coaxrName co) <> ppTs ts $$ nest 2 (ppPs ps)
where
ppTs [] = Outputable.empty
ppTs [t] = ptext (sLit "@") <> ppr_type TopPrec t
ppTs ts = ptext (sLit "@") <>
parens (hsep $ punctuate comma $ map pprType ts)
ppPs [] = Outputable.empty
ppPs [p] = pprParendCo p
ppPs (p : ps) = ptext (sLit "(") <+> pprCo p $$
vcat [ ptext (sLit ",") <+> pprCo q | q <- ps ] $$
ptext (sLit ")")
ppr_role :: Role -> SDoc
ppr_role r = underscore <> pp_role
where pp_role = case r of
Nominal -> char 'N'
Representational -> char 'R'
Phantom -> char 'P'
trans_co_list :: Coercion -> [Coercion] -> [Coercion]
trans_co_list (TransCo co1 co2) cos = trans_co_list co1 (trans_co_list co2 cos)
trans_co_list co cos = co : cos
instance Outputable LeftOrRight where
ppr CLeft = ptext (sLit "Left")
ppr CRight = ptext (sLit "Right")
ppr_fun_co :: TyPrec -> Coercion -> SDoc
ppr_fun_co p co = pprArrowChain p (split co)
where
split :: Coercion -> [SDoc]
split (TyConAppCo _ f [arg,res])
| f `hasKey` funTyConKey
= ppr_co FunPrec arg : split res
split co = [ppr_co TopPrec co]
ppr_forall_co :: TyPrec -> Coercion -> SDoc
ppr_forall_co p ty
= maybeParen p FunPrec $
sep [pprForAll tvs, ppr_co TopPrec rho]
where
(tvs, rho) = split1 [] ty
split1 tvs (ForAllCo tv ty) = split1 (tv:tvs) ty
split1 tvs ty = (reverse tvs, ty)
pprCoAxiom :: CoAxiom br -> SDoc
pprCoAxiom ax@(CoAxiom { co_ax_tc = tc, co_ax_branches = branches })
= hang (ptext (sLit "axiom") <+> ppr ax <+> dcolon)
2 (vcat (map (pprCoAxBranch tc) $ fromBranchList branches))
pprCoAxBranch :: TyCon -> CoAxBranch -> SDoc
pprCoAxBranch fam_tc (CoAxBranch { cab_tvs = tvs
, cab_lhs = lhs
, cab_rhs = rhs })
= hang (pprUserForAll tvs)
2 (hang (pprTypeApp fam_tc lhs) 2 (equals <+> (ppr rhs)))
pprCoAxBranchHdr :: CoAxiom br -> BranchIndex -> SDoc
pprCoAxBranchHdr ax@(CoAxiom { co_ax_tc = fam_tc, co_ax_name = name }) index
| CoAxBranch { cab_lhs = tys, cab_loc = loc } <- coAxiomNthBranch ax index
= hang (pprTypeApp fam_tc tys)
2 (ptext (sLit "-- Defined") <+> ppr_loc loc)
where
ppr_loc loc
| isGoodSrcSpan loc
= ptext (sLit "at") <+> ppr (srcSpanStart loc)
| otherwise
= ptext (sLit "in") <+>
quotes (ppr (nameModule name))
decomposeCo :: Arity -> Coercion -> [Coercion]
decomposeCo arity co
= [mkNthCo n co | n <- [0..(arity1)] ]
getCoVar_maybe :: Coercion -> Maybe CoVar
getCoVar_maybe (CoVarCo cv) = Just cv
getCoVar_maybe _ = Nothing
splitAppCo_maybe :: Coercion -> Maybe (Coercion, Coercion)
splitAppCo_maybe (AppCo co1 co2) = Just (co1, co2)
splitAppCo_maybe (TyConAppCo r tc cos)
| isDecomposableTyCon tc || cos `lengthExceeds` tyConArity tc
, Just (cos', co') <- snocView cos
, Just co'' <- setNominalRole_maybe co'
= Just (mkTyConAppCo r tc cos', co'')
splitAppCo_maybe (Refl r ty)
| Just (ty1, ty2) <- splitAppTy_maybe ty
= Just (Refl r ty1, Refl Nominal ty2)
splitAppCo_maybe _ = Nothing
splitForAllCo_maybe :: Coercion -> Maybe (TyVar, Coercion)
splitForAllCo_maybe (ForAllCo tv co) = Just (tv, co)
splitForAllCo_maybe _ = Nothing
coVarKind :: CoVar -> (Type,Type)
coVarKind cv
| Just (tc, [_kind,ty1,ty2]) <- splitTyConApp_maybe (varType cv)
= ASSERT(tc `hasKey` eqPrimTyConKey || tc `hasKey` eqReprPrimTyConKey)
(ty1,ty2)
| otherwise = panic "coVarKind, non coercion variable"
coVarRole :: CoVar -> Role
coVarRole cv
| tc `hasKey` eqPrimTyConKey
= Nominal
| tc `hasKey` eqReprPrimTyConKey
= Representational
| otherwise
= pprPanic "coVarRole: unknown tycon" (ppr cv)
where
tc = case tyConAppTyCon_maybe (varType cv) of
Just tc0 -> tc0
Nothing -> pprPanic "coVarRole: not tyconapp" (ppr cv)
mkCoercionType :: Role -> Type -> Type -> Type
mkCoercionType Nominal = mkPrimEqPred
mkCoercionType Representational = mkReprPrimEqPred
mkCoercionType Phantom = panic "mkCoercionType"
isReflCo :: Coercion -> Bool
isReflCo (Refl {}) = True
isReflCo _ = False
isReflCo_maybe :: Coercion -> Maybe Type
isReflCo_maybe (Refl _ ty) = Just ty
isReflCo_maybe _ = Nothing
mkCoVarCo :: CoVar -> Coercion
mkCoVarCo cv
| ty1 `eqType` ty2 = Refl (coVarRole cv) ty1
| otherwise = CoVarCo cv
where
(ty1, ty2) = ASSERT( isCoVar cv ) coVarKind cv
mkReflCo :: Role -> Type -> Coercion
mkReflCo = Refl
mkAxInstCo :: Role -> CoAxiom br -> BranchIndex -> [Type] -> Coercion
mkAxInstCo role ax index tys
| arity == n_tys = downgradeRole role ax_role $ AxiomInstCo ax_br index rtys
| otherwise = ASSERT( arity < n_tys )
downgradeRole role ax_role $
foldl AppCo (AxiomInstCo ax_br index (take arity rtys))
(drop arity rtys)
where
n_tys = length tys
ax_br = toBranchedAxiom ax
branch = coAxiomNthBranch ax_br index
arity = length $ coAxBranchTyVars branch
arg_roles = coAxBranchRoles branch
rtys = zipWith mkReflCo (arg_roles ++ repeat Nominal) tys
ax_role = coAxiomRole ax
mkUnbranchedAxInstCo :: Role -> CoAxiom Unbranched -> [Type] -> Coercion
mkUnbranchedAxInstCo role ax tys
= mkAxInstCo role ax 0 tys
mkAxInstLHS, mkAxInstRHS :: CoAxiom br -> BranchIndex -> [Type] -> Type
mkAxInstLHS ax index tys
| CoAxBranch { cab_tvs = tvs, cab_lhs = lhs } <- coAxiomNthBranch ax index
, (tys1, tys2) <- splitAtList tvs tys
= ASSERT( tvs `equalLength` tys1 )
mkTyConApp (coAxiomTyCon ax) (substTysWith tvs tys1 lhs ++ tys2)
mkAxInstRHS ax index tys
| CoAxBranch { cab_tvs = tvs, cab_rhs = rhs } <- coAxiomNthBranch ax index
, (tys1, tys2) <- splitAtList tvs tys
= ASSERT( tvs `equalLength` tys1 )
mkAppTys (substTyWith tvs tys1 rhs) tys2
mkUnbranchedAxInstRHS :: CoAxiom Unbranched -> [Type] -> Type
mkUnbranchedAxInstRHS ax = mkAxInstRHS ax 0
mkAppCo :: Coercion -> Coercion -> Coercion
mkAppCo co1 co2 = mkAppCoFlexible co1 Nominal co2
mkAppCoFlexible :: Coercion -> Role -> Coercion -> Coercion
mkAppCoFlexible (Refl r ty1) _ (Refl _ ty2)
= Refl r (mkAppTy ty1 ty2)
mkAppCoFlexible (Refl r ty1) r2 co2
| Just (tc, tys) <- splitTyConApp_maybe ty1
= TyConAppCo r tc (zip_roles (tyConRolesX r tc) tys)
where
zip_roles (r1:_) [] = [downgradeRole r1 r2 co2]
zip_roles (r1:rs) (ty1:tys) = mkReflCo r1 ty1 : zip_roles rs tys
zip_roles _ _ = panic "zip_roles"
mkAppCoFlexible (TyConAppCo r tc cos) r2 co
= case r of
Nominal -> ASSERT( r2 == Nominal )
TyConAppCo Nominal tc (cos ++ [co])
Representational -> TyConAppCo Representational tc (cos ++ [co'])
where new_role = (tyConRolesX Representational tc) !! (length cos)
co' = downgradeRole new_role r2 co
Phantom -> TyConAppCo Phantom tc (cos ++ [mkPhantomCo co])
mkAppCoFlexible co1 _r2 co2 = ASSERT( _r2 == Nominal )
AppCo co1 co2
mkAppCos :: Coercion -> [Coercion] -> Coercion
mkAppCos co1 cos = foldl mkAppCo co1 cos
mkTyConAppCo :: Role -> TyCon -> [Coercion] -> Coercion
mkTyConAppCo r tc cos
| Just (tv_co_prs, rhs_ty, leftover_cos) <- tcExpandTyCon_maybe tc cos
= mkAppCos (liftCoSubst r tv_co_prs rhs_ty) leftover_cos
| Just tys <- traverse isReflCo_maybe cos
= Refl r (mkTyConApp tc tys)
| otherwise = TyConAppCo r tc cos
mkFunCo :: Role -> Coercion -> Coercion -> Coercion
mkFunCo r co1 co2 = mkTyConAppCo r funTyCon [co1, co2]
mkForAllCo :: Var -> Coercion -> Coercion
mkForAllCo tv (Refl r ty) = ASSERT( isTyVar tv ) Refl r (mkForAllTy tv ty)
mkForAllCo tv co = ASSERT( isTyVar tv ) ForAllCo tv co
mkSymCo :: Coercion -> Coercion
mkSymCo co@(Refl {}) = co
mkSymCo (UnivCo s r ty1 ty2) = UnivCo s r ty2 ty1
mkSymCo (SymCo co) = co
mkSymCo co = SymCo co
mkTransCo :: Coercion -> Coercion -> Coercion
mkTransCo (Refl {}) co = co
mkTransCo co (Refl {}) = co
mkTransCo co1 co2 = TransCo co1 co2
mkNthCoRole :: Role -> Int -> Coercion -> Coercion
mkNthCoRole role n co
= downgradeRole role nth_role $ nth_co
where
nth_co = mkNthCo n co
nth_role = coercionRole nth_co
mkNthCo :: Int -> Coercion -> Coercion
mkNthCo n (Refl r ty) = ASSERT( ok_tc_app ty n )
Refl r' (tyConAppArgN n ty)
where tc = tyConAppTyCon ty
r' = nthRole r tc n
mkNthCo n co = ASSERT( ok_tc_app _ty1 n && ok_tc_app _ty2 n )
NthCo n co
where
Pair _ty1 _ty2 = coercionKind co
mkLRCo :: LeftOrRight -> Coercion -> Coercion
mkLRCo lr (Refl eq ty) = Refl eq (pickLR lr (splitAppTy ty))
mkLRCo lr co = LRCo lr co
ok_tc_app :: Type -> Int -> Bool
ok_tc_app ty n = case splitTyConApp_maybe ty of
Just (_, tys) -> tys `lengthExceeds` n
Nothing -> False
mkInstCo :: Coercion -> Type -> Coercion
mkInstCo co ty = InstCo co ty
mkUnsafeCo :: Type -> Type -> Coercion
mkUnsafeCo = mkUnivCo (fsLit "mkUnsafeCo") Representational
mkUnivCo :: FastString -> Role -> Type -> Type -> Coercion
mkUnivCo prov role ty1 ty2
| ty1 `eqType` ty2 = Refl role ty1
| otherwise = UnivCo prov role ty1 ty2
mkAxiomRuleCo :: CoAxiomRule -> [Type] -> [Coercion] -> Coercion
mkAxiomRuleCo = AxiomRuleCo
mkSubCo :: Coercion -> Coercion
mkSubCo (Refl Nominal ty) = Refl Representational ty
mkSubCo (TyConAppCo Nominal tc cos)
= TyConAppCo Representational tc (applyRoles tc cos)
mkSubCo (UnivCo s Nominal ty1 ty2) = UnivCo s Representational ty1 ty2
mkSubCo co = ASSERT2( coercionRole co == Nominal, ppr co <+> ppr (coercionRole co) )
SubCo co
downgradeRole_maybe :: Role
-> Role
-> Coercion -> Maybe Coercion
downgradeRole_maybe Representational Nominal co = Just (mkSubCo co)
downgradeRole_maybe Nominal Representational _ = Nothing
downgradeRole_maybe Phantom Phantom co = Just co
downgradeRole_maybe Phantom _ co = Just (mkPhantomCo co)
downgradeRole_maybe _ Phantom _ = Nothing
downgradeRole_maybe _ _ co = Just co
downgradeRole :: Role
-> Role
-> Coercion -> Coercion
downgradeRole r1 r2 co
= case downgradeRole_maybe r1 r2 co of
Just co' -> co'
Nothing -> pprPanic "downgradeRole" (ppr co)
setNominalRole_maybe :: Coercion -> Maybe Coercion
setNominalRole_maybe co
| Nominal <- coercionRole co = Just co
setNominalRole_maybe (SubCo co) = Just co
setNominalRole_maybe (Refl _ ty) = Just $ Refl Nominal ty
setNominalRole_maybe (TyConAppCo Representational tc coes)
= do { cos' <- mapM setNominalRole_maybe coes
; return $ TyConAppCo Nominal tc cos' }
setNominalRole_maybe (UnivCo s Representational ty1 ty2) = Just $ UnivCo s Nominal ty1 ty2
setNominalRole_maybe (TransCo co1 co2)
= TransCo <$> setNominalRole_maybe co1 <*> setNominalRole_maybe co2
setNominalRole_maybe (AppCo co1 co2)
= AppCo <$> setNominalRole_maybe co1 <*> pure co2
setNominalRole_maybe (ForAllCo tv co)
= ForAllCo tv <$> setNominalRole_maybe co
setNominalRole_maybe (NthCo n co)
= NthCo n <$> setNominalRole_maybe co
setNominalRole_maybe (InstCo co ty)
= InstCo <$> setNominalRole_maybe co <*> pure ty
setNominalRole_maybe _ = Nothing
mkPhantomCo :: Coercion -> Coercion
mkPhantomCo co
| Just ty <- isReflCo_maybe co = Refl Phantom ty
| Pair ty1 ty2 <- coercionKind co = UnivCo (fsLit "mkPhantomCo") Phantom ty1 ty2
applyRole :: Role -> Coercion -> Coercion
applyRole Nominal = id
applyRole Representational = mkSubCo
applyRole Phantom = mkPhantomCo
applyRoles :: TyCon -> [Coercion] -> [Coercion]
applyRoles tc cos
= zipWith applyRole (tyConRolesX Representational tc) cos
tyConRolesX :: Role -> TyCon -> [Role]
tyConRolesX Representational tc = tyConRoles tc ++ repeat Nominal
tyConRolesX role _ = repeat role
nthRole :: Role -> TyCon -> Int -> Role
nthRole Nominal _ _ = Nominal
nthRole Phantom _ _ = Phantom
nthRole Representational tc n
= (tyConRolesX Representational tc) !! n
ltRole :: Role -> Role -> Bool
ltRole Phantom _ = False
ltRole Representational Phantom = True
ltRole Representational _ = False
ltRole Nominal Nominal = False
ltRole Nominal _ = True
mkNewTypeCo :: Name -> TyCon -> [TyVar] -> [Role] -> Type -> CoAxiom Unbranched
mkNewTypeCo name tycon tvs roles rhs_ty
= CoAxiom { co_ax_unique = nameUnique name
, co_ax_name = name
, co_ax_implicit = True
, co_ax_role = Representational
, co_ax_tc = tycon
, co_ax_branches = FirstBranch branch }
where branch = CoAxBranch { cab_loc = getSrcSpan name
, cab_tvs = tvs
, cab_lhs = mkTyVarTys tvs
, cab_roles = roles
, cab_rhs = rhs_ty
, cab_incomps = [] }
mkPiCos :: Role -> [Var] -> Coercion -> Coercion
mkPiCos r vs co = foldr (mkPiCo r) co vs
mkPiCo :: Role -> Var -> Coercion -> Coercion
mkPiCo r v co | isTyVar v = mkForAllCo v co
| otherwise = mkFunCo r (mkReflCo r (varType v)) co
mkCoCast :: Coercion -> Coercion -> Coercion
mkCoCast c g
= mkSymCo g1 `mkTransCo` c `mkTransCo` g2
where
[_reflk, g1, g2] = decomposeCo 3 g
instNewTyCon_maybe :: TyCon -> [Type] -> Maybe (Type, Coercion)
instNewTyCon_maybe tc tys
| Just (tvs, ty, co_tc) <- unwrapNewTyConEtad_maybe tc
, tvs `leLength` tys
= Just ( applyTysX tvs ty tys
, mkUnbranchedAxInstCo Representational co_tc tys)
| otherwise
= Nothing
type NormaliseStepper = RecTcChecker
-> TyCon
-> [Type]
-> NormaliseStepResult
data NormaliseStepResult
= NS_Done
| NS_Abort
| NS_Step RecTcChecker Type Coercion
modifyStepResultCo :: (Coercion -> Coercion)
-> NormaliseStepResult -> NormaliseStepResult
modifyStepResultCo f (NS_Step rec_nts ty co) = NS_Step rec_nts ty (f co)
modifyStepResultCo _ result = result
composeSteppers :: NormaliseStepper -> NormaliseStepper
-> NormaliseStepper
composeSteppers step1 step2 rec_nts tc tys
= case step1 rec_nts tc tys of
success@(NS_Step {}) -> success
NS_Done -> step2 rec_nts tc tys
NS_Abort -> NS_Abort
unwrapNewTypeStepper :: NormaliseStepper
unwrapNewTypeStepper rec_nts tc tys
| Just (ty', co) <- instNewTyCon_maybe tc tys
= case checkRecTc rec_nts tc of
Just rec_nts' -> NS_Step rec_nts' ty' co
Nothing -> NS_Abort
| otherwise
= NS_Done
topNormaliseTypeX_maybe :: NormaliseStepper -> Type -> Maybe (Coercion, Type)
topNormaliseTypeX_maybe stepper
= go initRecTc Nothing
where
go rec_nts mb_co1 ty
| Just (tc, tys) <- splitTyConApp_maybe ty
= case stepper rec_nts tc tys of
NS_Step rec_nts' ty' co2
-> go rec_nts' (mb_co1 `trans` co2) ty'
NS_Done -> all_done
NS_Abort -> Nothing
| otherwise
= all_done
where
all_done | Just co <- mb_co1 = Just (co, ty)
| otherwise = Nothing
Nothing `trans` co2 = Just co2
(Just co1) `trans` co2 = Just (co1 `mkTransCo` co2)
topNormaliseNewType_maybe :: Type -> Maybe (Coercion, Type)
topNormaliseNewType_maybe ty
= topNormaliseTypeX_maybe unwrapNewTypeStepper ty
coreEqCoercion :: Coercion -> Coercion -> Bool
coreEqCoercion co1 co2 = coreEqCoercion2 rn_env co1 co2
where rn_env = mkRnEnv2 (mkInScopeSet (tyCoVarsOfCo co1 `unionVarSet` tyCoVarsOfCo co2))
coreEqCoercion2 :: RnEnv2 -> Coercion -> Coercion -> Bool
coreEqCoercion2 env (Refl eq1 ty1) (Refl eq2 ty2) = eq1 == eq2 && eqTypeX env ty1 ty2
coreEqCoercion2 env (TyConAppCo eq1 tc1 cos1) (TyConAppCo eq2 tc2 cos2)
= eq1 == eq2 && tc1 == tc2 && all2 (coreEqCoercion2 env) cos1 cos2
coreEqCoercion2 env (AppCo co11 co12) (AppCo co21 co22)
= coreEqCoercion2 env co11 co21 && coreEqCoercion2 env co12 co22
coreEqCoercion2 env (ForAllCo v1 co1) (ForAllCo v2 co2)
= coreEqCoercion2 (rnBndr2 env v1 v2) co1 co2
coreEqCoercion2 env (CoVarCo cv1) (CoVarCo cv2)
= rnOccL env cv1 == rnOccR env cv2
coreEqCoercion2 env (AxiomInstCo con1 ind1 cos1) (AxiomInstCo con2 ind2 cos2)
= con1 == con2
&& ind1 == ind2
&& all2 (coreEqCoercion2 env) cos1 cos2
coreEqCoercion2 env (UnivCo _ r1 ty11 ty12) (UnivCo _ r2 ty21 ty22)
= r1 == r2 && eqTypeX env ty11 ty21 && eqTypeX env ty12 ty22
coreEqCoercion2 env (SymCo co1) (SymCo co2)
= coreEqCoercion2 env co1 co2
coreEqCoercion2 env (TransCo co11 co12) (TransCo co21 co22)
= coreEqCoercion2 env co11 co21 && coreEqCoercion2 env co12 co22
coreEqCoercion2 env (NthCo d1 co1) (NthCo d2 co2)
= d1 == d2 && coreEqCoercion2 env co1 co2
coreEqCoercion2 env (LRCo d1 co1) (LRCo d2 co2)
= d1 == d2 && coreEqCoercion2 env co1 co2
coreEqCoercion2 env (InstCo co1 ty1) (InstCo co2 ty2)
= coreEqCoercion2 env co1 co2 && eqTypeX env ty1 ty2
coreEqCoercion2 env (SubCo co1) (SubCo co2)
= coreEqCoercion2 env co1 co2
coreEqCoercion2 env (AxiomRuleCo a1 ts1 cs1) (AxiomRuleCo a2 ts2 cs2)
= a1 == a2 && all2 (eqTypeX env) ts1 ts2 && all2 (coreEqCoercion2 env) cs1 cs2
coreEqCoercion2 _ _ _ = False
type CvSubstEnv = VarEnv Coercion
emptyCvSubstEnv :: CvSubstEnv
emptyCvSubstEnv = emptyVarEnv
data CvSubst
= CvSubst InScopeSet
TvSubstEnv
CvSubstEnv
instance Outputable CvSubst where
ppr (CvSubst ins tenv cenv)
= brackets $ sep[ ptext (sLit "CvSubst"),
nest 2 (ptext (sLit "In scope:") <+> ppr ins),
nest 2 (ptext (sLit "Type env:") <+> ppr tenv),
nest 2 (ptext (sLit "Coercion env:") <+> ppr cenv) ]
emptyCvSubst :: CvSubst
emptyCvSubst = CvSubst emptyInScopeSet emptyVarEnv emptyVarEnv
isEmptyCvSubst :: CvSubst -> Bool
isEmptyCvSubst (CvSubst _ tenv cenv) = isEmptyVarEnv tenv && isEmptyVarEnv cenv
getCvInScope :: CvSubst -> InScopeSet
getCvInScope (CvSubst in_scope _ _) = in_scope
zapCvSubstEnv :: CvSubst -> CvSubst
zapCvSubstEnv (CvSubst in_scope _ _) = CvSubst in_scope emptyVarEnv emptyVarEnv
cvTvSubst :: CvSubst -> TvSubst
cvTvSubst (CvSubst in_scope tvs _) = TvSubst in_scope tvs
tvCvSubst :: TvSubst -> CvSubst
tvCvSubst (TvSubst in_scope tenv) = CvSubst in_scope tenv emptyCvSubstEnv
extendTvSubst :: CvSubst -> TyVar -> Type -> CvSubst
extendTvSubst (CvSubst in_scope tenv cenv) tv ty
= CvSubst in_scope (extendVarEnv tenv tv ty) cenv
extendTvSubstAndInScope :: CvSubst -> TyVar -> Type -> CvSubst
extendTvSubstAndInScope (CvSubst in_scope tenv cenv) tv ty
= CvSubst (in_scope `extendInScopeSetSet` tyVarsOfType ty)
(extendVarEnv tenv tv ty)
cenv
extendCvSubstAndInScope :: CvSubst -> CoVar -> Coercion -> CvSubst
extendCvSubstAndInScope (CvSubst in_scope tenv cenv) cv co
= CvSubst (in_scope `extendInScopeSetSet` tyCoVarsOfCo co)
tenv
(extendVarEnv cenv cv co)
substCoVarBndr :: CvSubst -> CoVar -> (CvSubst, CoVar)
substCoVarBndr subst@(CvSubst in_scope tenv cenv) old_var
= ASSERT( isCoVar old_var )
(CvSubst (in_scope `extendInScopeSet` new_var) tenv new_cenv, new_var)
where
new_co = mkCoVarCo new_var
no_change = new_var == old_var && not (isReflCo new_co)
new_cenv | no_change = delVarEnv cenv old_var
| otherwise = extendVarEnv cenv old_var new_co
new_var = uniqAway in_scope subst_old_var
subst_old_var = mkCoVar (varName old_var) (substTy subst (varType old_var))
substTyVarBndr :: CvSubst -> TyVar -> (CvSubst, TyVar)
substTyVarBndr (CvSubst in_scope tenv cenv) old_var
= case Type.substTyVarBndr (TvSubst in_scope tenv) old_var of
(TvSubst in_scope' tenv', new_var) -> (CvSubst in_scope' tenv' cenv, new_var)
mkCvSubst :: InScopeSet -> [(Var,Coercion)] -> CvSubst
mkCvSubst in_scope prs = CvSubst in_scope Type.emptyTvSubstEnv (mkVarEnv prs)
zipOpenCvSubst :: [Var] -> [Coercion] -> CvSubst
zipOpenCvSubst vs cos
| debugIsOn && (length vs /= length cos)
= pprTrace "zipOpenCvSubst" (ppr vs $$ ppr cos) emptyCvSubst
| otherwise
= CvSubst (mkInScopeSet (tyCoVarsOfCos cos)) emptyTvSubstEnv (zipVarEnv vs cos)
substCoWithTy :: InScopeSet -> TyVar -> Type -> Coercion -> Coercion
substCoWithTy in_scope tv ty = substCoWithTys in_scope [tv] [ty]
substCoWithTys :: InScopeSet -> [TyVar] -> [Type] -> Coercion -> Coercion
substCoWithTys in_scope tvs tys co
| debugIsOn && (length tvs /= length tys)
= pprTrace "substCoWithTys" (ppr tvs $$ ppr tys) co
| otherwise
= ASSERT( length tvs == length tys )
substCo (CvSubst in_scope (zipVarEnv tvs tys) emptyVarEnv) co
substCo :: CvSubst -> Coercion -> Coercion
substCo subst co | isEmptyCvSubst subst = co
| otherwise = subst_co subst co
substCos :: CvSubst -> [Coercion] -> [Coercion]
substCos subst cos | isEmptyCvSubst subst = cos
| otherwise = map (substCo subst) cos
substTy :: CvSubst -> Type -> Type
substTy subst = Type.substTy (cvTvSubst subst)
subst_co :: CvSubst -> Coercion -> Coercion
subst_co subst co
= go co
where
go_ty :: Type -> Type
go_ty = Coercion.substTy subst
go :: Coercion -> Coercion
go (Refl eq ty) = Refl eq $! go_ty ty
go (TyConAppCo eq tc cos) = let args = map go cos
in args `seqList` TyConAppCo eq tc args
go (AppCo co1 co2) = mkAppCo (go co1) $! go co2
go (ForAllCo tv co) = case substTyVarBndr subst tv of
(subst', tv') ->
ForAllCo tv' $! subst_co subst' co
go (CoVarCo cv) = substCoVar subst cv
go (AxiomInstCo con ind cos) = AxiomInstCo con ind $! map go cos
go (UnivCo s r ty1 ty2) = (UnivCo s r $! go_ty ty1) $! go_ty ty2
go (SymCo co) = mkSymCo (go co)
go (TransCo co1 co2) = mkTransCo (go co1) (go co2)
go (NthCo d co) = mkNthCo d (go co)
go (LRCo lr co) = mkLRCo lr (go co)
go (InstCo co ty) = mkInstCo (go co) $! go_ty ty
go (SubCo co) = mkSubCo (go co)
go (AxiomRuleCo co ts cs) = let ts1 = map go_ty ts
cs1 = map go cs
in ts1 `seqList` cs1 `seqList`
AxiomRuleCo co ts1 cs1
substCoVar :: CvSubst -> CoVar -> Coercion
substCoVar (CvSubst in_scope _ cenv) cv
| Just co <- lookupVarEnv cenv cv = co
| Just cv1 <- lookupInScope in_scope cv = ASSERT( isCoVar cv1 ) CoVarCo cv1
| otherwise = WARN( True, ptext (sLit "substCoVar not in scope") <+> ppr cv $$ ppr in_scope)
ASSERT( isCoVar cv ) CoVarCo cv
substCoVars :: CvSubst -> [CoVar] -> [Coercion]
substCoVars subst cvs = map (substCoVar subst) cvs
lookupTyVar :: CvSubst -> TyVar -> Maybe Type
lookupTyVar (CvSubst _ tenv _) tv = lookupVarEnv tenv tv
lookupCoVar :: CvSubst -> Var -> Maybe Coercion
lookupCoVar (CvSubst _ _ cenv) v = lookupVarEnv cenv v
data LiftCoSubst = LCS InScopeSet LiftCoEnv
type LiftCoEnv = VarEnv Coercion
liftCoSubstWith :: Role -> [TyVar] -> [Coercion] -> Type -> Coercion
liftCoSubstWith r tvs cos ty
= liftCoSubst r (zipEqual "liftCoSubstWith" tvs cos) ty
liftCoSubst :: Role -> [(TyVar,Coercion)] -> Type -> Coercion
liftCoSubst r prs ty
| null prs = Refl r ty
| otherwise = ty_co_subst (LCS (mkInScopeSet (tyCoVarsOfCos (map snd prs)))
(mkVarEnv prs)) r ty
ty_co_subst :: LiftCoSubst -> Role -> Type -> Coercion
ty_co_subst subst role ty
= go role ty
where
go Phantom ty = lift_phantom ty
go role (TyVarTy tv) = liftCoSubstTyVar subst role tv
`orElse` Refl role (TyVarTy tv)
go role (AppTy ty1 ty2) = mkAppCo (go role ty1) (go Nominal ty2)
go role (TyConApp tc tys) = mkTyConAppCo role tc
(zipWith go (tyConRolesX role tc) tys)
go role (FunTy ty1 ty2) = mkFunCo role (go role ty1) (go role ty2)
go role (ForAllTy v ty) = mkForAllCo v' $! (ty_co_subst subst' role ty)
where
(subst', v') = liftCoSubstTyVarBndr subst v
go role ty@(LitTy {}) = ASSERT( role == Nominal )
mkReflCo role ty
lift_phantom ty = mkUnivCo (fsLit "lift_phantom")
Phantom (liftCoSubstLeft subst ty)
(liftCoSubstRight subst ty)
liftCoSubstTyVar :: LiftCoSubst -> Role -> TyVar -> Maybe Coercion
liftCoSubstTyVar (LCS _ cenv) r tv
= do { co <- lookupVarEnv cenv tv
; let co_role = coercionRole co
; downgradeRole_maybe r co_role co }
liftCoSubstTyVarBndr :: LiftCoSubst -> TyVar -> (LiftCoSubst, TyVar)
liftCoSubstTyVarBndr subst@(LCS in_scope cenv) old_var
= (LCS (in_scope `extendInScopeSet` new_var) new_cenv, new_var)
where
new_cenv | no_change = delVarEnv cenv old_var
| otherwise = extendVarEnv cenv old_var (Refl Nominal (TyVarTy new_var))
no_change = no_kind_change && (new_var == old_var)
new_var1 = uniqAway in_scope old_var
old_ki = tyVarKind old_var
no_kind_change = isEmptyVarSet (tyVarsOfType old_ki)
new_var | no_kind_change = new_var1
| otherwise = setTyVarKind new_var1 (subst_kind subst old_ki)
liftCoSubstLeft :: LiftCoSubst -> Type -> Type
liftCoSubstLeft (LCS in_scope cenv) ty
= Type.substTy (mkTvSubst in_scope (mapVarEnv (pFst . coercionKind) cenv)) ty
liftCoSubstRight :: LiftCoSubst -> Type -> Type
liftCoSubstRight (LCS in_scope cenv) ty
= Type.substTy (mkTvSubst in_scope (mapVarEnv (pSnd . coercionKind) cenv)) ty
subst_kind :: LiftCoSubst -> Kind -> Kind
subst_kind subst@(LCS _ cenv) kind
= go kind
where
go (LitTy n) = n `seq` LitTy n
go (TyVarTy kv) = subst_kv kv
go (TyConApp tc tys) = let args = map go tys
in args `seqList` TyConApp tc args
go (FunTy arg res) = (FunTy $! (go arg)) $! (go res)
go (AppTy fun arg) = mkAppTy (go fun) $! (go arg)
go (ForAllTy tv ty) = case liftCoSubstTyVarBndr subst tv of
(subst', tv') ->
ForAllTy tv' $! (subst_kind subst' ty)
subst_kv kv
| Just co <- lookupVarEnv cenv kv
, let co_kind = coercionKind co
= ASSERT2( pFst co_kind `eqKind` pSnd co_kind, ppr kv $$ ppr co )
pFst co_kind
| otherwise
= TyVarTy kv
liftCoMatch :: TyVarSet -> Type -> Coercion -> Maybe LiftCoSubst
liftCoMatch tmpls ty co
= case ty_co_match menv emptyVarEnv ty co of
Just cenv -> Just (LCS in_scope cenv)
Nothing -> Nothing
where
menv = ME { me_tmpls = tmpls, me_env = mkRnEnv2 in_scope }
in_scope = mkInScopeSet (tmpls `unionVarSet` tyCoVarsOfCo co)
ty_co_match :: MatchEnv -> LiftCoEnv -> Type -> Coercion -> Maybe LiftCoEnv
ty_co_match menv subst ty co
| Just ty' <- coreView ty = ty_co_match menv subst ty' co
ty_co_match menv cenv (TyVarTy tv1) co
| Just co1' <- lookupVarEnv cenv tv1'
= if coreEqCoercion2 (nukeRnEnvL rn_env) co1' co
then Just cenv
else Nothing
| tv1' `elemVarSet` me_tmpls menv
= if any (inRnEnvR rn_env) (varSetElems (tyCoVarsOfCo co))
then Nothing
else return (extendVarEnv cenv tv1' co)
| otherwise
= Nothing
where
rn_env = me_env menv
tv1' = rnOccL rn_env tv1
ty_co_match menv subst (AppTy ty1 ty2) co
| Just (co1, co2) <- splitAppCo_maybe co
= do { subst' <- ty_co_match menv subst ty1 co1
; ty_co_match menv subst' ty2 co2 }
ty_co_match menv subst (TyConApp tc1 tys) (TyConAppCo _ tc2 cos)
| tc1 == tc2 = ty_co_matches menv subst tys cos
ty_co_match menv subst (FunTy ty1 ty2) (TyConAppCo _ tc cos)
| tc == funTyCon = ty_co_matches menv subst [ty1,ty2] cos
ty_co_match menv subst (ForAllTy tv1 ty) (ForAllCo tv2 co)
= ty_co_match menv' subst ty co
where
menv' = menv { me_env = rnBndr2 (me_env menv) tv1 tv2 }
ty_co_match menv subst ty co
| Just co' <- pushRefl co = ty_co_match menv subst ty co'
| otherwise = Nothing
ty_co_matches :: MatchEnv -> LiftCoEnv -> [Type] -> [Coercion] -> Maybe LiftCoEnv
ty_co_matches menv = matchList (ty_co_match menv)
pushRefl :: Coercion -> Maybe Coercion
pushRefl (Refl Nominal (AppTy ty1 ty2))
= Just (AppCo (Refl Nominal ty1) (Refl Nominal ty2))
pushRefl (Refl r (FunTy ty1 ty2))
= Just (TyConAppCo r funTyCon [Refl r ty1, Refl r ty2])
pushRefl (Refl r (TyConApp tc tys))
= Just (TyConAppCo r tc (zipWith mkReflCo (tyConRolesX r tc) tys))
pushRefl (Refl r (ForAllTy tv ty)) = Just (ForAllCo tv (Refl r ty))
pushRefl _ = Nothing
seqCo :: Coercion -> ()
seqCo (Refl eq ty) = eq `seq` seqType ty
seqCo (TyConAppCo eq tc cos) = eq `seq` tc `seq` seqCos cos
seqCo (AppCo co1 co2) = seqCo co1 `seq` seqCo co2
seqCo (ForAllCo tv co) = tv `seq` seqCo co
seqCo (CoVarCo cv) = cv `seq` ()
seqCo (AxiomInstCo con ind cos) = con `seq` ind `seq` seqCos cos
seqCo (UnivCo s r ty1 ty2) = s `seq` r `seq` seqType ty1 `seq` seqType ty2
seqCo (SymCo co) = seqCo co
seqCo (TransCo co1 co2) = seqCo co1 `seq` seqCo co2
seqCo (NthCo _ co) = seqCo co
seqCo (LRCo _ co) = seqCo co
seqCo (InstCo co ty) = seqCo co `seq` seqType ty
seqCo (SubCo co) = seqCo co
seqCo (AxiomRuleCo _ ts cs) = seqTypes ts `seq` seqCos cs
seqCos :: [Coercion] -> ()
seqCos [] = ()
seqCos (co:cos) = seqCo co `seq` seqCos cos
coercionType :: Coercion -> Type
coercionType co = case coercionKindRole co of
(Pair ty1 ty2, r) -> mkCoercionType r ty1 ty2
coercionKind :: Coercion -> Pair Type
coercionKind co = go co
where
go (Refl _ ty) = Pair ty ty
go (TyConAppCo _ tc cos) = mkTyConApp tc <$> (sequenceA $ map go cos)
go (AppCo co1 co2) = mkAppTy <$> go co1 <*> go co2
go (ForAllCo tv co) = mkForAllTy tv <$> go co
go (CoVarCo cv) = toPair $ coVarKind cv
go (AxiomInstCo ax ind cos)
| CoAxBranch { cab_tvs = tvs, cab_lhs = lhs, cab_rhs = rhs } <- coAxiomNthBranch ax ind
, Pair tys1 tys2 <- sequenceA (map go cos)
= ASSERT( cos `equalLength` tvs )
Pair (substTyWith tvs tys1 (mkTyConApp (coAxiomTyCon ax) lhs))
(substTyWith tvs tys2 rhs)
go (UnivCo _ _ ty1 ty2) = Pair ty1 ty2
go (SymCo co) = swap $ go co
go (TransCo co1 co2) = Pair (pFst $ go co1) (pSnd $ go co2)
go (NthCo d co) = tyConAppArgN d <$> go co
go (LRCo lr co) = (pickLR lr . splitAppTy) <$> go co
go (InstCo aco ty) = go_app aco [ty]
go (SubCo co) = go co
go (AxiomRuleCo ax tys cos) =
case coaxrProves ax tys (map go cos) of
Just res -> res
Nothing -> panic "coercionKind: Malformed coercion"
go_app :: Coercion -> [Type] -> Pair Type
go_app (InstCo co ty) tys = go_app co (ty:tys)
go_app co tys = (`applyTys` tys) <$> go co
coercionKinds :: [Coercion] -> Pair [Type]
coercionKinds tys = sequenceA $ map coercionKind tys
coercionKindRole :: Coercion -> (Pair Type, Role)
coercionKindRole = go
where
go (Refl r ty) = (Pair ty ty, r)
go (TyConAppCo r tc cos)
= (mkTyConApp tc <$> (sequenceA $ map coercionKind cos), r)
go (AppCo co1 co2)
= let (tys1, r1) = go co1 in
(mkAppTy <$> tys1 <*> coercionKind co2, r1)
go (ForAllCo tv co)
= let (tys, r) = go co in
(mkForAllTy tv <$> tys, r)
go (CoVarCo cv) = (toPair $ coVarKind cv, coVarRole cv)
go co@(AxiomInstCo ax _ _) = (coercionKind co, coAxiomRole ax)
go (UnivCo _ r ty1 ty2) = (Pair ty1 ty2, r)
go (SymCo co) = first swap $ go co
go (TransCo co1 co2)
= let (tys1, r) = go co1 in
(Pair (pFst tys1) (pSnd $ coercionKind co2), r)
go (NthCo d co)
= let (Pair t1 t2, r) = go co
(tc1, args1) = splitTyConApp t1
(_tc2, args2) = splitTyConApp t2
in
ASSERT( tc1 == _tc2 )
((`getNth` d) <$> Pair args1 args2, nthRole r tc1 d)
go co@(LRCo {}) = (coercionKind co, Nominal)
go (InstCo co ty) = go_app co [ty]
go (SubCo co) = (coercionKind co, Representational)
go co@(AxiomRuleCo ax _ _) = (coercionKind co, coaxrRole ax)
go_app :: Coercion -> [Type] -> (Pair Type, Role)
go_app (InstCo co ty) tys = go_app co (ty:tys)
go_app co tys
= let (pair, r) = go co in
((`applyTys` tys) <$> pair, r)
coercionRole :: Coercion -> Role
coercionRole = snd . coercionKindRole
applyCo :: Type -> Coercion -> Type
applyCo ty co | Just ty' <- coreView ty = applyCo ty' co
applyCo (FunTy _ ty) _ = ty
applyCo _ _ = panic "applyCo"