{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
module GHC.Core.TyCo.Tidy
(
tidyType, tidyTypes,
tidyCo, tidyCos,
tidyTopType,
tidyOpenType, tidyOpenTypes,
tidyOpenTypeX, tidyOpenTypesX,
tidyFreeTyCoVars, tidyFreeTyCoVarX, tidyFreeTyCoVarsX,
tidyAvoiding,
tidyVarBndr, tidyVarBndrs, avoidNameClashes,
tidyForAllTyBinder, tidyForAllTyBinders,
tidyTyCoVarOcc
) where
import GHC.Prelude
import GHC.Data.FastString
import GHC.Core.TyCo.Rep
import GHC.Core.TyCo.FVs
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])
tidyFreeTyCoVarsX TidyEnv
tidy_env [TyCoVar]
tyvars)
tidyFreeTyCoVarsX :: TidyEnv -> [TyCoVar] -> (TidyEnv, [TyCoVar])
tidyFreeTyCoVarsX :: TidyEnv -> [TyCoVar] -> (TidyEnv, [TyCoVar])
tidyFreeTyCoVarsX 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)
tidyFreeTyCoVarX TidyEnv
env ([TyCoVar] -> (TidyEnv, [TyCoVar]))
-> [TyCoVar] -> (TidyEnv, [TyCoVar])
forall a b. (a -> b) -> a -> b
$
[TyCoVar] -> [TyCoVar]
scopedSort [TyCoVar]
tyvars
tidyFreeTyCoVarX :: TidyEnv -> TyCoVar -> (TidyEnv, TyCoVar)
tidyFreeTyCoVarX :: TidyEnv -> TyCoVar -> (TidyEnv, TyCoVar)
tidyFreeTyCoVarX 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 -> 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
tcv
= case VarEnv TyCoVar -> TyCoVar -> Maybe TyCoVar
forall a. VarEnv a -> TyCoVar -> Maybe a
lookupVarEnv VarEnv TyCoVar
subst TyCoVar
tcv of
Maybe TyCoVar
Nothing -> (Type -> Type) -> TyCoVar -> TyCoVar
updateVarType (TidyEnv -> Type -> Type
tidyType TidyEnv
env) TyCoVar
tcv
Just TyCoVar
tcv' -> TyCoVar
tcv'
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 (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)
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{})) = TidyEnv -> Type -> Type
tidyForAllType TidyEnv
env Type
ty
tidyForAllType :: TidyEnv -> Type -> Type
tidyForAllType :: TidyEnv -> Type -> Type
tidyForAllType TidyEnv
env Type
ty
= ([(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]
tcvs' [ForAllTyFlag]
vis)) (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$! TidyEnv -> Type -> Type
tidyType TidyEnv
body_env Type
body_ty
where
([TyCoVar]
tcvs, [ForAllTyFlag]
vis, Type
body_ty) = Type -> ([TyCoVar], [ForAllTyFlag], Type)
splitForAllTyCoVars' Type
ty
(TidyEnv
body_env, [TyCoVar]
tcvs') = TidyEnv -> [TyCoVar] -> (TidyEnv, [TyCoVar])
tidyVarBndrs TidyEnv
env [TyCoVar]
tcvs
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)
tidyAvoiding :: [OccName]
-> (TidyEnv -> a -> TidyEnv)
-> a -> TidyEnv
tidyAvoiding :: forall a. [OccName] -> (TidyEnv -> a -> TidyEnv) -> a -> TidyEnv
tidyAvoiding [OccName]
bound_var_avoids TidyEnv -> a -> TidyEnv
do_tidy a
thing
= (TidyOccEnv
occs' TidyOccEnv -> [OccName] -> TidyOccEnv
`delTidyOccEnvList` [OccName]
bound_var_avoids, VarEnv TyCoVar
vars')
where
(TidyOccEnv
occs', VarEnv TyCoVar
vars') = TidyEnv -> a -> TidyEnv
do_tidy TidyEnv
init_tidy_env a
thing
init_tidy_env :: TidyEnv
init_tidy_env = TidyOccEnv -> TidyEnv
mkEmptyTidyEnv ([OccName] -> TidyOccEnv
initTidyOccEnv [OccName]
bound_var_avoids)
trimTidyEnv :: TidyEnv -> [TyCoVar] -> TidyEnv
trimTidyEnv :: TidyEnv -> [TyCoVar] -> TidyEnv
trimTidyEnv (TidyOccEnv
occ_env, VarEnv TyCoVar
var_env) [TyCoVar]
tcvs
= (TidyOccEnv -> [OccName] -> TidyOccEnv
trimTidyOccEnv TidyOccEnv
occ_env ((TyCoVar -> OccName) -> [TyCoVar] -> [OccName]
forall a b. (a -> b) -> [a] -> [b]
map TyCoVar -> OccName
forall a. NamedThing a => a -> OccName
getOccName [TyCoVar]
tcvs), VarEnv TyCoVar
var_env)
tidyOpenTypesX :: TidyEnv -> [Type] -> (TidyEnv, [Type])
tidyOpenTypesX :: TidyEnv -> [Type] -> (TidyEnv, [Type])
tidyOpenTypesX TidyEnv
env [Type]
tys
= (TidyEnv
env1, TidyEnv -> [Type] -> [Type]
tidyTypes TidyEnv
inner_env [Type]
tys)
where
free_tcvs :: [TyCoVar]
free_tcvs :: [TyCoVar]
free_tcvs = [Type] -> [TyCoVar]
tyCoVarsOfTypesList [Type]
tys
(TidyEnv
env1, [TyCoVar]
free_tcvs') = TidyEnv -> [TyCoVar] -> (TidyEnv, [TyCoVar])
tidyFreeTyCoVarsX TidyEnv
env [TyCoVar]
free_tcvs
inner_env :: TidyEnv
inner_env = TidyEnv -> [TyCoVar] -> TidyEnv
trimTidyEnv TidyEnv
env1 [TyCoVar]
free_tcvs'
tidyOpenTypeX :: TidyEnv -> Type -> (TidyEnv, Type)
tidyOpenTypeX :: TidyEnv -> Type -> (TidyEnv, Type)
tidyOpenTypeX TidyEnv
env Type
ty
= (TidyEnv
env1, TidyEnv -> Type -> Type
tidyType TidyEnv
inner_env Type
ty)
where
free_tcvs :: [TyCoVar]
free_tcvs = Type -> [TyCoVar]
tyCoVarsOfTypeList Type
ty
(TidyEnv
env1, [TyCoVar]
free_tcvs') = TidyEnv -> [TyCoVar] -> (TidyEnv, [TyCoVar])
tidyFreeTyCoVarsX TidyEnv
env [TyCoVar]
free_tcvs
inner_env :: TidyEnv
inner_env = TidyEnv -> [TyCoVar] -> TidyEnv
trimTidyEnv TidyEnv
env1 [TyCoVar]
free_tcvs'
tidyOpenTypes :: TidyEnv -> [Type] -> [Type]
tidyOpenTypes :: TidyEnv -> [Type] -> [Type]
tidyOpenTypes TidyEnv
env [Type]
ty = (TidyEnv, [Type]) -> [Type]
forall a b. (a, b) -> b
snd (TidyEnv -> [Type] -> (TidyEnv, [Type])
tidyOpenTypesX TidyEnv
env [Type]
ty)
tidyOpenType :: TidyEnv -> Type -> Type
tidyOpenType :: TidyEnv -> Type -> Type
tidyOpenType TidyEnv
env Type
ty = (TidyEnv, Type) -> Type
forall a b. (a, b) -> b
snd (TidyEnv -> Type -> (TidyEnv, Type)
tidyOpenTypeX 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 TidyEnv
env 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 ForAllTyFlag
visL ForAllTyFlag
visR KindCoercion
h KindCoercion
co)
= ((((TyCoVar
-> ForAllTyFlag
-> ForAllTyFlag
-> KindCoercion
-> KindCoercion
-> KindCoercion
ForAllCo (TyCoVar
-> ForAllTyFlag
-> ForAllTyFlag
-> KindCoercion
-> KindCoercion
-> KindCoercion)
-> TyCoVar
-> ForAllTyFlag
-> ForAllTyFlag
-> KindCoercion
-> KindCoercion
-> KindCoercion
forall a b. (a -> b) -> a -> b
$! TyCoVar
tvp) (ForAllTyFlag
-> ForAllTyFlag -> KindCoercion -> KindCoercion -> KindCoercion)
-> ForAllTyFlag
-> ForAllTyFlag
-> KindCoercion
-> KindCoercion
-> KindCoercion
forall a b. (a -> b) -> a -> b
$! ForAllTyFlag
visL) (ForAllTyFlag -> KindCoercion -> KindCoercion -> KindCoercion)
-> ForAllTyFlag -> KindCoercion -> KindCoercion -> KindCoercion
forall a b. (a -> b) -> a -> b
$! ForAllTyFlag
visR) (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) = TyCoVar -> KindCoercion
CoVarCo (TyCoVar -> KindCoercion) -> TyCoVar -> KindCoercion
forall a b. (a -> b) -> a -> b
$! TyCoVar -> TyCoVar
go_cv TyCoVar
cv
go (HoleCo CoercionHole
h) = CoercionHole -> KindCoercion
HoleCo (CoercionHole -> KindCoercion) -> CoercionHole -> KindCoercion
forall a b. (a -> b) -> a -> b
$! CoercionHole -> CoercionHole
go_hole CoercionHole
h
go (AxiomCo CoAxiomRule
ax [KindCoercion]
cos) = CoAxiomRule -> [KindCoercion] -> KindCoercion
AxiomCo 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 (UnivCo UnivCoProvenance
prov Role
role Type
t1 Type
t2 [KindCoercion]
cos)
= ((UnivCoProvenance
-> Role -> Type -> Type -> [KindCoercion] -> KindCoercion
UnivCo UnivCoProvenance
prov Role
role
(Type -> Type -> [KindCoercion] -> KindCoercion)
-> Type -> Type -> [KindCoercion] -> KindCoercion
forall a b. (a -> b) -> a -> b
$! TidyEnv -> Type -> Type
tidyType TidyEnv
env Type
t1)
(Type -> [KindCoercion] -> KindCoercion)
-> Type -> [KindCoercion] -> KindCoercion
forall a b. (a -> b) -> a -> b
$! TidyEnv -> Type -> Type
tidyType TidyEnv
env Type
t2)
([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 (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_cv :: TyCoVar -> TyCoVar
go_cv TyCoVar
cv = TidyEnv -> TyCoVar -> TyCoVar
tidyTyCoVarOcc TidyEnv
env TyCoVar
cv
go_hole :: CoercionHole -> CoercionHole
go_hole (CoercionHole TyCoVar
cv IORef (Maybe KindCoercion)
r Bool
h) = (TyCoVar -> IORef (Maybe KindCoercion) -> Bool -> CoercionHole
CoercionHole (TyCoVar -> IORef (Maybe KindCoercion) -> Bool -> CoercionHole)
-> TyCoVar -> IORef (Maybe KindCoercion) -> Bool -> CoercionHole
forall a b. (a -> b) -> a -> b
$! TyCoVar -> TyCoVar
go_cv TyCoVar
cv) IORef (Maybe KindCoercion)
r Bool
h
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)