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