    module GHC.Core.Reduction
      (
         -- * Reductions
         Reduction(..), ReductionN, ReductionR, HetReduction(..),
         Reductions(..),
         mkReduction, mkReductions, mkHetReduction, coercionRedn,
         reductionOriginalType,
         downgradeRedn, mkSubRedn,
         mkTransRedn, mkCoherenceRightRedn, mkCoherenceRightMRedn,
         mkCastRedn1, mkCastRedn2,
         mkReflRedn, mkGReflRightRedn, mkGReflRightMRedn,
         mkGReflLeftRedn, mkGReflLeftMRedn,
         mkAppRedn, mkAppRedns, mkFunRedn,
         mkForAllRedn, mkHomoForAllRedn, mkTyConAppRedn, mkClassPredRedn,
         mkProofIrrelRedn, mkReflCoRedn,
         homogeniseHetRedn,
         unzipRedns,

         -- * Rewriting type arguments
         ArgsReductions(..),
         simplifyArgsWorker

      ) where

    import GHC.Prelude

    import GHC.Core.Class      ( Class(classTyCon) )
    import GHC.Core.Coercion
    import GHC.Core.Predicate  ( mkClassPred )
    import GHC.Core.TyCon      ( TyCon )
    import GHC.Core.Type

    import GHC.Data.Pair       ( Pair(Pair) )
    import GHC.Data.List.Infinite ( Infinite (..) )
    import qualified GHC.Data.List.Infinite as Inf

    import GHC.Types.Var       ( VarBndr(..), setTyVarKind )
    import GHC.Types.Var.Env   ( mkInScopeSet )
    import GHC.Types.Var.Set   ( TyCoVarSet )

    import GHC.Utils.Misc      ( HasDebugCallStack, equalLength )
    import GHC.Utils.Outputable
    import GHC.Utils.Panic     ( assertPpr )

    {-
    %************************************************************************
    %*                                                                      *
          Reductions
    %*                                                                      *
    %************************************************************************

    Note [The Reduction type]
    ~~~~~~~~~~~~~~~~~~~~~~~~~
    Many functions in the type-checker rewrite a type, using Given type equalitie
    or type-family reductions, and return a Reduction, which is just a pair of the
    coercion and the RHS type of the coercion:
      data Reduction = Reduction Coercion !Type

    The order of the arguments to the constructor serves as a reminder
    of what the Type is.  In
        Reduction co ty
    `ty` appears to the right of `co`, reminding us that we must have:
        co :: unrewritten_ty ~ ty

    Example functions that use this datatype:
       GHC.Core.FamInstEnv.topNormaliseType_maybe
         :: FamInstEnvs -> Type -> Maybe Reduction
       GHC.Tc.Solver.Rewrite.rewrite
         :: CtEvidence -> TcType -> TcS Reduction

    Having Reduction as a data type, with a strict Type field, rather than using
    a pair (Coercion,Type) gives several advantages (see #20161)
    * The strictness in Type improved performance in rewriting of type families
      (around 2.5% improvement in T9872),
    * Compared to the situation before, it gives improved consistency around
      orientation of rewritings, as a Reduction is always left-to-right
      (the coercion's RHS type is always the type stored in the 'Reduction').
      No more 'mkSymCo's needed to convert between left-to-right and right-to-left.

    One could imagine storing the LHS type of the coercion in the Reduction as well,
    but in fact `reductionOriginalType` is very seldom used, so it's not worth it.
    -}

    -- | A 'Reduction' is the result of an operation that rewrites a type @ty_in@.
    -- The 'Reduction' includes the rewritten type @ty_out@ and a 'Coercion' @co@
    -- such that @co :: ty_in ~ ty_out@, where the role of the coercion is determined
    -- by the context. That is, the LHS type of the coercion is the original type
    -- @ty_in@, while its RHS type is the rewritten type @ty_out@.
    --
    -- A Reduction is always homogeneous, unless it is wrapped inside a 'HetReduction',
    -- which separately stores the kind coercion.
    --
    -- See Note [The Reduction type].
    data Reduction =
      Reduction
        { Reduction -> Coercion
    reductionCoercion    :: Coercion
        , Reduction -> Type
    reductionReducedType :: !Type
        }
    -- N.B. the 'Coercion' field must be lazy: see for instance GHC.Tc.Solver.Rewrite.rewrite_tyvar2
    -- which returns an error in the 'Coercion' field when dealing with a Derived constraint
    -- (which is OK as this Coercion gets ignored later).
    -- We might want to revisit the strictness once Deriveds are removed.

    -- | Stores a heterogeneous reduction.
    --
    -- The stored kind coercion must relate the kinds of the
    -- stored reduction. That is, in @HetReduction (Reduction co xi) kco@,
    -- we must have:
    --
    -- >  co :: ty ~ xi
    -- > kco :: typeKind ty ~ typeKind xi
    data HetReduction =
      HetReduction
        Reduction
        MCoercionN
      -- N.B. strictness annotations don't seem to make a difference here

    -- | Create a heterogeneous reduction.
    --
    -- Pre-condition: the provided kind coercion (second argument)
    -- relates the kinds of the stored reduction.
    -- That is, if the coercion stored in the 'Reduction' is of the form
    --
    -- > co :: ty ~ xi
    --
    -- Then the kind coercion supplied must be of the form:
    --
    -- > kco :: typeKind ty ~ typeKind xi
    mkHetReduction :: Reduction  -- ^ heterogeneous reduction
                   -> MCoercionN -- ^ kind coercion
                   -> HetReduction
    mkHetReduction :: Reduction -> MCoercionN -> HetReduction
    mkHetReduction Reduction
    redn MCoercionN
    mco = Reduction -> MCoercionN -> HetReduction
    HetReduction Reduction
    redn MCoercionN
    mco
    {-# INLINE mkHetReduction #-}

    -- | Homogenise a heterogeneous reduction.
    --
    -- Given @HetReduction (Reduction co xi) kco@, with
    --
    -- >  co :: ty ~ xi
    -- > kco :: typeKind(ty) ~ typeKind(xi)
    --
    -- this returns the homogeneous reduction:
    --
    -- > hco :: ty ~ ( xi |> sym kco )
    homogeniseHetRedn :: Role -> HetReduction -> Reduction
    homogeniseHetRedn :: Role -> HetReduction -> Reduction
    homogeniseHetRedn Role
    role (HetReduction Reduction
    redn MCoercionN
    kco)
      = Role -> Reduction -> MCoercionN -> Reduction
    mkCoherenceRightMRedn Role
    role Reduction
    redn (MCoercionN -> MCoercionN
    mkSymMCo MCoercionN
    kco)
    {-# INLINE homogeniseHetRedn #-}

    -- | Create a 'Reduction' from a pair of a 'Coercion' and a 'Type.
    --
    -- Pre-condition: the RHS type of the coercion matches the provided type
    -- (perhaps up to zonking).
    --
    -- Use 'coercionRedn' when you only have the coercion.
    mkReduction :: Coercion -> Type -> Reduction
    mkReduction :: Coercion -> Type -> Reduction
    mkReduction Coercion
    co Type
    ty = Coercion -> Type -> Reduction
    Reduction Coercion
    co Type
    ty
    {-# INLINE mkReduction #-}

    instance Outputable Reduction where
      ppr :: Reduction -> SDoc
    ppr Reduction
    redn =
        SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc
    braces (SDoc -> SDoc) -> SDoc -> SDoc
    forall a b. (a -> b) -> a -> b
    $ [SDoc] -> SDoc
    forall doc. IsDoc doc => [doc] -> doc
    vcat
          [ String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "reductionOriginalType:" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> Type -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr (Reduction -> Type
    reductionOriginalType Reduction
    redn)
          , String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    " reductionReducedType:" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> Type -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr (Reduction -> Type
    reductionReducedType Reduction
    redn)
          , String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "    reductionCoercion:" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> Coercion -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr (Reduction -> Coercion
    reductionCoercion Reduction
    redn)
          ]

    -- | A 'Reduction' in which the 'Coercion' has 'Nominal' role.
    type ReductionN = Reduction

    -- | A 'Reduction' in which the 'Coercion' has 'Representational' role.
    type ReductionR = Reduction

    -- | Get the original, unreduced type corresponding to a 'Reduction'.
    --
    -- This is obtained by computing the LHS kind of the stored coercion,
    -- which may be slow.
    reductionOriginalType :: Reduction -> Type
    reductionOriginalType :: Reduction -> Type
    reductionOriginalType = HasDebugCallStack => Coercion -> Type
    Coercion -> Type
    coercionLKind (Coercion -> Type) -> (Reduction -> Coercion) -> Reduction -> Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Reduction -> Coercion
    reductionCoercion
    {-# INLINE reductionOriginalType #-}

    -- | Turn a 'Coercion' into a 'Reduction'
    -- by inspecting the RHS type of the coercion.
    --
    -- Prefer using 'mkReduction' when you already know
    -- the RHS type of the coercion, to avoid computing it anew.
    coercionRedn :: Coercion -> Reduction
    coercionRedn :: Coercion -> Reduction
    coercionRedn Coercion
    co = Coercion -> Type -> Reduction
    Reduction Coercion
    co (HasDebugCallStack => Coercion -> Type
    Coercion -> Type
    coercionRKind Coercion
    co)
    {-# INLINE coercionRedn #-}

    -- | Downgrade the role of the coercion stored in the 'Reduction'.
    downgradeRedn :: Role -- ^ desired role
                  -> Role -- ^ current role
                  -> Reduction
                  -> Reduction
    downgradeRedn :: Role -> Role -> Reduction -> Reduction
    downgradeRedn Role
    new_role Role
    old_role redn :: Reduction
    redn@(Reduction Coercion
    co Type
    _)
      = Reduction
    redn { reductionCoercion = downgradeRole new_role old_role co }
    {-# INLINE downgradeRedn #-}

    -- | Downgrade the role of the coercion stored in the 'Reduction',
    -- from 'Nominal' to 'Representational'.
    mkSubRedn :: Reduction -> Reduction
    mkSubRedn :: Reduction -> Reduction
    mkSubRedn redn :: Reduction
    redn@(Reduction Coercion
    co Type
    _) = Reduction
    redn { reductionCoercion = mkSubCo co }
    {-# INLINE mkSubRedn #-}

    -- | Compose a reduction with a coercion on the left.
    --
    -- Pre-condition: the provided coercion's RHS type must match the LHS type
    -- of the coercion that is stored in the reduction.
    mkTransRedn :: Coercion -> Reduction -> Reduction
    mkTransRedn :: Coercion -> Reduction -> Reduction
    mkTransRedn Coercion
    co1 redn :: Reduction
    redn@(Reduction Coercion
    co2 Type
    _)
      = Reduction
    redn { reductionCoercion = co1 `mkTransCo` co2 }
    {-# INLINE mkTransRedn #-}

    -- | The reflexive reduction.
    mkReflRedn :: Role -> Type -> Reduction
    mkReflRedn :: Role -> Type -> Reduction
    mkReflRedn Role
    r Type
    ty = Coercion -> Type -> Reduction
    mkReduction (Role -> Type -> Coercion
    mkReflCo Role
    r Type
    ty) Type
    ty

    -- | Create a 'Reduction' from a kind cast, in which
    -- the casted type is the rewritten type.
    --
    -- Given @ty :: k1@, @mco :: k1 ~ k2@,
    -- produces the 'Reduction' @ty ~res_co~> (ty |> mco)@
    -- at the given 'Role'.
    mkGReflRightRedn :: Role -> Type -> CoercionN -> Reduction
    mkGReflRightRedn :: Role -> Type -> Coercion -> Reduction
    mkGReflRightRedn Role
    role Type
    ty Coercion
    co
      = Coercion -> Type -> Reduction
    mkReduction
          (Role -> Type -> Coercion -> Coercion
    mkGReflRightCo Role
    role Type
    ty Coercion
    co)
          (Type -> Coercion -> Type
    mkCastTy Type
    ty Coercion
    co)
    {-# INLINE mkGReflRightRedn #-}

    -- | Create a 'Reduction' from a kind cast, in which
    -- the casted type is the rewritten type.
    --
    -- Given @ty :: k1@, @mco :: k1 ~ k2@,
    -- produces the 'Reduction' @ty ~res_co~> (ty |> mco)@
    -- at the given 'Role'.
    mkGReflRightMRedn :: Role -> Type -> MCoercionN -> Reduction
    mkGReflRightMRedn :: Role -> Type -> MCoercionN -> Reduction
    mkGReflRightMRedn Role
    role Type
    ty MCoercionN
    mco
      = Coercion -> Type -> Reduction
    mkReduction
          (Role -> Type -> MCoercionN -> Coercion
    mkGReflRightMCo Role
    role Type
    ty MCoercionN
    mco)
          (Type -> MCoercionN -> Type
    mkCastTyMCo Type
    ty MCoercionN
    mco)
    {-# INLINE mkGReflRightMRedn #-}

    -- | Create a 'Reduction' from a kind cast, in which
    -- the casted type is the original (non-rewritten) type.
    --
    -- Given @ty :: k1@, @mco :: k1 ~ k2@,
    -- produces the 'Reduction' @(ty |> mco) ~res_co~> ty@
    -- at the given 'Role'.
    mkGReflLeftRedn :: Role -> Type -> CoercionN -> Reduction
    mkGReflLeftRedn :: Role -> Type -> Coercion -> Reduction
    mkGReflLeftRedn Role
    role Type
    ty Coercion
    co
      = Coercion -> Type -> Reduction
    mkReduction
          (Role -> Type -> Coercion -> Coercion
    mkGReflLeftCo Role
    role Type
    ty Coercion
    co)
          Type
    ty
    {-# INLINE mkGReflLeftRedn #-}

    -- | Create a 'Reduction' from a kind cast, in which
    -- the casted type is the original (non-rewritten) type.
    --
    -- Given @ty :: k1@, @mco :: k1 ~ k2@,
    -- produces the 'Reduction' @(ty |> mco) ~res_co~> ty@
    -- at the given 'Role'.
    mkGReflLeftMRedn :: Role -> Type -> MCoercionN -> Reduction
    mkGReflLeftMRedn :: Role -> Type -> MCoercionN -> Reduction
    mkGReflLeftMRedn Role
    role Type
    ty MCoercionN
    mco
      = Coercion -> Type -> Reduction
    mkReduction
          (Role -> Type -> MCoercionN -> Coercion
    mkGReflLeftMCo Role
    role Type
    ty MCoercionN
    mco)
          Type
    ty
    {-# INLINE mkGReflLeftMRedn #-}

    -- | Apply a cast to the result of a 'Reduction'.
    --
    -- Given a 'Reduction' @ty1 ~co1~> (ty2 :: k2)@ and a kind coercion @kco@
    -- with LHS kind @k2@, produce a new 'Reduction' @ty1 ~co2~> ( ty2 |> kco )@
    -- of the given 'Role' (which must match the role of the coercion stored
    -- in the 'Reduction' argument).
    mkCoherenceRightRedn :: Role -> Reduction -> CoercionN -> Reduction
    mkCoherenceRightRedn :: Role -> Reduction -> Coercion -> Reduction
    mkCoherenceRightRedn Role
    r (Reduction Coercion
    co1 Type
    ty2) Coercion
    kco
      = Coercion -> Type -> Reduction
    mkReduction
          (HasDebugCallStack =>
    Role -> Type -> Coercion -> Coercion -> Coercion
    Role -> Type -> Coercion -> Coercion -> Coercion
    mkCoherenceRightCo Role
    r Type
    ty2 Coercion
    kco Coercion
    co1)
          (Type -> Coercion -> Type
    mkCastTy Type
    ty2 Coercion
    kco)
    {-# INLINE mkCoherenceRightRedn #-}

    -- | Apply a cast to the result of a 'Reduction', using an 'MCoercionN'.
    --
    -- Given a 'Reduction' @ty1 ~co1~> (ty2 :: k2)@ and a kind coercion @mco@
    -- with LHS kind @k2@, produce a new 'Reduction' @ty1 ~co2~> ( ty2 |> mco )@
    -- of the given 'Role' (which must match the role of the coercion stored
    -- in the 'Reduction' argument).
    mkCoherenceRightMRedn :: Role -> Reduction -> MCoercionN -> Reduction
    mkCoherenceRightMRedn :: Role -> Reduction -> MCoercionN -> Reduction
    mkCoherenceRightMRedn Role
    r (Reduction Coercion
    co1 Type
    ty2) MCoercionN
    kco
      = Coercion -> Type -> Reduction
    mkReduction
          (Role -> Type -> MCoercionN -> Coercion -> Coercion
    mkCoherenceRightMCo Role
    r Type
    ty2 MCoercionN
    kco Coercion
    co1)
          (Type -> MCoercionN -> Type
    mkCastTyMCo Type
    ty2 MCoercionN
    kco)
    {-# INLINE mkCoherenceRightMRedn #-}

    -- | Apply a cast to a 'Reduction', casting both the original and the reduced type.
    --
    -- Given @cast_co@ and 'Reduction' @ty ~co~> xi@, this function returns
    -- the 'Reduction' @(ty |> cast_co) ~return_co~> (xi |> cast_co)@
    -- of the given 'Role' (which must match the role of the coercion stored
    -- in the 'Reduction' argument).
    --
    -- Pre-condition: the 'Type' passed in is the same as the LHS type
    -- of the coercion stored in the 'Reduction'.
    mkCastRedn1 :: Role
                -> Type      -- ^ original type
                -> CoercionN -- ^ coercion to cast with
                -> Reduction -- ^ rewritten type, with rewriting coercion
                -> Reduction
    mkCastRedn1 :: Role -> Type -> Coercion -> Reduction -> Reduction
    mkCastRedn1 Role
    r Type
    ty Coercion
    cast_co (Reduction Coercion
    co Type
    xi)
      -- co :: ty ~r ty'
      -- return_co :: (ty |> cast_co) ~r (ty' |> cast_co)
      = Coercion -> Type -> Reduction
    mkReduction
          (Coercion -> Role -> Type -> Type -> Coercion -> Coercion
    castCoercionKind1 Coercion
    co Role
    r Type
    ty Type
    xi Coercion
    cast_co)
          (Type -> Coercion -> Type
    mkCastTy Type
    xi Coercion
    cast_co)
    {-# INLINE mkCastRedn1 #-}

    -- | Apply casts on both sides of a 'Reduction' (of the given 'Role').
    --
    -- Use 'mkCastRedn1' when you want to cast both the original and reduced types
    -- in a 'Reduction' using the same coercion.
    --
    -- Pre-condition: the 'Type' passed in is the same as the LHS type
    -- of the coercion stored in the 'Reduction'.
    mkCastRedn2 :: Role
                -> Type      -- ^ original type
                -> CoercionN -- ^ coercion to cast with on the left
                -> Reduction -- ^ rewritten type, with rewriting coercion
                -> CoercionN -- ^ coercion to cast with on the right
                -> Reduction
    mkCastRedn2 :: Role -> Type -> Coercion -> Reduction -> Coercion -> Reduction
    mkCastRedn2 Role
    r Type
    ty Coercion
    cast_co (Reduction Coercion
    nco Type
    nty) Coercion
    cast_co'
      = Coercion -> Type -> Reduction
    mkReduction
          (Coercion
    -> Role -> Type -> Type -> Coercion -> Coercion -> Coercion
    castCoercionKind2 Coercion
    nco Role
    r Type
    ty Type
    nty Coercion
    cast_co Coercion
    cast_co')
          (Type -> Coercion -> Type
    mkCastTy Type
    nty Coercion
    cast_co')
    {-# INLINE mkCastRedn2 #-}

    -- | Apply one 'Reduction' to another.
    --
    -- Combines 'mkAppCo' and 'mkAppTy`.
    mkAppRedn :: Reduction -> Reduction -> Reduction
    mkAppRedn :: Reduction -> Reduction -> Reduction
    mkAppRedn (Reduction Coercion
    co1 Type
    ty1) (Reduction Coercion
    co2 Type
    ty2)
      = Coercion -> Type -> Reduction
    mkReduction (Coercion -> Coercion -> Coercion
    mkAppCo Coercion
    co1 Coercion
    co2) (Type -> Type -> Type
    mkAppTy Type
    ty1 Type
    ty2)
    {-# INLINE mkAppRedn #-}

    -- | Create a function 'Reduction'.
    --
    -- Combines 'mkFunCo' and 'mkFunTy'.
    mkFunRedn :: Role
              -> FunTyFlag
              -> ReductionN -- ^ multiplicity reduction
              -> Reduction  -- ^ argument reduction
              -> Reduction  -- ^ result reduction
              -> Reduction
    mkFunRedn :: Role
    -> FunTyFlag -> Reduction -> Reduction -> Reduction -> Reduction
    mkFunRedn Role
    r FunTyFlag
    af
      (Reduction Coercion
    w_co Type
    w_ty)
      (Reduction Coercion
    arg_co Type
    arg_ty)
      (Reduction Coercion
    res_co Type
    res_ty)
        = Coercion -> Type -> Reduction
    mkReduction
            (Role -> FunTyFlag -> Coercion -> Coercion -> Coercion -> Coercion
    mkFunCo Role
    r FunTyFlag
    af Coercion
    w_co Coercion
    arg_co Coercion
    res_co)
            (HasDebugCallStack => FunTyFlag -> Type -> Type -> Type -> Type
    FunTyFlag -> Type -> Type -> Type -> Type
    mkFunTy   FunTyFlag
    af Type
    w_ty Type
    arg_ty Type
    res_ty)
    {-# INLINE mkFunRedn #-}

    -- | Create a 'Reduction' associated to a Π type,
    -- from a kind 'Reduction' and a body 'Reduction'.
    --
    -- Combines 'mkForAllCo' and 'mkForAllTy'.
    mkForAllRedn :: ForAllTyFlag
                 -> TyVar
                 -> ReductionN -- ^ kind reduction
                 -> Reduction  -- ^ body reduction
                 -> Reduction
    mkForAllRedn :: ForAllTyFlag -> TyVar -> Reduction -> Reduction -> Reduction
    mkForAllRedn ForAllTyFlag
    vis TyVar
    tv1 (Reduction Coercion
    h Type
    ki') (Reduction Coercion
    co Type
    ty)
      = Coercion -> Type -> Reduction
    mkReduction
          (HasDebugCallStack =>
    TyVar
    -> ForAllTyFlag -> ForAllTyFlag -> Coercion -> Coercion -> Coercion
    TyVar
    -> ForAllTyFlag -> ForAllTyFlag -> Coercion -> Coercion -> Coercion
    mkForAllCo TyVar
    tv1 ForAllTyFlag
    vis ForAllTyFlag
    vis Coercion
    h Coercion
    co)
          (ForAllTyBinder -> Type -> Type
    mkForAllTy (TyVar -> ForAllTyFlag -> ForAllTyBinder
    forall var argf. var -> argf -> VarBndr var argf
    Bndr TyVar
    tv2 ForAllTyFlag
    vis) Type
    ty)
      where
        tv2 :: TyVar
    tv2 = TyVar -> Type -> TyVar
    setTyVarKind TyVar
    tv1 Type
    ki'
    {-# INLINE mkForAllRedn #-}

    -- | Create a 'Reduction' of a quantified type from a
    -- 'Reduction' of the body.
    --
    -- Combines 'mkHomoForAllCos' and 'mkForAllTys'.
    mkHomoForAllRedn :: [TyVarBinder] -> Reduction -> Reduction
    mkHomoForAllRedn :: [ForAllTyBinder] -> Reduction -> Reduction
    mkHomoForAllRedn [ForAllTyBinder]
    bndrs (Reduction Coercion
    co Type
    ty)
      = Coercion -> Type -> Reduction
    mkReduction
          ([ForAllTyBinder] -> Coercion -> Coercion
    mkHomoForAllCos [ForAllTyBinder]
    bndrs Coercion
    co)
          ([ForAllTyBinder] -> Type -> Type
    mkForAllTys [ForAllTyBinder]
    bndrs Type
    ty)
    {-# INLINE mkHomoForAllRedn #-}

    -- | Create a 'Reduction' from a coercion between coercions.
    --
    -- Combines 'mkProofIrrelCo' and 'mkCoercionTy'.
    mkProofIrrelRedn :: Role      -- ^ role of the created coercion, "r"
                     -> CoercionN -- ^ co :: phi1 ~N phi2
                     -> Coercion  -- ^ g1 :: phi1
                     -> Coercion  -- ^ g2 :: phi2
                     -> Reduction -- ^ res_co :: g1 ~r g2
    mkProofIrrelRedn :: Role -> Coercion -> Coercion -> Coercion -> Reduction
    mkProofIrrelRedn Role
    role Coercion
    co Coercion
    g1 Coercion
    g2
      = Coercion -> Type -> Reduction
    mkReduction
          (Role -> Coercion -> Coercion -> Coercion -> Coercion
    mkProofIrrelCo Role
    role Coercion
    co Coercion
    g1 Coercion
    g2)
          (Coercion -> Type
    mkCoercionTy Coercion
    g2)
    {-# INLINE mkProofIrrelRedn #-}

    -- | Create a reflexive 'Reduction' whose RHS is the given 'Coercion',
    -- with the specified 'Role'.
    mkReflCoRedn :: Role -> Coercion -> Reduction
    mkReflCoRedn :: Role -> Coercion -> Reduction
    mkReflCoRedn Role
    role Coercion
    co
      = Coercion -> Type -> Reduction
    mkReduction
          (Role -> Type -> Coercion
    mkReflCo Role
    role Type
    co_ty)
          Type
    co_ty
      where
        co_ty :: Type
    co_ty = Coercion -> Type
    mkCoercionTy Coercion
    co
    {-# INLINE mkReflCoRedn #-}

    -- | A collection of 'Reduction's where the coercions and the types are stored separately.
    --
    -- Use 'unzipRedns' to obtain 'Reductions' from a list of 'Reduction's.
    --
    -- This datatype is used in 'mkAppRedns', 'mkClassPredRedns' and 'mkTyConAppRedn',
    -- which expect separate types and coercions.
    --
    -- Invariant: the two stored lists are of the same length,
    -- and the RHS type of each coercion is the corresponding type.
    data Reductions = Reductions [Coercion] [Type]

    -- | Create 'Reductions' from individual lists of coercions and types.
    --
    -- The lists should be of the same length, and the RHS type of each coercion
    -- should match the specified type in the other list.
    mkReductions :: [Coercion] -> [Type] -> Reductions
    mkReductions :: [Coercion] -> [Type] -> Reductions
    mkReductions [Coercion]
    cos [Type]
    tys = [Coercion] -> [Type] -> Reductions
    Reductions [Coercion]
    cos [Type]
    tys
    {-# INLINE mkReductions #-}

    -- | Combines 'mkAppCos' and 'mkAppTys'.
    mkAppRedns :: Reduction -> Reductions -> Reduction
    mkAppRedns :: Reduction -> Reductions -> Reduction
    mkAppRedns (Reduction Coercion
    co Type
    ty) (Reductions [Coercion]
    cos [Type]
    tys)
      = Coercion -> Type -> Reduction
    mkReduction (Coercion -> [Coercion] -> Coercion
    mkAppCos Coercion
    co [Coercion]
    cos) (Type -> [Type] -> Type
    mkAppTys Type
    ty [Type]
    tys)
    {-# INLINE mkAppRedns #-}

    -- | 'TyConAppCo' for 'Reduction's: combines 'mkTyConAppCo' and `mkTyConApp`.
    mkTyConAppRedn :: Role -> TyCon -> Reductions -> Reduction
    mkTyConAppRedn :: Role -> TyCon -> Reductions -> Reduction
    mkTyConAppRedn Role
    role TyCon
    tc (Reductions [Coercion]
    cos [Type]
    tys)
      = Coercion -> Type -> Reduction
    mkReduction (HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
    Role -> TyCon -> [Coercion] -> Coercion
    mkTyConAppCo Role
    role TyCon
    tc [Coercion]
    cos) (TyCon -> [Type] -> Type
    mkTyConApp TyCon
    tc [Type]
    tys)
    {-# INLINE mkTyConAppRedn #-}

    -- | Reduce the arguments of a 'Class' 'TyCon'.
    mkClassPredRedn :: Class -> Reductions -> Reduction
    mkClassPredRedn :: Class -> Reductions -> Reduction
    mkClassPredRedn Class
    cls (Reductions [Coercion]
    cos [Type]
    tys)
      = Coercion -> Type -> Reduction
    mkReduction
          (HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
    Role -> TyCon -> [Coercion] -> Coercion
    mkTyConAppCo Role
    Nominal (Class -> TyCon
    classTyCon Class
    cls) [Coercion]
    cos)
          (Class -> [Type] -> Type
    mkClassPred Class
    cls [Type]
    tys)
    {-# INLINE mkClassPredRedn #-}

    -- | Obtain 'Reductions' from a list of 'Reduction's by unzipping.
    unzipRedns :: [Reduction] -> Reductions
    unzipRedns :: [Reduction] -> Reductions
    unzipRedns = (Reduction -> Reductions -> Reductions)
    -> Reductions -> [Reduction] -> Reductions
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr Reduction -> Reductions -> Reductions
    accRedn ([Coercion] -> [Type] -> Reductions
    Reductions [] [])
      where
        accRedn :: Reduction -> Reductions -> Reductions
        accRedn :: Reduction -> Reductions -> Reductions
    accRedn (Reduction Coercion
    co Type
    xi) (Reductions [Coercion]
    cos [Type]
    xis)
          = [Coercion] -> [Type] -> Reductions
    Reductions (Coercion
    coCoercion -> [Coercion] -> [Coercion]
    forall a. a -> [a] -> [a]
    :[Coercion]
    cos) (Type
    xiType -> [Type] -> [Type]
    forall a. a -> [a] -> [a]
    :[Type]
    xis)
    {-# INLINE unzipRedns #-}
    -- NB: this function is currently used in two locations:
    --
    -- - GHC.Tc.Gen.Foreign.normaliseFfiType', with one call of the form:
    --
    --   unzipRedns <$> zipWithM f tys roles
    --
    -- - GHC.Tc.Solver.Monad.breakTyEqCycle_maybe, with two calls of the form:
    --
    --   unzipRedns <$> mapM f tys
    --
    -- It is possible to write 'mapAndUnzipM' functions to handle these cases,
    -- but the above locations aren't performance critical, so it was deemed
    -- to not be worth it.

    {-
    %************************************************************************
    %*                                                                      *
           Simplifying types
    %*                                                                      *
    %************************************************************************

    The function below morally belongs in GHC.Tc.Solver.Rewrite, but it is used also in
    FamInstEnv, and so lives here.

    Note [simplifyArgsWorker]
    ~~~~~~~~~~~~~~~~~~~~~~~~~
    Invariant (F2) of Note [Rewriting] in GHC.Tc.Solver.Rewrite says that
    rewriting is homogeneous.
    This causes some trouble when rewriting a function applied to a telescope
    of arguments, perhaps with dependency. For example, suppose

      type family F :: forall (j :: Type) (k :: Type). Maybe j -> Either j k -> Bool -> [k]

    and we wish to rewrite the args of (with kind applications explicit)

      F @a @b (Just @a c) (Right @a @b d) False

    where all variables are skolems and

      a :: Type
      b :: Type
      c :: a
      d :: b

      [G] aco :: a ~ fa
      [G] bco :: b ~ fb
      [G] cco :: c ~ fc
      [G] dco :: d ~ fd

    The first step is to rewrite all the arguments. This is done before calling
    simplifyArgsWorker. We start from

      a
      b
      Just @a c
      Right @a @b d
      False

    and get left-to-right reductions whose coercions are as follows:

      co1 :: a ~ fa
      co2 :: b ~ fb
      co3 :: (Just @a c) ~ (Just @fa (fc |> aco) |> co6)
      co4 :: (Right @a @b d) ~ (Right @fa @fb (fd |> bco) |> co7)
      co5 :: False ~ False

    where
      co6 = Maybe (sym aco) :: Maybe fa ~ Maybe a
      co7 = Either (sym aco) (sym bco) :: Either fa fb ~ Either a b

    We now process the rewritten args in left-to-right order. The first two args
    need no further processing. But now consider the third argument. Let f3 = the rewritten
    result, Just fa (fc |> aco) |> co6.
    This f3 rewritten argument has kind (Maybe a), due to homogeneity of rewriting (F2).
    And yet, when we build the application (F @fa @fb ...), we need this
    argument to have kind (Maybe fa), not (Maybe a). We must cast this argument.
    The coercion to use is determined by the kind of F:
    we see in F's kind that the third argument has kind Maybe j.
    Critically, we also know that the argument corresponding to j
    (in our example, a) rewrote with a coercion co1. We can thus know the
    coercion needed for the 3rd argument is (Maybe co1), thus building
    (f3 |> Maybe co1)

    More generally, we must use the Lifting Lemma, as implemented in
    Coercion.liftCoSubst. As we work left-to-right, any variable that is a
    dependent parameter (j and k, in our example) gets mapped in a lifting context
    to the coercion that is output from rewriting the corresponding argument (co1
    and co2, in our example). Then, after rewriting later arguments, we lift the
    kind of these arguments in the lifting context that we've be building up.
    This coercion is then used to keep the result of rewriting well-kinded.

    Working through our example, this is what happens:

      1. Extend the (empty) LC with [j |-> co1]. No new casting must be done,
         because the binder associated with the first argument has a closed type (no
         variables).

      2. Extend the LC with [k |-> co2]. No casting to do.

      3. Lifting the kind (Maybe j) with our LC
         yields co8 :: Maybe a ~ Maybe fa. Use (f3 |> co8) as the argument to F.

      4. Lifting the kind (Either j k) with our LC
         yields co9 :: Either a b ~ Either fa fb. Use (f4 |> co9) as the 4th
         argument to F, where f4 is the rewritten form of argument 4, written above.

      5. We lift Bool with our LC, getting <Bool>; casting has no effect.

    We're now almost done, but the new application

      F @fa @fb (f3 |> co8) (f4 |> co9) False

    has the wrong kind. Its kind is [fb], instead of the original [b].
    So we must use our LC one last time to lift the result kind [k],
    getting res_co :: [fb] ~ [b], and we cast our result.

    Accordingly, the final result is

      F
        @fa
        @fb
        (Just @fa (fc |> aco) |> Maybe (sym aco) |> sym (Maybe (sym aco)))
        (Right @fa @fb (fd |> bco) |> Either (sym aco) (sym bco) |> sym (Either (sym aco) (sym bco)))
        False
      |> [sym bco]

    The res_co (in this case, [sym bco]) is the third component of the
    tuple returned by simplifyArgsWorker.

    Note [Last case in simplifyArgsWorker]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    In writing simplifyArgsWorker's `go`, we know here that args cannot be empty,
    because that case is first. We've run out of
    binders. But perhaps inner_ki is a tyvar that has been instantiated with a
    Π-type.

    Here is an example.

      a :: forall (k :: Type). k -> k
      Proxy :: forall j. j -> Type
      type family Star
      axStar :: Star ~ Type
      type family NoWay :: Bool
      axNoWay :: NoWay ~ False
      bo :: Type
      [G] bc :: bo ~ Bool   (in inert set)

      co :: (forall j. j -> Type) ~ (forall (j :: Star). (j |> axStar) -> Star)
      co = forall (j :: sym axStar). (<j> -> sym axStar)

      We are rewriting:
      a (forall (j :: Star). (j |> axStar) -> Star)   -- 1
        (Proxy |> co)                                 -- 2
        (bo |> sym axStar)                            -- 3
        (NoWay |> sym bc)                             -- 4
          :: Star

    First, we rewrite all the arguments (before simplifyArgsWorker), like so:

        co1 :: (forall (j :: Star). (j |> axStar) -> Star) ~ (forall j. j -> Type) -- 1
        co2 :: (Proxy |> co) ~ (Proxy |> co)                                       -- 2
        co3 :: (bo |> sym axStar) ~ (Bool |> sym axStar)                           -- 3
        co4 :: (NoWay |> sym bc) ~ (False |> sym bc)                               -- 4

    Then we do the process described in Note [simplifyArgsWorker].

    1. Lifting Type (the kind of the first arg) gives us a reflexive coercion, so we
       don't use it. But we do build a lifting context [k -> co1] (where co1 is a
       result of rewriting an argument, written above).

    2. Lifting k gives us co1, so the second argument becomes (Proxy |> co |> co1).
       This is not a dependent argument, so we don't extend the lifting context.

    Now we need to deal with argument (3).
    The way we normally proceed is to lift the kind of the binder, to see whether
    it's dependent.
    But here, the remainder of the kind of `a` that we're left with
    after processing two arguments is just `k`.

    The way forward is look up k in the lifting context, getting co1. If we're at
    all well-typed, co1 will be a coercion between Π-types, with at least one binder.
    So, let's decompose co1 with decomposePiCos. This decomposition needs arguments to use
    to instantiate any kind parameters. Look at the type of co1. If we just
    decomposed it, we would end up with coercions whose types include j, which is
    out of scope here. Accordingly, decomposePiCos takes a list of types whose
    kinds are the *unrewritten* types in the decomposed coercion. (See comments on
    decomposePiCos.) Because the rewritten types have unrewritten kinds (because
    rewriting is homogeneous), passing the list of rewritten types to decomposePiCos
    just won't do: later arguments' kinds won't be as expected. So we need to get
    the *unrewritten* types to pass to decomposePiCos. We can do this easily enough
    by taking the kind of the argument coercions, passed in originally.

    (Alternative 1: We could re-engineer decomposePiCos to deal with this situation.
    But that function is already gnarly, and other call sites of decomposePiCos
    would suffer from the change, even though they are much more common than this one.)

    (Alternative 2: We could avoid calling decomposePiCos entirely, integrating its
    behavior into simplifyArgsWorker. This would work, I think, but then all of the
    complication of decomposePiCos would end up layered on top of all the complication
    here. Please, no.)

    (Alternative 3: We could pass the unrewritten arguments into simplifyArgsWorker
    so that we don't have to recreate them. But that would complicate the interface
    of this function to handle a very dark, dark corner case. Better to keep our
    demons to ourselves here instead of exposing them to callers. This decision is
    easily reversed if there is ever any performance trouble due to the call of
    coercionKind.)

    So we now call

      decomposePiCos co1
                     (Pair (forall (j :: Star). (j |> axStar) -> Star) (forall j. j -> Type))
                     [bo |> sym axStar, NoWay |> sym bc]

    to get

      co5 :: Star ~ Type
      co6 :: (j |> axStar) ~ (j |> co5), substituted to
                                  (bo |> sym axStar |> axStar) ~ (bo |> sym axStar |> co5)
                               == bo ~ bo
      res_co :: Type ~ Star

    We then use these casts on (the rewritten) (3) and (4) to get

      (Bool |> sym axStar |> co5 :: Type)   -- (C3)
      (False |> sym bc |> co6    :: bo)     -- (C4)

    We can simplify to

      Bool                        -- (C3)
      (False |> sym bc :: bo)     -- (C4)

    Of course, we still must do the processing in Note [simplifyArgsWorker] to finish
    the job. We thus want to recur. Our new function kind is the left-hand type of
    co1 (gotten, recall, by lifting the variable k that was the return kind of the
    original function). Why the left-hand type (as opposed to the right-hand type)?
    Because we have casted all the arguments according to decomposePiCos, which gets
    us from the right-hand type to the left-hand one. We thus recur with that new
    function kind, zapping our lifting context, because we have essentially applied
    it.

    This recursive call returns ([Bool, False], [...], Refl). The Bool and False
    are the correct arguments we wish to return. But we must be careful about the
    result coercion: our new, rewritten application will have kind Type, but we
    want to make sure that the result coercion casts this back to Star. (Why?
    Because we started with an application of kind Star, and rewriting is homogeneous.)

    So, we have to twiddle the result coercion appropriately.

    Let's check whether this is well-typed. We know

      a :: forall (k :: Type). k -> k

      a (forall j. j -> Type) :: (forall j. j -> Type) -> forall j. j -> Type

      a (forall j. j -> Type)
        Proxy
          :: forall j. j -> Type

      a (forall j. j -> Type)
        Proxy
        Bool
          :: Bool -> Type

      a (forall j. j -> Type)
        Proxy
        Bool
        False
          :: Type

      a (forall j. j -> Type)
        Proxy
        Bool
        False
         |> res_co
         :: Star

    as desired.

    Whew.

    Historical note: I (Richard E) once thought that the final part of the kind
    had to be a variable k (as in the example above). But it might not be: it could
    be an application of a variable. Here is the example:

      let f :: forall (a :: Type) (b :: a -> Type). b (Any @a)
          k :: Type
          x :: k

      rewrite (f @Type @((->) k) x)

    After instantiating [a |-> Type, b |-> ((->) k)], we see that `b (Any @a)`
    is `k -> Any @a`, and thus the third argument of `x :: k` is well-kinded.

    -}

    -- | Stores 'Reductions' as well as a kind coercion.
    --
    -- Used when rewriting arguments to a type function @f@.
    --
    -- Invariant:
    --   when the stored reductions are of the form
    --     co_i :: ty_i ~ xi_i,
    --   the kind coercion is of the form
    --      kco :: typeKind (f ty_1 ... ty_n) ~ typeKind (f xi_1 ... xi_n)
    --
    -- The type function @f@ depends on context.
    data ArgsReductions =
      ArgsReductions
        {-# UNPACK #-} !Reductions
        !MCoercionN
      -- The strictness annotations and UNPACK pragma here are crucial
      -- to getting good performance in simplifyArgsWorker's tight loop.

    -- This is shared between the rewriter and the normaliser in GHC.Core.FamInstEnv.
    -- See Note [simplifyArgsWorker]
    {-# INLINE simplifyArgsWorker #-}
    -- NB. INLINE yields a ~1% decrease in allocations in T9872d compared to INLINEABLE
    -- This function is only called in two locations, so the amount of code duplication
    -- should be rather reasonable despite the size of the function.
    simplifyArgsWorker :: HasDebugCallStack
                       => [PiTyBinder] -> Kind
                           -- the binders & result kind (not a Π-type) of the function applied to the args
                           -- list of binders can be shorter or longer than the list of args
                       -> TyCoVarSet   -- free vars of the args
                       -> Infinite Role-- list of roles, r
                       -> [Reduction]  -- rewritten type arguments, arg_i
                                       -- each comes with the coercion used to rewrite it,
                                       -- arg_co_i :: ty_i ~ arg_i
                       -> ArgsReductions
    -- Returns ArgsReductions (Reductions cos xis) res_co, where co_i :: ty_i ~ xi_i,
    -- and res_co :: kind (f ty_1 ... ty_n) ~ kind (f xi_1 ... xi_n), where f is the function
    -- that we are applying.
    -- Precondition: if f :: forall bndrs. inner_ki (where bndrs and inner_ki are passed in),
    -- then (f ty_1 ... ty_n) is well kinded. Note that (f arg_1 ... arg_n) might *not* be well-kinded.
    -- Massaging the arg_i in order to make the function application well-kinded is what this
    -- function is all about. That is, (f xi_1 ... xi_n), where xi_i are the returned arguments,
    -- *is* well kinded.
    simplifyArgsWorker :: HasDebugCallStack =>
    [PiTyBinder]
    -> Type
    -> TyCoVarSet
    -> Infinite Role
    -> [Reduction]
    -> ArgsReductions
    simplifyArgsWorker [PiTyBinder]
    orig_ki_binders Type
    orig_inner_ki TyCoVarSet
    orig_fvs
                       Infinite Role
    orig_roles [Reduction]
    orig_simplified_args
      = LiftingContext
    -> [PiTyBinder]
    -> Type
    -> Infinite Role
    -> [Reduction]
    -> ArgsReductions
    go LiftingContext
    orig_lc
           [PiTyBinder]
    orig_ki_binders Type
    orig_inner_ki
           Infinite Role
    orig_roles [Reduction]
    orig_simplified_args
      where
        orig_lc :: LiftingContext
    orig_lc = InScopeSet -> LiftingContext
    emptyLiftingContext (InScopeSet -> LiftingContext) -> InScopeSet -> LiftingContext
    forall a b. (a -> b) -> a -> b
    $ TyCoVarSet -> InScopeSet
    mkInScopeSet TyCoVarSet
    orig_fvs

        go :: LiftingContext  -- mapping from tyvars to rewriting coercions
           -> [PiTyBinder]    -- Unsubsted binders of function's kind
           -> Kind            -- Unsubsted result kind of function (not a Pi-type)
           -> Infinite Role   -- Roles at which to rewrite these ...
           -> [Reduction]     -- rewritten arguments, with their rewriting coercions
           -> ArgsReductions
        go :: LiftingContext
    -> [PiTyBinder]
    -> Type
    -> Infinite Role
    -> [Reduction]
    -> ArgsReductions
    go !LiftingContext
    lc [PiTyBinder]
    binders Type
    inner_ki Infinite Role
    _ []
            -- The !lc makes the function strict in the lifting context
            -- which means GHC can unbox that pair.  A modest win.
          = Reductions -> MCoercionN -> ArgsReductions
    ArgsReductions
              ([Coercion] -> [Type] -> Reductions
    mkReductions [] [])
              MCoercionN
    kind_co
          where
            final_kind :: Type
    final_kind = [PiTyBinder] -> Type -> Type
    HasDebugCallStack => [PiTyBinder] -> Type -> Type
    mkPiTys [PiTyBinder]
    binders Type
    inner_ki
            kind_co :: MCoercionN
    kind_co | Type -> Bool
    noFreeVarsOfType Type
    final_kind = MCoercionN
    MRefl
                    | Bool
    otherwise                   = Coercion -> MCoercionN
    MCo (Coercion -> MCoercionN) -> Coercion -> MCoercionN
    forall a b. (a -> b) -> a -> b
    $ HasDebugCallStack => Role -> LiftingContext -> Type -> Coercion
    Role -> LiftingContext -> Type -> Coercion
    liftCoSubst Role
    Nominal LiftingContext
    lc Type
    final_kind

        go LiftingContext
    lc (PiTyBinder
    binder:[PiTyBinder]
    binders) Type
    inner_ki (Inf Role
    role Infinite Role
    roles) (Reduction
    arg_redn:[Reduction]
    arg_redns)
          =  -- We rewrite an argument ty with arg_redn = Reduction arg_co arg
             -- By Note [Rewriting] in GHC.Tc.Solver.Rewrite invariant (F2),
             -- typeKind(ty) = typeKind(arg).
             -- However, it is possible that arg will be used as an argument to a function
             -- whose kind is different, if earlier arguments have been rewritten.
             -- We thus need to compose the reduction with a kind coercion to ensure
             -- well-kindedness (see the call to mkCoherenceRightRedn below).
             --
             -- The bangs here have been observed to improve performance
             -- significantly in optimized builds; see #18502
             let !kind_co :: Coercion
    kind_co = HasDebugCallStack => Role -> LiftingContext -> Type -> Coercion
    Role -> LiftingContext -> Type -> Coercion
    liftCoSubst Role
    Nominal LiftingContext
    lc (PiTyBinder -> Type
    piTyBinderType PiTyBinder
    binder)
                 !(Reduction Coercion
    casted_co Type
    casted_xi)
                          = Role -> Reduction -> Coercion -> Reduction
    mkCoherenceRightRedn Role
    role Reduction
    arg_redn Coercion
    kind_co
             -- now, extend the lifting context with the new binding
                 !new_lc :: LiftingContext
    new_lc | Just TyVar
    tv <- PiTyBinder -> Maybe TyVar
    namedPiTyBinder_maybe PiTyBinder
    binder
                         = LiftingContext -> TyVar -> Coercion -> LiftingContext
    extendLiftingContextAndInScope LiftingContext
    lc TyVar
    tv Coercion
    casted_co
                         | Bool
    otherwise
                         = LiftingContext
    lc
                 !(ArgsReductions (Reductions [Coercion]
    cos [Type]
    xis) MCoercionN
    final_kind_co)
                   = LiftingContext
    -> [PiTyBinder]
    -> Type
    -> Infinite Role
    -> [Reduction]
    -> ArgsReductions
    go LiftingContext
    new_lc [PiTyBinder]
    binders Type
    inner_ki Infinite Role
    roles [Reduction]
    arg_redns
             in Reductions -> MCoercionN -> ArgsReductions
    ArgsReductions
                  ([Coercion] -> [Type] -> Reductions
    Reductions (Coercion
    casted_coCoercion -> [Coercion] -> [Coercion]
    forall a. a -> [a] -> [a]
    :[Coercion]
    cos) (Type
    casted_xiType -> [Type] -> [Type]
    forall a. a -> [a] -> [a]
    :[Type]
    xis))
                  MCoercionN
    final_kind_co

        -- See Note [Last case in simplifyArgsWorker]
        go LiftingContext
    lc [] Type
    inner_ki Infinite Role
    roles [Reduction]
    arg_redns
          = let co1 :: Coercion
    co1 = HasDebugCallStack => Role -> LiftingContext -> Type -> Coercion
    Role -> LiftingContext -> Type -> Coercion
    liftCoSubst Role
    Nominal LiftingContext
    lc Type
    inner_ki
                co1_kind :: Pair Type
    co1_kind              = HasDebugCallStack => Coercion -> Pair Type
    Coercion -> Pair Type
    coercionKind Coercion
    co1
                unrewritten_tys :: [Type]
    unrewritten_tys       = (Reduction -> Type) -> [Reduction] -> [Type]
    forall a b. (a -> b) -> [a] -> [b]
    map Reduction -> Type
    reductionOriginalType [Reduction]
    arg_redns
                ([Coercion]
    arg_cos, Coercion
    res_co)     = HasDebugCallStack =>
    Coercion -> Pair Type -> [Type] -> ([Coercion], Coercion)
    Coercion -> Pair Type -> [Type] -> ([Coercion], Coercion)
    decomposePiCos Coercion
    co1 Pair Type
    co1_kind [Type]
    unrewritten_tys
                casted_args :: [Reduction]
    casted_args           = Bool -> SDoc -> [Reduction] -> [Reduction]
    forall a. HasCallStack => Bool -> SDoc -> a -> a
    assertPpr ([Reduction] -> [Coercion] -> Bool
    forall a b. [a] -> [b] -> Bool
    equalLength [Reduction]
    arg_redns [Coercion]
    arg_cos)
                                                  ([Reduction] -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr [Reduction]
    arg_redns SDoc -> SDoc -> SDoc
    forall doc. IsDoc doc => doc -> doc -> doc
    $$ [Coercion] -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr [Coercion]
    arg_cos)
                                      ([Reduction] -> [Reduction]) -> [Reduction] -> [Reduction]
    forall a b. (a -> b) -> a -> b
    $ (Role -> Reduction -> Coercion -> Reduction)
    -> [Role] -> [Reduction] -> [Coercion] -> [Reduction]
    forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
    zipWith3 Role -> Reduction -> Coercion -> Reduction
    mkCoherenceRightRedn (Infinite Role -> [Role]
    forall a. Infinite a -> [a]
    Inf.toList Infinite Role
    roles) [Reduction]
    arg_redns [Coercion]
    arg_cos
                   -- In general decomposePiCos can return fewer cos than tys,
                   -- but not here; because we're well typed, there will be enough
                   -- binders. Note that decomposePiCos does substitutions, so even
                   -- if the original substitution results in something ending with
                   -- ... -> k, that k will be substituted to perhaps reveal more
                   -- binders.
                zapped_lc :: LiftingContext
    zapped_lc             = LiftingContext -> LiftingContext
    zapLiftingContext LiftingContext
    lc
                Pair Type
    rewritten_kind Type
    _ = Pair Type
    co1_kind
                ([PiTyBinder]
    bndrs, Type
    new_inner)    = Type -> ([PiTyBinder], Type)
    splitPiTys Type
    rewritten_kind

                ArgsReductions Reductions
    redns_out MCoercionN
    res_co_out
                  = LiftingContext
    -> [PiTyBinder]
    -> Type
    -> Infinite Role
    -> [Reduction]
    -> ArgsReductions
    go LiftingContext
    zapped_lc [PiTyBinder]
    bndrs Type
    new_inner Infinite Role
    roles [Reduction]
    casted_args
            in
              Reductions -> MCoercionN -> ArgsReductions
    ArgsReductions Reductions
    redns_out (Coercion
    res_co Coercion -> MCoercionN -> MCoercionN
    `mkTransMCoR` MCoercionN
    res_co_out)