| otherwise

   = mk_forall_co v visL visR kind_co co

     CCoercion co -> CCoercion (mkForAllCo v visL visR MRefl co)

 -- mkForAllVisCos [tv{vis}] constructs a cast

 --   forall tv. res  ~R#   forall tv{vis} res`.

 mkPiCastCo _ _ ReflCastCo     = ReflCastCo

 mkPiCastCo r v (CCoercion co) = CCoercion (mkPiCo r v co)

 mkPiCastCo _ v (ZCoercion ty cos)

   | otherwise = ZCoercion (mkFunctionType (idMult v) (varType v) ty) cos

   where

     vis = coreTyLamForAllTyFlag

         -- 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

       -- Float app ticks: \x -> Tick t (e x) ==> Tick t e

     go (b : bs) (App fun arg) co

       = fmap (flip (foldr mkTick) ticks) $ go bs fun co'

             -- Float arg ticks: \x -> e (Tick t x) ==> Tick t e

            -> CastCoercion     -- Of kind (t1~t2)

            -> Type             -- Type (arg_t -> t1) of the function

                                --      to which the argument is supplied

            -> Maybe (CastCoercion  -- Of type (arg_t -> t1 ~  bndr_t -> t2)

                                --   (and similarly for tyvars, coercion args)

                     , [CoreTickish])

     -- See Note [Eta reduction with casted arguments]

        | Just tv <- getTyVar_maybe arg_ty

        , bndr == tv  = case splitForAllForAllTyBinder_maybe fun_ty of

            Just (Bndr _ vis, _) -> Just (fco, [])

                    -- The lambda we are eta-reducing always has visibility

                    -- 'coreTyLamForAllTyFlag' which may or may not match

                    -- the visibility on the inner function (#24014)

                                (text "fun:" <+> ppr bndr

                                 $$ text "arg:" <+> ppr arg_ty

                                 $$ text "fun_ty:" <+> ppr fun_ty)

        | bndr == v

        , let mult = idMult bndr

        , Just (_af, fun_mult, _, _) <- splitFunTy_maybe fun_ty

        , mult `eqType` fun_mult -- There is no change in multiplicity, otherwise we must abort

        = Just (mkFunResCastCo Representational bndr co, [])

        | (ticks, Var v) <- stripTicksTop tickishFloatable e

        , Just (_, fun_mult, _, res_ty) <- splitFunTy_maybe fun_ty

        , bndr == v

        , fun_mult `eqType` idMult bndr

        -- The simplifier combines multiple casts into one,

        -- so we can have a simple-minded pattern match here

        = Just (co', t:ticks)

 -- | Can we eta-reduce the given function

 -- See Note [Eta reduction soundness], criteria (B), (J), and (W).

 import qualified GHC.Core.Make

 import GHC.Core.Coercion hiding ( substCo, substCoVar )

 import GHC.Core.Reduction

 import GHC.Core.FamInstEnv      ( FamInstEnv, topNormaliseType_maybe )

 import GHC.Core.DataCon

 import GHC.Core.Opt.Stats ( Tick(..) )

         -> rebuild_go env (mkCastCo expr co') cont

            -- NB: mkCast implements the (Coercion co |> g) optimisation

         where

       Select { sc_bndr = bndr, sc_alts = alts, sc_env = se, sc_cont = cont }

         -> rebuildCase (se `setInScopeFromE` env) expr bndr alts cont

 -}

 -- See Note [Avoid re-simplifying coercions]

   | already_optimised = co  -- See Note [Avoid re-simplifying coercions]

   where

     empty_subst = mkEmptySubst (seInScope env)

     opts = seOptCoercionOpts env

                                                 , sc_dup = dup, sc_cont = tail

                                                 , sc_hole_ty = fun_ty })

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

           | Just (_, m_co1, res_ty, m_co2) <- pushCastCoValArg tyL co

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

 mkDupableContWithDmds env dmds (CastIt { sc_co = co, sc_hole_ty = ty, sc_opt = opt, sc_cont = cont })

   = do  { (floats, cont') <- mkDupableContWithDmds env dmds cont

                                  , sc_hole_ty = ty

                                  , sc_opt = True, sc_cont = cont' }) }

                  -- optOutCoercion: see Note [Avoid re-simplifying coercions]

   = EvExpr <$> zonkCoreExpr e

 zonkEvTerm (EvCastExpr e (CCoercion co) co_res_ty)

   = do { zap_casts <- hasZapCasts <$> lift getDynFlags

          else EvExpr <$> zonkCoreExpr (Cast e (CCoercion co))

        }

 zonkEvTerm ev@(EvCastExpr _ (ZCoercion{}) _)

   -fshow-warning-groups

   -fprefer-byte-code

   -fbreak-points

 warning settings:

   -Wpattern-namespace-specifier

 === :set

   -fshow-warning-groups

   -fprefer-byte-code

   -fbreak-points

 warning settings:

   -Wpattern-namespace-specifier

 Unit ID: b-0.0.0

   -fshow-warning-groups

   -fprefer-byte-code

   -fbreak-points

 warning settings:

   -Wpattern-namespace-specifier

 Unit ID: c-0.0.0

   -fshow-warning-groups

   -fprefer-byte-code

   -fbreak-points

 warning settings:

   -Wpattern-namespace-specifier

 Unit ID: d-0.0.0

   -fshow-warning-groups

   -fprefer-byte-code

   -fbreak-points

 warning settings:

   -Wpattern-namespace-specifier