applyForAllTy,

         decomposeFunCastCo,

         -- ** Decomposition

         instNewTyCon_maybe,

         -- ** Free variables

         tyCoVarsOfCo, tyCoVarsOfCos, coVarsOfCo,

         tyCoVarsOfCastCo,

         -- ** Substitution

         CvSubstEnv, emptyCvSubstEnv,

         eqCoercion, eqCoercionX, eqCastCoercion, eqCastCoercionX,

         -- ** Forcing evaluation of coercions

         -- * Pretty-printing

         pprCo, pprParendCo,

     Pair argl_ty argr_ty = coercionKind arg_co

     Pair resl_ty resr_ty = coercionKind res_co

 -- | Build a function 'Coercion' from two other 'Coercion's. That is,

   = mk_forall_co v visL visR kind_co co

 mkForAllCastCo :: HasDebugCallStack => Role -> TyCoVar -> ForAllTyFlag -> ForAllTyFlag

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

     ZCoercion ty cos -> ZCoercion (mkTyCoForAllTy v visR ty) cos

     ReflCastCo | visL `eqForAllVis` visR -> ReflCastCo

 mkSymCastCo ty (ZCoercion _ cos) = ZCoercion ty cos

 mkSymCastCo _  ReflCastCo        = ReflCastCo

 -- | mkTransCo creates a new 'Coercion' by composing the two

 --   given 'Coercion's transitively: (co1 ; co2)

 mkTransCo :: HasDebugCallStack => Coercion -> Coercion -> Coercion

 seqCastCoercion (ZCoercion ty cos) = seqType ty `seq` seqDVarSet cos

 seqCastCoercion ReflCastCo = ()

 seqCo :: Coercion -> ()

 seqCo (Refl ty)             = seqType ty

 seqCo (GRefl r ty mco)      = r `seq` seqType ty `seq` seqMCo mco

 --    See #19815 for a bit of data and discussion on this point

 coToCastCo co | isReflCo co = ReflCastCo

               | otherwise   = CCoercion co

 module GHC.Core.Coercion.Opt

    ( optCoercion, optTransCo

    , OptCoercionOpts (..)

    )

 where

   | otherwise

   = co1 `mkTransCo` co2

 -- AMG TODO: not clear if coercionLKind or substTy is better choice here

 optCastCoercion :: OptCoercionOpts -> Subst -> TypedCastCoercion -> TypedCastCoercion

 optCastCoercion _    env (TCC tyL ReflCastCo) = TCC (substTy env tyL) ReflCastCo

   where

     incoming_arity = count isId bndrs -- See Note [Eta reduction makes sense], point (2)

     go :: [Var]            -- Binders, innermost first, types [a3,a2,a1]

        -> CoreExpr         -- Of type tr

        -> CastCoercion     -- Of type tr ~ ts

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

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

     ok_arg :: Var              -- Of type bndr_t

            -> CoreExpr         -- Of type arg_t

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

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

 {- *********************************************************************

     old_arg_ty = funArgTy tyR

 pushCoercionIntoLambda

 -- This implements the Push rule from the paper on coercions

 --    (\x. e) |> co

 -- ===>

 --    (\x'. e |> co')

     | assert (not (isTyVar x) && not (isCoVar x)) True

     , Just (_, _, s1, _)   <- splitFunTy_maybe s1s2

     , Just (_, w1, t1,_t2) <- splitFunTy_maybe t1t2

     , typeHasFixedRuntimeRep t1

       -- We can't push the coercion into the lambda if it would create

       -- a representation-polymorphic binder.

     opts  = seOptCoercionOpts env

     subst_only = isEmptyTvSubst subst || reSimplifying env

 {- Note [Optimising coercions]

 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

 Some programs have very big coercions and we'd like to avoid repeatedly

 -}

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

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

                                     --   continuation passed to 'simplExprC'

          -> OutType                 -- ^ Type of the function applied to this arg

          -> StaticEnv -> CoreExpr   -- ^ Expression with its static envt

          -> SimplM OutExpr

 simplArg _ _ _ (Simplified {}) arg co

   = return $ mkCastCo arg co -- See Note [Avoid repeated simplification]

 import GHC.Core.Type as Type

    ( Type, extendTvSubst, extendCvSubst

    , substTy, getTyVar_maybe )

 import GHC.Core.TyCo.Ppr( pprParendType )

 import GHC.Core.Coercion as Coercion

 import GHC.Core.Tidy     ( tidyRules )

 import GHC.Core.Make

 import GHC.Core.Opt.OccurAnal( occurAnalyseExpr, occurAnalysePgm, zapLambdaBndrs )

 import GHC.Core.DataCon

 import GHC.Core.Type hiding ( substTy, extendTvSubst, extendCvSubst, extendTvSubstList

                             , isInScope, substTyVarBndr, cloneTyVarBndr )

 import GHC.Core.Predicate( isCoVarType )

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

 type SimpleClo = (SimpleOptEnv, InExpr)

 instance Outputable SimpleContItem where

   ppr (ApplyToArg (_, arg)) = text "ARG" <+> ppr arg

 data SimpleOptEnv

   = SOE { soe_opts :: {-# UNPACK #-} !SimpleOpts

       where (env', b') = subst_opt_bndr env b

     -- See Note [Eliminate casts in function position]

       | isNonCoVarId b

       -- Optimise the inner lambda to make it an 'OutExpr', which makes it

       -- possible to call 'pushCoercionIntoLambda' with the 'OutCoercion' 'co'.

       -- we need to do this to avoid mixing 'InExpr' and 'OutExpr', or two

       -- 'InExpr' with different environments (getting this wrong caused #26588 & #26589.)

       , Lam out_b out_body <- simple_app env e []

       = do_beta (soeZapSubst env) (Lam b' body') rest

         -- soeZapSubst: we've already optimised everything (the lambda and 'rest') by now.

       | otherwise

 simple_app env e as

   = rebuild_app env (simple_opt_expr env e) as

 add_cast :: SimpleOptEnv -> InTypedCastCoercion -> [SimpleContItem] -> [SimpleContItem]

   = as

   | otherwise

   = case as of

   where

 rebuild_app :: HasDebugCallStack

             => SimpleOptEnv -> OutExpr -> [SimpleContItem] -> OutExpr

     in_scope = soeInScope env

     mk_app out_fun = \case

       ApplyToArg arg -> App out_fun (simple_opt_clo in_scope arg)

 -- Like GHC.Core.Utils.mkCast, but does a full reflexivity check.

 -- mkCast doesn't do that because the Simplifier does (in simplCast)

 -- But in SimpleOpt it's nice to kill those nested casts (#18112)

 mk_cast e co

   = e

   | otherwise

 {- Note [Desugaring unlifted newtypes]

 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

     -- this implies that x is not in scope in gamma (makes this code simpler)

     , not (isTyVar x) && not (isCoVar x)

     , assert (not $ x `elemVarSet` tyCoVarsOfCastCo co) True

     , let res = Just (x',e',ts)

     = --pprTrace "exprIsLambda_maybe:Cast" (vcat [ppr casted_e,ppr co,ppr res)])

       res

 *                                                                      *

 ********************************************************************* -}

 tyCoVarsOfType :: Type -> TyCoVarSet

 -- The "deep" TyCoVars of the the type

 tyCoVarsOfType ty = runTyCoVars (deepTypeFV ty)

 -- See Note [Computing deep free variables]

 tyCoVarsOfCo co = runTyCoVars (deepCoFV co)

 tyCoVarsOfMCo :: MCoercion -> TyCoVarSet

 tyCoVarsOfMCo MRefl    = emptyVarSet

 tyCoVarsOfMCo (MCo co) = tyCoVarsOfCo co

 deepTypesFV :: [Type]     -> TyCoFV

 deepCoFV    :: Coercion   -> TyCoFV

 deepCosFV   :: [Coercion] -> TyCoFV

 deepTcvFolder :: TyCoFolder TyCoFV

 -- It's important that we use a one-shot EndoOS, to ensure that all

   where (_, _, f, _, _) = foldTyCo (afvFolder check_fv)

 anyFreeVarsOfCastCo :: (TyCoVar -> Bool) -> CastCoercion -> Bool

 noFreeVarsOfType :: Type -> Bool

 noFreeVarsOfType ty = not $ DM.getAny (runFVTop (f ty))

 instance Outputable CastCoercion where

   ppr = pprCastCo

 instance Outputable CoSel where

   ppr (SelTyCon n r) = text "Tc" <> parens (int n <> comma <> pprOneCharRole r)

   ppr SelForAll      = text "All"

     not_in v (WpCompose w1 w2)         = not_in v w1 && not_in v w2

     not_in v (WpEvApp (EvExpr e))      = not (v `elemVarSet` exprFreeVars e)

     not_in v (WpEvApp (EvCastExpr e co ty)) = not (v `elemVarSet` exprFreeVars e)

                                            && not (anyFreeVarsOfType (== v) ty)

     not_in _ (WpEvApp (EvTypeable {})) = False  -- Giving up; conservative

     not_in _ (WpEvApp (EvFun {}))      = False  -- Giving up; conservative

     not_in _ (WpEvLam {}) = False    -- Ditto

     not_in _ (WpLet {})   = False    -- Ditto

     not_in_submult :: TyVar -> SubMultCo -> Bool

     not_in_submult v = \case

       EqMultCo co -> not (anyFreeVarsOfCo (== v) co)