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

    {- **********************************************************************

                      TidyType

    ********************************************************************** -}

    {- Note [Tidying open types]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    When tidying some open types [t1,..,tn], we find their free vars, and tidy them first.

    But (tricky point) we restrict the occ_env part of inner_env to just the /free/
    vars of [t1..tn], so that we don't gratuitously rename the /bound/ variables.

    Example: assume the TidyEnv
          ({"a1","b"} , [a_4 :-> a1, b_7 :-> b])
    and call tidyOpenTypes on
          [a_1, forall a_2. Maybe (a_2,a_4), forall b. (b,a_1)]
    All the a's have the same OccName, but different uniques.

    The TidyOccEnv binding for "b" relates b_7, which doesn't appear free in the
    these types at all, so we don't want that to mess up the tidying for the
    (forall b...).

    So we proceed as follows:
      1. Find the free vars.
         In our example:the free vars are a_1 and a_4:

      2. Use tidyFreeTyCoVars to tidy them (workhorse: `tidyFreeCoVarX`)
         In our example:
          * a_4 already has a tidy form, a1, so don't change that
          * a_1 gets tidied to a2

      3. Trim the TidyOccEnv to OccNames of the tidied free vars (`trimTidyEnv`)
         In our example "a1" and "a2"

      4. Now tidy the types.  In our example we get
          [a2, forall a3. Maybe (a3,a1), forall b. (b, a2)]

    Note [Tidying is idempotent]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    Key invariant: tidyFreeTyCoVars is idempotent, at least if you start with
    an empty TidyEnv. This is important because:

      * The typechecker error message processing carefully tidies types, using
        global knowledge; see for example calls to `tidyCt` in GHC.Tc.Errors.

      * Then the type pretty-printer, GHC.Core.TyCo.Ppr.pprType tidies the type
        again, because that's important for pretty-printing types in general.

    But the second tidying is a no-op if the first step has happened, because
    all the free vars will have distinct OccNames, so no renaming needs to happen.

    Note [tidyAvoiding]
    ~~~~~~~~~~~~~~~~~~~
    Consider tidying this unsolved constraint in GHC.Tc.Errors.report_unsolved.
        C a_33, (forall a. Eq a => D a)
    Here a_33 is a free unification variable.  If we firs tidy [a_33 :-> "a"]
    then we have no choice but to tidy the `forall a` to something else. But it
    is confusing (sometimes very confusing) to gratuitously rename skolems in
    this way -- see #24868.  So it is better to :

      * Find the /bound/ skolems (just `a` in this case)
      * Initialise the TidyOccEnv to avoid using "a"
      * Now tidy the free a_33 to, say, "a1"
      * Delete "a" from the TidyOccEnv

    This is done by `tidyAvoiding`.

    The last step is very important; if we leave "a" in the TidyOccEnv, when
    we get to the (forall a. blah) we'll rename `a` to "a2", avoiding "a".
    -}

    -- | 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
    -- Precondition: input free vars are closed over kinds and
    -- This function does a scopedSort, so that tidied variables
    -- have tidied kinds.
    -- See Note [Tidying is idempotent]
    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])
    -- Precondition: input free vars are closed over kinds and
    -- This function does a scopedSort, so that tidied variables
    -- have tidied kinds.
    -- See Note [Tidying is idempotent]
    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)
    -- ^ 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'
    -- See Note [Tidying is idempotent]
    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')           -- Already substituted
            Maybe TyCoVar
    Nothing     -> 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
    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'

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

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

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

    ---------------
    tidyAvoiding :: [OccName]
                 -> (TidyEnv -> a -> TidyEnv)
                 -> a -> TidyEnv
    -- Initialise an empty TidyEnv with some bound vars to avoid,
    -- run the do_tidy function, and then remove the bound vars again.
    -- See Note [tidyAvoiding]
    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)

    ---------------
    -- | Grabs the free type variables, tidies them
    -- and then uses 'tidyType' to work over the type itself
    tidyOpenTypesX :: TidyEnv -> [Type] -> (TidyEnv, [Type])
    -- See Note [Tidying open types]
    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] -- Closed over kinds
        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)
    -- See Note [Tidying open types]
    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)

    ---------------
    -- | 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 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
                -- 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)          = 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 co :: KindCoercion
    co@(UnivCo { uco_lty :: KindCoercion -> Type
    uco_lty  = Type
    t1, uco_rty :: KindCoercion -> Type
    uco_rty = Type
    t2 })
                                 = KindCoercion
    co { uco_lty = tidyType env t1, uco_rty = tidyType env t2 }
                                   -- Don't bother to tidy the uco_deps field
        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
        -- Tidy even the holes; tidied types should have tidied kinds

    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)