-- Beta-reduction if possible, pushing any intervening casts past

     -- the argument. See Note [The EtaInfo mechanism]

     go subst (Lam v e) (EI (b:bs) mco)

       = go (Core.extendSubst subst v arg) e (EI bs mco')

     -- Stop pushing down; just wrap the expression up

     -- See Note [Check for reflexive casts in eta expansion]

     go subst e (EI bs mco) = Core.substExprSC subst e

                              `mkVarApps` bs

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

         -- with an explicit lambda having a non-function type

 mkEtaForAllMCo :: ForAllTyBinder -> Type -> CastCoercion -> CastCoercion

   = case mco of

       ReflCastCo | vis == coreTyLamForAllTyFlag -> ReflCastCo

                  | otherwise                    -> mk_fco (mkRepReflCo ty)

       CCoercion co                              -> mk_fco co

   where

     mk_fco co = CCoercion (mkForAllCo tcv vis coreTyLamForAllTyFlag MRefl co)

     -- coreTyLamForAllTyFlag: See Note [The EtaInfo mechanism], particularly

   by pushing the coercion into the arguments

 -}

 pushCoArgs fun_ty co (arg:args) = do

     ; if isReflCastCo m_co1

     }

 -- We have (fun |> co) arg, and we want to transform it to

 --         (fun arg) |> co

 -- This may fail, e.g. if (fun :: N) where N is a newtype

 -- 'co' is always Representational

 pushCoArg fun_ty co arg

   | Type ty <- arg

   | otherwise

              -- checkReflexiveCastCo: see Note [Check for reflexive casts in eta expansion]

              -- The coercion is very often (arg_co -> res_co), but without

              -- the argument coercion actually being ReflCo

 pushCastCoTyArg (CCoercion co)         ty = pushCoTyArg co ty

 pushCastCoTyArg (ZCoercion _fun_ty _cos) _ty = Nothing -- TODO do better

 -- We have (fun |> co) @ty

 -- Push the coercion through to return

 --         (fun @ty') |> co'

   -- -- = Just (ty, Nothing)

   | isReflCo co

   | isForAllTy_ty tyL

   = assertPpr (isForAllTy_ty tyR) (ppr co $$ ppr ty) $

   | otherwise

   = Nothing

         -- co2 :: ty1[ (ty|>co1)/a1 ] ~R ty2[ ty/a2 ]

         -- Arg of mkInstCo is always nominal, hence Nominal

 pushCastCoValArg _ (CCoercion co)     = pushCoValArg co

 pushCastCoValArg tyL (ZCoercion tyR cos)

   | isFunTy tyL  -- TODO: do we need to check this or can we assume it?

   , isFunTy tyR

   , typeHasFixedRuntimeRep new_arg_ty

   | otherwise = Nothing

   where

     new_arg_ty = funArgTy tyR

 -- If the LHS is well-typed, then so is the RHS. In particular, the argument

 -- @arg |> co_arg@ is guaranteed to have a fixed 'RuntimeRep', in the sense of

 -- Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete.

 pushCoValArg co

   -- The following is inefficient - don't do `eqType` here, the coercion

   -- optimizer will take care of it. See #14737.

   -- -- = Just (mkRepReflCo arg, Nothing)

   | isReflCo co

   | isFunTy tyL

   , (_, co1, co2) <- decomposeFunCo co

      (vcat [ text "co:" <+> ppr co

            , text "old_arg_ty:" <+> ppr old_arg_ty

            , text "new_arg_ty:" <+> ppr new_arg_ty ]) $

     -- Critically, coToCastCo to checks for ReflCo; the whole coercion may not

     -- be reflexive, but either of its components might be

     -- We could use isReflexiveCo, but it's not clear if the benefit

                       -- False: (mkTransCo co1 co2) is not fully optimised

                       -- See Note [Avoid re-simplifying coercions]

           = {-#SCC "addCoerce-pushCoTyArg" #-}

                ; return (ApplyToTy { sc_arg_ty  = arg_ty'

                                    , sc_cont    = tail'

                                    , sc_hole_ty = tyL }) }

           | not co_is_opt  -- pushCoValArg duplicates the coercion, so optimise first

           = addCoerce tyL (optOutCastCoercion (zapSubstEnv env) co co_is_opt) True cont

           = {-#SCC "addCoerce-pushCoValArg" #-}

                ; if isReflCastCo m_co1

                    then return (cont { sc_cont = tail'

                                          , sc_hole_ty = tyL }) ;

        | not (tickishIsCode t) = go subst floats expr cont

     go subst floats (Cast expr co1) (CC args m_co2) -- TODO: is the subst_ty below needed?

             -- See Note [Push coercions in exprIsConApp_maybe]

        = go subst floats expr (CC args' (m_co1' `mkTransCastCo` m_co2))