{-

 (c) The University of Glasgow 2006

 -}

         coercionType, mkCoercionType,

         coercionKind, coercionLKind, coercionRKind,coercionKinds,

         coercionRole, coercionKindRole,

         -- ** Constructing coercions

         mkGReflCo, mkGReflMCo, mkReflCo, mkRepReflCo, mkNomReflCo,

 import Data.List.NonEmpty ( NonEmpty (..) )

 import Control.DeepSeq

 {-

 %************************************************************************

 %*                                                                      *

 seqCos []       = ()

 seqCos (co:cos) = seqCo co `seq` seqCos cos

 {-

 %************************************************************************

 %*                                                                      *

   where

     flag (Rec {})                = FltLifted

     flag (NonRec bndr rhs)

       | exprOkForSpeculation rhs = FltOkSpec  -- Unlifted, and lifted but ok-for-spec (eg HNF)

       | otherwise                = FltCareful

               work_id   = mkLocalIdWithInfo work_name ManyTy work_ty work_info

               is_strict = isStrictId bndr

         ; (rhs_floats, work_rhs) <- prepareBinding env top_lvl is_rec is_strict

                                                    work_id (emptyFloats env) rhs

         ; work_unf <- mk_worker_unfolding top_lvl work_id work_rhs

         ; let  work_id_w_unf = work_id `setIdUnfolding` work_unf

         ; if postInlineUnconditionally env bind_cxt old_bndr bndr triv_rhs

              -- Almost always True, because the RHS is trivial

        ; let all_floats = rhs_floats1 `addLetFloats` anf_floats

        ; if doFloatFromRhs (seFloatEnable env) top_lvl is_rec strict_bind all_floats rhs2

          then -- Float!

               do { tick LetFloatFromLet

                  ; return (all_floats, rhs2) }

          else -- Abandon floating altogether; revert to original rhs

               -- Since we have already built rhs1, we just need to add

               -- rhs_floats1 to it

               return (emptyFloats env, wrapFloats rhs_floats1 rhs1) }

 {- Note [prepareRhs]

 --            x = Just a

 -- See Note [prepareRhs]

 prepareRhs env top_lvl occ rhs0

   | otherwise     = return (emptyLetFloats, rhs0)

   where

     -- We can't use exprIsExpandable because the WHOLE POINT is that

     -- just say no!

     is_expandable = go rhs0 0

        where

          go (App fun arg) n_val_args

            | isTypeArg arg             = go fun n_val_args

            | otherwise                 = go fun (n_val_args + 1)

     anfise :: OutExpr -> SimplM (LetFloats, OutExpr)

     anfise (Cast rhs co)

     anfise (App fun (Type ty))

         = do { (floats, rhs') <- anfise fun

              ; return (floats, App rhs' (Type ty)) }

 -- For the Demand argument, see Note [Keeping demand info in StrictArg Plan A]

 makeTrivial env top_lvl dmd occ_fs expr

   | exprIsTrivial expr                          -- Already trivial

   | Cast expr' co <- expr

   | otherwise -- 'expr' is not of form (Cast e co)

   = do  { (floats, expr1) <- prepareRhs env top_lvl occ_fs expr

     id_info = vanillaIdInfo `setDemandInfo` dmd

     expr_ty = exprType expr

 bindingOk :: TopLevelFlag -> CoreExpr -> Type -> Bool

 -- True iff we can have a binding of this expression at this level

 -- Precondition: the type is the type of the expression

   | Just env' <- preInlineUnconditionally env NotTopLevel bndr rhs env

     -- Because of the let-can-float invariant, it's ok to

     -- inline freely, or to drop the binding if it is dead.

          tick (PreInlineUnconditionally bndr)

        ; simplExprF env' body cont }

        ; simplLam (extendTvSubst env bndr arg_ty) body cont }

 -- Coercion beta-reduction

 -- Value beta-reduction

 -- This works for /coercion/ lambdas too

             , not ( isSimplified dup &&  -- See (SR2) in Note [Avoiding simplifying repeatedly]

                     not (exprIsTrivial arg) &&

                     not (isDeadOcc (idOccInfo bndr)) )

                     tick (PreInlineUnconditionally bndr)

                   ; simplLam env' body cont }

       = assert (isTyVar b )

         bind_args (extendTvSubst env' b ty) bs' args

     bind_args env' (b:bs') (arg : args)

       = assert (isId b) $

   | isStableUnfolding unfolding = False -- Note [Stable unfoldings and postInlineUnconditionally]

   | isTopLevel (bindContextLevel bind_cxt)

                                 = False -- Note [Top level and postInlineUnconditionally]

   | exprIsTrivial rhs           = True

   | BC_Join {} <- bind_cxt      = False -- See point (1) of Note [Duplicating join points]

                                         --     in GHC.Core.Opt.Simplify.Iteration

 ppr_expr add_par (Var id)      = ppr_id_occ add_par id

 ppr_expr add_par (Type ty)     = add_par (text "TYPE:" <+> ppr ty)       -- Weird

 ppr_expr add_par (Lit lit)     = pprLiteral add_par lit

 ppr_expr add_par (Cast expr co)

 type CoercionR = Coercion       -- always Representational

 type CoercionP = Coercion       -- always Phantom

 type MCoercionR = MCoercion     -- always Representational

 {- Note [KindCoercion]

 -}

 {-# INLINE trivial_expr_fold #-}

 -- ^ The worker function for Note [exprIsTrivial] and Note [getIdFromTrivialExpr]

 -- This is meant to have the code of both functions in one place and make it

 -- easy to derive custom predicates.

 --

 -- * returns (k_id x) if `e` is a variable `x` (with trivial wrapping)

 -- * returns (k_lit x) if `e` is a trivial literal `l` (with trivial wrapping)

 -- * returns k_not_triv otherwise

 --

 -- where "trivial wrapping" is

 -- * Type application or abstraction

 -- * Ticks other than `tickishIsCode`

 -- * `case e of {}` an empty case

   where

     -- If you change this function, be sure to change

     -- SetLevels.notWorthFloating as well!

     -- (Or yet better: Come up with a way to share code with this function.)

     go (Var v)                            = k_id v  -- See Note [Variables are trivial]

     go (Lit l)    | litIsTrivial l        = k_lit l

     go (App f arg)

       | not (isRuntimeArg arg)            = go f

       | exprIsUnaryClassFun f             = go arg

       | otherwise                         = k_not_triv

     go (Lam b e)  | not (isRuntimeVar b)  = go e

     go (Tick t e) | not (tickishIsCode t) = go e              -- See Note [Tick trivial]

     go (Case e b _ as)

       | null as

       = go e     -- See Note [Empty case is trivial]

     go _                                  = k_not_triv

 exprIsTrivial :: CoreExpr -> Bool

 {-

 Note [getIdFromTrivialExpr]

 getIdFromTrivialExpr :: HasDebugCallStack => CoreExpr -> Id

 -- See Note [getIdFromTrivialExpr]

   where

     panic = pprPanic "getIdFromTrivialExpr" (ppr e)

 getIdFromTrivialExpr_maybe :: CoreExpr -> Maybe Id

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

 *                                                                      *

     -- as the latter would panic.

   || exprIsTickedString expr

 -- | Check if the expression is zero or more Ticks wrapped around a literal

 -- string.

 exprIsTickedString :: CoreExpr -> Bool

 -- CoreArgs may not immediately look trivial, e.g., `case e of {}` or

 -- `case unsafeequalityProof of UnsafeRefl -> e` might intervene.

 -- Good thing we can just call `trivial_expr_fold` here.

   where

     panic = pprPanic "getStgArgFromTrivialArg" (ppr e)

 coreToStgArgs :: [CoreArg] -> CtsM ([StgArg], [StgTickish])