    -- (c) The University of Glasgow 2006

    {-# LANGUAGE CPP #-}

    module GHC.Core.Coercion.Opt
       ( optCoercion
       , OptCoercionOpts (..)
       )
    where

    import GHC.Prelude

    import GHC.Tc.Utils.TcType   ( exactTyCoVarsOfType )

    import GHC.Core.TyCo.Rep
    import GHC.Core.TyCo.Subst
    import GHC.Core.TyCo.Compare( eqType, eqForAllVis )
    import GHC.Core.Coercion
    import GHC.Core.Type as Type hiding( substTyVarBndr, substTy )
    import GHC.Core.TyCon
    import GHC.Core.Coercion.Axiom
    import GHC.Core.Unify

    import GHC.Types.Basic( SwapFlag(..), flipSwap, isSwapped, pickSwap, notSwapped )
    import GHC.Types.Var
    import GHC.Types.Var.Set
    import GHC.Types.Var.Env

    import GHC.Data.Pair

    import GHC.Utils.Outputable
    import GHC.Utils.Constants (debugIsOn)
    import GHC.Utils.Misc
    import GHC.Utils.Panic

    import Control.Monad   ( zipWithM )

    {-
    %************************************************************************
    %*                                                                      *
                     Optimising coercions
    %*                                                                      *
    %************************************************************************

    This module does coercion optimisation.  See the paper

       Evidence normalization in Systtem FV (RTA'13)
       https://simon.peytonjones.org/evidence-normalization/

    The paper is also in the GHC repo, in docs/opt-coercion.

    Note [Optimising coercion optimisation]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    Looking up a coercion's role or kind is linear in the size of the
    coercion. Thus, doing this repeatedly during the recursive descent
    of coercion optimisation is disastrous. We must be careful to avoid
    doing this if at all possible.

    Because it is generally easy to know a coercion's components' roles
    from the role of the outer coercion, we pass down the known role of
    the input in the algorithm below. We also keep functions opt_co2
    and opt_co3 separate from opt_co4, so that the former two do Phantom
    checks that opt_co4 can avoid. This is a big win because Phantom coercions
    rarely appear within non-phantom coercions -- only in some TyConAppCos
    and some AxiomInstCos. We handle these cases specially by calling
    opt_co2.

    Note [Optimising InstCo]
    ~~~~~~~~~~~~~~~~~~~~~~~~
    Optimising InstCo is pretty subtle: #15725, #25387.

    (1) tv is a type variable. We want to optimise

      InstCo (ForAllCo tv kco g) g2  -->   S(g)

    where S is some substitution. Let's look at the typing rules.

        kco : k1 ~ k2
        tv:k1 |- g : t1 ~ t2
        -----------------------------
        ForAllCo tv kco g : (all tv:k1.t1) ~ (all tv:k2.t2[tv |-> tv |> sym kco])

        g1 : (all tv:k1.t1') ~ (all tv:k2.t2')
        g2 : (s1:k1) ~ (s2:k2)
        --------------------
        InstCo g1 g2 : t1'[tv |-> s1] ~ t2'[tv |-> s2]

    Putting these two together

        kco : k1 ~ k2
        tv:k1 |- g : t1 ~ t2
        g2 : (s1:k1) ~ (s2:k2)
        --------------------
        InstCo (ForAllCo tv kco g) g2 : t1[tv |-> s1] ~ t2[tv |-> s2 |> sym kco]

    We thus want S(g) to have kind

      S(g) :: (t1[tv |-> s1]) ~ (t2[tv |-> s2 |> sym kco])

    All we need do is to substitute the coercion tv_co for tv:
      S = [tv :-> tv_co]
    where
      tv_co : s1 ~ (s2 |> sym kco)
    This looks bizarre, because we're substituting a /type variable/ with a
    /coercion/. However, this operation already exists: it's called *lifting*, and
    defined in GHC.Core.Coercion.  We just need to enhance the lifting operation to
    be able to deal with an ambient substitution, which is why a LiftingContext
    stores a TCvSubst.

    In general if
      S = [tv :-> tv_co]
      tv_co : r1 ~ r2
      g     : t1 ~ t2
    then
      S(g) : t1[tv :-> r1] ~ t2[tv :-> r2]

    The substitution S is embodied in the LiftingContext argument of `opt_co4`;
    See Note [The LiftingContext in optCoercion]

    (2) cv is a coercion variable
    Now consider we have (InstCo (ForAllCo cv h g) g2), we want to optimise.

    h : (t1 ~r t2) ~N (t3 ~r t4)
    cv : t1 ~r t2 |- g : t1' ~r2 t2'
    n1 = nth r 2 (downgradeRole r N h) :: t1 ~r t3
    n2 = nth r 3 (downgradeRole r N h) :: t2 ~r t4
    ------------------------------------------------
    ForAllCo cv h g : (all cv:t1 ~r t2. t1') ~r2
                      (all cv:t3 ~r t4. t2'[cv |-> n1 ; cv ; sym n2])

    g1 : (all cv:t1 ~r t2. t1') ~ (all cv: t3 ~r t4. t2')
    g2 : h1 ~N h2
    h1 : t1 ~r t2
    h2 : t3 ~r t4
    ------------------------------------------------
    InstCo g1 g2 : t1'[cv |-> h1] ~ t2'[cv |-> h2]

    We thus want some coercion proving this:

      t1'[cv |-> h1] ~ t2'[cv |-> n1 ; h2; sym n2]

    So we substitute the coercion variable c for the coercion
    (h1 ~N (n1; h2; sym n2)) in g.

    Note [The LiftingContext in optCoercion]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    To suppport Note [Optimising InstCo] the coercion optimiser carries a
    GHC.Core.Coercion.LiftingContext, which comprises
      * An ordinary Subst
      * The `lc_env`: a mapping from /type variables/ to /coercions/

    We don't actually have a separate function
       liftCoSubstCo :: LiftingContext -> Coercion -> Coercion
    The substitution of a type variable by a coercion is done by the calls to
    `liftCoSubst` (on a type) in the Refl and GRefl cases of `opt_co4`.

    We use the following invariants:
     (LC1) The coercions in the range of `lc_env` have already had all substitutions
           applied; they are "OutCoercions".  If you re-optimise these coercions, you
           must zap the LiftingContext first.

     (LC2) However they have /not/ had the "ambient sym" (the second argument of
           `opt_co4`) applied.  The ambient sym applies to the entire coercion not
           to the little bits being substituted.
    -}

    -- | Coercion optimisation options
    newtype OptCoercionOpts = OptCoercionOpts
       { OptCoercionOpts -> Bool
    optCoercionEnabled :: Bool  -- ^ Enable coercion optimisation (reduce its size)
       }

    optCoercion :: OptCoercionOpts -> Subst -> Coercion -> NormalCo
    -- ^ optCoercion applies a substitution to a coercion,
    --   *and* optimises it to reduce its size
    optCoercion :: OptCoercionOpts -> Subst -> Coercion -> Coercion
    optCoercion OptCoercionOpts
    opts Subst
    env Coercion
    co
      | OptCoercionOpts -> Bool
    optCoercionEnabled OptCoercionOpts
    opts
      = Subst -> Coercion -> Coercion
    optCoercion' Subst
    env Coercion
    co

    {-
      = pprTrace "optCoercion {" (text "Co:" <> ppr (coercionSize co)) $
        let result = optCoercion' env co in
        pprTrace "optCoercion }"
           (vcat [ text "Co:"    <+> ppr (coercionSize co)
                 , text "Optco:" <+> ppWhen (isReflCo result) (text "(refl)")
                                 <+> ppr (coercionSize result) ]) $
        result
    -}

      | Bool
    otherwise
      = HasDebugCallStack => Subst -> Coercion -> Coercion
    Subst -> Coercion -> Coercion
    substCo Subst
    env Coercion
    co

    optCoercion' :: Subst -> Coercion -> NormalCo
    optCoercion' :: Subst -> Coercion -> Coercion
    optCoercion' Subst
    env Coercion
    co
      | Bool
    debugIsOn
      = let out_co :: Coercion
    out_co = LiftingContext -> SwapFlag -> Coercion -> Coercion
    opt_co1 LiftingContext
    lc SwapFlag
    NotSwapped Coercion
    co
            (Pair Type
    in_ty1  Type
    in_ty2,  Role
    in_role)  = Coercion -> (Pair Type, Role)
    coercionKindRole Coercion
    co
            (Pair Type
    out_ty1 Type
    out_ty2, Role
    out_role) = Coercion -> (Pair Type, Role)
    coercionKindRole Coercion
    out_co

            details :: SDoc
    details = [SDoc] -> SDoc
    forall doc. IsDoc doc => [doc] -> doc
    vcat [ String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "in_co:" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> Coercion -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Coercion
    co
                           , String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "in_ty1:" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> Type -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Type
    in_ty1
                           , String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "in_ty2:" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> Type -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Type
    in_ty2
                           , String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "out_co:" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> Coercion -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Coercion
    out_co
                           , String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "out_ty1:" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> Type -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Type
    out_ty1
                           , String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "out_ty2:" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> Type -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Type
    out_ty2
                           , String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "in_role:" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> Role -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Role
    in_role
                           , String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "out_role:" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> Role -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Role
    out_role
                           ]
        in
        Bool -> String -> SDoc -> Coercion -> Coercion
    forall a. HasCallStack => Bool -> String -> SDoc -> a -> a
    warnPprTrace (Bool -> Bool
    not (Coercion -> Bool
    isReflCo Coercion
    out_co) Bool -> Bool -> Bool
    && Coercion -> Bool
    isReflexiveCo Coercion
    out_co)
                     String
    "optCoercion: reflexive but not refl" SDoc
    details (Coercion -> Coercion) -> Coercion -> Coercion
    forall a b. (a -> b) -> a -> b
    $
    --    assertPpr (substTyUnchecked env in_ty1 `eqType` out_ty1 &&
    --               substTyUnchecked env in_ty2 `eqType` out_ty2 &&
    --               in_role == out_role)
    --              (hang (text "optCoercion changed types!") 2 details) $
        Coercion
    out_co

      | Bool
    otherwise
      = LiftingContext -> SwapFlag -> Coercion -> Coercion
    opt_co1 LiftingContext
    lc SwapFlag
    NotSwapped Coercion
    co
      where
        lc :: LiftingContext
    lc = Subst -> LiftingContext
    mkSubstLiftingContext Subst
    env
    --    ppr_one cv = ppr cv <+> dcolon <+> ppr (coVarKind cv)

    type NormalCo    = Coercion
      -- Invariants:
      --  * The substitution has been fully applied
      --  * For trans coercions (co1 `trans` co2)
      --       co1 is not a trans, and neither co1 nor co2 is identity

    type NormalNonIdCo = NormalCo  -- Extra invariant: not the identity

    -- | Do we force the result to be representational?
    type ReprFlag = Bool

    -- | Optimize a coercion, making no assumptions. All coercions in
    -- the lifting context are already optimized (and sym'd if nec'y)
    opt_co1 :: LiftingContext
            -> SwapFlag   -- IsSwapped => apply Sym to the result
            -> Coercion -> NormalCo
    opt_co1 :: LiftingContext -> SwapFlag -> Coercion -> Coercion
    opt_co1 LiftingContext
    env SwapFlag
    sym Coercion
    co = LiftingContext -> SwapFlag -> Role -> Coercion -> Coercion
    opt_co2 LiftingContext
    env SwapFlag
    sym (Coercion -> Role
    coercionRole Coercion
    co) Coercion
    co

    -- See Note [Optimising coercion optimisation]
    -- | Optimize a coercion, knowing the coercion's role. No other assumptions.
    opt_co2 :: LiftingContext
            -> SwapFlag   -- ^IsSwapped => apply Sym to the result
            -> Role       -- ^ The role of the input coercion
            -> Coercion -> NormalCo
    opt_co2 :: LiftingContext -> SwapFlag -> Role -> Coercion -> Coercion
    opt_co2 LiftingContext
    env SwapFlag
    sym Role
    Phantom Coercion
    co = LiftingContext -> SwapFlag -> Coercion -> Coercion
    opt_phantom LiftingContext
    env SwapFlag
    sym Coercion
    co
    opt_co2 LiftingContext
    env SwapFlag
    sym Role
    r       Coercion
    co = LiftingContext -> SwapFlag -> Bool -> Role -> Coercion -> Coercion
    opt_co4 LiftingContext
    env SwapFlag
    sym Bool
    False Role
    r Coercion
    co

    -- See Note [Optimising coercion optimisation]
    -- | Optimize a coercion, knowing the coercion's non-Phantom role,
    --   and with an optional downgrade
    opt_co3 :: LiftingContext -> SwapFlag -> Maybe Role -> Role -> Coercion -> NormalCo
    opt_co3 :: LiftingContext
    -> SwapFlag -> Maybe Role -> Role -> Coercion -> Coercion
    opt_co3 LiftingContext
    env SwapFlag
    sym (Just Role
    Phantom)          Role
    _ Coercion
    co = LiftingContext -> SwapFlag -> Coercion -> Coercion
    opt_phantom LiftingContext
    env SwapFlag
    sym Coercion
    co
    opt_co3 LiftingContext
    env SwapFlag
    sym (Just Role
    Representational) Role
    r Coercion
    co = LiftingContext -> SwapFlag -> Bool -> Role -> Coercion -> Coercion
    opt_co4 LiftingContext
    env SwapFlag
    sym Bool
    True  Role
    r Coercion
    co
      -- if mrole is Just Nominal, that can't be a downgrade, so we can ignore
    opt_co3 LiftingContext
    env SwapFlag
    sym Maybe Role
    _                       Role
    r Coercion
    co = LiftingContext -> SwapFlag -> Bool -> Role -> Coercion -> Coercion
    opt_co4 LiftingContext
    env SwapFlag
    sym Bool
    False Role
    r Coercion
    co

    -- See Note [Optimising coercion optimisation]
    -- | Optimize a non-phantom coercion.
    opt_co4, opt_co4' :: LiftingContext -> SwapFlag -> ReprFlag
                      -> Role -> Coercion -> NormalCo
    -- Precondition:  In every call (opt_co4 lc sym rep role co)
    --                we should have role = coercionRole co
    -- Precondition:  role is not Phantom
    -- Postcondition: The resulting coercion is equivalant to
    --                     wrapsub (wrapsym (mksub co)
    --                 where wrapsym is SymCo if sym=True
    --                       wrapsub is SubCo if rep=True

    -- opt_co4 is there just to support tracing, when debugging
    -- Usually it just goes straight to opt_co4'
    opt_co4 :: LiftingContext -> SwapFlag -> Bool -> Role -> Coercion -> Coercion
    opt_co4 = LiftingContext -> SwapFlag -> Bool -> Role -> Coercion -> Coercion
    opt_co4'

    {-
    opt_co4 env sym rep r co
      = pprTrace "opt_co4 {"
       ( vcat [ text "Sym:" <+> ppr sym
              , text "Rep:" <+> ppr rep
              , text "Role:" <+> ppr r
              , text "Co:" <+> ppr co ]) $
       assert (r == coercionRole co )    $
       let result = opt_co4' env sym rep r co in
       pprTrace "opt_co4 }" (ppr co $$ text "---" $$ ppr result) $
       assertPpr (res_role == coercionRole result)
                 (vcat [ text "Role:" <+> ppr r
                       , text "Result: " <+>  ppr result
                       , text "Result type:" <+> ppr (coercionType result) ]) $
       result

      where
        res_role | rep       = Representational
                 | otherwise = r
    -}

    opt_co4' :: LiftingContext -> SwapFlag -> Bool -> Role -> Coercion -> Coercion
    opt_co4' LiftingContext
    env SwapFlag
    sym Bool
    rep Role
    r (Refl Type
    ty)
      = Bool -> SDoc -> Coercion -> Coercion
    forall a. HasCallStack => Bool -> SDoc -> a -> a
    assertPpr (Role
    r Role -> Role -> Bool
    forall a. Eq a => a -> a -> Bool
    == Role
    Nominal)
                  (String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "Expected role:" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> Role -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Role
    r    SDoc -> SDoc -> SDoc
    forall doc. IsDoc doc => doc -> doc -> doc
    $$
                   String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "Found role:" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> Role -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Role
    Nominal SDoc -> SDoc -> SDoc
    forall doc. IsDoc doc => doc -> doc -> doc
    $$
                   String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "Type:" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> Type -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Type
    ty) (Coercion -> Coercion) -> Coercion -> Coercion
    forall a b. (a -> b) -> a -> b
    $
        SwapFlag -> Coercion -> Coercion
    wrapSym SwapFlag
    sym (Coercion -> Coercion) -> Coercion -> Coercion
    forall a b. (a -> b) -> a -> b
    $ HasDebugCallStack => Role -> LiftingContext -> Type -> Coercion
    Role -> LiftingContext -> Type -> Coercion
    liftCoSubst (Bool -> Role -> Role
    chooseRole Bool
    rep Role
    r) LiftingContext
    env Type
    ty
            -- wrapSym: see (LC2) of Note [The LiftingContext in optCoercion]

    opt_co4' LiftingContext
    env SwapFlag
    sym Bool
    rep Role
    r (GRefl Role
    _r Type
    ty MCoercion
    MRefl)
      = Bool -> SDoc -> Coercion -> Coercion
    forall a. HasCallStack => Bool -> SDoc -> a -> a
    assertPpr (Role
    r Role -> Role -> Bool
    forall a. Eq a => a -> a -> Bool
    == Role
    _r)
                  (String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "Expected role:" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> Role -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Role
    r SDoc -> SDoc -> SDoc
    forall doc. IsDoc doc => doc -> doc -> doc
    $$
                   String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "Found role:" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> Role -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Role
    _r   SDoc -> SDoc -> SDoc
    forall doc. IsDoc doc => doc -> doc -> doc
    $$
                   String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "Type:" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> Type -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Type
    ty) (Coercion -> Coercion) -> Coercion -> Coercion
    forall a b. (a -> b) -> a -> b
    $
        SwapFlag -> Coercion -> Coercion
    wrapSym SwapFlag
    sym (Coercion -> Coercion) -> Coercion -> Coercion
    forall a b. (a -> b) -> a -> b
    $ HasDebugCallStack => Role -> LiftingContext -> Type -> Coercion
    Role -> LiftingContext -> Type -> Coercion
    liftCoSubst (Bool -> Role -> Role
    chooseRole Bool
    rep Role
    r) LiftingContext
    env Type
    ty
            -- wrapSym: see (LC2) of Note [The LiftingContext in optCoercion]

    opt_co4' LiftingContext
    env SwapFlag
    sym  Bool
    rep Role
    r (GRefl Role
    _r Type
    ty (MCo Coercion
    kco))
      = Bool -> SDoc -> Coercion -> Coercion
    forall a. HasCallStack => Bool -> SDoc -> a -> a
    assertPpr (Role
    r Role -> Role -> Bool
    forall a. Eq a => a -> a -> Bool
    == Role
    _r)
                  (String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "Expected role:" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> Role -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Role
    r SDoc -> SDoc -> SDoc
    forall doc. IsDoc doc => doc -> doc -> doc
    $$
                   String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "Found role:" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> Role -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Role
    _r   SDoc -> SDoc -> SDoc
    forall doc. IsDoc doc => doc -> doc -> doc
    $$
                   String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "Type:" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> Type -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Type
    ty) (Coercion -> Coercion) -> Coercion -> Coercion
    forall a b. (a -> b) -> a -> b
    $
        if Coercion -> Bool
    isGReflCo Coercion
    kco Bool -> Bool -> Bool
    || Coercion -> Bool
    isGReflCo Coercion
    kco'
        then SwapFlag -> Coercion -> Coercion
    wrapSym SwapFlag
    sym Coercion
    ty_co
        else SwapFlag -> Coercion -> Coercion
    wrapSym SwapFlag
    sym (Coercion -> Coercion) -> Coercion -> Coercion
    forall a b. (a -> b) -> a -> b
    $ HasDebugCallStack =>
    Role -> Type -> Coercion -> Coercion -> Coercion
    Role -> Type -> Coercion -> Coercion -> Coercion
    mk_coherence_right_co Role
    r' (HasDebugCallStack => Coercion -> Type
    Coercion -> Type
    coercionRKind Coercion
    ty_co) Coercion
    kco' Coercion
    ty_co
                -- ty :: k1
                -- kco :: k1 ~ k2
                -- Desired result coercion:   ty ~ ty |> co
      where
        r' :: Role
    r'    = Bool -> Role -> Role
    chooseRole Bool
    rep Role
    r
        ty_co :: Coercion
    ty_co = HasDebugCallStack => Role -> LiftingContext -> Type -> Coercion
    Role -> LiftingContext -> Type -> Coercion
    liftCoSubst Role
    r' LiftingContext
    env Type
    ty
        kco' :: Coercion
    kco'  = LiftingContext -> SwapFlag -> Bool -> Role -> Coercion -> Coercion
    opt_co4 LiftingContext
    env SwapFlag
    NotSwapped Bool
    False Role
    Nominal Coercion
    kco

    opt_co4' LiftingContext
    env SwapFlag
    sym Bool
    rep Role
    r (SymCo Coercion
    co)  = LiftingContext -> SwapFlag -> Bool -> Role -> Coercion -> Coercion
    opt_co4 LiftingContext
    env (SwapFlag -> SwapFlag
    flipSwap SwapFlag
    sym) Bool
    rep Role
    r Coercion
    co
      -- surprisingly, we don't have to do anything to the env here. This is
      -- because any "lifting" substitutions in the env are tied to ForAllCos,
      -- which treat their left and right sides differently. We don't want to
      -- exchange them.

    opt_co4' LiftingContext
    env SwapFlag
    sym Bool
    rep Role
    r g :: Coercion
    g@(TyConAppCo Role
    _r TyCon
    tc [Coercion]
    cos)
      = Bool -> Coercion -> Coercion
    forall a. HasCallStack => Bool -> a -> a
    assert (Role
    r Role -> Role -> Bool
    forall a. Eq a => a -> a -> Bool
    == Role
    _r) (Coercion -> Coercion) -> Coercion -> Coercion
    forall a b. (a -> b) -> a -> b
    $
        case (Bool
    rep, Role
    r) of
          (Bool
    True, Role
    Nominal) ->
            HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
    Role -> TyCon -> [Coercion] -> Coercion
    mkTyConAppCo Role
    Representational TyCon
    tc
                         ((Maybe Role -> Role -> Coercion -> Coercion)
    -> [Maybe Role] -> [Role] -> [Coercion] -> [Coercion]
    forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
    zipWith3 (LiftingContext
    -> SwapFlag -> Maybe Role -> Role -> Coercion -> Coercion
    opt_co3 LiftingContext
    env SwapFlag
    sym)
                                   ((Role -> Maybe Role) -> [Role] -> [Maybe Role]
    forall a b. (a -> b) -> [a] -> [b]
    map Role -> Maybe Role
    forall a. a -> Maybe a
    Just (TyCon -> [Role]
    tyConRoleListRepresentational TyCon
    tc))
                                   (Role -> [Role]
    forall a. a -> [a]
    repeat Role
    Nominal)
                                   [Coercion]
    cos)
          (Bool
    False, Role
    Nominal) ->
            HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
    Role -> TyCon -> [Coercion] -> Coercion
    mkTyConAppCo Role
    Nominal TyCon
    tc ((Coercion -> Coercion) -> [Coercion] -> [Coercion]
    forall a b. (a -> b) -> [a] -> [b]
    map (LiftingContext -> SwapFlag -> Bool -> Role -> Coercion -> Coercion
    opt_co4 LiftingContext
    env SwapFlag
    sym Bool
    False Role
    Nominal) [Coercion]
    cos)
          (Bool
    _, Role
    Representational) ->
                          -- must use opt_co2 here, because some roles may be P
                          -- See Note [Optimising coercion optimisation]
            HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
    Role -> TyCon -> [Coercion] -> Coercion
    mkTyConAppCo Role
    r TyCon
    tc ((Role -> Coercion -> Coercion)
    -> [Role] -> [Coercion] -> [Coercion]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith (LiftingContext -> SwapFlag -> Role -> Coercion -> Coercion
    opt_co2 LiftingContext
    env SwapFlag
    sym)
                                       (TyCon -> [Role]
    tyConRoleListRepresentational TyCon
    tc)  -- the current roles
                                       [Coercion]
    cos)
          (Bool
    _, Role
    Phantom) -> String -> SDoc -> Coercion
    forall a. HasCallStack => String -> SDoc -> a
    pprPanic String
    "opt_co4 sees a phantom!" (Coercion -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Coercion
    g)

    opt_co4' LiftingContext
    env SwapFlag
    sym Bool
    rep Role
    r (AppCo Coercion
    co1 Coercion
    co2)
      = Coercion -> Coercion -> Coercion
    mkAppCo (LiftingContext -> SwapFlag -> Bool -> Role -> Coercion -> Coercion
    opt_co4 LiftingContext
    env SwapFlag
    sym Bool
    rep Role
    r Coercion
    co1)
                (LiftingContext -> SwapFlag -> Bool -> Role -> Coercion -> Coercion
    opt_co4 LiftingContext
    env SwapFlag
    sym Bool
    False Role
    Nominal Coercion
    co2)

    opt_co4' LiftingContext
    env SwapFlag
    sym Bool
    rep Role
    r (ForAllCo { fco_tcv :: Coercion -> CoVar
    fco_tcv = CoVar
    tv, fco_visL :: Coercion -> ForAllTyFlag
    fco_visL = ForAllTyFlag
    visL, fco_visR :: Coercion -> ForAllTyFlag
    fco_visR = ForAllTyFlag
    visR
                                    , fco_kind :: Coercion -> Coercion
    fco_kind = Coercion
    k_co, fco_body :: Coercion -> Coercion
    fco_body = Coercion
    co })
      = case LiftingContext
    -> SwapFlag
    -> CoVar
    -> Coercion
    -> (LiftingContext, CoVar, Coercion)
    optForAllCoBndr LiftingContext
    env SwapFlag
    sym CoVar
    tv Coercion
    k_co of
          (LiftingContext
    env', CoVar
    tv', Coercion
    k_co') -> HasDebugCallStack =>
    CoVar
    -> ForAllTyFlag -> ForAllTyFlag -> Coercion -> Coercion -> Coercion
    CoVar
    -> ForAllTyFlag -> ForAllTyFlag -> Coercion -> Coercion -> Coercion
    mkForAllCo CoVar
    tv' ForAllTyFlag
    visL' ForAllTyFlag
    visR' Coercion
    k_co' (Coercion -> Coercion) -> Coercion -> Coercion
    forall a b. (a -> b) -> a -> b
    $
                                LiftingContext -> SwapFlag -> Bool -> Role -> Coercion -> Coercion
    opt_co4 LiftingContext
    env' SwapFlag
    sym Bool
    rep Role
    r Coercion
    co
         -- Use the "mk" functions to check for nested Refls
      where
        !(ForAllTyFlag
    visL', ForAllTyFlag
    visR') = SwapFlag
    -> (ForAllTyFlag, ForAllTyFlag) -> (ForAllTyFlag, ForAllTyFlag)
    forall a. SwapFlag -> (a, a) -> (a, a)
    swapSym SwapFlag
    sym (ForAllTyFlag
    visL, ForAllTyFlag
    visR)

    opt_co4' LiftingContext
    env SwapFlag
    sym Bool
    rep Role
    r (FunCo Role
    _r FunTyFlag
    afl FunTyFlag
    afr Coercion
    cow Coercion
    co1 Coercion
    co2)
      = Bool -> Coercion -> Coercion
    forall a. HasCallStack => Bool -> a -> a
    assert (Role
    r Role -> Role -> Bool
    forall a. Eq a => a -> a -> Bool
    == Role
    _r) (Coercion -> Coercion) -> Coercion -> Coercion
    forall a b. (a -> b) -> a -> b
    $
        Role
    -> FunTyFlag
    -> FunTyFlag
    -> Coercion
    -> Coercion
    -> Coercion
    -> Coercion
    mkFunCo2 Role
    r' FunTyFlag
    afl' FunTyFlag
    afr' Coercion
    cow' Coercion
    co1' Coercion
    co2'
      where
        co1' :: Coercion
    co1' = LiftingContext -> SwapFlag -> Bool -> Role -> Coercion -> Coercion
    opt_co4 LiftingContext
    env SwapFlag
    sym Bool
    rep Role
    r Coercion
    co1
        co2' :: Coercion
    co2' = LiftingContext -> SwapFlag -> Bool -> Role -> Coercion -> Coercion
    opt_co4 LiftingContext
    env SwapFlag
    sym Bool
    rep Role
    r Coercion
    co2
        cow' :: Coercion
    cow' = LiftingContext -> SwapFlag -> Coercion -> Coercion
    opt_co1 LiftingContext
    env SwapFlag
    sym Coercion
    cow
        !r' :: Role
    r' | Bool
    rep       = Role
    Representational
            | Bool
    otherwise = Role
    r
        !(FunTyFlag
    afl', FunTyFlag
    afr') = SwapFlag -> (FunTyFlag, FunTyFlag) -> (FunTyFlag, FunTyFlag)
    forall a. SwapFlag -> (a, a) -> (a, a)
    swapSym SwapFlag
    sym (FunTyFlag
    afl, FunTyFlag
    afr)

    opt_co4' LiftingContext
    env SwapFlag
    sym Bool
    rep Role
    r (CoVarCo CoVar
    cv)
      | Just Coercion
    co <- LiftingContext -> CoVar -> Maybe Coercion
    lcLookupCoVar LiftingContext
    env CoVar
    cv   -- see Note [Forall over coercion] for why
                                          -- this is the right thing here
      = -- pprTrace "CoVarCo" (ppr cv $$ ppr co) $
        LiftingContext -> SwapFlag -> Bool -> Role -> Coercion -> Coercion
    opt_co4 (LiftingContext -> LiftingContext
    zapLiftingContext LiftingContext
    env) SwapFlag
    sym Bool
    rep Role
    r Coercion
    co

      | Type
    ty1 HasCallStack => Type -> Type -> Bool
    Type -> Type -> Bool
    `eqType` Type
    ty2   -- See Note [Optimise CoVarCo to Refl]
      = Role -> Type -> Coercion
    mkReflCo (Bool -> Role -> Role
    chooseRole Bool
    rep Role
    r) Type
    ty1

      | Bool
    otherwise
      = Bool -> Coercion -> Coercion
    forall a. HasCallStack => Bool -> a -> a
    assert (CoVar -> Bool
    isCoVar CoVar
    cv1) (Coercion -> Coercion) -> Coercion -> Coercion
    forall a b. (a -> b) -> a -> b
    $
        Bool -> Role -> Coercion -> Coercion
    wrapRole Bool
    rep Role
    r (Coercion -> Coercion) -> Coercion -> Coercion
    forall a b. (a -> b) -> a -> b
    $ SwapFlag -> Coercion -> Coercion
    wrapSym SwapFlag
    sym (Coercion -> Coercion) -> Coercion -> Coercion
    forall a b. (a -> b) -> a -> b
    $
        CoVar -> Coercion
    CoVarCo CoVar
    cv1

      where
        Pair Type
    ty1 Type
    ty2 = HasDebugCallStack => CoVar -> Pair Type
    CoVar -> Pair Type
    coVarTypes CoVar
    cv1

        cv1 :: CoVar
    cv1 = case InScopeSet -> CoVar -> Maybe CoVar
    lookupInScope (LiftingContext -> InScopeSet
    lcInScopeSet LiftingContext
    env) CoVar
    cv of
                 Just CoVar
    cv1 -> CoVar
    cv1
                 Maybe CoVar
    Nothing  -> Bool -> String -> SDoc -> CoVar -> CoVar
    forall a. HasCallStack => Bool -> String -> SDoc -> a -> a
    warnPprTrace Bool
    True
                              String
    "opt_co: not in scope"
                              (CoVar -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr CoVar
    cv SDoc -> SDoc -> SDoc
    forall doc. IsDoc doc => doc -> doc -> doc
    $$ LiftingContext -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr LiftingContext
    env)
                              CoVar
    cv
              -- cv1 might have a substituted kind!

    opt_co4' LiftingContext
    _ SwapFlag
    _ Bool
    _ Role
    _ (HoleCo CoercionHole
    h)
      = String -> SDoc -> Coercion
    forall a. HasCallStack => String -> SDoc -> a
    pprPanic String
    "opt_univ fell into a hole" (CoercionHole -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr CoercionHole
    h)

    opt_co4' LiftingContext
    env SwapFlag
    sym Bool
    rep Role
    r (AxiomCo CoAxiomRule
    con [Coercion]
    cos)
        -- Do *not* push sym inside top-level axioms
        -- e.g. if g is a top-level axiom
        --   g a : f a ~ a
        -- then (sym (g ty)) /= g (sym ty) !!
      = Bool
    -> (Bool -> Role -> Coercion -> Coercion)
    -> Bool
    -> Role
    -> Coercion
    -> Coercion
    forall a. HasCallStack => Bool -> a -> a
    assert (Role
    r Role -> Role -> Bool
    forall a. Eq a => a -> a -> Bool
    == CoAxiomRule -> Role
    coAxiomRuleRole CoAxiomRule
    con )
        Bool -> Role -> Coercion -> Coercion
    wrapRole Bool
    rep (CoAxiomRule -> Role
    coAxiomRuleRole CoAxiomRule
    con) (Coercion -> Coercion) -> Coercion -> Coercion
    forall a b. (a -> b) -> a -> b
    $
        SwapFlag -> Coercion -> Coercion
    wrapSym SwapFlag
    sym (Coercion -> Coercion) -> Coercion -> Coercion
    forall a b. (a -> b) -> a -> b
    $
                           -- some sub-cos might be P: use opt_co2
                           -- See Note [Optimising coercion optimisation]
        CoAxiomRule -> [Coercion] -> Coercion
    AxiomCo CoAxiomRule
    con ((Role -> Coercion -> Coercion)
    -> [Role] -> [Coercion] -> [Coercion]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith (LiftingContext -> SwapFlag -> Role -> Coercion -> Coercion
    opt_co2 LiftingContext
    env SwapFlag
    NotSwapped)
                             (CoAxiomRule -> [Role]
    coAxiomRuleArgRoles CoAxiomRule
    con)
                             [Coercion]
    cos)
          -- Note that the_co does *not* have sym pushed into it

    opt_co4' LiftingContext
    env SwapFlag
    sym Bool
    rep Role
    r (UnivCo { uco_prov :: Coercion -> UnivCoProvenance
    uco_prov = UnivCoProvenance
    prov, uco_lty :: Coercion -> Type
    uco_lty = Type
    t1
                                  , uco_rty :: Coercion -> Type
    uco_rty = Type
    t2, uco_deps :: Coercion -> [Coercion]
    uco_deps = [Coercion]
    deps })
      = LiftingContext
    -> SwapFlag
    -> UnivCoProvenance
    -> [Coercion]
    -> Role
    -> Type
    -> Type
    -> Coercion
    opt_univ LiftingContext
    env SwapFlag
    sym UnivCoProvenance
    prov [Coercion]
    deps (Bool -> Role -> Role
    chooseRole Bool
    rep Role
    r) Type
    t1 Type
    t2

    opt_co4' LiftingContext
    env SwapFlag
    sym Bool
    rep Role
    r (TransCo Coercion
    co1 Coercion
    co2)
      -- sym (g `o` h) = sym h `o` sym g
      | SwapFlag -> Bool
    isSwapped SwapFlag
    sym = HasDebugCallStack => InScopeSet -> Coercion -> Coercion -> Coercion
    InScopeSet -> Coercion -> Coercion -> Coercion
    opt_trans InScopeSet
    in_scope Coercion
    co2' Coercion
    co1'
      | Bool
    otherwise     = HasDebugCallStack => InScopeSet -> Coercion -> Coercion -> Coercion
    InScopeSet -> Coercion -> Coercion -> Coercion
    opt_trans InScopeSet
    in_scope Coercion
    co1' Coercion
    co2'
      where
        co1' :: Coercion
    co1' = LiftingContext -> SwapFlag -> Bool -> Role -> Coercion -> Coercion
    opt_co4 LiftingContext
    env SwapFlag
    sym Bool
    rep Role
    r Coercion
    co1
        co2' :: Coercion
    co2' = LiftingContext -> SwapFlag -> Bool -> Role -> Coercion -> Coercion
    opt_co4 LiftingContext
    env SwapFlag
    sym Bool
    rep Role
    r Coercion
    co2
        in_scope :: InScopeSet
    in_scope = LiftingContext -> InScopeSet
    lcInScopeSet LiftingContext
    env

    opt_co4' LiftingContext
    env SwapFlag
    sym Bool
    rep Role
    r (SelCo CoSel
    cs Coercion
    co)
      -- Historical note 1: we used to check `co` for Refl, TyConAppCo etc
      -- before optimising `co`; but actually the SelCo will have been built
      -- with mkSelCo, so these tests always fail.

      -- Historical note 2: if rep=True and r=Nominal, we used to recursively
      -- call opt_co4 to re-optimse the result. But (a) that is inefficient
      -- and (b) wrapRole uses mkSubCo which does much the same job
      = Bool -> Role -> Coercion -> Coercion
    wrapRole Bool
    rep Role
    r (Coercion -> Coercion) -> Coercion -> Coercion
    forall a b. (a -> b) -> a -> b
    $ HasDebugCallStack => CoSel -> Coercion -> Coercion
    CoSel -> Coercion -> Coercion
    mkSelCo CoSel
    cs (Coercion -> Coercion) -> Coercion -> Coercion
    forall a b. (a -> b) -> a -> b
    $ LiftingContext -> SwapFlag -> Coercion -> Coercion
    opt_co1 LiftingContext
    env SwapFlag
    sym Coercion
    co

    opt_co4' LiftingContext
    env SwapFlag
    sym Bool
    rep Role
    r (LRCo LeftOrRight
    lr Coercion
    co)
      | Just (Coercion, Coercion)
    pr_co <- Coercion -> Maybe (Coercion, Coercion)
    splitAppCo_maybe Coercion
    co
      = Bool
    -> (LiftingContext
        -> SwapFlag -> Bool -> Role -> Coercion -> Coercion)
    -> LiftingContext
    -> SwapFlag
    -> Bool
    -> Role
    -> Coercion
    -> Coercion
    forall a. HasCallStack => Bool -> a -> a
    assert (Role
    r Role -> Role -> Bool
    forall a. Eq a => a -> a -> Bool
    == Role
    Nominal )
        LiftingContext -> SwapFlag -> Bool -> Role -> Coercion -> Coercion
    opt_co4 LiftingContext
    env SwapFlag
    sym Bool
    rep Role
    Nominal (LeftOrRight -> (Coercion, Coercion) -> Coercion
    forall {a}. LeftOrRight -> (a, a) -> a
    pick_lr LeftOrRight
    lr (Coercion, Coercion)
    pr_co)
      | Just (Coercion, Coercion)
    pr_co <- Coercion -> Maybe (Coercion, Coercion)
    splitAppCo_maybe Coercion
    co'
      = Bool -> Coercion -> Coercion
    forall a. HasCallStack => Bool -> a -> a
    assert (Role
    r Role -> Role -> Bool
    forall a. Eq a => a -> a -> Bool
    == Role
    Nominal) (Coercion -> Coercion) -> Coercion -> Coercion
    forall a b. (a -> b) -> a -> b
    $
        if Bool
    rep
        then LiftingContext -> SwapFlag -> Bool -> Role -> Coercion -> Coercion
    opt_co4 (LiftingContext -> LiftingContext
    zapLiftingContext LiftingContext
    env) SwapFlag
    NotSwapped Bool
    True Role
    Nominal (LeftOrRight -> (Coercion, Coercion) -> Coercion
    forall {a}. LeftOrRight -> (a, a) -> a
    pick_lr LeftOrRight
    lr (Coercion, Coercion)
    pr_co)
        else LeftOrRight -> (Coercion, Coercion) -> Coercion
    forall {a}. LeftOrRight -> (a, a) -> a
    pick_lr LeftOrRight
    lr (Coercion, Coercion)
    pr_co
      | Bool
    otherwise
      = Bool -> Role -> Coercion -> Coercion
    wrapRole Bool
    rep Role
    Nominal (Coercion -> Coercion) -> Coercion -> Coercion
    forall a b. (a -> b) -> a -> b
    $ LeftOrRight -> Coercion -> Coercion
    LRCo LeftOrRight
    lr Coercion
    co'
      where
        co' :: Coercion
    co' = LiftingContext -> SwapFlag -> Bool -> Role -> Coercion -> Coercion
    opt_co4 LiftingContext
    env SwapFlag
    sym Bool
    False Role
    Nominal Coercion
    co

        pick_lr :: LeftOrRight -> (a, a) -> a
    pick_lr LeftOrRight
    CLeft  (a
    l, a
    _) = a
    l
        pick_lr LeftOrRight
    CRight (a
    _, a
    r) = a
    r

    {-
    Note [Forall over coercion]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~
    Example:
      type (:~:) :: forall k. k -> k -> Type
      Refl :: forall k (a :: k) (b :: k). forall (cv :: (~#) k k a b). (:~:) k a b
      k1,k2,k3,k4 :: Type
      eta :: (k1 ~# k2) ~# (k3 ~# k4)    ==    ((~#) Type Type k1 k2) ~# ((~#) Type Type k3 k4)
      co1_3 :: k1 ~# k3
      co2_4 :: k2 ~# k4
      nth 2 eta :: k1 ~# k3
      nth 3 eta :: k2 ~# k4
      co11_31 :: <k1> ~# (sym co1_3)
      co22_24 :: <k2> ~# co2_4
      (forall (cv :: eta). Refl <Type> co1_3 co2_4 (co11_31 ;; cv ;; co22_24)) ::
        (forall (cv :: k1 ~# k2). Refl Type k1 k2 (<k1> ;; cv ;; <k2>) ~#
        (forall (cv :: k3 ~# k4). Refl Type k3 k4
           (sym co1_3 ;; nth 2 eta ;; cv ;; sym (nth 3 eta) ;; co2_4))
      co1_2 :: k1 ~# k2
      co3_4 :: k3 ~# k4
      co5 :: co1_2 ~# co3_4
      InstCo (forall (cv :: eta). Refl <Type> co1_3 co2_4 (co11_31 ;; cv ;; co22_24)) co5 ::
       (Refl Type k1 k2 (<k1> ;; cv ;; <k2>))[cv |-> co1_2] ~#
       (Refl Type k3 k4 (sym co1_3 ;; nth 2 eta ;; cv ;; sym (nth 3 eta) ;; co2_4))[cv |-> co3_4]
          ==
       (Refl Type k1 k2 (<k1> ;; co1_2 ;; <k2>)) ~#
        (Refl Type k3 k4 (sym co1_3 ;; nth 2 eta ;; co3_4 ;; sym (nth 3 eta) ;; co2_4))
          ==>
       Refl <Type> co1_3 co2_4 (co11_31 ;; co1_2 ;; co22_24)
    Conclusion: Because of the way this all works, we want to put in the *left-hand*
    coercion in co5's type. (In the code, co5 is called `arg`.)
    So we extend the environment binding cv to arg's left-hand type.
    -}

    -- See Note [Optimising InstCo]
    opt_co4' LiftingContext
    env SwapFlag
    sym Bool
    rep Role
    r (InstCo Coercion
    fun_co Coercion
    arg_co)
        -- forall over type...
      | Just (CoVar
    tv, ForAllTyFlag
    _visL, ForAllTyFlag
    _visR, Coercion
    k_co, Coercion
    body_co) <- Coercion
    -> Maybe (CoVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion)
    splitForAllCo_ty_maybe Coercion
    fun_co
        -- tv      :: k1
        -- k_co    :: k1 ~ k2
        -- body_co :: t1 ~ t2
        -- arg_co  :: (s1:k1) ~ (s2:k2)
      , let arg_co' :: Coercion
    arg_co'  = LiftingContext -> SwapFlag -> Bool -> Role -> Coercion -> Coercion
    opt_co4 LiftingContext
    env SwapFlag
    NotSwapped Bool
    False Role
    Nominal Coercion
    arg_co
                      -- Do /not/ push Sym into the arg_co, hence sym=False
                      -- see (LC2) of Note [The LiftingContext in optCoercion]
            k_co' :: Coercion
    k_co' = LiftingContext -> SwapFlag -> Bool -> Role -> Coercion -> Coercion
    opt_co4 LiftingContext
    env SwapFlag
    NotSwapped Bool
    False Role
    Nominal Coercion
    k_co
            s2' :: Type
    s2'   = HasDebugCallStack => Coercion -> Type
    Coercion -> Type
    coercionRKind Coercion
    arg_co'
            tv_co :: Coercion
    tv_co = HasDebugCallStack =>
    Role -> Type -> Coercion -> Coercion -> Coercion
    Role -> Type -> Coercion -> Coercion -> Coercion
    mk_coherence_right_co Role
    Nominal Type
    s2' (Coercion -> Coercion
    mkSymCo Coercion
    k_co') Coercion
    arg_co'
                       -- mkSymCo kind_co :: k2 ~ k1
                       -- tv_co   :: (s1 :: k1) ~ (((s2 :: k2) |> (sym kind_co)) :: k1)
      = LiftingContext -> SwapFlag -> Bool -> Role -> Coercion -> Coercion
    opt_co4 (LiftingContext -> CoVar -> Coercion -> LiftingContext
    extendLiftingContext LiftingContext
    env CoVar
    tv Coercion
    tv_co) SwapFlag
    sym Bool
    rep Role
    r Coercion
    body_co

        -- See Note [Forall over coercion]
      | Just (CoVar
    cv, ForAllTyFlag
    _visL, ForAllTyFlag
    _visR, Coercion
    _kind_co, Coercion
    body_co) <- Coercion
    -> Maybe (CoVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion)
    splitForAllCo_co_maybe Coercion
    fun_co
      , CoercionTy Coercion
    h1 <- HasDebugCallStack => Coercion -> Type
    Coercion -> Type
    coercionLKind Coercion
    arg_co
      , let h1' :: Coercion
    h1' = LiftingContext -> SwapFlag -> Bool -> Role -> Coercion -> Coercion
    opt_co4 LiftingContext
    env SwapFlag
    NotSwapped Bool
    False Role
    Nominal Coercion
    h1
      = LiftingContext -> SwapFlag -> Bool -> Role -> Coercion -> Coercion
    opt_co4 (LiftingContext -> CoVar -> Coercion -> LiftingContext
    extendLiftingContextCvSubst LiftingContext
    env CoVar
    cv Coercion
    h1') SwapFlag
    sym Bool
    rep Role
    r Coercion
    body_co

      -- OK so those cases didn't work.  See if it is a forall /after/ optimization
      -- If so, do an inefficient one-variable substitution, then re-optimize

        -- forall over type...
      | Just (CoVar
    tv', ForAllTyFlag
    _visL, ForAllTyFlag
    _visR, Coercion
    k_co', Coercion
    body_co') <- Coercion
    -> Maybe (CoVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion)
    splitForAllCo_ty_maybe Coercion
    fun_co'
      , let s2' :: Type
    s2'   = HasDebugCallStack => Coercion -> Type
    Coercion -> Type
    coercionRKind Coercion
    arg_co'
            tv_co :: Coercion
    tv_co = HasDebugCallStack =>
    Role -> Type -> Coercion -> Coercion -> Coercion
    Role -> Type -> Coercion -> Coercion -> Coercion
    mk_coherence_right_co Role
    Nominal Type
    s2' (Coercion -> Coercion
    mkSymCo Coercion
    k_co') Coercion
    arg_co'
            env' :: LiftingContext
    env'  = LiftingContext -> CoVar -> Coercion -> LiftingContext
    extendLiftingContext (LiftingContext -> LiftingContext
    zapLiftingContext LiftingContext
    env) CoVar
    tv' Coercion
    tv_co
      = LiftingContext -> SwapFlag -> Bool -> Role -> Coercion -> Coercion
    opt_co4 LiftingContext
    env' SwapFlag
    NotSwapped Bool
    False Role
    r' Coercion
    body_co'

        -- See Note [Forall over coercion]
      | Just (CoVar
    cv', ForAllTyFlag
    _visL, ForAllTyFlag
    _visR, Coercion
    _kind_co', Coercion
    body_co') <- Coercion
    -> Maybe (CoVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion)
    splitForAllCo_co_maybe Coercion
    fun_co'
      , CoercionTy Coercion
    h1' <- HasDebugCallStack => Coercion -> Type
    Coercion -> Type
    coercionLKind Coercion
    arg_co'
      , let env' :: LiftingContext
    env' = LiftingContext -> CoVar -> Coercion -> LiftingContext
    extendLiftingContextCvSubst (LiftingContext -> LiftingContext
    zapLiftingContext LiftingContext
    env) CoVar
    cv' Coercion
    h1'
      = LiftingContext -> SwapFlag -> Bool -> Role -> Coercion -> Coercion
    opt_co4 LiftingContext
    env' SwapFlag
    NotSwapped Bool
    False Role
    r' Coercion
    body_co'

      -- Those cases didn't work either, so rebuild the InstCo
      -- Push Sym into /both/ function /and/ arg_coument
      | Bool
    otherwise = Coercion -> Coercion -> Coercion
    InstCo Coercion
    fun_co' Coercion
    arg_co'

      where
        -- fun_co' arg_co' are both optimised, /and/ we have pushed `sym` into both
        -- So no more sym'ing on th results of fun_co' arg_co'
        fun_co' :: Coercion
    fun_co' = LiftingContext -> SwapFlag -> Bool -> Role -> Coercion -> Coercion
    opt_co4 LiftingContext
    env SwapFlag
    sym Bool
    rep Role
    r Coercion
    fun_co
        arg_co' :: Coercion
    arg_co' = LiftingContext -> SwapFlag -> Bool -> Role -> Coercion -> Coercion
    opt_co4 LiftingContext
    env SwapFlag
    sym Bool
    False Role
    Nominal Coercion
    arg_co
        r' :: Role
    r'   = Bool -> Role -> Role
    chooseRole Bool
    rep Role
    r

    opt_co4' LiftingContext
    env SwapFlag
    sym Bool
    _rep Role
    r (KindCo Coercion
    co)
      = Bool -> Coercion -> Coercion
    forall a. HasCallStack => Bool -> a -> a
    assert (Role
    r Role -> Role -> Bool
    forall a. Eq a => a -> a -> Bool
    == Role
    Nominal) (Coercion -> Coercion) -> Coercion -> Coercion
    forall a b. (a -> b) -> a -> b
    $
        let kco' :: Coercion
    kco' = HasDebugCallStack => Coercion -> Coercion
    Coercion -> Coercion
    promoteCoercion Coercion
    co in
        case Coercion
    kco' of
          KindCo Coercion
    co' -> HasDebugCallStack => Coercion -> Coercion
    Coercion -> Coercion
    promoteCoercion (LiftingContext -> SwapFlag -> Coercion -> Coercion
    opt_co1 LiftingContext
    env SwapFlag
    sym Coercion
    co')
          Coercion
    _          -> LiftingContext -> SwapFlag -> Bool -> Role -> Coercion -> Coercion
    opt_co4 LiftingContext
    env SwapFlag
    sym Bool
    False Role
    Nominal Coercion
    kco'
      -- This might be able to be optimized more to do the promotion
      -- and substitution/optimization at the same time

    opt_co4' LiftingContext
    env SwapFlag
    sym Bool
    _ Role
    r (SubCo Coercion
    co)
      = Bool -> Coercion -> Coercion
    forall a. HasCallStack => Bool -> a -> a
    assert (Role
    r Role -> Role -> Bool
    forall a. Eq a => a -> a -> Bool
    == Role
    Representational) (Coercion -> Coercion) -> Coercion -> Coercion
    forall a b. (a -> b) -> a -> b
    $
        LiftingContext -> SwapFlag -> Bool -> Role -> Coercion -> Coercion
    opt_co4 LiftingContext
    env SwapFlag
    sym Bool
    True Role
    Nominal Coercion
    co

    {- Note [Optimise CoVarCo to Refl]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    If we have (c :: t~t) we can optimise it to Refl. That increases the
    chances of floating the Refl upwards; e.g. Maybe c --> Refl (Maybe t)

    We do so here in optCoercion, not in mkCoVarCo; see Note [mkCoVarCo]
    in GHC.Core.Coercion.
    -}

    -------------
    -- | Optimize a phantom coercion. The input coercion may not necessarily
    -- be a phantom, but the output sure will be.
    opt_phantom :: LiftingContext -> SwapFlag -> Coercion -> NormalCo
    opt_phantom :: LiftingContext -> SwapFlag -> Coercion -> Coercion
    opt_phantom LiftingContext
    env SwapFlag
    sym (UnivCo { uco_prov :: Coercion -> UnivCoProvenance
    uco_prov = UnivCoProvenance
    prov, uco_lty :: Coercion -> Type
    uco_lty = Type
    t1
                                , uco_rty :: Coercion -> Type
    uco_rty = Type
    t2, uco_deps :: Coercion -> [Coercion]
    uco_deps = [Coercion]
    deps })
      = LiftingContext
    -> SwapFlag
    -> UnivCoProvenance
    -> [Coercion]
    -> Role
    -> Type
    -> Type
    -> Coercion
    opt_univ LiftingContext
    env SwapFlag
    sym UnivCoProvenance
    prov [Coercion]
    deps Role
    Phantom Type
    t1 Type
    t2

    opt_phantom LiftingContext
    env SwapFlag
    sym Coercion
    co
      = LiftingContext
    -> SwapFlag
    -> UnivCoProvenance
    -> [Coercion]
    -> Role
    -> Type
    -> Type
    -> Coercion
    opt_univ LiftingContext
    env SwapFlag
    sym UnivCoProvenance
    PhantomProv [Coercion -> Coercion
    mkKindCo Coercion
    co] Role
    Phantom Type
    ty1 Type
    ty2
      where
        Pair Type
    ty1 Type
    ty2 = HasDebugCallStack => Coercion -> Pair Type
    Coercion -> Pair Type
    coercionKind Coercion
    co

    {- Note [Differing kinds]
       ~~~~~~~~~~~~~~~~~~~~~~
    The two types may not have the same kind (although that would be very unusual).
    But even if they have the same kind, and the same type constructor, the number
    of arguments in a `CoTyConApp` can differ. Consider

      Any :: forall k. k

      Any @Type Int                :: Type
      Any @(Type->Type) Maybe Int  :: Type

    Hence the need to compare argument lengths; see #13658

    Note [opt_univ needs injectivity]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    If opt_univ sees a coercion between `T a1 a2` and `T b1 b2` it will optimize it
    by producing a TyConAppCo for T, and pushing the UnivCo into the arguments.  But
    this works only if T is injective. Otherwise we can have something like

      type family F x where
        F Int  = Int
        F Bool = Int

    where `UnivCo :: F Int ~ F Bool` is reasonable (it is effectively just an
    alternative representation for a couple of uses of AxiomInstCos) but we do not
    want to produce `F (UnivCo :: Int ~ Bool)` where the inner coercion is clearly
    inconsistent.  Hence the opt_univ case for TyConApps checks isInjectiveTyCon.
    See #19509.

     -}

    opt_univ :: LiftingContext -> SwapFlag -> UnivCoProvenance
             -> [Coercion]
             -> Role -> Type -> Type -> Coercion
    opt_univ :: LiftingContext
    -> SwapFlag
    -> UnivCoProvenance
    -> [Coercion]
    -> Role
    -> Type
    -> Type
    -> Coercion
    opt_univ LiftingContext
    env SwapFlag
    sym UnivCoProvenance
    prov [Coercion]
    deps Role
    role Type
    ty1 Type
    ty2
      = let ty1' :: Type
    ty1'  = Subst -> Type -> Type
    substTyUnchecked (LiftingContext -> Subst
    lcSubstLeft  LiftingContext
    env) Type
    ty1
            ty2' :: Type
    ty2'  = Subst -> Type -> Type
    substTyUnchecked (LiftingContext -> Subst
    lcSubstRight LiftingContext
    env) Type
    ty2
            deps' :: [Coercion]
    deps' = (Coercion -> Coercion) -> [Coercion] -> [Coercion]
    forall a b. (a -> b) -> [a] -> [b]
    map (LiftingContext -> SwapFlag -> Coercion -> Coercion
    opt_co1 LiftingContext
    env SwapFlag
    sym) [Coercion]
    deps
            (Type
    ty1'', Type
    ty2'') = SwapFlag -> (Type, Type) -> (Type, Type)
    forall a. SwapFlag -> (a, a) -> (a, a)
    swapSym SwapFlag
    sym (Type
    ty1', Type
    ty2')
        in
        UnivCoProvenance -> [Coercion] -> Role -> Type -> Type -> Coercion
    mkUnivCo UnivCoProvenance
    prov [Coercion]
    deps' Role
    role Type
    ty1'' Type
    ty2''

    {-
    opt_univ env PhantomProv cvs _r ty1 ty2
      = mkUnivCo PhantomProv cvs Phantom ty1' ty2'
      where
        ty1' = substTy (lcSubstLeft  env) ty1
        ty2' = substTy (lcSubstRight env) ty2

    opt_univ1 env prov cvs' role oty1 oty2
      | Just (tc1, tys1) <- splitTyConApp_maybe oty1
      , Just (tc2, tys2) <- splitTyConApp_maybe oty2
      , tc1 == tc2
      , isInjectiveTyCon tc1 role  -- see Note [opt_univ needs injectivity]
      , equalLength tys1 tys2 -- see Note [Differing kinds]
          -- NB: prov must not be the two interesting ones (ProofIrrel & Phantom);
          -- Phantom is already taken care of, and ProofIrrel doesn't relate tyconapps
      = let roles    = tyConRoleListX role tc1
            arg_cos  = zipWith3 (mkUnivCo prov cvs') roles tys1 tys2
            arg_cos' = zipWith (opt_co4 env False False) roles arg_cos
        in
        mkTyConAppCo role tc1 arg_cos'

      -- can't optimize the AppTy case because we can't build the kind coercions.

      | Just (Bndr tv1 vis1, ty1) <- splitForAllForAllTyBinder_maybe oty1
      , isTyVar tv1
      , Just (Bndr tv2 vis2, ty2) <- splitForAllForAllTyBinder_maybe oty2
      , isTyVar tv2
          -- NB: prov isn't interesting here either
      = let k1   = tyVarKind tv1
            k2   = tyVarKind tv2
            eta  = mkUnivCo prov cvs' Nominal k1 k2
              -- eta gets opt'ed soon, but not yet.
            ty2' = substTyWith [tv2] [TyVarTy tv1 `mkCastTy` eta] ty2

            (env', tv1', eta') = optForAllCoBndr env False tv1 eta
        in
        mkForAllCo tv1' vis1 vis2 eta' (opt_univ1 env' prov cvs' role ty1 ty2')

      | Just (Bndr cv1 vis1, ty1) <- splitForAllForAllTyBinder_maybe oty1
      , isCoVar cv1
      , Just (Bndr cv2 vis2, ty2) <- splitForAllForAllTyBinder_maybe oty2
      , isCoVar cv2
          -- NB: prov isn't interesting here either
      = let k1    = varType cv1
            k2    = varType cv2
            r'    = coVarRole cv1
            eta   = mkUnivCo prov cvs' Nominal k1 k2
            eta_d = downgradeRole r' Nominal eta
              -- eta gets opt'ed soon, but not yet.
            n_co  = (mkSymCo $ mkSelCo (SelTyCon 2 r') eta_d) `mkTransCo`
                    (mkCoVarCo cv1) `mkTransCo`
                    (mkSelCo (SelTyCon 3 r') eta_d)
            ty2'  = substTyWithCoVars [cv2] [n_co] ty2

            (env', cv1', eta') = optForAllCoBndr env False cv1 eta
        in
        mkForAllCo cv1' vis1 vis2 eta' (opt_univ1 env' prov cvs' role ty1 ty2')

      | otherwise
      = let ty1 = substTyUnchecked (lcSubstLeft  env) oty1
            ty2 = substTyUnchecked (lcSubstRight env) oty2
        in
        mkUnivCo prov cvs' role ty1 ty2
    -}

    -------------
    opt_transList :: HasDebugCallStack => InScopeSet -> [NormalCo] -> [NormalCo] -> [NormalCo]
    opt_transList :: HasDebugCallStack =>
    InScopeSet -> [Coercion] -> [Coercion] -> [Coercion]
    opt_transList InScopeSet
    is = String
    -> (Coercion -> Coercion -> Coercion)
    -> [Coercion]
    -> [Coercion]
    -> [Coercion]
    forall a b c.
    HasDebugCallStack =>
    String -> (a -> b -> c) -> [a] -> [b] -> [c]
    zipWithEqual String
    "opt_transList" (HasDebugCallStack => InScopeSet -> Coercion -> Coercion -> Coercion
    InScopeSet -> Coercion -> Coercion -> Coercion
    opt_trans InScopeSet
    is)
      -- The input lists must have identical length.

    opt_trans :: HasDebugCallStack => InScopeSet -> NormalCo -> NormalCo -> NormalCo

    -- opt_trans just allows us to add some debug tracing
    -- Usually it just goes to opt_trans'
    opt_trans :: HasDebugCallStack => InScopeSet -> Coercion -> Coercion -> Coercion
    opt_trans InScopeSet
    is Coercion
    co1 Coercion
    co2
      = -- (if coercionRKind co1 `eqType` coercionLKind co2
        --  then (\x -> x) else
        --  pprTrace "opt_trans" (vcat [ text "co1" <+> ppr co1
        --                             , text "co2" <+> ppr co2
        --                             , text "co1 kind" <+> ppr (coercionKind co1)
        --                             , text "co2 kind" <+> ppr (coercionKind co2)
        --                             , callStackDoc ])) $
        HasDebugCallStack => InScopeSet -> Coercion -> Coercion -> Coercion
    InScopeSet -> Coercion -> Coercion -> Coercion
    opt_trans' InScopeSet
    is Coercion
    co1 Coercion
    co2

    {-
    opt_trans is co1 co2
      = assertPpr (r1==r2) (vcat [ ppr r1 <+> ppr co1, ppr r2 <+> ppr co2]) $
        assertPpr (rres == r1) (vcat [ ppr r1 <+> ppr co1, ppr r2 <+> ppr co2, text "res" <+> ppr rres <+> ppr res ]) $
        res
      where
        res = opt_trans' is co1 co2
        rres = coercionRole res
        r1 = coercionRole co1
        r2 = coercionRole co1
    -}

    opt_trans' :: HasDebugCallStack => InScopeSet -> NormalCo -> NormalCo -> NormalCo
    opt_trans' :: HasDebugCallStack => InScopeSet -> Coercion -> Coercion -> Coercion
    opt_trans' InScopeSet
    is Coercion
    co1 Coercion
    co2
      | Coercion -> Bool
    isReflCo Coercion
    co1 = Coercion
    co2
        -- optimize when co1 is a Refl Co
      | Bool
    otherwise    = HasDebugCallStack => InScopeSet -> Coercion -> Coercion -> Coercion
    InScopeSet -> Coercion -> Coercion -> Coercion
    opt_trans1 InScopeSet
    is Coercion
    co1 Coercion
    co2

    opt_trans1 :: HasDebugCallStack => InScopeSet -> NormalNonIdCo -> NormalCo -> NormalCo
    -- First arg is not the identity
    opt_trans1 :: HasDebugCallStack => InScopeSet -> Coercion -> Coercion -> Coercion
    opt_trans1 InScopeSet
    is Coercion
    co1 Coercion
    co2
      | Coercion -> Bool
    isReflCo Coercion
    co2 = Coercion
    co1
        -- optimize when co2 is a Refl Co
      | Bool
    otherwise    = HasDebugCallStack => InScopeSet -> Coercion -> Coercion -> Coercion
    InScopeSet -> Coercion -> Coercion -> Coercion
    opt_trans2 InScopeSet
    is Coercion
    co1 Coercion
    co2

    opt_trans2 :: HasDebugCallStack => InScopeSet -> NormalNonIdCo -> NormalNonIdCo -> NormalCo
    -- Neither arg is the identity
    opt_trans2 :: HasDebugCallStack => InScopeSet -> Coercion -> Coercion -> Coercion
    opt_trans2 InScopeSet
    is (TransCo Coercion
    co1a Coercion
    co1b) Coercion
    co2
        -- Don't know whether the sub-coercions are the identity
      = HasDebugCallStack => InScopeSet -> Coercion -> Coercion -> Coercion
    InScopeSet -> Coercion -> Coercion -> Coercion
    opt_trans InScopeSet
    is Coercion
    co1a (HasDebugCallStack => InScopeSet -> Coercion -> Coercion -> Coercion
    InScopeSet -> Coercion -> Coercion -> Coercion
    opt_trans InScopeSet
    is Coercion
    co1b Coercion
    co2)

    opt_trans2 InScopeSet
    is Coercion
    co1 Coercion
    co2
      | Just Coercion
    co <- HasDebugCallStack =>
    InScopeSet -> Coercion -> Coercion -> Maybe Coercion
    InScopeSet -> Coercion -> Coercion -> Maybe Coercion
    opt_trans_rule InScopeSet
    is Coercion
    co1 Coercion
    co2
      = Coercion
    co

    opt_trans2 InScopeSet
    is Coercion
    co1 (TransCo Coercion
    co2a Coercion
    co2b)
      | Just Coercion
    co1_2a <- HasDebugCallStack =>
    InScopeSet -> Coercion -> Coercion -> Maybe Coercion
    InScopeSet -> Coercion -> Coercion -> Maybe Coercion
    opt_trans_rule InScopeSet
    is Coercion
    co1 Coercion
    co2a
      = if Coercion -> Bool
    isReflCo Coercion
    co1_2a
        then Coercion
    co2b
        else HasDebugCallStack => InScopeSet -> Coercion -> Coercion -> Coercion
    InScopeSet -> Coercion -> Coercion -> Coercion
    opt_trans1 InScopeSet
    is Coercion
    co1_2a Coercion
    co2b

    opt_trans2 InScopeSet
    _ Coercion
    co1 Coercion
    co2
      = HasDebugCallStack => Coercion -> Coercion -> Coercion
    Coercion -> Coercion -> Coercion
    mk_trans_co Coercion
    co1 Coercion
    co2

    ------
    -- Optimize coercions with a top-level use of transitivity.
    opt_trans_rule :: HasDebugCallStack => InScopeSet -> NormalNonIdCo -> NormalNonIdCo -> Maybe NormalCo

    opt_trans_rule :: HasDebugCallStack =>
    InScopeSet -> Coercion -> Coercion -> Maybe Coercion
    opt_trans_rule InScopeSet
    _ Coercion
    in_co1 Coercion
    in_co2
      | Bool -> SDoc -> Bool -> Bool
    forall a. HasCallStack => Bool -> SDoc -> a -> a
    assertPpr (HasDebugCallStack => Coercion -> Type
    Coercion -> Type
    coercionRKind Coercion
    in_co1 HasCallStack => Type -> Type -> Bool
    Type -> Type -> Bool
    `eqType` HasDebugCallStack => Coercion -> Type
    Coercion -> Type
    coercionLKind Coercion
    in_co2)
                  ([SDoc] -> SDoc
    forall doc. IsDoc doc => [doc] -> doc
    vcat [ String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "in_co1" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> Coercion -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Coercion
    in_co1
                       , String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "in_co2" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> Coercion -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Coercion
    in_co2
                       , String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "in_co1 kind" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> Pair Type -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr (HasDebugCallStack => Coercion -> Pair Type
    Coercion -> Pair Type
    coercionKind Coercion
    in_co1)
                       , String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "in_co2 kind" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> Pair Type -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr (HasDebugCallStack => Coercion -> Pair Type
    Coercion -> Pair Type
    coercionKind Coercion
    in_co2)
                       , SDoc
    HasCallStack => SDoc
    callStackDoc ]) (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $
        Bool
    False
      = String -> Maybe Coercion
    forall a. HasCallStack => String -> a
    panic String
    "opt_trans_rule"  -- This entire equation is purely assertion checking

    opt_trans_rule InScopeSet
    is in_co1 :: Coercion
    in_co1@(GRefl Role
    r1 Type
    t1 (MCo Coercion
    co1)) in_co2 :: Coercion
    in_co2@(GRefl Role
    r2 Type
    _t2 (MCo Coercion
    co2))
      = Bool -> Maybe Coercion -> Maybe Coercion
    forall a. HasCallStack => Bool -> a -> a
    assert (Role
    r1 Role -> Role -> Bool
    forall a. Eq a => a -> a -> Bool
    == Role
    r2) (Maybe Coercion -> Maybe Coercion)
    -> Maybe Coercion -> Maybe Coercion
    forall a b. (a -> b) -> a -> b
    $
        String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
    fireTransRule String
    "GRefl" Coercion
    in_co1 Coercion
    in_co2 (Coercion -> Maybe Coercion) -> Coercion -> Maybe Coercion
    forall a b. (a -> b) -> a -> b
    $
        Role -> Type -> Coercion -> Coercion
    mk_grefl_right_co Role
    r1 Type
    t1 (HasDebugCallStack => InScopeSet -> Coercion -> Coercion -> Coercion
    InScopeSet -> Coercion -> Coercion -> Coercion
    opt_trans InScopeSet
    is Coercion
    co1 Coercion
    co2)

    -- Push transitivity through matching destructors
    opt_trans_rule InScopeSet
    is in_co1 :: Coercion
    in_co1@(SelCo CoSel
    d1 Coercion
    co1) in_co2 :: Coercion
    in_co2@(SelCo CoSel
    d2 Coercion
    co2)
      | CoSel
    d1 CoSel -> CoSel -> Bool
    forall a. Eq a => a -> a -> Bool
    == CoSel
    d2
      , Coercion -> Role
    coercionRole Coercion
    co1 Role -> Role -> Bool
    forall a. Eq a => a -> a -> Bool
    == Coercion -> Role
    coercionRole Coercion
    co2
      , Coercion
    co1 Coercion -> Coercion -> Bool
    `compatible_co` Coercion
    co2
      = String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
    fireTransRule String
    "PushNth" Coercion
    in_co1 Coercion
    in_co2 (Coercion -> Maybe Coercion) -> Coercion -> Maybe Coercion
    forall a b. (a -> b) -> a -> b
    $
        HasDebugCallStack => CoSel -> Coercion -> Coercion
    CoSel -> Coercion -> Coercion
    mkSelCo CoSel
    d1 (HasDebugCallStack => InScopeSet -> Coercion -> Coercion -> Coercion
    InScopeSet -> Coercion -> Coercion -> Coercion
    opt_trans InScopeSet
    is Coercion
    co1 Coercion
    co2)

    opt_trans_rule InScopeSet
    is in_co1 :: Coercion
    in_co1@(LRCo LeftOrRight
    d1 Coercion
    co1) in_co2 :: Coercion
    in_co2@(LRCo LeftOrRight
    d2 Coercion
    co2)
      | LeftOrRight
    d1 LeftOrRight -> LeftOrRight -> Bool
    forall a. Eq a => a -> a -> Bool
    == LeftOrRight
    d2
      , Coercion
    co1 Coercion -> Coercion -> Bool
    `compatible_co` Coercion
    co2
      = String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
    fireTransRule String
    "PushLR" Coercion
    in_co1 Coercion
    in_co2 (Coercion -> Maybe Coercion) -> Coercion -> Maybe Coercion
    forall a b. (a -> b) -> a -> b
    $
        LeftOrRight -> Coercion -> Coercion
    mkLRCo LeftOrRight
    d1 (HasDebugCallStack => InScopeSet -> Coercion -> Coercion -> Coercion
    InScopeSet -> Coercion -> Coercion -> Coercion
    opt_trans InScopeSet
    is Coercion
    co1 Coercion
    co2)

    -- Push transitivity inside instantiation
    opt_trans_rule InScopeSet
    is in_co1 :: Coercion
    in_co1@(InstCo Coercion
    co1 Coercion
    ty1) in_co2 :: Coercion
    in_co2@(InstCo Coercion
    co2 Coercion
    ty2)
      | Coercion
    ty1 Coercion -> Coercion -> Bool
    `eqCoercion` Coercion
    ty2
      , Coercion
    co1 Coercion -> Coercion -> Bool
    `compatible_co` Coercion
    co2
      = String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
    fireTransRule String
    "TrPushInst" Coercion
    in_co1 Coercion
    in_co2 (Coercion -> Maybe Coercion) -> Coercion -> Maybe Coercion
    forall a b. (a -> b) -> a -> b
    $
        Coercion -> Coercion -> Coercion
    mkInstCo (HasDebugCallStack => InScopeSet -> Coercion -> Coercion -> Coercion
    InScopeSet -> Coercion -> Coercion -> Coercion
    opt_trans InScopeSet
    is Coercion
    co1 Coercion
    co2) Coercion
    ty1

    opt_trans_rule InScopeSet
    _
        in_co1 :: Coercion
    in_co1@(UnivCo { uco_prov :: Coercion -> UnivCoProvenance
    uco_prov = UnivCoProvenance
    p1, uco_role :: Coercion -> Role
    uco_role = Role
    r1, uco_lty :: Coercion -> Type
    uco_lty = Type
    tyl1, uco_deps :: Coercion -> [Coercion]
    uco_deps = [Coercion]
    deps1 })
        in_co2 :: Coercion
    in_co2@(UnivCo { uco_prov :: Coercion -> UnivCoProvenance
    uco_prov = UnivCoProvenance
    p2, uco_role :: Coercion -> Role
    uco_role = Role
    r2, uco_rty :: Coercion -> Type
    uco_rty = Type
    tyr2, uco_deps :: Coercion -> [Coercion]
    uco_deps = [Coercion]
    deps2 })
      | UnivCoProvenance
    p1 UnivCoProvenance -> UnivCoProvenance -> Bool
    forall a. Eq a => a -> a -> Bool
    == UnivCoProvenance
    p2    -- If the provenances are different, opt'ing will be very confusing
      = Bool -> Maybe Coercion -> Maybe Coercion
    forall a. HasCallStack => Bool -> a -> a
    assert (Role
    r1 Role -> Role -> Bool
    forall a. Eq a => a -> a -> Bool
    == Role
    r2) (Maybe Coercion -> Maybe Coercion)
    -> Maybe Coercion -> Maybe Coercion
    forall a b. (a -> b) -> a -> b
    $
        String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
    fireTransRule String
    "UnivCo" Coercion
    in_co1 Coercion
    in_co2 (Coercion -> Maybe Coercion) -> Coercion -> Maybe Coercion
    forall a b. (a -> b) -> a -> b
    $
        UnivCoProvenance -> [Coercion] -> Role -> Type -> Type -> Coercion
    mkUnivCo UnivCoProvenance
    p1 ([Coercion]
    deps1 [Coercion] -> [Coercion] -> [Coercion]
    forall a. [a] -> [a] -> [a]
    ++ [Coercion]
    deps2) Role
    r1 Type
    tyl1 Type
    tyr2

    -- Push transitivity down through matching top-level constructors.
    opt_trans_rule InScopeSet
    is in_co1 :: Coercion
    in_co1@(TyConAppCo Role
    r1 TyCon
    tc1 [Coercion]
    cos1) in_co2 :: Coercion
    in_co2@(TyConAppCo Role
    r2 TyCon
    tc2 [Coercion]
    cos2)
      | TyCon
    tc1 TyCon -> TyCon -> Bool
    forall a. Eq a => a -> a -> Bool
    == TyCon
    tc2
      = Bool -> Maybe Coercion -> Maybe Coercion
    forall a. HasCallStack => Bool -> a -> a
    assert (Role
    r1 Role -> Role -> Bool
    forall a. Eq a => a -> a -> Bool
    == Role
    r2) (Maybe Coercion -> Maybe Coercion)
    -> Maybe Coercion -> Maybe Coercion
    forall a b. (a -> b) -> a -> b
    $
        String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
    fireTransRule String
    "PushTyConApp" Coercion
    in_co1 Coercion
    in_co2 (Coercion -> Maybe Coercion) -> Coercion -> Maybe Coercion
    forall a b. (a -> b) -> a -> b
    $
        HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
    Role -> TyCon -> [Coercion] -> Coercion
    mkTyConAppCo Role
    r1 TyCon
    tc1 (HasDebugCallStack =>
    InScopeSet -> [Coercion] -> [Coercion] -> [Coercion]
    InScopeSet -> [Coercion] -> [Coercion] -> [Coercion]
    opt_transList InScopeSet
    is [Coercion]
    cos1 [Coercion]
    cos2)

    opt_trans_rule InScopeSet
    is in_co1 :: Coercion
    in_co1@(FunCo Role
    r1 FunTyFlag
    afl1 FunTyFlag
    afr1 Coercion
    w1 Coercion
    co1a Coercion
    co1b)
                      in_co2 :: Coercion
    in_co2@(FunCo Role
    r2 FunTyFlag
    afl2 FunTyFlag
    afr2 Coercion
    w2 Coercion
    co2a Coercion
    co2b)
      = Bool -> Maybe Coercion -> Maybe Coercion
    forall a. HasCallStack => Bool -> a -> a
    assert (Role
    r1 Role -> Role -> Bool
    forall a. Eq a => a -> a -> Bool
    == Role
    r2)     (Maybe Coercion -> Maybe Coercion)
    -> Maybe Coercion -> Maybe Coercion
    forall a b. (a -> b) -> a -> b
    $     -- Just like the TyConAppCo/TyConAppCo case
        Bool -> Maybe Coercion -> Maybe Coercion
    forall a. HasCallStack => Bool -> a -> a
    assert (FunTyFlag
    afr1 FunTyFlag -> FunTyFlag -> Bool
    forall a. Eq a => a -> a -> Bool
    == FunTyFlag
    afl2) (Maybe Coercion -> Maybe Coercion)
    -> Maybe Coercion -> Maybe Coercion
    forall a b. (a -> b) -> a -> b
    $
        String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
    fireTransRule String
    "PushFun" Coercion
    in_co1 Coercion
    in_co2 (Coercion -> Maybe Coercion) -> Coercion -> Maybe Coercion
    forall a b. (a -> b) -> a -> b
    $
        Role
    -> FunTyFlag
    -> FunTyFlag
    -> Coercion
    -> Coercion
    -> Coercion
    -> Coercion
    mkFunCo2 Role
    r1 FunTyFlag
    afl1 FunTyFlag
    afr2 (HasDebugCallStack => InScopeSet -> Coercion -> Coercion -> Coercion
    InScopeSet -> Coercion -> Coercion -> Coercion
    opt_trans InScopeSet
    is Coercion
    w1 Coercion
    w2)
                              (HasDebugCallStack => InScopeSet -> Coercion -> Coercion -> Coercion
    InScopeSet -> Coercion -> Coercion -> Coercion
    opt_trans InScopeSet
    is Coercion
    co1a Coercion
    co2a)
                              (HasDebugCallStack => InScopeSet -> Coercion -> Coercion -> Coercion
    InScopeSet -> Coercion -> Coercion -> Coercion
    opt_trans InScopeSet
    is Coercion
    co1b Coercion
    co2b)

    opt_trans_rule InScopeSet
    is in_co1 :: Coercion
    in_co1@(AppCo Coercion
    co1a Coercion
    co1b) in_co2 :: Coercion
    in_co2@(AppCo Coercion
    co2a Coercion
    co2b)
      -- Must call opt_trans_rule_app; see Note [EtaAppCo]
      = InScopeSet
    -> Coercion
    -> Coercion
    -> Coercion
    -> [Coercion]
    -> Coercion
    -> [Coercion]
    -> Maybe Coercion
    opt_trans_rule_app InScopeSet
    is Coercion
    in_co1 Coercion
    in_co2 Coercion
    co1a [Coercion
    co1b] Coercion
    co2a [Coercion
    co2b]

    -- Eta rules
    opt_trans_rule InScopeSet
    is co1 :: Coercion
    co1@(TyConAppCo Role
    r TyCon
    tc [Coercion]
    cos1) Coercion
    co2
      | Just [Coercion]
    cos2 <- TyCon -> Coercion -> Maybe [Coercion]
    etaTyConAppCo_maybe TyCon
    tc Coercion
    co2
      = String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
    fireTransRule String
    "EtaCompL" Coercion
    co1 Coercion
    co2 (Coercion -> Maybe Coercion) -> Coercion -> Maybe Coercion
    forall a b. (a -> b) -> a -> b
    $
        HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
    Role -> TyCon -> [Coercion] -> Coercion
    mkTyConAppCo Role
    r TyCon
    tc (HasDebugCallStack =>
    InScopeSet -> [Coercion] -> [Coercion] -> [Coercion]
    InScopeSet -> [Coercion] -> [Coercion] -> [Coercion]
    opt_transList InScopeSet
    is [Coercion]
    cos1 [Coercion]
    cos2)

    opt_trans_rule InScopeSet
    is Coercion
    co1 co2 :: Coercion
    co2@(TyConAppCo Role
    r TyCon
    tc [Coercion]
    cos2)
      | Just [Coercion]
    cos1 <- TyCon -> Coercion -> Maybe [Coercion]
    etaTyConAppCo_maybe TyCon
    tc Coercion
    co1
      = String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
    fireTransRule String
    "EtaCompR" Coercion
    co1 Coercion
    co2 (Coercion -> Maybe Coercion) -> Coercion -> Maybe Coercion
    forall a b. (a -> b) -> a -> b
    $
        HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
    Role -> TyCon -> [Coercion] -> Coercion
    mkTyConAppCo Role
    r TyCon
    tc (HasDebugCallStack =>
    InScopeSet -> [Coercion] -> [Coercion] -> [Coercion]
    InScopeSet -> [Coercion] -> [Coercion] -> [Coercion]
    opt_transList InScopeSet
    is [Coercion]
    cos1 [Coercion]
    cos2)

    opt_trans_rule InScopeSet
    is co1 :: Coercion
    co1@(AppCo Coercion
    co1a Coercion
    co1b) Coercion
    co2
      | Just (Coercion
    co2a,Coercion
    co2b) <- Coercion -> Maybe (Coercion, Coercion)
    etaAppCo_maybe Coercion
    co2
      = InScopeSet
    -> Coercion
    -> Coercion
    -> Coercion
    -> [Coercion]
    -> Coercion
    -> [Coercion]
    -> Maybe Coercion
    opt_trans_rule_app InScopeSet
    is Coercion
    co1 Coercion
    co2 Coercion
    co1a [Coercion
    co1b] Coercion
    co2a [Coercion
    co2b]

    opt_trans_rule InScopeSet
    is Coercion
    co1 co2 :: Coercion
    co2@(AppCo Coercion
    co2a Coercion
    co2b)
      | Just (Coercion
    co1a,Coercion
    co1b) <- Coercion -> Maybe (Coercion, Coercion)
    etaAppCo_maybe Coercion
    co1
      = InScopeSet
    -> Coercion
    -> Coercion
    -> Coercion
    -> [Coercion]
    -> Coercion
    -> [Coercion]
    -> Maybe Coercion
    opt_trans_rule_app InScopeSet
    is Coercion
    co1 Coercion
    co2 Coercion
    co1a [Coercion
    co1b] Coercion
    co2a [Coercion
    co2b]

    -- Push transitivity inside forall
    -- forall over types.
    opt_trans_rule InScopeSet
    is Coercion
    co1 Coercion
    co2
      | Just (CoVar
    tv1, ForAllTyFlag
    visL1, ForAllTyFlag
    _visR1, Coercion
    eta1, Coercion
    r1) <- Coercion
    -> Maybe (CoVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion)
    splitForAllCo_ty_maybe Coercion
    co1
      , Just (CoVar
    tv2, ForAllTyFlag
    _visL2, ForAllTyFlag
    visR2, Coercion
    eta2, Coercion
    r2) <- Coercion
    -> Maybe (CoVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion)
    etaForAllCo_ty_maybe Coercion
    co2
      = CoVar
    -> Coercion
    -> Coercion
    -> CoVar
    -> Coercion
    -> Coercion
    -> ForAllTyFlag
    -> ForAllTyFlag
    -> Maybe Coercion
    push_trans CoVar
    tv1 Coercion
    eta1 Coercion
    r1 CoVar
    tv2 Coercion
    eta2 Coercion
    r2 ForAllTyFlag
    visL1 ForAllTyFlag
    visR2

      | Just (CoVar
    tv2, ForAllTyFlag
    _visL2, ForAllTyFlag
    visR2, Coercion
    eta2, Coercion
    r2) <- Coercion
    -> Maybe (CoVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion)
    splitForAllCo_ty_maybe Coercion
    co2
      , Just (CoVar
    tv1, ForAllTyFlag
    visL1, ForAllTyFlag
    _visR1, Coercion
    eta1, Coercion
    r1) <- Coercion
    -> Maybe (CoVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion)
    etaForAllCo_ty_maybe Coercion
    co1
      = CoVar
    -> Coercion
    -> Coercion
    -> CoVar
    -> Coercion
    -> Coercion
    -> ForAllTyFlag
    -> ForAllTyFlag
    -> Maybe Coercion
    push_trans CoVar
    tv1 Coercion
    eta1 Coercion
    r1 CoVar
    tv2 Coercion
    eta2 Coercion
    r2 ForAllTyFlag
    visL1 ForAllTyFlag
    visR2

      where
      push_trans :: CoVar
    -> Coercion
    -> Coercion
    -> CoVar
    -> Coercion
    -> Coercion
    -> ForAllTyFlag
    -> ForAllTyFlag
    -> Maybe Coercion
    push_trans CoVar
    tv1 Coercion
    eta1 Coercion
    r1 CoVar
    tv2 Coercion
    eta2 Coercion
    r2 ForAllTyFlag
    visL ForAllTyFlag
    visR
        -- Given:
        --   co1 = /\ tv1 : eta1 <visL, visM>. r1
        --   co2 = /\ tv2 : eta2 <visM, visR>. r2
        -- Wanted:
        --   /\tv1 : (eta1;eta2) <visL, visR>.  (r1; r2[tv2 |-> tv1 |> eta1])
        = String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
    fireTransRule String
    "EtaAllTy_ty" Coercion
    co1 Coercion
    co2 (Coercion -> Maybe Coercion) -> Coercion -> Maybe Coercion
    forall a b. (a -> b) -> a -> b
    $
          HasDebugCallStack =>
    CoVar
    -> ForAllTyFlag -> ForAllTyFlag -> Coercion -> Coercion -> Coercion
    CoVar
    -> ForAllTyFlag -> ForAllTyFlag -> Coercion -> Coercion -> Coercion
    mkForAllCo CoVar
    tv1 ForAllTyFlag
    visL ForAllTyFlag
    visR (HasDebugCallStack => InScopeSet -> Coercion -> Coercion -> Coercion
    InScopeSet -> Coercion -> Coercion -> Coercion
    opt_trans InScopeSet
    is Coercion
    eta1 Coercion
    eta2) (HasDebugCallStack => InScopeSet -> Coercion -> Coercion -> Coercion
    InScopeSet -> Coercion -> Coercion -> Coercion
    opt_trans InScopeSet
    is' Coercion
    r1 Coercion
    r2')
        where
          is' :: InScopeSet
    is' = InScopeSet
    is InScopeSet -> CoVar -> InScopeSet
    `extendInScopeSet` CoVar
    tv1
          r2' :: Coercion
    r2' = [CoVar] -> [Type] -> Coercion -> Coercion
    substCoWithUnchecked [CoVar
    tv2] [Type -> Coercion -> Type
    mkCastTy (CoVar -> Type
    TyVarTy CoVar
    tv1) Coercion
    eta1] Coercion
    r2

    -- Push transitivity inside forall
    -- forall over coercions.
    opt_trans_rule InScopeSet
    is Coercion
    co1 Coercion
    co2
      | Just (CoVar
    cv1, ForAllTyFlag
    visL1, ForAllTyFlag
    _visR1, Coercion
    eta1, Coercion
    r1) <- Coercion
    -> Maybe (CoVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion)
    splitForAllCo_co_maybe Coercion
    co1
      , Just (CoVar
    cv2, ForAllTyFlag
    _visL2, ForAllTyFlag
    visR2, Coercion
    eta2, Coercion
    r2) <- Coercion
    -> Maybe (CoVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion)
    etaForAllCo_co_maybe Coercion
    co2
      = CoVar
    -> Coercion
    -> Coercion
    -> CoVar
    -> Coercion
    -> Coercion
    -> ForAllTyFlag
    -> ForAllTyFlag
    -> Maybe Coercion
    push_trans CoVar
    cv1 Coercion
    eta1 Coercion
    r1 CoVar
    cv2 Coercion
    eta2 Coercion
    r2 ForAllTyFlag
    visL1 ForAllTyFlag
    visR2

      | Just (CoVar
    cv2, ForAllTyFlag
    _visL2, ForAllTyFlag
    visR2, Coercion
    eta2, Coercion
    r2) <- Coercion
    -> Maybe (CoVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion)
    splitForAllCo_co_maybe Coercion
    co2
      , Just (CoVar
    cv1, ForAllTyFlag
    visL1, ForAllTyFlag
    _visR1, Coercion
    eta1, Coercion
    r1) <- Coercion
    -> Maybe (CoVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion)
    etaForAllCo_co_maybe Coercion
    co1
      = CoVar
    -> Coercion
    -> Coercion
    -> CoVar
    -> Coercion
    -> Coercion
    -> ForAllTyFlag
    -> ForAllTyFlag
    -> Maybe Coercion
    push_trans CoVar
    cv1 Coercion
    eta1 Coercion
    r1 CoVar
    cv2 Coercion
    eta2 Coercion
    r2 ForAllTyFlag
    visL1 ForAllTyFlag
    visR2

      where
      push_trans :: CoVar
    -> Coercion
    -> Coercion
    -> CoVar
    -> Coercion
    -> Coercion
    -> ForAllTyFlag
    -> ForAllTyFlag
    -> Maybe Coercion
    push_trans CoVar
    cv1 Coercion
    eta1 Coercion
    r1 CoVar
    cv2 Coercion
    eta2 Coercion
    r2 ForAllTyFlag
    visL ForAllTyFlag
    visR
        -- Given:
        --   co1 = /\ (cv1 : eta1) <visL, visM>. r1
        --   co2 = /\ (cv2 : eta2) <visM, visR>. r2
        -- Wanted:
        --   n1 = nth 2 eta1
        --   n2 = nth 3 eta1
        --   nco = /\ cv1 : (eta1;eta2). (r1; r2[cv2 |-> (sym n1);cv1;n2])
        = String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
    fireTransRule String
    "EtaAllTy_co" Coercion
    co1 Coercion
    co2 (Coercion -> Maybe Coercion) -> Coercion -> Maybe Coercion
    forall a b. (a -> b) -> a -> b
    $
          HasDebugCallStack =>
    CoVar
    -> ForAllTyFlag -> ForAllTyFlag -> Coercion -> Coercion -> Coercion
    CoVar
    -> ForAllTyFlag -> ForAllTyFlag -> Coercion -> Coercion -> Coercion
    mkForAllCo CoVar
    cv1 ForAllTyFlag
    visL ForAllTyFlag
    visR (HasDebugCallStack => InScopeSet -> Coercion -> Coercion -> Coercion
    InScopeSet -> Coercion -> Coercion -> Coercion
    opt_trans InScopeSet
    is Coercion
    eta1 Coercion
    eta2) (HasDebugCallStack => InScopeSet -> Coercion -> Coercion -> Coercion
    InScopeSet -> Coercion -> Coercion -> Coercion
    opt_trans InScopeSet
    is' Coercion
    r1 Coercion
    r2')
        where
          is' :: InScopeSet
    is'  = InScopeSet
    is InScopeSet -> CoVar -> InScopeSet
    `extendInScopeSet` CoVar
    cv1
          role :: Role
    role = CoVar -> Role
    coVarRole CoVar
    cv1
          eta1' :: Coercion
    eta1' = Role -> Role -> Coercion -> Coercion
    downgradeRole Role
    role Role
    Nominal Coercion
    eta1
          n1 :: Coercion
    n1   = HasDebugCallStack => CoSel -> Coercion -> Coercion
    CoSel -> Coercion -> Coercion
    mkSelCo (Int -> Role -> CoSel
    SelTyCon Int
    2 Role
    role) Coercion
    eta1'
          n2 :: Coercion
    n2   = HasDebugCallStack => CoSel -> Coercion -> Coercion
    CoSel -> Coercion -> Coercion
    mkSelCo (Int -> Role -> CoSel
    SelTyCon Int
    3 Role
    role) Coercion
    eta1'
          r2' :: Coercion
    r2'  = HasDebugCallStack => Subst -> Coercion -> Coercion
    Subst -> Coercion -> Coercion
    substCo ([CoVar] -> [Coercion] -> Subst
    HasDebugCallStack => [CoVar] -> [Coercion] -> Subst
    zipCvSubst [CoVar
    cv2] [(Coercion -> Coercion
    mkSymCo Coercion
    n1) HasDebugCallStack => Coercion -> Coercion -> Coercion
    Coercion -> Coercion -> Coercion
    `mk_trans_co`
                                            (CoVar -> Coercion
    mkCoVarCo CoVar
    cv1) HasDebugCallStack => Coercion -> Coercion -> Coercion
    Coercion -> Coercion -> Coercion
    `mk_trans_co` Coercion
    n2])
                        Coercion
    r2

    -- Push transitivity inside axioms
    opt_trans_rule InScopeSet
    is Coercion
    co1 Coercion
    co2

      -- TrPushAxSym/TrPushSymAx
      -- Put this first!  Otherwise (#23619) we get
      --    newtype N a = MkN a
      --    axN :: forall a. N a ~ a
      -- Now consider (axN ty ; sym (axN ty))
      -- If we put TrPushSymAxR first, we'll get
      --    (axN ty ; sym (axN ty)) :: N ty ~ N ty -- Obviously Refl
      --    --> axN (sym (axN ty))  :: N ty ~ N ty -- Very stupid
      | Just (SwapFlag
    sym1, CoAxiomRule
    axr1, [Coercion]
    cos1) <- Coercion -> Maybe (SwapFlag, CoAxiomRule, [Coercion])
    isAxiomCo_maybe Coercion
    co1
      , Just (SwapFlag
    sym2, CoAxiomRule
    axr2, [Coercion]
    cos2) <- Coercion -> Maybe (SwapFlag, CoAxiomRule, [Coercion])
    isAxiomCo_maybe Coercion
    co2
      , CoAxiomRule
    axr1 CoAxiomRule -> CoAxiomRule -> Bool
    forall a. Eq a => a -> a -> Bool
    == CoAxiomRule
    axr2
      , SwapFlag
    sym1 SwapFlag -> SwapFlag -> Bool
    forall a. Eq a => a -> a -> Bool
    == SwapFlag -> SwapFlag
    flipSwap SwapFlag
    sym2
      , Just (TyCon
    tc, Role
    role, CoAxBranch
    branch) <- CoAxiomRule -> Maybe (TyCon, Role, CoAxBranch)
    coAxiomRuleBranch_maybe CoAxiomRule
    axr1
      , let qtvs :: [CoVar]
    qtvs   = CoAxBranch -> [CoVar]
    coAxBranchTyVars CoAxBranch
    branch [CoVar] -> [CoVar] -> [CoVar]
    forall a. [a] -> [a] -> [a]
    ++ CoAxBranch -> [CoVar]
    coAxBranchCoVars CoAxBranch
    branch
            lhs :: Type
    lhs    = TyCon -> [Type] -> Type
    mkTyConApp TyCon
    tc (CoAxBranch -> [Type]
    coAxBranchLHS CoAxBranch
    branch)
            rhs :: Type
    rhs    = CoAxBranch -> Type
    coAxBranchRHS CoAxBranch
    branch
            pivot_tvs :: TyCoVarSet
    pivot_tvs = Type -> TyCoVarSet
    exactTyCoVarsOfType (SwapFlag -> Type -> Type -> Type
    forall a. SwapFlag -> a -> a -> a
    pickSwap SwapFlag
    sym2 Type
    lhs Type
    rhs)
      , (CoVar -> Bool) -> [CoVar] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all (CoVar -> TyCoVarSet -> Bool
    `elemVarSet` TyCoVarSet
    pivot_tvs) [CoVar]
    qtvs
      = String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
    fireTransRule String
    "TrPushAxSym" Coercion
    co1 Coercion
    co2 (Coercion -> Maybe Coercion) -> Coercion -> Maybe Coercion
    forall a b. (a -> b) -> a -> b
    $
        if SwapFlag -> Bool
    isSwapped SwapFlag
    sym2
           -- TrPushAxSym
        then Role -> [CoVar] -> [Coercion] -> Type -> Coercion
    liftCoSubstWith Role
    role [CoVar]
    qtvs (HasDebugCallStack =>
    InScopeSet -> [Coercion] -> [Coercion] -> [Coercion]
    InScopeSet -> [Coercion] -> [Coercion] -> [Coercion]
    opt_transList InScopeSet
    is [Coercion]
    cos1 ((Coercion -> Coercion) -> [Coercion] -> [Coercion]
    forall a b. (a -> b) -> [a] -> [b]
    map Coercion -> Coercion
    mkSymCo [Coercion]
    cos2)) Type
    lhs
           -- TrPushSymAx
        else Role -> [CoVar] -> [Coercion] -> Type -> Coercion
    liftCoSubstWith Role
    role [CoVar]
    qtvs (HasDebugCallStack =>
    InScopeSet -> [Coercion] -> [Coercion] -> [Coercion]
    InScopeSet -> [Coercion] -> [Coercion] -> [Coercion]
    opt_transList InScopeSet
    is ((Coercion -> Coercion) -> [Coercion] -> [Coercion]
    forall a b. (a -> b) -> [a] -> [b]
    map Coercion -> Coercion
    mkSymCo [Coercion]
    cos1) [Coercion]
    cos2) Type
    rhs

      -- See Note [Push transitivity inside axioms] and
      -- Note [Push transitivity inside newtype axioms only]
      -- TrPushSymAxR
      | Just (SwapFlag
    sym, CoAxiomRule
    axr, [Coercion]
    cos1) <- Coercion -> Maybe (SwapFlag, CoAxiomRule, [Coercion])
    isAxiomCo_maybe Coercion
    co1
      , SwapFlag -> Bool
    isSwapped SwapFlag
    sym
      , Just [Coercion]
    cos2 <- SwapFlag -> CoAxiomRule -> Coercion -> Maybe [Coercion]
    matchNewtypeBranch SwapFlag
    sym CoAxiomRule
    axr Coercion
    co2
      , let newAxInst :: Coercion
    newAxInst = CoAxiomRule -> [Coercion] -> Coercion
    AxiomCo CoAxiomRule
    axr (HasDebugCallStack =>
    InScopeSet -> [Coercion] -> [Coercion] -> [Coercion]
    InScopeSet -> [Coercion] -> [Coercion] -> [Coercion]
    opt_transList InScopeSet
    is ((Coercion -> Coercion) -> [Coercion] -> [Coercion]
    forall a b. (a -> b) -> [a] -> [b]
    map Coercion -> Coercion
    mkSymCo [Coercion]
    cos2) [Coercion]
    cos1)
      = String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
    fireTransRule String
    "TrPushSymAxR" Coercion
    co1 Coercion
    co2 (Coercion -> Maybe Coercion) -> Coercion -> Maybe Coercion
    forall a b. (a -> b) -> a -> b
    $ Coercion -> Coercion
    SymCo Coercion
    newAxInst

      -- TrPushAxR
      | Just (SwapFlag
    sym, CoAxiomRule
    axr, [Coercion]
    cos1) <- Coercion -> Maybe (SwapFlag, CoAxiomRule, [Coercion])
    isAxiomCo_maybe Coercion
    co1
      , SwapFlag -> Bool
    notSwapped SwapFlag
    sym
      , Just [Coercion]
    cos2 <- SwapFlag -> CoAxiomRule -> Coercion -> Maybe [Coercion]
    matchNewtypeBranch SwapFlag
    sym CoAxiomRule
    axr Coercion
    co2
      , let newAxInst :: Coercion
    newAxInst = CoAxiomRule -> [Coercion] -> Coercion
    AxiomCo CoAxiomRule
    axr (HasDebugCallStack =>
    InScopeSet -> [Coercion] -> [Coercion] -> [Coercion]
    InScopeSet -> [Coercion] -> [Coercion] -> [Coercion]
    opt_transList InScopeSet
    is [Coercion]
    cos1 [Coercion]
    cos2)
      = String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
    fireTransRule String
    "TrPushAxR" Coercion
    co1 Coercion
    co2 Coercion
    newAxInst

      -- TrPushSymAxL
      | Just (SwapFlag
    sym, CoAxiomRule
    axr, [Coercion]
    cos2) <- Coercion -> Maybe (SwapFlag, CoAxiomRule, [Coercion])
    isAxiomCo_maybe Coercion
    co2
      , SwapFlag -> Bool
    isSwapped SwapFlag
    sym
      , Just [Coercion]
    cos1 <- SwapFlag -> CoAxiomRule -> Coercion -> Maybe [Coercion]
    matchNewtypeBranch (SwapFlag -> SwapFlag
    flipSwap SwapFlag
    sym) CoAxiomRule
    axr Coercion
    co1
      , let newAxInst :: Coercion
    newAxInst = CoAxiomRule -> [Coercion] -> Coercion
    AxiomCo CoAxiomRule
    axr (HasDebugCallStack =>
    InScopeSet -> [Coercion] -> [Coercion] -> [Coercion]
    InScopeSet -> [Coercion] -> [Coercion] -> [Coercion]
    opt_transList InScopeSet
    is [Coercion]
    cos2 ((Coercion -> Coercion) -> [Coercion] -> [Coercion]
    forall a b. (a -> b) -> [a] -> [b]
    map Coercion -> Coercion
    mkSymCo [Coercion]
    cos1))
      = String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
    fireTransRule String
    "TrPushSymAxL" Coercion
    co1 Coercion
    co2 (Coercion -> Maybe Coercion) -> Coercion -> Maybe Coercion
    forall a b. (a -> b) -> a -> b
    $ Coercion -> Coercion
    SymCo Coercion
    newAxInst

      -- TrPushAxL
      | Just (SwapFlag
    sym, CoAxiomRule
    axr, [Coercion]
    cos2) <- Coercion -> Maybe (SwapFlag, CoAxiomRule, [Coercion])
    isAxiomCo_maybe Coercion
    co2
      , SwapFlag -> Bool
    notSwapped SwapFlag
    sym
      , Just [Coercion]
    cos1 <- SwapFlag -> CoAxiomRule -> Coercion -> Maybe [Coercion]
    matchNewtypeBranch (SwapFlag -> SwapFlag
    flipSwap SwapFlag
    sym) CoAxiomRule
    axr Coercion
    co1
      , let newAxInst :: Coercion
    newAxInst = CoAxiomRule -> [Coercion] -> Coercion
    AxiomCo CoAxiomRule
    axr (HasDebugCallStack =>
    InScopeSet -> [Coercion] -> [Coercion] -> [Coercion]
    InScopeSet -> [Coercion] -> [Coercion] -> [Coercion]
    opt_transList InScopeSet
    is [Coercion]
    cos1 [Coercion]
    cos2)
      = String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
    fireTransRule String
    "TrPushAxL" Coercion
    co1 Coercion
    co2 Coercion
    newAxInst

    opt_trans_rule InScopeSet
    _ Coercion
    co1 Coercion
    co2        -- Identity rule
      | let ty1 :: Type
    ty1 = HasDebugCallStack => Coercion -> Type
    Coercion -> Type
    coercionLKind Coercion
    co1
            r :: Role
    r   = Coercion -> Role
    coercionRole Coercion
    co1
            ty2 :: Type
    ty2 = HasDebugCallStack => Coercion -> Type
    Coercion -> Type
    coercionRKind Coercion
    co2
      , Type
    ty1 HasCallStack => Type -> Type -> Bool
    Type -> Type -> Bool
    `eqType` Type
    ty2
      = String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
    fireTransRule String
    "RedTypeDirRefl" Coercion
    co1 Coercion
    co2 (Coercion -> Maybe Coercion) -> Coercion -> Maybe Coercion
    forall a b. (a -> b) -> a -> b
    $
        Role -> Type -> Coercion
    mkReflCo Role
    r Type
    ty2

    opt_trans_rule InScopeSet
    _ Coercion
    _ Coercion
    _ = Maybe Coercion
    forall a. Maybe a
    Nothing

    -- See Note [EtaAppCo]
    opt_trans_rule_app :: InScopeSet
                       -> Coercion   -- original left-hand coercion (printing only)
                       -> Coercion   -- original right-hand coercion (printing only)
                       -> Coercion   -- left-hand coercion "function"
                       -> [Coercion] -- left-hand coercion "args"
                       -> Coercion   -- right-hand coercion "function"
                       -> [Coercion] -- right-hand coercion "args"
                       -> Maybe Coercion
    opt_trans_rule_app :: InScopeSet
    -> Coercion
    -> Coercion
    -> Coercion
    -> [Coercion]
    -> Coercion
    -> [Coercion]
    -> Maybe Coercion
    opt_trans_rule_app InScopeSet
    is Coercion
    orig_co1 Coercion
    orig_co2 Coercion
    co1a [Coercion]
    co1bs Coercion
    co2a [Coercion]
    co2bs
      | AppCo Coercion
    co1aa Coercion
    co1ab <- Coercion
    co1a
      , Just (Coercion
    co2aa, Coercion
    co2ab) <- Coercion -> Maybe (Coercion, Coercion)
    etaAppCo_maybe Coercion
    co2a
      = InScopeSet
    -> Coercion
    -> Coercion
    -> Coercion
    -> [Coercion]
    -> Coercion
    -> [Coercion]
    -> Maybe Coercion
    opt_trans_rule_app InScopeSet
    is Coercion
    orig_co1 Coercion
    orig_co2 Coercion
    co1aa (Coercion
    co1abCoercion -> [Coercion] -> [Coercion]
    forall a. a -> [a] -> [a]
    :[Coercion]
    co1bs) Coercion
    co2aa (Coercion
    co2abCoercion -> [Coercion] -> [Coercion]
    forall a. a -> [a] -> [a]
    :[Coercion]
    co2bs)

      | AppCo Coercion
    co2aa Coercion
    co2ab <- Coercion
    co2a
      , Just (Coercion
    co1aa, Coercion
    co1ab) <- Coercion -> Maybe (Coercion, Coercion)
    etaAppCo_maybe Coercion
    co1a
      = InScopeSet
    -> Coercion
    -> Coercion
    -> Coercion
    -> [Coercion]
    -> Coercion
    -> [Coercion]
    -> Maybe Coercion
    opt_trans_rule_app InScopeSet
    is Coercion
    orig_co1 Coercion
    orig_co2 Coercion
    co1aa (Coercion
    co1abCoercion -> [Coercion] -> [Coercion]
    forall a. a -> [a] -> [a]
    :[Coercion]
    co1bs) Coercion
    co2aa (Coercion
    co2abCoercion -> [Coercion] -> [Coercion]
    forall a. a -> [a] -> [a]
    :[Coercion]
    co2bs)

      | Bool
    otherwise
      = Bool -> Maybe Coercion -> Maybe Coercion
    forall a. HasCallStack => Bool -> a -> a
    assert ([Coercion]
    co1bs [Coercion] -> [Coercion] -> Bool
    forall a b. [a] -> [b] -> Bool
    `equalLength` [Coercion]
    co2bs) (Maybe Coercion -> Maybe Coercion)
    -> Maybe Coercion -> Maybe Coercion
    forall a b. (a -> b) -> a -> b
    $
        String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
    fireTransRule (String
    "EtaApps:" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show ([Coercion] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Coercion]
    co1bs)) Coercion
    orig_co1 Coercion
    orig_co2 (Coercion -> Maybe Coercion) -> Coercion -> Maybe Coercion
    forall a b. (a -> b) -> a -> b
    $
        let rt1a :: Type
    rt1a = HasDebugCallStack => Coercion -> Type
    Coercion -> Type
    coercionRKind Coercion
    co1a

            lt2a :: Type
    lt2a = HasDebugCallStack => Coercion -> Type
    Coercion -> Type
    coercionLKind Coercion
    co2a
            rt2a :: Role
    rt2a = Coercion -> Role
    coercionRole  Coercion
    co2a

            rt1bs :: [Type]
    rt1bs = (Coercion -> Type) -> [Coercion] -> [Type]
    forall a b. (a -> b) -> [a] -> [b]
    map HasDebugCallStack => Coercion -> Type
    Coercion -> Type
    coercionRKind [Coercion]
    co1bs
            lt2bs :: [Type]
    lt2bs = (Coercion -> Type) -> [Coercion] -> [Type]
    forall a b. (a -> b) -> [a] -> [b]
    map HasDebugCallStack => Coercion -> Type
    Coercion -> Type
    coercionLKind [Coercion]
    co2bs
            rt2bs :: [Role]
    rt2bs = (Coercion -> Role) -> [Coercion] -> [Role]
    forall a b. (a -> b) -> [a] -> [b]
    map Coercion -> Role
    coercionRole [Coercion]
    co2bs

            kcoa :: Coercion
    kcoa = Coercion -> Coercion
    mkKindCo (Coercion -> Coercion) -> Coercion -> Coercion
    forall a b. (a -> b) -> a -> b
    $ HasDebugCallStack => Type -> Type -> Coercion
    Type -> Type -> Coercion
    buildCoercion Type
    lt2a Type
    rt1a
            kcobs :: [Coercion]
    kcobs = (Coercion -> Coercion) -> [Coercion] -> [Coercion]
    forall a b. (a -> b) -> [a] -> [b]
    map Coercion -> Coercion
    mkKindCo ([Coercion] -> [Coercion]) -> [Coercion] -> [Coercion]
    forall a b. (a -> b) -> a -> b
    $ (Type -> Type -> Coercion) -> [Type] -> [Type] -> [Coercion]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith HasDebugCallStack => Type -> Type -> Coercion
    Type -> Type -> Coercion
    buildCoercion [Type]
    lt2bs [Type]
    rt1bs

            co2a' :: Coercion
    co2a'   = Role -> Type -> Coercion -> Coercion -> Coercion
    mkCoherenceLeftCo Role
    rt2a Type
    lt2a Coercion
    kcoa Coercion
    co2a
            co2bs' :: [Coercion]
    co2bs'  = (Role -> Type -> Coercion -> Coercion)
    -> [Role] -> [Type] -> [Coercion] -> [Coercion]
    forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
    zipWith3 Role -> Type -> Coercion -> Coercion
    mkGReflLeftCo [Role]
    rt2bs [Type]
    lt2bs [Coercion]
    kcobs
            co2bs'' :: [Coercion]
    co2bs'' = (Coercion -> Coercion -> Coercion)
    -> [Coercion] -> [Coercion] -> [Coercion]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith HasDebugCallStack => Coercion -> Coercion -> Coercion
    Coercion -> Coercion -> Coercion
    mk_trans_co [Coercion]
    co2bs' [Coercion]
    co2bs
        in
        Coercion -> [Coercion] -> Coercion
    mkAppCos (HasDebugCallStack => InScopeSet -> Coercion -> Coercion -> Coercion
    InScopeSet -> Coercion -> Coercion -> Coercion
    opt_trans InScopeSet
    is Coercion
    co1a Coercion
    co2a')
                 ((Coercion -> Coercion -> Coercion)
    -> [Coercion] -> [Coercion] -> [Coercion]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith (HasDebugCallStack => InScopeSet -> Coercion -> Coercion -> Coercion
    InScopeSet -> Coercion -> Coercion -> Coercion
    opt_trans InScopeSet
    is) [Coercion]
    co1bs [Coercion]
    co2bs'')

    fireTransRule :: String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
    fireTransRule :: String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
    fireTransRule String
    _rule Coercion
    _co1 Coercion
    _co2 Coercion
    res
      = Coercion -> Maybe Coercion
    forall a. a -> Maybe a
    Just Coercion
    res

    {-
    Note [Push transitivity inside axioms]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    opt_trans_rule tries to push transitivity inside axioms to deal with cases like
    the following:

        newtype N a = MkN a

        axN :: N a ~R# a

        covar :: a ~R# b
        co1 = axN <a> :: N a ~R# a
        co2 = axN <b> :: N b ~R# b

        co :: a ~R# b
        co = sym co1 ; N covar ; co2

    When we are optimising co, we want to notice that the two axiom instantiations
    cancel out. This is implemented by rules such as TrPushSymAxR, which transforms
        sym (axN <a>) ; N covar
    into
        sym (axN covar)
    so that TrPushSymAx can subsequently transform
        sym (axN covar) ; axN <b>
    into
        covar
    which is much more compact. In some perf test cases this kind of pattern can be
    generated repeatedly during simplification, so it is very important we squash it
    to stop coercions growing exponentially.  For more details see the paper:

        Evidence normalisation in System FC
        Dimitrios Vytiniotis and Simon Peyton Jones
        RTA'13, 2013
        https://www.microsoft.com/en-us/research/publication/evidence-normalization-system-fc-2/

    Note [Push transitivity inside newtype axioms only]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    The optimization described in Note [Push transitivity inside axioms] is possible
    for both newtype and type family axioms.  However, for type family axioms it is
    relatively common to have transitive sequences of axioms instantiations, for
    example:

        data Nat = Zero | Suc Nat

        type family Index (n :: Nat) (xs :: [Type]) :: Type where
          Index Zero    (x : xs) = x
          Index (Suc n) (x : xs) = Index n xs

        axIndex :: { forall x::Type. forall xs::[Type]. Index Zero (x : xs) ~ x
                   ; forall n::Nat. forall x::Type. forall xs::[Type]. Index (Suc n) (x : xs) ~ Index n xs }

        co :: Index (Suc (Suc Zero)) [a, b, c] ~ c
        co = axIndex[1] <Suc Zero> <a> <[b, c]>
           ; axIndex[1] <Zero> <b> <[c]>
           ; axIndex[0] <c> <[]>

    Not only are there no cancellation opportunities here, but calling matchAxiom
    repeatedly down the transitive chain is very expensive.  Hence we do not attempt
    to push transitivity inside type family axioms.  See #8095, !9210 and related tickets.

    This is implemented by opt_trans_rule checking that the axiom is for a newtype
    constructor (i.e. not a type family).  Adding these guards substantially
    improved performance (reduced bytes allocated by more than 10%) for the tests
    CoOpt_Singletons, LargeRecord, T12227, T12545, T13386, T15703, T5030, T8095.

    A side benefit is that we do not risk accidentally creating an ill-typed
    coercion; see Note [Why call checkAxInstCo during optimisation].

    There may exist programs that previously relied on pushing transitivity inside
    type family axioms to avoid creating huge coercions, which will regress in
    compile time performance as a result of this change.  We do not currently know
    of any examples, but if any come to light we may need to reconsider this
    behaviour.

    Note [Why call checkAxInstCo during optimisation]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    NB: The following is no longer relevant, because we no longer push transitivity
    into type family axioms (Note [Push transitivity inside newtype axioms only]).
    It is retained for reference in case we change this behaviour in the future.

    It is possible that otherwise-good-looking optimisations meet with disaster
    in the presence of axioms with multiple equations. Consider

    type family Equal (a :: *) (b :: *) :: Bool where
      Equal a a = True
      Equal a b = False
    type family Id (a :: *) :: * where
      Id a = a

    axEq :: { [a::*].       Equal a a ~ True
            ; [a::*, b::*]. Equal a b ~ False }
    axId :: [a::*]. Id a ~ a

    co1 = Equal (axId[0] Int) (axId[0] Bool)
      :: Equal (Id Int) (Id Bool) ~  Equal Int Bool
    co2 = axEq[1] <Int> <Bool>
      :: Equal Int Bool ~ False

    We wish to optimise (co1 ; co2). We end up in rule TrPushAxL, noting that
    co2 is an axiom and that matchAxiom succeeds when looking at co1. But, what
    happens when we push the coercions inside? We get

    co3 = axEq[1] (axId[0] Int) (axId[0] Bool)
      :: Equal (Id Int) (Id Bool) ~ False

    which is bogus! This is because the type system isn't smart enough to know
    that (Id Int) and (Id Bool) are Surely Apart, as they're headed by type
    families. At the time of writing, I (Richard Eisenberg) couldn't think of
    a way of detecting this any more efficient than just building the optimised
    coercion and checking.

    Note [EtaAppCo]
    ~~~~~~~~~~~~~~~
    Suppose we're trying to optimize (co1a co1b ; co2a co2b). Ideally, we'd
    like to rewrite this to (co1a ; co2a) (co1b ; co2b). The problem is that
    the resultant coercions might not be well kinded. Here is an example (things
    labeled with x don't matter in this example):

      k1 :: Type
      k2 :: Type

      a :: k1 -> Type
      b :: k1

      h :: k1 ~ k2

      co1a :: x1 ~ (a |> (h -> <Type>)
      co1b :: x2 ~ (b |> h)

      co2a :: a ~ x3
      co2b :: b ~ x4

    First, convince yourself of the following:

      co1a co1b :: x1 x2 ~ (a |> (h -> <Type>)) (b |> h)
      co2a co2b :: a b   ~ x3 x4

      (a |> (h -> <Type>)) (b |> h) `eqType` a b

    That last fact is due to Note [Non-trivial definitional equality] in GHC.Core.TyCo.Rep,
    where we ignore coercions in types as long as two types' kinds are the same.
    In our case, we meet this last condition, because

      (a |> (h -> <Type>)) (b |> h) :: Type
        and
      a b :: Type

    So the input coercion (co1a co1b ; co2a co2b) is well-formed. But the
    suggested output coercions (co1a ; co2a) and (co1b ; co2b) are not -- the
    kinds don't match up.

    The solution here is to twiddle the kinds in the output coercions. First, we
    need to find coercions

      ak :: kind(a |> (h -> <Type>)) ~ kind(a)
      bk :: kind(b |> h)             ~ kind(b)

    This can be done with mkKindCo and buildCoercion. The latter assumes two
    types are identical modulo casts and builds a coercion between them.

    Then, we build (co1a ; co2a |> sym ak) and (co1b ; co2b |> sym bk) as the
    output coercions. These are well-kinded.

    Also, note that all of this is done after accumulated any nested AppCo
    parameters. This step is to avoid quadratic behavior in calling coercionKind.

    The problem described here was first found in dependent/should_compile/dynamic-paper.

    -}

    -----------
    swapSym :: SwapFlag -> (a,a) -> (a,a)
    swapSym :: forall a. SwapFlag -> (a, a) -> (a, a)
    swapSym SwapFlag
    IsSwapped  (a
    x,a
    y) = (a
    y,a
    x)
    swapSym SwapFlag
    NotSwapped (a
    x,a
    y) = (a
    x,a
    y)

    wrapSym :: SwapFlag -> Coercion -> Coercion
    wrapSym :: SwapFlag -> Coercion -> Coercion
    wrapSym SwapFlag
    IsSwapped  Coercion
    co = Coercion -> Coercion
    mkSymCo Coercion
    co
    wrapSym SwapFlag
    NotSwapped Coercion
    co = Coercion
    co

    -- | Conditionally set a role to be representational
    wrapRole :: ReprFlag
             -> Role         -- ^ current role
             -> Coercion -> Coercion
    wrapRole :: Bool -> Role -> Coercion -> Coercion
    wrapRole Bool
    False Role
    _       = Coercion -> Coercion
    forall a. a -> a
    id
    wrapRole Bool
    True  Role
    current = Role -> Role -> Coercion -> Coercion
    downgradeRole Role
    Representational Role
    current

    -- | If we require a representational role, return that. Otherwise,
    -- return the "default" role provided.
    chooseRole :: ReprFlag
               -> Role    -- ^ "default" role
               -> Role
    chooseRole :: Bool -> Role -> Role
    chooseRole Bool
    True Role
    _ = Role
    Representational
    chooseRole Bool
    _    Role
    r = Role
    r

    -----------
    isAxiomCo_maybe :: Coercion -> Maybe (SwapFlag, CoAxiomRule, [Coercion])
    -- We don't expect to see nested SymCo; and that lets us write a simple,
    -- non-recursive function. (If we see a nested SymCo we'll just fail,
    -- which is ok.)
    isAxiomCo_maybe :: Coercion -> Maybe (SwapFlag, CoAxiomRule, [Coercion])
    isAxiomCo_maybe (SymCo (AxiomCo CoAxiomRule
    ax [Coercion]
    cos)) = (SwapFlag, CoAxiomRule, [Coercion])
    -> Maybe (SwapFlag, CoAxiomRule, [Coercion])
    forall a. a -> Maybe a
    Just (SwapFlag
    IsSwapped,  CoAxiomRule
    ax, [Coercion]
    cos)
    isAxiomCo_maybe (AxiomCo CoAxiomRule
    ax [Coercion]
    cos)         = (SwapFlag, CoAxiomRule, [Coercion])
    -> Maybe (SwapFlag, CoAxiomRule, [Coercion])
    forall a. a -> Maybe a
    Just (SwapFlag
    NotSwapped, CoAxiomRule
    ax, [Coercion]
    cos)
    isAxiomCo_maybe Coercion
    _                        = Maybe (SwapFlag, CoAxiomRule, [Coercion])
    forall a. Maybe a
    Nothing

    matchNewtypeBranch :: SwapFlag -- IsSwapped = match LHS, NotSwapped = match RHS
                       -> CoAxiomRule
                       -> Coercion -> Maybe [Coercion]
    matchNewtypeBranch :: SwapFlag -> CoAxiomRule -> Coercion -> Maybe [Coercion]
    matchNewtypeBranch SwapFlag
    sym CoAxiomRule
    axr Coercion
    co
      | Just (TyCon
    tc,CoAxBranch
    branch) <- CoAxiomRule -> Maybe (TyCon, CoAxBranch)
    isNewtypeAxiomRule_maybe CoAxiomRule
    axr
      , CoAxBranch { cab_tvs :: CoAxBranch -> [CoVar]
    cab_tvs = [CoVar]
    qtvs
                   , cab_cvs :: CoAxBranch -> [CoVar]
    cab_cvs = []   -- can't infer these, so fail if there are any
                   , cab_roles :: CoAxBranch -> [Role]
    cab_roles = [Role]
    roles
                   , cab_lhs :: CoAxBranch -> [Type]
    cab_lhs = [Type]
    lhs
                   , cab_rhs :: CoAxBranch -> Type
    cab_rhs = Type
    rhs } <- CoAxBranch
    branch
      , Just LiftingContext
    subst <- TyCoVarSet -> Type -> Coercion -> Maybe LiftingContext
    liftCoMatch ([CoVar] -> TyCoVarSet
    mkVarSet [CoVar]
    qtvs)
                                  (SwapFlag -> Type -> Type -> Type
    forall a. SwapFlag -> a -> a -> a
    pickSwap SwapFlag
    sym Type
    rhs (TyCon -> [Type] -> Type
    mkTyConApp TyCon
    tc [Type]
    lhs))
                                  Coercion
    co
      , (CoVar -> Bool) -> [CoVar] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all (CoVar -> LiftingContext -> Bool
    `isMappedByLC` LiftingContext
    subst) [CoVar]
    qtvs
      = (Role -> CoVar -> Maybe Coercion)
    -> [Role] -> [CoVar] -> Maybe [Coercion]
    forall (m :: * -> *) a b c.
    Applicative m =>
    (a -> b -> m c) -> [a] -> [b] -> m [c]
    zipWithM (LiftingContext -> Role -> CoVar -> Maybe Coercion
    liftCoSubstTyVar LiftingContext
    subst) [Role]
    roles [CoVar]
    qtvs

      | Bool
    otherwise
      = Maybe [Coercion]
    forall a. Maybe a
    Nothing

    -------------
    compatible_co :: Coercion -> Coercion -> Bool
    -- Check whether (co1 . co2) will be well-kinded
    compatible_co :: Coercion -> Coercion -> Bool
    compatible_co Coercion
    co1 Coercion
    co2
      = Type
    x1 HasCallStack => Type -> Type -> Bool
    Type -> Type -> Bool
    `eqType` Type
    x2
      where
        x1 :: Type
    x1 = HasDebugCallStack => Coercion -> Type
    Coercion -> Type
    coercionRKind Coercion
    co1
        x2 :: Type
    x2 = HasDebugCallStack => Coercion -> Type
    Coercion -> Type
    coercionLKind Coercion
    co2

    -------------
    {-
    etaForAllCo
    ~~~~~~~~~~~~~~~~~
    (1) etaForAllCo_ty_maybe
    Suppose we have

      g : all a1:k1.t1  ~  all a2:k2.t2

    but g is *not* a ForAllCo. We want to eta-expand it. So, we do this:

      g' = all a1:(ForAllKindCo g).(InstCo g (a1 ~ a1 |> ForAllKindCo g))

    Call the kind coercion h1 and the body coercion h2. We can see that

      h2 : t1 ~ t2[a2 |-> (a1 |> h1)]

    According to the typing rule for ForAllCo, we get that

      g' : all a1:k1.t1  ~  all a1:k2.(t2[a2 |-> (a1 |> h1)][a1 |-> a1 |> sym h1])

    or

      g' : all a1:k1.t1  ~  all a1:k2.(t2[a2 |-> a1])

    as desired.

    (2) etaForAllCo_co_maybe
    Suppose we have

      g : all c1:(s1~s2). t1 ~ all c2:(s3~s4). t2

    Similarly, we do this

      g' = all c1:h1. h2
         : all c1:(s1~s2). t1 ~ all c1:(s3~s4). t2[c2 |-> (sym eta1;c1;eta2)]
                                                  [c1 |-> eta1;c1;sym eta2]

    Here,

      h1   = mkSelCo Nominal 0 g       :: (s1~s2)~(s3~s4)
      eta1 = mkSelCo (SelTyCon 2 r) h1 :: (s1 ~ s3)
      eta2 = mkSelCo (SelTyCon 3 r) h1 :: (s2 ~ s4)
      h2   = mkInstCo g (cv1 ~ (sym eta1;c1;eta2))
    -}
    etaForAllCo_ty_maybe :: Coercion -> Maybe (TyVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion)
    -- Try to make the coercion be of form (forall tv:kind_co. co)
    etaForAllCo_ty_maybe :: Coercion
    -> Maybe (CoVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion)
    etaForAllCo_ty_maybe Coercion
    co
      | Just (CoVar
    tv, ForAllTyFlag
    visL, ForAllTyFlag
    visR, Coercion
    kind_co, Coercion
    r) <- Coercion
    -> Maybe (CoVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion)
    splitForAllCo_ty_maybe Coercion
    co
      = (CoVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion)
    -> Maybe (CoVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion)
    forall a. a -> Maybe a
    Just (CoVar
    tv, ForAllTyFlag
    visL, ForAllTyFlag
    visR, Coercion
    kind_co, Coercion
    r)

      | (Pair Type
    ty1 Type
    ty2, Role
    role)  <- Coercion -> (Pair Type, Role)
    coercionKindRole Coercion
    co
      , Just (Bndr CoVar
    tv1 ForAllTyFlag
    vis1, Type
    _) <- Type -> Maybe (ForAllTyBinder, Type)
    splitForAllForAllTyBinder_maybe Type
    ty1
      , CoVar -> Bool
    isTyVar CoVar
    tv1
      , Just (Bndr CoVar
    tv2 ForAllTyFlag
    vis2, Type
    _) <- Type -> Maybe (ForAllTyBinder, Type)
    splitForAllForAllTyBinder_maybe Type
    ty2
      , CoVar -> Bool
    isTyVar CoVar
    tv2
      -- can't eta-expand at nominal role unless visibilities match
      , (Role
    role Role -> Role -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Role
    Nominal) Bool -> Bool -> Bool
    || (ForAllTyFlag
    vis1 ForAllTyFlag -> ForAllTyFlag -> Bool
    `eqForAllVis` ForAllTyFlag
    vis2)
      , let kind_co :: Coercion
    kind_co = HasDebugCallStack => CoSel -> Coercion -> Coercion
    CoSel -> Coercion -> Coercion
    mkSelCo CoSel
    SelForAll Coercion
    co
      = (CoVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion)
    -> Maybe (CoVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion)
    forall a. a -> Maybe a
    Just ( CoVar
    tv1, ForAllTyFlag
    vis1, ForAllTyFlag
    vis2, Coercion
    kind_co
             , Coercion -> Coercion -> Coercion
    mkInstCo Coercion
    co (Role -> Type -> Coercion -> Coercion
    mk_grefl_right_co Role
    Nominal (CoVar -> Type
    TyVarTy CoVar
    tv1) Coercion
    kind_co))

      | Bool
    otherwise
      = Maybe (CoVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion)
    forall a. Maybe a
    Nothing

    etaForAllCo_co_maybe :: Coercion -> Maybe (CoVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion)
    -- Try to make the coercion be of form (forall cv:kind_co. co)
    etaForAllCo_co_maybe :: Coercion
    -> Maybe (CoVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion)
    etaForAllCo_co_maybe Coercion
    co
      | Just (CoVar
    cv, ForAllTyFlag
    visL, ForAllTyFlag
    visR, Coercion
    kind_co, Coercion
    r) <- Coercion
    -> Maybe (CoVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion)
    splitForAllCo_co_maybe Coercion
    co
      = (CoVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion)
    -> Maybe (CoVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion)
    forall a. a -> Maybe a
    Just (CoVar
    cv, ForAllTyFlag
    visL, ForAllTyFlag
    visR, Coercion
    kind_co, Coercion
    r)

      | (Pair Type
    ty1 Type
    ty2, Role
    role)  <- Coercion -> (Pair Type, Role)
    coercionKindRole Coercion
    co
      , Just (Bndr CoVar
    cv1 ForAllTyFlag
    vis1, Type
    _) <- Type -> Maybe (ForAllTyBinder, Type)
    splitForAllForAllTyBinder_maybe Type
    ty1
      , CoVar -> Bool
    isCoVar CoVar
    cv1
      , Just (Bndr CoVar
    cv2 ForAllTyFlag
    vis2, Type
    _) <- Type -> Maybe (ForAllTyBinder, Type)
    splitForAllForAllTyBinder_maybe Type
    ty2
      , CoVar -> Bool
    isCoVar CoVar
    cv2
      -- can't eta-expand at nominal role unless visibilities match
      , (Role
    role Role -> Role -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Role
    Nominal)
      = let kind_co :: Coercion
    kind_co  = HasDebugCallStack => CoSel -> Coercion -> Coercion
    CoSel -> Coercion -> Coercion
    mkSelCo CoSel
    SelForAll Coercion
    co
            r :: Role
    r        = CoVar -> Role
    coVarRole CoVar
    cv1
            l_co :: Coercion
    l_co     = CoVar -> Coercion
    mkCoVarCo CoVar
    cv1
            kind_co' :: Coercion
    kind_co' = Role -> Role -> Coercion -> Coercion
    downgradeRole Role
    r Role
    Nominal Coercion
    kind_co
            r_co :: Coercion
    r_co     = Coercion -> Coercion
    mkSymCo (HasDebugCallStack => CoSel -> Coercion -> Coercion
    CoSel -> Coercion -> Coercion
    mkSelCo (Int -> Role -> CoSel
    SelTyCon Int
    2 Role
    r) Coercion
    kind_co')
                       HasDebugCallStack => Coercion -> Coercion -> Coercion
    Coercion -> Coercion -> Coercion
    `mk_trans_co` Coercion
    l_co
                       HasDebugCallStack => Coercion -> Coercion -> Coercion
    Coercion -> Coercion -> Coercion
    `mk_trans_co` HasDebugCallStack => CoSel -> Coercion -> Coercion
    CoSel -> Coercion -> Coercion
    mkSelCo (Int -> Role -> CoSel
    SelTyCon Int
    3 Role
    r) Coercion
    kind_co'
        in (CoVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion)
    -> Maybe (CoVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion)
    forall a. a -> Maybe a
    Just ( CoVar
    cv1, ForAllTyFlag
    vis1, ForAllTyFlag
    vis2, Coercion
    kind_co
                , Coercion -> Coercion -> Coercion
    mkInstCo Coercion
    co (Role -> Coercion -> Coercion -> Coercion -> Coercion
    mkProofIrrelCo Role
    Nominal Coercion
    kind_co Coercion
    l_co Coercion
    r_co))

      | Bool
    otherwise
      = Maybe (CoVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion)
    forall a. Maybe a
    Nothing

    etaAppCo_maybe :: Coercion -> Maybe (Coercion,Coercion)
    -- If possible, split a coercion
    --   g :: t1a t1b ~ t2a t2b
    -- into a pair of coercions (left g, right g)
    etaAppCo_maybe :: Coercion -> Maybe (Coercion, Coercion)
    etaAppCo_maybe Coercion
    co
      | Just (Coercion
    co1,Coercion
    co2) <- Coercion -> Maybe (Coercion, Coercion)
    splitAppCo_maybe Coercion
    co
      = (Coercion, Coercion) -> Maybe (Coercion, Coercion)
    forall a. a -> Maybe a
    Just (Coercion
    co1,Coercion
    co2)
      | (Pair Type
    ty1 Type
    ty2, Role
    Nominal) <- Coercion -> (Pair Type, Role)
    coercionKindRole Coercion
    co
      , Just (Type
    _,Type
    t1) <- Type -> Maybe (Type, Type)
    splitAppTy_maybe Type
    ty1
      , Just (Type
    _,Type
    t2) <- Type -> Maybe (Type, Type)
    splitAppTy_maybe Type
    ty2
      , let isco1 :: Bool
    isco1 = Type -> Bool
    isCoercionTy Type
    t1
      , let isco2 :: Bool
    isco2 = Type -> Bool
    isCoercionTy Type
    t2
      , Bool
    isco1 Bool -> Bool -> Bool
    forall a. Eq a => a -> a -> Bool
    == Bool
    isco2
      = (Coercion, Coercion) -> Maybe (Coercion, Coercion)
    forall a. a -> Maybe a
    Just (LeftOrRight -> Coercion -> Coercion
    LRCo LeftOrRight
    CLeft Coercion
    co, LeftOrRight -> Coercion -> Coercion
    LRCo LeftOrRight
    CRight Coercion
    co)
      | Bool
    otherwise
      = Maybe (Coercion, Coercion)
    forall a. Maybe a
    Nothing

    etaTyConAppCo_maybe :: TyCon -> Coercion -> Maybe [Coercion]
    -- If possible, split a coercion
    --       g :: T s1 .. sn ~ T t1 .. tn
    -- into [ SelCo (SelTyCon 0)     g :: s1~t1
    --      , ...
    --      , SelCo (SelTyCon (n-1)) g :: sn~tn ]
    etaTyConAppCo_maybe :: TyCon -> Coercion -> Maybe [Coercion]
    etaTyConAppCo_maybe TyCon
    tc (TyConAppCo Role
    _ TyCon
    tc2 [Coercion]
    cos2)
      = Bool -> Maybe [Coercion] -> Maybe [Coercion]
    forall a. HasCallStack => Bool -> a -> a
    assert (TyCon
    tc TyCon -> TyCon -> Bool
    forall a. Eq a => a -> a -> Bool
    == TyCon
    tc2) (Maybe [Coercion] -> Maybe [Coercion])
    -> Maybe [Coercion] -> Maybe [Coercion]
    forall a b. (a -> b) -> a -> b
    $ [Coercion] -> Maybe [Coercion]
    forall a. a -> Maybe a
    Just [Coercion]
    cos2

    etaTyConAppCo_maybe TyCon
    tc Coercion
    co
      | Bool -> Bool
    not (TyCon -> Bool
    tyConMustBeSaturated TyCon
    tc)
      , (Pair Type
    ty1 Type
    ty2, Role
    r) <- Coercion -> (Pair Type, Role)
    coercionKindRole Coercion
    co
      , Just (TyCon
    tc1, [Type]
    tys1)  <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
    Type -> Maybe (TyCon, [Type])
    splitTyConApp_maybe Type
    ty1
      , Just (TyCon
    tc2, [Type]
    tys2)  <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
    Type -> Maybe (TyCon, [Type])
    splitTyConApp_maybe Type
    ty2
      , TyCon
    tc1 TyCon -> TyCon -> Bool
    forall a. Eq a => a -> a -> Bool
    == TyCon
    tc2
      , TyCon -> Role -> Bool
    isInjectiveTyCon TyCon
    tc Role
    r  -- See Note [SelCo and newtypes] in GHC.Core.TyCo.Rep
      , let n :: Int
    n = [Type] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Type]
    tys1
      , [Type]
    tys2 [Type] -> Int -> Bool
    forall a. [a] -> Int -> Bool
    `lengthIs` Int
    n      -- This can fail in an erroneous program
                               -- E.g. T a ~# T a b
                               -- #14607
      = Bool -> Maybe [Coercion] -> Maybe [Coercion]
    forall a. HasCallStack => Bool -> a -> a
    assert (TyCon
    tc TyCon -> TyCon -> Bool
    forall a. Eq a => a -> a -> Bool
    == TyCon
    tc1) (Maybe [Coercion] -> Maybe [Coercion])
    -> Maybe [Coercion] -> Maybe [Coercion]
    forall a b. (a -> b) -> a -> b
    $
        [Coercion] -> Maybe [Coercion]
    forall a. a -> Maybe a
    Just (Int -> Coercion -> Infinite Role -> [Coercion]
    decomposeCo Int
    n Coercion
    co (Role -> TyCon -> Infinite Role
    tyConRolesX Role
    r TyCon
    tc1))
        -- NB: n might be <> tyConArity tc
        -- e.g.   data family T a :: * -> *
        --        g :: T a b ~ T c d

      | Bool
    otherwise
      = Maybe [Coercion]
    forall a. Maybe a
    Nothing

    {-
    Note [Eta for AppCo]
    ~~~~~~~~~~~~~~~~~~~~
    Suppose we have
       g :: s1 t1 ~ s2 t2

    Then we can't necessarily make
       left  g :: s1 ~ s2
       right g :: t1 ~ t2
    because it's possible that
       s1 :: * -> *         t1 :: *
       s2 :: (*->*) -> *    t2 :: * -> *
    and in that case (left g) does not have the same
    kind on either side.

    It's enough to check that
      kind t1 = kind t2
    because if g is well-kinded then
      kind (s1 t2) = kind (s2 t2)
    and these two imply
      kind s1 = kind s2

    -}

    optForAllCoBndr :: LiftingContext -> SwapFlag
                    -> TyCoVar -> Coercion -> (LiftingContext, TyCoVar, Coercion)
    optForAllCoBndr :: LiftingContext
    -> SwapFlag
    -> CoVar
    -> Coercion
    -> (LiftingContext, CoVar, Coercion)
    optForAllCoBndr LiftingContext
    env SwapFlag
    sym
      = SwapFlag
    -> (Coercion -> Coercion)
    -> LiftingContext
    -> CoVar
    -> Coercion
    -> (LiftingContext, CoVar, Coercion)
    substForAllCoBndrUsingLC SwapFlag
    sym (LiftingContext -> SwapFlag -> Bool -> Role -> Coercion -> Coercion
    opt_co4 LiftingContext
    env SwapFlag
    sym Bool
    False Role
    Nominal) LiftingContext
    env

    {- **********************************************************************
    %*                                                                      *
           Assertion-checking versions of functions in Coercion.hs
    %*                                                                      *
    %********************************************************************* -}

    -- We can't check the assertions in the "main" functions of these
    -- functions, because the assertions don't hold during zonking.
    -- But they are fantastically helpful in finding bugs in the coercion
    -- optimiser itself, so I have copied them here with assertions.

    mk_trans_co :: HasDebugCallStack => Coercion -> Coercion -> Coercion
    -- Do assertion checking in mk_trans_co
    mk_trans_co :: HasDebugCallStack => Coercion -> Coercion -> Coercion
    mk_trans_co Coercion
    co1 Coercion
    co2
      = Bool -> SDoc -> Coercion -> Coercion
    forall a. HasCallStack => Bool -> SDoc -> a -> a
    assertPpr (HasDebugCallStack => Coercion -> Type
    Coercion -> Type
    coercionRKind Coercion
    co1 HasCallStack => Type -> Type -> Bool
    Type -> Type -> Bool
    `eqType` HasDebugCallStack => Coercion -> Type
    Coercion -> Type
    coercionLKind Coercion
    co2)
                  ([SDoc] -> SDoc
    forall doc. IsDoc doc => [doc] -> doc
    vcat [ String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "co1" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> Coercion -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Coercion
    co1
                        , String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "co2" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> Coercion -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Coercion
    co2
                        , String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "co1 kind" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> Pair Type -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr (HasDebugCallStack => Coercion -> Pair Type
    Coercion -> Pair Type
    coercionKind Coercion
    co1)
                        , String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "co2 kind" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> Pair Type -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr (HasDebugCallStack => Coercion -> Pair Type
    Coercion -> Pair Type
    coercionKind Coercion
    co2)
                        , SDoc
    HasCallStack => SDoc
    callStackDoc ]) (Coercion -> Coercion) -> Coercion -> Coercion
    forall a b. (a -> b) -> a -> b
    $
        HasDebugCallStack => Coercion -> Coercion -> Coercion
    Coercion -> Coercion -> Coercion
    mkTransCo Coercion
    co1 Coercion
    co2

    mk_coherence_right_co :: HasDebugCallStack => Role -> Type -> CoercionN -> Coercion -> Coercion
    mk_coherence_right_co :: HasDebugCallStack =>
    Role -> Type -> Coercion -> Coercion -> Coercion
    mk_coherence_right_co Role
    r Type
    ty Coercion
    co Coercion
    co2
      = Type -> Coercion -> Coercion -> Coercion
    forall r. HasDebugCallStack => Type -> Coercion -> r -> r
    assertGRefl Type
    ty Coercion
    co (Coercion -> Coercion) -> Coercion -> Coercion
    forall a b. (a -> b) -> a -> b
    $
        HasDebugCallStack =>
    Role -> Type -> Coercion -> Coercion -> Coercion
    Role -> Type -> Coercion -> Coercion -> Coercion
    mkCoherenceRightCo Role
    r Type
    ty Coercion
    co Coercion
    co2

    assertGRefl :: HasDebugCallStack => Type -> Coercion -> r -> r
    assertGRefl :: forall r. HasDebugCallStack => Type -> Coercion -> r -> r
    assertGRefl Type
    ty Coercion
    co r
    res
      = Bool -> SDoc -> r -> r
    forall a. HasCallStack => Bool -> SDoc -> a -> a
    assertPpr (HasDebugCallStack => Type -> Type
    Type -> Type
    typeKind Type
    ty HasCallStack => Type -> Type -> Bool
    Type -> Type -> Bool
    `eqType` HasDebugCallStack => Coercion -> Type
    Coercion -> Type
    coercionLKind Coercion
    co)
                  ([SDoc] -> SDoc
    forall doc. IsDoc doc => [doc] -> doc
    vcat [ String -> Type -> SDoc
    pp_ty String
    "ty" Type
    ty
                        , String -> Coercion -> SDoc
    pp_co String
    "co" Coercion
    co
                        , SDoc
    HasCallStack => SDoc
    callStackDoc ]) (r -> r) -> r -> r
    forall a b. (a -> b) -> a -> b
    $
        r
    res

    mk_grefl_right_co :: Role -> Type -> CoercionN -> Coercion
    mk_grefl_right_co :: Role -> Type -> Coercion -> Coercion
    mk_grefl_right_co Role
    r Type
    ty Coercion
    co
      = Type -> Coercion -> Coercion -> Coercion
    forall r. HasDebugCallStack => Type -> Coercion -> r -> r
    assertGRefl Type
    ty Coercion
    co (Coercion -> Coercion) -> Coercion -> Coercion
    forall a b. (a -> b) -> a -> b
    $
        Role -> Type -> Coercion -> Coercion
    mkGReflRightCo Role
    r Type
    ty Coercion
    co

    pp_co :: String -> Coercion -> SDoc
    pp_co :: String -> Coercion -> SDoc
    pp_co String
    s Coercion
    co = String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    s SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> SDoc -> Int -> SDoc -> SDoc
    hang (Coercion -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Coercion
    co) Int
    2 (SDoc
    dcolon SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> Pair Type -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr (HasDebugCallStack => Coercion -> Pair Type
    Coercion -> Pair Type
    coercionKind Coercion
    co))

    pp_ty :: String -> Type -> SDoc
    pp_ty :: String -> Type -> SDoc
    pp_ty String
    s Type
    ty = String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    s SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> SDoc -> Int -> SDoc -> SDoc
    hang (Type -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Type
    ty) Int
    2 (SDoc
    dcolon SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> Type -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr (HasDebugCallStack => Type -> Type
    Type -> Type
    typeKind Type
    ty))