{-# LANGUAGE BangPatterns #-}
{-# OPTIONS_GHC -Wno-incomplete-record-updates #-}
{-# OPTIONS_GHC -Wno-incomplete-uni-patterns   #-}

-- | Tidying types and coercions for printing in error messages.
module GHC.Core.TyCo.Tidy
  (
        -- * Tidying type related things up for printing
        tidyType,      tidyTypes,
        tidyOpenType,  tidyOpenTypes,
        tidyOpenKind,
        tidyVarBndr, tidyVarBndrs, tidyFreeTyCoVars, avoidNameClashes,
        tidyOpenTyCoVar, tidyOpenTyCoVars,
        tidyTyCoVarOcc,
        tidyTopType,
        tidyKind,
        tidyCo, tidyCos,
        tidyTyCoVarBinder, tidyTyCoVarBinders
  ) where

import GHC.Prelude

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 (seqList)

import Data.List (mapAccumL)

{-
%************************************************************************
%*                                                                      *
\subsection{TidyType}
%*                                                                      *
%************************************************************************
-}

-- | This tidies up a type for printing in an error message, or in
-- an interface file.
--
-- It doesn't change the uniques at all, just the print names.
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
-- Seed the occ_env with clashes among the names, see
-- Note [Tidying multiple names at once] in GHC.Types.Names.OccName
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
-- A TcTyVar with a System Name is probably a
-- unification variable; when we tidy them we give them a trailing
-- "0" (or 1 etc) so that they don't take precedence for the
-- un-modified name. Plus, indicating a unification variable in
-- this way is a helpful clue for users
getHelpfulOccName :: TyCoVar -> OccName
getHelpfulOccName TyCoVar
tv
  | Name -> Bool
isSystemName Name
name, TyCoVar -> Bool
isTcTyVar TyCoVar
tv
  = String -> OccName
mkTyVarOcc (OccName -> String
occNameString OccName
occ String -> String -> String
forall a. [a] -> [a] -> [a]
++ 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

tidyTyCoVarBinder :: TidyEnv -> VarBndr TyCoVar vis
                  -> (TidyEnv, VarBndr TyCoVar vis)
tidyTyCoVarBinder :: forall vis.
TidyEnv -> VarBndr TyCoVar vis -> (TidyEnv, VarBndr TyCoVar vis)
tidyTyCoVarBinder 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

tidyTyCoVarBinders :: TidyEnv -> [VarBndr TyCoVar vis]
                   -> (TidyEnv, [VarBndr TyCoVar vis])
tidyTyCoVarBinders :: forall vis.
TidyEnv
-> [VarBndr TyCoVar vis] -> (TidyEnv, [VarBndr TyCoVar vis])
tidyTyCoVarBinders 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)
tidyTyCoVarBinder
              ([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
-- ^ Add the free 'TyVar's to the env in tidy form,
-- so that we can tidy the type they are free in
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)
-- ^ Treat a new 'TyCoVar' as a binder, and give it a fresh tidy name
-- using the environment if one has not already been allocated. See
-- also 'tidyVarBndr'
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')              -- Already substituted
        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  -- Treat it as a binder

---------------
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]
map (TidyEnv -> Type -> Type
tidyType TidyEnv
env) [Type]
tys

---------------
tidyType :: TidyEnv -> Type -> Type
tidyType :: TidyEnv -> Type -> Type
tidyType TidyEnv
_   (LitTy TyLit
n)             = TyLit -> Type
LitTy TyLit
n
tidyType TidyEnv
env (TyVarTy TyCoVar
tv)          = TyCoVar -> Type
TyVarTy (TidyEnv -> TyCoVar -> TyCoVar
tidyTyCoVarOcc TidyEnv
env TyCoVar
tv)
tidyType TidyEnv
env (TyConApp TyCon
tycon [Type]
tys)  = let args :: [Type]
args = TidyEnv -> [Type] -> [Type]
tidyTypes TidyEnv
env [Type]
tys
                                     in [Type]
args [Type] -> Type -> Type
forall a b. [a] -> b -> b
`seqList` TyCon -> [Type] -> Type
TyConApp TyCon
tycon [Type]
args
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 AnonArgFlag
_ 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 :: Type
ft_mult = Type
w', ft_arg :: Type
ft_arg = Type
arg', ft_res :: Type
ft_res = Type
res' }
tidyType TidyEnv
env (ty :: Type
ty@(ForAllTy{}))     = [(TyCoVar, ArgFlag)] -> Type -> Type
mkForAllTys' ([TyCoVar] -> [ArgFlag] -> [(TyCoVar, ArgFlag)]
forall a b. [a] -> [b] -> [(a, b)]
zip [TyCoVar]
tvs' [ArgFlag]
vis) (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$! TidyEnv -> Type -> Type
tidyType TidyEnv
env' Type
body_ty
  where
    ([TyCoVar]
tvs, [ArgFlag]
vis, Type
body_ty) = Type -> ([TyCoVar], [ArgFlag], Type)
splitForAllTys' 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)


-- The following two functions differ from mkForAllTys and splitForAllTys in that
-- they expect/preserve the ArgFlag argument. These belong to "GHC.Core.Type", but
-- how should they be named?
mkForAllTys' :: [(TyCoVar, ArgFlag)] -> Type -> Type
mkForAllTys' :: [(TyCoVar, ArgFlag)] -> Type -> Type
mkForAllTys' [(TyCoVar, ArgFlag)]
tvvs Type
ty = ((TyCoVar, ArgFlag) -> Type -> Type)
-> Type -> [(TyCoVar, ArgFlag)] -> Type
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (TyCoVar, ArgFlag) -> Type -> Type
strictMkForAllTy Type
ty [(TyCoVar, ArgFlag)]
tvvs
  where
    strictMkForAllTy :: (TyCoVar, ArgFlag) -> Type -> Type
strictMkForAllTy (TyCoVar
tv,ArgFlag
vis) Type
ty = (TyCoVarBinder -> Type -> Type
ForAllTy (TyCoVarBinder -> Type -> Type) -> TyCoVarBinder -> Type -> Type
forall a b. (a -> b) -> a -> b
$! ((TyCoVar -> ArgFlag -> TyCoVarBinder
forall var argf. var -> argf -> VarBndr var argf
Bndr (TyCoVar -> ArgFlag -> TyCoVarBinder)
-> TyCoVar -> ArgFlag -> TyCoVarBinder
forall a b. (a -> b) -> a -> b
$! TyCoVar
tv) (ArgFlag -> TyCoVarBinder) -> ArgFlag -> TyCoVarBinder
forall a b. (a -> b) -> a -> b
$! ArgFlag
vis)) (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$! Type
ty

splitForAllTys' :: Type -> ([TyCoVar], [ArgFlag], Type)
splitForAllTys' :: Type -> ([TyCoVar], [ArgFlag], Type)
splitForAllTys' Type
ty = Type -> [TyCoVar] -> [ArgFlag] -> ([TyCoVar], [ArgFlag], Type)
go Type
ty [] []
  where
    go :: Type -> [TyCoVar] -> [ArgFlag] -> ([TyCoVar], [ArgFlag], Type)
go (ForAllTy (Bndr TyCoVar
tv ArgFlag
vis) Type
ty) [TyCoVar]
tvs [ArgFlag]
viss = Type -> [TyCoVar] -> [ArgFlag] -> ([TyCoVar], [ArgFlag], Type)
go Type
ty (TyCoVar
tvTyCoVar -> [TyCoVar] -> [TyCoVar]
forall a. a -> [a] -> [a]
:[TyCoVar]
tvs) (ArgFlag
visArgFlag -> [ArgFlag] -> [ArgFlag]
forall a. a -> [a] -> [a]
:[ArgFlag]
viss)
    go Type
ty                          [TyCoVar]
tvs [ArgFlag]
viss = ([TyCoVar] -> [TyCoVar]
forall a. [a] -> [a]
reverse [TyCoVar]
tvs, [ArgFlag] -> [ArgFlag]
forall a. [a] -> [a]
reverse [ArgFlag]
viss, Type
ty)


---------------
-- | Grabs the free type variables, tidies them
-- and then uses 'tidyType' to work over the type itself
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')
      -- The idea here was that we restrict the new TidyEnv to the
      -- _free_ vars of the types, so that we don't gratuitously rename
      -- the _bound_ variables of the types.

---------------
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')

---------------
-- | Calls 'tidyType' on a top-level type (i.e. with an empty tidying environment)
tidyTopType :: Type -> Type
tidyTopType :: Type -> Type
tidyTopType Type
ty = TidyEnv -> Type -> Type
tidyType TidyEnv
emptyTidyEnv Type
ty

---------------
tidyOpenKind :: TidyEnv -> Kind -> (TidyEnv, Kind)
tidyOpenKind :: TidyEnv -> Type -> (TidyEnv, Type)
tidyOpenKind = TidyEnv -> Type -> (TidyEnv, Type)
tidyOpenType

tidyKind :: TidyEnv -> Kind -> Kind
tidyKind :: TidyEnv -> Type -> Type
tidyKind = TidyEnv -> Type -> Type
tidyType

----------------
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 -> KindCoercion
go KindCoercion
co)

    go :: KindCoercion -> KindCoercion
go (Refl Type
ty)             = Type -> KindCoercion
Refl (TidyEnv -> Type -> Type
tidyType TidyEnv
env Type
ty)
    go (GRefl Role
r Type
ty MCoercion
mco)      = Role -> Type -> MCoercion -> KindCoercion
GRefl Role
r (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) = let args :: [KindCoercion]
args = (KindCoercion -> KindCoercion) -> [KindCoercion] -> [KindCoercion]
forall a b. (a -> b) -> [a] -> [b]
map KindCoercion -> KindCoercion
go [KindCoercion]
cos
                               in [KindCoercion]
args [KindCoercion] -> KindCoercion -> KindCoercion
forall a b. [a] -> b -> b
`seqList` Role -> TyCon -> [KindCoercion] -> KindCoercion
TyConAppCo Role
r TyCon
tc [KindCoercion]
args
    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
            -- the case above duplicates a bit of work in tidying h and the kind
            -- of tv. But the alternative is to use coercionKind, which seems worse.
    go (FunCo Role
r KindCoercion
w KindCoercion
co1 KindCoercion
co2)   = ((Role
-> KindCoercion -> KindCoercion -> KindCoercion -> KindCoercion
FunCo Role
r (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) = let args :: [KindCoercion]
args = (KindCoercion -> KindCoercion) -> [KindCoercion] -> [KindCoercion]
forall a b. (a -> b) -> [a] -> [b]
map KindCoercion -> KindCoercion
go [KindCoercion]
cos
                               in  [KindCoercion]
args [KindCoercion] -> KindCoercion -> KindCoercion
forall a b. [a] -> b -> b
`seqList` CoAxiom Branched -> BranchIndex -> [KindCoercion] -> KindCoercion
AxiomInstCo CoAxiom Branched
con BranchIndex
ind [KindCoercion]
args
    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 (NthCo Role
r BranchIndex
d KindCoercion
co)        = Role -> BranchIndex -> KindCoercion -> KindCoercion
NthCo Role
r BranchIndex
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)  = let cos1 :: [KindCoercion]
cos1 = TidyEnv -> [KindCoercion] -> [KindCoercion]
tidyCos TidyEnv
env [KindCoercion]
cos
                               in [KindCoercion]
cos1 [KindCoercion] -> KindCoercion -> KindCoercion
forall a b. [a] -> b -> b
`seqList` CoAxiomRule -> [KindCoercion] -> KindCoercion
AxiomRuleCo CoAxiomRule
ax [KindCoercion]
cos1

    go_prov :: UnivCoProvenance -> UnivCoProvenance
go_prov (PhantomProv KindCoercion
co)    = KindCoercion -> UnivCoProvenance
PhantomProv (KindCoercion -> KindCoercion
go KindCoercion
co)
    go_prov (ProofIrrelProv KindCoercion
co) = KindCoercion -> UnivCoProvenance
ProofIrrelProv (KindCoercion -> KindCoercion
go KindCoercion
co)
    go_prov p :: UnivCoProvenance
p@(PluginProv String
_)    = UnivCoProvenance
p
    go_prov p :: UnivCoProvenance
p@UnivCoProvenance
CorePrepProv      = UnivCoProvenance
p

tidyCos :: TidyEnv -> [Coercion] -> [Coercion]
tidyCos :: TidyEnv -> [KindCoercion] -> [KindCoercion]
tidyCos TidyEnv
env = (KindCoercion -> KindCoercion) -> [KindCoercion] -> [KindCoercion]
forall a b. (a -> b) -> [a] -> [b]
map (TidyEnv -> KindCoercion -> KindCoercion
tidyCo TidyEnv
env)