{-# LANGUAGE BangPatterns #-}
{-# 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,
        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)

{-
%************************************************************************
%*                                                                      *
\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.Name.Occurrence
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
  = 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
-- ^ 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'

---------------

{-
Note [Strictness in tidyType and friends]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

Since the result of tidying will be inserted into the HPT, a potentially
long-lived structure, we generally want to avoid pieces of the old AST
being retained by the thunks produced by tidying.

For this reason we take great care to ensure that all pieces of the tidied AST
are evaluated strictly.  So you will see lots of strict applications ($!) and
uses of `strictMap` in `tidyType`, `tidyTypes` and `tidyCo`.

In the case of tidying of lists (e.g. lists of arguments) we prefer to use
`strictMap f xs` rather than `seqList (map f xs)` as the latter will
unnecessarily allocate a thunk, which will then be almost-immediately
evaluated, for each list element.

Making `tidyType` strict has a rather large effect on performance: see #14738.
Sometimes as much as a 5% reduction in allocation.
-}

-- | Tidy a list of Types
--
-- See Note [Strictness in tidyType and friends]
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

---------------


-- | Tidy a Type
--
-- See Note [Strictness in tidyType and friends]
tidyType :: TidyEnv -> Type -> Type
tidyType :: TidyEnv -> Type -> Type
tidyType TidyEnv
_   t :: Type
t@(LitTy {})          = Type
t -- Preserve sharing
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 -- Preserve sharing if possible
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)


-- The following two functions differ from mkForAllTys and splitForAllTyCoVars in that
-- they expect/preserve the ForAllTyFlag argument. These belong to "GHC.Core.Type", but
-- how should they be named?
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)


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

---------------

-- | Tidy a Coercion
--
-- See Note [Strictness in tidyType and friends]
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
            -- 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 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)