-- ** Cast coercions

         castCoToCo,

         mkTransCastCo, mkTransCastCoCo, mkTransCoCastCo,

         -- ** Decomposition

         instNewTyCon_maybe,

         pickLR,

         isGReflCo, isReflCo, isReflCo_maybe, isGReflCo_maybe, isReflexiveCo, isReflexiveCo_maybe,

         isReflCoVar_maybe, isGReflMCo, mkGReflLeftMCo, mkGReflRightMCo,

         mkCoherenceRightMCo,

 seqCastCoercion :: CastCoercion -> ()

 seqCastCoercion (CCoercion co) = seqCo co

 seqCo :: Coercion -> ()

 seqCo (Refl ty)             = seqType ty

 -- have discarded the original 'Coercion'.

 castCoToCo :: Type -> CastCoercion -> CoercionR

 castCoToCo _      (CCoercion co)         = co

 -- | Compose two 'CastCoercion's transitively, like 'mkTransCo'.  If either is

 -- zapped the whole result will be zapped.

 mkTransCastCo :: HasDebugCallStack => CastCoercion -> CastCoercion -> CastCoercion

 mkTransCastCo cco (CCoercion co)     = mkTransCastCoCo cco co

 -- | Transitively compose a 'CastCoercion' followed by a 'Coercion'.

 mkTransCastCoCo :: HasDebugCallStack => CastCoercion -> Coercion -> CastCoercion

 mkTransCastCoCo (CCoercion co1)   co2 = CCoercion (mkTransCo co1 co2)

 -- | Transitively compose a 'Coercion' followed by a 'CastCoercion'.

 mkTransCoCastCo :: HasDebugCallStack => Coercion -> CastCoercion -> CastCoercion

 mkTransCoCastCo co1 (CCoercion co2)    = CCoercion (mkTransCo co1 co2)

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

 -- as it walks over the entire coercion.

 cast_co_fvs :: CastCoercion -> FV

 cast_co_fvs (CCoercion co)     fv_cand in_scope acc = (tyCoFVsOfCo co) fv_cand in_scope acc

 ---------

 rhs_fvs :: (Id, CoreExpr) -> FV

     go subst (Tick t e) eis

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

       = go subst e (EI bs mco')

       where

         mco' = checkReflexiveMCo (Core.substCo subst co `mkTransMCoR` mco)

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

 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

                     , [CoreTickish])

     -- See Note [Eta reduction with casted arguments]

        | Just tv <- getTyVar_maybe arg_ty

        , bndr == tv  = case splitForAllForAllTyBinder_maybe fun_ty of

              where !fco = mkForAllCo tv vis coreTyLamForAllTyFlag kco co

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

                    -- 'coreTyLamForAllTyFlag' which may or may not match

                                (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

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

        , Just (_, fun_mult, _, _) <- 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

     ok_arg bndr (Tick t arg) co fun_ty

        | tickishFloatable t, Just (co', ticks) <- ok_arg bndr arg co fun_ty

        = Just (co', t:ticks)

     ok_arg _ _ _ _ = Nothing

 -- | Can we eta-reduce the given function

     go :: [Var] -> CoreExpr -> ([Var], CoreExpr)

     -- The accumulator is in reverse order

     go bs (Lam b e)   = go (b:bs) e

     go bs e           = (reverse bs, e)

     -- We are in a cast; peel off casts until we hit a lambda.

     go_c :: [Var] -> CoreExpr -> Coercion -> ([Var], CoreExpr)

     -- (go_c bs e c) is same as (go bs e (e |> c))

     go_c bs (Lam b e)    co  = go_lam bs b e co

     go_c bs e            co  = (reverse bs, mkCast e co)

 castCoercionDmdEnv :: CastCoercion -> DmdEnv

 castCoercionDmdEnv (CCoercion co)    = coercionDmdEnv co

 coercionsDmdEnv :: [Coercion] -> DmdEnv

 coercionsDmdEnv cos

   = mkTermDmdEnv $ mapVarEnv (const topDmd) $ getUniqSet $ coVarsOfCos cos

   -- The VarSet from coVarsOfCos is really a VarEnv Var

 addVarDmd :: DmdType -> Var -> Demand -> DmdType

 addVarDmd (DmdType fv ds) var dmd

   = DmdType (addVarDmdEnv fv var dmd) ds

 -- We use this same function in SpecConstr, and Simplify.Iteration,

 -- when something binder-swap-like is happening

 scrutOkForBinderSwap (Var v)    = DoBinderSwap v MRefl

         -- Cast: see Note [Case of cast]

         -- isDictId: see Note [Care with binder-swap on dictionaries]

         -- The isDictId rejects a Constraint/Constraint binder-swap, perhaps

     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

       | -- Note [Casts and lambdas]

         seCastSwizzle env

       , not (any bad bndrs)

       where

         co_vars  = tyCoVarsOfCastCo co

         bad bndr = isCoVar bndr && bndr `elemVarSet` co_vars

 import GHC.Types.Literal( pprLiteral )

 import GHC.Types.Name( pprInfixName, pprPrefixName )

 import GHC.Types.Var

 import GHC.Types.Id

 import GHC.Types.Id.Info

 import GHC.Types.Demand

 pprOptCastCoercion :: CastCoercion -> SDoc

 pprOptCastCoercion (CCoercion co) = pprOptCo co

     where

       co_type = sdocOption sdocSuppressCoercionTypes $ \case

           True -> int (typeSize ty) <+> text "..."

 --     Note [Casts in the target]

 --     Note [Cancel reflexive casts]

     -- checkReflexiveMCo: cancel casts if possible

     -- This is important: see Note [Cancel reflexive casts]

 ------------------------ Literals ---------------------

 match _ subst (Lit lit1) (Lit lit2) mco

 import GHC.Core.Coercion.Opt ( optCoercion, OptCoercionOpts (..) )

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

                             , isInScope, substTyVarBndr, cloneTyVarBndr )

 import GHC.Core.Predicate( isCoVarType )

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

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

     go_cast_co (CCoercion co) = CCoercion (go_co co)

     go_co co = optCoercion (so_co_opts (soe_opts env)) subst co

 finish_app :: HasDebugCallStack

            => SimpleOptEnv -> OutExpr -> [SimpleClo] -> OutExpr

 -- See Note [Eliminate casts in function position]

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

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

   , Just (x',e') <- pushCoercionIntoLambda (soeInScope env) x e co

   = simple_app (soeZapSubst env) (Lam x' e') as

 finish_app env fun args

   = foldl mk_app fun args

   where

     go subst floats (Tick t expr) cont

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

             -- See Note [Push coercions in exprIsConApp_maybe]

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

     go subst floats (App fun arg) (CC args mco)

        | let arg_type = exprType arg

        , not (isTypeArg arg) && needsCaseBinding arg_type arg

     = Just (x, e, t:ts)

 -- Also possible: A casted lambda. Push the coercion inside

     | Just (x, e,ts) <- exprIsLambda_maybe ise casted_e

     -- Only do value lambdas.

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

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

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

     , Just (x',e') <- pushCoercionIntoLambda in_scope_set x e co

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

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

       res

 -- Another attempt: See if we find a partial unfolding

 exprIsLambda_maybe ise@(ISE in_scope_set id_unf) e

     | (Var f, as, ts) <- collectArgsTicks tickishFloatable e

         coVarsOfType, coVarsOfTypes,

         coVarsOfCo, coVarsOfCos,

         coVarsOfCastCo,

         tyCoVarsOfCastCoercionDSet,

         tyCoVarsOfCoDSet,

         tyCoVarsOfCoList,

         coVarsOfCoDSet, coVarsOfCosDSet,

 tyCoVarsOfCastCo :: CastCoercion -> TyCoVarSet

 tyCoVarsOfCastCo (CCoercion co)     = coVarsOfCo co

 tyCoVarsOfType :: Type -> TyCoVarSet

 -- The "deep" TyCoVars of the the type

 shallowCoVarsOfCos :: [Coercion] -> CoVarSet

 shallowCoVarsOfCos cos = filterVarSet isCoVar $ shallowTyCoVarsOfCos cos

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

 *                                                                      *

 coVarsOfCastCo :: CastCoercion -> CoVarSet

 coVarsOfCastCo (CCoercion co) = coVarsOfCo co

 -- See Note [Finding free coercion variables]

 coVarsOfType  :: Type       -> CoVarSet

 tyCoFVsOfCastCoercion :: CastCoercion -> FV

 tyCoFVsOfCastCoercion (CCoercion co) = tyCoFVsOfCo co

 tyCoFVsOfCo :: Coercion -> FV

 -- Extracts type and coercion variables from a coercion

 import GHC.Iface.Type

 import GHC.Types.Var.Set

 import GHC.Types.Var.Env

 tidyToIfaceCastCoSty :: CastCoercion -> PprStyle -> IfaceCastCoercion

 tidyToIfaceCastCoSty (CCoercion co)     sty = IfaceCCoercion (tidyToIfaceCoSty co sty)

 tidyToIfaceCoSty :: Coercion -> PprStyle -> IfaceCoercion

 tidyToIfaceCoSty co sty

 -- friends:

 import GHC.Types.Var

 import GHC.Core.TyCon

 import GHC.Core.Coercion.Axiom

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

 A "zapped cast" is a Cast that does not store the full Coercion being used to

 cast, but instead stores the type resulting from the cast and a set of CoVars

 Zapping casts is motivated by performance (see #8095 and related tickets).

 Sometimes the structure of the coercion can be very large, for example when

 using type families that take many reduction steps, and when Core Lint is

 not being used, the full structure of the coercion is not needed.  We merely

 need the result type (to support exprType) and the set of coercion variables

 Zapped casts are introduced in exactly one place: finish_rewrite in

 GHC.Tc.Solver.Solve. This uses a heuristic (isSmallCo) to determine whether

 This arises in practice with the Rep type family from GHC Generics.

 The `-fzap-casts` and `-fno-zap-casts` flags can be used to enable or disable

 cast zapping, for comparative performance testing or to ensure casts are not

 TODO: probably the boot libraries ought to be distributed with `-fno-zap-casts`,

 so users can get full checks from `-dcore-lint`.

 -}

 -- and free CoVars.  See Note [Zapped casts].

 data CastCoercion

   = CCoercion CoercionR        -- Not zapped; the Coercion has Representational role

   deriving Data.Data

 -- | A 'Coercion' is concrete evidence of the equality/convertibility

 castCoercionSize :: CastCoercion -> Int

 castCoercionSize (CCoercion co) = coercionSize co

 coercionSize :: Coercion -> Int

 coercionSize (Refl ty)             = typeSize ty

         substTyUnchecked, substTysUnchecked, substScaledTysUnchecked, substThetaUnchecked,

         substTyWithUnchecked, substScaledTyUnchecked,

         substCoUnchecked, substCoWithUnchecked,

         substTyWithInScope,

         substTys, substScaledTys, substTheta,

         lookupTyVar,

     lookupVarEnv tenv tv

 substCastCo :: HasDebugCallStack => Subst -> CastCoercion -> CastCoercion

 -- | Substitute within a 'Coercion'

 -- The substitution has to satisfy the invariants described in

 import GHC.Types.Name hiding (varName)

 import GHC.Types.Var

 import GHC.Types.Var.Env

 import GHC.Utils.Misc (strictMap)

 import Data.List (mapAccumL)

 tidyCastCo :: TidyEnv -> CastCoercion -> CastCoercion

 tidyCastCo env (CCoercion co) = CCoercion (tidyCo env co)

 import GHC.Core.Predicate( isCoVarType )

 import GHC.Core.FamInstEnv

 import GHC.Core.TyCo.Compare( eqType, eqTypeX )

 import GHC.Core.Coercion

 import GHC.Core.Reduction

 import GHC.Core.TyCon

 -- | Wrap the given expression in a zapped cast (see Note [Zapped casts] in

 -- GHC.Core.TyCo.Rep).

 mkCastZ expr ty cos =

     case expr of

       Tick t expr -> Tick t (mkCastZ expr ty cos)

 import GHC.Types.Demand ( isNopSig )

 import GHC.Types.Cpr ( topCprSig )

 import GHC.Types.SrcLoc (unLoc)

 import GHC.Utils.Outputable

 import GHC.Utils.Panic

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

 toIfaceCastCoercion :: CastCoercion -> IfaceCastCoercion

 toIfaceCastCoercion (CCoercion co) = IfaceCCoercion (toIfaceCoercion co)

 toIfaceCoercion :: Coercion -> IfaceCoercion

 toIfaceCoercion = toIfaceCoercionX emptyVarSet

 import GHC.Core.Coercion

 import GHC.Core.Coercion.Axiom

 import GHC.Core.FVs

 import GHC.Core.TyCo.Rep    -- needs to build types & coercions in a knot

 import GHC.Core.TyCo.Subst ( substTyCoVars )

 import GHC.Core.InstEnv

 tcIfaceCastCoercion :: IfaceCastCoercion -> IfL CastCoercion

 tcIfaceCastCoercion (IfaceCCoercion co)     = CCoercion <$> tcIfaceCo co

 tcIfaceCo :: IfaceCoercion -> IfL Coercion

 tcIfaceCo = go

 import GHC.Core.Reduction

 import GHC.Core.Coercion

 import GHC.Core.Class( classHasSCs )

 import GHC.Core.TyCo.Rep (Coercion(..))

 import GHC.Types.Id(  idType )

 mkCastCoercion :: Bool -> Type -> Coercion -> CastCoercion

 mkCastCoercion zap_casts lhs_ty co

    | isSmallCo co || not zap_casts = CCoercion co