where

     Pair ty1 ty2 = coVarTypes cv1

           -- cv1 might have a substituted kind!

 opt_co4' _ _ _ _ (HoleCo h)

         -- Check the let-can-float invariant

         -- See Note [Core let-can-float invariant] in GHC.Core

          -- Check that a join-point binder has a valid type

          -- NB: lintIdBinder has checked that it is not top-level bound

             JoinPoint arity ->  checkL (isValidJoinPointType arity binder_ty)

                                        (mkInvalidJoinPointMsg binder binder_ty)

        ; when (lf_check_inline_loop_breakers flags

                && isStableUnfolding (realIdUnfolding binder)

                && isStrongLoopBreaker (idOccInfo binder)

         -- We should check the unfolding, if any, but this is tricky because

         -- the unfolding is a SimplifiableCoreExpr. Give up for now.

 -- | Checks the RHS of bindings. It only differs from 'lintCoreExpr'

 -- in that it doesn't reject occurrences of the function 'makeStatic' when they

 -- appear at the top level and @lf_check_static_ptrs == AllowAtTopLevel@, and

      hsep [text "Binder's type:", ppr (idType binder)],

      hsep [text "Rhs type:", ppr ty]]

 mkNonTopExportedMsg :: Id -> SDoc

 mkNonTopExportedMsg binder

   = hsep [text "Non-top-level binder is marked as exported:", ppr binder]

 mkNonTopExternalNameMsg binder

   = hsep [text "Non-top-level binder has an external name:", ppr binder]

 mkKindErrMsg :: TyVar -> Type -> SDoc

 mkKindErrMsg tyvar arg_ty

   = vcat [text "Kinds don't match in type application:",

 reSimplifying (SimplEnv { seInlineDepth = n }) = n>0

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

 extendIdSubst env@(SimplEnv {seIdSubst = subst}) var res

   = assertPpr (isId var && not (isCoVar var)) (ppr var) $

     env { seIdSubst = extendVarEnv subst var res }

 mkRecFloats :: SimplFloats -> SimplFloats

 -- Flattens the floats into a single Rec group,

 -- They must either all be lifted LetFloats or all JoinFloats

 mkRecFloats floats@(SimplFloats { sfLetFloats  = LetFloats bs _ff

                                 , sfJoinFloats = jbs

                                 , sfInScope    = in_scope })

     flatten_rec :: OrdList OutBind -> OrdList OutBind

     -- Put CoVar bindings first (guaranteed non-recursive)

     -- then one recursive value binding

 wrapFloats :: SimplFloats -> OutExpr -> OutExpr

 -- Wrap the floats around the expression

         --

         -- See also Note [In-scope set as a substitution] in GHC.Core.Opt.Simplify.

 lookupRecBndr :: SimplEnv -> InId -> OutId

 -- Look up an Id which has been put into the envt by simplRecBndrs,

 -- but where we have not yet done its RHS

         (Subst in_scope' _ tv_env' cv_env', cv')

            -> (env { seInScope = in_scope', seTvSubst = tv_env', seCvSubst = cv_env' }, cv')

 substCo env co = Coercion.substCo (getTCvSubst env) co

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

         = do { (env', bndr') <- addBndrRules env bndr (lookupRecBndr env bndr) bind_cxt

              ; return (env', (bndr, bndr', rhs)) }

     go env [] = return (emptyFloats env, env)

     go env ((old_bndr, new_bndr, rhs) : pairs)

              ; (floats, env2) <- go env1 pairs

              ; return (float `addFloats` floats, env2) }

        ; simplTrace "makeTrivial:co" (ppr (Cast triv_expr triv_co)) $

          return (floats1 `addLetFlts` floats2, Cast triv_expr triv_co) }

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

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

         ; uniq <- getUniqueM

 -- Binder /can/ be a JoinId

 -- Precondition: rhs obeys the let-can-float invariant

 completeBind bind_cxt (old_bndr, unf_se) (new_bndr, new_rhs, env)

  = assert (isId new_bndr) $

    do { let old_info = idInfo old_bndr

             old_unf  = realUnfoldingInfo old_info

                    return ( emptyFloats env

                           , extendIdSubst env old_bndr $

                             DoneEx unf_rhs (idJoinPointHood new_bndr)) }

         else -- Keep the binding; do cast worker/wrapper

 --             simplTrace "completeBind" (vcat [ text "bndrs" <+> ppr old_bndr <+> ppr new_bndr

 import GHC.Core.Unfold

 import GHC.Core.Unfold.Make

 import GHC.Core.Opt.Simplify.Monad

 import GHC.Core.Coercion hiding( substCo )

 import GHC.Core.DataCon ( dataConWorkId, isNullaryRepDataCon )

 import GHC.Core.Multiplicity

   | not pre_inline_unconditionally           = Nothing

   | not active                               = Nothing

   | isTopLevel top_lvl && isDeadEndId bndr   = Nothing -- Note [Top-level bottoming Ids]

   | isExitJoinId bndr                        = Nothing -- Note [Do not inline exit join points]

                                                        -- in module Exitify

   | not (one_occ (idOccInfo bndr))           = Nothing

   | otherwise                                = Nothing

   where

     unf = idUnfolding bndr

     one_occ IAmDead = True -- Happens in ((\x.1) v)

     one_occ OneOcc{ occ_n_br   = 1

         -- canInlineInLam => free vars of rhs are (Once in_lam) or Many,

         -- so substituting rhs inside a lambda doesn't change the occ info.

         -- Sadly, not quite the same as exprIsHNF.

       -- not ticks.  Counting ticks cannot be duplicated, and non-counting

       -- ticks around a Lam will disappear anyway.

   | 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

   where

     do_tcv is v = EndoOS do_it

       where

                   | v `elemVarSet` acc = acc

                   | otherwise          = appEndoOS (deep_ty (varType v)) $

                                          acc `extendVarSet` v

   where

     do_tcv is v = EndoOS do_it

       where

                   | v `elemVarSet` acc = acc

                   | otherwise          = acc `extendVarSet` v

     do_covar is v = EndoOS do_it

       where

                   | v `elemVarSet` acc = acc

                   | otherwise          = appEndoOS (deep_cv_ty (varType v)) $

                                          acc `extendVarSet` v

 tyCoFVsOfCoVar :: CoVar -> FV

 tyCoFVsOfCoVar v fv_cand in_scope acc

   = (unitFV v `unionFV` tyCoFVsOfType (varType v)) fv_cand in_scope acc

 tyCoFVsOfCos :: [Coercion] -> FV

 tyCoFVsOfCos []       fv_cand in_scope acc = emptyFV fv_cand in_scope acc

       subst2 = extendIdSubstList subst1 [(id, Var id') | (id,id') <- prs]

 extendCorePrepEnvExpr :: CorePrepEnv -> Id -> CoreExpr -> CorePrepEnv

 extendCorePrepEnvExpr cpe id expr

 lookupCorePrepEnv :: CorePrepEnv -> Id -> CoreExpr

 lookupCorePrepEnv cpe id

         -- ** Operations on InScopeSets

         emptyInScopeSet, mkInScopeSet, mkInScopeSetList, delInScopeSet,

         extendInScopeSet, extendInScopeSetList, extendInScopeSetSet,

         unionInScope, elemInScopeSet, uniqAway,

         unsafeGetFreshLocalUnique,

         -- * The RnEnv2 type

 varSetInScope :: VarSet -> InScopeSet -> Bool

 varSetInScope vars (InScope s1) = vars `subVarSet` s1

 {-

 Note [Local uniques]

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

     , "fully_static"     =: fullyStatic

     , "host_fully_static" =: hostFullyStatic

     , "collect_timings"  =: collectTimings

     , "debug_ghc"        =: debugGhc Stage2

     , "debug_stage1_ghc" =: debugGhc Stage1

     , "lint"             =: enableLinting

   ? arg "-fprof-late"

 -- | Enable assertions for the stage2 compiler

   where

 -- | Build the stage3 compiler using the non-moving GC.

 enableBootNonmovingGc :: Flavour -> Flavour