    {-# LANGUAGE MultiWayIf #-}

    module GHC.Core.TyCo.FVs
      (     shallowTyCoVarsOfType, shallowTyCoVarsOfTypes,
            tyCoVarsOfType,        tyCoVarsOfTypes,
            tyCoVarsOfTypeDSet, tyCoVarsOfTypesDSet,

            tyCoFVsBndr, tyCoFVsVarBndr, tyCoFVsVarBndrs,
            tyCoFVsOfType, tyCoVarsOfTypeList,
            tyCoFVsOfTypes, tyCoVarsOfTypesList,
            deepTcvFolder,

            shallowTyCoVarsOfTyVarEnv, shallowTyCoVarsOfCoVarEnv,

            shallowTyCoVarsOfCo, shallowTyCoVarsOfCos,
            tyCoVarsOfCo, tyCoVarsOfCos, tyCoVarsOfMCo,
            coVarsOfType, coVarsOfTypes,
            coVarsOfCo, coVarsOfCos,
            tyCoVarsOfCoDSet,
            tyCoFVsOfCo, tyCoFVsOfCos,
            tyCoVarsOfCoList,
            coVarsOfCoDSet, coVarsOfCosDSet,

            almostDevoidCoVarOfCo,

            -- Injective free vars
            injectiveVarsOfType, injectiveVarsOfTypes, isInjectiveInType,
            invisibleVarsOfType, invisibleVarsOfTypes,

            -- Any and No Free vars
            anyFreeVarsOfType, anyFreeVarsOfTypes, anyFreeVarsOfCo,
            noFreeVarsOfType, noFreeVarsOfTypes, noFreeVarsOfCo,

            -- * Free type constructors
            tyConsOfType, tyConsOfTypes,

            -- * Free vars with visible/invisible separate
            visVarsOfTypes, visVarsOfType,

            -- * Occurrence-check expansion
            occCheckExpand,

            -- * Well-scoped free variables
            scopedSort, tyCoVarsOfTypeWellScoped,
            tyCoVarsOfTypesWellScoped,

            -- * Closing over kinds
            closeOverKindsDSet, closeOverKindsList,
            closeOverKinds,

            -- * Raw materials
            Endo(..), runTyCoVars
      ) where

    import GHC.Prelude

    import {-# SOURCE #-} GHC.Core.Type( partitionInvisibleTypes, coreView, rewriterView )
    import {-# SOURCE #-} GHC.Core.Coercion( coercionLKind )

    import GHC.Builtin.Types.Prim( funTyFlagTyCon )

    import Data.Monoid as DM ( Any(..) )
    import GHC.Core.TyCo.Rep
    import GHC.Core.TyCon
    import GHC.Core.Coercion.Axiom( CoAxiomRule(..), BuiltInFamRewrite(..), coAxiomTyCon )
    import GHC.Utils.FV

    import GHC.Types.Var
    import GHC.Types.Unique.FM
    import GHC.Types.Unique.Set

    import GHC.Types.Var.Set
    import GHC.Types.Var.Env
    import GHC.Utils.Misc
    import GHC.Utils.Panic
    import GHC.Data.Pair

    import Data.Semigroup

    {-
    %************************************************************************
    %*                                                                      *
                     Free variables of types and coercions
    %*                                                                      *
    %************************************************************************
    -}

    {- Note [Shallow and deep free variables]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    Definitions

    * Shallow free variables of a type: the variables
      affected by substitution. Specifically, the (TyVarTy tv)
      and (CoVar cv) that appear
        - In the type and coercions appearing in the type
        - In shallow free variables of the kind of a Forall binder
      but NOT in the kind of the /occurrences/ of a type variable.

    * Deep free variables of a type: shallow free variables, plus
      the deep free variables of the kinds of those variables.
      That is,  deepFVs( t ) = closeOverKinds( shallowFVs( t ) )

    Examples:

      Type                     Shallow     Deep
      ---------------------------------
      (a : (k:Type))           {a}        {a,k}
      forall (a:(k:Type)). a   {k}        {k}
      (a:k->Type) (b:k)        {a,b}      {a,b,k}
    -}

    {- Note [Free variables of types]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    The family of functions tyCoVarsOfType, tyCoVarsOfTypes etc, returns
    a VarSet that is closed over the types of its variables.  More precisely,
      if    S = tyCoVarsOfType( t )
      and   (a:k) is in S
      then  tyCoVarsOftype( k ) is a subset of S

    Example: The tyCoVars of this ((a:* -> k) Int) is {a, k}.

    We could /not/ close over the kinds of the variable occurrences, and
    instead do so at call sites, but it seems that we always want to do
    so, so it's easiest to do it here.

    It turns out that getting the free variables of types is performance critical,
    so we profiled several versions, exploring different implementation strategies.

    1. Baseline version: uses FV naively. Essentially:

       tyCoVarsOfType ty = fvVarSet $ tyCoFVsOfType ty

       This is not nice, because FV introduces some overhead to implement
       determinism, and through its "interesting var" function, neither of which
       we need here, so they are a complete waste.

    2. UnionVarSet version: instead of reusing the FV-based code, we simply used
       VarSets directly, trying to avoid the overhead of FV. E.g.:

       -- FV version:
       tyCoFVsOfType (AppTy fun arg)    a b c = (tyCoFVsOfType fun `unionFV` tyCoFVsOfType arg) a b c

       -- UnionVarSet version:
       tyCoVarsOfType (AppTy fun arg)    = (tyCoVarsOfType fun `unionVarSet` tyCoVarsOfType arg)

       This looks deceptively similar, but while FV internally builds a list- and
       set-generating function, the VarSet functions manipulate sets directly, and
       the latter performs a lot worse than the naive FV version.

    3. Accumulator-style VarSet version: this is what we use now. We do use VarSet
       as our data structure, but delegate the actual work to a new
       ty_co_vars_of_...  family of functions, which use accumulator style and the
       "in-scope set" filter found in the internals of FV, but without the
       determinism overhead.

    See #14880.

    Note [Closing over free variable kinds]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    tyCoVarsOfType and tyCoFVsOfType, while traversing a type, will also close over
    free variable kinds. In previous GHC versions, this happened naively: whenever
    we would encounter an occurrence of a free type variable, we would close over
    its kind. This, however is wrong for two reasons (see #14880):

    1. Efficiency. If we have Proxy (a::k) -> Proxy (a::k) -> Proxy (a::k), then
       we don't want to have to traverse k more than once.

    2. Correctness. Imagine we have forall k. b -> k, where b has
       kind k, for some k bound in an outer scope. If we look at b's kind inside
       the forall, we'll collect that k is free and then remove k from the set of
       free variables. This is plain wrong. We must instead compute that b is free
       and then conclude that b's kind is free.

    An obvious first approach is to move the closing-over-kinds from the
    occurrences of a type variable to after finding the free vars - however, this
    turns out to introduce performance regressions, and isn't even entirely
    correct.

    In fact, it isn't even important *when* we close over kinds; what matters is
    that we handle each type var exactly once, and that we do it in the right
    context.

    So the next approach we tried was to use the "in-scope set" part of FV or the
    equivalent argument in the accumulator-style `ty_co_vars_of_type` function, to
    say "don't bother with variables we have already closed over". This should work
    fine in theory, but the code is complicated and doesn't perform well.

    But there is a simpler way, which is implemented here. Consider the two points
    above:

    1. Efficiency: we now have an accumulator, so the second time we encounter 'a',
       we'll ignore it, certainly not looking at its kind - this is why
       pre-checking set membership before inserting ends up not only being faster,
       but also being correct.

    2. Correctness: we have an "in-scope set" (I think we should call it it a
      "bound-var set"), specifying variables that are bound by a forall in the type
      we are traversing; we simply ignore these variables, certainly not looking at
      their kind.

    So now consider:

        forall k. b -> k

    where b :: k->Type is free; but of course, it's a different k! When looking at
    b -> k we'll have k in the bound-var set. So we'll ignore the k. But suppose
    this is our first encounter with b; we want the free vars of its kind. But we
    want to behave as if we took the free vars of its kind at the end; that is,
    with no bound vars in scope.

    So the solution is easy. The old code was this:

      ty_co_vars_of_type (TyVarTy v) is acc
        | v `elemVarSet` is  = acc
        | v `elemVarSet` acc = acc
        | otherwise          = ty_co_vars_of_type (tyVarKind v) is (extendVarSet acc v)

    Now all we need to do is take the free vars of tyVarKind v *with an empty
    bound-var set*, thus:

    ty_co_vars_of_type (TyVarTy v) is acc
      | v `elemVarSet` is  = acc
      | v `elemVarSet` acc = acc
      | otherwise          = ty_co_vars_of_type (tyVarKind v) emptyVarSet (extendVarSet acc v)
                                                              ^^^^^^^^^^^

    And that's it. This works because a variable is either bound or free. If it is bound,
    then we won't look at it at all. If it is free, then all the variables free in its
    kind are free -- regardless of whether some local variable has the same Unique.
    So if we're looking at a variable occurrence at all, then all variables in its
    kind are free.

    Note [Free vars and synonyms]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    When finding free variables we generally do not expand synonyms.  So given
       type T a = Int
    the type (T [b]) will return `b` as a free variable, even though expanding the
    synonym would get rid of it.  Expanding synonyms might lead to types that look
    ill-scoped; an alternative we have not explored.

    But see `occCheckExpand` in this module for a function that does, selectively,
    expand synonyms to reduce free-var occurences.
    -}

    {- *********************************************************************
    *                                                                      *
              Endo for free variables
    *                                                                      *
    ********************************************************************* -}

    {- Note [Accumulating parameter free variables]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    We can use foldType to build an accumulating-parameter version of a
    free-var finder, thus:

        fvs :: Type -> TyCoVarSet
        fvs ty = appEndo (foldType folder ty) emptyVarSet

    Recall that
        foldType :: TyCoFolder env a -> env -> Type -> a

        newtype Endo a = Endo (a -> a)   -- In Data.Monoid
        instance Monoid a => Monoid (Endo a) where
           (Endo f) `mappend` (Endo g) = Endo (f.g)

        appEndo :: Endo a -> a -> a
        appEndo (Endo f) x = f x

    So `mappend` for Endos is just function composition.

    It's very important that, after optimisation, we end up with
    * an arity-three function
    * that is strict in the accumulator

       fvs env (TyVarTy v) acc
          | v `elemVarSet` env = acc
          | v `elemVarSet` acc = acc
          | otherwise          = acc `extendVarSet` v
       fvs env (AppTy t1 t2)   = fvs env t1 (fvs env t2 acc)
       ...

    The "strict in the accumulator" part is to ensure that in the
    AppTy equation we don't build a thunk for (fvs env t2 acc).

    The optimiser does do all this, but not very robustly. It depends
    critically on the basic arity-2 function not being exported, so that
    all its calls are visibly to three arguments. This analysis is
    done by the Call Arity pass.

    TL;DR: check this regularly!
    -}

    runTyCoVars :: Endo TyCoVarSet -> TyCoVarSet
    {-# INLINE runTyCoVars #-}
    runTyCoVars :: Endo VarSet -> VarSet
    runTyCoVars Endo VarSet
    f = Endo VarSet -> VarSet -> VarSet
    forall a. Endo a -> a -> a
    appEndo Endo VarSet
    f VarSet
    emptyVarSet

    {- *********************************************************************
    *                                                                      *
              Deep free variables
              See Note [Shallow and deep free variables]
    *                                                                      *
    ********************************************************************* -}

    tyCoVarsOfType :: Type -> TyCoVarSet
    -- The "deep" TyCoVars of the the type
    tyCoVarsOfType :: Type -> VarSet
    tyCoVarsOfType Type
    ty = Endo VarSet -> VarSet
    runTyCoVars (Type -> Endo VarSet
    deep_ty Type
    ty)
    -- Alternative:
    --   tyCoVarsOfType ty = closeOverKinds (shallowTyCoVarsOfType ty)

    tyCoVarsOfTypes :: [Type] -> TyCoVarSet
    -- The "deep" TyCoVars of the the type
    tyCoVarsOfTypes :: [Type] -> VarSet
    tyCoVarsOfTypes [Type]
    tys = Endo VarSet -> VarSet
    runTyCoVars ([Type] -> Endo VarSet
    deep_tys [Type]
    tys)
    -- Alternative:
    --   tyCoVarsOfTypes tys = closeOverKinds (shallowTyCoVarsOfTypes tys)

    tyCoVarsOfCo :: Coercion -> TyCoVarSet
    -- The "deep" TyCoVars of the the coercion
    -- See Note [Free variables of types]
    tyCoVarsOfCo :: Coercion -> VarSet
    tyCoVarsOfCo Coercion
    co = Endo VarSet -> VarSet
    runTyCoVars (Coercion -> Endo VarSet
    deep_co Coercion
    co)

    tyCoVarsOfMCo :: MCoercion -> TyCoVarSet
    tyCoVarsOfMCo :: MCoercion -> VarSet
    tyCoVarsOfMCo MCoercion
    MRefl    = VarSet
    emptyVarSet
    tyCoVarsOfMCo (MCo Coercion
    co) = Coercion -> VarSet
    tyCoVarsOfCo Coercion
    co

    tyCoVarsOfCos :: [Coercion] -> TyCoVarSet
    tyCoVarsOfCos :: [Coercion] -> VarSet
    tyCoVarsOfCos [Coercion]
    cos = Endo VarSet -> VarSet
    runTyCoVars ([Coercion] -> Endo VarSet
    deep_cos [Coercion]
    cos)

    deep_ty  :: Type       -> Endo TyCoVarSet
    deep_tys :: [Type]     -> Endo TyCoVarSet
    deep_co  :: Coercion   -> Endo TyCoVarSet
    deep_cos :: [Coercion] -> Endo TyCoVarSet
    (Type -> Endo VarSet
    deep_ty, [Type] -> Endo VarSet
    deep_tys, Coercion -> Endo VarSet
    deep_co, [Coercion] -> Endo VarSet
    deep_cos) = TyCoFolder VarSet (Endo VarSet)
    -> VarSet
    -> (Type -> Endo VarSet, [Type] -> Endo VarSet,
        Coercion -> Endo VarSet, [Coercion] -> Endo VarSet)
    forall a env.
    Monoid a =>
    TyCoFolder env a
    -> env -> (Type -> a, [Type] -> a, Coercion -> a, [Coercion] -> a)
    foldTyCo TyCoFolder VarSet (Endo VarSet)
    deepTcvFolder VarSet
    emptyVarSet

    deepTcvFolder :: TyCoFolder TyCoVarSet (Endo TyCoVarSet)
    deepTcvFolder :: TyCoFolder VarSet (Endo VarSet)
    deepTcvFolder = TyCoFolder { tcf_view :: Type -> Maybe Type
    tcf_view = Type -> Maybe Type
    noView  -- See Note [Free vars and synonyms]
                               , tcf_tyvar :: VarSet -> Var -> Endo VarSet
    tcf_tyvar = VarSet -> Var -> Endo VarSet
    do_tcv, tcf_covar :: VarSet -> Var -> Endo VarSet
    tcf_covar = VarSet -> Var -> Endo VarSet
    do_tcv
                               , tcf_hole :: VarSet -> CoercionHole -> Endo VarSet
    tcf_hole  = VarSet -> CoercionHole -> Endo VarSet
    do_hole, tcf_tycobinder :: VarSet -> Var -> ForAllTyFlag -> VarSet
    tcf_tycobinder = VarSet -> Var -> ForAllTyFlag -> VarSet
    forall {p}. VarSet -> Var -> p -> VarSet
    do_bndr }
      where
        do_tcv :: VarSet -> Var -> Endo VarSet
    do_tcv VarSet
    is Var
    v = (VarSet -> VarSet) -> Endo VarSet
    forall a. (a -> a) -> Endo a
    Endo VarSet -> VarSet
    do_it
          where
            do_it :: VarSet -> VarSet
    do_it VarSet
    acc | Var
    v Var -> VarSet -> Bool
    `elemVarSet` VarSet
    is  = VarSet
    acc
                      | Var
    v Var -> VarSet -> Bool
    `elemVarSet` VarSet
    acc = VarSet
    acc
                      | Bool
    otherwise          = Endo VarSet -> VarSet -> VarSet
    forall a. Endo a -> a -> a
    appEndo (Type -> Endo VarSet
    deep_ty (Var -> Type
    varType Var
    v)) (VarSet -> VarSet) -> VarSet -> VarSet
    forall a b. (a -> b) -> a -> b
    $
                                             VarSet
    acc VarSet -> Var -> VarSet
    `extendVarSet` Var
    v

        do_bndr :: VarSet -> Var -> p -> VarSet
    do_bndr VarSet
    is Var
    tcv p
    _ = VarSet -> Var -> VarSet
    extendVarSet VarSet
    is Var
    tcv
        do_hole :: VarSet -> CoercionHole -> Endo VarSet
    do_hole VarSet
    is CoercionHole
    hole  = VarSet -> Var -> Endo VarSet
    do_tcv VarSet
    is (CoercionHole -> Var
    coHoleCoVar CoercionHole
    hole)
                           -- See Note [CoercionHoles and coercion free variables]
                           -- in GHC.Core.TyCo.Rep

    {- *********************************************************************
    *                                                                      *
              Shallow free variables
              See Note [Shallow and deep free variables]
    *                                                                      *
    ********************************************************************* -}

    shallowTyCoVarsOfType :: Type -> TyCoVarSet
    -- See Note [Free variables of types]
    shallowTyCoVarsOfType :: Type -> VarSet
    shallowTyCoVarsOfType Type
    ty = Endo VarSet -> VarSet
    runTyCoVars (Type -> Endo VarSet
    shallow_ty Type
    ty)

    shallowTyCoVarsOfTypes :: [Type] -> TyCoVarSet
    shallowTyCoVarsOfTypes :: [Type] -> VarSet
    shallowTyCoVarsOfTypes [Type]
    tys = Endo VarSet -> VarSet
    runTyCoVars ([Type] -> Endo VarSet
    shallow_tys [Type]
    tys)

    shallowTyCoVarsOfCo :: Coercion -> TyCoVarSet
    shallowTyCoVarsOfCo :: Coercion -> VarSet
    shallowTyCoVarsOfCo Coercion
    co = Endo VarSet -> VarSet
    runTyCoVars (Coercion -> Endo VarSet
    shallow_co Coercion
    co)

    shallowTyCoVarsOfCos :: [Coercion] -> TyCoVarSet
    shallowTyCoVarsOfCos :: [Coercion] -> VarSet
    shallowTyCoVarsOfCos [Coercion]
    cos = Endo VarSet -> VarSet
    runTyCoVars ([Coercion] -> Endo VarSet
    shallow_cos [Coercion]
    cos)

    -- | Returns free variables of types, including kind variables as
    -- a non-deterministic set. For type synonyms it does /not/ expand the
    -- synonym.
    shallowTyCoVarsOfTyVarEnv :: TyVarEnv Type -> TyCoVarSet
    -- See Note [Free variables of types]
    shallowTyCoVarsOfTyVarEnv :: TyVarEnv Type -> VarSet
    shallowTyCoVarsOfTyVarEnv TyVarEnv Type
    tys = [Type] -> VarSet
    shallowTyCoVarsOfTypes (TyVarEnv Type -> [Type]
    forall {k} (key :: k) elt. UniqFM key elt -> [elt]
    nonDetEltsUFM TyVarEnv Type
    tys)
      -- It's OK to use nonDetEltsUFM here because we immediately
      -- forget the ordering by returning a set

    shallowTyCoVarsOfCoVarEnv :: CoVarEnv Coercion -> TyCoVarSet
    shallowTyCoVarsOfCoVarEnv :: CoVarEnv Coercion -> VarSet
    shallowTyCoVarsOfCoVarEnv CoVarEnv Coercion
    cos = [Coercion] -> VarSet
    shallowTyCoVarsOfCos (CoVarEnv Coercion -> [Coercion]
    forall {k} (key :: k) elt. UniqFM key elt -> [elt]
    nonDetEltsUFM CoVarEnv Coercion
    cos)
      -- It's OK to use nonDetEltsUFM here because we immediately
      -- forget the ordering by returning a set

    shallow_ty  :: Type       -> Endo TyCoVarSet
    shallow_tys :: [Type]     -> Endo TyCoVarSet
    shallow_co  :: Coercion   -> Endo TyCoVarSet
    shallow_cos :: [Coercion] -> Endo TyCoVarSet
    (Type -> Endo VarSet
    shallow_ty, [Type] -> Endo VarSet
    shallow_tys, Coercion -> Endo VarSet
    shallow_co, [Coercion] -> Endo VarSet
    shallow_cos) = TyCoFolder VarSet (Endo VarSet)
    -> VarSet
    -> (Type -> Endo VarSet, [Type] -> Endo VarSet,
        Coercion -> Endo VarSet, [Coercion] -> Endo VarSet)
    forall a env.
    Monoid a =>
    TyCoFolder env a
    -> env -> (Type -> a, [Type] -> a, Coercion -> a, [Coercion] -> a)
    foldTyCo TyCoFolder VarSet (Endo VarSet)
    shallowTcvFolder VarSet
    emptyVarSet

    shallowTcvFolder :: TyCoFolder TyCoVarSet (Endo TyCoVarSet)
    shallowTcvFolder :: TyCoFolder VarSet (Endo VarSet)
    shallowTcvFolder = TyCoFolder { tcf_view :: Type -> Maybe Type
    tcf_view = Type -> Maybe Type
    noView  -- See Note [Free vars and synonyms]
                                  , tcf_tyvar :: VarSet -> Var -> Endo VarSet
    tcf_tyvar = VarSet -> Var -> Endo VarSet
    do_tcv, tcf_covar :: VarSet -> Var -> Endo VarSet
    tcf_covar = VarSet -> Var -> Endo VarSet
    do_tcv
                                  , tcf_hole :: VarSet -> CoercionHole -> Endo VarSet
    tcf_hole  = VarSet -> CoercionHole -> Endo VarSet
    forall {a} {p} {p}. Monoid a => p -> p -> a
    do_hole, tcf_tycobinder :: VarSet -> Var -> ForAllTyFlag -> VarSet
    tcf_tycobinder = VarSet -> Var -> ForAllTyFlag -> VarSet
    forall {p}. VarSet -> Var -> p -> VarSet
    do_bndr }
      where
        do_tcv :: VarSet -> Var -> Endo VarSet
    do_tcv VarSet
    is Var
    v = (VarSet -> VarSet) -> Endo VarSet
    forall a. (a -> a) -> Endo a
    Endo VarSet -> VarSet
    do_it
          where
            do_it :: VarSet -> VarSet
    do_it VarSet
    acc | Var
    v Var -> VarSet -> Bool
    `elemVarSet` VarSet
    is  = VarSet
    acc
                      | Var
    v Var -> VarSet -> Bool
    `elemVarSet` VarSet
    acc = VarSet
    acc
                      | Bool
    otherwise          = VarSet
    acc VarSet -> Var -> VarSet
    `extendVarSet` Var
    v

        do_bndr :: VarSet -> Var -> p -> VarSet
    do_bndr VarSet
    is Var
    tcv p
    _ = VarSet -> Var -> VarSet
    extendVarSet VarSet
    is Var
    tcv
        do_hole :: p -> p -> a
    do_hole p
    _ p
    _  = a
    forall a. Monoid a => a
    mempty   -- Ignore coercion holes

    {- *********************************************************************
    *                                                                      *
              Free coercion variables
    *                                                                      *
    ********************************************************************* -}

    {- Note [Finding free coercion variables]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    Here we are only interested in the free /coercion/ variables.
    We can achieve this through a slightly different TyCo folder.

    Notice that we look deeply, into kinds.

    See #14880.
    -}

    -- See Note [Finding free coercion variables]
    coVarsOfType  :: Type       -> CoVarSet
    coVarsOfTypes :: [Type]     -> CoVarSet
    coVarsOfCo    :: Coercion   -> CoVarSet
    coVarsOfCos   :: [Coercion] -> CoVarSet

    coVarsOfType :: Type -> VarSet
    coVarsOfType  Type
    ty  = Endo VarSet -> VarSet
    runTyCoVars (Type -> Endo VarSet
    deep_cv_ty Type
    ty)
    coVarsOfTypes :: [Type] -> VarSet
    coVarsOfTypes [Type]
    tys = Endo VarSet -> VarSet
    runTyCoVars ([Type] -> Endo VarSet
    deep_cv_tys [Type]
    tys)
    coVarsOfCo :: Coercion -> VarSet
    coVarsOfCo    Coercion
    co  = Endo VarSet -> VarSet
    runTyCoVars (Coercion -> Endo VarSet
    deep_cv_co Coercion
    co)
    coVarsOfCos :: [Coercion] -> VarSet
    coVarsOfCos   [Coercion]
    cos = Endo VarSet -> VarSet
    runTyCoVars ([Coercion] -> Endo VarSet
    deep_cv_cos [Coercion]
    cos)

    deep_cv_ty  :: Type       -> Endo CoVarSet
    deep_cv_tys :: [Type]     -> Endo CoVarSet
    deep_cv_co  :: Coercion   -> Endo CoVarSet
    deep_cv_cos :: [Coercion] -> Endo CoVarSet
    (Type -> Endo VarSet
    deep_cv_ty, [Type] -> Endo VarSet
    deep_cv_tys, Coercion -> Endo VarSet
    deep_cv_co, [Coercion] -> Endo VarSet
    deep_cv_cos) = TyCoFolder VarSet (Endo VarSet)
    -> VarSet
    -> (Type -> Endo VarSet, [Type] -> Endo VarSet,
        Coercion -> Endo VarSet, [Coercion] -> Endo VarSet)
    forall a env.
    Monoid a =>
    TyCoFolder env a
    -> env -> (Type -> a, [Type] -> a, Coercion -> a, [Coercion] -> a)
    foldTyCo TyCoFolder VarSet (Endo VarSet)
    deepCoVarFolder VarSet
    emptyVarSet

    deepCoVarFolder :: TyCoFolder TyCoVarSet (Endo CoVarSet)
    deepCoVarFolder :: TyCoFolder VarSet (Endo VarSet)
    deepCoVarFolder = TyCoFolder { tcf_view :: Type -> Maybe Type
    tcf_view = Type -> Maybe Type
    noView
                                 , tcf_tyvar :: VarSet -> Var -> Endo VarSet
    tcf_tyvar = VarSet -> Var -> Endo VarSet
    forall {a} {p} {p}. Monoid a => p -> p -> a
    do_tyvar, tcf_covar :: VarSet -> Var -> Endo VarSet
    tcf_covar = VarSet -> Var -> Endo VarSet
    do_covar
                                 , tcf_hole :: VarSet -> CoercionHole -> Endo VarSet
    tcf_hole  = VarSet -> CoercionHole -> Endo VarSet
    do_hole, tcf_tycobinder :: VarSet -> Var -> ForAllTyFlag -> VarSet
    tcf_tycobinder = VarSet -> Var -> ForAllTyFlag -> VarSet
    forall {p}. VarSet -> Var -> p -> VarSet
    do_bndr }
      where
        do_tyvar :: p -> p -> a
    do_tyvar p
    _ p
    _  = a
    forall a. Monoid a => a
    mempty
          -- This do_tyvar means we won't see any CoVars in this
          -- TyVar's kind.   This may be wrong; but it's the way it's
          -- always been.  And its awkward to change, because
          -- the tyvar won't end up in the accumulator, so
          -- we'd look repeatedly.  Blargh.

        do_covar :: VarSet -> Var -> Endo VarSet
    do_covar VarSet
    is Var
    v = (VarSet -> VarSet) -> Endo VarSet
    forall a. (a -> a) -> Endo a
    Endo VarSet -> VarSet
    do_it
          where
            do_it :: VarSet -> VarSet
    do_it VarSet
    acc | Var
    v Var -> VarSet -> Bool
    `elemVarSet` VarSet
    is  = VarSet
    acc
                      | Var
    v Var -> VarSet -> Bool
    `elemVarSet` VarSet
    acc = VarSet
    acc
                      | Bool
    otherwise          = Endo VarSet -> VarSet -> VarSet
    forall a. Endo a -> a -> a
    appEndo (Type -> Endo VarSet
    deep_cv_ty (Var -> Type
    varType Var
    v)) (VarSet -> VarSet) -> VarSet -> VarSet
    forall a b. (a -> b) -> a -> b
    $
                                             VarSet
    acc VarSet -> Var -> VarSet
    `extendVarSet` Var
    v

        do_bndr :: VarSet -> Var -> p -> VarSet
    do_bndr VarSet
    is Var
    tcv p
    _ = VarSet -> Var -> VarSet
    extendVarSet VarSet
    is Var
    tcv
        do_hole :: VarSet -> CoercionHole -> Endo VarSet
    do_hole VarSet
    is CoercionHole
    hole  = VarSet -> Var -> Endo VarSet
    do_covar VarSet
    is (CoercionHole -> Var
    coHoleCoVar CoercionHole
    hole)
                           -- See Note [CoercionHoles and coercion free variables]
                           -- in GHC.Core.TyCo.Rep

    ------- Same again, but for DCoVarSet ----------
    --    But this time the free vars are shallow

    coVarsOfCosDSet :: [Coercion] -> DCoVarSet
    coVarsOfCosDSet :: [Coercion] -> DCoVarSet
    coVarsOfCosDSet [Coercion]
    cos = InterestingVarFun -> FV -> DCoVarSet
    fvDVarSetSome InterestingVarFun
    isCoVar ([Coercion] -> FV
    tyCoFVsOfCos [Coercion]
    cos)

    coVarsOfCoDSet :: Coercion -> DCoVarSet
    coVarsOfCoDSet :: Coercion -> DCoVarSet
    coVarsOfCoDSet Coercion
    co = InterestingVarFun -> FV -> DCoVarSet
    fvDVarSetSome InterestingVarFun
    isCoVar (Coercion -> FV
    tyCoFVsOfCo Coercion
    co)

    {- *********************************************************************
    *                                                                      *
              Closing over kinds
    *                                                                      *
    ********************************************************************* -}

    ------------- Closing over kinds -----------------

    closeOverKinds :: TyCoVarSet -> TyCoVarSet
    -- For each element of the input set,
    -- add the deep free variables of its kind
    closeOverKinds :: VarSet -> VarSet
    closeOverKinds VarSet
    vs = (Var -> VarSet -> VarSet) -> VarSet -> VarSet -> VarSet
    forall a. (Var -> a -> a) -> a -> VarSet -> a
    nonDetStrictFoldVarSet Var -> VarSet -> VarSet
    do_one VarSet
    vs VarSet
    vs
      where
        do_one :: Var -> VarSet -> VarSet
    do_one Var
    v VarSet
    acc = Endo VarSet -> VarSet -> VarSet
    forall a. Endo a -> a -> a
    appEndo (Type -> Endo VarSet
    deep_ty (Var -> Type
    varType Var
    v)) VarSet
    acc

    {- --------------- Alternative version 1 (using FV) ------------
    closeOverKinds = fvVarSet . closeOverKindsFV . nonDetEltsUniqSet
    -}

    {- ---------------- Alternative version 2 -------------

    -- | Add the kind variables free in the kinds of the tyvars in the given set.
    -- Returns a non-deterministic set.
    closeOverKinds :: TyCoVarSet -> TyCoVarSet
    closeOverKinds vs
       = go vs vs
      where
        go :: VarSet   -- Work list
           -> VarSet   -- Accumulator, always a superset of wl
           -> VarSet
        go wl acc
          | isEmptyVarSet wl = acc
          | otherwise        = go wl_kvs (acc `unionVarSet` wl_kvs)
          where
            k v inner_acc = ty_co_vars_of_type (varType v) acc inner_acc
            wl_kvs = nonDetFoldVarSet k emptyVarSet wl
            -- wl_kvs = union of shallow free vars of the kinds of wl
            --          but don't bother to collect vars in acc

    -}

    {- ---------------- Alternative version 3 -------------
    -- | Add the kind variables free in the kinds of the tyvars in the given set.
    -- Returns a non-deterministic set.
    closeOverKinds :: TyVarSet -> TyVarSet
    closeOverKinds vs = close_over_kinds vs emptyVarSet

    close_over_kinds :: TyVarSet  -- Work list
                     -> TyVarSet  -- Accumulator
                     -> TyVarSet
    -- Precondition: in any call (close_over_kinds wl acc)
    --  for every tv in acc, the shallow kind-vars of tv
    --  are either in the work list wl, or in acc
    -- Postcondition: result is the deep free vars of (wl `union` acc)
    close_over_kinds wl acc
      = nonDetFoldVarSet do_one acc wl
      where
        do_one :: Var -> TyVarSet -> TyVarSet
        -- (do_one v acc) adds v and its deep free-vars to acc
        do_one v acc | v `elemVarSet` acc
                     = acc
                     | otherwise
                     = close_over_kinds (shallowTyCoVarsOfType (varType v)) $
                       acc `extendVarSet` v
    -}

    {- *********************************************************************
    *                                                                      *
              The FV versions return deterministic results
    *                                                                      *
    ********************************************************************* -}

    -- | Given a list of tyvars returns a deterministic FV computation that
    -- returns the given tyvars with the kind variables free in the kinds of the
    -- given tyvars.
    closeOverKindsFV :: [TyVar] -> FV
    closeOverKindsFV :: [Var] -> FV
    closeOverKindsFV [Var]
    tvs =
      (Var -> FV) -> [Var] -> FV
    forall a. (a -> FV) -> [a] -> FV
    mapUnionFV (Type -> FV
    tyCoFVsOfType (Type -> FV) -> (Var -> Type) -> Var -> FV
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Var -> Type
    tyVarKind) [Var]
    tvs FV -> FV -> FV
    `unionFV` [Var] -> FV
    mkFVs [Var]
    tvs

    -- | Add the kind variables free in the kinds of the tyvars in the given set.
    -- Returns a deterministically ordered list.
    closeOverKindsList :: [TyVar] -> [TyVar]
    closeOverKindsList :: [Var] -> [Var]
    closeOverKindsList [Var]
    tvs = FV -> [Var]
    fvVarList (FV -> [Var]) -> FV -> [Var]
    forall a b. (a -> b) -> a -> b
    $ [Var] -> FV
    closeOverKindsFV [Var]
    tvs

    -- | Add the kind variables free in the kinds of the tyvars in the given set.
    -- Returns a deterministic set.
    closeOverKindsDSet :: DTyVarSet -> DTyVarSet
    closeOverKindsDSet :: DCoVarSet -> DCoVarSet
    closeOverKindsDSet = FV -> DCoVarSet
    fvDVarSet (FV -> DCoVarSet) -> (DCoVarSet -> FV) -> DCoVarSet -> DCoVarSet
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Var] -> FV
    closeOverKindsFV ([Var] -> FV) -> (DCoVarSet -> [Var]) -> DCoVarSet -> FV
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . DCoVarSet -> [Var]
    dVarSetElems

    -- | `tyCoFVsOfType` that returns free variables of a type in a deterministic
    -- set. For explanation of why using `VarSet` is not deterministic see
    -- Note [Deterministic FV] in "GHC.Utils.FV".
    tyCoVarsOfTypeDSet :: Type -> DTyCoVarSet
    -- See Note [Free variables of types]
    tyCoVarsOfTypeDSet :: Type -> DCoVarSet
    tyCoVarsOfTypeDSet Type
    ty = FV -> DCoVarSet
    fvDVarSet (FV -> DCoVarSet) -> FV -> DCoVarSet
    forall a b. (a -> b) -> a -> b
    $ Type -> FV
    tyCoFVsOfType Type
    ty

    -- | `tyCoFVsOfType` that returns free variables of a type in deterministic
    -- order. For explanation of why using `VarSet` is not deterministic see
    -- Note [Deterministic FV] in "GHC.Utils.FV".
    tyCoVarsOfTypeList :: Type -> [TyCoVar]
    -- See Note [Free variables of types]
    tyCoVarsOfTypeList :: Type -> [Var]
    tyCoVarsOfTypeList Type
    ty = FV -> [Var]
    fvVarList (FV -> [Var]) -> FV -> [Var]
    forall a b. (a -> b) -> a -> b
    $ Type -> FV
    tyCoFVsOfType Type
    ty

    -- | Returns free variables of types, including kind variables as
    -- a deterministic set. For type synonyms it does /not/ expand the
    -- synonym.
    tyCoVarsOfTypesDSet :: [Type] -> DTyCoVarSet
    -- See Note [Free variables of types]
    tyCoVarsOfTypesDSet :: [Type] -> DCoVarSet
    tyCoVarsOfTypesDSet [Type]
    tys = FV -> DCoVarSet
    fvDVarSet (FV -> DCoVarSet) -> FV -> DCoVarSet
    forall a b. (a -> b) -> a -> b
    $ [Type] -> FV
    tyCoFVsOfTypes [Type]
    tys

    -- | Returns free variables of types, including kind variables as
    -- a deterministically ordered list. For type synonyms it does /not/ expand the
    -- synonym.
    tyCoVarsOfTypesList :: [Type] -> [TyCoVar]
    -- See Note [Free variables of types]
    tyCoVarsOfTypesList :: [Type] -> [Var]
    tyCoVarsOfTypesList [Type]
    tys = FV -> [Var]
    fvVarList (FV -> [Var]) -> FV -> [Var]
    forall a b. (a -> b) -> a -> b
    $ [Type] -> FV
    tyCoFVsOfTypes [Type]
    tys

    -- | The worker for `tyCoFVsOfType` and `tyCoFVsOfTypeList`.
    -- The previous implementation used `unionVarSet` which is O(n+m) and can
    -- make the function quadratic.
    -- It's exported, so that it can be composed with
    -- other functions that compute free variables.
    -- See Note [FV naming conventions] in "GHC.Utils.FV".
    --
    -- Eta-expanded because that makes it run faster (apparently)
    -- See Note [FV eta expansion] in "GHC.Utils.FV" for explanation.
    tyCoFVsOfType :: Type -> FV
    -- See Note [Free variables of types]
    tyCoFVsOfType :: Type -> FV
    tyCoFVsOfType (TyVarTy Var
    v)        InterestingVarFun
    f VarSet
    bound_vars ([Var]
    acc_list, VarSet
    acc_set)
      | Bool -> Bool
    not (InterestingVarFun
    f Var
    v) = ([Var]
    acc_list, VarSet
    acc_set)
      | Var
    v Var -> VarSet -> Bool
    `elemVarSet` VarSet
    bound_vars = ([Var]
    acc_list, VarSet
    acc_set)
      | Var
    v Var -> VarSet -> Bool
    `elemVarSet` VarSet
    acc_set = ([Var]
    acc_list, VarSet
    acc_set)
      | Bool
    otherwise = Type -> FV
    tyCoFVsOfType (Var -> Type
    tyVarKind Var
    v) InterestingVarFun
    f
                                   VarSet
    emptyVarSet   -- See Note [Closing over free variable kinds]
                                   (Var
    vVar -> [Var] -> [Var]
    forall a. a -> [a] -> [a]
    :[Var]
    acc_list, VarSet -> Var -> VarSet
    extendVarSet VarSet
    acc_set Var
    v)
    tyCoFVsOfType (TyConApp TyCon
    _ [Type]
    tys)   InterestingVarFun
    f VarSet
    bound_vars ([Var], VarSet)
    acc = [Type] -> FV
    tyCoFVsOfTypes [Type]
    tys InterestingVarFun
    f VarSet
    bound_vars ([Var], VarSet)
    acc
                                                        -- See Note [Free vars and synonyms]
    tyCoFVsOfType (LitTy {})         InterestingVarFun
    f VarSet
    bound_vars ([Var], VarSet)
    acc = FV
    emptyFV InterestingVarFun
    f VarSet
    bound_vars ([Var], VarSet)
    acc
    tyCoFVsOfType (AppTy Type
    fun Type
    arg)    InterestingVarFun
    f VarSet
    bound_vars ([Var], VarSet)
    acc = (Type -> FV
    tyCoFVsOfType Type
    fun FV -> FV -> FV
    `unionFV` Type -> FV
    tyCoFVsOfType Type
    arg) InterestingVarFun
    f VarSet
    bound_vars ([Var], VarSet)
    acc
    tyCoFVsOfType (FunTy FunTyFlag
    _ Type
    w Type
    arg Type
    res)  InterestingVarFun
    f VarSet
    bound_vars ([Var], VarSet)
    acc = (Type -> FV
    tyCoFVsOfType Type
    w FV -> FV -> FV
    `unionFV` Type -> FV
    tyCoFVsOfType Type
    arg FV -> FV -> FV
    `unionFV` Type -> FV
    tyCoFVsOfType Type
    res) InterestingVarFun
    f VarSet
    bound_vars ([Var], VarSet)
    acc
    tyCoFVsOfType (ForAllTy ForAllTyBinder
    bndr Type
    ty) InterestingVarFun
    f VarSet
    bound_vars ([Var], VarSet)
    acc = ForAllTyBinder -> FV -> FV
    tyCoFVsBndr ForAllTyBinder
    bndr (Type -> FV
    tyCoFVsOfType Type
    ty)  InterestingVarFun
    f VarSet
    bound_vars ([Var], VarSet)
    acc
    tyCoFVsOfType (CastTy Type
    ty Coercion
    co)     InterestingVarFun
    f VarSet
    bound_vars ([Var], VarSet)
    acc = (Type -> FV
    tyCoFVsOfType Type
    ty FV -> FV -> FV
    `unionFV` Coercion -> FV
    tyCoFVsOfCo Coercion
    co) InterestingVarFun
    f VarSet
    bound_vars ([Var], VarSet)
    acc
    tyCoFVsOfType (CoercionTy Coercion
    co)    InterestingVarFun
    f VarSet
    bound_vars ([Var], VarSet)
    acc = Coercion -> FV
    tyCoFVsOfCo Coercion
    co InterestingVarFun
    f VarSet
    bound_vars ([Var], VarSet)
    acc

    tyCoFVsBndr :: ForAllTyBinder -> FV -> FV
    -- Free vars of (forall b. <thing with fvs>)
    tyCoFVsBndr :: ForAllTyBinder -> FV -> FV
    tyCoFVsBndr (Bndr Var
    tv ForAllTyFlag
    _) FV
    fvs = Var -> FV -> FV
    tyCoFVsVarBndr Var
    tv FV
    fvs

    tyCoFVsVarBndrs :: [Var] -> FV -> FV
    tyCoFVsVarBndrs :: [Var] -> FV -> FV
    tyCoFVsVarBndrs [Var]
    vars FV
    fvs = (Var -> FV -> FV) -> FV -> [Var] -> FV
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr Var -> FV -> FV
    tyCoFVsVarBndr FV
    fvs [Var]
    vars

    tyCoFVsVarBndr :: Var -> FV -> FV
    tyCoFVsVarBndr :: Var -> FV -> FV
    tyCoFVsVarBndr Var
    var FV
    fvs
      = Type -> FV
    tyCoFVsOfType (Var -> Type
    varType Var
    var)   -- Free vars of its type/kind
        FV -> FV -> FV
    `unionFV` Var -> FV -> FV
    delFV Var
    var FV
    fvs       -- Delete it from the thing-inside

    tyCoFVsOfTypes :: [Type] -> FV
    -- See Note [Free variables of types]
    tyCoFVsOfTypes :: [Type] -> FV
    tyCoFVsOfTypes (Type
    ty:[Type]
    tys) InterestingVarFun
    fv_cand VarSet
    in_scope ([Var], VarSet)
    acc = (Type -> FV
    tyCoFVsOfType Type
    ty FV -> FV -> FV
    `unionFV` [Type] -> FV
    tyCoFVsOfTypes [Type]
    tys) InterestingVarFun
    fv_cand VarSet
    in_scope ([Var], VarSet)
    acc
    tyCoFVsOfTypes []       InterestingVarFun
    fv_cand VarSet
    in_scope ([Var], VarSet)
    acc = FV
    emptyFV InterestingVarFun
    fv_cand VarSet
    in_scope ([Var], VarSet)
    acc

    -- | Get a deterministic set of the vars free in a coercion
    tyCoVarsOfCoDSet :: Coercion -> DTyCoVarSet
    -- See Note [Free variables of types]
    tyCoVarsOfCoDSet :: Coercion -> DCoVarSet
    tyCoVarsOfCoDSet Coercion
    co = FV -> DCoVarSet
    fvDVarSet (FV -> DCoVarSet) -> FV -> DCoVarSet
    forall a b. (a -> b) -> a -> b
    $ Coercion -> FV
    tyCoFVsOfCo Coercion
    co

    tyCoVarsOfCoList :: Coercion -> [TyCoVar]
    -- See Note [Free variables of types]
    tyCoVarsOfCoList :: Coercion -> [Var]
    tyCoVarsOfCoList Coercion
    co = FV -> [Var]
    fvVarList (FV -> [Var]) -> FV -> [Var]
    forall a b. (a -> b) -> a -> b
    $ Coercion -> FV
    tyCoFVsOfCo Coercion
    co

    tyCoFVsOfMCo :: MCoercion -> FV
    tyCoFVsOfMCo :: MCoercion -> FV
    tyCoFVsOfMCo MCoercion
    MRefl    = FV
    emptyFV
    tyCoFVsOfMCo (MCo Coercion
    co) = Coercion -> FV
    tyCoFVsOfCo Coercion
    co

    tyCoFVsOfCo :: Coercion -> FV
    -- Extracts type and coercion variables from a coercion
    -- See Note [Free variables of types]
    tyCoFVsOfCo :: Coercion -> FV
    tyCoFVsOfCo (Refl Type
    ty) InterestingVarFun
    fv_cand VarSet
    in_scope ([Var], VarSet)
    acc
      = Type -> FV
    tyCoFVsOfType Type
    ty InterestingVarFun
    fv_cand VarSet
    in_scope ([Var], VarSet)
    acc
    tyCoFVsOfCo (GRefl Role
    _ Type
    ty MCoercion
    mco) InterestingVarFun
    fv_cand VarSet
    in_scope ([Var], VarSet)
    acc
      = (Type -> FV
    tyCoFVsOfType Type
    ty FV -> FV -> FV
    `unionFV` MCoercion -> FV
    tyCoFVsOfMCo MCoercion
    mco) InterestingVarFun
    fv_cand VarSet
    in_scope ([Var], VarSet)
    acc
    tyCoFVsOfCo (TyConAppCo Role
    _ TyCon
    _ [Coercion]
    cos) InterestingVarFun
    fv_cand VarSet
    in_scope ([Var], VarSet)
    acc = [Coercion] -> FV
    tyCoFVsOfCos [Coercion]
    cos InterestingVarFun
    fv_cand VarSet
    in_scope ([Var], VarSet)
    acc
    tyCoFVsOfCo (AppCo Coercion
    co Coercion
    arg) InterestingVarFun
    fv_cand VarSet
    in_scope ([Var], VarSet)
    acc
      = (Coercion -> FV
    tyCoFVsOfCo Coercion
    co FV -> FV -> FV
    `unionFV` Coercion -> FV
    tyCoFVsOfCo Coercion
    arg) InterestingVarFun
    fv_cand VarSet
    in_scope ([Var], VarSet)
    acc
    tyCoFVsOfCo (ForAllCo { fco_tcv :: Coercion -> Var
    fco_tcv = Var
    tv, fco_kind :: Coercion -> Coercion
    fco_kind = Coercion
    kind_co, fco_body :: Coercion -> Coercion
    fco_body = Coercion
    co }) InterestingVarFun
    fv_cand VarSet
    in_scope ([Var], VarSet)
    acc
      = (Var -> FV -> FV
    tyCoFVsVarBndr Var
    tv (Coercion -> FV
    tyCoFVsOfCo Coercion
    co) FV -> FV -> FV
    `unionFV` Coercion -> FV
    tyCoFVsOfCo Coercion
    kind_co) InterestingVarFun
    fv_cand VarSet
    in_scope ([Var], VarSet)
    acc
    tyCoFVsOfCo (FunCo { fco_mult :: Coercion -> Coercion
    fco_mult = Coercion
    w, fco_arg :: Coercion -> Coercion
    fco_arg = Coercion
    co1, fco_res :: Coercion -> Coercion
    fco_res = Coercion
    co2 }) InterestingVarFun
    fv_cand VarSet
    in_scope ([Var], VarSet)
    acc
      = (Coercion -> FV
    tyCoFVsOfCo Coercion
    co1 FV -> FV -> FV
    `unionFV` Coercion -> FV
    tyCoFVsOfCo Coercion
    co2 FV -> FV -> FV
    `unionFV` Coercion -> FV
    tyCoFVsOfCo Coercion
    w) InterestingVarFun
    fv_cand VarSet
    in_scope ([Var], VarSet)
    acc
    tyCoFVsOfCo (CoVarCo Var
    v) InterestingVarFun
    fv_cand VarSet
    in_scope ([Var], VarSet)
    acc
      = Var -> FV
    tyCoFVsOfCoVar Var
    v InterestingVarFun
    fv_cand VarSet
    in_scope ([Var], VarSet)
    acc
    tyCoFVsOfCo (HoleCo CoercionHole
    h) InterestingVarFun
    fv_cand VarSet
    in_scope ([Var], VarSet)
    acc
      = Var -> FV
    tyCoFVsOfCoVar (CoercionHole -> Var
    coHoleCoVar CoercionHole
    h) InterestingVarFun
    fv_cand VarSet
    in_scope ([Var], VarSet)
    acc
        -- See Note [CoercionHoles and coercion free variables]
    tyCoFVsOfCo (AxiomCo CoAxiomRule
    _ [Coercion]
    cs)    InterestingVarFun
    fv_cand VarSet
    in_scope ([Var], VarSet)
    acc = [Coercion] -> FV
    tyCoFVsOfCos [Coercion]
    cs  InterestingVarFun
    fv_cand VarSet
    in_scope ([Var], VarSet)
    acc
    tyCoFVsOfCo (UnivCo { uco_lty :: Coercion -> Type
    uco_lty = Type
    t1, uco_rty :: Coercion -> Type
    uco_rty = Type
    t2, uco_deps :: Coercion -> [Coercion]
    uco_deps = [Coercion]
    deps}) InterestingVarFun
    fv_cand VarSet
    in_scope ([Var], VarSet)
    acc
      = ([Coercion] -> FV
    tyCoFVsOfCos [Coercion]
    deps FV -> FV -> FV
    `unionFV` Type -> FV
    tyCoFVsOfType Type
    t1
                          FV -> FV -> FV
    `unionFV` Type -> FV
    tyCoFVsOfType Type
    t2) InterestingVarFun
    fv_cand VarSet
    in_scope ([Var], VarSet)
    acc
    tyCoFVsOfCo (SymCo Coercion
    co)          InterestingVarFun
    fv_cand VarSet
    in_scope ([Var], VarSet)
    acc = Coercion -> FV
    tyCoFVsOfCo Coercion
    co InterestingVarFun
    fv_cand VarSet
    in_scope ([Var], VarSet)
    acc
    tyCoFVsOfCo (TransCo Coercion
    co1 Coercion
    co2)   InterestingVarFun
    fv_cand VarSet
    in_scope ([Var], VarSet)
    acc = (Coercion -> FV
    tyCoFVsOfCo Coercion
    co1 FV -> FV -> FV
    `unionFV` Coercion -> FV
    tyCoFVsOfCo Coercion
    co2) InterestingVarFun
    fv_cand VarSet
    in_scope ([Var], VarSet)
    acc
    tyCoFVsOfCo (SelCo CoSel
    _ Coercion
    co)        InterestingVarFun
    fv_cand VarSet
    in_scope ([Var], VarSet)
    acc = Coercion -> FV
    tyCoFVsOfCo Coercion
    co InterestingVarFun
    fv_cand VarSet
    in_scope ([Var], VarSet)
    acc
    tyCoFVsOfCo (LRCo LeftOrRight
    _ Coercion
    co)         InterestingVarFun
    fv_cand VarSet
    in_scope ([Var], VarSet)
    acc = Coercion -> FV
    tyCoFVsOfCo Coercion
    co InterestingVarFun
    fv_cand VarSet
    in_scope ([Var], VarSet)
    acc
    tyCoFVsOfCo (InstCo Coercion
    co Coercion
    arg)     InterestingVarFun
    fv_cand VarSet
    in_scope ([Var], VarSet)
    acc = (Coercion -> FV
    tyCoFVsOfCo Coercion
    co FV -> FV -> FV
    `unionFV` Coercion -> FV
    tyCoFVsOfCo Coercion
    arg) InterestingVarFun
    fv_cand VarSet
    in_scope ([Var], VarSet)
    acc
    tyCoFVsOfCo (KindCo Coercion
    co)         InterestingVarFun
    fv_cand VarSet
    in_scope ([Var], VarSet)
    acc = Coercion -> FV
    tyCoFVsOfCo Coercion
    co InterestingVarFun
    fv_cand VarSet
    in_scope ([Var], VarSet)
    acc
    tyCoFVsOfCo (SubCo Coercion
    co)          InterestingVarFun
    fv_cand VarSet
    in_scope ([Var], VarSet)
    acc = Coercion -> FV
    tyCoFVsOfCo Coercion
    co InterestingVarFun
    fv_cand VarSet
    in_scope ([Var], VarSet)
    acc

    tyCoFVsOfCoVar :: CoVar -> FV
    tyCoFVsOfCoVar :: Var -> FV
    tyCoFVsOfCoVar Var
    v InterestingVarFun
    fv_cand VarSet
    in_scope ([Var], VarSet)
    acc
      = (Var -> FV
    unitFV Var
    v FV -> FV -> FV
    `unionFV` Type -> FV
    tyCoFVsOfType (Var -> Type
    varType Var
    v)) InterestingVarFun
    fv_cand VarSet
    in_scope ([Var], VarSet)
    acc

    tyCoFVsOfCos :: [Coercion] -> FV
    tyCoFVsOfCos :: [Coercion] -> FV
    tyCoFVsOfCos []       InterestingVarFun
    fv_cand VarSet
    in_scope ([Var], VarSet)
    acc = FV
    emptyFV InterestingVarFun
    fv_cand VarSet
    in_scope ([Var], VarSet)
    acc
    tyCoFVsOfCos (Coercion
    co:[Coercion]
    cos) InterestingVarFun
    fv_cand VarSet
    in_scope ([Var], VarSet)
    acc = (Coercion -> FV
    tyCoFVsOfCo Coercion
    co FV -> FV -> FV
    `unionFV` [Coercion] -> FV
    tyCoFVsOfCos [Coercion]
    cos) InterestingVarFun
    fv_cand VarSet
    in_scope ([Var], VarSet)
    acc

    ----- Whether a covar is /Almost Devoid/ in a type or coercion ----

    -- | Given a covar and a coercion, returns True if covar is almost devoid in
    -- the coercion. That is, covar can only appear in Refl and GRefl.
    -- See (FC6) in Note [ForAllCo] in "GHC.Core.TyCo.Rep"
    almostDevoidCoVarOfCo :: CoVar -> Coercion -> Bool
    almostDevoidCoVarOfCo :: Var -> Coercion -> Bool
    almostDevoidCoVarOfCo Var
    cv Coercion
    co =
      Coercion -> InterestingVarFun
    almost_devoid_co_var_of_co Coercion
    co Var
    cv

    almost_devoid_co_var_of_co :: Coercion -> CoVar -> Bool
    almost_devoid_co_var_of_co :: Coercion -> InterestingVarFun
    almost_devoid_co_var_of_co (Refl {}) Var
    _ = Bool
    True   -- covar is allowed in Refl and
    almost_devoid_co_var_of_co (GRefl {}) Var
    _ = Bool
    True  -- GRefl, so we don't look into
                                                    -- the coercions
    almost_devoid_co_var_of_co (TyConAppCo Role
    _ TyCon
    _ [Coercion]
    cos) Var
    cv
      = [Coercion] -> InterestingVarFun
    almost_devoid_co_var_of_cos [Coercion]
    cos Var
    cv
    almost_devoid_co_var_of_co (AppCo Coercion
    co Coercion
    arg) Var
    cv
      = Coercion -> InterestingVarFun
    almost_devoid_co_var_of_co Coercion
    co Var
    cv
      Bool -> Bool -> Bool
    && Coercion -> InterestingVarFun
    almost_devoid_co_var_of_co Coercion
    arg Var
    cv
    almost_devoid_co_var_of_co (ForAllCo { fco_tcv :: Coercion -> Var
    fco_tcv = Var
    v, fco_kind :: Coercion -> Coercion
    fco_kind = Coercion
    kind_co, fco_body :: Coercion -> Coercion
    fco_body = Coercion
    co }) Var
    cv
      = Coercion -> InterestingVarFun
    almost_devoid_co_var_of_co Coercion
    kind_co Var
    cv
      Bool -> Bool -> Bool
    && (Var
    v Var -> InterestingVarFun
    forall a. Eq a => a -> a -> Bool
    == Var
    cv Bool -> Bool -> Bool
    || Coercion -> InterestingVarFun
    almost_devoid_co_var_of_co Coercion
    co Var
    cv)
    almost_devoid_co_var_of_co (FunCo { fco_mult :: Coercion -> Coercion
    fco_mult = Coercion
    w, fco_arg :: Coercion -> Coercion
    fco_arg = Coercion
    co1, fco_res :: Coercion -> Coercion
    fco_res = Coercion
    co2 }) Var
    cv
      =  Coercion -> InterestingVarFun
    almost_devoid_co_var_of_co Coercion
    w   Var
    cv
      Bool -> Bool -> Bool
    && Coercion -> InterestingVarFun
    almost_devoid_co_var_of_co Coercion
    co1 Var
    cv
      Bool -> Bool -> Bool
    && Coercion -> InterestingVarFun
    almost_devoid_co_var_of_co Coercion
    co2 Var
    cv
    almost_devoid_co_var_of_co (CoVarCo Var
    v) Var
    cv = Var
    v Var -> InterestingVarFun
    forall a. Eq a => a -> a -> Bool
    /= Var
    cv
    almost_devoid_co_var_of_co (HoleCo CoercionHole
    h)  Var
    cv = (CoercionHole -> Var
    coHoleCoVar CoercionHole
    h) Var -> InterestingVarFun
    forall a. Eq a => a -> a -> Bool
    /= Var
    cv
    almost_devoid_co_var_of_co (AxiomCo CoAxiomRule
    _ [Coercion]
    cs) Var
    cv
      = [Coercion] -> InterestingVarFun
    almost_devoid_co_var_of_cos [Coercion]
    cs Var
    cv
    almost_devoid_co_var_of_co (UnivCo { uco_lty :: Coercion -> Type
    uco_lty = Type
    t1, uco_rty :: Coercion -> Type
    uco_rty = Type
    t2, uco_deps :: Coercion -> [Coercion]
    uco_deps = [Coercion]
    deps }) Var
    cv
      =  [Coercion] -> InterestingVarFun
    almost_devoid_co_var_of_cos [Coercion]
    deps Var
    cv
      Bool -> Bool -> Bool
    && Type -> InterestingVarFun
    almost_devoid_co_var_of_type Type
    t1 Var
    cv
      Bool -> Bool -> Bool
    && Type -> InterestingVarFun
    almost_devoid_co_var_of_type Type
    t2 Var
    cv
    almost_devoid_co_var_of_co (SymCo Coercion
    co) Var
    cv
      = Coercion -> InterestingVarFun
    almost_devoid_co_var_of_co Coercion
    co Var
    cv
    almost_devoid_co_var_of_co (TransCo Coercion
    co1 Coercion
    co2) Var
    cv
      = Coercion -> InterestingVarFun
    almost_devoid_co_var_of_co Coercion
    co1 Var
    cv
      Bool -> Bool -> Bool
    && Coercion -> InterestingVarFun
    almost_devoid_co_var_of_co Coercion
    co2 Var
    cv
    almost_devoid_co_var_of_co (SelCo CoSel
    _ Coercion
    co) Var
    cv
      = Coercion -> InterestingVarFun
    almost_devoid_co_var_of_co Coercion
    co Var
    cv
    almost_devoid_co_var_of_co (LRCo LeftOrRight
    _ Coercion
    co) Var
    cv
      = Coercion -> InterestingVarFun
    almost_devoid_co_var_of_co Coercion
    co Var
    cv
    almost_devoid_co_var_of_co (InstCo Coercion
    co Coercion
    arg) Var
    cv
      = Coercion -> InterestingVarFun
    almost_devoid_co_var_of_co Coercion
    co Var
    cv
      Bool -> Bool -> Bool
    && Coercion -> InterestingVarFun
    almost_devoid_co_var_of_co Coercion
    arg Var
    cv
    almost_devoid_co_var_of_co (KindCo Coercion
    co) Var
    cv
      = Coercion -> InterestingVarFun
    almost_devoid_co_var_of_co Coercion
    co Var
    cv
    almost_devoid_co_var_of_co (SubCo Coercion
    co) Var
    cv
      = Coercion -> InterestingVarFun
    almost_devoid_co_var_of_co Coercion
    co Var
    cv

    almost_devoid_co_var_of_cos :: [Coercion] -> CoVar -> Bool
    almost_devoid_co_var_of_cos :: [Coercion] -> InterestingVarFun
    almost_devoid_co_var_of_cos [] Var
    _ = Bool
    True
    almost_devoid_co_var_of_cos (Coercion
    co:[Coercion]
    cos) Var
    cv
      = Coercion -> InterestingVarFun
    almost_devoid_co_var_of_co Coercion
    co Var
    cv
      Bool -> Bool -> Bool
    && [Coercion] -> InterestingVarFun
    almost_devoid_co_var_of_cos [Coercion]
    cos Var
    cv

    almost_devoid_co_var_of_type :: Type -> CoVar -> Bool
    almost_devoid_co_var_of_type :: Type -> InterestingVarFun
    almost_devoid_co_var_of_type (TyVarTy Var
    _) Var
    _ = Bool
    True
    almost_devoid_co_var_of_type (TyConApp TyCon
    _ [Type]
    tys) Var
    cv
      = [Type] -> InterestingVarFun
    almost_devoid_co_var_of_types [Type]
    tys Var
    cv
    almost_devoid_co_var_of_type (LitTy {}) Var
    _ = Bool
    True
    almost_devoid_co_var_of_type (AppTy Type
    fun Type
    arg) Var
    cv
      = Type -> InterestingVarFun
    almost_devoid_co_var_of_type Type
    fun Var
    cv
      Bool -> Bool -> Bool
    && Type -> InterestingVarFun
    almost_devoid_co_var_of_type Type
    arg Var
    cv
    almost_devoid_co_var_of_type (FunTy FunTyFlag
    _ Type
    w Type
    arg Type
    res) Var
    cv
      = Type -> InterestingVarFun
    almost_devoid_co_var_of_type Type
    w Var
    cv
      Bool -> Bool -> Bool
    && Type -> InterestingVarFun
    almost_devoid_co_var_of_type Type
    arg Var
    cv
      Bool -> Bool -> Bool
    && Type -> InterestingVarFun
    almost_devoid_co_var_of_type Type
    res Var
    cv
    almost_devoid_co_var_of_type (ForAllTy (Bndr Var
    v ForAllTyFlag
    _) Type
    ty) Var
    cv
      = Type -> InterestingVarFun
    almost_devoid_co_var_of_type (Var -> Type
    varType Var
    v) Var
    cv
      Bool -> Bool -> Bool
    && (Var
    v Var -> InterestingVarFun
    forall a. Eq a => a -> a -> Bool
    == Var
    cv Bool -> Bool -> Bool
    || Type -> InterestingVarFun
    almost_devoid_co_var_of_type Type
    ty Var
    cv)
    almost_devoid_co_var_of_type (CastTy Type
    ty Coercion
    co) Var
    cv
      = Type -> InterestingVarFun
    almost_devoid_co_var_of_type Type
    ty Var
    cv
      Bool -> Bool -> Bool
    && Coercion -> InterestingVarFun
    almost_devoid_co_var_of_co Coercion
    co Var
    cv
    almost_devoid_co_var_of_type (CoercionTy Coercion
    co) Var
    cv
      = Coercion -> InterestingVarFun
    almost_devoid_co_var_of_co Coercion
    co Var
    cv

    almost_devoid_co_var_of_types :: [Type] -> CoVar -> Bool
    almost_devoid_co_var_of_types :: [Type] -> InterestingVarFun
    almost_devoid_co_var_of_types [] Var
    _ = Bool
    True
    almost_devoid_co_var_of_types (Type
    ty:[Type]
    tys) Var
    cv
      = Type -> InterestingVarFun
    almost_devoid_co_var_of_type Type
    ty Var
    cv
      Bool -> Bool -> Bool
    && [Type] -> InterestingVarFun
    almost_devoid_co_var_of_types [Type]
    tys Var
    cv

    {-
    %************************************************************************
    %*                                                                      *
            Free tyvars, but with visible/invisible info
    %*                                                                      *
    %************************************************************************

    -}
    -- | Retrieve the free variables in this type, splitting them based
    -- on whether they are used visibly or invisibly. Invisible ones come
    -- first.
    visVarsOfType :: Type -> Pair TyCoVarSet
    visVarsOfType :: Type -> Pair VarSet
    visVarsOfType Type
    orig_ty = VarSet -> VarSet -> Pair VarSet
    forall a. a -> a -> Pair a
    Pair VarSet
    invis_vars VarSet
    vis_vars
      where
        Pair VarSet
    invis_vars1 VarSet
    vis_vars = Type -> Pair VarSet
    go Type
    orig_ty
        invis_vars :: VarSet
    invis_vars = VarSet
    invis_vars1 VarSet -> VarSet -> VarSet
    `minusVarSet` VarSet
    vis_vars

        go :: Type -> Pair VarSet
    go (TyVarTy Var
    tv)      = VarSet -> VarSet -> Pair VarSet
    forall a. a -> a -> Pair a
    Pair (Type -> VarSet
    tyCoVarsOfType (Type -> VarSet) -> Type -> VarSet
    forall a b. (a -> b) -> a -> b
    $ Var -> Type
    tyVarKind Var
    tv) (Var -> VarSet
    unitVarSet Var
    tv)
        go (AppTy Type
    t1 Type
    t2)     = Type -> Pair VarSet
    go Type
    t1 Pair VarSet -> Pair VarSet -> Pair VarSet
    forall a. Monoid a => a -> a -> a
    `mappend` Type -> Pair VarSet
    go Type
    t2
        go (TyConApp TyCon
    tc [Type]
    tys) = TyCon -> [Type] -> Pair VarSet
    go_tc TyCon
    tc [Type]
    tys
        go (FunTy FunTyFlag
    _ Type
    w Type
    t1 Type
    t2) = Type -> Pair VarSet
    go Type
    w Pair VarSet -> Pair VarSet -> Pair VarSet
    forall a. Monoid a => a -> a -> a
    `mappend` Type -> Pair VarSet
    go Type
    t1 Pair VarSet -> Pair VarSet -> Pair VarSet
    forall a. Monoid a => a -> a -> a
    `mappend` Type -> Pair VarSet
    go Type
    t2
        go (ForAllTy (Bndr Var
    tv ForAllTyFlag
    _) Type
    ty)
          = ((VarSet -> Var -> VarSet
    `delVarSet` Var
    tv) (VarSet -> VarSet) -> Pair VarSet -> Pair VarSet
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Type -> Pair VarSet
    go Type
    ty) Pair VarSet -> Pair VarSet -> Pair VarSet
    forall a. Monoid a => a -> a -> a
    `mappend`
            (VarSet -> Pair VarSet
    invisible (Type -> VarSet
    tyCoVarsOfType (Type -> VarSet) -> Type -> VarSet
    forall a b. (a -> b) -> a -> b
    $ Var -> Type
    varType Var
    tv))
        go (LitTy {}) = Pair VarSet
    forall a. Monoid a => a
    mempty
        go (CastTy Type
    ty Coercion
    co) = Type -> Pair VarSet
    go Type
    ty Pair VarSet -> Pair VarSet -> Pair VarSet
    forall a. Monoid a => a -> a -> a
    `mappend` VarSet -> Pair VarSet
    invisible (Coercion -> VarSet
    tyCoVarsOfCo Coercion
    co)
        go (CoercionTy Coercion
    co) = VarSet -> Pair VarSet
    invisible (VarSet -> Pair VarSet) -> VarSet -> Pair VarSet
    forall a b. (a -> b) -> a -> b
    $ Coercion -> VarSet
    tyCoVarsOfCo Coercion
    co

        invisible :: VarSet -> Pair VarSet
    invisible VarSet
    vs = VarSet -> VarSet -> Pair VarSet
    forall a. a -> a -> Pair a
    Pair VarSet
    vs VarSet
    emptyVarSet

        go_tc :: TyCon -> [Type] -> Pair VarSet
    go_tc TyCon
    tc [Type]
    tys = let ([Type]
    invis, [Type]
    vis) = TyCon -> [Type] -> ([Type], [Type])
    partitionInvisibleTypes TyCon
    tc [Type]
    tys in
                       VarSet -> Pair VarSet
    invisible ([Type] -> VarSet
    tyCoVarsOfTypes [Type]
    invis) Pair VarSet -> Pair VarSet -> Pair VarSet
    forall a. Monoid a => a -> a -> a
    `mappend` (Type -> Pair VarSet) -> [Type] -> Pair VarSet
    forall m a. Monoid m => (a -> m) -> [a] -> m
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap Type -> Pair VarSet
    go [Type]
    vis

    visVarsOfTypes :: [Type] -> Pair TyCoVarSet
    visVarsOfTypes :: [Type] -> Pair VarSet
    visVarsOfTypes = (Type -> Pair VarSet) -> [Type] -> Pair VarSet
    forall m a. Monoid m => (a -> m) -> [a] -> m
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap Type -> Pair VarSet
    visVarsOfType

    {- *********************************************************************
    *                                                                      *
                     Injective free vars
    *                                                                      *
    ********************************************************************* -}

    isInjectiveInType :: TyVar -> Type -> Bool
    -- True <=> tv /definitely/ appears injectively in ty
    -- A bit more efficient that (tv `elemVarSet` injectiveTyVarsOfType ty)
    -- Ignore occurrence in coercions, and even in injective positions of
    -- type families.
    isInjectiveInType :: Var -> Type -> Bool
    isInjectiveInType Var
    tv Type
    ty
      = Type -> Bool
    go Type
    ty
      where
        go :: Type -> Bool
    go Type
    ty | Just Type
    ty' <- Type -> Maybe Type
    rewriterView Type
    ty = Type -> Bool
    go Type
    ty'
        go (TyVarTy Var
    tv')                    = Var
    tv' Var -> InterestingVarFun
    forall a. Eq a => a -> a -> Bool
    == Var
    tv
        go (AppTy Type
    f Type
    a)                      = Type -> Bool
    go Type
    f Bool -> Bool -> Bool
    || Type -> Bool
    go Type
    a
        go (FunTy FunTyFlag
    _ Type
    w Type
    ty1 Type
    ty2)              = Type -> Bool
    go Type
    w Bool -> Bool -> Bool
    || Type -> Bool
    go Type
    ty1 Bool -> Bool -> Bool
    || Type -> Bool
    go Type
    ty2
        go (TyConApp TyCon
    tc [Type]
    tys)                = TyCon -> [Type] -> Bool
    go_tc TyCon
    tc [Type]
    tys
        go (ForAllTy (Bndr Var
    tv' ForAllTyFlag
    _) Type
    ty)       = Type -> Bool
    go (Var -> Type
    tyVarKind Var
    tv')
                                              Bool -> Bool -> Bool
    || (Var
    tv Var -> InterestingVarFun
    forall a. Eq a => a -> a -> Bool
    /= Var
    tv' Bool -> Bool -> Bool
    && Type -> Bool
    go Type
    ty)
        go LitTy{}                          = Bool
    False
        go (CastTy Type
    ty Coercion
    _)                    = Type -> Bool
    go Type
    ty
        go CoercionTy{}                     = Bool
    False

        go_tc :: TyCon -> [Type] -> Bool
    go_tc TyCon
    tc [Type]
    tys | TyCon -> Bool
    isTypeFamilyTyCon TyCon
    tc = Bool
    False
                     | Bool
    otherwise            = (Type -> Bool) -> [Type] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any Type -> Bool
    go [Type]
    tys

    -- | Returns the free variables of a 'Type' that are in injective positions.
    -- Specifically, it finds the free variables while:
    --
    -- * Expanding type synonyms
    --
    -- * Ignoring the coercion in @(ty |> co)@
    --
    -- * Ignoring the non-injective fields of a 'TyConApp'
    --
    --
    -- For example, if @F@ is a non-injective type family, then:
    --
    -- @
    -- injectiveTyVarsOf( Either c (Maybe (a, F b c)) ) = {a,c}
    -- @
    --
    -- If @'injectiveVarsOfType' ty = itvs@, then knowing @ty@ fixes @itvs@.
    -- More formally, if
    -- @a@ is in @'injectiveVarsOfType' ty@
    -- and  @S1(ty) ~ S2(ty)@,
    -- then @S1(a)  ~ S2(a)@,
    -- where @S1@ and @S2@ are arbitrary substitutions.
    --
    -- See @Note [When does a tycon application need an explicit kind signature?]@.
    injectiveVarsOfType :: Bool   -- ^ Should we look under injective type families?
                                  -- See Note [Coverage condition for injective type families]
                                  -- in "GHC.Tc.Instance.Family".
                        -> Type -> FV
    injectiveVarsOfType :: Bool -> Type -> FV
    injectiveVarsOfType Bool
    look_under_tfs = Type -> FV
    go
      where
        go :: Type -> FV
    go Type
    ty | Just Type
    ty' <- Type -> Maybe Type
    rewriterView Type
    ty = Type -> FV
    go Type
    ty'
        go (TyVarTy Var
    v)                      = Var -> FV
    unitFV Var
    v FV -> FV -> FV
    `unionFV` Type -> FV
    go (Var -> Type
    tyVarKind Var
    v)
        go (AppTy Type
    f Type
    a)                      = Type -> FV
    go Type
    f FV -> FV -> FV
    `unionFV` Type -> FV
    go Type
    a
        go (FunTy FunTyFlag
    _ Type
    w Type
    ty1 Type
    ty2)              = Type -> FV
    go Type
    w FV -> FV -> FV
    `unionFV` Type -> FV
    go Type
    ty1 FV -> FV -> FV
    `unionFV` Type -> FV
    go Type
    ty2
        go (TyConApp TyCon
    tc [Type]
    tys)                = TyCon -> [Type] -> FV
    go_tc TyCon
    tc [Type]
    tys
        go (ForAllTy (Bndr Var
    tv ForAllTyFlag
    _) Type
    ty)        = Type -> FV
    go (Var -> Type
    tyVarKind Var
    tv) FV -> FV -> FV
    `unionFV` Var -> FV -> FV
    delFV Var
    tv (Type -> FV
    go Type
    ty)
        go LitTy{}                          = FV
    emptyFV
        go (CastTy Type
    ty Coercion
    _)                    = Type -> FV
    go Type
    ty
        go CoercionTy{}                     = FV
    emptyFV

        go_tc :: TyCon -> [Type] -> FV
    go_tc TyCon
    tc [Type]
    tys
          | TyCon -> Bool
    isTypeFamilyTyCon TyCon
    tc
          = if | Bool
    look_under_tfs
               , Injective [Bool]
    flags <- TyCon -> Injectivity
    tyConInjectivityInfo TyCon
    tc
               -> (Type -> FV) -> [Type] -> FV
    forall a. (a -> FV) -> [a] -> FV
    mapUnionFV Type -> FV
    go ([Type] -> FV) -> [Type] -> FV
    forall a b. (a -> b) -> a -> b
    $
                  [Bool] -> [Type] -> [Type]
    forall a. [Bool] -> [a] -> [a]
    filterByList ([Bool]
    flags [Bool] -> [Bool] -> [Bool]
    forall a. [a] -> [a] -> [a]
    ++ Bool -> [Bool]
    forall a. a -> [a]
    repeat Bool
    True) [Type]
    tys
                             -- Oversaturated arguments to a tycon are
                             -- always injective, hence the repeat True
               | Bool
    otherwise   -- No injectivity info for this type family
               -> FV
    emptyFV

          | Bool
    otherwise        -- Data type, injective in all positions
          = (Type -> FV) -> [Type] -> FV
    forall a. (a -> FV) -> [a] -> FV
    mapUnionFV Type -> FV
    go [Type]
    tys

    -- | Returns the free variables of a 'Type' that are in injective positions.
    -- Specifically, it finds the free variables while:
    --
    -- * Expanding type synonyms
    --
    -- * Ignoring the coercion in @(ty |> co)@
    --
    -- * Ignoring the non-injective fields of a 'TyConApp'
    --
    -- See @Note [When does a tycon application need an explicit kind signature?]@.
    injectiveVarsOfTypes :: Bool -- ^ look under injective type families?
                                 -- See Note [Coverage condition for injective type families]
                                 -- in "GHC.Tc.Instance.Family".
                         -> [Type] -> FV
    injectiveVarsOfTypes :: Bool -> [Type] -> FV
    injectiveVarsOfTypes Bool
    look_under_tfs = (Type -> FV) -> [Type] -> FV
    forall a. (a -> FV) -> [a] -> FV
    mapUnionFV (Bool -> Type -> FV
    injectiveVarsOfType Bool
    look_under_tfs)

    {- *********************************************************************
    *                                                                      *
                     Invisible vars
    *                                                                      *
    ********************************************************************* -}

    -- | Returns the set of variables that are used invisibly anywhere within
    -- the given type. A variable will be included even if it is used both visibly
    -- and invisibly. An invisible use site includes:
    --   * In the kind of a variable
    --   * In the kind of a bound variable in a forall
    --   * In a coercion
    --   * In a Specified or Inferred argument to a function
    -- See Note [VarBndrs, ForAllTyBinders, TyConBinders, and visibility] in "GHC.Core.TyCo.Rep"
    invisibleVarsOfType :: Type -> FV
    invisibleVarsOfType :: Type -> FV
    invisibleVarsOfType = Type -> FV
    go
      where
        go :: Type -> FV
    go Type
    ty                 | Just Type
    ty' <- Type -> Maybe Type
    coreView Type
    ty
                              = Type -> FV
    go Type
    ty'
        go (TyVarTy Var
    v)        = Type -> FV
    go (Var -> Type
    tyVarKind Var
    v)
        go (AppTy Type
    f Type
    a)        = Type -> FV
    go Type
    f FV -> FV -> FV
    `unionFV` Type -> FV
    go Type
    a
        go (FunTy FunTyFlag
    _ Type
    w Type
    ty1 Type
    ty2) = Type -> FV
    go Type
    w FV -> FV -> FV
    `unionFV` Type -> FV
    go Type
    ty1 FV -> FV -> FV
    `unionFV` Type -> FV
    go Type
    ty2
        go (TyConApp TyCon
    tc [Type]
    tys)  = [Type] -> FV
    tyCoFVsOfTypes [Type]
    invisibles FV -> FV -> FV
    `unionFV`
                                [Type] -> FV
    invisibleVarsOfTypes [Type]
    visibles
          where ([Type]
    invisibles, [Type]
    visibles) = TyCon -> [Type] -> ([Type], [Type])
    partitionInvisibleTypes TyCon
    tc [Type]
    tys
        go (ForAllTy ForAllTyBinder
    tvb Type
    ty)  = ForAllTyBinder -> FV -> FV
    tyCoFVsBndr ForAllTyBinder
    tvb (FV -> FV) -> FV -> FV
    forall a b. (a -> b) -> a -> b
    $ Type -> FV
    go Type
    ty
        go LitTy{}            = FV
    emptyFV
        go (CastTy Type
    ty Coercion
    co)     = Coercion -> FV
    tyCoFVsOfCo Coercion
    co FV -> FV -> FV
    `unionFV` Type -> FV
    go Type
    ty
        go (CoercionTy Coercion
    co)    = Coercion -> FV
    tyCoFVsOfCo Coercion
    co

    -- | Like 'invisibleVarsOfType', but for many types.
    invisibleVarsOfTypes :: [Type] -> FV
    invisibleVarsOfTypes :: [Type] -> FV
    invisibleVarsOfTypes = (Type -> FV) -> [Type] -> FV
    forall a. (a -> FV) -> [a] -> FV
    mapUnionFV Type -> FV
    invisibleVarsOfType

    {- *********************************************************************
    *                                                                      *
                     Any free vars
    *                                                                      *
    ********************************************************************* -}

    {-# INLINE afvFolder #-}   -- so that specialization to (const True) works
    afvFolder :: (TyCoVar -> Bool) -> TyCoFolder TyCoVarSet DM.Any
    -- 'afvFolder' is short for "any-free-var folder", good for checking
    -- if any free var of a type satisfies a predicate `check_fv`
    afvFolder :: InterestingVarFun -> TyCoFolder VarSet Any
    afvFolder InterestingVarFun
    check_fv = TyCoFolder { tcf_view :: Type -> Maybe Type
    tcf_view = Type -> Maybe Type
    noView  -- See Note [Free vars and synonyms]
                                    , tcf_tyvar :: VarSet -> Var -> Any
    tcf_tyvar = VarSet -> Var -> Any
    do_tcv, tcf_covar :: VarSet -> Var -> Any
    tcf_covar = VarSet -> Var -> Any
    do_tcv
                                    , tcf_hole :: VarSet -> CoercionHole -> Any
    tcf_hole = VarSet -> CoercionHole -> Any
    forall {p} {p}. p -> p -> Any
    do_hole, tcf_tycobinder :: VarSet -> Var -> ForAllTyFlag -> VarSet
    tcf_tycobinder = VarSet -> Var -> ForAllTyFlag -> VarSet
    forall {p}. VarSet -> Var -> p -> VarSet
    do_bndr }
      where
        do_tcv :: VarSet -> Var -> Any
    do_tcv VarSet
    is Var
    tv = Bool -> Any
    Any (Bool -> Bool
    not (Var
    tv Var -> VarSet -> Bool
    `elemVarSet` VarSet
    is) Bool -> Bool -> Bool
    && InterestingVarFun
    check_fv Var
    tv)
        do_hole :: p -> p -> Any
    do_hole p
    _ p
    _  = Bool -> Any
    Any Bool
    False    -- I'm unsure; probably never happens
        do_bndr :: VarSet -> Var -> p -> VarSet
    do_bndr VarSet
    is Var
    tv p
    _ = VarSet
    is VarSet -> Var -> VarSet
    `extendVarSet` Var
    tv

    anyFreeVarsOfType :: (TyCoVar -> Bool) -> Type -> Bool
    anyFreeVarsOfType :: InterestingVarFun -> Type -> Bool
    anyFreeVarsOfType InterestingVarFun
    check_fv Type
    ty = Any -> Bool
    DM.getAny (Type -> Any
    f Type
    ty)
      where (Type -> Any
    f, [Type] -> Any
    _, Coercion -> Any
    _, [Coercion] -> Any
    _) = TyCoFolder VarSet Any
    -> VarSet
    -> (Type -> Any, [Type] -> Any, Coercion -> Any, [Coercion] -> Any)
    forall a env.
    Monoid a =>
    TyCoFolder env a
    -> env -> (Type -> a, [Type] -> a, Coercion -> a, [Coercion] -> a)
    foldTyCo (InterestingVarFun -> TyCoFolder VarSet Any
    afvFolder InterestingVarFun
    check_fv) VarSet
    emptyVarSet

    anyFreeVarsOfTypes :: (TyCoVar -> Bool) -> [Type] -> Bool
    anyFreeVarsOfTypes :: InterestingVarFun -> [Type] -> Bool
    anyFreeVarsOfTypes InterestingVarFun
    check_fv [Type]
    tys = Any -> Bool
    DM.getAny ([Type] -> Any
    f [Type]
    tys)
      where (Type -> Any
    _, [Type] -> Any
    f, Coercion -> Any
    _, [Coercion] -> Any
    _) = TyCoFolder VarSet Any
    -> VarSet
    -> (Type -> Any, [Type] -> Any, Coercion -> Any, [Coercion] -> Any)
    forall a env.
    Monoid a =>
    TyCoFolder env a
    -> env -> (Type -> a, [Type] -> a, Coercion -> a, [Coercion] -> a)
    foldTyCo (InterestingVarFun -> TyCoFolder VarSet Any
    afvFolder InterestingVarFun
    check_fv) VarSet
    emptyVarSet

    anyFreeVarsOfCo :: (TyCoVar -> Bool) -> Coercion -> Bool
    anyFreeVarsOfCo :: InterestingVarFun -> Coercion -> Bool
    anyFreeVarsOfCo InterestingVarFun
    check_fv Coercion
    co = Any -> Bool
    DM.getAny (Coercion -> Any
    f Coercion
    co)
      where (Type -> Any
    _, [Type] -> Any
    _, Coercion -> Any
    f, [Coercion] -> Any
    _) = TyCoFolder VarSet Any
    -> VarSet
    -> (Type -> Any, [Type] -> Any, Coercion -> Any, [Coercion] -> Any)
    forall a env.
    Monoid a =>
    TyCoFolder env a
    -> env -> (Type -> a, [Type] -> a, Coercion -> a, [Coercion] -> a)
    foldTyCo (InterestingVarFun -> TyCoFolder VarSet Any
    afvFolder InterestingVarFun
    check_fv) VarSet
    emptyVarSet

    noFreeVarsOfType :: Type -> Bool
    noFreeVarsOfType :: Type -> Bool
    noFreeVarsOfType Type
    ty = Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ Any -> Bool
    DM.getAny (Type -> Any
    f Type
    ty)
      where (Type -> Any
    f, [Type] -> Any
    _, Coercion -> Any
    _, [Coercion] -> Any
    _) = TyCoFolder VarSet Any
    -> VarSet
    -> (Type -> Any, [Type] -> Any, Coercion -> Any, [Coercion] -> Any)
    forall a env.
    Monoid a =>
    TyCoFolder env a
    -> env -> (Type -> a, [Type] -> a, Coercion -> a, [Coercion] -> a)
    foldTyCo (InterestingVarFun -> TyCoFolder VarSet Any
    afvFolder (Bool -> InterestingVarFun
    forall a b. a -> b -> a
    const Bool
    True)) VarSet
    emptyVarSet

    noFreeVarsOfTypes :: [Type] -> Bool
    noFreeVarsOfTypes :: [Type] -> Bool
    noFreeVarsOfTypes [Type]
    tys = Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ Any -> Bool
    DM.getAny ([Type] -> Any
    f [Type]
    tys)
      where (Type -> Any
    _, [Type] -> Any
    f, Coercion -> Any
    _, [Coercion] -> Any
    _) = TyCoFolder VarSet Any
    -> VarSet
    -> (Type -> Any, [Type] -> Any, Coercion -> Any, [Coercion] -> Any)
    forall a env.
    Monoid a =>
    TyCoFolder env a
    -> env -> (Type -> a, [Type] -> a, Coercion -> a, [Coercion] -> a)
    foldTyCo (InterestingVarFun -> TyCoFolder VarSet Any
    afvFolder (Bool -> InterestingVarFun
    forall a b. a -> b -> a
    const Bool
    True)) VarSet
    emptyVarSet

    noFreeVarsOfCo :: Coercion -> Bool
    noFreeVarsOfCo :: Coercion -> Bool
    noFreeVarsOfCo Coercion
    co = Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ Any -> Bool
    DM.getAny (Coercion -> Any
    f Coercion
    co)
      where (Type -> Any
    _, [Type] -> Any
    _, Coercion -> Any
    f, [Coercion] -> Any
    _) = TyCoFolder VarSet Any
    -> VarSet
    -> (Type -> Any, [Type] -> Any, Coercion -> Any, [Coercion] -> Any)
    forall a env.
    Monoid a =>
    TyCoFolder env a
    -> env -> (Type -> a, [Type] -> a, Coercion -> a, [Coercion] -> a)
    foldTyCo (InterestingVarFun -> TyCoFolder VarSet Any
    afvFolder (Bool -> InterestingVarFun
    forall a b. a -> b -> a
    const Bool
    True)) VarSet
    emptyVarSet

    {- *********************************************************************
    *                                                                      *
                     scopedSort
    *                                                                      *
    ********************************************************************* -}

    {- Note [ScopedSort]
    ~~~~~~~~~~~~~~~~~~~~
    Consider

      foo :: Proxy a -> Proxy (b :: k) -> Proxy (a :: k2) -> ()

    This function type is implicitly generalised over [a, b, k, k2]. These
    variables will be Specified; that is, they will be available for visible
    type application. This is because they are written in the type signature
    by the user.

    However, we must ask: what order will they appear in? In cases without
    dependency, this is easy: we just use the lexical left-to-right ordering
    of first occurrence. With dependency, we cannot get off the hook so
    easily.

    We thus state:

     * These variables appear in the order as given by ScopedSort, where
       the input to ScopedSort is the left-to-right order of first occurrence.

    Note that this applies only to *implicit* quantification, without a
    `forall`. If the user writes a `forall`, then we just use the order given.

    ScopedSort is defined thusly (as proposed in #15743):
      * Work left-to-right through the input list, with a cursor.
      * If variable v at the cursor is depended on by any earlier variable w,
        move v immediately before the leftmost such w.

    INVARIANT: The prefix of variables before the cursor form a valid telescope.

    Note that ScopedSort makes sense only after type inference is done and all
    types/kinds are fully settled and zonked.

    -}

    -- | Do a topological sort on a list of tyvars,
    --   so that binders occur before occurrences
    -- E.g. given  [ a::k, k::*, b::k ]
    -- it'll return a well-scoped list [ k::*, a::k, b::k ]
    --
    -- This is a deterministic sorting operation
    -- (that is, doesn't depend on Uniques).
    --
    -- It is also meant to be stable: that is, variables should not
    -- be reordered unnecessarily. This is specified in Note [ScopedSort]
    -- See also Note [Ordering of implicit variables] in "GHC.Rename.HsType"

    scopedSort :: [TyCoVar] -> [TyCoVar]
    scopedSort :: [Var] -> [Var]
    scopedSort = [Var] -> [VarSet] -> [Var] -> [Var]
    go [] []
      where
        go :: [TyCoVar] -- already sorted, in reverse order
           -> [TyCoVarSet] -- each set contains all the variables which must be placed
                           -- before the tv corresponding to the set; they are accumulations
                           -- of the fvs in the sorted tvs' kinds

                           -- This list is in 1-to-1 correspondence with the sorted tyvars
                           -- INVARIANT:
                           --   all (\tl -> all (`subVarSet` head tl) (tail tl)) (tails fv_list)
                           -- That is, each set in the list is a superset of all later sets.

           -> [TyCoVar] -- yet to be sorted
           -> [TyCoVar]
        go :: [Var] -> [VarSet] -> [Var] -> [Var]
    go [Var]
    acc [VarSet]
    _fv_list [] = [Var] -> [Var]
    forall a. [a] -> [a]
    reverse [Var]
    acc
        go [Var]
    acc  [VarSet]
    fv_list (Var
    tv:[Var]
    tvs)
          = [Var] -> [VarSet] -> [Var] -> [Var]
    go [Var]
    acc' [VarSet]
    fv_list' [Var]
    tvs
          where
            ([Var]
    acc', [VarSet]
    fv_list') = Var -> [Var] -> [VarSet] -> ([Var], [VarSet])
    insert Var
    tv [Var]
    acc [VarSet]
    fv_list

        insert :: TyCoVar       -- var to insert
               -> [TyCoVar]     -- sorted list, in reverse order
               -> [TyCoVarSet]  -- list of fvs, as above
               -> ([TyCoVar], [TyCoVarSet])   -- augmented lists
        insert :: Var -> [Var] -> [VarSet] -> ([Var], [VarSet])
    insert Var
    tv []     []         = ([Var
    tv], [Type -> VarSet
    tyCoVarsOfType (Var -> Type
    tyVarKind Var
    tv)])
        insert Var
    tv (Var
    a:[Var]
    as) (VarSet
    fvs:[VarSet]
    fvss)
          | Var
    tv Var -> VarSet -> Bool
    `elemVarSet` VarSet
    fvs
          , ([Var]
    as', [VarSet]
    fvss') <- Var -> [Var] -> [VarSet] -> ([Var], [VarSet])
    insert Var
    tv [Var]
    as [VarSet]
    fvss
          = (Var
    aVar -> [Var] -> [Var]
    forall a. a -> [a] -> [a]
    :[Var]
    as', VarSet
    fvs VarSet -> VarSet -> VarSet
    `unionVarSet` VarSet
    fv_tv VarSet -> [VarSet] -> [VarSet]
    forall a. a -> [a] -> [a]
    : [VarSet]
    fvss')

          | Bool
    otherwise
          = (Var
    tvVar -> [Var] -> [Var]
    forall a. a -> [a] -> [a]
    :Var
    aVar -> [Var] -> [Var]
    forall a. a -> [a] -> [a]
    :[Var]
    as, VarSet
    fvs VarSet -> VarSet -> VarSet
    `unionVarSet` VarSet
    fv_tv VarSet -> [VarSet] -> [VarSet]
    forall a. a -> [a] -> [a]
    : VarSet
    fvs VarSet -> [VarSet] -> [VarSet]
    forall a. a -> [a] -> [a]
    : [VarSet]
    fvss)
          where
            fv_tv :: VarSet
    fv_tv = Type -> VarSet
    tyCoVarsOfType (Var -> Type
    tyVarKind Var
    tv)

           -- lists not in correspondence
        insert Var
    _ [Var]
    _ [VarSet]
    _ = String -> ([Var], [VarSet])
    forall a. HasCallStack => String -> a
    panic String
    "scopedSort"

    -- | Get the free vars of a type in scoped order
    tyCoVarsOfTypeWellScoped :: Type -> [TyVar]
    tyCoVarsOfTypeWellScoped :: Type -> [Var]
    tyCoVarsOfTypeWellScoped = [Var] -> [Var]
    scopedSort ([Var] -> [Var]) -> (Type -> [Var]) -> Type -> [Var]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Type -> [Var]
    tyCoVarsOfTypeList

    -- | Get the free vars of types in scoped order
    tyCoVarsOfTypesWellScoped :: [Type] -> [TyVar]
    tyCoVarsOfTypesWellScoped :: [Type] -> [Var]
    tyCoVarsOfTypesWellScoped = [Var] -> [Var]
    scopedSort ([Var] -> [Var]) -> ([Type] -> [Var]) -> [Type] -> [Var]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Type] -> [Var]
    tyCoVarsOfTypesList

    {-
    ************************************************************************
    *                                                                      *
                Free type constructors
    *                                                                      *
    ************************************************************************
    -}

    {- Note [tyConsOfType]
    ~~~~~~~~~~~~~~~~~~~~~~
    It is slightly odd to find the TyCons of a type.  Especially since, via a type
    family reduction or axiom, a type that doesn't mention T might start to mention T.

    This function is used in only three places:
    * In GHC.Tc.Validity.validDerivPred, when identifying "exotic" predicates.
    * In GHC.Tc.Errors.Ppr.pprTcSolverReportMsg, when trying to print a helpful
      error about overlapping instances
    * In utils/dump-decls/Main.hs, an ill-documented module.

    None seem critical. Currently tyConsOfType looks inside coercions, but perhaps
    it doesn't even need to do that.
    -}

    -- | All type constructors occurring in the type; looking through type
    --   synonyms, but not newtypes.
    --  When it finds a Class, it returns the class TyCon.
    tyConsOfType :: Type -> UniqSet TyCon
    tyConsOfType :: Type -> UniqSet TyCon
    tyConsOfType Type
    ty
      = Type -> UniqSet TyCon
    go Type
    ty
      where
         go :: Type -> UniqSet TyCon  -- The UniqSet does duplicate elim
         go :: Type -> UniqSet TyCon
    go Type
    ty | Just Type
    ty' <- Type -> Maybe Type
    coreView Type
    ty = Type -> UniqSet TyCon
    go Type
    ty'
         go (TyVarTy {})                = UniqSet TyCon
    forall a. UniqSet a
    emptyUniqSet
         go (LitTy {})                  = UniqSet TyCon
    forall a. UniqSet a
    emptyUniqSet
         go (TyConApp TyCon
    tc [Type]
    tys)           = TyCon -> UniqSet TyCon
    forall {a}. Uniquable a => a -> UniqSet a
    go_tc TyCon
    tc UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
    forall a. UniqSet a -> UniqSet a -> UniqSet a
    `unionUniqSets` [Type] -> UniqSet TyCon
    tyConsOfTypes [Type]
    tys
         go (AppTy Type
    a Type
    b)                 = Type -> UniqSet TyCon
    go Type
    a UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
    forall a. UniqSet a -> UniqSet a -> UniqSet a
    `unionUniqSets` Type -> UniqSet TyCon
    go Type
    b
         go (FunTy FunTyFlag
    af Type
    w Type
    a Type
    b)            = Type -> UniqSet TyCon
    go Type
    w UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
    forall a. UniqSet a -> UniqSet a -> UniqSet a
    `unionUniqSets`
                                          Type -> UniqSet TyCon
    go Type
    a UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
    forall a. UniqSet a -> UniqSet a -> UniqSet a
    `unionUniqSets` Type -> UniqSet TyCon
    go Type
    b
                                          UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
    forall a. UniqSet a -> UniqSet a -> UniqSet a
    `unionUniqSets` TyCon -> UniqSet TyCon
    forall {a}. Uniquable a => a -> UniqSet a
    go_tc (FunTyFlag -> TyCon
    funTyFlagTyCon FunTyFlag
    af)
         go (ForAllTy (Bndr Var
    tv ForAllTyFlag
    _) Type
    ty)   = Type -> UniqSet TyCon
    go Type
    ty UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
    forall a. UniqSet a -> UniqSet a -> UniqSet a
    `unionUniqSets` Type -> UniqSet TyCon
    go (Var -> Type
    varType Var
    tv)
         go (CastTy Type
    ty Coercion
    co)              = Type -> UniqSet TyCon
    go Type
    ty UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
    forall a. UniqSet a -> UniqSet a -> UniqSet a
    `unionUniqSets` Coercion -> UniqSet TyCon
    go_co Coercion
    co
         go (CoercionTy Coercion
    co)             = Coercion -> UniqSet TyCon
    go_co Coercion
    co

         go_co :: Coercion -> UniqSet TyCon
    go_co (Refl Type
    ty)               = Type -> UniqSet TyCon
    go Type
    ty
         go_co (GRefl Role
    _ Type
    ty MCoercion
    mco)        = Type -> UniqSet TyCon
    go Type
    ty UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
    forall a. UniqSet a -> UniqSet a -> UniqSet a
    `unionUniqSets` MCoercion -> UniqSet TyCon
    go_mco MCoercion
    mco
         go_co (TyConAppCo Role
    _ TyCon
    tc [Coercion]
    args)  = TyCon -> UniqSet TyCon
    forall {a}. Uniquable a => a -> UniqSet a
    go_tc TyCon
    tc UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
    forall a. UniqSet a -> UniqSet a -> UniqSet a
    `unionUniqSets` [Coercion] -> UniqSet TyCon
    go_cos [Coercion]
    args
         go_co (AppCo Coercion
    co Coercion
    arg)          = Coercion -> UniqSet TyCon
    go_co Coercion
    co UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
    forall a. UniqSet a -> UniqSet a -> UniqSet a
    `unionUniqSets` Coercion -> UniqSet TyCon
    go_co Coercion
    arg
         go_co (ForAllCo { fco_kind :: Coercion -> Coercion
    fco_kind = Coercion
    kind_co, fco_body :: Coercion -> Coercion
    fco_body = Coercion
    co })
                                       = Coercion -> UniqSet TyCon
    go_co Coercion
    kind_co UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
    forall a. UniqSet a -> UniqSet a -> UniqSet a
    `unionUniqSets` Coercion -> UniqSet TyCon
    go_co Coercion
    co
         go_co (FunCo { fco_mult :: Coercion -> Coercion
    fco_mult = Coercion
    m, fco_arg :: Coercion -> Coercion
    fco_arg = Coercion
    a, fco_res :: Coercion -> Coercion
    fco_res = Coercion
    r })
                                       = Coercion -> UniqSet TyCon
    go_co Coercion
    m UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
    forall a. UniqSet a -> UniqSet a -> UniqSet a
    `unionUniqSets` Coercion -> UniqSet TyCon
    go_co Coercion
    a UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
    forall a. UniqSet a -> UniqSet a -> UniqSet a
    `unionUniqSets` Coercion -> UniqSet TyCon
    go_co Coercion
    r
         go_co (AxiomCo CoAxiomRule
    ax [Coercion]
    args)       = CoAxiomRule -> UniqSet TyCon
    go_ax CoAxiomRule
    ax UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
    forall a. UniqSet a -> UniqSet a -> UniqSet a
    `unionUniqSets` [Coercion] -> UniqSet TyCon
    go_cos [Coercion]
    args
         go_co (UnivCo { uco_lty :: Coercion -> Type
    uco_lty = Type
    t1, uco_rty :: Coercion -> Type
    uco_rty = Type
    t2, uco_deps :: Coercion -> [Coercion]
    uco_deps = [Coercion]
    cos })
                                       = Type -> UniqSet TyCon
    go Type
    t1 UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
    forall a. UniqSet a -> UniqSet a -> UniqSet a
    `unionUniqSets` Type -> UniqSet TyCon
    go Type
    t2 UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
    forall a. UniqSet a -> UniqSet a -> UniqSet a
    `unionUniqSets` [Coercion] -> UniqSet TyCon
    go_cos [Coercion]
    cos
         go_co (CoVarCo {})            = UniqSet TyCon
    forall a. UniqSet a
    emptyUniqSet
         go_co (HoleCo {})             = UniqSet TyCon
    forall a. UniqSet a
    emptyUniqSet
         go_co (SymCo Coercion
    co)              = Coercion -> UniqSet TyCon
    go_co Coercion
    co
         go_co (TransCo Coercion
    co1 Coercion
    co2)       = Coercion -> UniqSet TyCon
    go_co Coercion
    co1 UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
    forall a. UniqSet a -> UniqSet a -> UniqSet a
    `unionUniqSets` Coercion -> UniqSet TyCon
    go_co Coercion
    co2
         go_co (SelCo CoSel
    _ Coercion
    co)            = Coercion -> UniqSet TyCon
    go_co Coercion
    co
         go_co (LRCo LeftOrRight
    _ Coercion
    co)             = Coercion -> UniqSet TyCon
    go_co Coercion
    co
         go_co (InstCo Coercion
    co Coercion
    arg)         = Coercion -> UniqSet TyCon
    go_co Coercion
    co UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
    forall a. UniqSet a -> UniqSet a -> UniqSet a
    `unionUniqSets` Coercion -> UniqSet TyCon
    go_co Coercion
    arg
         go_co (KindCo Coercion
    co)             = Coercion -> UniqSet TyCon
    go_co Coercion
    co
         go_co (SubCo Coercion
    co)              = Coercion -> UniqSet TyCon
    go_co Coercion
    co

         go_mco :: MCoercion -> UniqSet TyCon
    go_mco MCoercion
    MRefl    = UniqSet TyCon
    forall a. UniqSet a
    emptyUniqSet
         go_mco (MCo Coercion
    co) = Coercion -> UniqSet TyCon
    go_co Coercion
    co

         go_cos :: [Coercion] -> UniqSet TyCon
    go_cos [Coercion]
    cos   = (Coercion -> UniqSet TyCon -> UniqSet TyCon)
    -> UniqSet TyCon -> [Coercion] -> UniqSet TyCon
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr (UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
    forall a. UniqSet a -> UniqSet a -> UniqSet a
    unionUniqSets (UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon)
    -> (Coercion -> UniqSet TyCon)
    -> Coercion
    -> UniqSet TyCon
    -> UniqSet TyCon
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Coercion -> UniqSet TyCon
    go_co)  UniqSet TyCon
    forall a. UniqSet a
    emptyUniqSet [Coercion]
    cos

         go_tc :: a -> UniqSet a
    go_tc a
    tc = a -> UniqSet a
    forall {a}. Uniquable a => a -> UniqSet a
    unitUniqSet a
    tc

         go_ax :: CoAxiomRule -> UniqSet TyCon
    go_ax (UnbranchedAxiom CoAxiom Unbranched
    ax) = TyCon -> UniqSet TyCon
    forall {a}. Uniquable a => a -> UniqSet a
    go_tc (TyCon -> UniqSet TyCon) -> TyCon -> UniqSet TyCon
    forall a b. (a -> b) -> a -> b
    $ CoAxiom Unbranched -> TyCon
    forall (br :: BranchFlag). CoAxiom br -> TyCon
    coAxiomTyCon CoAxiom Unbranched
    ax
         go_ax (BranchedAxiom CoAxiom Branched
    ax BranchIndex
    _) = TyCon -> UniqSet TyCon
    forall {a}. Uniquable a => a -> UniqSet a
    go_tc (TyCon -> UniqSet TyCon) -> TyCon -> UniqSet TyCon
    forall a b. (a -> b) -> a -> b
    $ CoAxiom Branched -> TyCon
    forall (br :: BranchFlag). CoAxiom br -> TyCon
    coAxiomTyCon CoAxiom Branched
    ax
         go_ax (BuiltInFamRew  BuiltInFamRewrite
    bif) = TyCon -> UniqSet TyCon
    forall {a}. Uniquable a => a -> UniqSet a
    go_tc (TyCon -> UniqSet TyCon) -> TyCon -> UniqSet TyCon
    forall a b. (a -> b) -> a -> b
    $ BuiltInFamRewrite -> TyCon
    bifrw_fam_tc BuiltInFamRewrite
    bif
         go_ax (BuiltInFamInj {})   = UniqSet TyCon
    forall a. UniqSet a
    emptyUniqSet  -- A free-floating axiom

    tyConsOfTypes :: [Type] -> UniqSet TyCon
    tyConsOfTypes :: [Type] -> UniqSet TyCon
    tyConsOfTypes [Type]
    tys = (Type -> UniqSet TyCon -> UniqSet TyCon)
    -> UniqSet TyCon -> [Type] -> UniqSet TyCon
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr (UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
    forall a. UniqSet a -> UniqSet a -> UniqSet a
    unionUniqSets (UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon)
    -> (Type -> UniqSet TyCon)
    -> Type
    -> UniqSet TyCon
    -> UniqSet TyCon
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Type -> UniqSet TyCon
    tyConsOfType) UniqSet TyCon
    forall a. UniqSet a
    emptyUniqSet [Type]
    tys

    {- **********************************************************************
    *                                                                       *
               Occurs check expansion
    %*                                                                      *
    %********************************************************************* -}

    {- Note [Occurs check expansion]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    (occurCheckExpand tv xi) expands synonyms in xi just enough to get rid
    of occurrences of tv outside type function arguments, if that is
    possible; otherwise, it returns Nothing.

    For example, suppose we have
      type F a b = [a]
    Then
      occCheckExpand b (F Int b) = Just [Int]
    but
      occCheckExpand a (F a Int) = Nothing

    We don't promise to do the absolute minimum amount of expanding
    necessary, but we try not to do expansions we don't need to.  We
    prefer doing inner expansions first.  For example,
      type F a b = (a, Int, a, [a])
      type G b   = Char
    We have
      occCheckExpand b (F (G b)) = Just (F Char)
    even though we could also expand F to get rid of b.

    Note [Occurrence checking: look inside kinds]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    Suppose we are considering unifying
       (alpha :: *)  ~  Int -> (beta :: alpha -> alpha)
    This may be an error (what is that alpha doing inside beta's kind?),
    but we must not make the mistake of actually unifying or we'll
    build an infinite data structure.  So when looking for occurrences
    of alpha in the rhs, we must look in the kinds of type variables
    that occur there.

    occCheckExpand tries to expand type synonyms to remove
    unnecessary occurrences of a variable, and thereby get past an
    occurs-check failure.  This is good; but
         we can't do it in the /kind/ of a variable /occurrence/

    For example #18451 built an infinite type:
        type Const a b = a
        data SameKind :: k -> k -> Type
        type T (k :: Const Type a) = forall (b :: k). SameKind a b

    We have
      b :: k
      k :: Const Type a
      a :: k   (must be same as b)

    So if we aren't careful, a's kind mentions a, which is bad.
    And expanding an /occurrence/ of 'a' doesn't help, because the
    /binding site/ is the master copy and all the occurrences should
    match it.

    Here's a related example:
       f :: forall a b (c :: Const Type b). Proxy '[a, c]

    The list means that 'a' gets the same kind as 'c'; but that
    kind mentions 'b', so the binders are out of order.

    Bottom line: in occCheckExpand, do not expand inside the kinds
    of occurrences.  See bad_var_occ in occCheckExpand.  And
    see #18451 for more debate.
    -}

    occCheckExpand :: [Var] -> Type -> Maybe Type
    -- See Note [Occurs check expansion]
    -- We may have needed to do some type synonym unfolding in order to
    -- get rid of the variable (or forall), so we also return the unfolded
    -- version of the type, which is guaranteed to be syntactically free
    -- of the given type variable.  If the type is already syntactically
    -- free of the variable, then the same type is returned.
    occCheckExpand :: [Var] -> Type -> Maybe Type
    occCheckExpand [Var]
    vs_to_avoid Type
    ty
      | [Var] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [Var]
    vs_to_avoid  -- Efficient shortcut
      = Type -> Maybe Type
    forall a. a -> Maybe a
    Just Type
    ty           -- Can happen, eg. GHC.Core.Utils.mkSingleAltCase

      | Bool
    otherwise
      = (VarSet, VarEnv Var) -> Type -> Maybe Type
    go ([Var] -> VarSet
    mkVarSet [Var]
    vs_to_avoid, VarEnv Var
    forall a. VarEnv a
    emptyVarEnv) Type
    ty
      where
        go :: (VarSet, VarEnv TyCoVar) -> Type -> Maybe Type
              -- The VarSet is the set of variables we are trying to avoid
              -- The VarEnv carries mappings necessary
              -- because of kind expansion
        go :: (VarSet, VarEnv Var) -> Type -> Maybe Type
    go (VarSet
    as, VarEnv Var
    env) ty :: Type
    ty@(TyVarTy Var
    tv)
          | Just Var
    tv' <- VarEnv Var -> Var -> Maybe Var
    forall a. VarEnv a -> Var -> Maybe a
    lookupVarEnv VarEnv Var
    env Var
    tv = Type -> Maybe Type
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Var -> Type
    mkTyVarTy Var
    tv')
          | VarSet -> InterestingVarFun
    bad_var_occ VarSet
    as Var
    tv               = Maybe Type
    forall a. Maybe a
    Nothing
          | Bool
    otherwise                       = Type -> Maybe Type
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Type
    ty

        go (VarSet, VarEnv Var)
    _   ty :: Type
    ty@(LitTy {}) = Type -> Maybe Type
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Type
    ty
        go (VarSet, VarEnv Var)
    cxt (AppTy Type
    ty1 Type
    ty2) = do { ty1' <- (VarSet, VarEnv Var) -> Type -> Maybe Type
    go (VarSet, VarEnv Var)
    cxt Type
    ty1
                                    ; ty2' <- go cxt ty2
                                    ; return (AppTy ty1' ty2') }
        go (VarSet, VarEnv Var)
    cxt ty :: Type
    ty@(FunTy FunTyFlag
    _ Type
    w Type
    ty1 Type
    ty2)
           = do { w'   <- (VarSet, VarEnv Var) -> Type -> Maybe Type
    go (VarSet, VarEnv Var)
    cxt Type
    w
                ; ty1' <- go cxt ty1
                ; ty2' <- go cxt ty2
                ; return (ty { ft_mult = w', ft_arg = ty1', ft_res = ty2' }) }
        go cxt :: (VarSet, VarEnv Var)
    cxt@(VarSet
    as, VarEnv Var
    env) (ForAllTy (Bndr Var
    tv ForAllTyFlag
    vis) Type
    body_ty)
           = do { ki' <- (VarSet, VarEnv Var) -> Type -> Maybe Type
    go (VarSet, VarEnv Var)
    cxt (Var -> Type
    varType Var
    tv)
                ; let tv'  = Var -> Type -> Var
    setVarType Var
    tv Type
    ki'
                      env' = VarEnv Var -> Var -> Var -> VarEnv Var
    forall a. VarEnv a -> Var -> a -> VarEnv a
    extendVarEnv VarEnv Var
    env Var
    tv Var
    tv'
                      as'  = VarSet
    as VarSet -> Var -> VarSet
    `delVarSet` Var
    tv
                ; body' <- go (as', env') body_ty
                ; return (ForAllTy (Bndr tv' vis) body') }

        -- For a type constructor application, first try expanding away the
        -- offending variable from the arguments.  If that doesn't work, next
        -- see if the type constructor is a type synonym, and if so, expand
        -- it and try again.
        go (VarSet, VarEnv Var)
    cxt ty :: Type
    ty@(TyConApp TyCon
    tc [Type]
    tys)
          = case (Type -> Maybe Type) -> [Type] -> Maybe [Type]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM ((VarSet, VarEnv Var) -> Type -> Maybe Type
    go (VarSet, VarEnv Var)
    cxt) [Type]
    tys of
              Just [Type]
    tys' -> Type -> Maybe Type
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (TyCon -> [Type] -> Type
    TyConApp TyCon
    tc [Type]
    tys')
              Maybe [Type]
    Nothing | Just Type
    ty' <- Type -> Maybe Type
    coreView Type
    ty -> (VarSet, VarEnv Var) -> Type -> Maybe Type
    go (VarSet, VarEnv Var)
    cxt Type
    ty'
                      | Bool
    otherwise               -> Maybe Type
    forall a. Maybe a
    Nothing
                          -- Failing that, try to expand a synonym

        go (VarSet, VarEnv Var)
    cxt (CastTy Type
    ty Coercion
    co) =  do { ty' <- (VarSet, VarEnv Var) -> Type -> Maybe Type
    go (VarSet, VarEnv Var)
    cxt Type
    ty
                                    ; co' <- go_co cxt co
                                    ; return (CastTy ty' co') }
        go (VarSet, VarEnv Var)
    cxt (CoercionTy Coercion
    co) = do { co' <- (VarSet, VarEnv Var) -> Coercion -> Maybe Coercion
    go_co (VarSet, VarEnv Var)
    cxt Coercion
    co
                                    ; return (CoercionTy co') }

        ------------------
        bad_var_occ :: VarSet -> Var -> Bool
        -- Works for TyVar and CoVar
        -- See Note [Occurrence checking: look inside kinds]
        bad_var_occ :: VarSet -> InterestingVarFun
    bad_var_occ VarSet
    vs_to_avoid Var
    v
           =  Var
    v                          Var -> VarSet -> Bool
    `elemVarSet`       VarSet
    vs_to_avoid
           Bool -> Bool -> Bool
    || Type -> VarSet
    tyCoVarsOfType (Var -> Type
    varType Var
    v) VarSet -> VarSet -> Bool
    `intersectsVarSet` VarSet
    vs_to_avoid

        ------------------
        go_mco :: (VarSet, VarEnv Var) -> MCoercion -> Maybe MCoercion
    go_mco (VarSet, VarEnv Var)
    _   MCoercion
    MRefl = MCoercion -> Maybe MCoercion
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return MCoercion
    MRefl
        go_mco (VarSet, VarEnv Var)
    ctx (MCo Coercion
    co) = Coercion -> MCoercion
    MCo (Coercion -> MCoercion) -> Maybe Coercion -> Maybe MCoercion
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (VarSet, VarEnv Var) -> Coercion -> Maybe Coercion
    go_co (VarSet, VarEnv Var)
    ctx Coercion
    co

        ------------------
        go_co :: (VarSet, VarEnv Var) -> Coercion -> Maybe Coercion
    go_co (VarSet, VarEnv Var)
    cxt (Refl Type
    ty)                 = do { ty' <- (VarSet, VarEnv Var) -> Type -> Maybe Type
    go (VarSet, VarEnv Var)
    cxt Type
    ty
                                                 ; return (Refl ty') }
        go_co (VarSet, VarEnv Var)
    cxt (GRefl Role
    r Type
    ty MCoercion
    mco)          = do { mco' <- (VarSet, VarEnv Var) -> MCoercion -> Maybe MCoercion
    go_mco (VarSet, VarEnv Var)
    cxt MCoercion
    mco
                                                 ; ty' <- go cxt ty
                                                 ; return (GRefl r ty' mco') }
          -- Note: Coercions do not contain type synonyms
        go_co (VarSet, VarEnv Var)
    cxt (TyConAppCo Role
    r TyCon
    tc [Coercion]
    args)    = do { args' <- (Coercion -> Maybe Coercion) -> [Coercion] -> Maybe [Coercion]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM ((VarSet, VarEnv Var) -> Coercion -> Maybe Coercion
    go_co (VarSet, VarEnv Var)
    cxt) [Coercion]
    args
                                                 ; return (TyConAppCo r tc args') }
        go_co (VarSet, VarEnv Var)
    cxt (AppCo Coercion
    co Coercion
    arg)            = do { co' <- (VarSet, VarEnv Var) -> Coercion -> Maybe Coercion
    go_co (VarSet, VarEnv Var)
    cxt Coercion
    co
                                                 ; arg' <- go_co cxt arg
                                                 ; return (AppCo co' arg') }
        go_co (VarSet, VarEnv Var)
    cxt (SymCo Coercion
    co)                = do { co' <- (VarSet, VarEnv Var) -> Coercion -> Maybe Coercion
    go_co (VarSet, VarEnv Var)
    cxt Coercion
    co
                                                 ; return (SymCo co') }
        go_co (VarSet, VarEnv Var)
    cxt (TransCo Coercion
    co1 Coercion
    co2)         = do { co1' <- (VarSet, VarEnv Var) -> Coercion -> Maybe Coercion
    go_co (VarSet, VarEnv Var)
    cxt Coercion
    co1
                                                 ; co2' <- go_co cxt co2
                                                 ; return (TransCo co1' co2') }
        go_co (VarSet, VarEnv Var)
    cxt (SelCo CoSel
    n Coercion
    co)              = do { co' <- (VarSet, VarEnv Var) -> Coercion -> Maybe Coercion
    go_co (VarSet, VarEnv Var)
    cxt Coercion
    co
                                                 ; return (SelCo n co') }
        go_co (VarSet, VarEnv Var)
    cxt (LRCo LeftOrRight
    lr Coercion
    co)              = do { co' <- (VarSet, VarEnv Var) -> Coercion -> Maybe Coercion
    go_co (VarSet, VarEnv Var)
    cxt Coercion
    co
                                                 ; return (LRCo lr co') }
        go_co (VarSet, VarEnv Var)
    cxt (InstCo Coercion
    co Coercion
    arg)           = do { co' <- (VarSet, VarEnv Var) -> Coercion -> Maybe Coercion
    go_co (VarSet, VarEnv Var)
    cxt Coercion
    co
                                                 ; arg' <- go_co cxt arg
                                                 ; return (InstCo co' arg') }
        go_co (VarSet, VarEnv Var)
    cxt (KindCo Coercion
    co)               = do { co' <- (VarSet, VarEnv Var) -> Coercion -> Maybe Coercion
    go_co (VarSet, VarEnv Var)
    cxt Coercion
    co
                                                 ; return (KindCo co') }
        go_co (VarSet, VarEnv Var)
    cxt (SubCo Coercion
    co)                = do { co' <- (VarSet, VarEnv Var) -> Coercion -> Maybe Coercion
    go_co (VarSet, VarEnv Var)
    cxt Coercion
    co
                                                 ; return (SubCo co') }

        go_co cxt :: (VarSet, VarEnv Var)
    cxt@(VarSet
    as, VarEnv Var
    env) co :: Coercion
    co@(ForAllCo { fco_tcv :: Coercion -> Var
    fco_tcv = Var
    tv, fco_kind :: Coercion -> Coercion
    fco_kind = Coercion
    kind_co, fco_body :: Coercion -> Coercion
    fco_body = Coercion
    body_co })
          = do { kind_co' <- (VarSet, VarEnv Var) -> Coercion -> Maybe Coercion
    go_co (VarSet, VarEnv Var)
    cxt Coercion
    kind_co
               ; let tv' = Var -> Type -> Var
    setVarType Var
    tv (Type -> Var) -> Type -> Var
    forall a b. (a -> b) -> a -> b
    $
                           HasDebugCallStack => Coercion -> Type
    Coercion -> Type
    coercionLKind Coercion
    kind_co'
                     env' = VarEnv Var -> Var -> Var -> VarEnv Var
    forall a. VarEnv a -> Var -> a -> VarEnv a
    extendVarEnv VarEnv Var
    env Var
    tv Var
    tv'
                     as'  = VarSet
    as VarSet -> Var -> VarSet
    `delVarSet` Var
    tv
               ; body' <- go_co (as', env') body_co
               ; return (co { fco_tcv = tv', fco_kind = kind_co', fco_body = body' }) }

        go_co (VarSet, VarEnv Var)
    cxt co :: Coercion
    co@(FunCo { fco_mult :: Coercion -> Coercion
    fco_mult = Coercion
    w, fco_arg :: Coercion -> Coercion
    fco_arg = Coercion
    co1 ,fco_res :: Coercion -> Coercion
    fco_res = Coercion
    co2 })
          = do { co1' <- (VarSet, VarEnv Var) -> Coercion -> Maybe Coercion
    go_co (VarSet, VarEnv Var)
    cxt Coercion
    co1
               ; co2' <- go_co cxt co2
               ; w' <- go_co cxt w
               ; return (co { fco_mult = w', fco_arg = co1', fco_res = co2' })}

        go_co (VarSet
    as,VarEnv Var
    env) co :: Coercion
    co@(CoVarCo Var
    c)
          | Just Var
    c' <- VarEnv Var -> Var -> Maybe Var
    forall a. VarEnv a -> Var -> Maybe a
    lookupVarEnv VarEnv Var
    env Var
    c   = Coercion -> Maybe Coercion
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Var -> Coercion
    CoVarCo Var
    c')
          | VarSet -> InterestingVarFun
    bad_var_occ VarSet
    as Var
    c                = Maybe Coercion
    forall a. Maybe a
    Nothing
          | Bool
    otherwise                       = Coercion -> Maybe Coercion
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Coercion
    co

        go_co (VarSet
    as,VarEnv Var
    _) co :: Coercion
    co@(HoleCo CoercionHole
    h)
          | VarSet -> InterestingVarFun
    bad_var_occ VarSet
    as (CoercionHole -> Var
    ch_co_var CoercionHole
    h)    = Maybe Coercion
    forall a. Maybe a
    Nothing
          | Bool
    otherwise                       = Coercion -> Maybe Coercion
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Coercion
    co

        go_co (VarSet, VarEnv Var)
    cxt (AxiomCo CoAxiomRule
    ax [Coercion]
    cs)           = do { cs' <- (Coercion -> Maybe Coercion) -> [Coercion] -> Maybe [Coercion]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM ((VarSet, VarEnv Var) -> Coercion -> Maybe Coercion
    go_co (VarSet, VarEnv Var)
    cxt) [Coercion]
    cs
                                                 ; return (AxiomCo ax cs') }
        go_co (VarSet, VarEnv Var)
    cxt co :: Coercion
    co@(UnivCo { uco_lty :: Coercion -> Type
    uco_lty = Type
    ty1, uco_rty :: Coercion -> Type
    uco_rty = Type
    ty2, uco_deps :: Coercion -> [Coercion]
    uco_deps = [Coercion]
    cos })
          = do { ty1' <- (VarSet, VarEnv Var) -> Type -> Maybe Type
    go (VarSet, VarEnv Var)
    cxt Type
    ty1
               ; ty2' <- go cxt ty2
               ; cos' <- mapM (go_co cxt) cos
               ; return (co { uco_lty = ty1', uco_rty = ty2', uco_deps = cos' }) }