-- ** Cast coercions

         castCoToCo,

         mkTransCastCo, mkTransCastCoCo, mkTransCoCastCo,

         -- ** Decomposition

         instNewTyCon_maybe,

         coToMCo, kindCoToMKindCo,

         mkTransMCo, mkTransMCoL, mkTransMCoR, mkCastTyMCo, mkSymMCo,

         isReflMCo, checkReflexiveMCo,

         -- ** Coercion variables

 mkCastTyMCo ty MRefl    = ty

 mkCastTyMCo ty (MCo co) = ty `mkCastTy` co

 mkGReflLeftMCo :: Role -> Type -> MCoercionN -> Coercion

 mkGReflLeftMCo r ty MRefl    = mkReflCo r ty

     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,

 -- given @co1 :: a ~ b@ and @co2 :: x ~ y@ produce @co :: (a -> x) ~ (b -> y)@

 -- or @(a => x) ~ (b => y)@, depending on the kind of @a@/@b@.

   | otherwise

   = mk_forall_co v visL visR kind_co co

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

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

 -- See Note [Required foralls in Core] in GHC.Core.TyCo.Rep

   | isReflMCo kco          = co { fco_body = mkSymCo body_co }

 mkSymCo co                 = SymCo co

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

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

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

 mkPiCos :: Role -> [Var] -> Coercion -> Coercion

 mkPiCos r vs co = foldr (mkPiCo r) co vs

 -- | Make a forall 'Coercion', where both types related by the coercion

 -- are quantified over the same variable.

 mkPiCo  :: Role -> Var -> Coercion -> Coercion

                             mkFunResCo r v co

               | otherwise = mkFunResCo r v co

 mkFunResCo :: Role -> Id -> Coercion -> Coercion

 -- Given res_co :: res1 ~ res2,

 --   mkFunResCo r m arg res_co :: (arg -> res1) ~r (arg -> res2)

     arg_co = mkReflCo role (varType id)

     mult   = multToCo (idMult id)

 -- mkCoCast (c :: s1 ~?r t1) (g :: (s1 ~?r t1) ~#R (s2 ~?r t2)) :: s2 ~?r t2

 -- The first coercion might be lifted or unlifted; thus the ~? above

 -- Lifted and unlifted equalities take different numbers of arguments,

 -- but requires the type to be supplied by the caller because it cannot be

 -- recovered in the 'ZCoercion' case.

 castCoercionLKind :: HasDebugCallStack => Type -> CastCoercion -> Type

 castCoercionLKind lhs_ty (ZCoercion _ _) = lhs_ty

 castCoercionLKind lhs_ty ReflCastCo = lhs_ty

 mkTransCoCastCo co1 (ZCoercion ty cos) = ZCoercion ty (shallowCoVarsOfCo co1 `unionVarSet` cos)

 mkTransCoCastCo co1 ReflCastCo         = CCoercion co1

 -- | Slowly checks if the coercion is reflexive. Don't call this in a loop,

 -- as it walks over the entire coercion.

 isReflexiveCastCo :: Type -> CastCoercion -> Bool

 isReflexiveCastCo _      (CCoercion co) = isReflexiveCo co

 isReflexiveCastCo lhs_ty (ZCoercion rhs_ty _) = lhs_ty `eqType` rhs_ty

 isReflexiveCastCo _      ReflCastCo           = True

 module GHC.Core.Coercion.Opt

    ( optCoercion

    , OptCoercionOpts (..)

    )

 where

    { optCoercionEnabled :: Bool  -- ^ Enable coercion optimisation (reduce its size)

    }

 optCoercion :: OptCoercionOpts -> Subst -> Coercion -> NormalCo

 -- ^ optCoercion applies a substitution to a coercion,

 --   *and* optimises it to reduce its size

 -- We should really never care about the contents of a cast coercion. Instead,

 -- just look up the coercion's RHS type.

 newtype CastCoercionMap a = CastCoercionMap (CastCoercionMapG a)

 -- TODO(22292): derive

    , etaExpandToJoinPoint, etaExpandToJoinPointRule

    -- ** Coercions and casts

    , pushCoercionIntoLambda, pushCoDataCon, collectBindersPushingCo

    )

 where

 -}

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

      -- See Note [The EtaInfo mechanism]

 instance Outputable EtaInfo where

     go subst (Tick t e) eis

       = Tick (substTickish subst t) (go subst e eis)

       = go subst e (EI bs mco')

       where

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

     go subst (Case e b ty alts) eis

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

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

 etaInfoAppTy ty (EI bs mco)

   = applyTypeToArgs ty1 (map varToCoreExpr bs)

   where

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

 etaInfoAbs :: EtaInfo -> CoreExpr -> CoreExpr

 -- See Note [The EtaInfo mechanism]

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

 -- | @mkEtaWW n _ fvs ty@ will compute the 'EtaInfo' necessary for eta-expanding

     go _ [] subst _

        ----------- Done!  No more expansion needed

     go n oss@(one_shot:oss1) subst ty

        ----------- Forall types  (forall a. ty)

              --  we'd have had to zap it for the recursive call)

        , (in_scope, EI bs mco) <- go n oss subst ty'

          -- mco :: subst(ty') ~ b1_ty -> ... -> bn_ty -> tr

        | otherwise       -- We have an expression of arity > 0,

                          -- but its type isn't a function, or a binder

                          -- does not have a fixed runtime representation

        = warnPprTrace True "mkEtaWW" ((ppr orig_oss <+> ppr orig_ty) $$ ppr_orig_expr)

         -- This *can* legitimately happen:

         -- e.g.  coerce Int (\x. x) Essentially the programmer is

         -- playing fast and loose with types (Happy does this a lot).

         -- So we simply decline to eta-expand.  Otherwise we'd end up

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

 mkEtaForAllMCo (Bndr tcv vis) ty mco

   = case mco of

   where

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

     -- the (EtaInfo Invariant).  (sym co) wraps a lambda that always has

     -- a ForAllTyFlag of coreTyLamForAllTyFlag; see Note [Required foralls in Core]

 tryEtaReduce :: UnVarSet -> [Var] -> CoreExpr -> SubDemand -> Maybe CoreExpr

 -- Return an expression equal to (\bndrs. body)

 tryEtaReduce rec_ids bndrs body eval_sd

   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

        -> Maybe CoreExpr   -- Of type a1 -> a2 -> a3 -> ts

     -- See Note [Eta reduction with casted arguments]

     -- for why we have an accumulating coercion

     -- See Note [Eta reduction with casted function]

     go bs (Cast e co1) co2

     go bs (Tick t e) co

       | tickishFloatable t

       , remaining_bndrs `ltLength` bndrs

             -- Only reply Just if /something/ has happened

       , ok_fun fun

             reduced_bndrs = mkVarSet (dropList remaining_bndrs bndrs)

             -- reduced_bndrs are the ones we are eta-reducing away

       , used_vars `disjointVarSet` reduced_bndrs

           -- See Note [Eta reduction makes sense], intro and point (1)

           -- NB: don't compute used_vars from exprFreeVars (mkCast fun co)

           --     because the latter may be ill formed if the guard fails (#21801)

     go _remaining_bndrs _fun  _  = -- pprTrace "tER fail" (ppr _fun $$ ppr _remaining_bndrs) $

                                    Nothing

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

     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

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

        , 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

     ok_arg bndr (Cast e co_arg) co fun_ty

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

     ok_arg bndr (Tick t arg) co fun_ty

   by pushing the coercion into the arguments

 -}

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

 -- C.f. simplCast in GHC.Core.Opt.Simplify

 -- 'co' is always Representational

   | Type ty <- arg

        ; return (Type ty', m_co') }

   | otherwise

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

              -- the argument coercion actually being ReflCo

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

 -- Push the coercion through to return

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

 -- 'co' is always Representational

 pushCoTyArg co ty

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

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

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

 -- | If @pushCoValArg co = Just (co_arg, co_res)@, then

 --

 -- > (\x.body) |> co  =  (\y. let { x = y |> co_arg } in body) |> co_res)

 -- 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 ]) $

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

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

     -- is worth the cost, and it makes no difference in #18223

     Pair tyL tyR = coercionKind co

 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

     , Pair s1s2 t1t2 <- coercionKind co

     , Just {}              <- splitFunTy_maybe s1s2

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

     | otherwise

     = Nothing

               -> Maybe (DataCon

                        , [Type]      -- Universal type args

                        , [CoreExpr]) -- All other args incl existentials

 -- where co :: (T t1 .. tn) ~ (T s1 .. sn)

 -- The left-hand one must be a T, because exprIsConApp returned True

 -- but the right-hand one might not be.  (Though it usually will.)

 push_dc_refl :: DataCon -> [CoreExpr] -> (DataCon, [Type], [CoreExpr])

 push_dc_refl dc dc_args

 import GHC.Core

 import GHC.Core.FVs

 import GHC.Core.Utils   ( exprIsTrivial, isDefaultAlt, isExpandableApp,

 import GHC.Core.Opt.Arity   ( joinRhsArity, isOneShotBndr )

 import GHC.Core.Coercion

 import GHC.Core.Type

            -- If  x :-> (y, co)  is in the env,

            -- then please replace x by (y |> mco)

            -- Invariant of course: idType x = exprType (y |> mco)

               -- Domain is Global and Local Ids

               -- Range is just Local Ids

            , occ_bs_rng  :: !VarSet

       -- Do not add [x :-> x] to occ_bs_env, else lookupBndrSwap will loop

   = env { occ_bs_env = extendVarEnv swap_env scrut_var (case_bndr', mco)

         , occ_bs_rng = rng_vars `extendVarSet` case_bndr'

   | otherwise

   = env

 -- | See bBinderSwaOk.

 data BinderSwapDecision

   = NoBinderSwap

 scrutOkForBinderSwap :: OutExpr -> BinderSwapDecision

 -- If (scrutOkForBinderSwap e = DoBinderSwap v mco, then

 scrutOkForBinderSwap e

   = case e of

       Tick _ e        -> scrutOkForBinderSwap e  -- Drop ticks

                          -- Cast: see Note [Case of cast]

       _               -> NoBinderSwap

     -- Why do we iterate here?

     -- See (BS2) in Note [The binder-swap substitution]

     case lookupBndrSwap env bndr1 of

 {- Historical note [Proxy let-bindings]

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

 import GHC.Core.Opt.ConstantFold

 import GHC.Core.Type hiding ( substCo, substTy, substTyVar, extendTvSubst, extendCvSubst )

 import GHC.Core.TyCo.Compare( eqType )

 import GHC.Core.Opt.Simplify.Env

 import GHC.Core.Opt.Simplify.Inline

 import GHC.Core.Opt.Simplify.Utils

 import GHC.Core.Unfold.Make

 import GHC.Core.Utils

 import GHC.Core.Opt.Arity ( ArityType, exprArity, arityTypeBotSigs_maybe

                           , typeArity, arityTypeArity, etaExpandAT )

 import GHC.Core.SimpleOpt ( exprIsConApp_maybe, joinPointBinding_maybe, joinPointBindings_maybe )

 import GHC.Core.FVs     ( mkRuleInfo {- exprsFreeIds -} )

 import GHC.Types.Basic

 import GHC.Types.Tickish

 import GHC.Types.Var    ( isTyCoVar )

 import GHC.Builtin.Types.Prim( realWorldStatePrimTy )

 import GHC.Builtin.Names( runRWKey, seqHashKey )

     mk_worker_unfolding top_lvl work_id work_rhs

       = case realUnfoldingInfo info of -- NB: the real one, even for loop-breakers

            unf@(CoreUnfolding { uf_tmpl = unf_rhs, uf_src = src })

            _ -> mkLetUnfolding env top_lvl VanillaSrc work_id False work_rhs

 tryCastWorkerWrapper env _ _ bndr rhs  -- All other bindings

     subst = getTCvSubst env

     opts  = seOptCoercionOpts env

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

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

 -- long as this is a non-scoping tick, to let case and application

       Stop {}          -> return (emptyFloats env, expr)

       TickIt t cont    -> rebuild_go env (mkTick t expr) cont

       CastIt { sc_co = co, sc_opt = opt, sc_cont = 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

 -}

 optOutCoercion :: SimplEnvIS -> OutCoercion -> Bool -> OutCoercion

 -- See Note [Avoid re-simplifying coercions]

 optOutCoercion env co already_optimised

 simplCast :: SimplEnv -> InExpr -> InCastCoercion -> SimplCont

           -> SimplM (SimplFloats, OutExpr)

 simplCast env body co0 cont0