{-# LANGUAGE BangPatterns #-}
{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
module GHC.Core.TyCo.Tidy
(
tidyType, tidyTypes,
tidyOpenType, tidyOpenTypes,
tidyVarBndr, tidyVarBndrs, tidyFreeTyCoVars, avoidNameClashes,
tidyOpenTyCoVar, tidyOpenTyCoVars,
tidyTyCoVarOcc,
tidyTopType,
tidyCo, tidyCos,
tidyForAllTyBinder, tidyForAllTyBinders
) where
import GHC.Prelude
import GHC.Data.FastString
import GHC.Core.TyCo.Rep
import GHC.Core.TyCo.FVs (tyCoVarsOfTypesWellScoped, tyCoVarsOfTypeList)
import GHC.Types.Name hiding (varName)
import GHC.Types.Var
import GHC.Types.Var.Env
import GHC.Utils.Misc (strictMap)
import Data.List (mapAccumL)
tidyVarBndrs :: TidyEnv -> [TyCoVar] -> (TidyEnv, [TyCoVar])
tidyVarBndrs :: TidyEnv -> [TyCoVar] -> (TidyEnv, [TyCoVar])
tidyVarBndrs TidyEnv
tidy_env [TyCoVar]
tvs
= (TidyEnv -> TyCoVar -> (TidyEnv, TyCoVar))
-> TidyEnv -> [TyCoVar] -> (TidyEnv, [TyCoVar])
forall (t :: * -> *) s a b.
Traversable t =>
(s -> a -> (s, b)) -> s -> t a -> (s, t b)
mapAccumL TidyEnv -> TyCoVar -> (TidyEnv, TyCoVar)
tidyVarBndr ([TyCoVar] -> TidyEnv -> TidyEnv
avoidNameClashes [TyCoVar]
tvs TidyEnv
tidy_env) [TyCoVar]
tvs
tidyVarBndr :: TidyEnv -> TyCoVar -> (TidyEnv, TyCoVar)
tidyVarBndr :: TidyEnv -> TyCoVar -> (TidyEnv, TyCoVar)
tidyVarBndr tidy_env :: TidyEnv
tidy_env@(TidyOccEnv
occ_env, VarEnv TyCoVar
subst) TyCoVar
var
= case TidyOccEnv -> OccName -> (TidyOccEnv, OccName)
tidyOccName TidyOccEnv
occ_env (TyCoVar -> OccName
getHelpfulOccName TyCoVar
var) of
(TidyOccEnv
occ_env', OccName
occ') -> ((TidyOccEnv
occ_env', VarEnv TyCoVar
subst'), TyCoVar
var')
where
subst' :: VarEnv TyCoVar
subst' = VarEnv TyCoVar -> TyCoVar -> TyCoVar -> VarEnv TyCoVar
forall a. VarEnv a -> TyCoVar -> a -> VarEnv a
extendVarEnv VarEnv TyCoVar
subst TyCoVar
var TyCoVar
var'
var' :: TyCoVar
var' = (Type -> Type) -> TyCoVar -> TyCoVar
updateVarType (TidyEnv -> Type -> Type
tidyType TidyEnv
tidy_env) (TyCoVar -> Name -> TyCoVar
setVarName TyCoVar
var Name
name')
name' :: Name
name' = Name -> OccName -> Name
tidyNameOcc Name
name OccName
occ'
name :: Name
name = TyCoVar -> Name
varName TyCoVar
var
avoidNameClashes :: [TyCoVar] -> TidyEnv -> TidyEnv
avoidNameClashes :: [TyCoVar] -> TidyEnv -> TidyEnv
avoidNameClashes [TyCoVar]
tvs (TidyOccEnv
occ_env, VarEnv TyCoVar
subst)
= (TidyOccEnv -> [OccName] -> TidyOccEnv
avoidClashesOccEnv TidyOccEnv
occ_env [OccName]
occs, VarEnv TyCoVar
subst)
where
occs :: [OccName]
occs = (TyCoVar -> OccName) -> [TyCoVar] -> [OccName]
forall a b. (a -> b) -> [a] -> [b]
map TyCoVar -> OccName
getHelpfulOccName [TyCoVar]
tvs
getHelpfulOccName :: TyCoVar -> OccName
getHelpfulOccName :: TyCoVar -> OccName
getHelpfulOccName TyCoVar
tv
| Name -> Bool
isSystemName Name
name, TyCoVar -> Bool
isTcTyVar TyCoVar
tv
= FastString -> OccName
mkTyVarOccFS (OccName -> FastString
occNameFS OccName
occ FastString -> FastString -> FastString
`appendFS` String -> FastString
fsLit String
"0")
| Bool
otherwise
= OccName
occ
where
name :: Name
name = TyCoVar -> Name
varName TyCoVar
tv
occ :: OccName
occ = Name -> OccName
forall a. NamedThing a => a -> OccName
getOccName Name
name
tidyForAllTyBinder :: TidyEnv -> VarBndr TyCoVar vis
-> (TidyEnv, VarBndr TyCoVar vis)
tidyForAllTyBinder :: forall vis.
TidyEnv -> VarBndr TyCoVar vis -> (TidyEnv, VarBndr TyCoVar vis)
tidyForAllTyBinder TidyEnv
tidy_env (Bndr TyCoVar
tv vis
vis)
= (TidyEnv
tidy_env', TyCoVar -> vis -> VarBndr TyCoVar vis
forall var argf. var -> argf -> VarBndr var argf
Bndr TyCoVar
tv' vis
vis)
where
(TidyEnv
tidy_env', TyCoVar
tv') = TidyEnv -> TyCoVar -> (TidyEnv, TyCoVar)
tidyVarBndr TidyEnv
tidy_env TyCoVar
tv
tidyForAllTyBinders :: TidyEnv -> [VarBndr TyCoVar vis]
-> (TidyEnv, [VarBndr TyCoVar vis])
tidyForAllTyBinders :: forall vis.
TidyEnv
-> [VarBndr TyCoVar vis] -> (TidyEnv, [VarBndr TyCoVar vis])
tidyForAllTyBinders TidyEnv
tidy_env [VarBndr TyCoVar vis]
tvbs
= (TidyEnv -> VarBndr TyCoVar vis -> (TidyEnv, VarBndr TyCoVar vis))
-> TidyEnv
-> [VarBndr TyCoVar vis]
-> (TidyEnv, [VarBndr TyCoVar vis])
forall (t :: * -> *) s a b.
Traversable t =>
(s -> a -> (s, b)) -> s -> t a -> (s, t b)
mapAccumL TidyEnv -> VarBndr TyCoVar vis -> (TidyEnv, VarBndr TyCoVar vis)
forall vis.
TidyEnv -> VarBndr TyCoVar vis -> (TidyEnv, VarBndr TyCoVar vis)
tidyForAllTyBinder
([TyCoVar] -> TidyEnv -> TidyEnv
avoidNameClashes ([VarBndr TyCoVar vis] -> [TyCoVar]
forall tv argf. [VarBndr tv argf] -> [tv]
binderVars [VarBndr TyCoVar vis]
tvbs) TidyEnv
tidy_env) [VarBndr TyCoVar vis]
tvbs
tidyFreeTyCoVars :: TidyEnv -> [TyCoVar] -> TidyEnv
tidyFreeTyCoVars :: TidyEnv -> [TyCoVar] -> TidyEnv
tidyFreeTyCoVars TidyEnv
tidy_env [TyCoVar]
tyvars
= (TidyEnv, [TyCoVar]) -> TidyEnv
forall a b. (a, b) -> a
fst (TidyEnv -> [TyCoVar] -> (TidyEnv, [TyCoVar])
tidyOpenTyCoVars TidyEnv
tidy_env [TyCoVar]
tyvars)
tidyOpenTyCoVars :: TidyEnv -> [TyCoVar] -> (TidyEnv, [TyCoVar])
tidyOpenTyCoVars :: TidyEnv -> [TyCoVar] -> (TidyEnv, [TyCoVar])
tidyOpenTyCoVars TidyEnv
env [TyCoVar]
tyvars = (TidyEnv -> TyCoVar -> (TidyEnv, TyCoVar))
-> TidyEnv -> [TyCoVar] -> (TidyEnv, [TyCoVar])
forall (t :: * -> *) s a b.
Traversable t =>
(s -> a -> (s, b)) -> s -> t a -> (s, t b)
mapAccumL TidyEnv -> TyCoVar -> (TidyEnv, TyCoVar)
tidyOpenTyCoVar TidyEnv
env [TyCoVar]
tyvars
tidyOpenTyCoVar :: TidyEnv -> TyCoVar -> (TidyEnv, TyCoVar)
tidyOpenTyCoVar :: TidyEnv -> TyCoVar -> (TidyEnv, TyCoVar)
tidyOpenTyCoVar env :: TidyEnv
env@(TidyOccEnv
_, VarEnv TyCoVar
subst) TyCoVar
tyvar
= case VarEnv TyCoVar -> TyCoVar -> Maybe TyCoVar
forall a. VarEnv a -> TyCoVar -> Maybe a
lookupVarEnv VarEnv TyCoVar
subst TyCoVar
tyvar of
Just TyCoVar
tyvar' -> (TidyEnv
env, TyCoVar
tyvar')
Maybe TyCoVar
Nothing ->
let env' :: TidyEnv
env' = TidyEnv -> [TyCoVar] -> TidyEnv
tidyFreeTyCoVars TidyEnv
env (Type -> [TyCoVar]
tyCoVarsOfTypeList (TyCoVar -> Type
tyVarKind TyCoVar
tyvar))
in TidyEnv -> TyCoVar -> (TidyEnv, TyCoVar)
tidyVarBndr TidyEnv
env' TyCoVar
tyvar
tidyTyCoVarOcc :: TidyEnv -> TyCoVar -> TyCoVar
tidyTyCoVarOcc :: TidyEnv -> TyCoVar -> TyCoVar
tidyTyCoVarOcc env :: TidyEnv
env@(TidyOccEnv
_, VarEnv TyCoVar
subst) TyCoVar
tv
= case VarEnv TyCoVar -> TyCoVar -> Maybe TyCoVar
forall a. VarEnv a -> TyCoVar -> Maybe a
lookupVarEnv VarEnv TyCoVar
subst TyCoVar
tv of
Maybe TyCoVar
Nothing -> (Type -> Type) -> TyCoVar -> TyCoVar
updateVarType (TidyEnv -> Type -> Type
tidyType TidyEnv
env) TyCoVar
tv
Just TyCoVar
tv' -> TyCoVar
tv'
tidyTypes :: TidyEnv -> [Type] -> [Type]
tidyTypes :: TidyEnv -> [Type] -> [Type]
tidyTypes TidyEnv
env [Type]
tys = (Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
strictMap (TidyEnv -> Type -> Type
tidyType TidyEnv
env) [Type]
tys
tidyType :: TidyEnv -> Type -> Type
tidyType :: TidyEnv -> Type -> Type
tidyType TidyEnv
_ t :: Type
t@(LitTy {}) = Type
t
tidyType TidyEnv
env (TyVarTy TyCoVar
tv) = TyCoVar -> Type
TyVarTy (TyCoVar -> Type) -> TyCoVar -> Type
forall a b. (a -> b) -> a -> b
$! TidyEnv -> TyCoVar -> TyCoVar
tidyTyCoVarOcc TidyEnv
env TyCoVar
tv
tidyType TidyEnv
_ t :: Type
t@(TyConApp TyCon
_ []) = Type
t
tidyType TidyEnv
env (TyConApp TyCon
tycon [Type]
tys) = TyCon -> [Type] -> Type
TyConApp TyCon
tycon ([Type] -> Type) -> [Type] -> Type
forall a b. (a -> b) -> a -> b
$! TidyEnv -> [Type] -> [Type]
tidyTypes TidyEnv
env [Type]
tys
tidyType TidyEnv
env (AppTy Type
fun Type
arg) = (Type -> Type -> Type
AppTy (Type -> Type -> Type) -> Type -> Type -> Type
forall a b. (a -> b) -> a -> b
$! (TidyEnv -> Type -> Type
tidyType TidyEnv
env Type
fun)) (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$! (TidyEnv -> Type -> Type
tidyType TidyEnv
env Type
arg)
tidyType TidyEnv
env ty :: Type
ty@(FunTy FunTyFlag
_ Type
w Type
arg Type
res) = let { !w' :: Type
w' = TidyEnv -> Type -> Type
tidyType TidyEnv
env Type
w
; !arg' :: Type
arg' = TidyEnv -> Type -> Type
tidyType TidyEnv
env Type
arg
; !res' :: Type
res' = TidyEnv -> Type -> Type
tidyType TidyEnv
env Type
res }
in Type
ty { ft_mult = w', ft_arg = arg', ft_res = res' }
tidyType TidyEnv
env (ty :: Type
ty@(ForAllTy{})) = ([(TyCoVar, ForAllTyFlag)] -> Type -> Type
mkForAllTys' ([(TyCoVar, ForAllTyFlag)] -> Type -> Type)
-> [(TyCoVar, ForAllTyFlag)] -> Type -> Type
forall a b. (a -> b) -> a -> b
$! ([TyCoVar] -> [ForAllTyFlag] -> [(TyCoVar, ForAllTyFlag)]
forall a b. [a] -> [b] -> [(a, b)]
zip [TyCoVar]
tvs' [ForAllTyFlag]
vis)) (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$! TidyEnv -> Type -> Type
tidyType TidyEnv
env' Type
body_ty
where
([TyCoVar]
tvs, [ForAllTyFlag]
vis, Type
body_ty) = Type -> ([TyCoVar], [ForAllTyFlag], Type)
splitForAllTyCoVars' Type
ty
(TidyEnv
env', [TyCoVar]
tvs') = TidyEnv -> [TyCoVar] -> (TidyEnv, [TyCoVar])
tidyVarBndrs TidyEnv
env [TyCoVar]
tvs
tidyType TidyEnv
env (CastTy Type
ty KindCoercion
co) = (Type -> KindCoercion -> Type
CastTy (Type -> KindCoercion -> Type) -> Type -> KindCoercion -> Type
forall a b. (a -> b) -> a -> b
$! TidyEnv -> Type -> Type
tidyType TidyEnv
env Type
ty) (KindCoercion -> Type) -> KindCoercion -> Type
forall a b. (a -> b) -> a -> b
$! (TidyEnv -> KindCoercion -> KindCoercion
tidyCo TidyEnv
env KindCoercion
co)
tidyType TidyEnv
env (CoercionTy KindCoercion
co) = KindCoercion -> Type
CoercionTy (KindCoercion -> Type) -> KindCoercion -> Type
forall a b. (a -> b) -> a -> b
$! (TidyEnv -> KindCoercion -> KindCoercion
tidyCo TidyEnv
env KindCoercion
co)
mkForAllTys' :: [(TyCoVar, ForAllTyFlag)] -> Type -> Type
mkForAllTys' :: [(TyCoVar, ForAllTyFlag)] -> Type -> Type
mkForAllTys' [(TyCoVar, ForAllTyFlag)]
tvvs Type
ty = ((TyCoVar, ForAllTyFlag) -> Type -> Type)
-> Type -> [(TyCoVar, ForAllTyFlag)] -> Type
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (TyCoVar, ForAllTyFlag) -> Type -> Type
strictMkForAllTy Type
ty [(TyCoVar, ForAllTyFlag)]
tvvs
where
strictMkForAllTy :: (TyCoVar, ForAllTyFlag) -> Type -> Type
strictMkForAllTy (TyCoVar
tv,ForAllTyFlag
vis) Type
ty = (ForAllTyBinder -> Type -> Type
ForAllTy (ForAllTyBinder -> Type -> Type) -> ForAllTyBinder -> Type -> Type
forall a b. (a -> b) -> a -> b
$! ((TyCoVar -> ForAllTyFlag -> ForAllTyBinder
forall var argf. var -> argf -> VarBndr var argf
Bndr (TyCoVar -> ForAllTyFlag -> ForAllTyBinder)
-> TyCoVar -> ForAllTyFlag -> ForAllTyBinder
forall a b. (a -> b) -> a -> b
$! TyCoVar
tv) (ForAllTyFlag -> ForAllTyBinder) -> ForAllTyFlag -> ForAllTyBinder
forall a b. (a -> b) -> a -> b
$! ForAllTyFlag
vis)) (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$! Type
ty
splitForAllTyCoVars' :: Type -> ([TyCoVar], [ForAllTyFlag], Type)
splitForAllTyCoVars' :: Type -> ([TyCoVar], [ForAllTyFlag], Type)
splitForAllTyCoVars' Type
ty = Type
-> [TyCoVar] -> [ForAllTyFlag] -> ([TyCoVar], [ForAllTyFlag], Type)
go Type
ty [] []
where
go :: Type
-> [TyCoVar] -> [ForAllTyFlag] -> ([TyCoVar], [ForAllTyFlag], Type)
go (ForAllTy (Bndr TyCoVar
tv ForAllTyFlag
vis) Type
ty) [TyCoVar]
tvs [ForAllTyFlag]
viss = Type
-> [TyCoVar] -> [ForAllTyFlag] -> ([TyCoVar], [ForAllTyFlag], Type)
go Type
ty (TyCoVar
tvTyCoVar -> [TyCoVar] -> [TyCoVar]
forall a. a -> [a] -> [a]
:[TyCoVar]
tvs) (ForAllTyFlag
visForAllTyFlag -> [ForAllTyFlag] -> [ForAllTyFlag]
forall a. a -> [a] -> [a]
:[ForAllTyFlag]
viss)
go Type
ty [TyCoVar]
tvs [ForAllTyFlag]
viss = ([TyCoVar] -> [TyCoVar]
forall a. [a] -> [a]
reverse [TyCoVar]
tvs, [ForAllTyFlag] -> [ForAllTyFlag]
forall a. [a] -> [a]
reverse [ForAllTyFlag]
viss, Type
ty)
tidyOpenTypes :: TidyEnv -> [Type] -> (TidyEnv, [Type])
tidyOpenTypes :: TidyEnv -> [Type] -> (TidyEnv, [Type])
tidyOpenTypes TidyEnv
env [Type]
tys
= (TidyEnv
env', TidyEnv -> [Type] -> [Type]
tidyTypes (TidyOccEnv
trimmed_occ_env, VarEnv TyCoVar
var_env) [Type]
tys)
where
(env' :: TidyEnv
env'@(TidyOccEnv
_, VarEnv TyCoVar
var_env), [TyCoVar]
tvs') = TidyEnv -> [TyCoVar] -> (TidyEnv, [TyCoVar])
tidyOpenTyCoVars TidyEnv
env ([TyCoVar] -> (TidyEnv, [TyCoVar]))
-> [TyCoVar] -> (TidyEnv, [TyCoVar])
forall a b. (a -> b) -> a -> b
$
[Type] -> [TyCoVar]
tyCoVarsOfTypesWellScoped [Type]
tys
trimmed_occ_env :: TidyOccEnv
trimmed_occ_env = [OccName] -> TidyOccEnv
initTidyOccEnv ((TyCoVar -> OccName) -> [TyCoVar] -> [OccName]
forall a b. (a -> b) -> [a] -> [b]
map TyCoVar -> OccName
forall a. NamedThing a => a -> OccName
getOccName [TyCoVar]
tvs')
tidyOpenType :: TidyEnv -> Type -> (TidyEnv, Type)
tidyOpenType :: TidyEnv -> Type -> (TidyEnv, Type)
tidyOpenType TidyEnv
env Type
ty = let (TidyEnv
env', [Type
ty']) = TidyEnv -> [Type] -> (TidyEnv, [Type])
tidyOpenTypes TidyEnv
env [Type
ty] in
(TidyEnv
env', Type
ty')
tidyTopType :: Type -> Type
tidyTopType :: Type -> Type
tidyTopType Type
ty = TidyEnv -> Type -> Type
tidyType TidyEnv
emptyTidyEnv Type
ty
tidyCo :: TidyEnv -> Coercion -> Coercion
tidyCo :: TidyEnv -> KindCoercion -> KindCoercion
tidyCo env :: TidyEnv
env@(TidyOccEnv
_, VarEnv TyCoVar
subst) KindCoercion
co
= KindCoercion -> KindCoercion
go KindCoercion
co
where
go_mco :: MCoercion -> MCoercion
go_mco MCoercion
MRefl = MCoercion
MRefl
go_mco (MCo KindCoercion
co) = KindCoercion -> MCoercion
MCo (KindCoercion -> MCoercion) -> KindCoercion -> MCoercion
forall a b. (a -> b) -> a -> b
$! KindCoercion -> KindCoercion
go KindCoercion
co
go :: KindCoercion -> KindCoercion
go (Refl Type
ty) = Type -> KindCoercion
Refl (Type -> KindCoercion) -> Type -> KindCoercion
forall a b. (a -> b) -> a -> b
$! TidyEnv -> Type -> Type
tidyType TidyEnv
env Type
ty
go (GRefl Role
r Type
ty MCoercion
mco) = (Role -> Type -> MCoercion -> KindCoercion
GRefl Role
r (Type -> MCoercion -> KindCoercion)
-> Type -> MCoercion -> KindCoercion
forall a b. (a -> b) -> a -> b
$! TidyEnv -> Type -> Type
tidyType TidyEnv
env Type
ty) (MCoercion -> KindCoercion) -> MCoercion -> KindCoercion
forall a b. (a -> b) -> a -> b
$! MCoercion -> MCoercion
go_mco MCoercion
mco
go (TyConAppCo Role
r TyCon
tc [KindCoercion]
cos) = Role -> TyCon -> [KindCoercion] -> KindCoercion
TyConAppCo Role
r TyCon
tc ([KindCoercion] -> KindCoercion) -> [KindCoercion] -> KindCoercion
forall a b. (a -> b) -> a -> b
$! (KindCoercion -> KindCoercion) -> [KindCoercion] -> [KindCoercion]
forall a b. (a -> b) -> [a] -> [b]
strictMap KindCoercion -> KindCoercion
go [KindCoercion]
cos
go (AppCo KindCoercion
co1 KindCoercion
co2) = (KindCoercion -> KindCoercion -> KindCoercion
AppCo (KindCoercion -> KindCoercion -> KindCoercion)
-> KindCoercion -> KindCoercion -> KindCoercion
forall a b. (a -> b) -> a -> b
$! KindCoercion -> KindCoercion
go KindCoercion
co1) (KindCoercion -> KindCoercion) -> KindCoercion -> KindCoercion
forall a b. (a -> b) -> a -> b
$! KindCoercion -> KindCoercion
go KindCoercion
co2
go (ForAllCo TyCoVar
tv KindCoercion
h KindCoercion
co) = ((TyCoVar -> KindCoercion -> KindCoercion -> KindCoercion
ForAllCo (TyCoVar -> KindCoercion -> KindCoercion -> KindCoercion)
-> TyCoVar -> KindCoercion -> KindCoercion -> KindCoercion
forall a b. (a -> b) -> a -> b
$! TyCoVar
tvp) (KindCoercion -> KindCoercion -> KindCoercion)
-> KindCoercion -> KindCoercion -> KindCoercion
forall a b. (a -> b) -> a -> b
$! (KindCoercion -> KindCoercion
go KindCoercion
h)) (KindCoercion -> KindCoercion) -> KindCoercion -> KindCoercion
forall a b. (a -> b) -> a -> b
$! (TidyEnv -> KindCoercion -> KindCoercion
tidyCo TidyEnv
envp KindCoercion
co)
where (TidyEnv
envp, TyCoVar
tvp) = TidyEnv -> TyCoVar -> (TidyEnv, TyCoVar)
tidyVarBndr TidyEnv
env TyCoVar
tv
go (FunCo Role
r FunTyFlag
afl FunTyFlag
afr KindCoercion
w KindCoercion
co1 KindCoercion
co2) = ((Role
-> FunTyFlag
-> FunTyFlag
-> KindCoercion
-> KindCoercion
-> KindCoercion
-> KindCoercion
FunCo Role
r FunTyFlag
afl FunTyFlag
afr (KindCoercion -> KindCoercion -> KindCoercion -> KindCoercion)
-> KindCoercion -> KindCoercion -> KindCoercion -> KindCoercion
forall a b. (a -> b) -> a -> b
$! KindCoercion -> KindCoercion
go KindCoercion
w) (KindCoercion -> KindCoercion -> KindCoercion)
-> KindCoercion -> KindCoercion -> KindCoercion
forall a b. (a -> b) -> a -> b
$! KindCoercion -> KindCoercion
go KindCoercion
co1) (KindCoercion -> KindCoercion) -> KindCoercion -> KindCoercion
forall a b. (a -> b) -> a -> b
$! KindCoercion -> KindCoercion
go KindCoercion
co2
go (CoVarCo TyCoVar
cv) = case VarEnv TyCoVar -> TyCoVar -> Maybe TyCoVar
forall a. VarEnv a -> TyCoVar -> Maybe a
lookupVarEnv VarEnv TyCoVar
subst TyCoVar
cv of
Maybe TyCoVar
Nothing -> TyCoVar -> KindCoercion
CoVarCo TyCoVar
cv
Just TyCoVar
cv' -> TyCoVar -> KindCoercion
CoVarCo TyCoVar
cv'
go (HoleCo CoercionHole
h) = CoercionHole -> KindCoercion
HoleCo CoercionHole
h
go (AxiomInstCo CoAxiom Branched
con BranchIndex
ind [KindCoercion]
cos) = CoAxiom Branched -> BranchIndex -> [KindCoercion] -> KindCoercion
AxiomInstCo CoAxiom Branched
con BranchIndex
ind ([KindCoercion] -> KindCoercion) -> [KindCoercion] -> KindCoercion
forall a b. (a -> b) -> a -> b
$! (KindCoercion -> KindCoercion) -> [KindCoercion] -> [KindCoercion]
forall a b. (a -> b) -> [a] -> [b]
strictMap KindCoercion -> KindCoercion
go [KindCoercion]
cos
go (UnivCo UnivCoProvenance
p Role
r Type
t1 Type
t2) = (((UnivCoProvenance -> Role -> Type -> Type -> KindCoercion
UnivCo (UnivCoProvenance -> Role -> Type -> Type -> KindCoercion)
-> UnivCoProvenance -> Role -> Type -> Type -> KindCoercion
forall a b. (a -> b) -> a -> b
$! (UnivCoProvenance -> UnivCoProvenance
go_prov UnivCoProvenance
p)) (Role -> Type -> Type -> KindCoercion)
-> Role -> Type -> Type -> KindCoercion
forall a b. (a -> b) -> a -> b
$! Role
r) (Type -> Type -> KindCoercion) -> Type -> Type -> KindCoercion
forall a b. (a -> b) -> a -> b
$!
TidyEnv -> Type -> Type
tidyType TidyEnv
env Type
t1) (Type -> KindCoercion) -> Type -> KindCoercion
forall a b. (a -> b) -> a -> b
$! TidyEnv -> Type -> Type
tidyType TidyEnv
env Type
t2
go (SymCo KindCoercion
co) = KindCoercion -> KindCoercion
SymCo (KindCoercion -> KindCoercion) -> KindCoercion -> KindCoercion
forall a b. (a -> b) -> a -> b
$! KindCoercion -> KindCoercion
go KindCoercion
co
go (TransCo KindCoercion
co1 KindCoercion
co2) = (KindCoercion -> KindCoercion -> KindCoercion
TransCo (KindCoercion -> KindCoercion -> KindCoercion)
-> KindCoercion -> KindCoercion -> KindCoercion
forall a b. (a -> b) -> a -> b
$! KindCoercion -> KindCoercion
go KindCoercion
co1) (KindCoercion -> KindCoercion) -> KindCoercion -> KindCoercion
forall a b. (a -> b) -> a -> b
$! KindCoercion -> KindCoercion
go KindCoercion
co2
go (SelCo CoSel
d KindCoercion
co) = CoSel -> KindCoercion -> KindCoercion
SelCo CoSel
d (KindCoercion -> KindCoercion) -> KindCoercion -> KindCoercion
forall a b. (a -> b) -> a -> b
$! KindCoercion -> KindCoercion
go KindCoercion
co
go (LRCo LeftOrRight
lr KindCoercion
co) = LeftOrRight -> KindCoercion -> KindCoercion
LRCo LeftOrRight
lr (KindCoercion -> KindCoercion) -> KindCoercion -> KindCoercion
forall a b. (a -> b) -> a -> b
$! KindCoercion -> KindCoercion
go KindCoercion
co
go (InstCo KindCoercion
co KindCoercion
ty) = (KindCoercion -> KindCoercion -> KindCoercion
InstCo (KindCoercion -> KindCoercion -> KindCoercion)
-> KindCoercion -> KindCoercion -> KindCoercion
forall a b. (a -> b) -> a -> b
$! KindCoercion -> KindCoercion
go KindCoercion
co) (KindCoercion -> KindCoercion) -> KindCoercion -> KindCoercion
forall a b. (a -> b) -> a -> b
$! KindCoercion -> KindCoercion
go KindCoercion
ty
go (KindCo KindCoercion
co) = KindCoercion -> KindCoercion
KindCo (KindCoercion -> KindCoercion) -> KindCoercion -> KindCoercion
forall a b. (a -> b) -> a -> b
$! KindCoercion -> KindCoercion
go KindCoercion
co
go (SubCo KindCoercion
co) = KindCoercion -> KindCoercion
SubCo (KindCoercion -> KindCoercion) -> KindCoercion -> KindCoercion
forall a b. (a -> b) -> a -> b
$! KindCoercion -> KindCoercion
go KindCoercion
co
go (AxiomRuleCo CoAxiomRule
ax [KindCoercion]
cos) = CoAxiomRule -> [KindCoercion] -> KindCoercion
AxiomRuleCo CoAxiomRule
ax ([KindCoercion] -> KindCoercion) -> [KindCoercion] -> KindCoercion
forall a b. (a -> b) -> a -> b
$ (KindCoercion -> KindCoercion) -> [KindCoercion] -> [KindCoercion]
forall a b. (a -> b) -> [a] -> [b]
strictMap KindCoercion -> KindCoercion
go [KindCoercion]
cos
go_prov :: UnivCoProvenance -> UnivCoProvenance
go_prov (PhantomProv KindCoercion
co) = KindCoercion -> UnivCoProvenance
PhantomProv (KindCoercion -> UnivCoProvenance)
-> KindCoercion -> UnivCoProvenance
forall a b. (a -> b) -> a -> b
$! KindCoercion -> KindCoercion
go KindCoercion
co
go_prov (ProofIrrelProv KindCoercion
co) = KindCoercion -> UnivCoProvenance
ProofIrrelProv (KindCoercion -> UnivCoProvenance)
-> KindCoercion -> UnivCoProvenance
forall a b. (a -> b) -> a -> b
$! KindCoercion -> KindCoercion
go KindCoercion
co
go_prov p :: UnivCoProvenance
p@(PluginProv String
_) = UnivCoProvenance
p
go_prov p :: UnivCoProvenance
p@(CorePrepProv Bool
_) = UnivCoProvenance
p
tidyCos :: TidyEnv -> [Coercion] -> [Coercion]
tidyCos :: TidyEnv -> [KindCoercion] -> [KindCoercion]
tidyCos TidyEnv
env = (KindCoercion -> KindCoercion) -> [KindCoercion] -> [KindCoercion]
forall a b. (a -> b) -> [a] -> [b]
strictMap (TidyEnv -> KindCoercion -> KindCoercion
tidyCo TidyEnv
env)