module GHC.Core.TyCo.Subst
(
Subst(..), TvSubstEnv, CvSubstEnv, IdSubstEnv,
emptyIdSubstEnv, emptyTvSubstEnv, emptyCvSubstEnv, composeTCvSubst,
emptySubst, mkEmptySubst, isEmptyTCvSubst, isEmptySubst,
mkTCvSubst, mkTvSubst, mkCvSubst, mkIdSubst,
getTvSubstEnv, getIdSubstEnv,
getCvSubstEnv, getSubstInScope, setInScope, getSubstRangeTyCoFVs,
isInScope, elemSubst, notElemSubst, zapSubst,
extendSubstInScope, extendSubstInScopeList, extendSubstInScopeSet,
extendTCvSubst, extendTCvSubstWithClone,
extendCvSubst, extendCvSubstWithClone,
extendTvSubst, extendTvSubstWithClone,
extendTvSubstList, extendTvSubstAndInScope,
extendTCvSubstList,
unionSubst, 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, substDCoVarSet,
substTyVar, substTyVars, substTyVarToTyVar,
substTyCoVars,
substTyCoBndr, substForAllCoBndr,
substVarBndrUsing, substForAllCoBndrUsing,
checkValidSubst, isValidTCvSubst,
) where
import GHC.Prelude
import {-# SOURCE #-} GHC.Core.Type
( mkCastTy, mkAppTy, isCoercionTy, mkTyConApp, getTyVar_maybe )
import {-# SOURCE #-} GHC.Core.Coercion
( mkCoVarCo, mkKindCo, mkSelCo, mkTransCo
, mkNomReflCo, mkSubCo, mkSymCo
, mkFunCo2, mkForAllCo, mkUnivCo
, mkAxiomCo, mkAppCo, mkGReflCo
, mkInstCo, mkLRCo, mkTyConAppCo
, mkCoercionType
, coercionKind, coercionLKind, coVarTypesRole )
import {-# SOURCE #-} GHC.Core.TyCo.Ppr ( pprTyVar )
import {-# SOURCE #-} GHC.Core.Ppr ( )
import {-# SOURCE #-} GHC.Core ( CoreExpr )
import GHC.Core.TyCo.Rep
import GHC.Core.TyCo.FVs
import GHC.Types.Basic( SwapFlag(..), isSwapped, pickSwap, notSwapped )
import GHC.Types.Var
import GHC.Types.Var.Set
import GHC.Types.Var.Env
import GHC.Data.Pair
import GHC.Utils.Constants (debugIsOn)
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 GHC.Utils.Panic
import Data.List (mapAccumL)
data Subst
= Subst InScopeSet
IdSubstEnv
TvSubstEnv
CvSubstEnv
type IdSubstEnv = IdEnv CoreExpr
type TvSubstEnv = TyVarEnv Type
type CvSubstEnv = CoVarEnv Coercion
emptyIdSubstEnv :: IdSubstEnv
emptyIdSubstEnv :: IdSubstEnv
emptyIdSubstEnv = IdSubstEnv
forall a. VarEnv a
emptyVarEnv
emptyTvSubstEnv :: TvSubstEnv
emptyTvSubstEnv :: TvSubstEnv
emptyTvSubstEnv = TvSubstEnv
forall a. VarEnv a
emptyVarEnv
emptyCvSubstEnv :: CvSubstEnv
emptyCvSubstEnv :: CvSubstEnv
emptyCvSubstEnv = CvSubstEnv
forall a. VarEnv a
emptyVarEnv
composeTCvSubst :: Subst -> Subst -> Subst
composeTCvSubst :: Subst -> Subst -> Subst
composeTCvSubst subst1 :: Subst
subst1@(Subst InScopeSet
is1 IdSubstEnv
ids1 TvSubstEnv
tenv1 CvSubstEnv
cenv1) (Subst InScopeSet
is2 IdSubstEnv
_ TvSubstEnv
tenv2 CvSubstEnv
cenv2)
= InScopeSet -> IdSubstEnv -> TvSubstEnv -> CvSubstEnv -> Subst
Subst InScopeSet
is3 IdSubstEnv
ids1 TvSubstEnv
tenv3 CvSubstEnv
cenv3
where
is3 :: InScopeSet
is3 = InScopeSet
is1 InScopeSet -> InScopeSet -> InScopeSet
`unionInScope` InScopeSet
is2
tenv3 :: TvSubstEnv
tenv3 = 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 (HasDebugCallStack => Subst -> Type -> Type
Subst -> Type -> Type
substTy Subst
extended_subst1) TvSubstEnv
tenv2
cenv3 :: CvSubstEnv
cenv3 = 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 (HasDebugCallStack => Subst -> Coercion -> Coercion
Subst -> Coercion -> Coercion
substCo Subst
extended_subst1) CvSubstEnv
cenv2
extended_subst1 :: Subst
extended_subst1 = Subst
subst1 Subst -> InScopeSet -> Subst
`setInScope` InScopeSet
is3
emptySubst :: Subst
emptySubst :: Subst
emptySubst = InScopeSet -> IdSubstEnv -> TvSubstEnv -> CvSubstEnv -> Subst
Subst InScopeSet
emptyInScopeSet IdSubstEnv
forall a. VarEnv a
emptyVarEnv TvSubstEnv
forall a. VarEnv a
emptyVarEnv CvSubstEnv
forall a. VarEnv a
emptyVarEnv
mkEmptySubst :: InScopeSet -> Subst
mkEmptySubst :: InScopeSet -> Subst
mkEmptySubst InScopeSet
in_scope = InScopeSet -> IdSubstEnv -> TvSubstEnv -> CvSubstEnv -> Subst
Subst InScopeSet
in_scope IdSubstEnv
forall a. VarEnv a
emptyVarEnv TvSubstEnv
forall a. VarEnv a
emptyVarEnv CvSubstEnv
forall a. VarEnv a
emptyVarEnv
isEmptySubst :: Subst -> Bool
isEmptySubst :: Subst -> Bool
isEmptySubst (Subst InScopeSet
_ IdSubstEnv
id_env TvSubstEnv
tv_env CvSubstEnv
cv_env)
= IdSubstEnv -> Bool
forall a. VarEnv a -> Bool
isEmptyVarEnv IdSubstEnv
id_env Bool -> Bool -> Bool
&& TvSubstEnv -> Bool
forall a. VarEnv a -> Bool
isEmptyVarEnv TvSubstEnv
tv_env Bool -> Bool -> Bool
&& CvSubstEnv -> Bool
forall a. VarEnv a -> Bool
isEmptyVarEnv CvSubstEnv
cv_env
isEmptyTCvSubst :: Subst -> Bool
isEmptyTCvSubst :: Subst -> Bool
isEmptyTCvSubst (Subst InScopeSet
_ IdSubstEnv
_ TvSubstEnv
tv_env CvSubstEnv
cv_env)
= TvSubstEnv -> Bool
forall a. VarEnv a -> Bool
isEmptyVarEnv TvSubstEnv
tv_env Bool -> Bool -> Bool
&& CvSubstEnv -> Bool
forall a. VarEnv a -> Bool
isEmptyVarEnv CvSubstEnv
cv_env
mkTCvSubst :: InScopeSet -> TvSubstEnv -> CvSubstEnv -> Subst
mkTCvSubst :: InScopeSet -> TvSubstEnv -> CvSubstEnv -> Subst
mkTCvSubst InScopeSet
in_scope TvSubstEnv
tvs CvSubstEnv
cvs = InScopeSet -> IdSubstEnv -> TvSubstEnv -> CvSubstEnv -> Subst
Subst InScopeSet
in_scope IdSubstEnv
emptyIdSubstEnv TvSubstEnv
tvs CvSubstEnv
cvs
mkIdSubst :: InScopeSet -> IdSubstEnv -> Subst
mkIdSubst :: InScopeSet -> IdSubstEnv -> Subst
mkIdSubst InScopeSet
in_scope IdSubstEnv
ids = InScopeSet -> IdSubstEnv -> TvSubstEnv -> CvSubstEnv -> Subst
Subst InScopeSet
in_scope IdSubstEnv
ids TvSubstEnv
emptyTvSubstEnv CvSubstEnv
emptyCvSubstEnv
mkTvSubst :: InScopeSet -> TvSubstEnv -> Subst
mkTvSubst :: InScopeSet -> TvSubstEnv -> Subst
mkTvSubst InScopeSet
in_scope TvSubstEnv
tenv = InScopeSet -> IdSubstEnv -> TvSubstEnv -> CvSubstEnv -> Subst
Subst InScopeSet
in_scope IdSubstEnv
emptyIdSubstEnv TvSubstEnv
tenv CvSubstEnv
emptyCvSubstEnv
mkCvSubst :: InScopeSet -> CvSubstEnv -> Subst
mkCvSubst :: InScopeSet -> CvSubstEnv -> Subst
mkCvSubst InScopeSet
in_scope CvSubstEnv
cenv = InScopeSet -> IdSubstEnv -> TvSubstEnv -> CvSubstEnv -> Subst
Subst InScopeSet
in_scope IdSubstEnv
emptyIdSubstEnv TvSubstEnv
emptyTvSubstEnv CvSubstEnv
cenv
getIdSubstEnv :: Subst -> IdSubstEnv
getIdSubstEnv :: Subst -> IdSubstEnv
getIdSubstEnv (Subst InScopeSet
_ IdSubstEnv
ids TvSubstEnv
_ CvSubstEnv
_) = IdSubstEnv
ids
getTvSubstEnv :: Subst -> TvSubstEnv
getTvSubstEnv :: Subst -> TvSubstEnv
getTvSubstEnv (Subst InScopeSet
_ IdSubstEnv
_ TvSubstEnv
tenv CvSubstEnv
_) = TvSubstEnv
tenv
getCvSubstEnv :: Subst -> CvSubstEnv
getCvSubstEnv :: Subst -> CvSubstEnv
getCvSubstEnv (Subst InScopeSet
_ IdSubstEnv
_ TvSubstEnv
_ CvSubstEnv
cenv) = CvSubstEnv
cenv
getSubstInScope :: Subst -> InScopeSet
getSubstInScope :: Subst -> InScopeSet
getSubstInScope (Subst InScopeSet
in_scope IdSubstEnv
_ TvSubstEnv
_ CvSubstEnv
_) = InScopeSet
in_scope
setInScope :: Subst -> InScopeSet -> Subst
setInScope :: Subst -> InScopeSet -> Subst
setInScope (Subst InScopeSet
_ IdSubstEnv
ids TvSubstEnv
tvs CvSubstEnv
cvs) InScopeSet
in_scope = InScopeSet -> IdSubstEnv -> TvSubstEnv -> CvSubstEnv -> Subst
Subst InScopeSet
in_scope IdSubstEnv
ids TvSubstEnv
tvs CvSubstEnv
cvs
getSubstRangeTyCoFVs :: Subst -> VarSet
getSubstRangeTyCoFVs :: Subst -> VarSet
getSubstRangeTyCoFVs (Subst InScopeSet
_ IdSubstEnv
_ TvSubstEnv
tenv CvSubstEnv
cenv)
= VarSet
tenvFVs VarSet -> VarSet -> VarSet
`unionVarSet` VarSet
cenvFVs
where
tenvFVs :: VarSet
tenvFVs = TvSubstEnv -> VarSet
shallowTyCoVarsOfTyVarEnv TvSubstEnv
tenv
cenvFVs :: VarSet
cenvFVs = CvSubstEnv -> VarSet
shallowTyCoVarsOfCoVarEnv CvSubstEnv
cenv
isInScope :: Var -> Subst -> Bool
isInScope :: Var -> Subst -> Bool
isInScope Var
v (Subst InScopeSet
in_scope IdSubstEnv
_ TvSubstEnv
_ CvSubstEnv
_) = Var
v Var -> InScopeSet -> Bool
`elemInScopeSet` InScopeSet
in_scope
elemSubst :: Var -> Subst -> Bool
elemSubst :: Var -> Subst -> Bool
elemSubst Var
v (Subst InScopeSet
_ IdSubstEnv
ids TvSubstEnv
tenv CvSubstEnv
cenv)
| Var -> Bool
isTyVar Var
v
= Var
v Var -> TvSubstEnv -> Bool
forall a. Var -> VarEnv a -> Bool
`elemVarEnv` TvSubstEnv
tenv
| Var -> Bool
isCoVar Var
v
= Var
v Var -> CvSubstEnv -> Bool
forall a. Var -> VarEnv a -> Bool
`elemVarEnv` CvSubstEnv
cenv
| Bool
otherwise
= Var
v Var -> IdSubstEnv -> Bool
forall a. Var -> VarEnv a -> Bool
`elemVarEnv` IdSubstEnv
ids
notElemSubst :: Var -> Subst -> Bool
notElemSubst :: Var -> Subst -> Bool
notElemSubst Var
v = Bool -> Bool
not (Bool -> Bool) -> (Subst -> Bool) -> Subst -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Subst -> Bool
elemSubst Var
v
zapSubst :: Subst -> Subst
zapSubst :: Subst -> Subst
zapSubst (Subst InScopeSet
in_scope IdSubstEnv
_ TvSubstEnv
_ CvSubstEnv
_) = InScopeSet -> IdSubstEnv -> TvSubstEnv -> CvSubstEnv -> Subst
Subst InScopeSet
in_scope IdSubstEnv
forall a. VarEnv a
emptyVarEnv TvSubstEnv
forall a. VarEnv a
emptyVarEnv CvSubstEnv
forall a. VarEnv a
emptyVarEnv
extendSubstInScope :: Subst -> Var -> Subst
extendSubstInScope :: Subst -> Var -> Subst
extendSubstInScope (Subst InScopeSet
in_scope IdSubstEnv
ids TvSubstEnv
tvs CvSubstEnv
cvs) Var
v
= InScopeSet -> IdSubstEnv -> TvSubstEnv -> CvSubstEnv -> Subst
Subst (InScopeSet
in_scope InScopeSet -> Var -> InScopeSet
`extendInScopeSet` Var
v)
IdSubstEnv
ids TvSubstEnv
tvs CvSubstEnv
cvs
extendSubstInScopeList :: Subst -> [Var] -> Subst
extendSubstInScopeList :: Subst -> [Var] -> Subst
extendSubstInScopeList (Subst InScopeSet
in_scope IdSubstEnv
ids TvSubstEnv
tvs CvSubstEnv
cvs) [Var]
vs
= InScopeSet -> IdSubstEnv -> TvSubstEnv -> CvSubstEnv -> Subst
Subst (InScopeSet
in_scope InScopeSet -> [Var] -> InScopeSet
`extendInScopeSetList` [Var]
vs)
IdSubstEnv
ids TvSubstEnv
tvs CvSubstEnv
cvs
extendSubstInScopeSet :: Subst -> VarSet -> Subst
extendSubstInScopeSet :: Subst -> VarSet -> Subst
extendSubstInScopeSet (Subst InScopeSet
in_scope IdSubstEnv
ids TvSubstEnv
tvs CvSubstEnv
cvs) VarSet
vs
= InScopeSet -> IdSubstEnv -> TvSubstEnv -> CvSubstEnv -> Subst
Subst (InScopeSet
in_scope InScopeSet -> VarSet -> InScopeSet
`extendInScopeSetSet` VarSet
vs)
IdSubstEnv
ids TvSubstEnv
tvs CvSubstEnv
cvs
extendTCvSubst :: Subst -> TyCoVar -> Type -> Subst
extendTCvSubst :: Subst -> Var -> Type -> Subst
extendTCvSubst Subst
subst Var
v Type
ty
| Var -> Bool
isTyVar Var
v
= Subst -> Var -> Type -> Subst
extendTvSubst Subst
subst Var
v Type
ty
| CoercionTy Coercion
co <- Type
ty
= Subst -> Var -> Coercion -> Subst
extendCvSubst Subst
subst Var
v Coercion
co
| Bool
otherwise
= String -> SDoc -> Subst
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"extendTCvSubst" (Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
v SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"|->" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty)
extendTCvSubstWithClone :: Subst -> TyCoVar -> TyCoVar -> Subst
extendTCvSubstWithClone :: Subst -> Var -> Var -> Subst
extendTCvSubstWithClone Subst
subst Var
tcv
| Var -> Bool
isTyVar Var
tcv = Subst -> Var -> Var -> Subst
extendTvSubstWithClone Subst
subst Var
tcv
| Bool
otherwise = Subst -> Var -> Var -> Subst
extendCvSubstWithClone Subst
subst Var
tcv
extendTvSubst :: Subst -> TyVar -> Type -> Subst
extendTvSubst :: Subst -> Var -> Type -> Subst
extendTvSubst (Subst InScopeSet
in_scope IdSubstEnv
ids TvSubstEnv
tvs CvSubstEnv
cvs) Var
tv Type
ty
= Bool -> Subst -> Subst
forall a. HasCallStack => Bool -> a -> a
assert (Var -> Bool
isTyVar Var
tv) (Subst -> Subst) -> Subst -> Subst
forall a b. (a -> b) -> a -> b
$
InScopeSet -> IdSubstEnv -> TvSubstEnv -> CvSubstEnv -> Subst
Subst InScopeSet
in_scope IdSubstEnv
ids (TvSubstEnv -> Var -> Type -> TvSubstEnv
forall a. VarEnv a -> Var -> a -> VarEnv a
extendVarEnv TvSubstEnv
tvs Var
tv Type
ty) CvSubstEnv
cvs
extendTvSubstWithClone :: Subst -> TyVar -> TyVar -> Subst
extendTvSubstWithClone :: Subst -> Var -> Var -> Subst
extendTvSubstWithClone (Subst InScopeSet
in_scope IdSubstEnv
idenv TvSubstEnv
tenv CvSubstEnv
cenv) Var
tv Var
tv'
= InScopeSet -> IdSubstEnv -> TvSubstEnv -> CvSubstEnv -> Subst
Subst (InScopeSet -> Var -> InScopeSet
extendInScopeSet InScopeSet
in_scope Var
tv')
IdSubstEnv
idenv
(TvSubstEnv -> Var -> Type -> TvSubstEnv
forall a. VarEnv a -> Var -> a -> VarEnv a
extendVarEnv TvSubstEnv
tenv Var
tv (Var -> Type
mkTyVarTy Var
tv'))
CvSubstEnv
cenv
extendCvSubst :: Subst -> CoVar -> Coercion -> Subst
extendCvSubst :: Subst -> Var -> Coercion -> Subst
extendCvSubst (Subst InScopeSet
in_scope IdSubstEnv
ids TvSubstEnv
tvs CvSubstEnv
cvs) Var
v Coercion
r
= Bool -> Subst -> Subst
forall a. HasCallStack => Bool -> a -> a
assert (Var -> Bool
isCoVar Var
v) (Subst -> Subst) -> Subst -> Subst
forall a b. (a -> b) -> a -> b
$
InScopeSet -> IdSubstEnv -> TvSubstEnv -> CvSubstEnv -> Subst
Subst InScopeSet
in_scope IdSubstEnv
ids TvSubstEnv
tvs (CvSubstEnv -> Var -> Coercion -> CvSubstEnv
forall a. VarEnv a -> Var -> a -> VarEnv a
extendVarEnv CvSubstEnv
cvs Var
v Coercion
r)
extendCvSubstWithClone :: Subst -> CoVar -> CoVar -> Subst
extendCvSubstWithClone :: Subst -> Var -> Var -> Subst
extendCvSubstWithClone (Subst InScopeSet
in_scope IdSubstEnv
ids TvSubstEnv
tenv CvSubstEnv
cenv) Var
cv Var
cv'
= InScopeSet -> IdSubstEnv -> TvSubstEnv -> CvSubstEnv -> Subst
Subst (InScopeSet -> VarSet -> InScopeSet
extendInScopeSetSet InScopeSet
in_scope VarSet
new_in_scope)
IdSubstEnv
ids
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 :: Subst -> TyVar -> Type -> Subst
extendTvSubstAndInScope :: Subst -> Var -> Type -> Subst
extendTvSubstAndInScope (Subst InScopeSet
in_scope IdSubstEnv
ids TvSubstEnv
tenv CvSubstEnv
cenv) Var
tv Type
ty
= InScopeSet -> IdSubstEnv -> TvSubstEnv -> CvSubstEnv -> Subst
Subst (InScopeSet
in_scope InScopeSet -> VarSet -> InScopeSet
`extendInScopeSetSet` Type -> VarSet
tyCoVarsOfType Type
ty)
IdSubstEnv
ids
(TvSubstEnv -> Var -> Type -> TvSubstEnv
forall a. VarEnv a -> Var -> a -> VarEnv a
extendVarEnv TvSubstEnv
tenv Var
tv Type
ty)
CvSubstEnv
cenv
extendTvSubstList :: Subst -> [(TyVar,Type)] -> Subst
extendTvSubstList :: Subst -> [(Var, Type)] -> Subst
extendTvSubstList Subst
subst [(Var, Type)]
vrs
= (Subst -> (Var, Type) -> Subst) -> Subst -> [(Var, Type)] -> Subst
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Subst -> (Var, Type) -> Subst
extend Subst
subst [(Var, Type)]
vrs
where
extend :: Subst -> (Var, Type) -> Subst
extend Subst
subst (Var
v, Type
r) = Subst -> Var -> Type -> Subst
extendTvSubst Subst
subst Var
v Type
r
extendTCvSubstList :: Subst -> [Var] -> [Type] -> Subst
extendTCvSubstList :: Subst -> [Var] -> [Type] -> Subst
extendTCvSubstList Subst
subst [Var]
tvs [Type]
tys
= (Subst -> Var -> Type -> Subst)
-> Subst -> [Var] -> [Type] -> Subst
forall acc a b. (acc -> a -> b -> acc) -> acc -> [a] -> [b] -> acc
foldl2 Subst -> Var -> Type -> Subst
extendTCvSubst Subst
subst [Var]
tvs [Type]
tys
unionSubst :: Subst -> Subst -> Subst
unionSubst :: Subst -> Subst -> Subst
unionSubst (Subst InScopeSet
in_scope1 IdSubstEnv
ids1 TvSubstEnv
tenv1 CvSubstEnv
cenv1) (Subst InScopeSet
in_scope2 IdSubstEnv
ids2 TvSubstEnv
tenv2 CvSubstEnv
cenv2)
= Bool
-> (InScopeSet -> IdSubstEnv -> TvSubstEnv -> CvSubstEnv -> Subst)
-> InScopeSet
-> IdSubstEnv
-> TvSubstEnv
-> CvSubstEnv
-> Subst
forall a. HasCallStack => Bool -> a -> a
assert (IdSubstEnv
ids1 IdSubstEnv -> IdSubstEnv -> Bool
forall a. VarEnv a -> VarEnv a -> Bool
`disjointVarEnv` IdSubstEnv
ids2
Bool -> Bool -> Bool
&& TvSubstEnv
tenv1 TvSubstEnv -> TvSubstEnv -> Bool
forall a. VarEnv a -> VarEnv a -> Bool
`disjointVarEnv` TvSubstEnv
tenv2
Bool -> Bool -> Bool
&& CvSubstEnv
cenv1 CvSubstEnv -> CvSubstEnv -> Bool
forall a. VarEnv a -> VarEnv a -> Bool
`disjointVarEnv` CvSubstEnv
cenv2 )
InScopeSet -> IdSubstEnv -> TvSubstEnv -> CvSubstEnv -> Subst
Subst (InScopeSet
in_scope1 InScopeSet -> InScopeSet -> InScopeSet
`unionInScope` InScopeSet
in_scope2)
(IdSubstEnv
ids1 IdSubstEnv -> IdSubstEnv -> IdSubstEnv
forall a. VarEnv a -> VarEnv a -> VarEnv a
`plusVarEnv` IdSubstEnv
ids2)
(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] -> Subst
zipTvSubst :: HasDebugCallStack => [Var] -> [Type] -> Subst
zipTvSubst [Var]
tvs [Type]
tys
= InScopeSet -> TvSubstEnv -> Subst
mkTvSubst (VarSet -> InScopeSet
mkInScopeSet ([Type] -> VarSet
shallowTyCoVarsOfTypes [Type]
tys)) TvSubstEnv
tenv
where
tenv :: TvSubstEnv
tenv = [Var] -> [Type] -> TvSubstEnv
HasDebugCallStack => [Var] -> [Type] -> TvSubstEnv
zipTyEnv [Var]
tvs [Type]
tys
zipCvSubst :: HasDebugCallStack => [CoVar] -> [Coercion] -> Subst
zipCvSubst :: HasDebugCallStack => [Var] -> [Coercion] -> Subst
zipCvSubst [Var]
cvs [Coercion]
cos
= InScopeSet -> CvSubstEnv -> Subst
mkCvSubst (VarSet -> InScopeSet
mkInScopeSet ([Coercion] -> VarSet
shallowTyCoVarsOfCos [Coercion]
cos)) CvSubstEnv
cenv
where
cenv :: CvSubstEnv
cenv = [Var] -> [Coercion] -> CvSubstEnv
HasDebugCallStack => [Var] -> [Coercion] -> CvSubstEnv
zipCoEnv [Var]
cvs [Coercion]
cos
zipTCvSubst :: HasDebugCallStack => [TyCoVar] -> [Type] -> Subst
zipTCvSubst :: HasDebugCallStack => [Var] -> [Type] -> Subst
zipTCvSubst [Var]
tcvs [Type]
tys
= [Var] -> [Type] -> Subst -> Subst
zip_tcvsubst [Var]
tcvs [Type]
tys (Subst -> Subst) -> Subst -> Subst
forall a b. (a -> b) -> a -> b
$
InScopeSet -> Subst
mkEmptySubst (InScopeSet -> Subst) -> InScopeSet -> Subst
forall a b. (a -> b) -> a -> b
$ VarSet -> InScopeSet
mkInScopeSet (VarSet -> InScopeSet) -> VarSet -> InScopeSet
forall a b. (a -> b) -> a -> b
$ [Type] -> VarSet
shallowTyCoVarsOfTypes [Type]
tys
where zip_tcvsubst :: [TyCoVar] -> [Type] -> Subst -> Subst
zip_tcvsubst :: [Var] -> [Type] -> Subst -> Subst
zip_tcvsubst (Var
tv:[Var]
tvs) (Type
ty:[Type]
tys) Subst
subst
= [Var] -> [Type] -> Subst -> Subst
zip_tcvsubst [Var]
tvs [Type]
tys (Subst -> Var -> Type -> Subst
extendTCvSubst Subst
subst Var
tv Type
ty)
zip_tcvsubst [] [] Subst
subst = Subst
subst
zip_tcvsubst [Var]
_ [Type]
_ Subst
_ = String -> SDoc -> Subst
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"zipTCvSubst: length mismatch"
([Var] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Var]
tcvs SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
tys)
mkTvSubstPrs :: [(TyVar, Type)] -> Subst
mkTvSubstPrs :: [(Var, Type)] -> Subst
mkTvSubstPrs [] = Subst
emptySubst
mkTvSubstPrs [(Var, Type)]
prs =
Bool -> SDoc -> Subst -> Subst
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr Bool
onlyTyVarsAndNoCoercionTy (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"prs" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [(Var, Type)] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [(Var, Type)]
prs) (Subst -> Subst) -> Subst -> Subst
forall a b. (a -> b) -> a -> b
$
InScopeSet -> TvSubstEnv -> Subst
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
shallowTyCoVarsOfTypes ([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)
| (Var
tv, Type
ty) <- [(Var, Type)]
prs ]
zipTyEnv :: HasDebugCallStack => [TyVar] -> [Type] -> TvSubstEnv
zipTyEnv :: HasDebugCallStack => [Var] -> [Type] -> TvSubstEnv
zipTyEnv [Var]
tyvars [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 Bool -> Bool -> Bool
&& ([Var]
tyvars [Var] -> [Type] -> Bool
forall a b. [a] -> [b] -> Bool
`equalLength` [Type]
tys))
= String -> SDoc -> TvSubstEnv
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"zipTyEnv" ([Var] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Var]
tyvars SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
tys)
| Bool
otherwise
= Bool
-> ([Var] -> [Type] -> TvSubstEnv) -> [Var] -> [Type] -> TvSubstEnv
forall a. HasCallStack => Bool -> a -> a
assert ((Type -> Bool) -> [Type] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Bool -> Bool
not (Bool -> Bool) -> (Type -> Bool) -> Type -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Bool
isCoercionTy) [Type]
tys )
[Var] -> [Type] -> TvSubstEnv
forall key elt. Uniquable key => [key] -> [elt] -> UniqFM key elt
zipToUFM [Var]
tyvars [Type]
tys
zipCoEnv :: HasDebugCallStack => [CoVar] -> [Coercion] -> CvSubstEnv
zipCoEnv :: HasDebugCallStack => [Var] -> [Coercion] -> CvSubstEnv
zipCoEnv [Var]
cvs [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 String
"zipCoEnv" ([Var] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Var]
cvs SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [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. HasDebugCallStack => String -> [a] -> [b] -> [(a, b)]
zipEqual String
"zipCoEnv" [Var]
cvs [Coercion]
cos)
instance Outputable Subst where
ppr :: Subst -> SDoc
ppr (Subst InScopeSet
in_scope IdSubstEnv
ids TvSubstEnv
tvs CvSubstEnv
cvs)
= String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"<InScope =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc
in_scope_doc
SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
" IdSubst =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> IdSubstEnv -> SDoc
forall a. Outputable a => a -> SDoc
ppr IdSubstEnv
ids
SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
" TvSubst =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TvSubstEnv -> SDoc
forall a. Outputable a => a -> SDoc
ppr TvSubstEnv
tvs
SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
" CvSubst =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> CvSubstEnv -> SDoc
forall a. Outputable a => a -> SDoc
ppr CvSubstEnv
cvs
SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> Char -> SDoc
forall doc. IsLine doc => Char -> doc
char Char
'>'
where
in_scope_doc :: SDoc
in_scope_doc = VarSet -> ([Var] -> SDoc) -> SDoc
pprVarSet (InScopeSet -> VarSet
getInScopeVars InScopeSet
in_scope) (SDoc -> SDoc
forall doc. IsLine doc => doc -> doc
braces (SDoc -> SDoc) -> ([Var] -> SDoc) -> [Var] -> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [SDoc] -> SDoc
forall doc. IsLine doc => [doc] -> doc
fsep ([SDoc] -> SDoc) -> ([Var] -> [SDoc]) -> [Var] -> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Var -> SDoc) -> [Var] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr)
substTyWith :: HasDebugCallStack => [TyVar] -> [Type] -> Type -> Type
substTyWith :: HasDebugCallStack => [Var] -> [Type] -> Type -> Type
substTyWith [Var]
tvs [Type]
tys = {-#SCC "substTyWith" #-}
Bool -> (Subst -> Type -> Type) -> Subst -> Type -> Type
forall a. HasCallStack => Bool -> a -> a
assert ([Var]
tvs [Var] -> [Type] -> Bool
forall a b. [a] -> [b] -> Bool
`equalLength` [Type]
tys )
HasDebugCallStack => Subst -> Type -> Type
Subst -> Type -> Type
substTy ([Var] -> [Type] -> Subst
HasDebugCallStack => [Var] -> [Type] -> Subst
zipTvSubst [Var]
tvs [Type]
tys)
substTyWithUnchecked :: [TyVar] -> [Type] -> Type -> Type
substTyWithUnchecked :: [Var] -> [Type] -> Type -> Type
substTyWithUnchecked [Var]
tvs [Type]
tys
= Bool -> (Subst -> Type -> Type) -> Subst -> Type -> Type
forall a. HasCallStack => Bool -> a -> a
assert ([Var]
tvs [Var] -> [Type] -> Bool
forall a b. [a] -> [b] -> Bool
`equalLength` [Type]
tys )
Subst -> Type -> Type
substTyUnchecked ([Var] -> [Type] -> Subst
HasDebugCallStack => [Var] -> [Type] -> Subst
zipTvSubst [Var]
tvs [Type]
tys)
substTyWithInScope :: HasDebugCallStack => InScopeSet -> [TyVar] -> [Type] -> Type -> Type
substTyWithInScope :: HasDebugCallStack => InScopeSet -> [Var] -> [Type] -> Type -> Type
substTyWithInScope InScopeSet
in_scope [Var]
tvs [Type]
tys Type
ty =
Bool -> (Subst -> Type -> Type) -> Subst -> Type -> Type
forall a. HasCallStack => Bool -> a -> a
assert ([Var]
tvs [Var] -> [Type] -> Bool
forall a b. [a] -> [b] -> Bool
`equalLength` [Type]
tys )
HasDebugCallStack => Subst -> Type -> Type
Subst -> Type -> Type
substTy (InScopeSet -> TvSubstEnv -> Subst
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 :: HasDebugCallStack => [TyVar] -> [Type] -> Coercion -> Coercion
substCoWith :: HasDebugCallStack => [Var] -> [Type] -> Coercion -> Coercion
substCoWith [Var]
tvs [Type]
tys = Bool
-> (Subst -> Coercion -> Coercion) -> Subst -> Coercion -> Coercion
forall a. HasCallStack => Bool -> a -> a
assert ([Var]
tvs [Var] -> [Type] -> Bool
forall a b. [a] -> [b] -> Bool
`equalLength` [Type]
tys )
HasDebugCallStack => Subst -> Coercion -> Coercion
Subst -> Coercion -> Coercion
substCo ([Var] -> [Type] -> Subst
HasDebugCallStack => [Var] -> [Type] -> Subst
zipTvSubst [Var]
tvs [Type]
tys)
substCoWithUnchecked :: [TyVar] -> [Type] -> Coercion -> Coercion
substCoWithUnchecked :: [Var] -> [Type] -> Coercion -> Coercion
substCoWithUnchecked [Var]
tvs [Type]
tys
= Bool
-> (Subst -> Coercion -> Coercion) -> Subst -> Coercion -> Coercion
forall a. HasCallStack => Bool -> a -> a
assert ([Var]
tvs [Var] -> [Type] -> Bool
forall a b. [a] -> [b] -> Bool
`equalLength` [Type]
tys )
Subst -> Coercion -> Coercion
substCoUnchecked ([Var] -> [Type] -> Subst
HasDebugCallStack => [Var] -> [Type] -> Subst
zipTvSubst [Var]
tvs [Type]
tys)
substTyWithCoVars :: [CoVar] -> [Coercion] -> Type -> Type
substTyWithCoVars :: [Var] -> [Coercion] -> Type -> Type
substTyWithCoVars [Var]
cvs [Coercion]
cos = HasDebugCallStack => Subst -> Type -> Type
Subst -> Type -> Type
substTy ([Var] -> [Coercion] -> Subst
HasDebugCallStack => [Var] -> [Coercion] -> Subst
zipCvSubst [Var]
cvs [Coercion]
cos)
substTysWith :: HasDebugCallStack => [TyVar] -> [Type] -> [Type] -> [Type]
substTysWith :: HasDebugCallStack => [Var] -> [Type] -> [Type] -> [Type]
substTysWith [Var]
tvs [Type]
tys = Bool -> (Subst -> [Type] -> [Type]) -> Subst -> [Type] -> [Type]
forall a. HasCallStack => Bool -> a -> a
assert ([Var]
tvs [Var] -> [Type] -> Bool
forall a b. [a] -> [b] -> Bool
`equalLength` [Type]
tys )
HasDebugCallStack => Subst -> [Type] -> [Type]
Subst -> [Type] -> [Type]
substTys ([Var] -> [Type] -> Subst
HasDebugCallStack => [Var] -> [Type] -> Subst
zipTvSubst [Var]
tvs [Type]
tys)
substTysWithCoVars :: HasDebugCallStack => [CoVar] -> [Coercion] -> [Type] -> [Type]
substTysWithCoVars :: HasDebugCallStack => [Var] -> [Coercion] -> [Type] -> [Type]
substTysWithCoVars [Var]
cvs [Coercion]
cos = Bool -> (Subst -> [Type] -> [Type]) -> Subst -> [Type] -> [Type]
forall a. HasCallStack => Bool -> a -> a
assert ([Var]
cvs [Var] -> [Coercion] -> Bool
forall a b. [a] -> [b] -> Bool
`equalLength` [Coercion]
cos )
HasDebugCallStack => Subst -> [Type] -> [Type]
Subst -> [Type] -> [Type]
substTys ([Var] -> [Coercion] -> Subst
HasDebugCallStack => [Var] -> [Coercion] -> Subst
zipCvSubst [Var]
cvs [Coercion]
cos)
substTyAddInScope :: HasDebugCallStack => Subst -> Type -> Type
substTyAddInScope :: HasDebugCallStack => Subst -> Type -> Type
substTyAddInScope Subst
subst Type
ty =
HasDebugCallStack => Subst -> Type -> Type
Subst -> Type -> Type
substTy (Subst -> VarSet -> Subst
extendSubstInScopeSet Subst
subst (VarSet -> Subst) -> VarSet -> Subst
forall a b. (a -> b) -> a -> b
$ Type -> VarSet
tyCoVarsOfType Type
ty) Type
ty
isValidTCvSubst :: Subst -> Bool
isValidTCvSubst :: Subst -> Bool
isValidTCvSubst (Subst InScopeSet
in_scope IdSubstEnv
_ TvSubstEnv
tenv 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
shallowTyCoVarsOfTyVarEnv TvSubstEnv
tenv
cenvFVs :: VarSet
cenvFVs = CvSubstEnv -> VarSet
shallowTyCoVarsOfCoVarEnv CvSubstEnv
cenv
checkValidSubst :: HasDebugCallStack => Subst -> [Type] -> [Coercion] -> a -> a
checkValidSubst :: forall a.
HasDebugCallStack =>
Subst -> [Type] -> [Coercion] -> a -> a
checkValidSubst subst :: Subst
subst@(Subst InScopeSet
in_scope IdSubstEnv
_ TvSubstEnv
tenv CvSubstEnv
cenv) [Type]
tys [Coercion]
cos a
a
= Bool -> SDoc -> a -> a
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (Subst -> Bool
isValidTCvSubst Subst
subst)
(String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"in_scope" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> InScopeSet -> SDoc
forall a. Outputable a => a -> SDoc
ppr InScopeSet
in_scope SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$
String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"tenv" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TvSubstEnv -> SDoc
forall a. Outputable a => a -> SDoc
ppr TvSubstEnv
tenv SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$
String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"tenvFVs" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> VarSet -> SDoc
forall a. Outputable a => a -> SDoc
ppr (TvSubstEnv -> VarSet
shallowTyCoVarsOfTyVarEnv TvSubstEnv
tenv) SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$
String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"cenv" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> CvSubstEnv -> SDoc
forall a. Outputable a => a -> SDoc
ppr CvSubstEnv
cenv SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$
String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"cenvFVs" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> VarSet -> SDoc
forall a. Outputable a => a -> SDoc
ppr (CvSubstEnv -> VarSet
shallowTyCoVarsOfCoVarEnv CvSubstEnv
cenv) SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$
String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"tys" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
tys SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$
String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"cos" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [Coercion] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Coercion]
cos) (a -> a) -> a -> a
forall a b. (a -> b) -> a -> b
$
Bool -> SDoc -> a -> a
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr Bool
tysCosFVsInScope
(String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"in_scope" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> InScopeSet -> SDoc
forall a. Outputable a => a -> SDoc
ppr InScopeSet
in_scope SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$
String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"tenv" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TvSubstEnv -> SDoc
forall a. Outputable a => a -> SDoc
ppr TvSubstEnv
tenv SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$
String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"cenv" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> CvSubstEnv -> SDoc
forall a. Outputable a => a -> SDoc
ppr CvSubstEnv
cenv SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$
String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"tys" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
tys SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$
String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"cos" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [Coercion] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Coercion]
cos SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$
String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"needInScope" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> VarSet -> SDoc
forall a. Outputable a => a -> SDoc
ppr VarSet
needInScope)
a
a
where
substDomain :: [Unique]
substDomain = TvSubstEnv -> [Unique]
forall {k} (key :: k) elt. UniqFM key elt -> [Unique]
nonDetKeysUFM TvSubstEnv
tenv [Unique] -> [Unique] -> [Unique]
forall a. [a] -> [a] -> [a]
++ CvSubstEnv -> [Unique]
forall {k} (key :: k) elt. UniqFM key elt -> [Unique]
nonDetKeysUFM CvSubstEnv
cenv
needInScope :: VarSet
needInScope = ([Type] -> VarSet
shallowTyCoVarsOfTypes [Type]
tys VarSet -> VarSet -> VarSet
`unionVarSet`
[Coercion] -> VarSet
shallowTyCoVarsOfCos [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 :: HasDebugCallStack => Subst -> Type -> Type
substTy :: HasDebugCallStack => Subst -> Type -> Type
substTy Subst
subst Type
ty
| Subst -> Bool
isEmptyTCvSubst Subst
subst = Type
ty
| Bool
otherwise = Subst -> [Type] -> [Coercion] -> Type -> Type
forall a.
HasDebugCallStack =>
Subst -> [Type] -> [Coercion] -> a -> a
checkValidSubst Subst
subst [Type
ty] [] (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$
Subst -> Type -> Type
subst_ty Subst
subst Type
ty
substTyUnchecked :: Subst -> Type -> Type
substTyUnchecked :: Subst -> Type -> Type
substTyUnchecked Subst
subst Type
ty
| Subst -> Bool
isEmptyTCvSubst Subst
subst = Type
ty
| Bool
otherwise = Subst -> Type -> Type
subst_ty Subst
subst Type
ty
substScaledTy :: HasDebugCallStack => Subst -> Scaled Type -> Scaled Type
substScaledTy :: HasDebugCallStack => Subst -> Scaled Type -> Scaled Type
substScaledTy Subst
subst Scaled Type
scaled_ty = (Type -> Type) -> Scaled Type -> Scaled Type
mapScaledType (HasDebugCallStack => Subst -> Type -> Type
Subst -> Type -> Type
substTy Subst
subst) Scaled Type
scaled_ty
substScaledTyUnchecked :: HasDebugCallStack => Subst -> Scaled Type -> Scaled Type
substScaledTyUnchecked :: HasDebugCallStack => Subst -> Scaled Type -> Scaled Type
substScaledTyUnchecked Subst
subst Scaled Type
scaled_ty = (Type -> Type) -> Scaled Type -> Scaled Type
mapScaledType (Subst -> Type -> Type
substTyUnchecked Subst
subst) Scaled Type
scaled_ty
substTys :: HasDebugCallStack => Subst -> [Type] -> [Type]
substTys :: HasDebugCallStack => Subst -> [Type] -> [Type]
substTys Subst
subst [Type]
tys
| Subst -> Bool
isEmptyTCvSubst Subst
subst = [Type]
tys
| Bool
otherwise = Subst -> [Type] -> [Coercion] -> [Type] -> [Type]
forall a.
HasDebugCallStack =>
Subst -> [Type] -> [Coercion] -> a -> a
checkValidSubst Subst
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 (Subst -> Type -> Type
subst_ty Subst
subst) [Type]
tys
substScaledTys :: HasDebugCallStack => Subst -> [Scaled Type] -> [Scaled Type]
substScaledTys :: HasDebugCallStack => Subst -> [Scaled Type] -> [Scaled Type]
substScaledTys Subst
subst [Scaled Type]
scaled_tys
| Subst -> Bool
isEmptyTCvSubst Subst
subst = [Scaled Type]
scaled_tys
| Bool
otherwise = Subst -> [Type] -> [Coercion] -> [Scaled Type] -> [Scaled Type]
forall a.
HasDebugCallStack =>
Subst -> [Type] -> [Coercion] -> a -> a
checkValidSubst Subst
subst ((Scaled Type -> Type) -> [Scaled Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Scaled Type -> Type
forall a. Scaled a -> Type
scaledMult [Scaled Type]
scaled_tys [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ (Scaled Type -> Type) -> [Scaled Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Scaled Type -> Type
forall a. Scaled a -> a
scaledThing [Scaled Type]
scaled_tys) [] ([Scaled Type] -> [Scaled Type]) -> [Scaled Type] -> [Scaled Type]
forall a b. (a -> b) -> a -> b
$
(Scaled Type -> Scaled Type) -> [Scaled Type] -> [Scaled Type]
forall a b. (a -> b) -> [a] -> [b]
map ((Type -> Type) -> Scaled Type -> Scaled Type
mapScaledType (Subst -> Type -> Type
subst_ty Subst
subst)) [Scaled Type]
scaled_tys
substTysUnchecked :: Subst -> [Type] -> [Type]
substTysUnchecked :: Subst -> [Type] -> [Type]
substTysUnchecked Subst
subst [Type]
tys
| Subst -> Bool
isEmptyTCvSubst Subst
subst = [Type]
tys
| Bool
otherwise = (Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> Type -> Type
subst_ty Subst
subst) [Type]
tys
substScaledTysUnchecked :: Subst -> [Scaled Type] -> [Scaled Type]
substScaledTysUnchecked :: Subst -> [Scaled Type] -> [Scaled Type]
substScaledTysUnchecked Subst
subst [Scaled Type]
tys
| Subst -> Bool
isEmptyTCvSubst Subst
subst = [Scaled Type]
tys
| Bool
otherwise = (Scaled Type -> Scaled Type) -> [Scaled Type] -> [Scaled Type]
forall a b. (a -> b) -> [a] -> [b]
map ((Type -> Type) -> Scaled Type -> Scaled Type
mapScaledType (Subst -> Type -> Type
subst_ty Subst
subst)) [Scaled Type]
tys
substTheta :: HasDebugCallStack => Subst -> ThetaType -> ThetaType
substTheta :: HasDebugCallStack => Subst -> [Type] -> [Type]
substTheta = HasDebugCallStack => Subst -> [Type] -> [Type]
Subst -> [Type] -> [Type]
substTys
substThetaUnchecked :: Subst -> ThetaType -> ThetaType
substThetaUnchecked :: Subst -> [Type] -> [Type]
substThetaUnchecked = Subst -> [Type] -> [Type]
substTysUnchecked
subst_ty :: Subst -> Type -> Type
subst_ty :: Subst -> Type -> Type
subst_ty Subst
subst Type
ty
= Type -> Type
go Type
ty
where
go :: Type -> Type
go (TyVarTy Var
tv) = Subst -> Var -> Type
substTyVar Subst
subst Var
tv
go (AppTy Type
fun Type
arg) = (Type -> Type -> Type
mkAppTy (Type -> Type -> Type) -> Type -> Type -> Type
forall a b. (a -> b) -> a -> b
$! (Type -> Type
go Type
fun)) (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$! (Type -> Type
go Type
arg)
go ty :: Type
ty@(TyConApp TyCon
tc []) = TyCon
tc TyCon -> Type -> Type
forall a b. a -> b -> b
`seq` Type
ty
go (TyConApp TyCon
tc [Type]
tys) = (TyCon -> [Type] -> Type
mkTyConApp (TyCon -> [Type] -> Type) -> TyCon -> [Type] -> Type
forall a b. (a -> b) -> a -> b
$! TyCon
tc) ([Type] -> Type) -> [Type] -> Type
forall a b. (a -> b) -> a -> b
$! (Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
strictMap Type -> Type
go [Type]
tys
go ty :: Type
ty@(FunTy { ft_mult :: Type -> Type
ft_mult = Type
mult, ft_arg :: Type -> Type
ft_arg = Type
arg, ft_res :: Type -> Type
ft_res = Type
res })
= let !mult' :: Type
mult' = Type -> Type
go Type
mult
!arg' :: Type
arg' = Type -> Type
go Type
arg
!res' :: Type
res' = Type -> Type
go Type
res
in Type
ty { ft_mult = mult', ft_arg = arg', ft_res = res' }
go (ForAllTy (Bndr Var
tv ForAllTyFlag
vis) Type
ty)
= case Subst -> Var -> (Subst, Var)
substVarBndrUnchecked Subst
subst Var
tv of
(Subst
subst', Var
tv') ->
(VarBndr Var ForAllTyFlag -> Type -> Type
ForAllTy (VarBndr Var ForAllTyFlag -> Type -> Type)
-> VarBndr Var ForAllTyFlag -> Type -> Type
forall a b. (a -> b) -> a -> b
$! ((Var -> ForAllTyFlag -> VarBndr Var ForAllTyFlag
forall var argf. var -> argf -> VarBndr var argf
Bndr (Var -> ForAllTyFlag -> VarBndr Var ForAllTyFlag)
-> Var -> ForAllTyFlag -> VarBndr Var ForAllTyFlag
forall a b. (a -> b) -> a -> b
$! Var
tv') ForAllTyFlag
vis)) (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$!
(Subst -> Type -> Type
subst_ty Subst
subst' Type
ty)
go (LitTy TyLit
n) = TyLit -> Type
LitTy (TyLit -> Type) -> TyLit -> Type
forall a b. (a -> b) -> a -> b
$! TyLit
n
go (CastTy Type
ty 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
$! (Subst -> Coercion -> Coercion
subst_co Subst
subst Coercion
co)
go (CoercionTy Coercion
co) = Coercion -> Type
CoercionTy (Coercion -> Type) -> Coercion -> Type
forall a b. (a -> b) -> a -> b
$! (Subst -> Coercion -> Coercion
subst_co Subst
subst Coercion
co)
substTyVar :: Subst -> TyVar -> Type
substTyVar :: Subst -> Var -> Type
substTyVar (Subst InScopeSet
_ IdSubstEnv
_ TvSubstEnv
tenv CvSubstEnv
_) Var
tv
= Bool -> Type -> Type
forall a. HasCallStack => Bool -> a -> a
assert (Var -> Bool
isTyVar Var
tv) (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$
case TvSubstEnv -> Var -> Maybe Type
forall a. VarEnv a -> Var -> Maybe a
lookupVarEnv TvSubstEnv
tenv Var
tv of
Just Type
ty -> Type
ty
Maybe Type
Nothing -> Var -> Type
TyVarTy Var
tv
substTyVarToTyVar :: HasDebugCallStack => Subst -> TyVar -> TyVar
substTyVarToTyVar :: HasDebugCallStack => Subst -> Var -> Var
substTyVarToTyVar (Subst InScopeSet
_ IdSubstEnv
_ TvSubstEnv
tenv CvSubstEnv
_) Var
tv
= Bool -> Var -> Var
forall a. HasCallStack => Bool -> a -> a
assert (Var -> Bool
isTyVar Var
tv) (Var -> Var) -> Var -> Var
forall a b. (a -> b) -> a -> b
$
case TvSubstEnv -> Var -> Maybe Type
forall a. VarEnv a -> Var -> Maybe a
lookupVarEnv TvSubstEnv
tenv Var
tv of
Just Type
ty -> case Type -> Maybe Var
getTyVar_maybe Type
ty of
Just Var
tv -> Var
tv
Maybe Var
Nothing -> String -> SDoc -> Var
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"substTyVarToTyVar" (Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
tv SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty)
Maybe Type
Nothing -> Var
tv
substTyVars :: Subst -> [TyVar] -> [Type]
substTyVars :: Subst -> [Var] -> [Type]
substTyVars Subst
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
$ Subst -> Var -> Type
substTyVar Subst
subst
substTyCoVars :: Subst -> [TyCoVar] -> [Type]
substTyCoVars :: Subst -> [Var] -> [Type]
substTyCoVars Subst
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
$ Subst -> Var -> Type
substTyCoVar Subst
subst
substTyCoVar :: Subst -> TyCoVar -> Type
substTyCoVar :: Subst -> Var -> Type
substTyCoVar Subst
subst Var
tv
| Var -> Bool
isTyVar Var
tv = Subst -> Var -> Type
substTyVar Subst
subst Var
tv
| Bool
otherwise = Coercion -> Type
CoercionTy (Coercion -> Type) -> Coercion -> Type
forall a b. (a -> b) -> a -> b
$ Subst -> Var -> Coercion
substCoVar Subst
subst Var
tv
lookupTyVar :: Subst -> TyVar -> Maybe Type
lookupTyVar :: Subst -> Var -> Maybe Type
lookupTyVar (Subst InScopeSet
_ IdSubstEnv
_ TvSubstEnv
tenv CvSubstEnv
_) Var
tv
= Bool
-> (TvSubstEnv -> Var -> Maybe Type)
-> TvSubstEnv
-> Var
-> Maybe Type
forall a. HasCallStack => Bool -> a -> a
assert (Var -> Bool
isTyVar Var
tv )
TvSubstEnv -> Var -> Maybe Type
forall a. VarEnv a -> Var -> Maybe a
lookupVarEnv TvSubstEnv
tenv Var
tv
substCo :: HasDebugCallStack => Subst -> Coercion -> Coercion
substCo :: HasDebugCallStack => Subst -> Coercion -> Coercion
substCo Subst
subst Coercion
co
| Subst -> Bool
isEmptyTCvSubst Subst
subst = Coercion
co
| Bool
otherwise = Subst -> [Type] -> [Coercion] -> Coercion -> Coercion
forall a.
HasDebugCallStack =>
Subst -> [Type] -> [Coercion] -> a -> a
checkValidSubst Subst
subst [] [Coercion
co] (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$ Subst -> Coercion -> Coercion
subst_co Subst
subst Coercion
co
substCoUnchecked :: Subst -> Coercion -> Coercion
substCoUnchecked :: Subst -> Coercion -> Coercion
substCoUnchecked Subst
subst Coercion
co
| Subst -> Bool
isEmptyTCvSubst Subst
subst = Coercion
co
| Bool
otherwise = Subst -> Coercion -> Coercion
subst_co Subst
subst Coercion
co
substCos :: HasDebugCallStack => Subst -> [Coercion] -> [Coercion]
substCos :: HasDebugCallStack => Subst -> [Coercion] -> [Coercion]
substCos Subst
subst [Coercion]
cos
| Subst -> Bool
isEmptyTCvSubst Subst
subst = [Coercion]
cos
| Bool
otherwise = Subst -> [Type] -> [Coercion] -> [Coercion] -> [Coercion]
forall a.
HasDebugCallStack =>
Subst -> [Type] -> [Coercion] -> a -> a
checkValidSubst Subst
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 (Subst -> Coercion -> Coercion
subst_co Subst
subst) [Coercion]
cos
subst_co :: Subst -> Coercion -> Coercion
subst_co :: Subst -> Coercion -> Coercion
subst_co Subst
subst Coercion
co
= Coercion -> Coercion
go Coercion
co
where
go_ty :: Type -> Type
go_ty :: Type -> Type
go_ty = Subst -> Type -> Type
subst_ty Subst
subst
go_mco :: MCoercion -> MCoercion
go_mco :: MCoercion -> MCoercion
go_mco MCoercion
MRefl = MCoercion
MRefl
go_mco (MCo Coercion
co) = Coercion -> MCoercion
MCo (Coercion -> Coercion
go Coercion
co)
go :: Coercion -> Coercion
go :: Coercion -> Coercion
go (Refl Type
ty) = Type -> Coercion
mkNomReflCo (Type -> Coercion) -> Type -> Coercion
forall a b. (a -> b) -> a -> b
$! (Type -> Type
go_ty Type
ty)
go (GRefl Role
r Type
ty 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 Role
r TyCon
tc [Coercion]
args)= HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
Role -> TyCon -> [Coercion] -> Coercion
mkTyConAppCo Role
r TyCon
tc ([Coercion] -> Coercion) -> [Coercion] -> Coercion
forall a b. (a -> b) -> a -> b
$! [Coercion] -> [Coercion]
go_cos [Coercion]
args
go (AxiomCo CoAxiomRule
con [Coercion]
cos) = CoAxiomRule -> [Coercion] -> Coercion
mkAxiomCo CoAxiomRule
con ([Coercion] -> Coercion) -> [Coercion] -> Coercion
forall a b. (a -> b) -> a -> b
$! [Coercion] -> [Coercion]
go_cos [Coercion]
cos
go (AppCo Coercion
co 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 Var
tv ForAllTyFlag
visL ForAllTyFlag
visR Coercion
kind_co Coercion
co)
= case Subst -> Var -> Coercion -> (Subst, Var, Coercion)
substForAllCoBndrUnchecked Subst
subst Var
tv Coercion
kind_co of
(Subst
subst', Var
tv', Coercion
kind_co') ->
((HasDebugCallStack =>
Var
-> ForAllTyFlag -> ForAllTyFlag -> Coercion -> Coercion -> Coercion
Var
-> ForAllTyFlag -> ForAllTyFlag -> Coercion -> Coercion -> Coercion
mkForAllCo (Var
-> ForAllTyFlag
-> ForAllTyFlag
-> Coercion
-> Coercion
-> Coercion)
-> Var
-> ForAllTyFlag
-> ForAllTyFlag
-> Coercion
-> Coercion
-> Coercion
forall a b. (a -> b) -> a -> b
$! Var
tv') ForAllTyFlag
visL ForAllTyFlag
visR (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
$! Subst -> Coercion -> Coercion
subst_co Subst
subst' Coercion
co
go (FunCo Role
r FunTyFlag
afl FunTyFlag
afr Coercion
w Coercion
co1 Coercion
co2) = ((Role
-> FunTyFlag
-> FunTyFlag
-> Coercion
-> Coercion
-> Coercion
-> Coercion
mkFunCo2 Role
r FunTyFlag
afl FunTyFlag
afr (Coercion -> Coercion -> Coercion -> Coercion)
-> Coercion -> Coercion -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$! Coercion -> Coercion
go Coercion
w) (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 Var
cv) = Subst -> Var -> Coercion
substCoVar Subst
subst Var
cv
go (UnivCo { uco_prov :: Coercion -> UnivCoProvenance
uco_prov = UnivCoProvenance
p, uco_role :: Coercion -> Role
uco_role = Role
r
, uco_lty :: Coercion -> Type
uco_lty = Type
t1, uco_rty :: Coercion -> Type
uco_rty = Type
t2, uco_deps :: Coercion -> [Coercion]
uco_deps = [Coercion]
deps })
= ((((UnivCoProvenance -> [Coercion] -> Role -> Type -> Type -> Coercion
mkUnivCo (UnivCoProvenance
-> [Coercion] -> Role -> Type -> Type -> Coercion)
-> UnivCoProvenance
-> [Coercion]
-> Role
-> Type
-> Type
-> Coercion
forall a b. (a -> b) -> a -> b
$! UnivCoProvenance
p) ([Coercion] -> Role -> Type -> Type -> Coercion)
-> [Coercion] -> Role -> Type -> Type -> Coercion
forall a b. (a -> b) -> a -> b
$! [Coercion] -> [Coercion]
go_cos [Coercion]
deps) (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 Coercion
co) = Coercion -> Coercion
mkSymCo (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$! (Coercion -> Coercion
go Coercion
co)
go (TransCo Coercion
co1 Coercion
co2) = (HasDebugCallStack => Coercion -> Coercion -> Coercion
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 (SelCo CoSel
d Coercion
co) = HasDebugCallStack => CoSel -> Coercion -> Coercion
CoSel -> Coercion -> Coercion
mkSelCo CoSel
d (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$! (Coercion -> Coercion
go Coercion
co)
go (LRCo LeftOrRight
lr 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 Coercion
co 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 Coercion
co) = Coercion -> Coercion
mkKindCo (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$! (Coercion -> Coercion
go Coercion
co)
go (SubCo Coercion
co) = HasDebugCallStack => Coercion -> Coercion
Coercion -> Coercion
mkSubCo (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$! (Coercion -> Coercion
go Coercion
co)
go (HoleCo CoercionHole
h) = CoercionHole -> Coercion
HoleCo (CoercionHole -> Coercion) -> CoercionHole -> Coercion
forall a b. (a -> b) -> a -> b
$! CoercionHole -> CoercionHole
go_hole CoercionHole
h
go_cos :: [Coercion] -> [Coercion]
go_cos [Coercion]
cos = let cos' :: [Coercion]
cos' = (Coercion -> Coercion) -> [Coercion] -> [Coercion]
forall a b. (a -> b) -> [a] -> [b]
map Coercion -> Coercion
go [Coercion]
cos
in [Coercion]
cos' [Coercion] -> [Coercion] -> [Coercion]
forall a b. [a] -> b -> b
`seqList` [Coercion]
cos'
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 = updateVarType go_ty cv }
substDCoVarSet :: Subst -> DCoVarSet -> DCoVarSet
substDCoVarSet :: Subst -> DCoVarSet -> DCoVarSet
substDCoVarSet Subst
subst DCoVarSet
cvs = [Coercion] -> DCoVarSet
coVarsOfCosDSet ([Coercion] -> DCoVarSet) -> [Coercion] -> DCoVarSet
forall a b. (a -> b) -> a -> b
$ (Var -> Coercion) -> [Var] -> [Coercion]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> Var -> Coercion
substCoVar Subst
subst) ([Var] -> [Coercion]) -> [Var] -> [Coercion]
forall a b. (a -> b) -> a -> b
$
DCoVarSet -> [Var]
dVarSetElems DCoVarSet
cvs
substForAllCoBndr :: Subst -> TyCoVar -> KindCoercion
-> (Subst, TyCoVar, Coercion)
substForAllCoBndr :: Subst -> Var -> Coercion -> (Subst, Var, Coercion)
substForAllCoBndr Subst
subst
= SwapFlag
-> (Coercion -> Coercion)
-> Subst
-> Var
-> Coercion
-> (Subst, Var, Coercion)
substForAllCoBndrUsing SwapFlag
NotSwapped (HasDebugCallStack => Subst -> Coercion -> Coercion
Subst -> Coercion -> Coercion
substCo Subst
subst) Subst
subst
substForAllCoBndrUnchecked :: Subst -> TyCoVar -> KindCoercion
-> (Subst, TyCoVar, Coercion)
substForAllCoBndrUnchecked :: Subst -> Var -> Coercion -> (Subst, Var, Coercion)
substForAllCoBndrUnchecked Subst
subst
= SwapFlag
-> (Coercion -> Coercion)
-> Subst
-> Var
-> Coercion
-> (Subst, Var, Coercion)
substForAllCoBndrUsing SwapFlag
NotSwapped (Subst -> Coercion -> Coercion
substCoUnchecked Subst
subst) Subst
subst
substForAllCoBndrUsing :: SwapFlag
-> (Coercion -> Coercion)
-> Subst -> TyCoVar -> KindCoercion
-> (Subst, TyCoVar, KindCoercion)
substForAllCoBndrUsing :: SwapFlag
-> (Coercion -> Coercion)
-> Subst
-> Var
-> Coercion
-> (Subst, Var, Coercion)
substForAllCoBndrUsing SwapFlag
sym Coercion -> Coercion
sco Subst
subst Var
old_var
| Var -> Bool
isTyVar Var
old_var = SwapFlag
-> (Coercion -> Coercion)
-> Subst
-> Var
-> Coercion
-> (Subst, Var, Coercion)
substForAllCoTyVarBndrUsing SwapFlag
sym Coercion -> Coercion
sco Subst
subst Var
old_var
| Bool
otherwise = SwapFlag
-> (Coercion -> Coercion)
-> Subst
-> Var
-> Coercion
-> (Subst, Var, Coercion)
substForAllCoCoVarBndrUsing SwapFlag
sym Coercion -> Coercion
sco Subst
subst Var
old_var
substForAllCoTyVarBndrUsing :: SwapFlag
-> (Coercion -> Coercion)
-> Subst -> TyVar -> KindCoercion
-> (Subst, TyVar, KindCoercion)
substForAllCoTyVarBndrUsing :: SwapFlag
-> (Coercion -> Coercion)
-> Subst
-> Var
-> Coercion
-> (Subst, Var, Coercion)
substForAllCoTyVarBndrUsing SwapFlag
sym Coercion -> Coercion
sco (Subst InScopeSet
in_scope IdSubstEnv
idenv TvSubstEnv
tenv CvSubstEnv
cenv) Var
old_var Coercion
old_kind_co
= Bool -> (Subst, Var, Coercion) -> (Subst, Var, Coercion)
forall a. HasCallStack => Bool -> a -> a
assert (Var -> Bool
isTyVar Var
old_var )
( InScopeSet -> IdSubstEnv -> TvSubstEnv -> CvSubstEnv -> Subst
Subst (InScopeSet
in_scope InScopeSet -> Var -> InScopeSet
`extendInScopeSet` Var
new_var) IdSubstEnv
idenv TvSubstEnv
new_env CvSubstEnv
cenv
, Var
new_var, Coercion
new_kind_co )
where
new_env :: TvSubstEnv
new_env | Bool
no_change, SwapFlag -> Bool
notSwapped SwapFlag
sym
= TvSubstEnv -> Var -> TvSubstEnv
forall a. VarEnv a -> Var -> VarEnv a
delVarEnv TvSubstEnv
tenv Var
old_var
| SwapFlag -> Bool
isSwapped SwapFlag
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
new_ki1 :: Type
new_ki1 = HasDebugCallStack => Coercion -> Type
Coercion -> Type
coercionLKind 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 :: SwapFlag
-> (Coercion -> Coercion)
-> Subst -> CoVar -> KindCoercion
-> (Subst, CoVar, KindCoercion)
substForAllCoCoVarBndrUsing :: SwapFlag
-> (Coercion -> Coercion)
-> Subst
-> Var
-> Coercion
-> (Subst, Var, Coercion)
substForAllCoCoVarBndrUsing SwapFlag
sym Coercion -> Coercion
sco (Subst InScopeSet
in_scope IdSubstEnv
idenv TvSubstEnv
tenv CvSubstEnv
cenv)
Var
old_var Coercion
old_kind_co
= Bool -> (Subst, Var, Coercion) -> (Subst, Var, Coercion)
forall a. HasCallStack => Bool -> a -> a
assert (Var -> Bool
isCoVar Var
old_var )
( InScopeSet -> IdSubstEnv -> TvSubstEnv -> CvSubstEnv -> Subst
Subst (InScopeSet
in_scope InScopeSet -> Var -> InScopeSet
`extendInScopeSet` Var
new_var) IdSubstEnv
idenv TvSubstEnv
tenv CvSubstEnv
new_cenv
, Var
new_var, Coercion
new_kind_co )
where
new_cenv :: CvSubstEnv
new_cenv | Bool
no_change, SwapFlag -> Bool
notSwapped SwapFlag
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 Type
h1 Type
h2 = HasDebugCallStack => Coercion -> Pair Type
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 = SwapFlag -> Type -> Type -> Type
forall a. SwapFlag -> a -> a -> a
pickSwap SwapFlag
sym Type
h1 Type
h2
substCoVar :: Subst -> CoVar -> Coercion
substCoVar :: Subst -> Var -> Coercion
substCoVar (Subst InScopeSet
_ IdSubstEnv
_ TvSubstEnv
_ CvSubstEnv
cenv) Var
cv
= case CvSubstEnv -> Var -> Maybe Coercion
forall a. VarEnv a -> Var -> Maybe a
lookupVarEnv CvSubstEnv
cenv Var
cv of
Just Coercion
co -> Coercion
co
Maybe Coercion
Nothing -> Var -> Coercion
CoVarCo Var
cv
substCoVars :: Subst -> [CoVar] -> [Coercion]
substCoVars :: Subst -> [Var] -> [Coercion]
substCoVars Subst
subst [Var]
cvs = (Var -> Coercion) -> [Var] -> [Coercion]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> Var -> Coercion
substCoVar Subst
subst) [Var]
cvs
lookupCoVar :: Subst -> Var -> Maybe Coercion
lookupCoVar :: Subst -> Var -> Maybe Coercion
lookupCoVar (Subst InScopeSet
_ IdSubstEnv
_ TvSubstEnv
_ CvSubstEnv
cenv) Var
v = CvSubstEnv -> Var -> Maybe Coercion
forall a. VarEnv a -> Var -> Maybe a
lookupVarEnv CvSubstEnv
cenv Var
v
substTyVarBndr :: HasDebugCallStack => Subst -> TyVar -> (Subst, TyVar)
substTyVarBndr :: HasDebugCallStack => Subst -> Var -> (Subst, Var)
substTyVarBndr = (Subst -> Type -> Type) -> Subst -> Var -> (Subst, Var)
substTyVarBndrUsing HasDebugCallStack => Subst -> Type -> Type
Subst -> Type -> Type
substTy
substTyVarBndrs :: HasDebugCallStack => Subst -> [TyVar] -> (Subst, [TyVar])
substTyVarBndrs :: HasDebugCallStack => Subst -> [Var] -> (Subst, [Var])
substTyVarBndrs = (Subst -> Var -> (Subst, Var)) -> Subst -> [Var] -> (Subst, [Var])
forall (t :: * -> *) s a b.
Traversable t =>
(s -> a -> (s, b)) -> s -> t a -> (s, t b)
mapAccumL HasDebugCallStack => Subst -> Var -> (Subst, Var)
Subst -> Var -> (Subst, Var)
substTyVarBndr
substVarBndr :: HasDebugCallStack => Subst -> TyCoVar -> (Subst, TyCoVar)
substVarBndr :: HasDebugCallStack => Subst -> Var -> (Subst, Var)
substVarBndr = (Subst -> Type -> Type) -> Subst -> Var -> (Subst, Var)
substVarBndrUsing HasDebugCallStack => Subst -> Type -> Type
Subst -> Type -> Type
substTy
substVarBndrs :: HasDebugCallStack => Subst -> [TyCoVar] -> (Subst, [TyCoVar])
substVarBndrs :: HasDebugCallStack => Subst -> [Var] -> (Subst, [Var])
substVarBndrs = (Subst -> Var -> (Subst, Var)) -> Subst -> [Var] -> (Subst, [Var])
forall (t :: * -> *) s a b.
Traversable t =>
(s -> a -> (s, b)) -> s -> t a -> (s, t b)
mapAccumL HasDebugCallStack => Subst -> Var -> (Subst, Var)
Subst -> Var -> (Subst, Var)
substVarBndr
substCoVarBndr :: HasDebugCallStack => Subst -> CoVar -> (Subst, CoVar)
substCoVarBndr :: HasDebugCallStack => Subst -> Var -> (Subst, Var)
substCoVarBndr = (Subst -> Type -> Type) -> Subst -> Var -> (Subst, Var)
substCoVarBndrUsing HasDebugCallStack => Subst -> Type -> Type
Subst -> Type -> Type
substTy
substVarBndrUnchecked :: Subst -> TyCoVar -> (Subst, TyCoVar)
substVarBndrUnchecked :: Subst -> Var -> (Subst, Var)
substVarBndrUnchecked = (Subst -> Type -> Type) -> Subst -> Var -> (Subst, Var)
substVarBndrUsing Subst -> Type -> Type
substTyUnchecked
substVarBndrUsing :: (Subst -> Type -> Type)
-> Subst -> TyCoVar -> (Subst, TyCoVar)
substVarBndrUsing :: (Subst -> Type -> Type) -> Subst -> Var -> (Subst, Var)
substVarBndrUsing Subst -> Type -> Type
subst_fn Subst
subst Var
v
| Var -> Bool
isTyVar Var
v = (Subst -> Type -> Type) -> Subst -> Var -> (Subst, Var)
substTyVarBndrUsing Subst -> Type -> Type
subst_fn Subst
subst Var
v
| Bool
otherwise = (Subst -> Type -> Type) -> Subst -> Var -> (Subst, Var)
substCoVarBndrUsing Subst -> Type -> Type
subst_fn Subst
subst Var
v
substTyVarBndrUsing
:: (Subst -> Type -> Type)
-> Subst -> TyVar -> (Subst, TyVar)
substTyVarBndrUsing :: (Subst -> Type -> Type) -> Subst -> Var -> (Subst, Var)
substTyVarBndrUsing Subst -> Type -> Type
subst_fn subst :: Subst
subst@(Subst InScopeSet
in_scope IdSubstEnv
idenv TvSubstEnv
tenv CvSubstEnv
cenv) Var
old_var
= Bool -> SDoc -> (Subst, Var) -> (Subst, Var)
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr Bool
_no_capture (Var -> SDoc
pprTyVar Var
old_var SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ Var -> SDoc
pprTyVar Var
new_var SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ Subst -> SDoc
forall a. Outputable a => a -> SDoc
ppr Subst
subst) ((Subst, Var) -> (Subst, Var)) -> (Subst, Var) -> (Subst, Var)
forall a b. (a -> b) -> a -> b
$
Bool -> (Subst, Var) -> (Subst, Var)
forall a. HasCallStack => Bool -> a -> a
assert (Var -> Bool
isTyVar Var
old_var )
(InScopeSet -> IdSubstEnv -> TvSubstEnv -> CvSubstEnv -> Subst
Subst (InScopeSet
in_scope InScopeSet -> Var -> InScopeSet
`extendInScopeSet` Var
new_var) IdSubstEnv
idenv 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
shallowTyCoVarsOfTyVarEnv 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 (Subst -> Type -> Type
subst_fn Subst
subst Type
old_ki)
substCoVarBndrUsing
:: (Subst -> Type -> Type)
-> Subst -> CoVar -> (Subst, CoVar)
substCoVarBndrUsing :: (Subst -> Type -> Type) -> Subst -> Var -> (Subst, Var)
substCoVarBndrUsing Subst -> Type -> Type
subst_fn subst :: Subst
subst@(Subst InScopeSet
in_scope IdSubstEnv
idenv TvSubstEnv
tenv CvSubstEnv
cenv) Var
old_var
= Bool -> (Subst, Var) -> (Subst, Var)
forall a. HasCallStack => Bool -> a -> a
assert (Var -> Bool
isCoVar Var
old_var)
(InScopeSet -> IdSubstEnv -> TvSubstEnv -> CvSubstEnv -> Subst
Subst (InScopeSet
in_scope InScopeSet -> Var -> InScopeSet
`extendInScopeSet` Var
new_var) IdSubstEnv
idenv 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
(Type
t1, Type
t2, Role
role) = HasDebugCallStack => Var -> (Type, Type, Role)
Var -> (Type, Type, Role)
coVarTypesRole Var
old_var
t1' :: Type
t1' = Subst -> Type -> Type
subst_fn Subst
subst Type
t1
t2' :: Type
t2' = Subst -> Type -> Type
subst_fn Subst
subst Type
t2
new_var_type :: Type
new_var_type = Role -> Type -> Type -> Type
mkCoercionType Role
role Type
t1' Type
t2'
cloneTyVarBndr :: Subst -> TyVar -> Unique -> (Subst, TyVar)
cloneTyVarBndr :: Subst -> Var -> Unique -> (Subst, Var)
cloneTyVarBndr subst :: Subst
subst@(Subst InScopeSet
in_scope IdSubstEnv
id_env TvSubstEnv
tv_env CvSubstEnv
cv_env) Var
tv Unique
uniq
= Bool -> SDoc -> (Subst, Var) -> (Subst, Var)
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (Var -> Bool
isTyVar Var
tv) (Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
tv)
( InScopeSet -> IdSubstEnv -> TvSubstEnv -> CvSubstEnv -> Subst
Subst (InScopeSet -> Var -> InScopeSet
extendInScopeSet InScopeSet
in_scope Var
tv')
IdSubstEnv
id_env
(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 (HasDebugCallStack => Subst -> Type -> Type
Subst -> Type -> Type
substTy Subst
subst Type
old_ki)
tv' :: Var
tv' = Var -> Unique -> Var
setVarUnique Var
tv1 Unique
uniq
cloneTyVarBndrs :: Subst -> [TyVar] -> UniqSupply -> (Subst, [TyVar])
cloneTyVarBndrs :: Subst -> [Var] -> UniqSupply -> (Subst, [Var])
cloneTyVarBndrs Subst
subst [] UniqSupply
_usupply = (Subst
subst, [])
cloneTyVarBndrs Subst
subst (Var
t:[Var]
ts) UniqSupply
usupply = (Subst
subst'', Var
tvVar -> [Var] -> [Var]
forall a. a -> [a] -> [a]
:[Var]
tvs)
where
(Unique
uniq, UniqSupply
usupply') = UniqSupply -> (Unique, UniqSupply)
takeUniqFromSupply UniqSupply
usupply
(Subst
subst' , Var
tv ) = Subst -> Var -> Unique -> (Subst, Var)
cloneTyVarBndr Subst
subst Var
t Unique
uniq
(Subst
subst'', [Var]
tvs) = Subst -> [Var] -> UniqSupply -> (Subst, [Var])
cloneTyVarBndrs Subst
subst' [Var]
ts UniqSupply
usupply'
substTyCoBndr :: Subst -> PiTyBinder -> (Subst, PiTyBinder)
substTyCoBndr :: Subst -> PiTyBinder -> (Subst, PiTyBinder)
substTyCoBndr Subst
subst (Anon Scaled Type
ty FunTyFlag
af) = (Subst
subst, Scaled Type -> FunTyFlag -> PiTyBinder
Anon (HasDebugCallStack => Subst -> Scaled Type -> Scaled Type
Subst -> Scaled Type -> Scaled Type
substScaledTy Subst
subst Scaled Type
ty) FunTyFlag
af)
substTyCoBndr Subst
subst (Named (Bndr Var
tv ForAllTyFlag
vis)) = (Subst
subst', VarBndr Var ForAllTyFlag -> PiTyBinder
Named (Var -> ForAllTyFlag -> VarBndr Var ForAllTyFlag
forall var argf. var -> argf -> VarBndr var argf
Bndr Var
tv' ForAllTyFlag
vis))
where
(Subst
subst', Var
tv') = HasDebugCallStack => Subst -> Var -> (Subst, Var)
Subst -> Var -> (Subst, Var)
substVarBndr Subst
subst Var
tv