-- 'co' is always Representational

 pushCoArg co arg

   | Type ty <- arg

        ; return (Type ty', m_co') }

   | otherwise

        ; let arg_mco' = checkReflexiveMCo arg_mco

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

        ; return (arg `mkCastMCo` arg_mco', m_co') }

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

 -- Push the coercion through to return

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

 -- 'co' is always Representational

 -- If the returned coercion is Nothing, then it would have been reflexive;

 -- it's faster not to compute it, though.

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

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

   -- -- | tyL `eqType` tyR

   -- -- = Just (ty, Nothing)

   | isForAllTy_ty tyL

   | otherwise

   = Nothing

   where

     co1 = mkSymCo (mkSelCo SelForAll co)

        -- co1 :: k2 ~N k1

        -- kinds of the types related by a coercion between forall-types.

        -- See the SelCo case in GHC.Core.Lint.

         -- Arg of mkInstCo is always nominal, hence Nominal

 --

 --

 -- or, equivalently

 --

 --

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

   -- -- | tyL `eqType` tyR

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

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

   | otherwise

   = Nothing

   where

     new_arg_ty = funArgTy tyL

 pushCoercionIntoLambda

     :: HasDebugCallStack => InScopeSet -> Var -> CoreExpr -> CoercionR -> Maybe (Var, CoreExpr)

 import GHC.Core

 import GHC.Core.Opt.Simplify.Monad

 import GHC.Core.Opt.ConstantFold

 import GHC.Core.Opt.Simplify.Env

 import GHC.Core.Opt.Simplify.Inline

 import GHC.Core.Opt.Simplify.Utils

 import GHC.Core.Make       ( FloatBind, mkImpossibleExpr, castBottomExpr )

 import qualified GHC.Core.Make

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

 import GHC.Core.Reduction

 import GHC.Core.Coercion.Opt    ( optCoercion )

 import GHC.Core.FamInstEnv      ( FamInstEnv, topNormaliseType_maybe )

 import GHC.Core.DataCon

 import GHC.Core.Ppr     ( pprCoreExpr )

 import GHC.Core.Unfold

 import GHC.Core.Unfold.Make

 simplCoercion :: SimplEnv -> InCoercion -> SimplM OutCoercion

 simplCoercion env co

   where

     subst = getTCvSubst env

     opts  = seOptCoercionOpts env

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

 -- | Push a TickIt context outwards past applications and cases, as

 pushCast env co cont

   = go co True cont

   where

     go :: OutCoercion -> Bool -> SimplCont -> SimplM SimplCont

     go co1 _ (CastIt { sc_co = co2, sc_cont = cont })  -- See Note [Optimising reflexivity]

       = go (mkTransCo co1 co2) False cont

                   -- See Note [Avoid re-simplifying coercions]

     go co co_is_opt (ApplyToTy { sc_arg_ty = arg_ty, sc_cont = tail })

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

         do { tail' <- go_mco m_co' co_is_opt tail

            ; return (ApplyToTy { sc_arg_ty  = arg_ty'

                                , sc_cont    = tail'

                                     -- NB!  As the cast goes past, the

                                     -- type of the hole changes (#16312)

       = -- pushCoValArg duplicates the coercion, so optimise first

         go (optOutCoercion (zapSubstEnv env) co co_is_opt) True cont

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

            ; return (ApplyToVal { sc_arg  = arg

                                 , sc_env  = arg_se

                                 , sc_cast = arg_mco `mkTransMCo` m_co1

                                 , sc_cont = tail'

     go co co_is_opt cont

       | isReflCo co = return cont  -- Having this at the end makes a huge

                                    -- See Note [Optimising reflexivity]

       | otherwise = return (CastIt { sc_co = co, sc_opt = co_is_opt, sc_cont = cont })

         -- If the first parameter is MRefl, then simplifying revealed a

         -- reflexive coercion. Omit.

     go_mco :: MOutCoercion -> Bool -> SimplCont -> SimplM SimplCont

         -- * Substitutions

         Subst(..), TvSubstEnv, CvSubstEnv, IdSubstEnv,

         emptyIdSubstEnv, emptyTvSubstEnv, emptyCvSubstEnv, composeTCvSubst,

         mkSubst, mkTCvSubst, mkTvSubst, mkCvSubst, mkIdSubst,

         getTvSubstEnv, getIdSubstEnv,

         getCvSubstEnv, substInScopeSet, setInScope, getSubstRangeTyCoFVs,

 isEmptySubst (Subst _ id_env tv_env cv_env)

   = isEmptyVarEnv id_env && isEmptyVarEnv tv_env && isEmptyVarEnv cv_env

 -- | Checks whether the tyvar and covar environments are empty.

 -- This function should be used over 'isEmptySubst' when substituting

 -- for types, because types currently do not contain expressions; we can

 import GHC.Core

 import GHC.Core.Coercion.Axiom

 import GHC.Core.Coercion

 import GHC.Core.Ppr ()   -- Instance OutputableBndr TyVar

 import GHC.Core.Predicate

 import GHC.Core.Type

   | assertPpr (coercionRole co == Representational)

               (vcat [text "Coercion of wrong role passed to evCastE:", ppr ee, ppr co]) $

     isReflCo co = ee

 evDFunApp :: DFunId -> [Type] -> [EvExpr] -> EvTerm

 -- Dictionary instance application, including when the "dictionary function"