    -- (c) The University of Glasgow 2006

    {-# LANGUAGE ScopedTypeVariables, PatternSynonyms, MultiWayIf #-}

    {-# LANGUAGE DeriveFunctor #-}

    module GHC.Core.Unify (
            tcMatchTy, tcMatchTyKi,
            tcMatchTys, tcMatchTyKis,
            tcMatchTyX, tcMatchTysX, tcMatchTyKisX,
            tcMatchTyX_BM, ruleMatchTyKiX,

            -- Side-effect free unification
            tcUnifyTy, tcUnifyTyKi, tcUnifyTys, tcUnifyTyKis,
            tcUnifyTysFG, tcUnifyTyWithTFs,
            BindFun, BindFlag(..), matchBindFun, alwaysBindFun,
            UnifyResult, UnifyResultM(..), MaybeApartReason(..),
            typesCantMatch, typesAreApart,

            -- Matching a type against a lifted type (coercion)
            liftCoMatch,

            -- The core flattening algorithm
            flattenTys, flattenTysX,

       ) where

    import GHC.Prelude

    import GHC.Types.Var
    import GHC.Types.Var.Env
    import GHC.Types.Var.Set
    import GHC.Types.Name( Name, mkSysTvName, mkSystemVarName )
    import GHC.Builtin.Names( tYPETyConKey, cONSTRAINTTyConKey )
    import GHC.Core.Type     hiding ( getTvSubstEnv )
    import GHC.Core.Coercion hiding ( getCvSubstEnv )
    import GHC.Core.TyCon
    import GHC.Core.TyCo.Rep
    import GHC.Core.TyCo.Compare ( eqType, tcEqType )
    import GHC.Core.TyCo.FVs     ( tyCoVarsOfCoList, tyCoFVsOfTypes )
    import GHC.Core.TyCo.Subst   ( mkTvSubst, emptyIdSubstEnv )
    import GHC.Core.Map.Type
    import GHC.Utils.FV( FV, fvVarList )
    import GHC.Utils.Misc
    import GHC.Data.Pair
    import GHC.Utils.Outputable
    import GHC.Types.Unique
    import GHC.Types.Unique.FM
    import GHC.Types.Unique.Set
    import GHC.Exts( oneShot )
    import GHC.Utils.Panic
    import GHC.Data.FastString

    import Data.List ( mapAccumL )
    import Control.Monad
    import qualified Data.Semigroup as S
    import GHC.Builtin.Types.Prim (fUNTyCon)
    import GHC.Core.Multiplicity

    {-

    Unification is much tricker than you might think.

    1. The substitution we generate binds the *template type variables*
       which are given to us explicitly.

    2. We want to match in the presence of foralls;
            e.g     (forall a. t1) ~ (forall b. t2)

       That is what the RnEnv2 is for; it does the alpha-renaming
       that makes it as if a and b were the same variable.
       Initialising the RnEnv2, so that it can generate a fresh
       binder when necessary, entails knowing the free variables of
       both types.

    3. We must be careful not to bind a template type variable to a
       locally bound variable.  E.g.
            (forall a. x) ~ (forall b. b)
       where x is the template type variable.  Then we do not want to
       bind x to a/b!  This is a kind of occurs check.
       The necessary locals accumulate in the RnEnv2.

    Note [tcMatchTy vs tcMatchTyKi]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    This module offers two variants of matching: with kinds and without.
    The TyKi variant takes two types, of potentially different kinds,
    and matches them. Along the way, it necessarily also matches their
    kinds. The Ty variant instead assumes that the kinds are already
    eqType and so skips matching up the kinds.

    How do you choose between them?

    1. If you know that the kinds of the two types are eqType, use
       the Ty variant. It is more efficient, as it does less work.

    2. If the kinds of variables in the template type might mention type families,
       use the Ty variant (and do other work to make sure the kinds
       work out). These pure unification functions do a straightforward
       syntactic unification and do no complex reasoning about type
       families. Note that the types of the variables in instances can indeed
       mention type families, so instance lookup must use the Ty variant.

       (Nothing goes terribly wrong -- no panics -- if there might be type
       families in kinds in the TyKi variant. You just might get match
       failure even though a reducing a type family would lead to success.)

    3. Otherwise, if you're sure that the variable kinds do not mention
       type families and you're not already sure that the kind of the template
       equals the kind of the target, then use the TyKi version.
    -}

    -- | Some unification functions are parameterised by a 'BindFun', which
    -- says whether or not to allow a certain unification to take place.
    -- A 'BindFun' takes the 'TyVar' involved along with the 'Type' it will
    -- potentially be bound to.
    --
    -- It is possible for the variable to actually be a coercion variable
    -- (Note [Matching coercion variables]), but only when one-way matching.
    -- In this case, the 'Type' will be a 'CoercionTy'.
    type BindFun = TyCoVar -> Type -> BindFlag

    -- | @tcMatchTy t1 t2@ produces a substitution (over fvs(t1))
    -- @s@ such that @s(t1)@ equals @t2@.
    -- The returned substitution might bind coercion variables,
    -- if the variable is an argument to a GADT constructor.
    --
    -- Precondition: typeKind ty1 `eqType` typeKind ty2
    --
    -- We don't pass in a set of "template variables" to be bound
    -- by the match, because tcMatchTy (and similar functions) are
    -- always used on top-level types, so we can bind any of the
    -- free variables of the LHS.
    -- See also Note [tcMatchTy vs tcMatchTyKi]
    tcMatchTy :: Type -> Type -> Maybe Subst
    tcMatchTy :: Type -> Type -> Maybe Subst
    tcMatchTy Type
    ty1 Type
    ty2 = [Type] -> [Type] -> Maybe Subst
    tcMatchTys [Type
    ty1] [Type
    ty2]

    tcMatchTyX_BM :: BindFun -> Subst
                  -> Type -> Type -> Maybe Subst
    tcMatchTyX_BM :: BindFun -> Subst -> Type -> Type -> Maybe Subst
    tcMatchTyX_BM BindFun
    bind_me Subst
    subst Type
    ty1 Type
    ty2
      = BindFun -> Bool -> Subst -> [Type] -> [Type] -> Maybe Subst
    tc_match_tys_x BindFun
    bind_me Bool
    False Subst
    subst [Type
    ty1] [Type
    ty2]

    -- | Like 'tcMatchTy', but allows the kinds of the types to differ,
    -- and thus matches them as well.
    -- See also Note [tcMatchTy vs tcMatchTyKi]
    tcMatchTyKi :: Type -> Type -> Maybe Subst
    tcMatchTyKi :: Type -> Type -> Maybe Subst
    tcMatchTyKi Type
    ty1 Type
    ty2
      = BindFun -> Bool -> [Type] -> [Type] -> Maybe Subst
    tc_match_tys BindFun
    alwaysBindFun Bool
    True [Type
    ty1] [Type
    ty2]

    -- | This is similar to 'tcMatchTy', but extends a substitution
    -- See also Note [tcMatchTy vs tcMatchTyKi]
    tcMatchTyX :: Subst            -- ^ Substitution to extend
               -> Type                -- ^ Template
               -> Type                -- ^ Target
               -> Maybe Subst
    tcMatchTyX :: Subst -> Type -> Type -> Maybe Subst
    tcMatchTyX Subst
    subst Type
    ty1 Type
    ty2
      = BindFun -> Bool -> Subst -> [Type] -> [Type] -> Maybe Subst
    tc_match_tys_x BindFun
    alwaysBindFun Bool
    False Subst
    subst [Type
    ty1] [Type
    ty2]

    -- | Like 'tcMatchTy' but over a list of types.
    -- See also Note [tcMatchTy vs tcMatchTyKi]
    tcMatchTys :: [Type]         -- ^ Template
               -> [Type]         -- ^ Target
               -> Maybe Subst    -- ^ One-shot; in principle the template
                                 -- variables could be free in the target
    tcMatchTys :: [Type] -> [Type] -> Maybe Subst
    tcMatchTys [Type]
    tys1 [Type]
    tys2
      = BindFun -> Bool -> [Type] -> [Type] -> Maybe Subst
    tc_match_tys BindFun
    alwaysBindFun Bool
    False [Type]
    tys1 [Type]
    tys2

    -- | Like 'tcMatchTyKi' but over a list of types.
    -- See also Note [tcMatchTy vs tcMatchTyKi]
    tcMatchTyKis :: [Type]         -- ^ Template
                 -> [Type]         -- ^ Target
                 -> Maybe Subst -- ^ One-shot substitution
    tcMatchTyKis :: [Type] -> [Type] -> Maybe Subst
    tcMatchTyKis [Type]
    tys1 [Type]
    tys2
      = BindFun -> Bool -> [Type] -> [Type] -> Maybe Subst
    tc_match_tys BindFun
    alwaysBindFun Bool
    True [Type]
    tys1 [Type]
    tys2

    -- | Like 'tcMatchTys', but extending a substitution
    -- See also Note [tcMatchTy vs tcMatchTyKi]
    tcMatchTysX :: Subst       -- ^ Substitution to extend
                -> [Type]         -- ^ Template
                -> [Type]         -- ^ Target
                -> Maybe Subst -- ^ One-shot substitution
    tcMatchTysX :: Subst -> [Type] -> [Type] -> Maybe Subst
    tcMatchTysX Subst
    subst [Type]
    tys1 [Type]
    tys2
      = BindFun -> Bool -> Subst -> [Type] -> [Type] -> Maybe Subst
    tc_match_tys_x BindFun
    alwaysBindFun Bool
    False Subst
    subst [Type]
    tys1 [Type]
    tys2

    -- | Like 'tcMatchTyKis', but extending a substitution
    -- See also Note [tcMatchTy vs tcMatchTyKi]
    tcMatchTyKisX :: Subst        -- ^ Substitution to extend
                  -> [Type]          -- ^ Template
                  -> [Type]          -- ^ Target
                  -> Maybe Subst  -- ^ One-shot substitution
    tcMatchTyKisX :: Subst -> [Type] -> [Type] -> Maybe Subst
    tcMatchTyKisX Subst
    subst [Type]
    tys1 [Type]
    tys2
      = BindFun -> Bool -> Subst -> [Type] -> [Type] -> Maybe Subst
    tc_match_tys_x BindFun
    alwaysBindFun Bool
    True Subst
    subst [Type]
    tys1 [Type]
    tys2

    -- | Same as tc_match_tys_x, but starts with an empty substitution
    tc_match_tys :: BindFun
                 -> Bool          -- ^ match kinds?
                 -> [Type]
                 -> [Type]
                 -> Maybe Subst
    tc_match_tys :: BindFun -> Bool -> [Type] -> [Type] -> Maybe Subst
    tc_match_tys BindFun
    bind_me Bool
    match_kis [Type]
    tys1 [Type]
    tys2
      = BindFun -> Bool -> Subst -> [Type] -> [Type] -> Maybe Subst
    tc_match_tys_x BindFun
    bind_me Bool
    match_kis (InScopeSet -> Subst
    mkEmptySubst InScopeSet
    in_scope) [Type]
    tys1 [Type]
    tys2
      where
        in_scope :: InScopeSet
    in_scope = VarSet -> InScopeSet
    mkInScopeSet ([Type] -> VarSet
    tyCoVarsOfTypes [Type]
    tys1 VarSet -> VarSet -> VarSet
    `unionVarSet` [Type] -> VarSet
    tyCoVarsOfTypes [Type]
    tys2)

    -- | Worker for 'tcMatchTysX' and 'tcMatchTyKisX'
    tc_match_tys_x :: BindFun
                   -> Bool          -- ^ match kinds?
                   -> Subst
                   -> [Type]
                   -> [Type]
                   -> Maybe Subst
    tc_match_tys_x :: BindFun -> Bool -> Subst -> [Type] -> [Type] -> Maybe Subst
    tc_match_tys_x BindFun
    bind_me Bool
    match_kis (Subst InScopeSet
    in_scope IdSubstEnv
    id_env TvSubstEnv
    tv_env CvSubstEnv
    cv_env) [Type]
    tys1 [Type]
    tys2
      = case BindFun
    -> Bool
    -> Bool
    -> Bool
    -> MultiplicityFlag
    -> RnEnv2
    -> TvSubstEnv
    -> CvSubstEnv
    -> [Type]
    -> [Type]
    -> UnifyResultM (TvSubstEnv, CvSubstEnv)
    tc_unify_tys BindFun
    bind_me
                          Bool
    False  -- Matching, not unifying
                          Bool
    False  -- Not an injectivity check
                          Bool
    match_kis
                          MultiplicityFlag
    RespectMultiplicities
                          (InScopeSet -> RnEnv2
    mkRnEnv2 InScopeSet
    in_scope) TvSubstEnv
    tv_env CvSubstEnv
    cv_env [Type]
    tys1 [Type]
    tys2 of
          Unifiable (TvSubstEnv
    tv_env', CvSubstEnv
    cv_env')
            -> Subst -> Maybe Subst
    forall a. a -> Maybe a
    Just (Subst -> Maybe Subst) -> Subst -> Maybe Subst
    forall a b. (a -> b) -> a -> b
    $ InScopeSet -> IdSubstEnv -> TvSubstEnv -> CvSubstEnv -> Subst
    Subst InScopeSet
    in_scope IdSubstEnv
    id_env TvSubstEnv
    tv_env' CvSubstEnv
    cv_env'
          UnifyResultM (TvSubstEnv, CvSubstEnv)
    _ -> Maybe Subst
    forall a. Maybe a
    Nothing

    -- | This one is called from the expression matcher,
    -- which already has a MatchEnv in hand
    ruleMatchTyKiX
      :: TyCoVarSet          -- ^ template variables
      -> RnEnv2
      -> TvSubstEnv          -- ^ type substitution to extend
      -> Type                -- ^ Template
      -> Type                -- ^ Target
      -> Maybe TvSubstEnv
    ruleMatchTyKiX :: VarSet -> RnEnv2 -> TvSubstEnv -> Type -> Type -> Maybe TvSubstEnv
    ruleMatchTyKiX VarSet
    tmpl_tvs RnEnv2
    rn_env TvSubstEnv
    tenv Type
    tmpl Type
    target
    -- See Note [Kind coercions in Unify]
      = case BindFun
    -> Bool
    -> Bool
    -> Bool
    -> MultiplicityFlag
    -> RnEnv2
    -> TvSubstEnv
    -> CvSubstEnv
    -> [Type]
    -> [Type]
    -> UnifyResultM (TvSubstEnv, CvSubstEnv)
    tc_unify_tys (VarSet -> BindFun
    matchBindFun VarSet
    tmpl_tvs) Bool
    False Bool
    False
                          Bool
    True -- <-- this means to match the kinds
                          MultiplicityFlag
    IgnoreMultiplicities
                            -- See Note [Rewrite rules ignore multiplicities in FunTy]
                          RnEnv2
    rn_env TvSubstEnv
    tenv CvSubstEnv
    emptyCvSubstEnv [Type
    tmpl] [Type
    target] of
          Unifiable (TvSubstEnv
    tenv', CvSubstEnv
    _) -> TvSubstEnv -> Maybe TvSubstEnv
    forall a. a -> Maybe a
    Just TvSubstEnv
    tenv'
          UnifyResultM (TvSubstEnv, CvSubstEnv)
    _                    -> Maybe TvSubstEnv
    forall a. Maybe a
    Nothing

    -- | Allow binding only for any variable in the set. Variables may
    -- be bound to any type.
    -- Used when doing simple matching; e.g. can we find a substitution
    --
    -- @
    -- S = [a :-> t1, b :-> t2] such that
    --     S( Maybe (a, b->Int )  =   Maybe (Bool, Char -> Int)
    -- @
    matchBindFun :: TyCoVarSet -> BindFun
    matchBindFun :: VarSet -> BindFun
    matchBindFun VarSet
    tvs OutTyVar
    tv Type
    _ty
      | OutTyVar
    tv OutTyVar -> VarSet -> Bool
    `elemVarSet` VarSet
    tvs = BindFlag
    BindMe
      | Bool
    otherwise           = BindFlag
    Apart

    -- | Allow the binding of any variable to any type
    alwaysBindFun :: BindFun
    alwaysBindFun :: BindFun
    alwaysBindFun OutTyVar
    _tv Type
    _ty = BindFlag
    BindMe

    {-
    ************************************************************************
    *                                                                      *
                    GADTs
    *                                                                      *
    ************************************************************************

    Note [Pruning dead case alternatives]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    Consider        data T a where
                       T1 :: T Int
                       T2 :: T a

                    newtype X = MkX Int
                    newtype Y = MkY Char

                    type family F a
                    type instance F Bool = Int

    Now consider    case x of { T1 -> e1; T2 -> e2 }

    The question before the house is this: if I know something about the type
    of x, can I prune away the T1 alternative?

    Suppose x::T Char.  It's impossible to construct a (T Char) using T1,
            Answer = YES we can prune the T1 branch (clearly)

    Suppose x::T (F a), where 'a' is in scope.  Then 'a' might be instantiated
    to 'Bool', in which case x::T Int, so
            ANSWER = NO (clearly)

    We see here that we want precisely the apartness check implemented within
    tcUnifyTysFG. So that's what we do! Two types cannot match if they are surely
    apart. Note that since we are simply dropping dead code, a conservative test
    suffices.
    -}

    -- | Given a list of pairs of types, are any two members of a pair surely
    -- apart, even after arbitrary type function evaluation and substitution?
    typesCantMatch :: [(Type,Type)] -> Bool
    -- See Note [Pruning dead case alternatives]
    typesCantMatch :: [(Type, Type)] -> Bool
    typesCantMatch [(Type, Type)]
    prs = ((Type, Type) -> Bool) -> [(Type, Type)] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any ((Type -> Type -> Bool) -> (Type, Type) -> Bool
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry Type -> Type -> Bool
    typesAreApart) [(Type, Type)]
    prs

    typesAreApart :: Type -> Type -> Bool
    typesAreApart :: Type -> Type -> Bool
    typesAreApart Type
    t1 Type
    t2 = case BindFun -> [Type] -> [Type] -> UnifyResult
    tcUnifyTysFG BindFun
    alwaysBindFun [Type
    t1] [Type
    t2] of
                            UnifyResult
    SurelyApart -> Bool
    True
                            UnifyResult
    _           -> Bool
    False
    {-
    ************************************************************************
    *                                                                      *
                 Unification
    *                                                                      *
    ************************************************************************

    Note [Fine-grained unification]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    Do the types (x, x) and ([y], y) unify? The answer is seemingly "no" --
    no substitution to finite types makes these match. But, a substitution to
    *infinite* types can unify these two types: [x |-> [[[...]]], y |-> [[[...]]] ].
    Why do we care? Consider these two type family instances:

    type instance F x x   = Int
    type instance F [y] y = Bool

    If we also have

    type instance Looper = [Looper]

    then the instances potentially overlap. The solution is to use unification
    over infinite terms. This is possible (see [1] for lots of gory details), but
    a full algorithm is a little more power than we need. Instead, we make a
    conservative approximation and just omit the occurs check.

    [1]: http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/axioms-extended.pdf

    tcUnifyTys considers an occurs-check problem as the same as general unification
    failure.

    tcUnifyTysFG ("fine-grained") returns one of three results: success, occurs-check
    failure ("MaybeApart"), or general failure ("SurelyApart").

    See also #8162.

    It's worth noting that unification in the presence of infinite types is not
    complete. This means that, sometimes, a closed type family does not reduce
    when it should. See test case indexed-types/should_fail/Overlap15 for an
    example.

    Note [Unification result]
    ~~~~~~~~~~~~~~~~~~~~~~~~~
    When unifying t1 ~ t2, we return
    * Unifiable s, if s is a substitution such that s(t1) is syntactically the
      same as s(t2), modulo type-synonym expansion.
    * SurelyApart, if there is no substitution s such that s(t1) = s(t2),
      where "=" includes type-family reductions.
    * MaybeApart mar s, when we aren't sure. `mar` is a MaybeApartReason.

    Examples
    * [a] ~ Maybe b: SurelyApart, because [] and Maybe can't unify
    * [(a,Int)] ~ [(Bool,b)]:  Unifiable
    * [F Int] ~ [Bool]: MaybeApart MARTypeFamily, because F Int might reduce to Bool (the unifier
                        does not try this)
    * a ~ Maybe a: MaybeApart MARInfinite. Not Unifiable clearly, but not SurelyApart either; consider
           a := Loop
           where  type family Loop where Loop = Maybe Loop

    There is the possibility that two types are MaybeApart for *both* reasons:

    * (a, F Int) ~ (Maybe a, Bool)

    What reason should we use? The *only* consumer of the reason is described
    in Note [Infinitary substitution in lookup] in GHC.Core.InstEnv. The goal
    there is identify which instances might match a target later (but don't
    match now) -- except that we want to ignore the possibility of infinitary
    substitutions. So let's examine a concrete scenario:

      class C a b c
      instance C a (Maybe a) Bool
      -- other instances, including one that will actually match
      [W] C b b (F Int)

    Do we want the instance as a future possibility? No. The only way that
    instance can match is in the presence of an infinite type (infinitely
    nested Maybes). We thus say that MARInfinite takes precedence, so that
    InstEnv treats this case as an infinitary substitution case; the fact
    that a type family is involved is only incidental. We thus define
    the Semigroup instance for MaybeApartReason to prefer MARInfinite.

    Note [The substitution in MaybeApart]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    The constructor MaybeApart carries data with it, typically a TvSubstEnv. Why?
    Because consider unifying these:

    (a, a, Int) ~ (b, [b], Bool)

    If we go left-to-right, we start with [a |-> b]. Then, on the middle terms, we
    apply the subst we have so far and discover that we need [b |-> [b]]. Because
    this fails the occurs check, we say that the types are MaybeApart (see above
    Note [Fine-grained unification]). But, we can't stop there! Because if we
    continue, we discover that Int is SurelyApart from Bool, and therefore the
    types are apart. This has practical consequences for the ability for closed
    type family applications to reduce. See test case
    indexed-types/should_compile/Overlap14.

    Note [Rewrite rules ignore multiplicities in FunTy]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    Consider the following (higher-order) rule:

    m :: Bool -> Bool -> Bool
    {-# RULES "m" forall f. m (f True) = f #-}

    let x = m ((,) @Bool @Bool True True)

    The rewrite rule expects an `f :: Bool -> Bool`, but `(,) @Bool @Bool True ::
    Bool %1 -> Bool` is linear (see Note [Data constructors are linear by default]
    in GHC.Core.Multiplicity) Should the rule match? Yes! According to the
    principles laid out in Note [Linting linearity] in GHC.Core.Lint, optimisation
    shouldn't be constrained by linearity.

    However, when matching the template variable `f` to `(,) True`, we do check that
    their types unify (see Note [Matching variable types] in GHC.Core.Rules). So
    when unifying types for the sake of rule-matching, the unification algorithm
    must be able to ignore multiplicities altogether.

    How is this done?
      (1) The `um_arr_mult` field of `UMEnv` recordsw when we are doing rule-matching,
          and hence want to ignore multiplicities.
      (2) The field is set to True in by `ruleMatchTyKiX`.
      (3) It is consulted when matching `FunTy` in `unify_ty`.

    Wrinkle in (3). In `unify_tc_app`, in `unify_ty`, `FunTy` is handled as if it
    was a regular type constructor. In this case, and when the types being unified
    are *function* arrows, but not constraint arrows, then the first argument is a
    multiplicity.

    We select this situation by comparing the type constructor with fUNTyCon. In
    this case, and this case only, we can safely drop the first argument (using the
    tail function) and unify the rest.
    -}

    -- | Simple unification of two types; all type variables are bindable
    -- Precondition: the kinds are already equal
    tcUnifyTy :: Type -> Type       -- All tyvars are bindable
              -> Maybe Subst
                           -- A regular one-shot (idempotent) substitution
    tcUnifyTy :: Type -> Type -> Maybe Subst
    tcUnifyTy Type
    t1 Type
    t2 = BindFun -> [Type] -> [Type] -> Maybe Subst
    tcUnifyTys BindFun
    alwaysBindFun [Type
    t1] [Type
    t2]

    -- | Like 'tcUnifyTy', but also unifies the kinds
    tcUnifyTyKi :: Type -> Type -> Maybe Subst
    tcUnifyTyKi :: Type -> Type -> Maybe Subst
    tcUnifyTyKi Type
    t1 Type
    t2 = BindFun -> [Type] -> [Type] -> Maybe Subst
    tcUnifyTyKis BindFun
    alwaysBindFun [Type
    t1] [Type
    t2]

    -- | Unify two types, treating type family applications as possibly unifying
    -- with anything and looking through injective type family applications.
    -- Precondition: kinds are the same
    tcUnifyTyWithTFs :: Bool  -- ^ True <=> do two-way unification;
                              --   False <=> do one-way matching.
                              --   See end of sec 5.2 from the paper
                     -> InScopeSet     -- Should include the free tyvars of both Type args
                     -> Type -> Type   -- Types to unify
                     -> Maybe Subst
    -- This algorithm is an implementation of the "Algorithm U" presented in
    -- the paper "Injective type families for Haskell", Figures 2 and 3.
    -- The code is incorporated with the standard unifier for convenience, but
    -- its operation should match the specification in the paper.
    tcUnifyTyWithTFs :: Bool -> InScopeSet -> Type -> Type -> Maybe Subst
    tcUnifyTyWithTFs Bool
    twoWay InScopeSet
    in_scope Type
    t1 Type
    t2
      = case BindFun
    -> Bool
    -> Bool
    -> Bool
    -> MultiplicityFlag
    -> RnEnv2
    -> TvSubstEnv
    -> CvSubstEnv
    -> [Type]
    -> [Type]
    -> UnifyResultM (TvSubstEnv, CvSubstEnv)
    tc_unify_tys BindFun
    alwaysBindFun Bool
    twoWay Bool
    True Bool
    False MultiplicityFlag
    RespectMultiplicities
                           RnEnv2
    rn_env TvSubstEnv
    emptyTvSubstEnv CvSubstEnv
    emptyCvSubstEnv
                           [Type
    t1] [Type
    t2] of
          Unifiable          (TvSubstEnv
    tv_subst, CvSubstEnv
    _cv_subst) -> Subst -> Maybe Subst
    forall a. a -> Maybe a
    Just (Subst -> Maybe Subst) -> Subst -> Maybe Subst
    forall a b. (a -> b) -> a -> b
    $ TvSubstEnv -> Subst
    maybe_fix TvSubstEnv
    tv_subst
          MaybeApart MaybeApartReason
    _reason (TvSubstEnv
    tv_subst, CvSubstEnv
    _cv_subst) -> Subst -> Maybe Subst
    forall a. a -> Maybe a
    Just (Subst -> Maybe Subst) -> Subst -> Maybe Subst
    forall a b. (a -> b) -> a -> b
    $ TvSubstEnv -> Subst
    maybe_fix TvSubstEnv
    tv_subst
          -- we want to *succeed* in questionable cases. This is a
          -- pre-unification algorithm.
          UnifyResultM (TvSubstEnv, CvSubstEnv)
    SurelyApart      -> Maybe Subst
    forall a. Maybe a
    Nothing
      where
        rn_env :: RnEnv2
    rn_env   = InScopeSet -> RnEnv2
    mkRnEnv2 InScopeSet
    in_scope

        maybe_fix :: TvSubstEnv -> Subst
    maybe_fix | Bool
    twoWay    = InScopeSet -> TvSubstEnv -> Subst
    niFixSubst InScopeSet
    in_scope
                  | Bool
    otherwise = InScopeSet -> TvSubstEnv -> Subst
    mkTvSubst InScopeSet
    in_scope -- when matching, don't confuse
                                                   -- domain with range

    -----------------
    tcUnifyTys :: BindFun
               -> [Type] -> [Type]
               -> Maybe Subst
                                    -- ^ A regular one-shot (idempotent) substitution
                                    -- that unifies the erased types. See comments
                                    -- for 'tcUnifyTysFG'

    -- The two types may have common type variables, and indeed do so in the
    -- second call to tcUnifyTys in GHC.Tc.Instance.FunDeps.checkClsFD
    tcUnifyTys :: BindFun -> [Type] -> [Type] -> Maybe Subst
    tcUnifyTys BindFun
    bind_fn [Type]
    tys1 [Type]
    tys2
      = case BindFun -> [Type] -> [Type] -> UnifyResult
    tcUnifyTysFG BindFun
    bind_fn [Type]
    tys1 [Type]
    tys2 of
          Unifiable Subst
    result -> Subst -> Maybe Subst
    forall a. a -> Maybe a
    Just Subst
    result
          UnifyResult
    _                -> Maybe Subst
    forall a. Maybe a
    Nothing

    -- | Like 'tcUnifyTys' but also unifies the kinds
    tcUnifyTyKis :: BindFun
                 -> [Type] -> [Type]
                 -> Maybe Subst
    tcUnifyTyKis :: BindFun -> [Type] -> [Type] -> Maybe Subst
    tcUnifyTyKis BindFun
    bind_fn [Type]
    tys1 [Type]
    tys2
      = case BindFun -> [Type] -> [Type] -> UnifyResult
    tcUnifyTyKisFG BindFun
    bind_fn [Type]
    tys1 [Type]
    tys2 of
          Unifiable Subst
    result -> Subst -> Maybe Subst
    forall a. a -> Maybe a
    Just Subst
    result
          UnifyResult
    _                -> Maybe Subst
    forall a. Maybe a
    Nothing

    -- This type does double-duty. It is used in the UM (unifier monad) and to
    -- return the final result. See Note [Fine-grained unification]
    type UnifyResult = UnifyResultM Subst

    -- | See Note [Unification result]
    data UnifyResultM a = Unifiable a        -- the subst that unifies the types
                        | MaybeApart MaybeApartReason
                                     a       -- the subst has as much as we know
                                             -- it must be part of a most general unifier
                                             -- See Note [The substitution in MaybeApart]
                        | SurelyApart
                        deriving (forall a b. (a -> b) -> UnifyResultM a -> UnifyResultM b)
    -> (forall a b. a -> UnifyResultM b -> UnifyResultM a)
    -> Functor UnifyResultM
    forall a b. a -> UnifyResultM b -> UnifyResultM a
    forall a b. (a -> b) -> UnifyResultM a -> UnifyResultM b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    $cfmap :: forall a b. (a -> b) -> UnifyResultM a -> UnifyResultM b
    fmap :: forall a b. (a -> b) -> UnifyResultM a -> UnifyResultM b
    $c<$ :: forall a b. a -> UnifyResultM b -> UnifyResultM a
    <$ :: forall a b. a -> UnifyResultM b -> UnifyResultM a
    Functor

    -- | Why are two types 'MaybeApart'? 'MARInfinite' takes precedence:
    -- This is used (only) in Note [Infinitary substitution in lookup] in GHC.Core.InstEnv
    -- As of Feb 2022, we never differentiate between MARTypeFamily and MARTypeVsConstraint;
    -- it's really only MARInfinite that's interesting here.
    data MaybeApartReason
      = MARTypeFamily   -- ^ matching e.g. F Int ~? Bool

      | MARInfinite     -- ^ matching e.g. a ~? Maybe a

      | MARTypeVsConstraint  -- ^ matching Type ~? Constraint or the arrow types
        -- See Note [Type and Constraint are not apart] in GHC.Builtin.Types.Prim

    instance Outputable MaybeApartReason where
      ppr :: MaybeApartReason -> SDoc
    ppr MaybeApartReason
    MARTypeFamily       = String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "MARTypeFamily"
      ppr MaybeApartReason
    MARInfinite         = String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "MARInfinite"
      ppr MaybeApartReason
    MARTypeVsConstraint = String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "MARTypeVsConstraint"

    instance Semigroup MaybeApartReason where
      -- see end of Note [Unification result] for why
      MaybeApartReason
    MARTypeFamily       <> :: MaybeApartReason -> MaybeApartReason -> MaybeApartReason
    <> MaybeApartReason
    r = MaybeApartReason
    r
      MaybeApartReason
    MARInfinite         <> MaybeApartReason
    _ = MaybeApartReason
    MARInfinite
      MaybeApartReason
    MARTypeVsConstraint <> MaybeApartReason
    r = MaybeApartReason
    r

    instance Applicative UnifyResultM where
      pure :: forall a. a -> UnifyResultM a
    pure  = a -> UnifyResultM a
    forall a. a -> UnifyResultM a
    Unifiable
      <*> :: forall a b.
    UnifyResultM (a -> b) -> UnifyResultM a -> UnifyResultM b
    (<*>) = UnifyResultM (a -> b) -> UnifyResultM a -> UnifyResultM b
    forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
    ap

    instance Monad UnifyResultM where
      UnifyResultM a
    SurelyApart  >>= :: forall a b.
    UnifyResultM a -> (a -> UnifyResultM b) -> UnifyResultM b
    >>= a -> UnifyResultM b
    _ = UnifyResultM b
    forall a. UnifyResultM a
    SurelyApart
      MaybeApart MaybeApartReason
    r1 a
    x >>= a -> UnifyResultM b
    f = case a -> UnifyResultM b
    f a
    x of
                                Unifiable b
    y     -> MaybeApartReason -> b -> UnifyResultM b
    forall a. MaybeApartReason -> a -> UnifyResultM a
    MaybeApart MaybeApartReason
    r1 b
    y
                                MaybeApart MaybeApartReason
    r2 b
    y -> MaybeApartReason -> b -> UnifyResultM b
    forall a. MaybeApartReason -> a -> UnifyResultM a
    MaybeApart (MaybeApartReason
    r1 MaybeApartReason -> MaybeApartReason -> MaybeApartReason
    forall a. Semigroup a => a -> a -> a
    S.<> MaybeApartReason
    r2) b
    y
                                UnifyResultM b
    SurelyApart     -> UnifyResultM b
    forall a. UnifyResultM a
    SurelyApart
      Unifiable a
    x  >>= a -> UnifyResultM b
    f = a -> UnifyResultM b
    f a
    x

    -- | @tcUnifyTysFG bind_tv tys1 tys2@ attempts to find a substitution @s@ (whose
    -- domain elements all respond 'BindMe' to @bind_tv@) such that
    -- @s(tys1)@ and that of @s(tys2)@ are equal, as witnessed by the returned
    -- Coercions. This version requires that the kinds of the types are the same,
    -- if you unify left-to-right.
    tcUnifyTysFG :: BindFun
                 -> [Type] -> [Type]
                 -> UnifyResult
    tcUnifyTysFG :: BindFun -> [Type] -> [Type] -> UnifyResult
    tcUnifyTysFG BindFun
    bind_fn [Type]
    tys1 [Type]
    tys2
      = Bool -> BindFun -> [Type] -> [Type] -> UnifyResult
    tc_unify_tys_fg Bool
    False BindFun
    bind_fn [Type]
    tys1 [Type]
    tys2

    tcUnifyTyKisFG :: BindFun
                   -> [Type] -> [Type]
                   -> UnifyResult
    tcUnifyTyKisFG :: BindFun -> [Type] -> [Type] -> UnifyResult
    tcUnifyTyKisFG BindFun
    bind_fn [Type]
    tys1 [Type]
    tys2
      = Bool -> BindFun -> [Type] -> [Type] -> UnifyResult
    tc_unify_tys_fg Bool
    True BindFun
    bind_fn [Type]
    tys1 [Type]
    tys2

    tc_unify_tys_fg :: Bool
                    -> BindFun
                    -> [Type] -> [Type]
                    -> UnifyResult
    tc_unify_tys_fg :: Bool -> BindFun -> [Type] -> [Type] -> UnifyResult
    tc_unify_tys_fg Bool
    match_kis BindFun
    bind_fn [Type]
    tys1 [Type]
    tys2
      = do { (env, _) <- BindFun
    -> Bool
    -> Bool
    -> Bool
    -> MultiplicityFlag
    -> RnEnv2
    -> TvSubstEnv
    -> CvSubstEnv
    -> [Type]
    -> [Type]
    -> UnifyResultM (TvSubstEnv, CvSubstEnv)
    tc_unify_tys BindFun
    bind_fn Bool
    True Bool
    False Bool
    match_kis MultiplicityFlag
    RespectMultiplicities RnEnv2
    rn_env
                                      TvSubstEnv
    emptyTvSubstEnv CvSubstEnv
    emptyCvSubstEnv
                                      [Type]
    tys1 [Type]
    tys2
           ; return $ niFixSubst in_scope env }
      where
        in_scope :: InScopeSet
    in_scope = VarSet -> InScopeSet
    mkInScopeSet (VarSet -> InScopeSet) -> VarSet -> InScopeSet
    forall a b. (a -> b) -> a -> b
    $ [Type] -> VarSet
    tyCoVarsOfTypes [Type]
    tys1 VarSet -> VarSet -> VarSet
    `unionVarSet` [Type] -> VarSet
    tyCoVarsOfTypes [Type]
    tys2
        rn_env :: RnEnv2
    rn_env   = InScopeSet -> RnEnv2
    mkRnEnv2 InScopeSet
    in_scope

    -- | This function is actually the one to call the unifier -- a little
    -- too general for outside clients, though.
    tc_unify_tys :: BindFun
                 -> AmIUnifying -- ^ True <=> unify; False <=> match
                 -> Bool        -- ^ True <=> doing an injectivity check
                 -> Bool        -- ^ True <=> treat the kinds as well
                 -> MultiplicityFlag -- ^ see Note [Rewrite rules ignore multiplicities in FunTy] in GHC.Core.Unify
                 -> RnEnv2
                 -> TvSubstEnv  -- ^ substitution to extend
                 -> CvSubstEnv
                 -> [Type] -> [Type]
                 -> UnifyResultM (TvSubstEnv, CvSubstEnv)
    -- NB: It's tempting to ASSERT here that, if we're not matching kinds, then
    -- the kinds of the types should be the same. However, this doesn't work,
    -- as the types may be a dependent telescope, where later types have kinds
    -- that mention variables occurring earlier in the list of types. Here's an
    -- example (from typecheck/should_fail/T12709):
    --   template: [rep :: RuntimeRep,       a :: TYPE rep]
    --   target:   [LiftedRep :: RuntimeRep, Int :: TYPE LiftedRep]
    -- We can see that matching the first pair will make the kinds of the second
    -- pair equal. Yet, we still don't need a separate pass to unify the kinds
    -- of these types, so it's appropriate to use the Ty variant of unification.
    -- See also Note [tcMatchTy vs tcMatchTyKi].
    tc_unify_tys :: BindFun
    -> Bool
    -> Bool
    -> Bool
    -> MultiplicityFlag
    -> RnEnv2
    -> TvSubstEnv
    -> CvSubstEnv
    -> [Type]
    -> [Type]
    -> UnifyResultM (TvSubstEnv, CvSubstEnv)
    tc_unify_tys BindFun
    bind_fn Bool
    unif Bool
    inj_check Bool
    match_kis MultiplicityFlag
    match_mults RnEnv2
    rn_env TvSubstEnv
    tv_env CvSubstEnv
    cv_env [Type]
    tys1 [Type]
    tys2
      = TvSubstEnv
    -> CvSubstEnv
    -> UM (TvSubstEnv, CvSubstEnv)
    -> UnifyResultM (TvSubstEnv, CvSubstEnv)
    forall a. TvSubstEnv -> CvSubstEnv -> UM a -> UnifyResultM a
    initUM TvSubstEnv
    tv_env CvSubstEnv
    cv_env (UM (TvSubstEnv, CvSubstEnv)
     -> UnifyResultM (TvSubstEnv, CvSubstEnv))
    -> UM (TvSubstEnv, CvSubstEnv)
    -> UnifyResultM (TvSubstEnv, CvSubstEnv)
    forall a b. (a -> b) -> a -> b
    $
        do { Bool -> UM () -> UM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when Bool
    match_kis (UM () -> UM ()) -> UM () -> UM ()
    forall a b. (a -> b) -> a -> b
    $
             UMEnv -> [Type] -> [Type] -> UM ()
    unify_tys UMEnv
    env [Type]
    kis1 [Type]
    kis2
           ; UMEnv -> [Type] -> [Type] -> UM ()
    unify_tys UMEnv
    env [Type]
    tys1 [Type]
    tys2
           ; (,) (TvSubstEnv -> CvSubstEnv -> (TvSubstEnv, CvSubstEnv))
    -> UM TvSubstEnv -> UM (CvSubstEnv -> (TvSubstEnv, CvSubstEnv))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> UM TvSubstEnv
    getTvSubstEnv UM (CvSubstEnv -> (TvSubstEnv, CvSubstEnv))
    -> UM CvSubstEnv -> UM (TvSubstEnv, CvSubstEnv)
    forall a b. UM (a -> b) -> UM a -> UM b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> UM CvSubstEnv
    getCvSubstEnv }
      where
        env :: UMEnv
    env = UMEnv { um_bind_fun :: BindFun
    um_bind_fun = BindFun
    bind_fn
                    , um_skols :: VarSet
    um_skols    = VarSet
    emptyVarSet
                    , um_unif :: Bool
    um_unif     = Bool
    unif
                    , um_inj_tf :: Bool
    um_inj_tf   = Bool
    inj_check
                    , um_arr_mult :: MultiplicityFlag
    um_arr_mult = MultiplicityFlag
    match_mults
                    , um_rn_env :: RnEnv2
    um_rn_env   = RnEnv2
    rn_env }

        kis1 :: [Type]
    kis1 = (Type -> Type) -> [Type] -> [Type]
    forall a b. (a -> b) -> [a] -> [b]
    map HasDebugCallStack => Type -> Type
    Type -> Type
    typeKind [Type]
    tys1
        kis2 :: [Type]
    kis2 = (Type -> Type) -> [Type] -> [Type]
    forall a b. (a -> b) -> [a] -> [b]
    map HasDebugCallStack => Type -> Type
    Type -> Type
    typeKind [Type]
    tys2

    instance Outputable a => Outputable (UnifyResultM a) where
      ppr :: UnifyResultM a -> SDoc
    ppr UnifyResultM a
    SurelyApart      = String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "SurelyApart"
      ppr (Unifiable a
    x)    = String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "Unifiable" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> a -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr a
    x
      ppr (MaybeApart MaybeApartReason
    r a
    x) = String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "MaybeApart" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> MaybeApartReason -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr MaybeApartReason
    r SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> a -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr a
    x

    {-
    ************************************************************************
    *                                                                      *
                    Non-idempotent substitution
    *                                                                      *
    ************************************************************************

    Note [Non-idempotent substitution]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    During unification we use a TvSubstEnv/CvSubstEnv pair that is
      (a) non-idempotent
      (b) loop-free; ie repeatedly applying it yields a fixed point

    Note [Finding the substitution fixpoint]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    Finding the fixpoint of a non-idempotent substitution arising from a
    unification is much trickier than it looks, because of kinds.  Consider
       T k (H k (f:k)) ~ T * (g:*)
    If we unify, we get the substitution
       [ k -> *
       , g -> H k (f:k) ]
    To make it idempotent we don't want to get just
       [ k -> *
       , g -> H * (f:k) ]
    We also want to substitute inside f's kind, to get
       [ k -> *
       , g -> H k (f:*) ]
    If we don't do this, we may apply the substitution to something,
    and get an ill-formed type, i.e. one where typeKind will fail.
    This happened, for example, in #9106.

    It gets worse.  In #14164 we wanted to take the fixpoint of
    this substitution
       [ xs_asV :-> F a_aY6 (z_aY7 :: a_aY6)
                            (rest_aWF :: G a_aY6 (z_aY7 :: a_aY6))
       , a_aY6  :-> a_aXQ ]

    We have to apply the substitution for a_aY6 two levels deep inside
    the invocation of F!  We don't have a function that recursively
    applies substitutions inside the kinds of variable occurrences (and
    probably rightly so).

    So, we work as follows:

     1. Start with the current substitution (which we are
        trying to fixpoint
           [ xs :-> F a (z :: a) (rest :: G a (z :: a))
           , a  :-> b ]

     2. Take all the free vars of the range of the substitution:
           {a, z, rest, b}
        NB: the free variable finder closes over
        the kinds of variable occurrences

     3. If none are in the domain of the substitution, stop.
        We have found a fixpoint.

     4. Remove the variables that are bound by the substitution, leaving
           {z, rest, b}

     5. Do a topo-sort to put them in dependency order:
           [ b :: *, z :: a, rest :: G a z ]

     6. Apply the substitution left-to-right to the kinds of these
        tyvars, extending it each time with a new binding, so we
        finish up with
           [ xs   :-> ..as before..
           , a    :-> b
           , b    :-> b    :: *
           , z    :-> z    :: b
           , rest :-> rest :: G b (z :: b) ]
        Note that rest now has the right kind

     7. Apply this extended substitution (once) to the range of
        the /original/ substitution.  (Note that we do the
        extended substitution would go on forever if you tried
        to find its fixpoint, because it maps z to z.)

     8. And go back to step 1

    In Step 6 we use the free vars from Step 2 as the initial
    in-scope set, because all of those variables appear in the
    range of the substitution, so they must all be in the in-scope
    set.  But NB that the type substitution engine does not look up
    variables in the in-scope set; it is used only to ensure no
    shadowing.
    -}

    niFixSubst :: InScopeSet -> TvSubstEnv -> Subst
    -- Find the idempotent fixed point of the non-idempotent substitution
    -- This is surprisingly tricky:
    --   see Note [Finding the substitution fixpoint]
    -- ToDo: use laziness instead of iteration?
    niFixSubst :: InScopeSet -> TvSubstEnv -> Subst
    niFixSubst InScopeSet
    in_scope TvSubstEnv
    tenv
      | Bool
    not_fixpoint = InScopeSet -> TvSubstEnv -> Subst
    niFixSubst InScopeSet
    in_scope ((Type -> Type) -> TvSubstEnv -> TvSubstEnv
    forall a b. (a -> b) -> VarEnv a -> VarEnv b
    mapVarEnv (HasDebugCallStack => Subst -> Type -> Type
    Subst -> Type -> Type
    substTy Subst
    subst) TvSubstEnv
    tenv)
      | Bool
    otherwise    = Subst
    subst
      where
        range_fvs :: FV
        range_fvs :: FV
    range_fvs = [Type] -> FV
    tyCoFVsOfTypes (TvSubstEnv -> [Type]
    forall {k} (key :: k) elt. UniqFM key elt -> [elt]
    nonDetEltsUFM TvSubstEnv
    tenv)
              -- It's OK to use nonDetEltsUFM here because the
              -- order of range_fvs, range_tvs is immaterial

        range_tvs :: [TyVar]
        range_tvs :: [OutTyVar]
    range_tvs = FV -> [OutTyVar]
    fvVarList FV
    range_fvs

        not_fixpoint :: Bool
    not_fixpoint  = (OutTyVar -> Bool) -> [OutTyVar] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any OutTyVar -> Bool
    in_domain [OutTyVar]
    range_tvs
        in_domain :: OutTyVar -> Bool
    in_domain OutTyVar
    tv  = OutTyVar
    tv OutTyVar -> TvSubstEnv -> Bool
    forall a. OutTyVar -> VarEnv a -> Bool
    `elemVarEnv` TvSubstEnv
    tenv

        free_tvs :: [OutTyVar]
    free_tvs = [OutTyVar] -> [OutTyVar]
    scopedSort ((OutTyVar -> Bool) -> [OutTyVar] -> [OutTyVar]
    forall a. (a -> Bool) -> [a] -> [a]
    filterOut OutTyVar -> Bool
    in_domain [OutTyVar]
    range_tvs)

        -- See Note [Finding the substitution fixpoint], Step 6
        subst :: Subst
    subst = (Subst -> OutTyVar -> Subst) -> Subst -> [OutTyVar] -> Subst
    forall b a. (b -> a -> b) -> b -> [a] -> b
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl' Subst -> OutTyVar -> Subst
    add_free_tv
                      (InScopeSet -> TvSubstEnv -> Subst
    mkTvSubst InScopeSet
    in_scope TvSubstEnv
    tenv)
                      [OutTyVar]
    free_tvs

        add_free_tv :: Subst -> TyVar -> Subst
        add_free_tv :: Subst -> OutTyVar -> Subst
    add_free_tv Subst
    subst OutTyVar
    tv
          = Subst -> OutTyVar -> Type -> Subst
    extendTvSubst Subst
    subst OutTyVar
    tv (OutTyVar -> Type
    mkTyVarTy OutTyVar
    tv')
         where
            tv' :: OutTyVar
    tv' = (Type -> Type) -> OutTyVar -> OutTyVar
    updateTyVarKind (HasDebugCallStack => Subst -> Type -> Type
    Subst -> Type -> Type
    substTy Subst
    subst) OutTyVar
    tv

    niSubstTvSet :: TvSubstEnv -> TyCoVarSet -> TyCoVarSet
    -- Apply the non-idempotent substitution to a set of type variables,
    -- remembering that the substitution isn't necessarily idempotent
    -- This is used in the occurs check, before extending the substitution
    niSubstTvSet :: TvSubstEnv -> VarSet -> VarSet
    niSubstTvSet TvSubstEnv
    tsubst VarSet
    tvs
      = (OutTyVar -> VarSet -> VarSet) -> VarSet -> VarSet -> VarSet
    forall elt a. (elt -> a -> a) -> a -> UniqSet elt -> a
    nonDetStrictFoldUniqSet (VarSet -> VarSet -> VarSet
    unionVarSet (VarSet -> VarSet -> VarSet)
    -> (OutTyVar -> VarSet) -> OutTyVar -> VarSet -> VarSet
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . OutTyVar -> VarSet
    get) VarSet
    emptyVarSet VarSet
    tvs
      -- It's OK to use a non-deterministic fold here because we immediately forget
      -- the ordering by creating a set.
      where
        get :: OutTyVar -> VarSet
    get OutTyVar
    tv
          | Just Type
    ty <- TvSubstEnv -> OutTyVar -> Maybe Type
    forall a. VarEnv a -> OutTyVar -> Maybe a
    lookupVarEnv TvSubstEnv
    tsubst OutTyVar
    tv
          = TvSubstEnv -> VarSet -> VarSet
    niSubstTvSet TvSubstEnv
    tsubst (Type -> VarSet
    tyCoVarsOfType Type
    ty)

          | Bool
    otherwise
          = OutTyVar -> VarSet
    unitVarSet OutTyVar
    tv

    {-
    ************************************************************************
    *                                                                      *
                    unify_ty: the main workhorse
    *                                                                      *
    ************************************************************************

    Note [Specification of unification]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    The pure unifier, unify_ty, defined in this module, tries to work out
    a substitution to make two types say True to eqType. NB: eqType is
    itself not purely syntactic; it accounts for CastTys;
    see Note [Non-trivial definitional equality] in GHC.Core.TyCo.Rep

    Unlike the "impure unifiers" in the typechecker (the eager unifier in
    GHC.Tc.Utils.Unify, and the constraint solver itself in GHC.Tc.Solver.Equality),
    the pure unifier does /not/ work up to ~.

    The algorithm implemented here is rather delicate, and we depend on it
    to uphold certain properties. This is a summary of these required
    properties.

    Notation:
     θ,φ  substitutions
     ξ    type-function-free types
     τ,σ  other types
     τ♭   type τ, flattened

     ≡    eqType

    (U1) Soundness.
         If (unify τ₁ τ₂) = Unifiable θ, then θ(τ₁) ≡ θ(τ₂).
         θ is a most general unifier for τ₁ and τ₂.

    (U2) Completeness.
         If (unify ξ₁ ξ₂) = SurelyApart,
         then there exists no substitution θ such that θ(ξ₁) ≡ θ(ξ₂).

    These two properties are stated as Property 11 in the "Closed Type Families"
    paper (POPL'14). Below, this paper is called [CTF].

    (U3) Apartness under substitution.
         If (unify ξ τ♭) = SurelyApart, then (unify ξ θ(τ)♭) = SurelyApart,
         for any θ. (Property 12 from [CTF])

    (U4) Apart types do not unify.
         If (unify ξ τ♭) = SurelyApart, then there exists no θ
         such that θ(ξ) = θ(τ). (Property 13 from [CTF])

    THEOREM. Completeness w.r.t ~
        If (unify τ₁♭ τ₂♭) = SurelyApart,
        then there exists no proof that (τ₁ ~ τ₂).

    PROOF. See appendix of [CTF].

    The unification algorithm is used for type family injectivity, as described
    in the "Injective Type Families" paper (Haskell'15), called [ITF]. When run
    in this mode, it has the following properties.

    (I1) If (unify σ τ) = SurelyApart, then σ and τ are not unifiable, even
         after arbitrary type family reductions. Note that σ and τ are
         not flattened here.

    (I2) If (unify σ τ) = MaybeApart θ, and if some
         φ exists such that φ(σ) ~ φ(τ), then φ extends θ.

    Furthermore, the RULES matching algorithm requires this property,
    but only when using this algorithm for matching:

    (M1) If (match σ τ) succeeds with θ, then all matchable tyvars
         in σ are bound in θ.

         Property M1 means that we must extend the substitution with,
         say (a ↦ a) when appropriate during matching.
         See also Note [Self-substitution when matching].

    (M2) Completeness of matching.
         If θ(σ) = τ, then (match σ τ) = Unifiable φ,
         where θ is an extension of φ.

    Sadly, property M2 and I2 conflict. Consider

    type family F1 a b where
      F1 Int    Bool   = Char
      F1 Double String = Char

    Consider now two matching problems:

    P1. match (F1 a Bool) (F1 Int Bool)
    P2. match (F1 a Bool) (F1 Double String)

    In case P1, we must find (a ↦ Int) to satisfy M2.
    In case P2, we must /not/ find (a ↦ Double), in order to satisfy I2. (Note
    that the correct mapping for I2 is (a ↦ Int). There is no way to discover
    this, but we mustn't map a to anything else!)

    We thus must parameterize the algorithm over whether it's being used
    for an injectivity check (refrain from looking at non-injective arguments
    to type families) or not (do indeed look at those arguments).  This is
    implemented  by the um_inj_tf field of UMEnv.

    (It's all a question of whether or not to include equation (7) from Fig. 2
    of [ITF].)

    This extra parameter is a bit fiddly, perhaps, but seemingly less so than
    having two separate, almost-identical algorithms.

    Note [Self-substitution when matching]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    What should happen when we're *matching* (not unifying) a1 with a1? We
    should get a substitution [a1 |-> a1]. A successful match should map all
    the template variables (except ones that disappear when expanding synonyms).
    But when unifying, we don't want to do this, because we'll then fall into
    a loop.

    This arrangement affects the code in three places:
     - If we're matching a refined template variable, don't recur. Instead, just
       check for equality. That is, if we know [a |-> Maybe a] and are matching
       (a ~? Maybe Int), we want to just fail.

     - Skip the occurs check when matching. This comes up in two places, because
       matching against variables is handled separately from matching against
       full-on types.

    Note that this arrangement was provoked by a real failure, where the same
    unique ended up in the template as in the target. (It was a rule firing when
    compiling Data.List.NonEmpty.)

    Note [Matching coercion variables]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    Consider this:

       type family F a

       data G a where
         MkG :: F a ~ Bool => G a

       type family Foo (x :: G a) :: F a
       type instance Foo MkG = False

    We would like that to be accepted. For that to work, we need to introduce
    a coercion variable on the left and then use it on the right. Accordingly,
    at use sites of Foo, we need to be able to use matching to figure out the
    value for the coercion. (See the desugared version:

       axFoo :: [a :: *, c :: F a ~ Bool]. Foo (MkG c) = False |> (sym c)

    ) We never want this action to happen during *unification* though, when
    all bets are off.

    Note [Kind coercions in Unify]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    We wish to match/unify while ignoring casts. But, we can't just ignore
    them completely, or we'll end up with ill-kinded substitutions. For example,
    say we're matching `a` with `ty |> co`. If we just drop the cast, we'll
    return [a |-> ty], but `a` and `ty` might have different kinds. We can't
    just match/unify their kinds, either, because this might gratuitously
    fail. After all, `co` is the witness that the kinds are the same -- they
    may look nothing alike.

    So, we pass a kind coercion to the match/unify worker. This coercion witnesses
    the equality between the substed kind of the left-hand type and the substed
    kind of the right-hand type. Note that we do not unify kinds at the leaves
    (as we did previously). We thus have

    Hence: (Unification Kind Invariant)
    -----------------------------------
    In the call
         unify_ty ty1 ty2 kco
    it must be that
         subst(kco) :: subst(kind(ty1)) ~N subst(kind(ty2))
    where `subst` is the ambient substitution in the UM monad.  And in the call
         unify_tys tys1 tys2
    (which has no kco), after we unify any prefix of tys1,tys2, the kinds of the
    head of the remaining tys1,tys2 are identical after substitution.  This
    implies, for example, that the kinds of the head of tys1,tys2 are identical
    after substitution.

    To get this coercion, we first have to match/unify
    the kinds before looking at the types. Happily, we need look only one level
    up, as all kinds are guaranteed to have kind *.

    When we're working with type applications (either TyConApp or AppTy) we
    need to worry about establishing INVARIANT, as the kinds of the function
    & arguments aren't (necessarily) included in the kind of the result.
    When unifying two TyConApps, this is easy, because the two TyCons are
    the same. Their kinds are thus the same. As long as we unify left-to-right,
    we'll be sure to unify types' kinds before the types themselves. (For example,
    think about Proxy :: forall k. k -> *. Unifying the first args matches up
    the kinds of the second args.)

    For AppTy, we must unify the kinds of the functions, but once these are
    unified, we can continue unifying arguments without worrying further about
    kinds.

    The interface to this module includes both "...Ty" functions and
    "...TyKi" functions. The former assume that INVARIANT is already
    established, either because the kinds are the same or because the
    list of types being passed in are the well-typed arguments to some
    type constructor (see two paragraphs above). The latter take a separate
    pre-pass over the kinds to establish INVARIANT. Sometimes, it's important
    not to take the second pass, as it caused #12442.

    We thought, at one point, that this was all unnecessary: why should
    casts be in types in the first place? But they are sometimes. In
    dependent/should_compile/KindEqualities2, we see, for example the
    constraint Num (Int |> (blah ; sym blah)).  We naturally want to find
    a dictionary for that constraint, which requires dealing with
    coercions in this manner.

    Note [Matching in the presence of casts (1)]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    When matching, it is crucial that no variables from the template
    end up in the range of the matching substitution (obviously!).
    When unifying, that's not a constraint; instead we take the fixpoint
    of the substitution at the end.

    So what should we do with this, when matching?
       unify_ty (tmpl |> co) tgt kco

    Previously, wrongly, we pushed 'co' in the (horrid) accumulating
    'kco' argument like this:
       unify_ty (tmpl |> co) tgt kco
         = unify_ty tmpl tgt (kco ; co)

    But that is obviously wrong because 'co' (from the template) ends
    up in 'kco', which in turn ends up in the range of the substitution.

    This all came up in #13910.  Because we match tycon arguments
    left-to-right, the ambient substitution will already have a matching
    substitution for any kinds; so there is an easy fix: just apply
    the substitution-so-far to the coercion from the LHS.

    Note that

    * When matching, the first arg of unify_ty is always the template;
      we never swap round.

    * The above argument is distressingly indirect. We seek a
      better way.

    * One better way is to ensure that type patterns (the template
      in the matching process) have no casts.  See #14119.

    Note [Matching in the presence of casts (2)]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    There is another wrinkle (#17395).  Suppose (T :: forall k. k -> Type)
    and we are matching
       tcMatchTy (T k (a::k))  (T j (b::j))

    Then we'll match k :-> j, as expected. But then in unify_tys
    we invoke
       unify_tys env (a::k) (b::j) (Refl j)

    Although we have unified k and j, it's very important that we put
    (Refl j), /not/ (Refl k) as the fourth argument to unify_tys.
    If we put (Refl k) we'd end up with the substitution
      a :-> b |> Refl k
    which is bogus because one of the template variables, k,
    appears in the range of the substitution.  Eek.

    Similar care is needed in unify_ty_app.

    Note [Polykinded tycon applications]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    Suppose  T :: forall k. Type -> K
    and we are unifying
      ty1:  T @Type         Int       :: Type
      ty2:  T @(Type->Type) Int Int   :: Type

    These two TyConApps have the same TyCon at the front but they
    (legitimately) have different numbers of arguments.  They
    are surelyApart, so we can report that without looking any
    further (see #15704).

    Note [Unifying type applications]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    Unifying type applications is quite subtle, as we found
    in #23134 and #22647, when type families are involved.

    Suppose
       type family F a :: Type -> Type
       type family G k :: k = r | r -> k

    and consider these examples:

    * F Int ~ F Char, where F is injective
      Since F is injective, we can reduce this to Int ~ Char,
      therefore SurelyApart.

    * F Int ~ F Char, where F is not injective
      Without injectivity, return MaybeApart.

    * G Type ~ G (Type -> Type) Int
      Even though G is injective and the arguments to G are different,
      we cannot deduce apartness because the RHS is oversaturated.
      For example, G might be defined as
        G Type = Maybe Int
        G (Type -> Type) = Maybe
      So we return MaybeApart.

    * F Int Bool ~ F Int Char       -- SurelyApart (since Bool is apart from Char)
      F Int Bool ~ Maybe a          -- MaybeApart
      F Int Bool ~ a b              -- MaybeApart
      F Int Bool ~ Char -> Bool     -- MaybeApart
      An oversaturated type family can match an application,
      whether it's a TyConApp, AppTy or FunTy. Decompose.

    * F Int ~ a b
      We cannot decompose a saturated, or under-saturated
      type family application. We return MaybeApart.

    To handle all those conditions, unify_ty goes through
    the following checks in sequence, where Fn is a type family
    of arity n:

    * (C1) Fn x_1 ... x_n ~ Fn y_1 .. y_n
      A saturated application.
      Here we can unify arguments in which Fn is injective.
    * (C2) Fn x_1 ... x_n ~ anything, anything ~ Fn x_1 ... x_n
      A saturated type family can match anything - we return MaybeApart.
    * (C3) Fn x_1 ... x_m ~ a b, a b ~ Fn x_1 ... x_m where m > n
      An oversaturated type family can be decomposed.
    * (C4) Fn x_1 ... x_m ~ anything, anything ~ Fn x_1 ... x_m, where m > n
      If we couldn't decompose in the previous step, we return SurelyApart.

    Afterwards, the rest of the code doesn't have to worry about type families.

    Note [Unifying type synonyms]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    Consider the task of unifying two 'Type's of the form

      TyConApp tc [] ~ TyConApp tc []

    where `tc` is a type synonym. A naive way to perform this comparison these
    would first expand the synonym and then compare the resulting expansions.

    However, this is obviously wasteful and the RHS of `tc` may be large; it is
    much better to rather compare the TyCons directly. Consequently, before
    expanding type synonyms in type comparisons we first look for a nullary
    TyConApp and simply compare the TyCons if we find one.

    Of course, if we find that the TyCons are *not* equal then we still need to
    perform the expansion as their RHSs may still be unifiable.  E.g
        type T = S (a->a)
        type S a = [a]
    and consider
        T Int ~ S (Int -> Int)

    We can't decompose non-nullary synonyms.  E.g.
        type R a = F a    -- Where F is a type family
    and consider
        R (a->a) ~ R Int
    We can't conclude that  (a->) ~ Int.  (There is a currently-missed opportunity
    here; if we knew that R was /injective/, perhaps we could decompose.)

    We perform the nullary-type-synonym optimisation in a number of places:

     * GHC.Core.Unify.unify_ty
     * GHC.Tc.Solver.Equality.can_eq_nc'
     * GHC.Tc.Utils.Unify.uType

    This optimisation is especially helpful for the ubiquitous GHC.Types.Type,
    since GHC prefers to use the type synonym over @TYPE 'LiftedRep@ applications
    whenever possible. See Note [Using synonyms to compress types] in
    GHC.Core.Type for details.

    c.f. Note [Comparing type synonyms] in GHC.Core.TyCo.Compare
    -}

    -------------- unify_ty: the main workhorse -----------

    type AmIUnifying = Bool   -- True  <=> Unifying
                              -- False <=> Matching

    unify_ty :: UMEnv
             -> Type -> Type  -- Types to be unified and a co
             -> CoercionN     -- A coercion between their kinds
                              -- See Note [Kind coercions in Unify]
             -> UM ()
    -- Precondition: see (Unification Kind Invariant)
    --
    -- See Note [Specification of unification]
    -- Respects newtypes, PredTypes
    -- See Note [Computing equality on types] in GHC.Core.Type
    unify_ty :: UMEnv -> Type -> Type -> CoercionN -> UM ()
    unify_ty UMEnv
    _env (TyConApp TyCon
    tc1 []) (TyConApp TyCon
    tc2 []) CoercionN
    _kco
      -- See Note [Unifying type synonyms]
      | TyCon
    tc1 TyCon -> TyCon -> Bool
    forall a. Eq a => a -> a -> Bool
    == TyCon
    tc2
      = () -> UM ()
    forall a. a -> UM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

    unify_ty UMEnv
    env Type
    ty1 Type
    ty2 CoercionN
    kco
        -- Now handle the cases we can "look through": synonyms and casts.
      | Just Type
    ty1' <- Type -> Maybe Type
    coreView Type
    ty1 = UMEnv -> Type -> Type -> CoercionN -> UM ()
    unify_ty UMEnv
    env Type
    ty1' Type
    ty2 CoercionN
    kco
      | Just Type
    ty2' <- Type -> Maybe Type
    coreView Type
    ty2 = UMEnv -> Type -> Type -> CoercionN -> UM ()
    unify_ty UMEnv
    env Type
    ty1 Type
    ty2' CoercionN
    kco
      | CastTy Type
    ty1' CoercionN
    co <- Type
    ty1     = if UMEnv -> Bool
    um_unif UMEnv
    env
                                    then UMEnv -> Type -> Type -> CoercionN -> UM ()
    unify_ty UMEnv
    env Type
    ty1' Type
    ty2 (CoercionN
    co HasDebugCallStack => CoercionN -> CoercionN -> CoercionN
    CoercionN -> CoercionN -> CoercionN
    `mkTransCo` CoercionN
    kco)
                                    else -- See Note [Matching in the presence of casts (1)]
                                         do { subst <- UMEnv -> UM Subst
    getSubst UMEnv
    env
                                            ; let co' = HasDebugCallStack => Subst -> CoercionN -> CoercionN
    Subst -> CoercionN -> CoercionN
    substCo Subst
    subst CoercionN
    co
                                            ; unify_ty env ty1' ty2 (co' `mkTransCo` kco) }
      | CastTy Type
    ty2' CoercionN
    co <- Type
    ty2     = UMEnv -> Type -> Type -> CoercionN -> UM ()
    unify_ty UMEnv
    env Type
    ty1 Type
    ty2' (CoercionN
    kco HasDebugCallStack => CoercionN -> CoercionN -> CoercionN
    CoercionN -> CoercionN -> CoercionN
    `mkTransCo` CoercionN -> CoercionN
    mkSymCo CoercionN
    co)

    unify_ty UMEnv
    env (TyVarTy OutTyVar
    tv1) Type
    ty2 CoercionN
    kco
      = UMEnv -> OutTyVar -> Type -> CoercionN -> UM ()
    uVar UMEnv
    env OutTyVar
    tv1 Type
    ty2 CoercionN
    kco
    unify_ty UMEnv
    env Type
    ty1 (TyVarTy OutTyVar
    tv2) CoercionN
    kco
      | UMEnv -> Bool
    um_unif UMEnv
    env  -- If unifying, can swap args
      = UMEnv -> OutTyVar -> Type -> CoercionN -> UM ()
    uVar (UMEnv -> UMEnv
    umSwapRn UMEnv
    env) OutTyVar
    tv2 Type
    ty1 (CoercionN -> CoercionN
    mkSymCo CoercionN
    kco)

    unify_ty UMEnv
    env Type
    ty1 Type
    ty2 CoercionN
    _kco

      -- Handle non-oversaturated type families first
      -- See Note [Unifying type applications]
      --
      -- (C1) If we have T x1 ... xn ~ T y1 ... yn, use injectivity information of T
      -- Note that both sides must not be oversaturated
      | Just (TyCon
    tc1, [Type]
    tys1) <- Maybe (TyCon, [Type]) -> Maybe (TyCon, [Type])
    isSatTyFamApp Maybe (TyCon, [Type])
    mb_tc_app1
      , Just (TyCon
    tc2, [Type]
    tys2) <- Maybe (TyCon, [Type]) -> Maybe (TyCon, [Type])
    isSatTyFamApp Maybe (TyCon, [Type])
    mb_tc_app2
      , TyCon
    tc1 TyCon -> TyCon -> Bool
    forall a. Eq a => a -> a -> Bool
    == TyCon
    tc2
      = do { let inj :: [Bool]
    inj = case TyCon -> Injectivity
    tyConInjectivityInfo TyCon
    tc1 of
                              Injectivity
    NotInjective -> Bool -> [Bool]
    forall a. a -> [a]
    repeat Bool
    False
                              Injective [Bool]
    bs -> [Bool]
    bs

                 ([Type]
    inj_tys1, [Type]
    noninj_tys1) = [Bool] -> [Type] -> ([Type], [Type])
    forall a. [Bool] -> [a] -> ([a], [a])
    partitionByList [Bool]
    inj [Type]
    tys1
                 ([Type]
    inj_tys2, [Type]
    noninj_tys2) = [Bool] -> [Type] -> ([Type], [Type])
    forall a. [Bool] -> [a] -> ([a], [a])
    partitionByList [Bool]
    inj [Type]
    tys2

           ; UMEnv -> [Type] -> [Type] -> UM ()
    unify_tys UMEnv
    env [Type]
    inj_tys1 [Type]
    inj_tys2
           ; Bool -> UM () -> UM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (UMEnv -> Bool
    um_inj_tf UMEnv
    env) (UM () -> UM ()) -> UM () -> UM ()
    forall a b. (a -> b) -> a -> b
    $ -- See (end of) Note [Specification of unification]
             MaybeApartReason -> UM () -> UM ()
    don'tBeSoSure MaybeApartReason
    MARTypeFamily (UM () -> UM ()) -> UM () -> UM ()
    forall a b. (a -> b) -> a -> b
    $ UMEnv -> [Type] -> [Type] -> UM ()
    unify_tys UMEnv
    env [Type]
    noninj_tys1 [Type]
    noninj_tys2 }

      | Just (TyCon, [Type])
    _ <- Maybe (TyCon, [Type]) -> Maybe (TyCon, [Type])
    isSatTyFamApp Maybe (TyCon, [Type])
    mb_tc_app1  -- (C2) A (not-over-saturated) type-family application
      = MaybeApartReason -> UM ()
    maybeApart MaybeApartReason
    MARTypeFamily            -- behaves like a type variable; might match

      | Just (TyCon, [Type])
    _ <- Maybe (TyCon, [Type]) -> Maybe (TyCon, [Type])
    isSatTyFamApp Maybe (TyCon, [Type])
    mb_tc_app2  -- (C2) A (not-over-saturated) type-family application
                                            -- behaves like a type variable; might unify
                                            -- but doesn't match (as in the TyVarTy case)
      = if UMEnv -> Bool
    um_unif UMEnv
    env then MaybeApartReason -> UM ()
    maybeApart MaybeApartReason
    MARTypeFamily else UM ()
    forall a. UM a
    surelyApart

      -- Handle oversaturated type families.
      --
      -- They can match an application (TyConApp/FunTy/AppTy), this is handled
      -- the same way as in the AppTy case below.
      --
      -- If there is no application, an oversaturated type family can only
      -- match a type variable or a saturated type family,
      -- both of which we handled earlier. So we can say surelyApart.
      | Just (TyCon
    tc1, [Type]
    _) <- Maybe (TyCon, [Type])
    mb_tc_app1
      , TyCon -> Bool
    isTypeFamilyTyCon TyCon
    tc1
      = if | Just (Type
    ty1a, Type
    ty1b) <- Type -> Maybe (Type, Type)
    tcSplitAppTyNoView_maybe Type
    ty1
           , Just (Type
    ty2a, Type
    ty2b) <- Type -> Maybe (Type, Type)
    tcSplitAppTyNoView_maybe Type
    ty2
           -> UMEnv -> Type -> [Type] -> Type -> [Type] -> UM ()
    unify_ty_app UMEnv
    env Type
    ty1a [Type
    ty1b] Type
    ty2a [Type
    ty2b]            -- (C3)
           | Bool
    otherwise -> UM ()
    forall a. UM a
    surelyApart                             -- (C4)

      | Just (TyCon
    tc2, [Type]
    _) <- Maybe (TyCon, [Type])
    mb_tc_app2
      , TyCon -> Bool
    isTypeFamilyTyCon TyCon
    tc2
      = if | Just (Type
    ty1a, Type
    ty1b) <- Type -> Maybe (Type, Type)
    tcSplitAppTyNoView_maybe Type
    ty1
           , Just (Type
    ty2a, Type
    ty2b) <- Type -> Maybe (Type, Type)
    tcSplitAppTyNoView_maybe Type
    ty2
           -> UMEnv -> Type -> [Type] -> Type -> [Type] -> UM ()
    unify_ty_app UMEnv
    env Type
    ty1a [Type
    ty1b] Type
    ty2a [Type
    ty2b]            -- (C3)
           | Bool
    otherwise -> UM ()
    forall a. UM a
    surelyApart                             -- (C4)

      -- At this point, neither tc1 nor tc2 can be a type family.
      | Just (TyCon
    tc1, [Type]
    tys1) <- Maybe (TyCon, [Type])
    mb_tc_app1
      , Just (TyCon
    tc2, [Type]
    tys2) <- Maybe (TyCon, [Type])
    mb_tc_app2
      , TyCon
    tc1 TyCon -> TyCon -> Bool
    forall a. Eq a => a -> a -> Bool
    == TyCon
    tc2
      = do { Bool -> SDoc -> UM ()
    forall (m :: * -> *).
    (HasCallStack, Applicative m) =>
    Bool -> SDoc -> m ()
    massertPpr (TyCon -> Role -> Bool
    isInjectiveTyCon TyCon
    tc1 Role
    Nominal) (TyCon -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr TyCon
    tc1)
           ; TyCon -> [Type] -> [Type] -> UM ()
    unify_tc_app TyCon
    tc1 [Type]
    tys1 [Type]
    tys2
           }

      -- TYPE and CONSTRAINT are not Apart
      -- See Note [Type and Constraint are not apart] in GHC.Builtin.Types.Prim
      -- NB: at this point we know that the two TyCons do not match
      | Just (TyCon
    tc1,[Type]
    _) <- Maybe (TyCon, [Type])
    mb_tc_app1, let u1 :: Unique
    u1 = TyCon -> Unique
    tyConUnique TyCon
    tc1
      , Just (TyCon
    tc2,[Type]
    _) <- Maybe (TyCon, [Type])
    mb_tc_app2, let u2 :: Unique
    u2 = TyCon -> Unique
    tyConUnique TyCon
    tc2
      , (Unique
    u1 Unique -> Unique -> Bool
    forall a. Eq a => a -> a -> Bool
    == Unique
    tYPETyConKey Bool -> Bool -> Bool
    && Unique
    u2 Unique -> Unique -> Bool
    forall a. Eq a => a -> a -> Bool
    == Unique
    cONSTRAINTTyConKey) Bool -> Bool -> Bool
    ||
        (Unique
    u2 Unique -> Unique -> Bool
    forall a. Eq a => a -> a -> Bool
    == Unique
    tYPETyConKey Bool -> Bool -> Bool
    && Unique
    u1 Unique -> Unique -> Bool
    forall a. Eq a => a -> a -> Bool
    == Unique
    cONSTRAINTTyConKey)
      = MaybeApartReason -> UM ()
    maybeApart MaybeApartReason
    MARTypeVsConstraint
        -- We don't bother to look inside; wrinkle (W3) in GHC.Builtin.Types.Prim
        -- Note [Type and Constraint are not apart]

      -- The arrow types are not Apart
      -- See Note [Type and Constraint are not apart] in GHC.Builtin.Types.Prim
      --     wrinkle (W2)
      -- NB1: at this point we know that the two TyCons do not match
      -- NB2: In the common FunTy/FunTy case you might wonder if we want to go via
      --      splitTyConApp_maybe.  But yes we do: we need to look at those implied
      --      kind argument in order to satisfy (Unification Kind Invariant)
      | FunTy {} <- Type
    ty1
      , FunTy {} <- Type
    ty2
      = MaybeApartReason -> UM ()
    maybeApart MaybeApartReason
    MARTypeVsConstraint
        -- We don't bother to look inside; wrinkle (W3) in GHC.Builtin.Types.Prim
        -- Note [Type and Constraint are not apart]

      where
        mb_tc_app1 :: Maybe (TyCon, [Type])
    mb_tc_app1 = HasDebugCallStack => Type -> Maybe (TyCon, [Type])
    Type -> Maybe (TyCon, [Type])
    splitTyConApp_maybe Type
    ty1
        mb_tc_app2 :: Maybe (TyCon, [Type])
    mb_tc_app2 = HasDebugCallStack => Type -> Maybe (TyCon, [Type])
    Type -> Maybe (TyCon, [Type])
    splitTyConApp_maybe Type
    ty2

        unify_tc_app :: TyCon -> [Type] -> [Type] -> UM ()
    unify_tc_app TyCon
    tc [Type]
    tys1 [Type]
    tys2
          | TyCon
    tc TyCon -> TyCon -> Bool
    forall a. Eq a => a -> a -> Bool
    == TyCon
    fUNTyCon
          , MultiplicityFlag
    IgnoreMultiplicities <- UMEnv -> MultiplicityFlag
    um_arr_mult UMEnv
    env
          , (Type
    _mult1 : [Type]
    no_mult_tys1) <- [Type]
    tys1
          , (Type
    _mult2 : [Type]
    no_mult_tys2) <- [Type]
    tys2
          = -- We're comparing function arrow types here (not constraint arrow
            -- types!), and they have at least one argument, which is the arrow's
            -- multiplicity annotation. The flag `um_arr_mult` instructs us to
            -- ignore multiplicities in this very case. This is a little tricky: see
            -- point (3) in Note [Rewrite rules ignore multiplicities in FunTy].
             UMEnv -> [Type] -> [Type] -> UM ()
    unify_tys UMEnv
    env [Type]
    no_mult_tys1 [Type]
    no_mult_tys2

          | Bool
    otherwise
          = UMEnv -> [Type] -> [Type] -> UM ()
    unify_tys UMEnv
    env [Type]
    tys1 [Type]
    tys2

            -- Applications need a bit of care!
            -- They can match FunTy and TyConApp, so use splitAppTy_maybe
            -- NB: we've already dealt with type variables,
            -- so if one type is an App the other one jolly well better be too
    unify_ty UMEnv
    env (AppTy Type
    ty1a Type
    ty1b) Type
    ty2 CoercionN
    _kco
      | Just (Type
    ty2a, Type
    ty2b) <- Type -> Maybe (Type, Type)
    tcSplitAppTyNoView_maybe Type
    ty2
      = UMEnv -> Type -> [Type] -> Type -> [Type] -> UM ()
    unify_ty_app UMEnv
    env Type
    ty1a [Type
    ty1b] Type
    ty2a [Type
    ty2b]

    unify_ty UMEnv
    env Type
    ty1 (AppTy Type
    ty2a Type
    ty2b) CoercionN
    _kco
      | Just (Type
    ty1a, Type
    ty1b) <- Type -> Maybe (Type, Type)
    tcSplitAppTyNoView_maybe Type
    ty1
      = UMEnv -> Type -> [Type] -> Type -> [Type] -> UM ()
    unify_ty_app UMEnv
    env Type
    ty1a [Type
    ty1b] Type
    ty2a [Type
    ty2b]

    unify_ty UMEnv
    _ (LitTy TyLit
    x) (LitTy TyLit
    y) CoercionN
    _kco | TyLit
    x TyLit -> TyLit -> Bool
    forall a. Eq a => a -> a -> Bool
    == TyLit
    y = () -> UM ()
    forall a. a -> UM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

    unify_ty UMEnv
    env (ForAllTy (Bndr OutTyVar
    tv1 ForAllTyFlag
    _) Type
    ty1) (ForAllTy (Bndr OutTyVar
    tv2 ForAllTyFlag
    _) Type
    ty2) CoercionN
    kco
      = do { UMEnv -> Type -> Type -> CoercionN -> UM ()
    unify_ty UMEnv
    env (OutTyVar -> Type
    varType OutTyVar
    tv1) (OutTyVar -> Type
    varType OutTyVar
    tv2) (Type -> CoercionN
    mkNomReflCo Type
    liftedTypeKind)
           ; let env' :: UMEnv
    env' = UMEnv -> OutTyVar -> OutTyVar -> UMEnv
    umRnBndr2 UMEnv
    env OutTyVar
    tv1 OutTyVar
    tv2
           ; UMEnv -> Type -> Type -> CoercionN -> UM ()
    unify_ty UMEnv
    env' Type
    ty1 Type
    ty2 CoercionN
    kco }

    -- See Note [Matching coercion variables]
    unify_ty UMEnv
    env (CoercionTy CoercionN
    co1) (CoercionTy CoercionN
    co2) CoercionN
    kco
      = do { c_subst <- UM CvSubstEnv
    getCvSubstEnv
           ; case co1 of
               CoVarCo OutTyVar
    cv
                 | Bool -> Bool
    not (UMEnv -> Bool
    um_unif UMEnv
    env)
                 , Bool -> Bool
    not (OutTyVar
    cv OutTyVar -> CvSubstEnv -> Bool
    forall a. OutTyVar -> VarEnv a -> Bool
    `elemVarEnv` CvSubstEnv
    c_subst)
                 , let (CoercionN
    _, CoercionN
    co_l, CoercionN
    co_r) = HasDebugCallStack => CoercionN -> (CoercionN, CoercionN, CoercionN)
    CoercionN -> (CoercionN, CoercionN, CoercionN)
    decomposeFunCo CoercionN
    kco
                         -- Because the coercion is used in a type, it should be safe to
                         -- ignore the multiplicity coercion.
                          -- cv :: t1 ~ t2
                          -- co2 :: s1 ~ s2
                          -- co_l :: t1 ~ s1
                          -- co_r :: t2 ~ s2
                       rhs_co :: CoercionN
    rhs_co = CoercionN
    co_l HasDebugCallStack => CoercionN -> CoercionN -> CoercionN
    CoercionN -> CoercionN -> CoercionN
    `mkTransCo` CoercionN
    co2 HasDebugCallStack => CoercionN -> CoercionN -> CoercionN
    CoercionN -> CoercionN -> CoercionN
    `mkTransCo` CoercionN -> CoercionN
    mkSymCo CoercionN
    co_r
                 , BindFlag
    BindMe <- UMEnv -> BindFun
    tvBindFlag UMEnv
    env OutTyVar
    cv (CoercionN -> Type
    CoercionTy CoercionN
    rhs_co)
                 -> do { UMEnv -> VarSet -> UM ()
    checkRnEnv UMEnv
    env (CoercionN -> VarSet
    tyCoVarsOfCo CoercionN
    co2)
                       ; OutTyVar -> CoercionN -> UM ()
    extendCvEnv OutTyVar
    cv CoercionN
    rhs_co }
               CoercionN
    _ -> () -> UM ()
    forall a. a -> UM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return () }

    unify_ty UMEnv
    _ Type
    _ Type
    _ CoercionN
    _ = UM ()
    forall a. UM a
    surelyApart

    unify_ty_app :: UMEnv -> Type -> [Type] -> Type -> [Type] -> UM ()
    unify_ty_app :: UMEnv -> Type -> [Type] -> Type -> [Type] -> UM ()
    unify_ty_app UMEnv
    env Type
    ty1 [Type]
    ty1args Type
    ty2 [Type]
    ty2args
      | Just (Type
    ty1', Type
    ty1a) <- HasDebugCallStack => Type -> Maybe (Type, Type)
    Type -> Maybe (Type, Type)
    splitAppTyNoView_maybe Type
    ty1
      , Just (Type
    ty2', Type
    ty2a) <- HasDebugCallStack => Type -> Maybe (Type, Type)
    Type -> Maybe (Type, Type)
    splitAppTyNoView_maybe Type
    ty2
      = UMEnv -> Type -> [Type] -> Type -> [Type] -> UM ()
    unify_ty_app UMEnv
    env Type
    ty1' (Type
    ty1a Type -> [Type] -> [Type]
    forall a. a -> [a] -> [a]
    : [Type]
    ty1args) Type
    ty2' (Type
    ty2a Type -> [Type] -> [Type]
    forall a. a -> [a] -> [a]
    : [Type]
    ty2args)

      | Bool
    otherwise
      = do { let ki1 :: Type
    ki1 = HasDebugCallStack => Type -> Type
    Type -> Type
    typeKind Type
    ty1
                 ki2 :: Type
    ki2 = HasDebugCallStack => Type -> Type
    Type -> Type
    typeKind Type
    ty2
               -- See Note [Kind coercions in Unify]
           ; UMEnv -> Type -> Type -> CoercionN -> UM ()
    unify_ty  UMEnv
    env Type
    ki1 Type
    ki2 (Type -> CoercionN
    mkNomReflCo Type
    liftedTypeKind)
           ; UMEnv -> Type -> Type -> CoercionN -> UM ()
    unify_ty  UMEnv
    env Type
    ty1 Type
    ty2 (Type -> CoercionN
    mkNomReflCo Type
    ki2)
                     -- Very important: 'ki2' not 'ki1'
                     -- See Note [Matching in the presence of casts (2)]
           ; UMEnv -> [Type] -> [Type] -> UM ()
    unify_tys UMEnv
    env [Type]
    ty1args [Type]
    ty2args }

    unify_tys :: UMEnv -> [Type] -> [Type] -> UM ()
    -- Precondition: see (Unification Kind Invariant)
    unify_tys :: UMEnv -> [Type] -> [Type] -> UM ()
    unify_tys UMEnv
    env [Type]
    orig_xs [Type]
    orig_ys
      = [Type] -> [Type] -> UM ()
    go [Type]
    orig_xs [Type]
    orig_ys
      where
        go :: [Type] -> [Type] -> UM ()
    go []     []     = () -> UM ()
    forall a. a -> UM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
        go (Type
    x:[Type]
    xs) (Type
    y:[Type]
    ys)
          -- See Note [Kind coercions in Unify]
          = do { UMEnv -> Type -> Type -> CoercionN -> UM ()
    unify_ty UMEnv
    env Type
    x Type
    y (Type -> CoercionN
    mkNomReflCo (Type -> CoercionN) -> Type -> CoercionN
    forall a b. (a -> b) -> a -> b
    $ HasDebugCallStack => Type -> Type
    Type -> Type
    typeKind Type
    y)
                     -- Very important: 'y' not 'x'
                     -- See Note [Matching in the presence of casts (2)]
               ; [Type] -> [Type] -> UM ()
    go [Type]
    xs [Type]
    ys }
        go [Type]
    _ [Type]
    _ = UM ()
    forall a. UM a
    surelyApart
          -- Possibly different saturations of a polykinded tycon
          -- See Note [Polykinded tycon applications]

    isSatTyFamApp :: Maybe (TyCon, [Type]) -> Maybe (TyCon, [Type])
    -- Return the argument if we have a saturated type family application
    -- If it is /over/ saturated then we return False.  E.g.
    --     unify_ty (F a b) (c d)    where F has arity 1
    -- we definitely want to decompose that type application! (#22647)
    isSatTyFamApp :: Maybe (TyCon, [Type]) -> Maybe (TyCon, [Type])
    isSatTyFamApp tapp :: Maybe (TyCon, [Type])
    tapp@(Just (TyCon
    tc, [Type]
    tys))
      |  TyCon -> Bool
    isTypeFamilyTyCon TyCon
    tc
      Bool -> Bool -> Bool
    && Bool -> Bool
    not ([Type]
    tys [Type] -> Arity -> Bool
    forall a. [a] -> Arity -> Bool
    `lengthExceeds` TyCon -> Arity
    tyConArity TyCon
    tc)  -- Not over-saturated
      = Maybe (TyCon, [Type])
    tapp
    isSatTyFamApp Maybe (TyCon, [Type])
    _ = Maybe (TyCon, [Type])
    forall a. Maybe a
    Nothing

    ---------------------------------
    uVar :: UMEnv
         -> InTyVar         -- Variable to be unified
         -> Type            -- with this Type
         -> Coercion        -- :: kind tv ~N kind ty
         -> UM ()

    uVar :: UMEnv -> OutTyVar -> Type -> CoercionN -> UM ()
    uVar UMEnv
    env OutTyVar
    tv1 Type
    ty CoercionN
    kco
     = do { -- Apply the ambient renaming
            let tv1' :: OutTyVar
    tv1' = UMEnv -> OutTyVar -> OutTyVar
    umRnOccL UMEnv
    env OutTyVar
    tv1

            -- Check to see whether tv1 is refined by the substitution
          ; subst <- UM TvSubstEnv
    getTvSubstEnv
          ; case (lookupVarEnv subst tv1') of
              Just Type
    ty' | UMEnv -> Bool
    um_unif UMEnv
    env                -- Unifying, so call
                       -> UMEnv -> Type -> Type -> CoercionN -> UM ()
    unify_ty UMEnv
    env Type
    ty' Type
    ty CoercionN
    kco   -- back into unify
                       | Bool
    otherwise
                       -> -- Matching, we don't want to just recur here.
                          -- this is because the range of the subst is the target
                          -- type, not the template type. So, just check for
                          -- normal type equality.
                          Bool -> UM () -> UM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless ((Type
    ty' Type -> CoercionN -> Type
    `mkCastTy` CoercionN
    kco) HasDebugCallStack => Type -> Type -> Bool
    Type -> Type -> Bool
    `tcEqType` Type
    ty) (UM () -> UM ()) -> UM () -> UM ()
    forall a b. (a -> b) -> a -> b
    $
                            UM ()
    forall a. UM a
    surelyApart
                          -- NB: it's important to use `tcEqType` instead of `eqType` here,
                          -- otherwise we might not reject a substitution
                          -- which unifies `Type` with `Constraint`, e.g.
                          -- a call to tc_unify_tys with arguments
                          --
                          --   tys1 = [k,k]
                          --   tys2 = [Type, Constraint]
                          --
                          -- See test cases: T11715b, T20521.
              Maybe Type
    Nothing  -> UMEnv -> OutTyVar -> Type -> Type -> CoercionN -> UM ()
    uUnrefined UMEnv
    env OutTyVar
    tv1' Type
    ty Type
    ty CoercionN
    kco } -- No, continue

    uUnrefined :: UMEnv
               -> OutTyVar          -- variable to be unified
               -> Type              -- with this Type
               -> Type              -- (version w/ expanded synonyms)
               -> Coercion          -- :: kind tv ~N kind ty
               -> UM ()

    -- We know that tv1 isn't refined

    uUnrefined :: UMEnv -> OutTyVar -> Type -> Type -> CoercionN -> UM ()
    uUnrefined UMEnv
    env OutTyVar
    tv1' Type
    ty2 Type
    ty2' CoercionN
    kco
      | Just Type
    ty2'' <- Type -> Maybe Type
    coreView Type
    ty2'
      = UMEnv -> OutTyVar -> Type -> Type -> CoercionN -> UM ()
    uUnrefined UMEnv
    env OutTyVar
    tv1' Type
    ty2 Type
    ty2'' CoercionN
    kco    -- Unwrap synonyms
                    -- This is essential, in case we have
                    --      type Foo a = a
                    -- and then unify a ~ Foo a

      | TyVarTy OutTyVar
    tv2 <- Type
    ty2'
      = do { let tv2' :: OutTyVar
    tv2' = UMEnv -> OutTyVar -> OutTyVar
    umRnOccR UMEnv
    env OutTyVar
    tv2
           ; Bool -> UM () -> UM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (OutTyVar
    tv1' OutTyVar -> OutTyVar -> Bool
    forall a. Eq a => a -> a -> Bool
    == OutTyVar
    tv2' Bool -> Bool -> Bool
    && UMEnv -> Bool
    um_unif UMEnv
    env) (UM () -> UM ()) -> UM () -> UM ()
    forall a b. (a -> b) -> a -> b
    $ do
               -- If we are unifying a ~ a, just return immediately
               -- Do not extend the substitution
               -- See Note [Self-substitution when matching]

              -- Check to see whether tv2 is refined
           { subst <- UM TvSubstEnv
    getTvSubstEnv
           ; case lookupVarEnv subst tv2 of
             {  Just Type
    ty' | UMEnv -> Bool
    um_unif UMEnv
    env -> UMEnv -> OutTyVar -> Type -> Type -> CoercionN -> UM ()
    uUnrefined UMEnv
    env OutTyVar
    tv1' Type
    ty' Type
    ty' CoercionN
    kco
             ;  Maybe Type
    _ ->

        do {   -- So both are unrefined
               -- Bind one or the other, depending on which is bindable
           ; let rhs1 :: Type
    rhs1 = Type
    ty2 Type -> CoercionN -> Type
    `mkCastTy` CoercionN -> CoercionN
    mkSymCo CoercionN
    kco
                 rhs2 :: Type
    rhs2 = Type
    ty1 Type -> CoercionN -> Type
    `mkCastTy` CoercionN
    kco
                 b1 :: BindFlag
    b1  = UMEnv -> BindFun
    tvBindFlag UMEnv
    env OutTyVar
    tv1' Type
    rhs1
                 b2 :: BindFlag
    b2  = UMEnv -> BindFun
    tvBindFlag UMEnv
    env OutTyVar
    tv2' Type
    rhs2
                 ty1 :: Type
    ty1 = OutTyVar -> Type
    mkTyVarTy OutTyVar
    tv1'
           ; case (BindFlag
    b1, BindFlag
    b2) of
               (BindFlag
    BindMe, BindFlag
    _) -> UMEnv -> OutTyVar -> Type -> UM ()
    bindTv UMEnv
    env OutTyVar
    tv1' Type
    rhs1
               (BindFlag
    _, BindFlag
    BindMe) | UMEnv -> Bool
    um_unif UMEnv
    env
                           -> UMEnv -> OutTyVar -> Type -> UM ()
    bindTv (UMEnv -> UMEnv
    umSwapRn UMEnv
    env) OutTyVar
    tv2 Type
    rhs2

               (BindFlag, BindFlag)
    _ | OutTyVar
    tv1' OutTyVar -> OutTyVar -> Bool
    forall a. Eq a => a -> a -> Bool
    == OutTyVar
    tv2' -> () -> UM ()
    forall a. a -> UM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
                 -- How could this happen? If we're only matching and if
                 -- we're comparing forall-bound variables.

               (BindFlag, BindFlag)
    _ -> UM ()
    forall a. UM a
    surelyApart
      }}}}

    uUnrefined UMEnv
    env OutTyVar
    tv1' Type
    ty2 Type
    _ CoercionN
    kco -- ty2 is not a type variable
      = case UMEnv -> BindFun
    tvBindFlag UMEnv
    env OutTyVar
    tv1' Type
    rhs of
          BindFlag
    Apart  -> UM ()
    forall a. UM a
    surelyApart
          BindFlag
    BindMe -> UMEnv -> OutTyVar -> Type -> UM ()
    bindTv UMEnv
    env OutTyVar
    tv1' Type
    rhs
      where
        rhs :: Type
    rhs = Type
    ty2 Type -> CoercionN -> Type
    `mkCastTy` CoercionN -> CoercionN
    mkSymCo CoercionN
    kco

    bindTv :: UMEnv -> OutTyVar -> Type -> UM ()
    -- OK, so we want to extend the substitution with tv := ty
    -- But first, we must do a couple of checks
    bindTv :: UMEnv -> OutTyVar -> Type -> UM ()
    bindTv UMEnv
    env OutTyVar
    tv1 Type
    ty2
      = do  { let free_tvs2 :: VarSet
    free_tvs2 = Type -> VarSet
    tyCoVarsOfType Type
    ty2

            -- Make sure tys mentions no local variables
            -- E.g.  (forall a. b) ~ (forall a. [a])
            -- We should not unify b := [a]!
            ; UMEnv -> VarSet -> UM ()
    checkRnEnv UMEnv
    env VarSet
    free_tvs2

            -- Occurs check, see Note [Fine-grained unification]
            -- Make sure you include 'kco' (which ty2 does) #14846
            ; occurs <- UMEnv -> OutTyVar -> VarSet -> UM Bool
    occursCheck UMEnv
    env OutTyVar
    tv1 VarSet
    free_tvs2

            ; if occurs then maybeApart MARInfinite
                        else extendTvEnv tv1 ty2 }

    occursCheck :: UMEnv -> TyVar -> VarSet -> UM Bool
    occursCheck :: UMEnv -> OutTyVar -> VarSet -> UM Bool
    occursCheck UMEnv
    env OutTyVar
    tv VarSet
    free_tvs
      | UMEnv -> Bool
    um_unif UMEnv
    env
      = do { tsubst <- UM TvSubstEnv
    getTvSubstEnv
           ; return (tv `elemVarSet` niSubstTvSet tsubst free_tvs) }

      | Bool
    otherwise      -- Matching; no occurs check
      = Bool -> UM Bool
    forall a. a -> UM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False   -- See Note [Self-substitution when matching]

    {-
    %************************************************************************
    %*                                                                      *
                    Binding decisions
    *                                                                      *
    ************************************************************************
    -}

    data BindFlag
      = BindMe      -- ^ A regular type variable

      | Apart       -- ^ Declare that this type variable is /apart/ from the
                    -- type provided. That is, the type variable will never
                    -- be instantiated to that type.
                    -- See also Note [Binding when looking up instances]
                    -- in GHC.Core.InstEnv.
      deriving BindFlag -> BindFlag -> Bool
    (BindFlag -> BindFlag -> Bool)
    -> (BindFlag -> BindFlag -> Bool) -> Eq BindFlag
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: BindFlag -> BindFlag -> Bool
    == :: BindFlag -> BindFlag -> Bool
    $c/= :: BindFlag -> BindFlag -> Bool
    /= :: BindFlag -> BindFlag -> Bool
    Eq
    -- NB: It would be conceivable to have an analogue to MaybeApart here,
    -- but there is not yet a need.

    {-
    ************************************************************************
    *                                                                      *
                    Unification monad
    *                                                                      *
    ************************************************************************
    -}

    data UMEnv
      = UMEnv { UMEnv -> Bool
    um_unif :: AmIUnifying

              , UMEnv -> Bool
    um_inj_tf :: Bool
                -- Checking for injectivity?
                -- See (end of) Note [Specification of unification]

              , UMEnv -> MultiplicityFlag
    um_arr_mult :: MultiplicityFlag
                -- Whether to unify multiplicity arguments when unifying arrows.
                -- See Note [Rewrite rules ignore multiplicities in FunTy]

              , UMEnv -> RnEnv2
    um_rn_env :: RnEnv2
                -- Renaming InTyVars to OutTyVars; this eliminates
                -- shadowing, and lines up matching foralls on the left
                -- and right

              , UMEnv -> VarSet
    um_skols :: TyVarSet
                -- OutTyVars bound by a forall in this unification;
                -- Do not bind these in the substitution!
                -- See the function tvBindFlag

              , UMEnv -> BindFun
    um_bind_fun :: BindFun
                -- User-supplied BindFlag function,
                -- for variables not in um_skols
              }

    data UMState = UMState
                       { UMState -> TvSubstEnv
    um_tv_env   :: TvSubstEnv
                       , UMState -> CvSubstEnv
    um_cv_env   :: CvSubstEnv }

    newtype UM a
      = UM' { forall a. UM a -> UMState -> UnifyResultM (UMState, a)
    unUM :: UMState -> UnifyResultM (UMState, a) }
        -- See Note [The one-shot state monad trick] in GHC.Utils.Monad

    pattern UM :: (UMState -> UnifyResultM (UMState, a)) -> UM a
    -- See Note [The one-shot state monad trick] in GHC.Utils.Monad
    pattern $mUM :: forall {r} {a}.
    UM a
    -> ((UMState -> UnifyResultM (UMState, a)) -> r)
    -> ((# #) -> r)
    -> r
    $bUM :: forall a. (UMState -> UnifyResultM (UMState, a)) -> UM a
    UM m <- UM' m
      where
        UM UMState -> UnifyResultM (UMState, a)
    m = (UMState -> UnifyResultM (UMState, a)) -> UM a
    forall a. (UMState -> UnifyResultM (UMState, a)) -> UM a
    UM' ((UMState -> UnifyResultM (UMState, a))
    -> UMState -> UnifyResultM (UMState, a)
    forall a b. (a -> b) -> a -> b
    oneShot UMState -> UnifyResultM (UMState, a)
    m)
    {-# COMPLETE UM #-}

    instance Functor UM where
      fmap :: forall a b. (a -> b) -> UM a -> UM b
    fmap a -> b
    f (UM UMState -> UnifyResultM (UMState, a)
    m) = (UMState -> UnifyResultM (UMState, b)) -> UM b
    forall a. (UMState -> UnifyResultM (UMState, a)) -> UM a
    UM (\UMState
    s -> ((UMState, a) -> (UMState, b))
    -> UnifyResultM (UMState, a) -> UnifyResultM (UMState, b)
    forall a b. (a -> b) -> UnifyResultM a -> UnifyResultM b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (\(UMState
    s', a
    v) -> (UMState
    s', a -> b
    f a
    v)) (UMState -> UnifyResultM (UMState, a)
    m UMState
    s))

    instance Applicative UM where
          pure :: forall a. a -> UM a
    pure a
    a = (UMState -> UnifyResultM (UMState, a)) -> UM a
    forall a. (UMState -> UnifyResultM (UMState, a)) -> UM a
    UM (\UMState
    s -> (UMState, a) -> UnifyResultM (UMState, a)
    forall a. a -> UnifyResultM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (UMState
    s, a
    a))
          <*> :: forall a b. UM (a -> b) -> UM a -> UM b
    (<*>)  = UM (a -> b) -> UM a -> UM b
    forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
    ap

    instance Monad UM where
      {-# INLINE (>>=) #-}
      -- See Note [INLINE pragmas and (>>)] in GHC.Utils.Monad
      UM a
    m >>= :: forall a b. UM a -> (a -> UM b) -> UM b
    >>= a -> UM b
    k  = (UMState -> UnifyResultM (UMState, b)) -> UM b
    forall a. (UMState -> UnifyResultM (UMState, a)) -> UM a
    UM (\UMState
    state ->
                      do { (state', v) <- UM a -> UMState -> UnifyResultM (UMState, a)
    forall a. UM a -> UMState -> UnifyResultM (UMState, a)
    unUM UM a
    m UMState
    state
                         ; unUM (k v) state' })

    instance MonadFail UM where
        fail :: forall a. String -> UM a
    fail String
    _   = (UMState -> UnifyResultM (UMState, a)) -> UM a
    forall a. (UMState -> UnifyResultM (UMState, a)) -> UM a
    UM (\UMState
    _ -> UnifyResultM (UMState, a)
    forall a. UnifyResultM a
    SurelyApart) -- failed pattern match

    initUM :: TvSubstEnv  -- subst to extend
           -> CvSubstEnv
           -> UM a -> UnifyResultM a
    initUM :: forall a. TvSubstEnv -> CvSubstEnv -> UM a -> UnifyResultM a
    initUM TvSubstEnv
    subst_env CvSubstEnv
    cv_subst_env UM a
    um
      = case UM a -> UMState -> UnifyResultM (UMState, a)
    forall a. UM a -> UMState -> UnifyResultM (UMState, a)
    unUM UM a
    um UMState
    state of
          Unifiable (UMState
    _, a
    subst)    -> a -> UnifyResultM a
    forall a. a -> UnifyResultM a
    Unifiable a
    subst
          MaybeApart MaybeApartReason
    r (UMState
    _, a
    subst) -> MaybeApartReason -> a -> UnifyResultM a
    forall a. MaybeApartReason -> a -> UnifyResultM a
    MaybeApart MaybeApartReason
    r a
    subst
          UnifyResultM (UMState, a)
    SurelyApart             -> UnifyResultM a
    forall a. UnifyResultM a
    SurelyApart
      where
        state :: UMState
    state = UMState { um_tv_env :: TvSubstEnv
    um_tv_env = TvSubstEnv
    subst_env
                        , um_cv_env :: CvSubstEnv
    um_cv_env = CvSubstEnv
    cv_subst_env }

    tvBindFlag :: UMEnv -> OutTyVar -> Type -> BindFlag
    tvBindFlag :: UMEnv -> BindFun
    tvBindFlag UMEnv
    env OutTyVar
    tv Type
    rhs
      | OutTyVar
    tv OutTyVar -> VarSet -> Bool
    `elemVarSet` UMEnv -> VarSet
    um_skols UMEnv
    env = BindFlag
    Apart
      | Bool
    otherwise                    = UMEnv -> BindFun
    um_bind_fun UMEnv
    env OutTyVar
    tv Type
    rhs

    getTvSubstEnv :: UM TvSubstEnv
    getTvSubstEnv :: UM TvSubstEnv
    getTvSubstEnv = (UMState -> UnifyResultM (UMState, TvSubstEnv)) -> UM TvSubstEnv
    forall a. (UMState -> UnifyResultM (UMState, a)) -> UM a
    UM ((UMState -> UnifyResultM (UMState, TvSubstEnv)) -> UM TvSubstEnv)
    -> (UMState -> UnifyResultM (UMState, TvSubstEnv)) -> UM TvSubstEnv
    forall a b. (a -> b) -> a -> b
    $ \UMState
    state -> (UMState, TvSubstEnv) -> UnifyResultM (UMState, TvSubstEnv)
    forall a. a -> UnifyResultM a
    Unifiable (UMState
    state, UMState -> TvSubstEnv
    um_tv_env UMState
    state)

    getCvSubstEnv :: UM CvSubstEnv
    getCvSubstEnv :: UM CvSubstEnv
    getCvSubstEnv = (UMState -> UnifyResultM (UMState, CvSubstEnv)) -> UM CvSubstEnv
    forall a. (UMState -> UnifyResultM (UMState, a)) -> UM a
    UM ((UMState -> UnifyResultM (UMState, CvSubstEnv)) -> UM CvSubstEnv)
    -> (UMState -> UnifyResultM (UMState, CvSubstEnv)) -> UM CvSubstEnv
    forall a b. (a -> b) -> a -> b
    $ \UMState
    state -> (UMState, CvSubstEnv) -> UnifyResultM (UMState, CvSubstEnv)
    forall a. a -> UnifyResultM a
    Unifiable (UMState
    state, UMState -> CvSubstEnv
    um_cv_env UMState
    state)

    getSubst :: UMEnv -> UM Subst
    getSubst :: UMEnv -> UM Subst
    getSubst UMEnv
    env = do { tv_env <- UM TvSubstEnv
    getTvSubstEnv
                      ; cv_env <- getCvSubstEnv
                      ; let in_scope = RnEnv2 -> InScopeSet
    rnInScopeSet (UMEnv -> RnEnv2
    um_rn_env UMEnv
    env)
                      ; return (mkTCvSubst in_scope tv_env cv_env) }

    extendTvEnv :: TyVar -> Type -> UM ()
    extendTvEnv :: OutTyVar -> Type -> UM ()
    extendTvEnv OutTyVar
    tv Type
    ty = (UMState -> UnifyResultM (UMState, ())) -> UM ()
    forall a. (UMState -> UnifyResultM (UMState, a)) -> UM a
    UM ((UMState -> UnifyResultM (UMState, ())) -> UM ())
    -> (UMState -> UnifyResultM (UMState, ())) -> UM ()
    forall a b. (a -> b) -> a -> b
    $ \UMState
    state ->
      (UMState, ()) -> UnifyResultM (UMState, ())
    forall a. a -> UnifyResultM a
    Unifiable (UMState
    state { um_tv_env = extendVarEnv (um_tv_env state) tv ty }, ())

    extendCvEnv :: CoVar -> Coercion -> UM ()
    extendCvEnv :: OutTyVar -> CoercionN -> UM ()
    extendCvEnv OutTyVar
    cv CoercionN
    co = (UMState -> UnifyResultM (UMState, ())) -> UM ()
    forall a. (UMState -> UnifyResultM (UMState, a)) -> UM a
    UM ((UMState -> UnifyResultM (UMState, ())) -> UM ())
    -> (UMState -> UnifyResultM (UMState, ())) -> UM ()
    forall a b. (a -> b) -> a -> b
    $ \UMState
    state ->
      (UMState, ()) -> UnifyResultM (UMState, ())
    forall a. a -> UnifyResultM a
    Unifiable (UMState
    state { um_cv_env = extendVarEnv (um_cv_env state) cv co }, ())

    umRnBndr2 :: UMEnv -> TyCoVar -> TyCoVar -> UMEnv
    umRnBndr2 :: UMEnv -> OutTyVar -> OutTyVar -> UMEnv
    umRnBndr2 UMEnv
    env OutTyVar
    v1 OutTyVar
    v2
      = UMEnv
    env { um_rn_env = rn_env', um_skols = um_skols env `extendVarSet` v' }
      where
        (RnEnv2
    rn_env', OutTyVar
    v') = RnEnv2 -> OutTyVar -> OutTyVar -> (RnEnv2, OutTyVar)
    rnBndr2_var (UMEnv -> RnEnv2
    um_rn_env UMEnv
    env) OutTyVar
    v1 OutTyVar
    v2

    checkRnEnv :: UMEnv -> VarSet -> UM ()
    checkRnEnv :: UMEnv -> VarSet -> UM ()
    checkRnEnv UMEnv
    env VarSet
    varset
      | VarSet -> Bool
    isEmptyVarSet VarSet
    skol_vars           = () -> UM ()
    forall a. a -> UM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
      | VarSet
    varset VarSet -> VarSet -> Bool
    `disjointVarSet` VarSet
    skol_vars = () -> UM ()
    forall a. a -> UM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
      | Bool
    otherwise                         = UM ()
    forall a. UM a
    surelyApart
      where
        skol_vars :: VarSet
    skol_vars = UMEnv -> VarSet
    um_skols UMEnv
    env
        -- NB: That isEmptyVarSet guard is a critical optimization;
        -- it means we don't have to calculate the free vars of
        -- the type, often saving quite a bit of allocation.

    -- | Converts any SurelyApart to a MaybeApart
    don'tBeSoSure :: MaybeApartReason -> UM () -> UM ()
    don'tBeSoSure :: MaybeApartReason -> UM () -> UM ()
    don'tBeSoSure MaybeApartReason
    r UM ()
    um = (UMState -> UnifyResultM (UMState, ())) -> UM ()
    forall a. (UMState -> UnifyResultM (UMState, a)) -> UM a
    UM ((UMState -> UnifyResultM (UMState, ())) -> UM ())
    -> (UMState -> UnifyResultM (UMState, ())) -> UM ()
    forall a b. (a -> b) -> a -> b
    $ \ UMState
    state ->
      case UM () -> UMState -> UnifyResultM (UMState, ())
    forall a. UM a -> UMState -> UnifyResultM (UMState, a)
    unUM UM ()
    um UMState
    state of
        UnifyResultM (UMState, ())
    SurelyApart -> MaybeApartReason -> (UMState, ()) -> UnifyResultM (UMState, ())
    forall a. MaybeApartReason -> a -> UnifyResultM a
    MaybeApart MaybeApartReason
    r (UMState
    state, ())
        UnifyResultM (UMState, ())
    other       -> UnifyResultM (UMState, ())
    other

    umRnOccL :: UMEnv -> TyVar -> TyVar
    umRnOccL :: UMEnv -> OutTyVar -> OutTyVar
    umRnOccL UMEnv
    env OutTyVar
    v = RnEnv2 -> OutTyVar -> OutTyVar
    rnOccL (UMEnv -> RnEnv2
    um_rn_env UMEnv
    env) OutTyVar
    v

    umRnOccR :: UMEnv -> TyVar -> TyVar
    umRnOccR :: UMEnv -> OutTyVar -> OutTyVar
    umRnOccR UMEnv
    env OutTyVar
    v = RnEnv2 -> OutTyVar -> OutTyVar
    rnOccR (UMEnv -> RnEnv2
    um_rn_env UMEnv
    env) OutTyVar
    v

    umSwapRn :: UMEnv -> UMEnv
    umSwapRn :: UMEnv -> UMEnv
    umSwapRn UMEnv
    env = UMEnv
    env { um_rn_env = rnSwap (um_rn_env env) }

    maybeApart :: MaybeApartReason -> UM ()
    maybeApart :: MaybeApartReason -> UM ()
    maybeApart MaybeApartReason
    r = (UMState -> UnifyResultM (UMState, ())) -> UM ()
    forall a. (UMState -> UnifyResultM (UMState, a)) -> UM a
    UM (\UMState
    state -> MaybeApartReason -> (UMState, ()) -> UnifyResultM (UMState, ())
    forall a. MaybeApartReason -> a -> UnifyResultM a
    MaybeApart MaybeApartReason
    r (UMState
    state, ()))

    surelyApart :: UM a
    surelyApart :: forall a. UM a
    surelyApart = (UMState -> UnifyResultM (UMState, a)) -> UM a
    forall a. (UMState -> UnifyResultM (UMState, a)) -> UM a
    UM (\UMState
    _ -> UnifyResultM (UMState, a)
    forall a. UnifyResultM a
    SurelyApart)

    {-
    %************************************************************************
    %*                                                                      *
                Matching a (lifted) type against a coercion
    %*                                                                      *
    %************************************************************************

    This section defines essentially an inverse to liftCoSubst. It is defined
    here to avoid a dependency from Coercion on this module.

    -}

    data MatchEnv = ME { MatchEnv -> VarSet
    me_tmpls :: TyVarSet
                       , MatchEnv -> RnEnv2
    me_env   :: RnEnv2 }

    -- | 'liftCoMatch' is sort of inverse to 'liftCoSubst'.  In particular, if
    --   @liftCoMatch vars ty co == Just s@, then @liftCoSubst s ty == co@,
    --   where @==@ there means that the result of 'liftCoSubst' has the same
    --   type as the original co; but may be different under the hood.
    --   That is, it matches a type against a coercion of the same
    --   "shape", and returns a lifting substitution which could have been
    --   used to produce the given coercion from the given type.
    --   Note that this function is incomplete -- it might return Nothing
    --   when there does indeed exist a possible lifting context.
    --
    -- This function is incomplete in that it doesn't respect the equality
    -- in `eqType`. That is, it's possible that this will succeed for t1 and
    -- fail for t2, even when t1 `eqType` t2. That's because it depends on
    -- there being a very similar structure between the type and the coercion.
    -- This incompleteness shouldn't be all that surprising, especially because
    -- it depends on the structure of the coercion, which is a silly thing to do.
    --
    -- The lifting context produced doesn't have to be exacting in the roles
    -- of the mappings. This is because any use of the lifting context will
    -- also require a desired role. Thus, this algorithm prefers mapping to
    -- nominal coercions where it can do so.
    liftCoMatch :: TyCoVarSet -> Type -> Coercion -> Maybe LiftingContext
    liftCoMatch :: VarSet -> Type -> CoercionN -> Maybe LiftingContext
    liftCoMatch VarSet
    tmpls Type
    ty CoercionN
    co
      = do { cenv1 <- MatchEnv
    -> CvSubstEnv
    -> Type
    -> CoercionN
    -> CoercionN
    -> CoercionN
    -> Maybe CvSubstEnv
    ty_co_match MatchEnv
    menv CvSubstEnv
    forall a. VarEnv a
    emptyVarEnv Type
    ki CoercionN
    ki_co CoercionN
    ki_ki_co CoercionN
    ki_ki_co
           ; cenv2 <- ty_co_match menv cenv1       ty co
                                  (mkNomReflCo co_lkind) (mkNomReflCo co_rkind)
           ; return (LC (mkEmptySubst in_scope) cenv2) }
      where
        menv :: MatchEnv
    menv     = ME { me_tmpls :: VarSet
    me_tmpls = VarSet
    tmpls, me_env :: RnEnv2
    me_env = InScopeSet -> RnEnv2
    mkRnEnv2 InScopeSet
    in_scope }
        in_scope :: InScopeSet
    in_scope = VarSet -> InScopeSet
    mkInScopeSet (VarSet
    tmpls VarSet -> VarSet -> VarSet
    `unionVarSet` CoercionN -> VarSet
    tyCoVarsOfCo CoercionN
    co)
        -- Like tcMatchTy, assume all the interesting variables
        -- in ty are in tmpls

        ki :: Type
    ki       = HasDebugCallStack => Type -> Type
    Type -> Type
    typeKind Type
    ty
        ki_co :: CoercionN
    ki_co    = HasDebugCallStack => CoercionN -> CoercionN
    CoercionN -> CoercionN
    promoteCoercion CoercionN
    co
        ki_ki_co :: CoercionN
    ki_ki_co = Type -> CoercionN
    mkNomReflCo Type
    liftedTypeKind

        Pair Type
    co_lkind Type
    co_rkind = HasDebugCallStack => CoercionN -> Pair Type
    CoercionN -> Pair Type
    coercionKind CoercionN
    ki_co

    -- | 'ty_co_match' does all the actual work for 'liftCoMatch'.
    ty_co_match :: MatchEnv   -- ^ ambient helpful info
                -> LiftCoEnv  -- ^ incoming subst
                -> Type       -- ^ ty, type to match
                -> Coercion   -- ^ co :: lty ~r rty, coercion to match against
                -> Coercion   -- ^ :: kind(lsubst(ty)) ~N kind(lty)
                -> Coercion   -- ^ :: kind(rsubst(ty)) ~N kind(rty)
                -> Maybe LiftCoEnv
       -- ^ Just env ==> liftCoSubst Nominal env ty == co, modulo roles.
       -- Also: Just env ==> lsubst(ty) == lty and rsubst(ty) == rty,
       -- where lsubst = lcSubstLeft(env) and rsubst = lcSubstRight(env)
    ty_co_match :: MatchEnv
    -> CvSubstEnv
    -> Type
    -> CoercionN
    -> CoercionN
    -> CoercionN
    -> Maybe CvSubstEnv
    ty_co_match MatchEnv
    menv CvSubstEnv
    subst Type
    ty CoercionN
    co CoercionN
    lkco CoercionN
    rkco
      | Just Type
    ty' <- Type -> Maybe Type
    coreView Type
    ty = MatchEnv
    -> CvSubstEnv
    -> Type
    -> CoercionN
    -> CoercionN
    -> CoercionN
    -> Maybe CvSubstEnv
    ty_co_match MatchEnv
    menv CvSubstEnv
    subst Type
    ty' CoercionN
    co CoercionN
    lkco CoercionN
    rkco

      -- handle Refl case:
      | Type -> VarSet
    tyCoVarsOfType Type
    ty VarSet -> CvSubstEnv -> Bool
    forall a. VarSet -> VarEnv a -> Bool
    `isNotInDomainOf` CvSubstEnv
    subst
      , Just (Type
    ty', Role
    _) <- CoercionN -> Maybe (Type, Role)
    isReflCo_maybe CoercionN
    co
      , Type
    ty HasCallStack => Type -> Type -> Bool
    Type -> Type -> Bool
    `eqType` Type
    ty'
        -- Why `eqType` and not `tcEqType`? Because this function is only used
        -- during coercion optimisation, after type-checking has finished.
      = CvSubstEnv -> Maybe CvSubstEnv
    forall a. a -> Maybe a
    Just CvSubstEnv
    subst

      where
        isNotInDomainOf :: VarSet -> VarEnv a -> Bool
        isNotInDomainOf :: forall a. VarSet -> VarEnv a -> Bool
    isNotInDomainOf VarSet
    set VarEnv a
    env
          = (OutTyVar -> Bool) -> VarSet -> Bool
    noneSet (\OutTyVar
    v -> OutTyVar -> VarEnv a -> Bool
    forall a. OutTyVar -> VarEnv a -> Bool
    elemVarEnv OutTyVar
    v VarEnv a
    env) VarSet
    set

        noneSet :: (Var -> Bool) -> VarSet -> Bool
        noneSet :: (OutTyVar -> Bool) -> VarSet -> Bool
    noneSet OutTyVar -> Bool
    f = (OutTyVar -> Bool) -> VarSet -> Bool
    allVarSet (Bool -> Bool
    not (Bool -> Bool) -> (OutTyVar -> Bool) -> OutTyVar -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . OutTyVar -> Bool
    f)

    ty_co_match MatchEnv
    menv CvSubstEnv
    subst Type
    ty CoercionN
    co CoercionN
    lkco CoercionN
    rkco
      | CastTy Type
    ty' CoercionN
    co' <- Type
    ty
         -- See Note [Matching in the presence of casts (1)]
      = let empty_subst :: Subst
    empty_subst  = InScopeSet -> Subst
    mkEmptySubst (RnEnv2 -> InScopeSet
    rnInScopeSet (MatchEnv -> RnEnv2
    me_env MatchEnv
    menv))
            substed_co_l :: CoercionN
    substed_co_l = HasDebugCallStack => Subst -> CoercionN -> CoercionN
    Subst -> CoercionN -> CoercionN
    substCo (Subst -> CvSubstEnv -> Subst
    liftEnvSubstLeft Subst
    empty_subst CvSubstEnv
    subst)  CoercionN
    co'
            substed_co_r :: CoercionN
    substed_co_r = HasDebugCallStack => Subst -> CoercionN -> CoercionN
    Subst -> CoercionN -> CoercionN
    substCo (Subst -> CvSubstEnv -> Subst
    liftEnvSubstRight Subst
    empty_subst CvSubstEnv
    subst) CoercionN
    co'
        in
        MatchEnv
    -> CvSubstEnv
    -> Type
    -> CoercionN
    -> CoercionN
    -> CoercionN
    -> Maybe CvSubstEnv
    ty_co_match MatchEnv
    menv CvSubstEnv
    subst Type
    ty' CoercionN
    co (CoercionN
    substed_co_l HasDebugCallStack => CoercionN -> CoercionN -> CoercionN
    CoercionN -> CoercionN -> CoercionN
    `mkTransCo` CoercionN
    lkco)
                                      (CoercionN
    substed_co_r HasDebugCallStack => CoercionN -> CoercionN -> CoercionN
    CoercionN -> CoercionN -> CoercionN
    `mkTransCo` CoercionN
    rkco)

      | SymCo CoercionN
    co' <- CoercionN
    co
      = CvSubstEnv -> CvSubstEnv
    swapLiftCoEnv (CvSubstEnv -> CvSubstEnv) -> Maybe CvSubstEnv -> Maybe CvSubstEnv
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MatchEnv
    -> CvSubstEnv
    -> Type
    -> CoercionN
    -> CoercionN
    -> CoercionN
    -> Maybe CvSubstEnv
    ty_co_match MatchEnv
    menv (CvSubstEnv -> CvSubstEnv
    swapLiftCoEnv CvSubstEnv
    subst) Type
    ty CoercionN
    co' CoercionN
    rkco CoercionN
    lkco

      -- Match a type variable against a non-refl coercion
    ty_co_match MatchEnv
    menv CvSubstEnv
    subst (TyVarTy OutTyVar
    tv1) CoercionN
    co CoercionN
    lkco CoercionN
    rkco
      | Just CoercionN
    co1' <- CvSubstEnv -> OutTyVar -> Maybe CoercionN
    forall a. VarEnv a -> OutTyVar -> Maybe a
    lookupVarEnv CvSubstEnv
    subst OutTyVar
    tv1' -- tv1' is already bound to co1
      = if RnEnv2 -> CoercionN -> CoercionN -> Bool
    eqCoercionX (RnEnv2 -> RnEnv2
    nukeRnEnvL RnEnv2
    rn_env) CoercionN
    co1' CoercionN
    co
        then CvSubstEnv -> Maybe CvSubstEnv
    forall a. a -> Maybe a
    Just CvSubstEnv
    subst
        else Maybe CvSubstEnv
    forall a. Maybe a
    Nothing       -- no match since tv1 matches two different coercions

      | OutTyVar
    tv1' OutTyVar -> VarSet -> Bool
    `elemVarSet` MatchEnv -> VarSet
    me_tmpls MatchEnv
    menv           -- tv1' is a template var
      = if (OutTyVar -> Bool) -> [OutTyVar] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any (RnEnv2 -> OutTyVar -> Bool
    inRnEnvR RnEnv2
    rn_env) (CoercionN -> [OutTyVar]
    tyCoVarsOfCoList CoercionN
    co)
        then Maybe CvSubstEnv
    forall a. Maybe a
    Nothing      -- occurs check failed
        else CvSubstEnv -> Maybe CvSubstEnv
    forall a. a -> Maybe a
    Just (CvSubstEnv -> Maybe CvSubstEnv) -> CvSubstEnv -> Maybe CvSubstEnv
    forall a b. (a -> b) -> a -> b
    $ CvSubstEnv -> OutTyVar -> CoercionN -> CvSubstEnv
    forall a. VarEnv a -> OutTyVar -> a -> VarEnv a
    extendVarEnv CvSubstEnv
    subst OutTyVar
    tv1' (CoercionN -> CvSubstEnv) -> CoercionN -> CvSubstEnv
    forall a b. (a -> b) -> a -> b
    $
                    CoercionN -> CoercionN -> CoercionN -> CoercionN
    castCoercionKind CoercionN
    co (CoercionN -> CoercionN
    mkSymCo CoercionN
    lkco) (CoercionN -> CoercionN
    mkSymCo CoercionN
    rkco)

      | Bool
    otherwise
      = Maybe CvSubstEnv
    forall a. Maybe a
    Nothing

      where
        rn_env :: RnEnv2
    rn_env = MatchEnv -> RnEnv2
    me_env MatchEnv
    menv
        tv1' :: OutTyVar
    tv1' = RnEnv2 -> OutTyVar -> OutTyVar
    rnOccL RnEnv2
    rn_env OutTyVar
    tv1

      -- just look through SubCo's. We don't really care about roles here.
    ty_co_match MatchEnv
    menv CvSubstEnv
    subst Type
    ty (SubCo CoercionN
    co) CoercionN
    lkco CoercionN
    rkco
      = MatchEnv
    -> CvSubstEnv
    -> Type
    -> CoercionN
    -> CoercionN
    -> CoercionN
    -> Maybe CvSubstEnv
    ty_co_match MatchEnv
    menv CvSubstEnv
    subst Type
    ty CoercionN
    co CoercionN
    lkco CoercionN
    rkco

    ty_co_match MatchEnv
    menv CvSubstEnv
    subst (AppTy Type
    ty1a Type
    ty1b) CoercionN
    co CoercionN
    _lkco CoercionN
    _rkco
      | Just (CoercionN
    co2, CoercionN
    arg2) <- CoercionN -> Maybe (CoercionN, CoercionN)
    splitAppCo_maybe CoercionN
    co     -- c.f. Unify.match on AppTy
      = MatchEnv
    -> CvSubstEnv
    -> Type
    -> [Type]
    -> CoercionN
    -> [CoercionN]
    -> Maybe CvSubstEnv
    ty_co_match_app MatchEnv
    menv CvSubstEnv
    subst Type
    ty1a [Type
    ty1b] CoercionN
    co2 [CoercionN
    arg2]
    ty_co_match MatchEnv
    menv CvSubstEnv
    subst Type
    ty1 (AppCo CoercionN
    co2 CoercionN
    arg2) CoercionN
    _lkco CoercionN
    _rkco
      | Just (Type
    ty1a, Type
    ty1b) <- HasDebugCallStack => Type -> Maybe (Type, Type)
    Type -> Maybe (Type, Type)
    splitAppTyNoView_maybe Type
    ty1
           -- yes, the one from Type, not TcType; this is for coercion optimization
      = MatchEnv
    -> CvSubstEnv
    -> Type
    -> [Type]
    -> CoercionN
    -> [CoercionN]
    -> Maybe CvSubstEnv
    ty_co_match_app MatchEnv
    menv CvSubstEnv
    subst Type
    ty1a [Type
    ty1b] CoercionN
    co2 [CoercionN
    arg2]

    ty_co_match MatchEnv
    menv CvSubstEnv
    subst (TyConApp TyCon
    tc1 [Type]
    tys) (TyConAppCo Role
    _ TyCon
    tc2 [CoercionN]
    cos) CoercionN
    _lkco CoercionN
    _rkco
      = MatchEnv
    -> CvSubstEnv
    -> TyCon
    -> [Type]
    -> TyCon
    -> [CoercionN]
    -> Maybe CvSubstEnv
    ty_co_match_tc MatchEnv
    menv CvSubstEnv
    subst TyCon
    tc1 [Type]
    tys TyCon
    tc2 [CoercionN]
    cos

    ty_co_match MatchEnv
    menv CvSubstEnv
    subst (FunTy { ft_mult :: Type -> Type
    ft_mult = Type
    w, ft_arg :: Type -> Type
    ft_arg = Type
    ty1, ft_res :: Type -> Type
    ft_res = Type
    ty2 })
                (FunCo { fco_mult :: CoercionN -> CoercionN
    fco_mult = CoercionN
    co_w, fco_arg :: CoercionN -> CoercionN
    fco_arg = CoercionN
    co1, fco_res :: CoercionN -> CoercionN
    fco_res = CoercionN
    co2 }) CoercionN
    _lkco CoercionN
    _rkco
      = MatchEnv -> CvSubstEnv -> [Type] -> [CoercionN] -> Maybe CvSubstEnv
    ty_co_match_args MatchEnv
    menv CvSubstEnv
    subst [Type
    w,    Type
    rep1,    Type
    rep2,    Type
    ty1, Type
    ty2]
                                    [CoercionN
    co_w, CoercionN
    co1_rep, CoercionN
    co2_rep, CoercionN
    co1, CoercionN
    co2]
      where
         rep1 :: Type
    rep1    = HasDebugCallStack => Type -> Type
    Type -> Type
    getRuntimeRep Type
    ty1
         rep2 :: Type
    rep2    = HasDebugCallStack => Type -> Type
    Type -> Type
    getRuntimeRep Type
    ty2
         co1_rep :: CoercionN
    co1_rep = HasDebugCallStack => CoercionN -> CoercionN
    CoercionN -> CoercionN
    mkRuntimeRepCo CoercionN
    co1
         co2_rep :: CoercionN
    co2_rep = HasDebugCallStack => CoercionN -> CoercionN
    CoercionN -> CoercionN
    mkRuntimeRepCo CoercionN
    co2
        -- NB: we include the RuntimeRep arguments in the matching;
        --     not doing so caused #21205.

    ty_co_match MatchEnv
    menv CvSubstEnv
    subst (ForAllTy (Bndr OutTyVar
    tv1 ForAllTyFlag
    vis1t) Type
    ty1)
                           (ForAllCo OutTyVar
    tv2 ForAllTyFlag
    vis1c ForAllTyFlag
    vis2c CoercionN
    kind_co2 CoercionN
    co2)
                           CoercionN
    lkco CoercionN
    rkco
      | OutTyVar -> Bool
    isTyVar OutTyVar
    tv1 Bool -> Bool -> Bool
    && OutTyVar -> Bool
    isTyVar OutTyVar
    tv2
      , ForAllTyFlag
    vis1t ForAllTyFlag -> ForAllTyFlag -> Bool
    forall a. Eq a => a -> a -> Bool
    == ForAllTyFlag
    vis1c Bool -> Bool -> Bool
    && ForAllTyFlag
    vis1c ForAllTyFlag -> ForAllTyFlag -> Bool
    forall a. Eq a => a -> a -> Bool
    == ForAllTyFlag
    vis2c -- Is this necessary?
          -- Is this visibility check necessary?  @rae says: yes, I think the
          -- check is necessary, if we're caring about visibility (and we are).
          -- But ty_co_match is a dark and not important corner.
      = do { subst1 <- MatchEnv
    -> CvSubstEnv
    -> Type
    -> CoercionN
    -> CoercionN
    -> CoercionN
    -> Maybe CvSubstEnv
    ty_co_match MatchEnv
    menv CvSubstEnv
    subst (OutTyVar -> Type
    tyVarKind OutTyVar
    tv1) CoercionN
    kind_co2
                                   CoercionN
    ki_ki_co CoercionN
    ki_ki_co
           ; let rn_env0 = MatchEnv -> RnEnv2
    me_env MatchEnv
    menv
                 rn_env1 = RnEnv2 -> OutTyVar -> OutTyVar -> RnEnv2
    rnBndr2 RnEnv2
    rn_env0 OutTyVar
    tv1 OutTyVar
    tv2
                 menv'   = MatchEnv
    menv { me_env = rn_env1 }
           ; ty_co_match menv' subst1 ty1 co2 lkco rkco }
      where
        ki_ki_co :: CoercionN
    ki_ki_co = Type -> CoercionN
    mkNomReflCo Type
    liftedTypeKind

    -- ty_co_match menv subst (ForAllTy (Bndr cv1 _) ty1)
    --                        (ForAllCo cv2 kind_co2 co2)
    --                        lkco rkco
    --   | isCoVar cv1 && isCoVar cv2
    --   We seems not to have enough information for this case
    --   1. Given:
    --        cv1      :: (s1 :: k1) ~r (s2 :: k2)
    --        kind_co2 :: (s1' ~ s2') ~N (t1 ~ t2)
    --        eta1      = mkSelCo (SelTyCon 2 role) (downgradeRole r Nominal kind_co2)
    --                 :: s1' ~ t1
    --        eta2      = mkSelCo (SelTyCon 3 role) (downgradeRole r Nominal kind_co2)
    --                 :: s2' ~ t2
    --      Wanted:
    --        subst1 <- ty_co_match menv subst  s1 eta1 kco1 kco2
    --        subst2 <- ty_co_match menv subst1 s2 eta2 kco3 kco4
    --      Question: How do we get kcoi?
    --   2. Given:
    --        lkco :: <*>    -- See Note [Weird typing rule for ForAllTy] in GHC.Core.TyCo.Rep
    --        rkco :: <*>
    --      Wanted:
    --        ty_co_match menv' subst2 ty1 co2 lkco' rkco'
    --      Question: How do we get lkco' and rkco'?

    ty_co_match MatchEnv
    _ CvSubstEnv
    subst (CoercionTy {}) CoercionN
    _ CoercionN
    _ CoercionN
    _
      = CvSubstEnv -> Maybe CvSubstEnv
    forall a. a -> Maybe a
    Just CvSubstEnv
    subst -- don't inspect coercions

    ty_co_match MatchEnv
    menv CvSubstEnv
    subst Type
    ty (GRefl Role
    r Type
    t (MCo CoercionN
    co)) CoercionN
    lkco CoercionN
    rkco
      =  MatchEnv
    -> CvSubstEnv
    -> Type
    -> CoercionN
    -> CoercionN
    -> CoercionN
    -> Maybe CvSubstEnv
    ty_co_match MatchEnv
    menv CvSubstEnv
    subst Type
    ty (Role -> Type -> MCoercion -> CoercionN
    GRefl Role
    r Type
    t MCoercion
    MRefl) CoercionN
    lkco (CoercionN
    rkco HasDebugCallStack => CoercionN -> CoercionN -> CoercionN
    CoercionN -> CoercionN -> CoercionN
    `mkTransCo` CoercionN -> CoercionN
    mkSymCo CoercionN
    co)

    ty_co_match MatchEnv
    menv CvSubstEnv
    subst Type
    ty CoercionN
    co1 CoercionN
    lkco CoercionN
    rkco
      | Just (CastTy Type
    t CoercionN
    co, Role
    r) <- CoercionN -> Maybe (Type, Role)
    isReflCo_maybe CoercionN
    co1
      -- In @pushRefl@, pushing reflexive coercion inside CastTy will give us
      -- t |> co ~ t ; <t> ; t ~ t |> co
      -- But transitive coercions are not helpful. Therefore we deal
      -- with it here: we do recursion on the smaller reflexive coercion,
      -- while propagating the correct kind coercions.
      = let kco' :: CoercionN
    kco' = CoercionN -> CoercionN
    mkSymCo CoercionN
    co
        in MatchEnv
    -> CvSubstEnv
    -> Type
    -> CoercionN
    -> CoercionN
    -> CoercionN
    -> Maybe CvSubstEnv
    ty_co_match MatchEnv
    menv CvSubstEnv
    subst Type
    ty (Role -> Type -> CoercionN
    mkReflCo Role
    r Type
    t) (CoercionN
    lkco HasDebugCallStack => CoercionN -> CoercionN -> CoercionN
    CoercionN -> CoercionN -> CoercionN
    `mkTransCo` CoercionN
    kco')
                                                    (CoercionN
    rkco HasDebugCallStack => CoercionN -> CoercionN -> CoercionN
    CoercionN -> CoercionN -> CoercionN
    `mkTransCo` CoercionN
    kco')

    ty_co_match MatchEnv
    menv CvSubstEnv
    subst Type
    ty CoercionN
    co CoercionN
    lkco CoercionN
    rkco
      | Just CoercionN
    co' <- CoercionN -> Maybe CoercionN
    pushRefl CoercionN
    co = MatchEnv
    -> CvSubstEnv
    -> Type
    -> CoercionN
    -> CoercionN
    -> CoercionN
    -> Maybe CvSubstEnv
    ty_co_match MatchEnv
    menv CvSubstEnv
    subst Type
    ty CoercionN
    co' CoercionN
    lkco CoercionN
    rkco
      | Bool
    otherwise               = Maybe CvSubstEnv
    forall a. Maybe a
    Nothing

    ty_co_match_tc :: MatchEnv -> LiftCoEnv
                   -> TyCon -> [Type]
                   -> TyCon -> [Coercion]
                   -> Maybe LiftCoEnv
    ty_co_match_tc :: MatchEnv
    -> CvSubstEnv
    -> TyCon
    -> [Type]
    -> TyCon
    -> [CoercionN]
    -> Maybe CvSubstEnv
    ty_co_match_tc MatchEnv
    menv CvSubstEnv
    subst TyCon
    tc1 [Type]
    tys1 TyCon
    tc2 [CoercionN]
    cos2
      = do { Bool -> Maybe ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (TyCon
    tc1 TyCon -> TyCon -> Bool
    forall a. Eq a => a -> a -> Bool
    == TyCon
    tc2)
           ; MatchEnv -> CvSubstEnv -> [Type] -> [CoercionN] -> Maybe CvSubstEnv
    ty_co_match_args MatchEnv
    menv CvSubstEnv
    subst [Type]
    tys1 [CoercionN]
    cos2 }

    ty_co_match_app :: MatchEnv -> LiftCoEnv
                    -> Type -> [Type] -> Coercion -> [Coercion]
                    -> Maybe LiftCoEnv
    ty_co_match_app :: MatchEnv
    -> CvSubstEnv
    -> Type
    -> [Type]
    -> CoercionN
    -> [CoercionN]
    -> Maybe CvSubstEnv
    ty_co_match_app MatchEnv
    menv CvSubstEnv
    subst Type
    ty1 [Type]
    ty1args CoercionN
    co2 [CoercionN]
    co2args
      | Just (Type
    ty1', Type
    ty1a) <- HasDebugCallStack => Type -> Maybe (Type, Type)
    Type -> Maybe (Type, Type)
    splitAppTyNoView_maybe Type
    ty1
      , Just (CoercionN
    co2', CoercionN
    co2a) <- CoercionN -> Maybe (CoercionN, CoercionN)
    splitAppCo_maybe CoercionN
    co2
      = MatchEnv
    -> CvSubstEnv
    -> Type
    -> [Type]
    -> CoercionN
    -> [CoercionN]
    -> Maybe CvSubstEnv
    ty_co_match_app MatchEnv
    menv CvSubstEnv
    subst Type
    ty1' (Type
    ty1a Type -> [Type] -> [Type]
    forall a. a -> [a] -> [a]
    : [Type]
    ty1args) CoercionN
    co2' (CoercionN
    co2a CoercionN -> [CoercionN] -> [CoercionN]
    forall a. a -> [a] -> [a]
    : [CoercionN]
    co2args)

      | Bool
    otherwise
      = do { subst1 <- MatchEnv
    -> CvSubstEnv
    -> Type
    -> CoercionN
    -> CoercionN
    -> CoercionN
    -> Maybe CvSubstEnv
    ty_co_match MatchEnv
    menv CvSubstEnv
    subst Type
    ki1 CoercionN
    ki2 CoercionN
    ki_ki_co CoercionN
    ki_ki_co
           ; let Pair lkco rkco = mkNomReflCo <$> coercionKind ki2
           ; subst2 <- ty_co_match menv subst1 ty1 co2 lkco rkco
           ; ty_co_match_args menv subst2 ty1args co2args }
      where
        ki1 :: Type
    ki1 = HasDebugCallStack => Type -> Type
    Type -> Type
    typeKind Type
    ty1
        ki2 :: CoercionN
    ki2 = HasDebugCallStack => CoercionN -> CoercionN
    CoercionN -> CoercionN
    promoteCoercion CoercionN
    co2
        ki_ki_co :: CoercionN
    ki_ki_co = Type -> CoercionN
    mkNomReflCo Type
    liftedTypeKind

    ty_co_match_args :: MatchEnv -> LiftCoEnv -> [Type] -> [Coercion]
                     -> Maybe LiftCoEnv
    ty_co_match_args :: MatchEnv -> CvSubstEnv -> [Type] -> [CoercionN] -> Maybe CvSubstEnv
    ty_co_match_args MatchEnv
    menv CvSubstEnv
    subst (Type
    ty:[Type]
    tys) (CoercionN
    arg:[CoercionN]
    args)
      = do { let Pair Type
    lty Type
    rty = HasDebugCallStack => CoercionN -> Pair Type
    CoercionN -> Pair Type
    coercionKind CoercionN
    arg
                 lkco :: CoercionN
    lkco = Type -> CoercionN
    mkNomReflCo (HasDebugCallStack => Type -> Type
    Type -> Type
    typeKind Type
    lty)
                 rkco :: CoercionN
    rkco = Type -> CoercionN
    mkNomReflCo (HasDebugCallStack => Type -> Type
    Type -> Type
    typeKind Type
    rty)
           ; subst' <- MatchEnv
    -> CvSubstEnv
    -> Type
    -> CoercionN
    -> CoercionN
    -> CoercionN
    -> Maybe CvSubstEnv
    ty_co_match MatchEnv
    menv CvSubstEnv
    subst Type
    ty CoercionN
    arg CoercionN
    lkco CoercionN
    rkco
           ; ty_co_match_args menv subst' tys args }
    ty_co_match_args MatchEnv
    _    CvSubstEnv
    subst []       [] = CvSubstEnv -> Maybe CvSubstEnv
    forall a. a -> Maybe a
    Just CvSubstEnv
    subst
    ty_co_match_args MatchEnv
    _    CvSubstEnv
    _     [Type]
    _        [CoercionN]
    _  = Maybe CvSubstEnv
    forall a. Maybe a
    Nothing

    pushRefl :: Coercion -> Maybe Coercion
    pushRefl :: CoercionN -> Maybe CoercionN
    pushRefl CoercionN
    co =
      case (CoercionN -> Maybe (Type, Role)
    isReflCo_maybe CoercionN
    co) of
        Just (AppTy Type
    ty1 Type
    ty2, Role
    Nominal)
          -> CoercionN -> Maybe CoercionN
    forall a. a -> Maybe a
    Just (CoercionN -> CoercionN -> CoercionN
    AppCo (Role -> Type -> CoercionN
    mkReflCo Role
    Nominal Type
    ty1) (Type -> CoercionN
    mkNomReflCo Type
    ty2))
        Just (FunTy FunTyFlag
    af Type
    w Type
    ty1 Type
    ty2, Role
    r)
          ->  CoercionN -> Maybe CoercionN
    forall a. a -> Maybe a
    Just (Role
    -> FunTyFlag
    -> FunTyFlag
    -> CoercionN
    -> CoercionN
    -> CoercionN
    -> CoercionN
    FunCo Role
    r FunTyFlag
    af FunTyFlag
    af (Role -> Type -> CoercionN
    mkReflCo Role
    r Type
    w) (Role -> Type -> CoercionN
    mkReflCo Role
    r Type
    ty1) (Role -> Type -> CoercionN
    mkReflCo Role
    r Type
    ty2))
        Just (TyConApp TyCon
    tc [Type]
    tys, Role
    r)
          -> CoercionN -> Maybe CoercionN
    forall a. a -> Maybe a
    Just (Role -> TyCon -> [CoercionN] -> CoercionN
    TyConAppCo Role
    r TyCon
    tc ((Role -> Type -> CoercionN) -> [Role] -> [Type] -> [CoercionN]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith Role -> Type -> CoercionN
    mkReflCo (Role -> TyCon -> [Role]
    tyConRoleListX Role
    r TyCon
    tc) [Type]
    tys))
        Just (ForAllTy (Bndr OutTyVar
    tv ForAllTyFlag
    vis) Type
    ty, Role
    r)
          -> CoercionN -> Maybe CoercionN
    forall a. a -> Maybe a
    Just (ForAllCo { fco_tcv :: OutTyVar
    fco_tcv = OutTyVar
    tv, fco_visL :: ForAllTyFlag
    fco_visL = ForAllTyFlag
    vis, fco_visR :: ForAllTyFlag
    fco_visR = ForAllTyFlag
    vis
                            , fco_kind :: CoercionN
    fco_kind = Type -> CoercionN
    mkNomReflCo (OutTyVar -> Type
    varType OutTyVar
    tv)
                            , fco_body :: CoercionN
    fco_body = Role -> Type -> CoercionN
    mkReflCo Role
    r Type
    ty })
        Maybe (Type, Role)
    _ -> Maybe CoercionN
    forall a. Maybe a
    Nothing

    {-
    ************************************************************************
    *                                                                      *
                  Flattening
    *                                                                      *
    ************************************************************************

    Note [Flattening type-family applications when matching instances]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    As described in "Closed type families with overlapping equations"
    http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/axioms-extended.pdf
    we need to flatten core types before unifying them, when checking for "surely-apart"
    against earlier equations of a closed type family.
    Flattening means replacing all top-level uses of type functions with
    fresh variables, *taking care to preserve sharing*. That is, the type
    (Either (F a b) (F a b)) should flatten to (Either c c), never (Either
    c d).

    Here is a nice example of why it's all necessary:

      type family F a b where
        F Int Bool = Char
        F a   b    = Double
      type family G a         -- open, no instances

    How do we reduce (F (G Float) (G Float))? The first equation clearly doesn't match,
    while the second equation does. But, before reducing, we must make sure that the
    target can never become (F Int Bool). Well, no matter what G Float becomes, it
    certainly won't become *both* Int and Bool, so indeed we're safe reducing
    (F (G Float) (G Float)) to Double.

    This is necessary not only to get more reductions (which we might be
    willing to give up on), but for substitutivity. If we have (F x x), we
    can see that (F x x) can reduce to Double. So, it had better be the
    case that (F blah blah) can reduce to Double, no matter what (blah)
    is!  Flattening as done below ensures this.

    We also use this flattening operation to check for class instances.
    If we have
      instance C (Maybe b)
      instance {-# OVERLAPPING #-} C (Maybe Bool)
      [W] C (Maybe (F a))
    we want to know that the second instance might match later. So we
    flatten the (F a) in the target before trying to unify with instances.
    (This is done in GHC.Core.InstEnv.lookupInstEnv'.)

    The algorithm works by building up a TypeMap TyVar, mapping
    type family applications to fresh variables. This mapping must
    be threaded through all the function calls, as any entry in
    the mapping must be propagated to all future nodes in the tree.

    The algorithm also must track the set of in-scope variables, in
    order to make fresh variables as it flattens. (We are far from a
    source of fresh Uniques.) See Wrinkle 2, below.

    There are wrinkles, of course:

    1. The flattening algorithm must account for the possibility
       of inner `forall`s. (A `forall` seen here can happen only
       because of impredicativity. However, the flattening operation
       is an algorithm in Core, which is impredicative.)
       Suppose we have (forall b. F b) -> (forall b. F b). Of course,
       those two bs are entirely unrelated, and so we should certainly
       not flatten the two calls F b to the same variable. Instead, they
       must be treated separately. We thus carry a substitution that
       freshens variables; we must apply this substitution (in
       `coreFlattenTyFamApp`) before looking up an application in the environment.
       Note that the range of the substitution contains only TyVars, never anything
       else.

       For the sake of efficiency, we only apply this substitution when absolutely
       necessary. Namely:

       * We do not perform the substitution at all if it is empty.
       * We only need to worry about the arguments of a type family that are within
         the arity of said type family, so we can get away with not applying the
         substitution to any oversaturated type family arguments.
       * Importantly, we do /not/ achieve this substitution by recursively
         flattening the arguments, as this would be wrong. Consider `F (G a)`,
         where F and G are type families. We might decide that `F (G a)` flattens
         to `beta`. Later, the substitution is non-empty (but does not map `a`) and
         so we flatten `G a` to `gamma` and try to flatten `F gamma`. Of course,
         `F gamma` is unknown, and so we flatten it to `delta`, but it really
         should have been `beta`! Argh!

         Moral of the story: instead of flattening the arguments, just substitute
         them directly.

    2. There are two different reasons we might add a variable
       to the in-scope set as we work:

         A. We have just invented a new flattening variable.
         B. We have entered a `forall`.

       Annoying here is that in-scope variable source (A) must be
       threaded through the calls. For example, consider (F b -> forall c. F c).
       Suppose that, when flattening F b, we invent a fresh variable c.
       Now, when we encounter (forall c. F c), we need to know c is already in
       scope so that we locally rename c to c'. However, if we don't thread through
       the in-scope set from one argument of (->) to the other, we won't know this
       and might get very confused.

       In contrast, source (B) increases only as we go deeper, as in-scope sets
       normally do. However, even here we must be careful. The TypeMap TyVar that
       contains mappings from type family applications to freshened variables will
       be threaded through both sides of (forall b. F b) -> (forall b. F b). We
       thus must make sure that the two `b`s don't get renamed to the same b1. (If
       they did, then looking up `F b1` would yield the same flatten var for
       each.) So, even though `forall`-bound variables should really be in the
       in-scope set only when they are in scope, we retain these variables even
       outside of their scope. This ensures that, if we encounter a fresh
       `forall`-bound b, we will rename it to b2, not b1. Note that keeping a
       larger in-scope set than strictly necessary is always OK, as in-scope sets
       are only ever used to avoid collisions.

       Sadly, the freshening substitution described in (1) really mustn't bind
       variables outside of their scope: note that its domain is the *unrenamed*
       variables. This means that the substitution gets "pushed down" (like a
       reader monad) while the in-scope set gets threaded (like a state monad).
       Because a Subst contains its own in-scope set, we don't carry a Subst;
       instead, we just carry a TvSubstEnv down, tying it to the InScopeSet
       traveling separately as necessary.

    3. Consider `F ty_1 ... ty_n`, where F is a type family with arity k:

         type family F ty_1 ... ty_k :: res_k

       It's tempting to just flatten `F ty_1 ... ty_n` to `alpha`, where alpha is a
       flattening skolem. But we must instead flatten it to
       `alpha ty_(k+1) ... ty_n`—that is, by only flattening up to the arity of the
       type family.

       Why is this better? Consider the following concrete example from #16995:

         type family Param :: Type -> Type

         type family LookupParam (a :: Type) :: Type where
           LookupParam (f Char) = Bool
           LookupParam x        = Int

         foo :: LookupParam (Param ())
         foo = 42

       In order for `foo` to typecheck, `LookupParam (Param ())` must reduce to
       `Int`. But if we flatten `Param ()` to `alpha`, then GHC can't be sure if
       `alpha` is apart from `f Char`, so it won't fall through to the second
       equation. But since the `Param` type family has arity 0, we can instead
       flatten `Param ()` to `alpha ()`, about which GHC knows with confidence is
       apart from `f Char`, permitting the second equation to be reached.

       Not only does this allow more programs to be accepted, it's also important
       for correctness. Not doing this was the root cause of the Core Lint error
       in #16995.

    flattenTys is defined here because of module dependencies.
    -}

    data FlattenEnv
      = FlattenEnv { FlattenEnv -> TypeMap (OutTyVar, TyCon, [Type])
    fe_type_map :: TypeMap (TyVar, TyCon, [Type])
                     -- domain: exactly-saturated type family applications
                     -- range: (fresh variable, type family tycon, args)
                   , FlattenEnv -> InScopeSet
    fe_in_scope :: InScopeSet }
                     -- See Note [Flattening type-family applications when matching instances]

    emptyFlattenEnv :: InScopeSet -> FlattenEnv
    emptyFlattenEnv :: InScopeSet -> FlattenEnv
    emptyFlattenEnv InScopeSet
    in_scope
      = FlattenEnv { fe_type_map :: TypeMap (OutTyVar, TyCon, [Type])
    fe_type_map = TypeMap (OutTyVar, TyCon, [Type])
    forall a. TypeMap a
    emptyTypeMap
                   , fe_in_scope :: InScopeSet
    fe_in_scope = InScopeSet
    in_scope }

    updateInScopeSet :: FlattenEnv -> (InScopeSet -> InScopeSet) -> FlattenEnv
    updateInScopeSet :: FlattenEnv -> (InScopeSet -> InScopeSet) -> FlattenEnv
    updateInScopeSet FlattenEnv
    env InScopeSet -> InScopeSet
    upd = FlattenEnv
    env { fe_in_scope = upd (fe_in_scope env) }

    flattenTys :: InScopeSet -> [Type] -> [Type]
    -- See Note [Flattening type-family applications when matching instances]
    flattenTys :: InScopeSet -> [Type] -> [Type]
    flattenTys InScopeSet
    in_scope [Type]
    tys = ([Type], TyVarEnv (TyCon, [Type])) -> [Type]
    forall a b. (a, b) -> a
    fst (InScopeSet -> [Type] -> ([Type], TyVarEnv (TyCon, [Type]))
    flattenTysX InScopeSet
    in_scope [Type]
    tys)

    flattenTysX :: InScopeSet -> [Type] -> ([Type], TyVarEnv (TyCon, [Type]))
    -- See Note [Flattening type-family applications when matching instances]
    -- NB: the returned types mention the fresh type variables
    --     in the domain of the returned env, whose range includes
    --     the original type family applications. Building a substitution
    --     from this information and applying it would yield the original
    --     types -- almost. The problem is that the original type might
    --     have something like (forall b. F a b); the returned environment
    --     can't really sensibly refer to that b. So it may include a locally-
    --     bound tyvar in its range. Currently, the only usage of this env't
    --     checks whether there are any meta-variables in it
    --     (in GHC.Tc.Solver.Monad.mightEqualLater), so this is all OK.
    flattenTysX :: InScopeSet -> [Type] -> ([Type], TyVarEnv (TyCon, [Type]))
    flattenTysX InScopeSet
    in_scope [Type]
    tys
      = let (FlattenEnv
    env, [Type]
    result) = TvSubstEnv -> FlattenEnv -> [Type] -> (FlattenEnv, [Type])
    coreFlattenTys TvSubstEnv
    emptyTvSubstEnv (InScopeSet -> FlattenEnv
    emptyFlattenEnv InScopeSet
    in_scope) [Type]
    tys in
        ([Type]
    result, TypeMap (OutTyVar, TyCon, [Type]) -> TyVarEnv (TyCon, [Type])
    build_env (FlattenEnv -> TypeMap (OutTyVar, TyCon, [Type])
    fe_type_map FlattenEnv
    env))
      where
        build_env :: TypeMap (TyVar, TyCon, [Type]) -> TyVarEnv (TyCon, [Type])
        build_env :: TypeMap (OutTyVar, TyCon, [Type]) -> TyVarEnv (TyCon, [Type])
    build_env TypeMap (OutTyVar, TyCon, [Type])
    env_in
          = ((OutTyVar, TyCon, [Type])
     -> TyVarEnv (TyCon, [Type]) -> TyVarEnv (TyCon, [Type]))
    -> TypeMap (OutTyVar, TyCon, [Type])
    -> TyVarEnv (TyCon, [Type])
    -> TyVarEnv (TyCon, [Type])
    forall a b. (a -> b -> b) -> TypeMap a -> b -> b
    forall (m :: * -> *) a b.
    TrieMap m =>
    (a -> b -> b) -> m a -> b -> b
    foldTM (\(OutTyVar
    tv, TyCon
    tc, [Type]
    tys) TyVarEnv (TyCon, [Type])
    env_out -> TyVarEnv (TyCon, [Type])
    -> OutTyVar -> (TyCon, [Type]) -> TyVarEnv (TyCon, [Type])
    forall a. VarEnv a -> OutTyVar -> a -> VarEnv a
    extendVarEnv TyVarEnv (TyCon, [Type])
    env_out OutTyVar
    tv (TyCon
    tc, [Type]
    tys))
                   TypeMap (OutTyVar, TyCon, [Type])
    env_in TyVarEnv (TyCon, [Type])
    forall a. VarEnv a
    emptyVarEnv

    coreFlattenTys :: TvSubstEnv -> FlattenEnv
                   -> [Type] -> (FlattenEnv, [Type])
    coreFlattenTys :: TvSubstEnv -> FlattenEnv -> [Type] -> (FlattenEnv, [Type])
    coreFlattenTys TvSubstEnv
    subst = (FlattenEnv -> Type -> (FlattenEnv, Type))
    -> FlattenEnv -> [Type] -> (FlattenEnv, [Type])
    forall (t :: * -> *) s a b.
    Traversable t =>
    (s -> a -> (s, b)) -> s -> t a -> (s, t b)
    mapAccumL (TvSubstEnv -> FlattenEnv -> Type -> (FlattenEnv, Type)
    coreFlattenTy TvSubstEnv
    subst)

    coreFlattenTy :: TvSubstEnv -> FlattenEnv
                  -> Type -> (FlattenEnv, Type)
    coreFlattenTy :: TvSubstEnv -> FlattenEnv -> Type -> (FlattenEnv, Type)
    coreFlattenTy TvSubstEnv
    subst = FlattenEnv -> Type -> (FlattenEnv, Type)
    go
      where
        go :: FlattenEnv -> Type -> (FlattenEnv, Type)
    go FlattenEnv
    env Type
    ty | Just Type
    ty' <- Type -> Maybe Type
    coreView Type
    ty = FlattenEnv -> Type -> (FlattenEnv, Type)
    go FlattenEnv
    env Type
    ty'

        go FlattenEnv
    env (TyVarTy OutTyVar
    tv)
          | Just Type
    ty <- TvSubstEnv -> OutTyVar -> Maybe Type
    forall a. VarEnv a -> OutTyVar -> Maybe a
    lookupVarEnv TvSubstEnv
    subst OutTyVar
    tv = (FlattenEnv
    env, Type
    ty)
          | Bool
    otherwise                        = let (FlattenEnv
    env', Type
    ki) = FlattenEnv -> Type -> (FlattenEnv, Type)
    go FlattenEnv
    env (OutTyVar -> Type
    tyVarKind OutTyVar
    tv) in
                                               (FlattenEnv
    env', OutTyVar -> Type
    mkTyVarTy (OutTyVar -> Type) -> OutTyVar -> Type
    forall a b. (a -> b) -> a -> b
    $ OutTyVar -> Type -> OutTyVar
    setTyVarKind OutTyVar
    tv Type
    ki)
        go FlattenEnv
    env (AppTy Type
    ty1 Type
    ty2) = let (FlattenEnv
    env1, Type
    ty1') = FlattenEnv -> Type -> (FlattenEnv, Type)
    go FlattenEnv
    env  Type
    ty1
                                     (FlattenEnv
    env2, Type
    ty2') = FlattenEnv -> Type -> (FlattenEnv, Type)
    go FlattenEnv
    env1 Type
    ty2 in
                                 (FlattenEnv
    env2, Type -> Type -> Type
    AppTy Type
    ty1' Type
    ty2')
        go FlattenEnv
    env (TyConApp TyCon
    tc [Type]
    tys)
             -- NB: Don't just check if isFamilyTyCon: this catches *data* families,
             -- which are generative and thus can be preserved during flattening
          | Bool -> Bool
    not (TyCon -> Role -> Bool
    isGenerativeTyCon TyCon
    tc Role
    Nominal)
          = TvSubstEnv -> FlattenEnv -> TyCon -> [Type] -> (FlattenEnv, Type)
    coreFlattenTyFamApp TvSubstEnv
    subst FlattenEnv
    env TyCon
    tc [Type]
    tys

          | Bool
    otherwise
          = let (FlattenEnv
    env', [Type]
    tys') = TvSubstEnv -> FlattenEnv -> [Type] -> (FlattenEnv, [Type])
    coreFlattenTys TvSubstEnv
    subst FlattenEnv
    env [Type]
    tys in
            (FlattenEnv
    env', TyCon -> [Type] -> Type
    mkTyConApp TyCon
    tc [Type]
    tys')

        go FlattenEnv
    env ty :: Type
    ty@(FunTy { ft_mult :: Type -> Type
    ft_mult = Type
    mult, ft_arg :: Type -> Type
    ft_arg = Type
    ty1, ft_res :: Type -> Type
    ft_res = Type
    ty2 })
          = let (FlattenEnv
    env1, Type
    ty1') = FlattenEnv -> Type -> (FlattenEnv, Type)
    go FlattenEnv
    env  Type
    ty1
                (FlattenEnv
    env2, Type
    ty2') = FlattenEnv -> Type -> (FlattenEnv, Type)
    go FlattenEnv
    env1 Type
    ty2
                (FlattenEnv
    env3, Type
    mult') = FlattenEnv -> Type -> (FlattenEnv, Type)
    go FlattenEnv
    env2 Type
    mult in
            (FlattenEnv
    env3, Type
    ty { ft_mult = mult', ft_arg = ty1', ft_res = ty2' })

        go FlattenEnv
    env (ForAllTy (Bndr OutTyVar
    tv ForAllTyFlag
    vis) Type
    ty)
          = let (FlattenEnv
    env1, TvSubstEnv
    subst', OutTyVar
    tv') = TvSubstEnv
    -> FlattenEnv -> OutTyVar -> (FlattenEnv, TvSubstEnv, OutTyVar)
    coreFlattenVarBndr TvSubstEnv
    subst FlattenEnv
    env OutTyVar
    tv
                (FlattenEnv
    env2, Type
    ty') = TvSubstEnv -> FlattenEnv -> Type -> (FlattenEnv, Type)
    coreFlattenTy TvSubstEnv
    subst' FlattenEnv
    env1 Type
    ty in
            (FlattenEnv
    env2, VarBndr OutTyVar ForAllTyFlag -> Type -> Type
    ForAllTy (OutTyVar -> ForAllTyFlag -> VarBndr OutTyVar ForAllTyFlag
    forall var argf. var -> argf -> VarBndr var argf
    Bndr OutTyVar
    tv' ForAllTyFlag
    vis) Type
    ty')

        go FlattenEnv
    env ty :: Type
    ty@(LitTy {}) = (FlattenEnv
    env, Type
    ty)

        go FlattenEnv
    env (CastTy Type
    ty CoercionN
    co)
          = let (FlattenEnv
    env1, Type
    ty') = FlattenEnv -> Type -> (FlattenEnv, Type)
    go FlattenEnv
    env Type
    ty
                (FlattenEnv
    env2, CoercionN
    co') = TvSubstEnv -> FlattenEnv -> CoercionN -> (FlattenEnv, CoercionN)
    coreFlattenCo TvSubstEnv
    subst FlattenEnv
    env1 CoercionN
    co in
            (FlattenEnv
    env2, Type -> CoercionN -> Type
    CastTy Type
    ty' CoercionN
    co')

        go FlattenEnv
    env (CoercionTy CoercionN
    co)
          = let (FlattenEnv
    env', CoercionN
    co') = TvSubstEnv -> FlattenEnv -> CoercionN -> (FlattenEnv, CoercionN)
    coreFlattenCo TvSubstEnv
    subst FlattenEnv
    env CoercionN
    co in
            (FlattenEnv
    env', CoercionN -> Type
    CoercionTy CoercionN
    co')

    -- when flattening, we don't care about the contents of coercions.
    -- so, just return a fresh variable of the right (flattened) type
    coreFlattenCo :: TvSubstEnv -> FlattenEnv
                  -> Coercion -> (FlattenEnv, Coercion)
    coreFlattenCo :: TvSubstEnv -> FlattenEnv -> CoercionN -> (FlattenEnv, CoercionN)
    coreFlattenCo TvSubstEnv
    subst FlattenEnv
    env CoercionN
    co
      = (FlattenEnv
    env2, OutTyVar -> CoercionN
    mkCoVarCo OutTyVar
    covar)
      where
        (FlattenEnv
    env1, Type
    kind') = TvSubstEnv -> FlattenEnv -> Type -> (FlattenEnv, Type)
    coreFlattenTy TvSubstEnv
    subst FlattenEnv
    env (CoercionN -> Type
    coercionType CoercionN
    co)
        covar :: OutTyVar
    covar         = InScopeSet -> Type -> OutTyVar
    mkFlattenFreshCoVar (FlattenEnv -> InScopeSet
    fe_in_scope FlattenEnv
    env1) Type
    kind'
        -- Add the covar to the FlattenEnv's in-scope set.
        -- See Note [Flattening type-family applications when matching instances], wrinkle 2A.
        env2 :: FlattenEnv
    env2          = FlattenEnv -> (InScopeSet -> InScopeSet) -> FlattenEnv
    updateInScopeSet FlattenEnv
    env1 ((InScopeSet -> OutTyVar -> InScopeSet)
    -> OutTyVar -> InScopeSet -> InScopeSet
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip InScopeSet -> OutTyVar -> InScopeSet
    extendInScopeSet OutTyVar
    covar)

    coreFlattenVarBndr :: TvSubstEnv -> FlattenEnv
                       -> TyCoVar -> (FlattenEnv, TvSubstEnv, TyVar)
    coreFlattenVarBndr :: TvSubstEnv
    -> FlattenEnv -> OutTyVar -> (FlattenEnv, TvSubstEnv, OutTyVar)
    coreFlattenVarBndr TvSubstEnv
    subst FlattenEnv
    env OutTyVar
    tv
      = (FlattenEnv
    env2, TvSubstEnv
    subst', OutTyVar
    tv')
      where
        -- See Note [Flattening type-family applications when matching instances], wrinkle 2B.
        kind :: Type
    kind          = OutTyVar -> Type
    varType OutTyVar
    tv
        (FlattenEnv
    env1, Type
    kind') = TvSubstEnv -> FlattenEnv -> Type -> (FlattenEnv, Type)
    coreFlattenTy TvSubstEnv
    subst FlattenEnv
    env Type
    kind
        tv' :: OutTyVar
    tv'           = InScopeSet -> OutTyVar -> OutTyVar
    uniqAway (FlattenEnv -> InScopeSet
    fe_in_scope FlattenEnv
    env1) (OutTyVar -> Type -> OutTyVar
    setVarType OutTyVar
    tv Type
    kind')
        subst' :: TvSubstEnv
    subst'        = TvSubstEnv -> OutTyVar -> Type -> TvSubstEnv
    forall a. VarEnv a -> OutTyVar -> a -> VarEnv a
    extendVarEnv TvSubstEnv
    subst OutTyVar
    tv (OutTyVar -> Type
    mkTyVarTy OutTyVar
    tv')
        env2 :: FlattenEnv
    env2          = FlattenEnv -> (InScopeSet -> InScopeSet) -> FlattenEnv
    updateInScopeSet FlattenEnv
    env1 ((InScopeSet -> OutTyVar -> InScopeSet)
    -> OutTyVar -> InScopeSet -> InScopeSet
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip InScopeSet -> OutTyVar -> InScopeSet
    extendInScopeSet OutTyVar
    tv')

    coreFlattenTyFamApp :: TvSubstEnv -> FlattenEnv
                        -> TyCon         -- type family tycon
                        -> [Type]        -- args, already flattened
                        -> (FlattenEnv, Type)
    coreFlattenTyFamApp :: TvSubstEnv -> FlattenEnv -> TyCon -> [Type] -> (FlattenEnv, Type)
    coreFlattenTyFamApp TvSubstEnv
    tv_subst FlattenEnv
    env TyCon
    fam_tc [Type]
    fam_args
      = case TypeMap (OutTyVar, TyCon, [Type])
    -> Type -> Maybe (OutTyVar, TyCon, [Type])
    forall a. TypeMap a -> Type -> Maybe a
    lookupTypeMap TypeMap (OutTyVar, TyCon, [Type])
    type_map Type
    fam_ty of
          Just (OutTyVar
    tv, TyCon
    _, [Type]
    _) -> (FlattenEnv
    env', Type -> [Type] -> Type
    mkAppTys (OutTyVar -> Type
    mkTyVarTy OutTyVar
    tv) [Type]
    leftover_args')
          Maybe (OutTyVar, TyCon, [Type])
    Nothing ->
            let tyvar_name :: Name
    tyvar_name = TyCon -> Name
    forall a. Uniquable a => a -> Name
    mkFlattenFreshTyName TyCon
    fam_tc
                tv :: OutTyVar
    tv         = InScopeSet -> OutTyVar -> OutTyVar
    uniqAway InScopeSet
    in_scope (OutTyVar -> OutTyVar) -> OutTyVar -> OutTyVar
    forall a b. (a -> b) -> a -> b
    $
                             Name -> Type -> OutTyVar
    mkTyVar Name
    tyvar_name (HasDebugCallStack => Type -> Type
    Type -> Type
    typeKind Type
    fam_ty)

                ty' :: Type
    ty'   = Type -> [Type] -> Type
    mkAppTys (OutTyVar -> Type
    mkTyVarTy OutTyVar
    tv) [Type]
    leftover_args'
                env'' :: FlattenEnv
    env'' = FlattenEnv
    env' { fe_type_map = extendTypeMap type_map fam_ty
                                                           (tv, fam_tc, sat_fam_args)
                             , fe_in_scope = extendInScopeSet in_scope tv }
            in (FlattenEnv
    env'', Type
    ty')
      where
        arity :: Arity
    arity = TyCon -> Arity
    tyConArity TyCon
    fam_tc
        tcv_subst :: Subst
    tcv_subst = InScopeSet -> IdSubstEnv -> TvSubstEnv -> CvSubstEnv -> Subst
    Subst (FlattenEnv -> InScopeSet
    fe_in_scope FlattenEnv
    env) IdSubstEnv
    emptyIdSubstEnv TvSubstEnv
    tv_subst CvSubstEnv
    forall a. VarEnv a
    emptyVarEnv
        ([Type]
    sat_fam_args, [Type]
    leftover_args) = Bool -> ([Type], [Type]) -> ([Type], [Type])
    forall a. HasCallStack => Bool -> a -> a
    assert (Arity
    arity Arity -> Arity -> Bool
    forall a. Ord a => a -> a -> Bool
    <= [Type] -> Arity
    forall a. [a] -> Arity
    forall (t :: * -> *) a. Foldable t => t a -> Arity
    length [Type]
    fam_args) (([Type], [Type]) -> ([Type], [Type]))
    -> ([Type], [Type]) -> ([Type], [Type])
    forall a b. (a -> b) -> a -> b
    $
                                        Arity -> [Type] -> ([Type], [Type])
    forall a. Arity -> [a] -> ([a], [a])
    splitAt Arity
    arity [Type]
    fam_args
        -- Apply the substitution before looking up an application in the
        -- environment. See Note [Flattening type-family applications when matching instances],
        -- wrinkle 1.
        -- NB: substTys short-cuts the common case when the substitution is empty.
        sat_fam_args' :: [Type]
    sat_fam_args' = HasDebugCallStack => Subst -> [Type] -> [Type]
    Subst -> [Type] -> [Type]
    substTys Subst
    tcv_subst [Type]
    sat_fam_args
        (FlattenEnv
    env', [Type]
    leftover_args') = TvSubstEnv -> FlattenEnv -> [Type] -> (FlattenEnv, [Type])
    coreFlattenTys TvSubstEnv
    tv_subst FlattenEnv
    env [Type]
    leftover_args
        -- `fam_tc` may be over-applied to `fam_args` (see
        -- Note [Flattening type-family applications when matching instances]
        -- wrinkle 3), so we split it into the arguments needed to saturate it
        -- (sat_fam_args') and the rest (leftover_args')
        fam_ty :: Type
    fam_ty = TyCon -> [Type] -> Type
    mkTyConApp TyCon
    fam_tc [Type]
    sat_fam_args'
        FlattenEnv { fe_type_map :: FlattenEnv -> TypeMap (OutTyVar, TyCon, [Type])
    fe_type_map = TypeMap (OutTyVar, TyCon, [Type])
    type_map
                   , fe_in_scope :: FlattenEnv -> InScopeSet
    fe_in_scope = InScopeSet
    in_scope } = FlattenEnv
    env'

    mkFlattenFreshTyName :: Uniquable a => a -> Name
    mkFlattenFreshTyName :: forall a. Uniquable a => a -> Name
    mkFlattenFreshTyName a
    unq
      = Unique -> FastString -> Name
    mkSysTvName (a -> Unique
    forall a. Uniquable a => a -> Unique
    getUnique a
    unq) (String -> FastString
    fsLit String
    "flt")

    mkFlattenFreshCoVar :: InScopeSet -> Kind -> CoVar
    mkFlattenFreshCoVar :: InScopeSet -> Type -> OutTyVar
    mkFlattenFreshCoVar InScopeSet
    in_scope Type
    kind
      = let uniq :: Unique
    uniq = InScopeSet -> Unique
    unsafeGetFreshLocalUnique InScopeSet
    in_scope
            name :: Name
    name = Unique -> FastString -> Name
    mkSystemVarName Unique
    uniq (String -> FastString
    fsLit String
    "flc")
        in Name -> Type -> OutTyVar
    mkCoVar Name
    name Type
    kind