module TyCoSubst
(
TCvSubst(..), TvSubstEnv, CvSubstEnv,
emptyTvSubstEnv, emptyCvSubstEnv, composeTCvSubstEnv, composeTCvSubst,
emptyTCvSubst, mkEmptyTCvSubst, isEmptyTCvSubst,
mkTCvSubst, mkTvSubst, mkCvSubst,
getTvSubstEnv,
getCvSubstEnv, getTCvInScope, getTCvSubstRangeFVs,
isInScope, notElemTCvSubst,
setTvSubstEnv, setCvSubstEnv, zapTCvSubst,
extendTCvInScope, extendTCvInScopeList, extendTCvInScopeSet,
extendTCvSubst, extendTCvSubstWithClone,
extendCvSubst, extendCvSubstWithClone,
extendTvSubst, extendTvSubstBinderAndInScope, extendTvSubstWithClone,
extendTvSubstList, extendTvSubstAndInScope,
extendTCvSubstList,
unionTCvSubst, zipTyEnv, zipCoEnv, mkTyCoInScopeSet,
zipTvSubst, zipCvSubst,
zipTCvSubst,
mkTvSubstPrs,
substTyWith, substTyWithCoVars, substTysWith, substTysWithCoVars,
substCoWith,
substTy, substTyAddInScope,
substTyUnchecked, substTysUnchecked, substThetaUnchecked,
substTyWithUnchecked,
substCoUnchecked, substCoWithUnchecked,
substTyWithInScope,
substTys, substTheta,
lookupTyVar,
substCo, substCos, substCoVar, substCoVars, lookupCoVar,
cloneTyVarBndr, cloneTyVarBndrs,
substVarBndr, substVarBndrs,
substTyVarBndr, substTyVarBndrs,
substCoVarBndr,
substTyVar, substTyVars, substTyCoVars,
substForAllCoBndr,
substVarBndrUsing, substForAllCoBndrUsing,
checkValidSubst, isValidTCvSubst,
) where
#include "HsVersions.h"
import GhcPrelude
import Type ( mkCastTy, mkAppTy, isCoercionTy )
import Coercion ( mkCoVarCo, mkKindCo, mkNthCo, mkTransCo
, mkNomReflCo, mkSubCo, mkSymCo
, mkFunCo, mkForAllCo, mkUnivCo
, mkAxiomInstCo, mkAppCo, mkGReflCo
, mkInstCo, mkLRCo, mkTyConAppCo
, mkCoercionType
, coercionKind, coVarKindsTypesRole )
import TyCoRep
import TyCoFVs
import TyCoPpr
import Var
import VarSet
import VarEnv
import Pair
import Util
import UniqSupply
import Unique
import UniqFM
import UniqSet
import Outputable
import Data.List (mapAccumL)
data TCvSubst
= TCvSubst InScopeSet
TvSubstEnv
CvSubstEnv
type TvSubstEnv = TyVarEnv Type
type CvSubstEnv = CoVarEnv Coercion
emptyTvSubstEnv :: TvSubstEnv
emptyTvSubstEnv = emptyVarEnv
emptyCvSubstEnv :: CvSubstEnv
emptyCvSubstEnv = emptyVarEnv
composeTCvSubstEnv :: InScopeSet
-> (TvSubstEnv, CvSubstEnv)
-> (TvSubstEnv, CvSubstEnv)
-> (TvSubstEnv, CvSubstEnv)
composeTCvSubstEnv in_scope (tenv1, cenv1) (tenv2, cenv2)
= ( tenv1 `plusVarEnv` mapVarEnv (substTy subst1) tenv2
, cenv1 `plusVarEnv` mapVarEnv (substCo subst1) cenv2 )
where
subst1 = TCvSubst in_scope tenv1 cenv1
composeTCvSubst :: TCvSubst -> TCvSubst -> TCvSubst
composeTCvSubst (TCvSubst is1 tenv1 cenv1) (TCvSubst is2 tenv2 cenv2)
= TCvSubst is3 tenv3 cenv3
where
is3 = is1 `unionInScope` is2
(tenv3, cenv3) = composeTCvSubstEnv is3 (tenv1, cenv1) (tenv2, cenv2)
emptyTCvSubst :: TCvSubst
emptyTCvSubst = TCvSubst emptyInScopeSet emptyTvSubstEnv emptyCvSubstEnv
mkEmptyTCvSubst :: InScopeSet -> TCvSubst
mkEmptyTCvSubst is = TCvSubst is emptyTvSubstEnv emptyCvSubstEnv
isEmptyTCvSubst :: TCvSubst -> Bool
isEmptyTCvSubst (TCvSubst _ tenv cenv) = isEmptyVarEnv tenv && isEmptyVarEnv cenv
mkTCvSubst :: InScopeSet -> (TvSubstEnv, CvSubstEnv) -> TCvSubst
mkTCvSubst in_scope (tenv, cenv) = TCvSubst in_scope tenv cenv
mkTvSubst :: InScopeSet -> TvSubstEnv -> TCvSubst
mkTvSubst in_scope tenv = TCvSubst in_scope tenv emptyCvSubstEnv
mkCvSubst :: InScopeSet -> CvSubstEnv -> TCvSubst
mkCvSubst in_scope cenv = TCvSubst in_scope emptyTvSubstEnv cenv
getTvSubstEnv :: TCvSubst -> TvSubstEnv
getTvSubstEnv (TCvSubst _ env _) = env
getCvSubstEnv :: TCvSubst -> CvSubstEnv
getCvSubstEnv (TCvSubst _ _ env) = env
getTCvInScope :: TCvSubst -> InScopeSet
getTCvInScope (TCvSubst in_scope _ _) = in_scope
getTCvSubstRangeFVs :: TCvSubst -> VarSet
getTCvSubstRangeFVs (TCvSubst _ tenv cenv)
= unionVarSet tenvFVs cenvFVs
where
tenvFVs = tyCoVarsOfTypesSet tenv
cenvFVs = tyCoVarsOfCosSet cenv
isInScope :: Var -> TCvSubst -> Bool
isInScope v (TCvSubst in_scope _ _) = v `elemInScopeSet` in_scope
notElemTCvSubst :: Var -> TCvSubst -> Bool
notElemTCvSubst v (TCvSubst _ tenv cenv)
| isTyVar v
= not (v `elemVarEnv` tenv)
| otherwise
= not (v `elemVarEnv` cenv)
setTvSubstEnv :: TCvSubst -> TvSubstEnv -> TCvSubst
setTvSubstEnv (TCvSubst in_scope _ cenv) tenv = TCvSubst in_scope tenv cenv
setCvSubstEnv :: TCvSubst -> CvSubstEnv -> TCvSubst
setCvSubstEnv (TCvSubst in_scope tenv _) cenv = TCvSubst in_scope tenv cenv
zapTCvSubst :: TCvSubst -> TCvSubst
zapTCvSubst (TCvSubst in_scope _ _) = TCvSubst in_scope emptyVarEnv emptyVarEnv
extendTCvInScope :: TCvSubst -> Var -> TCvSubst
extendTCvInScope (TCvSubst in_scope tenv cenv) var
= TCvSubst (extendInScopeSet in_scope var) tenv cenv
extendTCvInScopeList :: TCvSubst -> [Var] -> TCvSubst
extendTCvInScopeList (TCvSubst in_scope tenv cenv) vars
= TCvSubst (extendInScopeSetList in_scope vars) tenv cenv
extendTCvInScopeSet :: TCvSubst -> VarSet -> TCvSubst
extendTCvInScopeSet (TCvSubst in_scope tenv cenv) vars
= TCvSubst (extendInScopeSetSet in_scope vars) tenv cenv
extendTCvSubst :: TCvSubst -> TyCoVar -> Type -> TCvSubst
extendTCvSubst subst v ty
| isTyVar v
= extendTvSubst subst v ty
| CoercionTy co <- ty
= extendCvSubst subst v co
| otherwise
= pprPanic "extendTCvSubst" (ppr v <+> text "|->" <+> ppr ty)
extendTCvSubstWithClone :: TCvSubst -> TyCoVar -> TyCoVar -> TCvSubst
extendTCvSubstWithClone subst tcv
| isTyVar tcv = extendTvSubstWithClone subst tcv
| otherwise = extendCvSubstWithClone subst tcv
extendTvSubst :: TCvSubst -> TyVar -> Type -> TCvSubst
extendTvSubst (TCvSubst in_scope tenv cenv) tv ty
= TCvSubst in_scope (extendVarEnv tenv tv ty) cenv
extendTvSubstBinderAndInScope :: TCvSubst -> TyCoBinder -> Type -> TCvSubst
extendTvSubstBinderAndInScope subst (Named (Bndr v _)) ty
= ASSERT( isTyVar v )
extendTvSubstAndInScope subst v ty
extendTvSubstBinderAndInScope subst (Anon {}) _
= subst
extendTvSubstWithClone :: TCvSubst -> TyVar -> TyVar -> TCvSubst
extendTvSubstWithClone (TCvSubst in_scope tenv cenv) tv tv'
= TCvSubst (extendInScopeSetSet in_scope new_in_scope)
(extendVarEnv tenv tv (mkTyVarTy tv'))
cenv
where
new_in_scope = tyCoVarsOfType (tyVarKind tv') `extendVarSet` tv'
extendCvSubst :: TCvSubst -> CoVar -> Coercion -> TCvSubst
extendCvSubst (TCvSubst in_scope tenv cenv) v co
= TCvSubst in_scope tenv (extendVarEnv cenv v co)
extendCvSubstWithClone :: TCvSubst -> CoVar -> CoVar -> TCvSubst
extendCvSubstWithClone (TCvSubst in_scope tenv cenv) cv cv'
= TCvSubst (extendInScopeSetSet in_scope new_in_scope)
tenv
(extendVarEnv cenv cv (mkCoVarCo cv'))
where
new_in_scope = tyCoVarsOfType (varType cv') `extendVarSet` cv'
extendTvSubstAndInScope :: TCvSubst -> TyVar -> Type -> TCvSubst
extendTvSubstAndInScope (TCvSubst in_scope tenv cenv) tv ty
= TCvSubst (in_scope `extendInScopeSetSet` tyCoVarsOfType ty)
(extendVarEnv tenv tv ty)
cenv
extendTvSubstList :: TCvSubst -> [Var] -> [Type] -> TCvSubst
extendTvSubstList subst tvs tys
= foldl2 extendTvSubst subst tvs tys
extendTCvSubstList :: TCvSubst -> [Var] -> [Type] -> TCvSubst
extendTCvSubstList subst tvs tys
= foldl2 extendTCvSubst subst tvs tys
unionTCvSubst :: TCvSubst -> TCvSubst -> TCvSubst
unionTCvSubst (TCvSubst in_scope1 tenv1 cenv1) (TCvSubst in_scope2 tenv2 cenv2)
= ASSERT( not (tenv1 `intersectsVarEnv` tenv2)
&& not (cenv1 `intersectsVarEnv` cenv2) )
TCvSubst (in_scope1 `unionInScope` in_scope2)
(tenv1 `plusVarEnv` tenv2)
(cenv1 `plusVarEnv` cenv2)
zipTvSubst :: HasDebugCallStack => [TyVar] -> [Type] -> TCvSubst
zipTvSubst tvs tys
= mkTvSubst (mkInScopeSet (tyCoVarsOfTypes tys)) tenv
where
tenv = zipTyEnv tvs tys
zipCvSubst :: HasDebugCallStack => [CoVar] -> [Coercion] -> TCvSubst
zipCvSubst cvs cos
= TCvSubst (mkInScopeSet (tyCoVarsOfCos cos)) emptyTvSubstEnv cenv
where
cenv = zipCoEnv cvs cos
zipTCvSubst :: HasDebugCallStack => [TyCoVar] -> [Type] -> TCvSubst
zipTCvSubst tcvs tys
= zip_tcvsubst tcvs tys (mkEmptyTCvSubst $ mkInScopeSet (tyCoVarsOfTypes tys))
where zip_tcvsubst :: [TyCoVar] -> [Type] -> TCvSubst -> TCvSubst
zip_tcvsubst (tv:tvs) (ty:tys) subst
= zip_tcvsubst tvs tys (extendTCvSubst subst tv ty)
zip_tcvsubst [] [] subst = subst
zip_tcvsubst _ _ _ = pprPanic "zipTCvSubst: length mismatch"
(ppr tcvs <+> ppr tys)
mkTvSubstPrs :: [(TyVar, Type)] -> TCvSubst
mkTvSubstPrs prs =
ASSERT2( onlyTyVarsAndNoCoercionTy, text "prs" <+> ppr prs )
mkTvSubst in_scope tenv
where tenv = mkVarEnv prs
in_scope = mkInScopeSet $ tyCoVarsOfTypes $ map snd prs
onlyTyVarsAndNoCoercionTy =
and [ isTyVar tv && not (isCoercionTy ty)
| (tv, ty) <- prs ]
zipTyEnv :: HasDebugCallStack => [TyVar] -> [Type] -> TvSubstEnv
zipTyEnv tyvars tys
| debugIsOn
, not (all isTyVar tyvars)
= pprPanic "zipTyEnv" (ppr tyvars <+> ppr tys)
| otherwise
= ASSERT( all (not . isCoercionTy) tys )
mkVarEnv (zipEqual "zipTyEnv" tyvars tys)
zipCoEnv :: HasDebugCallStack => [CoVar] -> [Coercion] -> CvSubstEnv
zipCoEnv cvs cos
| debugIsOn
, not (all isCoVar cvs)
= pprPanic "zipCoEnv" (ppr cvs <+> ppr cos)
| otherwise
= mkVarEnv (zipEqual "zipCoEnv" cvs cos)
instance Outputable TCvSubst where
ppr (TCvSubst ins tenv cenv)
= brackets $ sep[ text "TCvSubst",
nest 2 (text "In scope:" <+> ppr ins),
nest 2 (text "Type env:" <+> ppr tenv),
nest 2 (text "Co env:" <+> ppr cenv) ]
substTyWith :: HasCallStack => [TyVar] -> [Type] -> Type -> Type
substTyWith tvs tys =
ASSERT( tvs `equalLength` tys )
substTy (zipTvSubst tvs tys)
substTyWithUnchecked :: [TyVar] -> [Type] -> Type -> Type
substTyWithUnchecked tvs tys
= ASSERT( tvs `equalLength` tys )
substTyUnchecked (zipTvSubst tvs tys)
substTyWithInScope :: InScopeSet -> [TyVar] -> [Type] -> Type -> Type
substTyWithInScope in_scope tvs tys ty =
ASSERT( tvs `equalLength` tys )
substTy (mkTvSubst in_scope tenv) ty
where tenv = zipTyEnv tvs tys
substCoWith :: HasCallStack => [TyVar] -> [Type] -> Coercion -> Coercion
substCoWith tvs tys = ASSERT( tvs `equalLength` tys )
substCo (zipTvSubst tvs tys)
substCoWithUnchecked :: [TyVar] -> [Type] -> Coercion -> Coercion
substCoWithUnchecked tvs tys
= ASSERT( tvs `equalLength` tys )
substCoUnchecked (zipTvSubst tvs tys)
substTyWithCoVars :: [CoVar] -> [Coercion] -> Type -> Type
substTyWithCoVars cvs cos = substTy (zipCvSubst cvs cos)
substTysWith :: [TyVar] -> [Type] -> [Type] -> [Type]
substTysWith tvs tys = ASSERT( tvs `equalLength` tys )
substTys (zipTvSubst tvs tys)
substTysWithCoVars :: [CoVar] -> [Coercion] -> [Type] -> [Type]
substTysWithCoVars cvs cos = ASSERT( cvs `equalLength` cos )
substTys (zipCvSubst cvs cos)
substTyAddInScope :: TCvSubst -> Type -> Type
substTyAddInScope subst ty =
substTy (extendTCvInScopeSet subst $ tyCoVarsOfType ty) ty
isValidTCvSubst :: TCvSubst -> Bool
isValidTCvSubst (TCvSubst in_scope tenv cenv) =
(tenvFVs `varSetInScope` in_scope) &&
(cenvFVs `varSetInScope` in_scope)
where
tenvFVs = tyCoVarsOfTypesSet tenv
cenvFVs = tyCoVarsOfCosSet cenv
checkValidSubst :: HasCallStack => TCvSubst -> [Type] -> [Coercion] -> a -> a
checkValidSubst subst@(TCvSubst in_scope tenv cenv) tys cos a
= ASSERT2( isValidTCvSubst subst,
text "in_scope" <+> ppr in_scope $$
text "tenv" <+> ppr tenv $$
text "tenvFVs" <+> ppr (tyCoVarsOfTypesSet tenv) $$
text "cenv" <+> ppr cenv $$
text "cenvFVs" <+> ppr (tyCoVarsOfCosSet cenv) $$
text "tys" <+> ppr tys $$
text "cos" <+> ppr cos )
ASSERT2( tysCosFVsInScope,
text "in_scope" <+> ppr in_scope $$
text "tenv" <+> ppr tenv $$
text "cenv" <+> ppr cenv $$
text "tys" <+> ppr tys $$
text "cos" <+> ppr cos $$
text "needInScope" <+> ppr needInScope )
a
where
substDomain = nonDetKeysUFM tenv ++ nonDetKeysUFM cenv
needInScope = (tyCoVarsOfTypes tys `unionVarSet` tyCoVarsOfCos cos)
`delListFromUniqSet_Directly` substDomain
tysCosFVsInScope = needInScope `varSetInScope` in_scope
substTy :: HasCallStack => TCvSubst -> Type -> Type
substTy subst ty
| isEmptyTCvSubst subst = ty
| otherwise = checkValidSubst subst [ty] [] $
subst_ty subst ty
substTyUnchecked :: TCvSubst -> Type -> Type
substTyUnchecked subst ty
| isEmptyTCvSubst subst = ty
| otherwise = subst_ty subst ty
substTys :: HasCallStack => TCvSubst -> [Type] -> [Type]
substTys subst tys
| isEmptyTCvSubst subst = tys
| otherwise = checkValidSubst subst tys [] $ map (subst_ty subst) tys
substTysUnchecked :: TCvSubst -> [Type] -> [Type]
substTysUnchecked subst tys
| isEmptyTCvSubst subst = tys
| otherwise = map (subst_ty subst) tys
substTheta :: HasCallStack => TCvSubst -> ThetaType -> ThetaType
substTheta = substTys
substThetaUnchecked :: TCvSubst -> ThetaType -> ThetaType
substThetaUnchecked = substTysUnchecked
subst_ty :: TCvSubst -> Type -> Type
subst_ty subst ty
= go ty
where
go (TyVarTy tv) = substTyVar subst tv
go (AppTy fun arg) = mkAppTy (go fun) $! (go arg)
go (TyConApp tc tys) = let args = map go tys
in args `seqList` TyConApp tc args
go ty@(FunTy { ft_arg = arg, ft_res = res })
= let !arg' = go arg
!res' = go res
in ty { ft_arg = arg', ft_res = res' }
go (ForAllTy (Bndr tv vis) ty)
= case substVarBndrUnchecked subst tv of
(subst', tv') ->
(ForAllTy $! ((Bndr $! tv') vis)) $!
(subst_ty subst' ty)
go (LitTy n) = LitTy $! n
go (CastTy ty co) = (mkCastTy $! (go ty)) $! (subst_co subst co)
go (CoercionTy co) = CoercionTy $! (subst_co subst co)
substTyVar :: TCvSubst -> TyVar -> Type
substTyVar (TCvSubst _ tenv _) tv
= ASSERT( isTyVar tv )
case lookupVarEnv tenv tv of
Just ty -> ty
Nothing -> TyVarTy tv
substTyVars :: TCvSubst -> [TyVar] -> [Type]
substTyVars subst = map $ substTyVar subst
substTyCoVars :: TCvSubst -> [TyCoVar] -> [Type]
substTyCoVars subst = map $ substTyCoVar subst
substTyCoVar :: TCvSubst -> TyCoVar -> Type
substTyCoVar subst tv
| isTyVar tv = substTyVar subst tv
| otherwise = CoercionTy $ substCoVar subst tv
lookupTyVar :: TCvSubst -> TyVar -> Maybe Type
lookupTyVar (TCvSubst _ tenv _) tv
= ASSERT( isTyVar tv )
lookupVarEnv tenv tv
substCo :: HasCallStack => TCvSubst -> Coercion -> Coercion
substCo subst co
| isEmptyTCvSubst subst = co
| otherwise = checkValidSubst subst [] [co] $ subst_co subst co
substCoUnchecked :: TCvSubst -> Coercion -> Coercion
substCoUnchecked subst co
| isEmptyTCvSubst subst = co
| otherwise = subst_co subst co
substCos :: HasCallStack => TCvSubst -> [Coercion] -> [Coercion]
substCos subst cos
| isEmptyTCvSubst subst = cos
| otherwise = checkValidSubst subst [] cos $ map (subst_co subst) cos
subst_co :: TCvSubst -> Coercion -> Coercion
subst_co subst co
= go co
where
go_ty :: Type -> Type
go_ty = subst_ty subst
go_mco :: MCoercion -> MCoercion
go_mco MRefl = MRefl
go_mco (MCo co) = MCo (go co)
go :: Coercion -> Coercion
go (Refl ty) = mkNomReflCo $! (go_ty ty)
go (GRefl r ty mco) = (mkGReflCo r $! (go_ty ty)) $! (go_mco mco)
go (TyConAppCo r tc args)= let args' = map go args
in args' `seqList` mkTyConAppCo r tc args'
go (AppCo co arg) = (mkAppCo $! go co) $! go arg
go (ForAllCo tv kind_co co)
= case substForAllCoBndrUnchecked subst tv kind_co of
(subst', tv', kind_co') ->
((mkForAllCo $! tv') $! kind_co') $! subst_co subst' co
go (FunCo r co1 co2) = (mkFunCo r $! go co1) $! go co2
go (CoVarCo cv) = substCoVar subst cv
go (AxiomInstCo con ind cos) = mkAxiomInstCo con ind $! map go cos
go (UnivCo p r t1 t2) = (((mkUnivCo $! go_prov p) $! r) $!
(go_ty t1)) $! (go_ty t2)
go (SymCo co) = mkSymCo $! (go co)
go (TransCo co1 co2) = (mkTransCo $! (go co1)) $! (go co2)
go (NthCo r d co) = mkNthCo r d $! (go co)
go (LRCo lr co) = mkLRCo lr $! (go co)
go (InstCo co arg) = (mkInstCo $! (go co)) $! go arg
go (KindCo co) = mkKindCo $! (go co)
go (SubCo co) = mkSubCo $! (go co)
go (AxiomRuleCo c cs) = let cs1 = map go cs
in cs1 `seqList` AxiomRuleCo c cs1
go (HoleCo h) = HoleCo $! go_hole h
go_prov UnsafeCoerceProv = UnsafeCoerceProv
go_prov (PhantomProv kco) = PhantomProv (go kco)
go_prov (ProofIrrelProv kco) = ProofIrrelProv (go kco)
go_prov p@(PluginProv _) = p
go_hole h@(CoercionHole { ch_co_var = cv })
= h { ch_co_var = updateVarType go_ty cv }
substForAllCoBndr :: TCvSubst -> TyCoVar -> KindCoercion
-> (TCvSubst, TyCoVar, Coercion)
substForAllCoBndr subst
= substForAllCoBndrUsing False (substCo subst) subst
substForAllCoBndrUnchecked :: TCvSubst -> TyCoVar -> KindCoercion
-> (TCvSubst, TyCoVar, Coercion)
substForAllCoBndrUnchecked subst
= substForAllCoBndrUsing False (substCoUnchecked subst) subst
substForAllCoBndrUsing :: Bool
-> (Coercion -> Coercion)
-> TCvSubst -> TyCoVar -> KindCoercion
-> (TCvSubst, TyCoVar, KindCoercion)
substForAllCoBndrUsing sym sco subst old_var
| isTyVar old_var = substForAllCoTyVarBndrUsing sym sco subst old_var
| otherwise = substForAllCoCoVarBndrUsing sym sco subst old_var
substForAllCoTyVarBndrUsing :: Bool
-> (Coercion -> Coercion)
-> TCvSubst -> TyVar -> KindCoercion
-> (TCvSubst, TyVar, KindCoercion)
substForAllCoTyVarBndrUsing sym sco (TCvSubst in_scope tenv cenv) old_var old_kind_co
= ASSERT( isTyVar old_var )
( TCvSubst (in_scope `extendInScopeSet` new_var) new_env cenv
, new_var, new_kind_co )
where
new_env | no_change && not sym = delVarEnv tenv old_var
| sym = extendVarEnv tenv old_var $
TyVarTy new_var `CastTy` new_kind_co
| otherwise = extendVarEnv tenv old_var (TyVarTy new_var)
no_kind_change = noFreeVarsOfCo old_kind_co
no_change = no_kind_change && (new_var == old_var)
new_kind_co | no_kind_change = old_kind_co
| otherwise = sco old_kind_co
Pair new_ki1 _ = coercionKind new_kind_co
new_var = uniqAway in_scope (setTyVarKind old_var new_ki1)
substForAllCoCoVarBndrUsing :: Bool
-> (Coercion -> Coercion)
-> TCvSubst -> CoVar -> KindCoercion
-> (TCvSubst, CoVar, KindCoercion)
substForAllCoCoVarBndrUsing sym sco (TCvSubst in_scope tenv cenv)
old_var old_kind_co
= ASSERT( isCoVar old_var )
( TCvSubst (in_scope `extendInScopeSet` new_var) tenv new_cenv
, new_var, new_kind_co )
where
new_cenv | no_change && not sym = delVarEnv cenv old_var
| otherwise = extendVarEnv cenv old_var (mkCoVarCo new_var)
no_kind_change = noFreeVarsOfCo old_kind_co
no_change = no_kind_change && (new_var == old_var)
new_kind_co | no_kind_change = old_kind_co
| otherwise = sco old_kind_co
Pair h1 h2 = coercionKind new_kind_co
new_var = uniqAway in_scope $ mkCoVar (varName old_var) new_var_type
new_var_type | sym = h2
| otherwise = h1
substCoVar :: TCvSubst -> CoVar -> Coercion
substCoVar (TCvSubst _ _ cenv) cv
= case lookupVarEnv cenv cv of
Just co -> co
Nothing -> CoVarCo cv
substCoVars :: TCvSubst -> [CoVar] -> [Coercion]
substCoVars subst cvs = map (substCoVar subst) cvs
lookupCoVar :: TCvSubst -> Var -> Maybe Coercion
lookupCoVar (TCvSubst _ _ cenv) v = lookupVarEnv cenv v
substTyVarBndr :: HasCallStack => TCvSubst -> TyVar -> (TCvSubst, TyVar)
substTyVarBndr = substTyVarBndrUsing substTy
substTyVarBndrs :: HasCallStack => TCvSubst -> [TyVar] -> (TCvSubst, [TyVar])
substTyVarBndrs = mapAccumL substTyVarBndr
substVarBndr :: HasCallStack => TCvSubst -> TyCoVar -> (TCvSubst, TyCoVar)
substVarBndr = substVarBndrUsing substTy
substVarBndrs :: HasCallStack => TCvSubst -> [TyCoVar] -> (TCvSubst, [TyCoVar])
substVarBndrs = mapAccumL substVarBndr
substCoVarBndr :: HasCallStack => TCvSubst -> CoVar -> (TCvSubst, CoVar)
substCoVarBndr = substCoVarBndrUsing substTy
substVarBndrUnchecked :: TCvSubst -> TyCoVar -> (TCvSubst, TyCoVar)
substVarBndrUnchecked = substVarBndrUsing substTyUnchecked
substVarBndrUsing :: (TCvSubst -> Type -> Type)
-> TCvSubst -> TyCoVar -> (TCvSubst, TyCoVar)
substVarBndrUsing subst_fn subst v
| isTyVar v = substTyVarBndrUsing subst_fn subst v
| otherwise = substCoVarBndrUsing subst_fn subst v
substTyVarBndrUsing
:: (TCvSubst -> Type -> Type)
-> TCvSubst -> TyVar -> (TCvSubst, TyVar)
substTyVarBndrUsing subst_fn subst@(TCvSubst in_scope tenv cenv) old_var
= ASSERT2( _no_capture, pprTyVar old_var $$ pprTyVar new_var $$ ppr subst )
ASSERT( isTyVar old_var )
(TCvSubst (in_scope `extendInScopeSet` new_var) new_env cenv, new_var)
where
new_env | no_change = delVarEnv tenv old_var
| otherwise = extendVarEnv tenv old_var (TyVarTy new_var)
_no_capture = not (new_var `elemVarSet` tyCoVarsOfTypesSet tenv)
old_ki = tyVarKind old_var
no_kind_change = noFreeVarsOfType old_ki
no_change = no_kind_change && (new_var == old_var)
new_var | no_kind_change = uniqAway in_scope old_var
| otherwise = uniqAway in_scope $
setTyVarKind old_var (subst_fn subst old_ki)
substCoVarBndrUsing
:: (TCvSubst -> Type -> Type)
-> TCvSubst -> CoVar -> (TCvSubst, CoVar)
substCoVarBndrUsing subst_fn subst@(TCvSubst in_scope tenv cenv) old_var
= ASSERT( isCoVar old_var )
(TCvSubst (in_scope `extendInScopeSet` new_var) tenv new_cenv, new_var)
where
new_co = mkCoVarCo new_var
no_kind_change = noFreeVarsOfTypes [t1, t2]
no_change = new_var == old_var && no_kind_change
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) new_var_type
(_, _, t1, t2, role) = coVarKindsTypesRole old_var
t1' = subst_fn subst t1
t2' = subst_fn subst t2
new_var_type = mkCoercionType role t1' t2'
cloneTyVarBndr :: TCvSubst -> TyVar -> Unique -> (TCvSubst, TyVar)
cloneTyVarBndr subst@(TCvSubst in_scope tv_env cv_env) tv uniq
= ASSERT2( isTyVar tv, ppr tv )
(TCvSubst (extendInScopeSet in_scope tv')
(extendVarEnv tv_env tv (mkTyVarTy tv')) cv_env, tv')
where
old_ki = tyVarKind tv
no_kind_change = noFreeVarsOfType old_ki
tv1 | no_kind_change = tv
| otherwise = setTyVarKind tv (substTy subst old_ki)
tv' = setVarUnique tv1 uniq
cloneTyVarBndrs :: TCvSubst -> [TyVar] -> UniqSupply -> (TCvSubst, [TyVar])
cloneTyVarBndrs subst [] _usupply = (subst, [])
cloneTyVarBndrs subst (t:ts) usupply = (subst'', tv:tvs)
where
(uniq, usupply') = takeUniqFromSupply usupply
(subst' , tv ) = cloneTyVarBndr subst t uniq
(subst'', tvs) = cloneTyVarBndrs subst' ts usupply'