module GHC.Core.TyCo.Subst
(
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,
zipTvSubst, zipCvSubst,
zipTCvSubst,
mkTvSubstPrs,
substTyWith, substTyWithCoVars, substTysWith, substTysWithCoVars,
substCoWith,
substTy, substTyAddInScope, substScaledTy,
substTyUnchecked, substTysUnchecked, substScaledTysUnchecked, substThetaUnchecked,
substTyWithUnchecked, substScaledTyUnchecked,
substCoUnchecked, substCoWithUnchecked,
substTyWithInScope,
substTys, substScaledTys, 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 GHC.Prelude
import GHC.Core.Type
( mkCastTy, mkAppTy, isCoercionTy )
import GHC.Core.Coercion
( mkCoVarCo, mkKindCo, mkNthCo, mkTransCo
, mkNomReflCo, mkSubCo, mkSymCo
, mkFunCo, mkForAllCo, mkUnivCo
, mkAxiomInstCo, mkAppCo, mkGReflCo
, mkInstCo, mkLRCo, mkTyConAppCo
, mkCoercionType
, coercionKind, coercionLKind, coVarKindsTypesRole )
import GHC.Core.TyCo.Ppr ( pprTyVar )
import GHC.Core.TyCo.Rep
import GHC.Core.TyCo.FVs
import GHC.Types.Var
import GHC.Types.Var.Set
import GHC.Types.Var.Env
import GHC.Data.Pair
import GHC.Utils.Misc
import GHC.Types.Unique.Supply
import GHC.Types.Unique
import GHC.Types.Unique.FM
import GHC.Types.Unique.Set
import GHC.Utils.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 = shallowTyCoVarsOfTyVarEnv tenv
cenvFVs = shallowTyCoVarsOfCoVarEnv 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( tenv1 `disjointVarEnv` tenv2
&& cenv1 `disjointVarEnv` cenv2 )
TCvSubst (in_scope1 `unionInScope` in_scope2)
(tenv1 `plusVarEnv` tenv2)
(cenv1 `plusVarEnv` cenv2)
zipTvSubst :: HasDebugCallStack => [TyVar] -> [Type] -> TCvSubst
zipTvSubst tvs tys
= mkTvSubst (mkInScopeSet (shallowTyCoVarsOfTypes tys)) tenv
where
tenv = zipTyEnv tvs tys
zipCvSubst :: HasDebugCallStack => [CoVar] -> [Coercion] -> TCvSubst
zipCvSubst cvs cos
= TCvSubst (mkInScopeSet (shallowTyCoVarsOfCos cos)) emptyTvSubstEnv cenv
where
cenv = zipCoEnv cvs cos
zipTCvSubst :: HasDebugCallStack => [TyCoVar] -> [Type] -> TCvSubst
zipTCvSubst tcvs tys
= zip_tcvsubst tcvs tys $
mkEmptyTCvSubst $ mkInScopeSet $ shallowTyCoVarsOfTypes 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 $ shallowTyCoVarsOfTypes $ 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 && (tyvars `equalLength` tys))
= 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 = shallowTyCoVarsOfTyVarEnv tenv
cenvFVs = shallowTyCoVarsOfCoVarEnv 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 (shallowTyCoVarsOfTyVarEnv tenv) $$
text "cenv" <+> ppr cenv $$
text "cenvFVs" <+> ppr (shallowTyCoVarsOfCoVarEnv 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 = (shallowTyCoVarsOfTypes tys `unionVarSet`
shallowTyCoVarsOfCos 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
substScaledTy :: HasCallStack => TCvSubst -> Scaled Type -> Scaled Type
substScaledTy subst scaled_ty = mapScaledType (substTy subst) scaled_ty
substScaledTyUnchecked :: HasCallStack => TCvSubst -> Scaled Type -> Scaled Type
substScaledTyUnchecked subst scaled_ty = mapScaledType (substTyUnchecked subst) scaled_ty
substTys :: HasCallStack => TCvSubst -> [Type] -> [Type]
substTys subst tys
| isEmptyTCvSubst subst = tys
| otherwise = checkValidSubst subst tys [] $ map (subst_ty subst) tys
substScaledTys :: HasCallStack => TCvSubst -> [Scaled Type] -> [Scaled Type]
substScaledTys subst scaled_tys
| isEmptyTCvSubst subst = scaled_tys
| otherwise = checkValidSubst subst (map scaledMult scaled_tys ++ map scaledThing scaled_tys) [] $
map (mapScaledType (subst_ty subst)) scaled_tys
substTysUnchecked :: TCvSubst -> [Type] -> [Type]
substTysUnchecked subst tys
| isEmptyTCvSubst subst = tys
| otherwise = map (subst_ty subst) tys
substScaledTysUnchecked :: TCvSubst -> [Scaled Type] -> [Scaled Type]
substScaledTysUnchecked subst tys
| isEmptyTCvSubst subst = tys
| otherwise = map (mapScaledType (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 ty@(TyConApp tc []) = tc `seq` ty
go (TyConApp tc tys) = (mkTyConApp $! tc) $! strictMap go tys
go ty@(FunTy { ft_mult = mult, ft_arg = arg, ft_res = res })
= let !mult' = go mult
!arg' = go arg
!res' = go res
in ty { ft_mult = mult', 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 w co1 co2) = ((mkFunCo r $! go w) $! 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 (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
new_ki1 = coercionLKind 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` shallowTyCoVarsOfTyVarEnv 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'