Drop the app invariantghc-9.5-start

previously, GHC had the "let/app-invariant" which said that the RHS of a
let or the argument of an application must be of lifted type or ok for
speculation. We want this on let to freely float them around, and we
wanted that on app to freely convert between the two (e.g. in
beta-reduction or inlining).

However, the app invariant meant that simple code didn't stay simple and
this got in the way of rules matching. By removing the app invariant,
this thus fixes #20554.

The new invariant is now called "let-can-float invariant", which is
hopefully easier to guess its meaning correctly.

Dropping the app invariant means that everywhere where we effectively do
beta-reduction (in the two simplifiers, but also in `exprIsConApp_maybe`
and other innocent looking places) we now have to check if the argument
must be evaluated (unlifted and side-effecting), and analyses have to be
adjusted to the new semantics of `App`.

Also, `LetFloats` in the simplifier can now also carry such non-floating
bindings.

The fix for DmdAnal, refine by Sebastian, makes functions with unlifted
arguments strict in these arguments, which changes some signatures.

This causes some extra calls to `exprType` and `exprOkForSpeculation`,
so some perf benchmarks regress a bit (while others improve).

Metric Decrease:
    T9020
Metric Increase:
    LargeRecord
    T12545
    T15164
    T16577
    T18223
    T5642
    T9961

Co-authored-by: Sebastian Graf <sebastian.graf@kit.edu>

23 files changed, 383 insertions, 271 deletions

diff --git a/compiler/GHC/Builtin/PrimOps.hs b/compiler/GHC/Builtin/PrimOps.hs
index d1df0fbaf2..574cfa4659 100644
--- a/compiler/GHC/Builtin/PrimOps.hs
+++ b/compiler/GHC/Builtin/PrimOps.hs
@@ -325,8 +325,8 @@ Note [Checking versus non-checking primops]
       never throw an exception, so we cannot rewrite to a call to error.
 
   It is important that a non-checking primop never be transformed in a way that
-  would cause it to bottom. Doing so would violate Core's let/app invariant
-  (see Note [Core let/app invariant] in GHC.Core) which is critical to
+  would cause it to bottom. Doing so would violate Core's let-can-float invariant
+  (see Note [Core let-can-float invariant] in GHC.Core) which is critical to
   the simplifier's ability to float without fear of changing program meaning.
 
 
@@ -479,7 +479,7 @@ Two main predicates on primops test these flags:
   * The "no-float-out" thing is achieved by ensuring that we never
     let-bind a can_fail or has_side_effects primop.  The RHS of a
     let-binding (which can float in and out freely) satisfies
-    exprOkForSpeculation; this is the let/app invariant.  And
+    exprOkForSpeculation; this is the let-can-float invariant.  And
     exprOkForSpeculation is false of can_fail and has_side_effects.
 
   * So can_fail and has_side_effects primops will appear only as the
diff --git a/compiler/GHC/Builtin/primops.txt.pp b/compiler/GHC/Builtin/primops.txt.pp
index 0c2671ee81..d21d6a1f6f 100644
--- a/compiler/GHC/Builtin/primops.txt.pp
+++ b/compiler/GHC/Builtin/primops.txt.pp
@@ -3173,7 +3173,7 @@ primop  ReallyUnsafePtrEqualityOp "reallyUnsafePtrEquality#" GenPrimOp
 -- unnecessarily conservative, but it prevented reallyUnsafePtrEquality# from
 -- floating out of places where its arguments were known to be forced.
 -- Unfortunately, GHC could sometimes lose track of whether those arguments
--- were forced, leading to let/app invariant failures (see #13027 and the
+-- were forced, leading to let-can-float invariant failures (see #13027 and the
 -- discussion in #11444). Now that ok_for_speculation skips over lifted
 -- arguments, we need to explicitly prevent reallyUnsafePtrEquality#
 -- from floating out. Imagine if we had
@@ -3788,7 +3788,7 @@ section "Prefetch"
   to reflect that these operations have side effects with respect to the runtime
   performance characteristics of the resulting code. Additionally, if the prefetchValue
   operations did not have this attribute, GHC does a float out transformation that
-  results in a let/app violation, at least with the current design.
+  results in a let-can-float invariant violation, at least with the current design.
   }
 
 
diff --git a/compiler/GHC/Core.hs b/compiler/GHC/Core.hs
index c5d0a86d14..e82f0b2d8a 100644
--- a/compiler/GHC/Core.hs
+++ b/compiler/GHC/Core.hs
@@ -175,7 +175,6 @@ These data types are the heart of the compiler
 -- *  Primitive literals
 --
 -- *  Applications: note that the argument may be a 'Type'.
---    See Note [Core let/app invariant]
 --    See Note [Representation polymorphism invariants]
 --
 -- *  Lambda abstraction
@@ -186,7 +185,7 @@ These data types are the heart of the compiler
 --    bound and then executing the sub-expression.
 --
 --    See Note [Core letrec invariant]
---    See Note [Core let/app invariant]
+--    See Note [Core let-can-float invariant]
 --    See Note [Representation polymorphism invariants]
 --    See Note [Core type and coercion invariant]
 --
@@ -421,11 +420,11 @@ parts of the compilation pipeline.
   in the object file, the content of the exported literal is given a label with
   the _bytes suffix.
 
-Note [Core let/app invariant]
+Note [Core let-can-float invariant]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-The let/app invariant
-     the right hand side of a non-recursive 'Let', and
-     the argument of an 'App',
+The let-can-float invariant:
+
+    The right hand side of a non-recursive 'Let'
     /may/ be of unlifted type, but only if
     the expression is ok-for-speculation
     or the 'Let' is for a join point.
@@ -445,12 +444,29 @@ In this situation you should use @case@ rather than a @let@. The function
 alternatively use 'GHC.Core.Make.mkCoreLet' rather than this constructor directly,
 which will generate a @case@ if necessary
 
-The let/app invariant is initially enforced by mkCoreLet and mkCoreApp in
-GHC.Core.Make.
+The let-can-float invariant is initially enforced by mkCoreLet in GHC.Core.Make.
 
-For discussion of some implications of the let/app invariant primops see
+For discussion of some implications of the let-can-float invariant primops see
 Note [Checking versus non-checking primops] in GHC.Builtin.PrimOps.
 
+Historical Note [The let/app invariant]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Before 2022 GHC used the "let/app invariant", which applied the let-can-float rules
+to the argument of an application, as well as to the RHS of a let.  This made some
+kind of sense, because 'let' can always be encoded as application:
+   let x=rhs in b   =    (\x.b) rhs
+
+But the let/app invariant got in the way of RULES; see #19313.  For example
+  up :: Int# -> Int#
+  {-# RULES "up/down" forall x. up (down x) = x #-}
+The LHS of this rule doesn't satisfy the let/app invariant.
+
+Indeed RULES is a big reason that GHC doesn't use ANF, where the argument of an
+application is always a variable or a constant.  To allow RULES to work nicely
+we need to allow lots of things in the arguments of a call.
+
+TL;DR: we relaxed the let/app invariant to become the let-can-float invariant.
+
 Note [Case expression invariants]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Case expressions are one of the more complicated elements of the Core
@@ -749,7 +765,7 @@ Join points must follow these invariants:
 However, join points have simpler invariants in other ways
 
   5. A join point can have an unboxed type without the RHS being
-     ok-for-speculation (i.e. drop the let/app invariant)
+     ok-for-speculation (i.e. drop the let-can-float invariant)
      e.g.  let j :: Int# = factorial x in ...
 
   6. The RHS of join point is not required to have a fixed runtime representation,
@@ -1846,8 +1862,8 @@ mkDoubleLit       d = Lit (mkLitDouble d)
 mkDoubleLitDouble d = Lit (mkLitDouble (toRational d))
 
 -- | Bind all supplied binding groups over an expression in a nested let expression. Assumes
--- that the rhs satisfies the let/app invariant.  Prefer to use 'GHC.Core.Make.mkCoreLets' if
--- possible, which does guarantee the invariant
+-- that the rhs satisfies the let-can-float invariant.  Prefer to use
+-- 'GHC.Core.Make.mkCoreLets' if possible, which does guarantee the invariant
 mkLets        :: [Bind b] -> Expr b -> Expr b
 -- | Bind all supplied binders over an expression in a nested lambda expression. Prefer to
 -- use 'GHC.Core.Make.mkCoreLams' if possible
diff --git a/compiler/GHC/Core/Lint.hs b/compiler/GHC/Core/Lint.hs
index 6390d83b1e..8ee39cbe88 100644
--- a/compiler/GHC/Core/Lint.hs
+++ b/compiler/GHC/Core/Lint.hs
@@ -631,8 +631,8 @@ lintLetBind top_lvl rec_flag binder rhs rhs_ty
        ; checkL (not (isCoVar binder) || isCoArg rhs)
                 (mkLetErr binder rhs)
 
-        -- Check the let/app invariant
-        -- See Note [Core let/app invariant] in GHC.Core
+        -- Check the let-can-float invariant
+        -- See Note [Core let-can-float invariant] in GHC.Core
        ; checkL ( isJoinId binder
                || mightBeLiftedType binder_ty
                || (isNonRec rec_flag && exprOkForSpeculation rhs)
@@ -1285,10 +1285,7 @@ lintCoreArg (fun_ty, fun_ue) arg
          do { checkL (typeHasFixedRuntimeRep arg_ty)
                      (text "Argument does not have a fixed runtime representation"
                       <+> ppr arg <+> dcolon
-                      <+> parens (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty)))
-
-            ; checkL (mightBeLiftedType arg_ty || exprOkForSpeculation arg)
-                     (mkLetAppMsg arg) }
+                      <+> parens (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))) }
 
        ; lintValApp arg fun_ty arg_ty fun_ue arg_ue }
 
@@ -3267,11 +3264,6 @@ mkRhsMsg binder what ty
      hsep [text "Binder's type:", ppr (idType binder)],
      hsep [text "Rhs type:", ppr ty]]
 
-mkLetAppMsg :: CoreExpr -> SDoc
-mkLetAppMsg e
-  = hang (text "This argument does not satisfy the let/app invariant:")
-       2 (ppr e)
-
 badBndrTyMsg :: Id -> SDoc -> SDoc
 badBndrTyMsg binder what
   = vcat [ text "The type of this binder is" <+> what <> colon <+> ppr binder
diff --git a/compiler/GHC/Core/Make.hs b/compiler/GHC/Core/Make.hs
index 932bf8aa8d..fe0f289026 100644
--- a/compiler/GHC/Core/Make.hs
+++ b/compiler/GHC/Core/Make.hs
@@ -71,7 +71,7 @@ import GHC.Types.Literal
 import GHC.Types.Unique.Supply
 
 import GHC.Core
-import GHC.Core.Utils ( exprType, needsCaseBinding, mkSingleAltCase, bindNonRec )
+import GHC.Core.Utils ( exprType, mkSingleAltCase, bindNonRec )
 import GHC.Core.Type
 import GHC.Core.Coercion ( isCoVar )
 import GHC.Core.DataCon  ( DataCon, dataConWorkId )
@@ -115,9 +115,9 @@ sortQuantVars vs = sorted_tcvs ++ ids
     sorted_tcvs = scopedSort tcvs
 
 -- | Bind a binding group over an expression, using a @let@ or @case@ as
--- appropriate (see "GHC.Core#let_app_invariant")
+-- appropriate (see "GHC.Core#let_can_float_invariant")
 mkCoreLet :: CoreBind -> CoreExpr -> CoreExpr
-mkCoreLet (NonRec bndr rhs) body        -- See Note [Core let/app invariant]
+mkCoreLet (NonRec bndr rhs) body        -- See Note [Core let-can-float invariant]
   = bindNonRec bndr rhs body
 mkCoreLet bind body
   = Let bind body
@@ -141,9 +141,6 @@ mkCoreConApps con args = mkCoreApps (Var (dataConWorkId con)) args
 
 -- | Construct an expression which represents the application of a number of
 -- expressions to another. The leftmost expression in the list is applied first
---
--- Respects the let/app invariant by building a case expression where necessary
---   See Note [Core let/app invariant] in "GHC.Core"
 mkCoreApps :: CoreExpr -- ^ function
            -> [CoreExpr] -- ^ arguments
            -> CoreExpr
@@ -156,9 +153,6 @@ mkCoreApps fun args
 
 -- | Construct an expression which represents the application of one expression
 -- to the other
---
--- Respects the let/app invariant by building a case expression where necessary
---   See Note [Core let/app invariant] in "GHC.Core"
 mkCoreApp :: SDoc
           -> CoreExpr -- ^ function
           -> CoreExpr -- ^ argument
@@ -170,9 +164,6 @@ mkCoreApp s fun arg
 -- paired with its type to an argument. The result is paired with its type. This
 -- function is not exported and used in the definition of 'mkCoreApp' and
 -- 'mkCoreApps'.
---
--- Respects the let/app invariant by building a case expression where necessary
---   See Note [Core let/app invariant] in "GHC.Core"
 mkCoreAppTyped :: SDoc -> (CoreExpr, Type) -> CoreExpr -> (CoreExpr, Type)
 mkCoreAppTyped _ (fun, fun_ty) (Type ty)
   = (App fun (Type ty), piResultTy fun_ty ty)
@@ -180,20 +171,9 @@ mkCoreAppTyped _ (fun, fun_ty) (Coercion co)
   = (App fun (Coercion co), funResultTy fun_ty)
 mkCoreAppTyped d (fun, fun_ty) arg
   = assertPpr (isFunTy fun_ty) (ppr fun $$ ppr arg $$ d)
-    (mkValApp fun arg (Scaled mult arg_ty) res_ty, res_ty)
+    (App fun arg, res_ty)
   where
-    (mult, arg_ty, res_ty) = splitFunTy fun_ty
-
--- | Build an application (e1 e2),
--- or a strict binding  (case e2 of x -> e1 x)
--- using the latter when necessary to respect the let/app invariant
---   See Note [Core let/app invariant] in GHC.Core
-mkValApp :: CoreExpr -> CoreExpr -> Scaled Type -> Type -> CoreExpr
-mkValApp fun arg (Scaled w arg_ty) res_ty
-  | not (needsCaseBinding arg_ty arg)
-  = App fun arg                -- The vastly common case
-  | otherwise
-  = mkStrictApp fun arg (Scaled w arg_ty) res_ty
+    (_mult, _arg_ty, res_ty) = splitFunTy fun_ty
 
 {- *********************************************************************
 *                                                                      *
@@ -225,25 +205,6 @@ mkWildCase :: CoreExpr -- ^ scrutinee
 mkWildCase scrut (Scaled w scrut_ty) res_ty alts
   = Case scrut (mkWildValBinder w scrut_ty) res_ty alts
 
--- | Build a strict application (case e2 of x -> e1 x)
-mkStrictApp :: CoreExpr -> CoreExpr -> Scaled Type -> Type -> CoreExpr
-mkStrictApp fun arg (Scaled w arg_ty) res_ty
-  = Case arg arg_id res_ty [Alt DEFAULT [] (App fun (Var arg_id))]
-       -- mkDefaultCase looks attractive here, and would be sound.
-       -- But it uses (exprType alt_rhs) to compute the result type,
-       -- whereas here we already know that the result type is res_ty
-  where
-    arg_id = mkWildValBinder w arg_ty
-        -- Lots of shadowing, but it doesn't matter,
-        -- because 'fun' and 'res_ty' should not have a free wild-id
-        --
-        -- This is Dangerous.  But this is the only place we play this
-        -- game, mkStrictApp returns an expression that does not have
-        -- a free wild-id.  So the only way 'fun' could get a free wild-id
-        -- would be if you take apart this case expression (or some other
-        -- expression that uses mkWildValBinder, of which there are not
-        -- many), and pass a fragment of it as the fun part of a 'mkStrictApp'.
-
 mkIfThenElse :: CoreExpr -- ^ guard
              -> CoreExpr -- ^ then
              -> CoreExpr -- ^ else
diff --git a/compiler/GHC/Core/Opt/CSE.hs b/compiler/GHC/Core/Opt/CSE.hs
index 4f6917d554..e51e2cb0ce 100644
--- a/compiler/GHC/Core/Opt/CSE.hs
+++ b/compiler/GHC/Core/Opt/CSE.hs
@@ -273,8 +273,8 @@ all trivial expressions. Consider
    case x |> co of (y::Array# Int) { ... }
 
 We do not want to extend the substitution with (y -> x |> co); since y
-is of unlifted type, this would destroy the let/app invariant if (x |>
-co) was not ok-for-speculation.
+is of unlifted type, this would destroy the let-can-float invariant if
+(x |> co) was not ok-for-speculation.
 
 But surely (x |> co) is ok-for-speculation, because it's a trivial
 expression, and x's type is also unlifted, presumably.  Well, maybe
diff --git a/compiler/GHC/Core/Opt/ConstantFold.hs b/compiler/GHC/Core/Opt/ConstantFold.hs
index bb44ed4bd5..8c372d3396 100644
--- a/compiler/GHC/Core/Opt/ConstantFold.hs
+++ b/compiler/GHC/Core/Opt/ConstantFold.hs
@@ -1414,11 +1414,11 @@ as follows:
     let x = I# (error "invalid shift")
     in ...
 
-This was originally done in the fix to #16449 but this breaks the let/app
-invariant (see Note [Core let/app invariant] in GHC.Core) as noted in #16742.
-For the reasons discussed in Note [Checking versus non-checking primops] (in
-the PrimOp module) there is no safe way rewrite the argument of I# such that
-it bottoms.
+This was originally done in the fix to #16449 but this breaks the let-can-float
+invariant (see Note [Core let-can-float invariant] in GHC.Core) as noted in
+#16742. For the reasons discussed in Note [Checking versus non-checking
+primops] (in the PrimOp module) there is no safe way to rewrite the argument of I#
+such that it bottoms.
 
 Consequently we instead take advantage of the fact that large shifts are
 undefined behavior (see associated documentation in primops.txt.pp) and
diff --git a/compiler/GHC/Core/Opt/DmdAnal.hs b/compiler/GHC/Core/Opt/DmdAnal.hs
index 945af5ea9e..ca51fd5f4c 100644
--- a/compiler/GHC/Core/Opt/DmdAnal.hs
+++ b/compiler/GHC/Core/Opt/DmdAnal.hs
@@ -285,7 +285,7 @@ dmdAnalBindLetUp top_lvl env id rhs anal_body = WithDmdType final_ty (R (NonRec
 
     id_dmd'            = finaliseLetBoxity (ae_fam_envs env) (idType id) id_dmd
     !id'               = setBindIdDemandInfo top_lvl id id_dmd'
-    (rhs_ty, rhs')     = dmdAnalStar env (dmdTransformThunkDmd rhs id_dmd') rhs
+    (rhs_ty, rhs')     = dmdAnalStar env id_dmd' rhs
 
     -- See Note [Absence analysis for stable unfoldings and RULES]
     rule_fvs           = bndrRuleAndUnfoldingIds id
@@ -335,27 +335,33 @@ dmdAnalBindLetDown top_lvl env dmd bind anal_body = case bind of
         -- the vanilla call demand seem to be due to (b).  So we don't
         -- bother to re-analyse the RHS.
 
--- If e is complicated enough to become a thunk, its contents will be evaluated
--- at most once, so oneify it.
-dmdTransformThunkDmd :: CoreExpr -> Demand -> Demand
-dmdTransformThunkDmd e
-  | exprIsTrivial e = id
-  | otherwise       = oneifyDmd
+-- | Mimic the effect of 'GHC.Core.Prep.mkFloat', turning non-trivial argument
+-- expressions/RHSs into a proper let-bound thunk (lifted) or a case (with
+-- unlifted scrutinee).
+anticipateANF :: CoreExpr -> Card -> Card
+anticipateANF e n
+  | exprIsTrivial e                               = n -- trivial expr won't have a binding
+  | Just Unlifted <- typeLevity_maybe (exprType e)
+  , not (isAbs n && exprOkForSpeculation e)       = case_bind n
+  | otherwise                                     = let_bind  n
+  where
+    case_bind _ = C_11       -- evaluated exactly once
+    let_bind    = oneifyCard -- evaluated at most once
 
 -- Do not process absent demands
 -- Otherwise act like in a normal demand analysis
 -- See ↦* relation in the Cardinality Analysis paper
 dmdAnalStar :: AnalEnv
             -> Demand   -- This one takes a *Demand*
-            -> CoreExpr -- Should obey the let/app invariant
+            -> CoreExpr
             -> (PlusDmdArg, CoreExpr)
 dmdAnalStar env (n :* sd) e
   -- NB: (:*) expands AbsDmd and BotDmd as needed
-  -- See Note [Analysing with absent demand]
   | WithDmdType dmd_ty e' <- dmdAnal env sd e
-  = assertPpr (mightBeLiftedType (exprType e) || exprOkForSpeculation e) (ppr e)
-    -- The argument 'e' should satisfy the let/app invariant
-    (toPlusDmdArg $ multDmdType n dmd_ty, e')
+  , n' <- anticipateANF e n
+      -- See Note [Anticipating ANF in demand analysis]
+      -- and Note [Analysing with absent demand]
+  = (toPlusDmdArg $ multDmdType n' dmd_ty, e')
 
 -- Main Demand Analsysis machinery
 dmdAnal, dmdAnal' :: AnalEnv
@@ -398,7 +404,7 @@ dmdAnal' env dmd (App fun arg)
         call_dmd          = mkCalledOnceDmd dmd
         WithDmdType fun_ty fun' = dmdAnal env call_dmd fun
         (arg_dmd, res_ty) = splitDmdTy fun_ty
-        (arg_ty, arg')    = dmdAnalStar env (dmdTransformThunkDmd arg arg_dmd) arg
+        (arg_ty, arg')    = dmdAnalStar env arg_dmd arg
     in
 --    pprTrace "dmdAnal:app" (vcat
 --         [ text "dmd =" <+> ppr dmd
@@ -589,6 +595,45 @@ addCaseBndrDmd case_sd fld_dmds
     scrut_sd = case_sd `plusSubDmd` mkProd Unboxed fld_dmds
 
 {-
+Note [Anticipating ANF in demand analysis]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When analysing non-complex (e.g., trivial) thunks and complex function
+arguments, we have to pretend that the expression is really in administrative
+normal form (ANF), the conversion to which is done by CorePrep.
+
+Consider
+```
+f x = let y = x |> co in y `seq` y `seq` ()
+```
+E.g., 'y' is a let-binding with a trivial RHS. That may occur if 'y' can't be
+inlined, for example. Now, is 'x' used once? It may appear as if that is the
+case, since its only occurrence is in 'y's memoised RHS. But actually, CorePrep
+will *not* allocate a thunk for 'y', because it is trivial and could just
+re-use the memoisation mechanism of 'x'! By saying that 'x' is used once it
+becomes a single-entry thunk and a call to 'f' will evaluate it twice.
+The same applies to trivial arguments, e.g., `f z` really evaluates `z` twice.
+
+So, somewhat counter-intuitively, trivial arguments and let RHSs will *not* be
+memoised. On the other hand, evaluation of non-trivial arguments and let RHSs
+*will* be memoised. In fact, consider the effect of conversion to ANF on complex
+function arguments (as done by 'GHC.Core.Prep.mkFloat'):
+```
+f2 (g2 x) ===> let y = g2 x in f2 y                   (if `y` is lifted)
+f3 (g3 x) ===> case g3 x of y { __DEFAULT -> f3 y }   (if `y` is not lifted)
+```
+So if a lifted argument like `g2 x` is complex enough, it will be memoised.
+Regardless how many times 'f2' evaluates its parameter, the argument will be
+evaluated at most once to WHNF.
+Similarly, when an unlifted argument like `g3 x` is complex enough, we will
+evaluate it *exactly* once to WHNF, no matter how 'f3' evaluates its parameter.
+
+Note that any evaluation beyond WHNF is not affected by memoisation. So this
+Note affects the outer 'Card' of a 'Demand', but not its nested 'SubDemand'.
+'anticipateANF' predicts the effect of case-binding and let-binding complex
+arguments, as well as the lack of memoisation for trivial let RHSs.
+In particular, this takes care of the gripes in
+Note [Analysing with absent demand] relating to unlifted types.
+
 Note [Analysing with absent demand]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Suppose we analyse an expression with demand A.  The "A" means
@@ -599,7 +644,8 @@ There are several wrinkles:
   Reason: Note [Always analyse in virgin pass]
 
   But we can post-process the results to ignore all the usage
-  demands coming back. This is done by multDmdType.
+  demands coming back. This is done by 'multDmdType' with the appropriate
+  (absent) evaluation cardinality A or B.
 
 * Nevertheless, which sub-demand should we pick for analysis?
   Since the demand was absent, any would do. Worker/wrapper will replace
@@ -610,33 +656,36 @@ There are several wrinkles:
   be bottoming. Better pick 'seqSubDmd', so that we annotate many of those
   nested bindings with A themselves.
 
-* In a previous incarnation of GHC we needed to be extra careful in the
-  case of an *unlifted type*, because unlifted values are evaluated
-  even if they are not used.  Example (see #9254):
+* Since we allow unlifted arguments that are not ok-for-speculation,
+  we need to be extra careful in the following situation, because unlifted
+  values are evaluated even if they are not used. Example from #9254:
      f :: (() -> (# Int#, () #)) -> ()
           -- Strictness signature is
-          --    <CS(S(A,SU))>
+          --    <1C1(P(A,1L))>
           -- I.e. calls k, but discards first component of result
      f k = case k () of (# _, r #) -> r
 
      g :: Int -> ()
      g y = f (\n -> (# case y of I# y2 -> y2, n #))
 
-  Here f's strictness signature says (correctly) that it calls its
-  argument function and ignores the first component of its result.
-  This is correct in the sense that it'd be fine to (say) modify the
-  function so that always returned 0# in the first component.
-
-  But in function g, we *will* evaluate the 'case y of ...', because
-  it has type Int#.  So 'y' will be evaluated.  So we must record this
-  usage of 'y', else 'g' will say 'y' is absent, and will w/w so that
-  'y' is bound to an aBSENT_ERROR thunk.
-
-  However, the argument of toSubDmd always satisfies the let/app
-  invariant; so if it is unlifted it is also okForSpeculation, and so
-  can be evaluated in a short finite time -- and that rules out nasty
-  cases like the one above.  (I'm not quite sure why this was a
-  problem in an earlier version of GHC, but it isn't now.)
+  Here, f's strictness signature says (correctly) that it calls its argument
+  function and ignores the first component of its result.
+
+  But in function g, we *will* evaluate the 'case y of ...', because it has type
+  Int#. So in the program as written, 'y' will be evaluated. Hence we must
+  record this usage of 'y', else 'g' will say 'y' is absent, and will w/w so
+  that 'y' is bound to an absent filler (see Note [Absent fillers]), leading
+  to a crash when 'y' is evaluated.
+
+  Now, worker/wrapper could be smarter and replace `case y of I# y2 -> y2`
+  with a suitable absent filler such as `RUBBISH[IntRep] @Int#`.
+  But as long as worker/wrapper isn't equipped to do so, we must be cautious,
+  and follow Note [Anticipating ANF in demand analysis]. That is, in
+  'dmdAnalStar', we will set the evaluation cardinality to C_11, anticipating
+  the case binding of the complex argument `case y of I# y2 -> y2`. This
+  cardinlities' only effect is in the call to 'multDmdType', where it makes sure
+  that the demand on the arg's free variable 'y' is not absent and strict, so
+  that it is ultimately passed unboxed to 'g'.
 
 Note [Always analyse in virgin pass]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/compiler/GHC/Core/Opt/FloatIn.hs b/compiler/GHC/Core/Opt/FloatIn.hs
index ed62d3dfb2..88411a7add 100644
--- a/compiler/GHC/Core/Opt/FloatIn.hs
+++ b/compiler/GHC/Core/Opt/FloatIn.hs
@@ -194,14 +194,11 @@ fiExpr platform to_drop ann_expr@(_,AnnApp {})
     add_arg :: (Type,FreeVarSet) -> CoreExprWithFVs -> (Type,FreeVarSet)
     add_arg (fun_ty, extra_fvs) (_, AnnType ty)
       = (piResultTy fun_ty ty, extra_fvs)
-
     add_arg (fun_ty, extra_fvs) (arg_fvs, arg)
-      | noFloatIntoArg arg arg_ty
-      = (res_ty, extra_fvs `unionDVarSet` arg_fvs)
+      | noFloatIntoArg arg
+      = (funResultTy fun_ty, extra_fvs `unionDVarSet` arg_fvs)
       | otherwise
-      = (res_ty, extra_fvs)
-      where
-       (_, arg_ty, res_ty) = splitFunTy fun_ty
+      = (funResultTy fun_ty, extra_fvs)
 
 {- Note [Dead bindings]
 ~~~~~~~~~~~~~~~~~~~~~~~
@@ -212,15 +209,6 @@ only way that can happen is if the binding wrapped the literal
 But, while this may be unusual it is not actually wrong, and it did
 once happen (#15696).
 
-Note [Do not destroy the let/app invariant]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Watch out for
-   f (x +# y)
-We don't want to float bindings into here
-   f (case ... of { x -> x +# y })
-because that might destroy the let/app invariant, which requires
-unlifted function arguments to be ok-for-speculation.
-
 Note [Join points]
 ~~~~~~~~~~~~~~~~~~
 Generally, we don't need to worry about join points - there are places we're
@@ -588,14 +576,14 @@ noFloatIntoRhs is_rec bndr rhs
   | isJoinId bndr
   = isRec is_rec -- Joins are one-shot iff non-recursive
 
-  | otherwise
-  = noFloatIntoArg rhs (idType bndr)
+  | Just Unlifted <- typeLevity_maybe (idType bndr)
+  = True  -- Preserve let-can-float invariant, see Note [noFloatInto considerations]
 
-noFloatIntoArg :: CoreExprWithFVs' -> Type -> Bool
-noFloatIntoArg expr expr_ty
-  | Just Unlifted <- typeLevity_maybe expr_ty
-  = True  -- See Note [Do not destroy the let/app invariant]
+  | otherwise
+  = noFloatIntoArg rhs
 
+noFloatIntoArg :: CoreExprWithFVs' -> Bool
+noFloatIntoArg expr
    | AnnLam bndr e <- expr
    , (bndrs, _) <- collectAnnBndrs e
    =  noFloatIntoLam (bndr:bndrs)  -- Wrinkle 1 (a)
@@ -610,11 +598,11 @@ noFloatIntoArg expr expr_ty
 {- Note [noFloatInto considerations]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 When do we want to float bindings into
-   - noFloatIntoRHs: the RHS of a let-binding
+   - noFloatIntoRhs: the RHS of a let-binding
    - noFloatIntoArg: the argument of a function application
 
-Definitely don't float in if it has unlifted type; that
-would destroy the let/app invariant.
+Definitely don't float into RHS if it has unlifted type;
+that would destroy the let-can-float invariant.
 
 * Wrinkle 1: do not float in if
      (a) any non-one-shot value lambdas
diff --git a/compiler/GHC/Core/Opt/SetLevels.hs b/compiler/GHC/Core/Opt/SetLevels.hs
index eab4d0ef4e..21ddfbda22 100644
--- a/compiler/GHC/Core/Opt/SetLevels.hs
+++ b/compiler/GHC/Core/Opt/SetLevels.hs
@@ -912,15 +912,15 @@ Note [Test cheapness with exprOkForSpeculation]
 We don't want to float very cheap expressions by boxing and unboxing.
 But we use exprOkForSpeculation for the test, not exprIsCheap.
 Why?  Because it's important /not/ to transform
-     f (a /# 3)
+     let x = a /# 3
 to
-     f (case bx of I# a -> a /# 3)
-and float bx = I# (a /# 3), because the application of f no
-longer obeys the let/app invariant.  But (a /# 3) is ok-for-spec
+     let x = case bx of I# a -> a /# 3
+because the let binding no
+longer obeys the let-can-float invariant.  But (a /# 3) is ok-for-spec
 due to a special hack that says division operators can't fail
 when the denominator is definitely non-zero.  And yet that
 same expression says False to exprIsCheap.  Simplest way to
-guarantee the let/app invariant is to use the same function!
+guarantee the let-can-float invariant is to use the same function!
 
 If an expression is okay for speculation, we could also float it out
 *without* boxing and unboxing, since evaluating it early is okay.
diff --git a/compiler/GHC/Core/Opt/Simplify.hs b/compiler/GHC/Core/Opt/Simplify.hs
index e1b54cf5da..cc7529179b 100644
--- a/compiler/GHC/Core/Opt/Simplify.hs
+++ b/compiler/GHC/Core/Opt/Simplify.hs
@@ -6,6 +6,7 @@
 
 
 {-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE MultiWayIf #-}
 
 {-# OPTIONS_GHC -Wno-incomplete-record-updates -Wno-incomplete-uni-patterns #-}
 module GHC.Core.Opt.Simplify ( simplTopBinds, simplExpr, simplImpRules ) where
@@ -71,6 +72,7 @@ import GHC.Utils.Constants (debugIsOn)
 import GHC.Utils.Trace
 import GHC.Utils.Monad  ( mapAccumLM, liftIO )
 import GHC.Utils.Logger
+import GHC.Utils.Misc
 
 import Control.Monad
 
@@ -324,7 +326,7 @@ simplLazyBind :: SimplEnv
               -> SimplM (SimplFloats, SimplEnv)
 -- Precondition: the OutId is already in the InScopeSet of the incoming 'env'
 -- Precondition: not a JoinId
--- Precondition: rhs obeys the let/app invariant
+-- Precondition: rhs obeys the let-can-float invariant
 -- NOT used for JoinIds
 simplLazyBind env top_lvl is_rec bndr bndr1 rhs rhs_se
   = assert (isId bndr )
@@ -402,7 +404,7 @@ simplNonRecX :: SimplEnv
 -- A specialised variant of simplNonRec used when the RHS is already
 -- simplified, notably in knownCon.  It uses case-binding where necessary.
 --
--- Precondition: rhs satisfies the let/app invariant
+-- Precondition: rhs satisfies the let-can-float invariant
 
 simplNonRecX env bndr new_rhs
   | assertPpr (not (isJoinId bndr)) (ppr bndr) $
@@ -739,7 +741,8 @@ Here we want to make e1,e2 trivial and get
 That's what the 'go' loop in prepareRhs does
 -}
 
-prepareRhs :: SimplEnv -> TopLevelFlag
+prepareRhs :: HasDebugCallStack
+           => SimplEnv -> TopLevelFlag
            -> FastString    -- Base for any new variables
            -> OutExpr
            -> SimplM (LetFloats, OutExpr)
@@ -762,10 +765,11 @@ prepareRhs env top_lvl occ rhs0
              ; return (is_exp, floats, App rhs' (Type ty)) }
     go n_val_args (App fun arg)
         = do { (is_exp, floats1, fun') <- go (n_val_args+1) fun
-             ; case is_exp of
-                False -> return (False, emptyLetFloats, App fun arg)
-                True  -> do { (floats2, arg') <- makeTrivial env top_lvl topDmd occ arg
-                            ; return (True, floats1 `addLetFlts` floats2, App fun' arg') } }
+             ; if is_exp
+               then do { (floats2, arg') <- makeTrivial env top_lvl topDmd occ arg
+                       ; return (True, floats1 `addLetFlts` floats2, App fun' arg') }
+               else return (False, emptyLetFloats, App fun arg)
+             }
     go n_val_args (Var fun)
         = return (is_exp, emptyLetFloats, Var fun)
         where
@@ -793,16 +797,17 @@ prepareRhs env top_lvl occ rhs0
     go _ other
         = return (False, emptyLetFloats, other)
 
-makeTrivialArg :: SimplEnv -> ArgSpec -> SimplM (LetFloats, ArgSpec)
+makeTrivialArg :: HasDebugCallStack => SimplEnv -> ArgSpec -> SimplM (LetFloats, ArgSpec)
 makeTrivialArg env arg@(ValArg { as_arg = e, as_dmd = dmd })
   = do { (floats, e') <- makeTrivial env NotTopLevel dmd (fsLit "arg") e
        ; return (floats, arg { as_arg = e' }) }
 makeTrivialArg _ arg
   = return (emptyLetFloats, arg)  -- CastBy, TyArg
 
-makeTrivial :: SimplEnv -> TopLevelFlag -> Demand
+makeTrivial :: HasDebugCallStack
+            => SimplEnv -> TopLevelFlag -> Demand
             -> FastString  -- ^ A "friendly name" to build the new binder from
-            -> OutExpr     -- ^ This expression satisfies the let/app invariant
+            -> OutExpr
             -> SimplM (LetFloats, OutExpr)
 -- Binds the expression to a variable, if it's not trivial, returning the variable
 -- For the Demand argument, see Note [Keeping demand info in StrictArg Plan A]
@@ -824,10 +829,11 @@ makeTrivial env top_lvl dmd occ_fs expr
     id_info = vanillaIdInfo `setDemandInfo` dmd
     expr_ty = exprType expr
 
-makeTrivialBinding :: SimplEnv -> TopLevelFlag
+makeTrivialBinding :: HasDebugCallStack
+                   => SimplEnv -> TopLevelFlag
                    -> FastString  -- ^ a "friendly name" to build the new binder from
                    -> IdInfo
-                   -> OutExpr     -- ^ This expression satisfies the let/app invariant
+                   -> OutExpr
                    -> OutType     -- Type of the expression
                    -> SimplM (LetFloats, OutId)
 makeTrivialBinding env top_lvl occ_fs info expr expr_ty
@@ -923,7 +929,7 @@ completeBind :: SimplEnv
 --      * or by adding to the floats in the envt
 --
 -- Binder /can/ be a JoinId
--- Precondition: rhs obeys the let/app invariant
+-- Precondition: rhs obeys the let-can-float invariant
 completeBind env bind_cxt old_bndr new_bndr new_rhs
  | isCoVar old_bndr
  = case new_rhs of
@@ -1477,13 +1483,9 @@ rebuild env expr cont
 
       StrictArg { sc_fun = fun, sc_cont = cont, sc_fun_ty = fun_ty }
         -> rebuildCall env (addValArgTo fun expr fun_ty ) cont
-      StrictBind { sc_bndr = b, sc_body = body
-                 , sc_env = se, sc_cont = cont }
-        -> do { (floats1, env') <- simplNonRecX (se `setInScopeFromE` env) b expr
-                                  -- expr satisfies let/app since it started life
-                                  -- in a call to simplNonRecE
-              ; (floats2, expr') <- simplLam env' body cont
-              ; return (floats1 `addFloats` floats2, expr') }
+
+      StrictBind { sc_bndr = b, sc_body = body, sc_env = se, sc_cont = cont }
+        -> completeBindX (se `setInScopeFromE` env) b expr body cont
 
       ApplyToTy  { sc_arg_ty = ty, sc_cont = cont}
         -> rebuild env (App expr (Type ty)) cont
@@ -1493,6 +1495,27 @@ rebuild env expr cont
         -> do { (_, _, arg') <- simplArg env dup_flag se arg
               ; rebuild env (App expr arg') cont }
 
+completeBindX :: SimplEnv
+              -> InId -> OutExpr   -- Bind this Id to this (simplified) expression
+                                   -- (the let-can-float invariant may not be satisfied)
+              -> InExpr  -- In this lambda
+              -> SimplCont         -- Consumed by this continuation
+              -> SimplM (SimplFloats, OutExpr)
+completeBindX env bndr rhs body cont
+  | needsCaseBinding (idType bndr) rhs -- Enforcing the let-can-float-invariant
+  = do { (env1, bndr1) <- simplNonRecBndr env bndr
+       ; (floats, expr') <- simplLam env1 body cont
+       -- Do not float floats past the Case binder below
+       ; let expr'' = wrapFloats floats expr'
+       ; let case_expr = Case rhs bndr1 (contResultType cont) [Alt DEFAULT [] expr'']
+       ; return (emptyFloats env, case_expr) }
+
+  | otherwise
+  = do  { (floats1, env') <- simplNonRecX env bndr rhs
+        ; (floats2, expr') <- simplLam env' body cont
+        ; return (floats1 `addFloats` floats2, expr') }
+
+
 {-
 ************************************************************************
 *                                                                      *
@@ -1645,12 +1668,10 @@ simpl_lam env bndr body (ApplyToVal { sc_arg = arg, sc_env = arg_se
                                     , sc_cont = cont, sc_dup = dup })
   | isSimplified dup  -- Don't re-simplify if we've simplified it once
                       -- See Note [Avoiding exponential behaviour]
-  = do  { tick (BetaReduction bndr)
-        ; (floats1, env') <- simplNonRecX env bndr arg
-        ; (floats2, expr') <- simplLam env' body cont
-        ; return (floats1 `addFloats` floats2, expr') }
+  =  do { tick (BetaReduction bndr)
+        ; completeBindX env bndr arg body cont }
 
-  | otherwise
+  | otherwise         -- See Note [Avoiding exponential behaviour]
   = do  { tick (BetaReduction bndr)
         ; simplNonRecE env bndr (arg, arg_se) body cont }
 
@@ -1699,34 +1720,36 @@ simplNonRecE :: SimplEnv
 --     cont< let b = rhs_se(rhs) in body >
 --
 -- It deals with strict bindings, via the StrictBind continuation,
--- which may abort the whole process
+-- which may abort the whole process.
 --
--- Precondition: rhs satisfies the let/app invariant
---               Note [Core let/app invariant] in GHC.Core
+-- The RHS may not satisfy the let-can-float invariant yet
 
 simplNonRecE env bndr (rhs, rhs_se) body cont
-  | assert (isId bndr && not (isJoinId bndr) ) True
-  , Just env' <- preInlineUnconditionally env NotTopLevel bndr rhs rhs_se
-  = do { tick (PreInlineUnconditionally bndr)
-       ; -- pprTrace "preInlineUncond" (ppr bndr <+> ppr rhs) $
-         simplLam env' body cont }
-
-  | otherwise
-  = do { (env1, bndr1) <- simplNonRecBndr env bndr
-
-       -- Deal with strict bindings
-       -- See Note [Dark corner with representation polymorphism]
-       ; if isStrictId bndr1 && sm_case_case (getMode env)
-         then simplExprF (rhs_se `setInScopeFromE` env) rhs
-                   (StrictBind { sc_bndr = bndr, sc_body = body
-                               , sc_env = env, sc_cont = cont, sc_dup = NoDup })
-
-       -- Deal with lazy bindings
-         else do
-       { (env2, bndr2)    <- addBndrRules env1 bndr bndr1 (BC_Let NotTopLevel NonRecursive)
-       ; (floats1, env3)  <- simplLazyBind env2 NotTopLevel NonRecursive bndr bndr2 rhs rhs_se
-       ; (floats2, expr') <- simplLam env3 body cont
-       ; return (floats1 `addFloats` floats2, expr') } }
+  = assert (isId bndr && not (isJoinId bndr) ) $
+    do { (env1, bndr1) <- simplNonRecBndr env bndr
+       ; let needs_case_binding = needsCaseBinding (idType bndr1) rhs
+         -- See Note [Dark corner with representation polymorphism]
+       ; if | not needs_case_binding
+            , Just env' <- preInlineUnconditionally env NotTopLevel bndr rhs rhs_se ->
+            do { tick (PreInlineUnconditionally bndr)
+               ; -- pprTrace "preInlineUncond" (ppr bndr <+> ppr rhs) $
+                 simplLam env' body cont }
+
+
+             -- Deal with strict bindings
+             -- See Note [Dark corner with representation polymorphism]
+            | isStrictId bndr1 && sm_case_case (getMode env)
+            || needs_case_binding ->
+            simplExprF (rhs_se `setInScopeFromE` env) rhs
+                       (StrictBind { sc_bndr = bndr, sc_body = body
+                                   , sc_env = env, sc_cont = cont, sc_dup = NoDup })
+
+            -- Deal with lazy bindings
+            | otherwise ->
+            do { (env2, bndr2)    <- addBndrRules env1 bndr bndr1 (BC_Let NotTopLevel NonRecursive)
+               ; (floats1, env3)  <- simplLazyBind env2 NotTopLevel NonRecursive bndr bndr2 rhs rhs_se
+               ; (floats2, expr') <- simplLam env3 body cont
+               ; return (floats1 `addFloats` floats2, expr') } }
 
 ------------------
 simplRecE :: SimplEnv
@@ -1750,8 +1773,8 @@ simplRecE env pairs body cont
 
 {- Note [Dark corner with representation polymorphism]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-In `simplNonRecE`, the call to `isStrictId` will fail if the binder
-does not have a fixed runtime representation, e.g. if it is of kind (TYPE r).
+In `simplNonRecE`, the call to `needsCaseBinding` or to `isStrictId` will fail
+if the binder does not have a fixed runtime representation, e.g. if it is of kind (TYPE r).
 So we are careful to call `isStrictId` on the OutId, not the InId, in case we have
      ((\(r::RuntimeRep) \(x::TYPE r). blah) Lifted arg)
 That will lead to `simplNonRecE env (x::TYPE r) arg`, and we can't tell
@@ -2567,7 +2590,7 @@ this transformation:
 We treat the unlifted and lifted cases separately:
 
 * Unlifted case: 'e' satisfies exprOkForSpeculation
-  (ok-for-spec is needed to satisfy the let/app invariant).
+  (ok-for-spec is needed to satisfy the let-can-float invariant).
   This turns     case a +# b of r -> ...r...
   into           let r = a +# b in ...r...
   and thence     .....(a +# b)....
@@ -2779,7 +2802,7 @@ rebuildCase env scrut case_bndr alts cont
       assert (null bs) $
       do { (floats1, env') <- simplNonRecX env case_bndr case_bndr_rhs
              -- scrut is a constructor application,
-             -- hence satisfies let/app invariant
+             -- hence satisfies let-can-float invariant
          ; (floats2, expr') <- simplExprF env' rhs cont
          ; case wfloats of
              [] -> return (floats1 `addFloats` floats2, expr')
@@ -3217,11 +3240,11 @@ We pin on a (OtherCon []) unfolding to the case-binder of a Case,
 even though it'll be over-ridden in every case alternative with a more
 informative unfolding.  Why?  Because suppose a later, less clever, pass
 simply replaces all occurrences of the case binder with the binder itself;
-then Lint may complain about the let/app invariant.  Example
+then Lint may complain about the let-can-float invariant.  Example
     case e of b { DEFAULT -> let v = reallyUnsafePtrEquality# b y in ....
                 ; K       -> blah }
 
-The let/app invariant requires that y is evaluated in the call to
+The let-can-float invariant requires that y is evaluated in the call to
 reallyUnsafePtrEquality#, which it is.  But we still want that to be true if we
 propagate binders to occurrences.
 
@@ -3326,7 +3349,7 @@ knownCon env scrut dc_floats dc dc_ty_args dc_args bndr bs rhs cont
              -- it via postInlineUnconditionally.
              -- Nevertheless we must keep it if the case-binder is alive,
              -- because it may be used in the con_app.  See Note [knownCon occ info]
-           ; (floats1, env2) <- simplNonRecX env' b' arg  -- arg satisfies let/app invariant
+           ; (floats1, env2) <- simplNonRecX env' b' arg  -- arg satisfies let-can-float invariant
            ; (floats2, env3)  <- bind_args env2 bs' args
            ; return (floats1 `addFloats` floats2, env3) }
 
diff --git a/compiler/GHC/Core/Opt/Simplify/Env.hs b/compiler/GHC/Core/Opt/Simplify/Env.hs
index bcfef36be2..3873bfddb7 100644
--- a/compiler/GHC/Core/Opt/Simplify/Env.hs
+++ b/compiler/GHC/Core/Opt/Simplify/Env.hs
@@ -56,7 +56,7 @@ import GHC.Types.Var.Env
 import GHC.Types.Var.Set
 import GHC.Data.OrdList
 import GHC.Types.Id as Id
-import GHC.Core.Make            ( mkWildValBinder )
+import GHC.Core.Make            ( mkWildValBinder, mkCoreLet )
 import GHC.Driver.Session       ( DynFlags )
 import GHC.Builtin.Types
 import GHC.Core.TyCo.Rep        ( TyCoBinder(..) )
@@ -436,7 +436,8 @@ Note [LetFloats]
 ~~~~~~~~~~~~~~~~
 The LetFloats is a bunch of bindings, classified by a FloatFlag.
 
-* All of them satisfy the let/app invariant
+The `FloatFlag` contains summary information about the bindings, see the data
+type declaration of `FloatFlag`
 
 Examples
 
@@ -447,10 +448,8 @@ Examples
   NonRec x# (y +# 3)    FltOkSpec   -- Unboxed, but ok-for-spec'n
 
   NonRec x* (f y)       FltCareful  -- Strict binding; might fail or diverge
-
-Can't happen:
-  NonRec x# (a /# b)    -- Might fail; does not satisfy let/app
-  NonRec x# (f y)       -- Might diverge; does not satisfy let/app
+  NonRec x# (a /# b)    FltCareful  -- Might fail; does not satisfy let-can-float invariant
+  NonRec x# (f y)       FltCareful  -- Might diverge; does not satisfy let-can-float invariant
 -}
 
 data LetFloats = LetFloats (OrdList OutBind) FloatFlag
@@ -462,19 +461,22 @@ type JoinFloats = OrdList JoinFloat
 data FloatFlag
   = FltLifted   -- All bindings are lifted and lazy *or*
                 --     consist of a single primitive string literal
-                --  Hence ok to float to top level, or recursive
+                -- Hence ok to float to top level, or recursive
+                -- NB: consequence: all bindings satisfy let-can-float invariant
 
   | FltOkSpec   -- All bindings are FltLifted *or*
                 --      strict (perhaps because unlifted,
                 --      perhaps because of a strict binder),
                 --        *and* ok-for-speculation
-                --  Hence ok to float out of the RHS
-                --  of a lazy non-recursive let binding
-                --  (but not to top level, or into a rec group)
+                -- Hence ok to float out of the RHS
+                -- of a lazy non-recursive let binding
+                -- (but not to top level, or into a rec group)
+                -- NB: consequence: all bindings satisfy let-can-float invariant
 
   | FltCareful  -- At least one binding is strict (or unlifted)
                 --      and not guaranteed cheap
-                --      Do not float these bindings out of a lazy let
+                -- Do not float these bindings out of a lazy let!
+                -- NB: some bindings may not satisfy let-can-float
 
 instance Outputable LetFloats where
   ppr (LetFloats binds ff) = ppr ff $$ ppr (fromOL binds)
@@ -520,7 +522,7 @@ emptyLetFloats = LetFloats nilOL FltLifted
 emptyJoinFloats :: JoinFloats
 emptyJoinFloats = nilOL
 
-unitLetFloat :: OutBind -> LetFloats
+unitLetFloat :: HasDebugCallStack => OutBind -> LetFloats
 -- This key function constructs a singleton float with the right form
 unitLetFloat bind = assert (all (not . isJoinId) (bindersOf bind)) $
                     LetFloats (unitOL bind) (flag bind)
@@ -532,11 +534,7 @@ unitLetFloat bind = assert (all (not . isJoinId) (bindersOf bind)) $
           -- String literals can be floated freely.
           -- See Note [Core top-level string literals] in GHC.Core.
       | exprOkForSpeculation rhs = FltOkSpec  -- Unlifted, and lifted but ok-for-spec (eg HNF)
-      | otherwise                = assertPpr (not (isUnliftedType (idType bndr))) (ppr bndr)
-                                   -- NB: binders always have a fixed RuntimeRep, so calling
-                                   -- isUnliftedType is OK here
-                                   FltCareful
-      -- Unlifted binders can only be let-bound if exprOkForSpeculation holds
+      | otherwise                = FltCareful
 
 unitJoinFloat :: OutBind -> JoinFloats
 unitJoinFloat bind = assert (all isJoinId (bindersOf bind)) $
@@ -641,13 +639,15 @@ mkRecFloats floats@(SimplFloats { sfLetFloats  = LetFloats bs _ff
               | otherwise   = unitJoinFloat (Rec (flattenBinds (fromOL jbs)))
 
 wrapFloats :: SimplFloats -> OutExpr -> OutExpr
--- Wrap the floats around the expression; they should all
--- satisfy the let/app invariant, so mkLets should do the job just fine
-wrapFloats (SimplFloats { sfLetFloats  = LetFloats bs _
+-- Wrap the floats around the expression
+wrapFloats (SimplFloats { sfLetFloats  = LetFloats bs flag
                         , sfJoinFloats = jbs }) body
-  = foldrOL Let (wrapJoinFloats jbs body) bs
+  = foldrOL mk_let (wrapJoinFloats jbs body) bs
      -- Note: Always safe to put the joins on the inside
      -- since the values can't refer to them
+  where
+    mk_let | FltCareful <- flag = mkCoreLet -- need to enforce let-can-float-invariant
+           | otherwise          = Let       -- let-can-float invariant hold
 
 wrapJoinFloatsX :: SimplFloats -> OutExpr -> (SimplFloats, OutExpr)
 -- Wrap the sfJoinFloats of the env around the expression,
diff --git a/compiler/GHC/Core/Opt/Simplify/Utils.hs b/compiler/GHC/Core/Opt/Simplify/Utils.hs
index 71468fc808..b8d5d9ab43 100644
--- a/compiler/GHC/Core/Opt/Simplify/Utils.hs
+++ b/compiler/GHC/Core/Opt/Simplify/Utils.hs
@@ -1290,8 +1290,8 @@ preInlineUnconditionally
     :: SimplEnv -> TopLevelFlag -> InId
     -> InExpr -> StaticEnv  -- These two go together
     -> Maybe SimplEnv       -- Returned env has extended substitution
--- Precondition: rhs satisfies the let/app invariant
--- See Note [Core let/app invariant] in GHC.Core
+-- Precondition: rhs satisfies the let-can-float invariant
+-- See Note [Core let-can-float invariant] in GHC.Core
 -- Reason: we don't want to inline single uses, or discard dead bindings,
 --         for unlifted, side-effect-ful bindings
 preInlineUnconditionally env top_lvl bndr rhs rhs_env
@@ -1416,8 +1416,8 @@ postInlineUnconditionally
     -> OccInfo          -- From the InId
     -> OutExpr
     -> Bool
--- Precondition: rhs satisfies the let/app invariant
--- See Note [Core let/app invariant] in GHC.Core
+-- Precondition: rhs satisfies the let-can-float invariant
+-- See Note [Core let-can-float invariant] in GHC.Core
 -- Reason: we don't want to inline single uses, or discard dead bindings,
 --         for unlifted, side-effect-ful bindings
 postInlineUnconditionally env bind_cxt bndr occ_info rhs
diff --git a/compiler/GHC/Core/SimpleOpt.hs b/compiler/GHC/Core/SimpleOpt.hs
index 92f1c7987e..fa6fcda351 100644
--- a/compiler/GHC/Core/SimpleOpt.hs
+++ b/compiler/GHC/Core/SimpleOpt.hs
@@ -27,7 +27,7 @@ import GHC.Core.Utils
 import GHC.Core.FVs
 import GHC.Core.Unfold
 import GHC.Core.Unfold.Make
-import GHC.Core.Make ( FloatBind(..) )
+import GHC.Core.Make ( FloatBind(..), mkWildValBinder )
 import GHC.Core.Opt.OccurAnal( occurAnalyseExpr, occurAnalysePgm, zapLambdaBndrs )
 import GHC.Types.Literal
 import GHC.Types.Id
@@ -343,8 +343,19 @@ simple_app env e@(Lam {}) as@(_:_)
     n_args = length as
 
     do_beta env (Lam b body) (a:as)
-      | (env', mb_pr) <- simple_bind_pair env b Nothing a NotTopLevel
-      = wrapLet mb_pr $ do_beta env' body as
+      | -- simpl binder before looking at its type
+        -- See Note [Dark corner with representation polymorphism]
+        needsCaseBinding (idType b') (snd a)
+        -- This arg must not be inlined (side-effects) and cannot be let-bound,
+        -- due to the let-can-float invariant. So simply case-bind it here.
+      , let a' = simple_opt_clo env a
+      = mkDefaultCase a' b' $ do_beta env' body as
+
+      | (env'', mb_pr) <- simple_bind_pair env' b (Just b') a NotTopLevel
+      = wrapLet mb_pr $ do_beta env'' body as
+
+      where (env', b') = subst_opt_bndr env b
+
     do_beta env body as
       = simple_app env body as
 
@@ -1122,6 +1133,30 @@ exprIsConApp_maybe (in_scope, id_unf) expr
            MRefl    -> go subst floats expr (CC args' co2)
 
     go subst floats (App fun arg) (CC args co)
+       | let arg_type = exprType arg
+       , not (isTypeArg arg) && needsCaseBinding arg_type arg
+       -- An unlifted argument that’s not ok for speculation must not simply be
+       -- put into the args, as these are going to be substituted into the case
+       -- alternatives, and possibly lost on the way.
+       --
+       -- Instead, we need need to
+       -- make sure they are evaluated right here (using a case float), and
+       -- the case binder can then be substituted into the case alternaties.
+       --
+       -- Example:
+       -- Simplifying  case Mk# exp of Mk# a → rhs
+       -- will use     exprIsConApp_maybe (Mk# exp)
+       --
+       -- Bad:  returning (Mk#, [exp]) with no floats
+       --       simplifier produces rhs[exp/a], changing semantics if exp is not ok-for-spec
+       -- Good: returning (Mk#, [x]) with a float of  case exp of x { DEFAULT -> [] }
+       --       simplifier produces case exp of a { DEFAULT -> exp[x/a] }
+       = let arg' = subst_expr subst arg
+             bndr = uniqAway (subst_in_scope subst) (mkWildValBinder Many arg_type)
+             float = FloatCase arg' bndr DEFAULT []
+             subst' = subst_extend_in_scope subst bndr
+         in go subst' (float:floats) fun (CC (Var bndr : args) co)
+       | otherwise
        = go subst floats fun (CC (subst_expr subst arg : args) co)
 
     go subst floats (Lam bndr body) (CC (arg:args) co)
@@ -1220,6 +1255,13 @@ exprIsConApp_maybe (in_scope, id_unf) expr
     ----------------------------
     -- Operations on the (Either InScopeSet GHC.Core.Subst)
     -- The Left case is wildly dominant
+
+    subst_in_scope (Left in_scope) = in_scope
+    subst_in_scope (Right s) = substInScope s
+
+    subst_extend_in_scope (Left in_scope) v = Left (in_scope `extendInScopeSet` v)
+    subst_extend_in_scope (Right s) v = Right (s `extendInScope` v)
+
     subst_co (Left {}) co = co
     subst_co (Right s) co = GHC.Core.Subst.substCo s co
 
diff --git a/compiler/GHC/Core/Utils.hs b/compiler/GHC/Core/Utils.hs
index 90f8f3f032..ed1dd6f246 100644
--- a/compiler/GHC/Core/Utils.hs
+++ b/compiler/GHC/Core/Utils.hs
@@ -496,7 +496,7 @@ stripTicksT p expr = fromOL $ go expr
 ************************************************************************
 -}
 
-bindNonRec :: Id -> CoreExpr -> CoreExpr -> CoreExpr
+bindNonRec :: HasDebugCallStack => Id -> CoreExpr -> CoreExpr -> CoreExpr
 -- ^ @bindNonRec x r b@ produces either:
 --
 -- > let x = r in b
@@ -522,8 +522,8 @@ bindNonRec bndr rhs body
     case_bind = mkDefaultCase rhs bndr body
     let_bind  = Let (NonRec bndr rhs) body
 
--- | Tests whether we have to use a @case@ rather than @let@ binding for this expression
--- as per the invariants of 'CoreExpr': see "GHC.Core#let_app_invariant"
+-- | Tests whether we have to use a @case@ rather than @let@ binding for this
+-- expression as per the invariants of 'CoreExpr': see "GHC.Core#let_can_float_invariant"
 needsCaseBinding :: Type -> CoreExpr -> Bool
 needsCaseBinding ty rhs =
   mightBeUnliftedType ty && not (exprOkForSpeculation rhs)
@@ -1599,7 +1599,8 @@ expr_ok primop_ok (Case scrut bndr _ alts)
 expr_ok primop_ok other_expr
   | (expr, args) <- collectArgs other_expr
   = case stripTicksTopE (not . tickishCounts) expr of
-        Var f            -> app_ok primop_ok f args
+        Var f ->
+           app_ok primop_ok f args
 
         -- 'LitRubbish' is the only literal that can occur in the head of an
         -- application and will not be matched by the above case (Var /= Lit).
@@ -1645,7 +1646,7 @@ app_ok primop_ok fun args
 
         | otherwise
         -> primop_ok op  -- Check the primop itself
-        && and (zipWith primop_arg_ok arg_tys args)  -- Check the arguments
+        && and (zipWith arg_ok arg_tys args)  -- Check the arguments
 
       _  -- Unlifted types
          -- c.f. the Var case of exprIsHNF
@@ -1657,7 +1658,8 @@ app_ok primop_ok fun args
                   -- and we'd need to actually test n_val_args == 0.
 
          -- Partial applications
-         | idArity fun > n_val_args -> True
+         | idArity fun > n_val_args ->
+           and (zipWith arg_ok arg_tys args)  -- Check the arguments
 
          -- Functions that terminate fast without raising exceptions etc
          -- See Note [Discarding unnecessary unsafeEqualityProofs]
@@ -1671,9 +1673,10 @@ app_ok primop_ok fun args
     n_val_args   = valArgCount args
     (arg_tys, _) = splitPiTys (idType fun)
 
-    primop_arg_ok :: TyBinder -> CoreExpr -> Bool
-    primop_arg_ok (Named _) _ = True   -- A type argument
-    primop_arg_ok (Anon _ ty) arg      -- A term argument
+    -- Used for arguments to primops and to partial applications
+    arg_ok :: TyBinder -> CoreExpr -> Bool
+    arg_ok (Named _) _ = True   -- A type argument
+    arg_ok (Anon _ ty) arg      -- A term argument
        | Just Lifted <- typeLevity_maybe (scaledThing ty)
        = True -- See Note [Primops with lifted arguments]
        | otherwise
@@ -1714,12 +1717,12 @@ But we restrict it sharply:
                                                ; False -> e2 }
                        in ...) ...
 
-  Does the RHS of v satisfy the let/app invariant?  Previously we said
+  Does the RHS of v satisfy the let-can-float invariant?  Previously we said
   yes, on the grounds that y is evaluated.  But the binder-swap done
   by GHC.Core.Opt.SetLevels would transform the inner alternative to
      DEFAULT -> ... (let v::Int# = case x of { ... }
                      in ...) ....
-  which does /not/ satisfy the let/app invariant, because x is
+  which does /not/ satisfy the let-can-float invariant, because x is
   not evaluated. See Note [Binder-swap during float-out]
   in GHC.Core.Opt.SetLevels.  To avoid this awkwardness it seems simpler
   to stick to unlifted scrutinees where the issue does not
@@ -1823,25 +1826,25 @@ Now consider these examples:
  * case x of y { DEFAULT -> ....y.... }
    Should 'y' (alone) be considered ok-for-speculation?
 
- * case x of y { DEFAULT -> ....f (dataToTag# y)... }
+ * case x of y { DEFAULT -> ....let z = dataToTag# y... }
    Should (dataToTag# y) be considered ok-for-spec?
 
 You could argue 'yes', because in the case alternative we know that
 'y' is evaluated.  But the binder-swap transformation, which is
 extremely useful for float-out, changes these expressions to
    case x of y { DEFAULT -> ....x.... }
-   case x of y { DEFAULT -> ....f (dataToTag# x)... }
+   case x of y { DEFAULT -> ....let z = dataToTag# x... }
 
-And now the expression does not obey the let/app invariant!  Yikes!
-Moreover we really might float (f (dataToTag# x)) outside the case,
-and then it really, really doesn't obey the let/app invariant.
+And now the expression does not obey the let-can-float invariant!  Yikes!
+Moreover we really might float (dataToTag# x) outside the case,
+and then it really, really doesn't obey the let-can-float invariant.
 
 The solution is simple: exprOkForSpeculation does not try to take
 advantage of the evaluated-ness of (lifted) variables.  And it returns
 False (always) for DataToTagOp and SeqOp.
 
 Note that exprIsHNF /can/ and does take advantage of evaluated-ness;
-it doesn't have the trickiness of the let/app invariant to worry about.
+it doesn't have the trickiness of the let-can-float invariant to worry about.
 
 Note [Discarding unnecessary unsafeEqualityProofs]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1892,9 +1895,8 @@ but one might imagine a more systematic check in future.
 --
 -- > C (f x :: Int#)
 --
--- Suppose @f x@ diverges; then @C (f x)@ is not a value. However this can't
--- happen: see "GHC.Core#let_app_invariant". This invariant states that arguments of
--- unboxed type must be ok-for-speculation (or trivial).
+-- Suppose @f x@ diverges; then @C (f x)@ is not a value.
+-- We check for this using needsCaseBinding below
 exprIsHNF :: CoreExpr -> Bool           -- True => Value-lambda, constructor, PAP
 exprIsHNF = exprIsHNFlike isDataConWorkId isEvaldUnfolding
 
@@ -1908,7 +1910,7 @@ exprIsConLike = exprIsHNFlike isConLikeId isConLikeUnfolding
 -- constructors / CONLIKE functions (as determined by the function argument)
 -- or PAPs.
 --
-exprIsHNFlike :: (Var -> Bool) -> (Unfolding -> Bool) -> CoreExpr -> Bool
+exprIsHNFlike :: HasDebugCallStack => (Var -> Bool) -> (Unfolding -> Bool) -> CoreExpr -> Bool
 exprIsHNFlike is_con is_con_unf = is_hnf_like
   where
     is_hnf_like (Var v) -- NB: There are no value args at this point
@@ -1949,7 +1951,13 @@ exprIsHNFlike is_con is_con_unf = is_hnf_like
     app_is_value (Tick _ f) nva = app_is_value f nva
     app_is_value (Cast f _) nva = app_is_value f nva
     app_is_value (App f a)  nva
-      | isValArg a              = app_is_value f (nva + 1)
+      | isValArg a              =
+        app_is_value f (nva + 1) &&
+        not (needsCaseBinding (exprType a) a)
+          -- For example  f (x /# y)  where f has arity two, and the first
+          -- argument is unboxed. This is not a value!
+          -- But  f 34#  is a value.
+          -- NB: Check app_is_value first, the arity check is cheaper
       | otherwise               = app_is_value f nva
     app_is_value _          _   = False
 
diff --git a/compiler/GHC/HsToCore/Utils.hs b/compiler/GHC/HsToCore/Utils.hs
index effc1c9688..b962b9bd39 100644
--- a/compiler/GHC/HsToCore/Utils.hs
+++ b/compiler/GHC/HsToCore/Utils.hs
@@ -471,14 +471,12 @@ There are a few subtleties in the desugaring of `seq`:
     Consider,
        f x y = x `seq` (y `seq` (# x,y #))
 
-    The [Core let/app invariant] means that, other things being equal, because
-    the argument to the outer 'seq' has an unlifted type, we'll use call-by-value thus:
+    Because the argument to the outer 'seq' has an unlifted type, we'll use
+    call-by-value, and compile it as if we had
 
        f x y = case (y `seq` (# x,y #)) of v -> x `seq` v
 
-    But that is bad for two reasons:
-      (a) we now evaluate y before x, and
-      (b) we can't bind v to an unboxed pair
+    But that is bad, because we now evaluate y before x!
 
     Seq is very, very special!  So we recognise it right here, and desugar to
             case x of _ -> case y of _ -> (# x,y #)
diff --git a/compiler/GHC/Stg/Lint.hs b/compiler/GHC/Stg/Lint.hs
index 0ec0650693..657aa1603f 100644
--- a/compiler/GHC/Stg/Lint.hs
+++ b/compiler/GHC/Stg/Lint.hs
@@ -6,7 +6,7 @@ A lint pass to check basic STG invariants:
 - Variables should be defined before used.
 
 - Let bindings should not have unboxed types (unboxed bindings should only
-  appear in case), except when they're join points (see Note [Core let/app
+  appear in case), except when they're join points (see Note [Core let-can-float
   invariant] and #14117).
 
 - If linting after unarisation, invariants listed in Note [Post-unarisation
diff --git a/testsuite/tests/simplCore/should_compile/T18231.stderr b/testsuite/tests/simplCore/should_compile/T18231.stderr
index ee5f474423..b126952774 100644
--- a/testsuite/tests/simplCore/should_compile/T18231.stderr
+++ b/testsuite/tests/simplCore/should_compile/T18231.stderr
@@ -1,6 +1,6 @@
 
 ==================== Tidy Core ====================
-Result size of Tidy Core = {terms: 24, types: 20, coercions: 5, joins: 0/0}
+Result size of Tidy Core = {terms: 29, types: 26, coercions: 5, joins: 0/0}
 
 -- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
 T18231.$trModule4 :: GHC.Prim.Addr#
@@ -23,14 +23,18 @@ T18231.$trModule :: GHC.Types.Module
 T18231.$trModule = GHC.Types.Module T18231.$trModule3 T18231.$trModule1
 
 Rec {
--- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
-lvl :: Data.Functor.Identity.Identity ((), Int)
-lvl = lvl
+-- RHS size: {terms: 3, types: 1, coercions: 0, joins: 0/0}
+T18231.$wa' :: (# #) -> Data.Functor.Identity.Identity ((), Int)
+T18231.$wa' = \ _ -> T18231.$wa' GHC.Prim.(##)
 end Rec }
 
+-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
+lvl :: Data.Functor.Identity.Identity ((), Int)
+lvl = T18231.$wa' GHC.Prim.(##)
+
 -- RHS size: {terms: 5, types: 3, coercions: 0, joins: 0/0}
 T18231.m1 :: Int -> Data.Functor.Identity.Identity ((), Int)
-T18231.m1 = \ (eta2 :: Int) -> case eta2 of { GHC.Types.I# x -> lvl }
+T18231.m1 = \ (eta2 :: Int) -> case eta2 of { GHC.Types.I# ww -> lvl }
 
 -- RHS size: {terms: 1, types: 0, coercions: 5, joins: 0/0}
 m :: State Int ()
diff --git a/testsuite/tests/simplCore/should_run/UnliftedArgRule.hs b/testsuite/tests/simplCore/should_run/UnliftedArgRule.hs
new file mode 100644
index 0000000000..8e7c40b75c
--- /dev/null
+++ b/testsuite/tests/simplCore/should_run/UnliftedArgRule.hs
@@ -0,0 +1,24 @@
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE BangPatterns #-}
+import GHC.Exts
+import System.IO.Unsafe ( unsafePerformIO )
+
+z# :: Int -> Int#
+z# _ = unsafePerformIO (putStrLn "Can you read this?")  `seq` 0#
+{-# NOINLINE z# #-}
+
+f :: Int# -> Int
+f _ = unsafePerformIO (putStrLn "Rewrite rule did not match? Bad!")  `seq` 0
+{-# NOINLINE f #-}
+
+g :: Int -> Int
+g _ = 1
+{-# NOINLINE g #-}
+
+h :: Int# -> Int
+h _ = 2
+{-# NOINLINE h #-}
+
+main = print (f (z# 3))
+
+{-# RULES "f to h.g" forall x. f x = g (h x) #-}
diff --git a/testsuite/tests/simplCore/should_run/UnliftedArgRule.stdout b/testsuite/tests/simplCore/should_run/UnliftedArgRule.stdout
new file mode 100644
index 0000000000..760847f1c0
--- /dev/null
+++ b/testsuite/tests/simplCore/should_run/UnliftedArgRule.stdout
@@ -0,0 +1,2 @@
+Can you read this?
+1
diff --git a/testsuite/tests/simplCore/should_run/all.T b/testsuite/tests/simplCore/should_run/all.T
index 69a7475524..c8daab50eb 100644
--- a/testsuite/tests/simplCore/should_run/all.T
+++ b/testsuite/tests/simplCore/should_run/all.T
@@ -98,5 +98,5 @@ test('NumConstantFolding32', normal, compile_and_run, [''])
 test('NumConstantFolding', normal, compile_and_run, [''])
 test('T19413', normal, compile_and_run, [''])
 test('T20203', normal, compile, ['-O -dsuppress-all -dsuppress-uniques -dno-typeable-binds -ddump-simpl'])
-test('T19313', expect_broken(19131), compile_and_run, [''])
-
+test('T19313', normal, compile_and_run, [''])
+test('UnliftedArgRule', normal, compile_and_run, [''])
diff --git a/testsuite/tests/stranal/should_compile/T18894.stderr b/testsuite/tests/stranal/should_compile/T18894.stderr
index ba4a213e4c..22888e53a2 100644
--- a/testsuite/tests/stranal/should_compile/T18894.stderr
+++ b/testsuite/tests/stranal/should_compile/T18894.stderr
@@ -67,9 +67,10 @@ g2
                   Unf=Unf{Src=<vanilla>, TopLvl=False, Value=False, ConLike=False,
                           WorkFree=False, Expandable=False, Guidance=IF_ARGS [] 2 0}]
                  c1# = GHC.Prim.andI# 1# (GHC.Prim.<# wild 0#) } in
-               case GHC.Prim.quotInt# (GHC.Prim.-# 2# c1#) wild of wild
+               case GHC.Prim.-# (GHC.Prim.quotInt# (GHC.Prim.-# 2# c1#) wild) c1#
+               of ds2
                { __DEFAULT ->
-               GHC.Types.I# (GHC.Prim.-# wild c1#)
+               GHC.Types.I# ds2
                };
              0# -> GHC.Real.divZeroError @Int
            });
@@ -166,9 +167,10 @@ g1
                   Unf=Unf{Src=<vanilla>, TopLvl=False, Value=False, ConLike=False,
                           WorkFree=False, Expandable=False, Guidance=IF_ARGS [] 2 0}]
                  c1# = GHC.Prim.andI# 1# (GHC.Prim.<# wild 0#) } in
-               case GHC.Prim.quotInt# (GHC.Prim.-# 2# c1#) wild of wild
+               case GHC.Prim.-# (GHC.Prim.quotInt# (GHC.Prim.-# 2# c1#) wild) c1#
+               of ds2
                { __DEFAULT ->
-               GHC.Types.I# (GHC.Prim.-# wild c1#)
+               GHC.Types.I# ds2
                };
              0# -> GHC.Real.divZeroError @Int
            });
@@ -282,9 +284,10 @@ $wg2
                     Unf=Unf{Src=<vanilla>, TopLvl=False, Value=False, ConLike=False,
                             WorkFree=False, Expandable=False, Guidance=IF_ARGS [] 2 0}]
                    c1# = GHC.Prim.andI# 1# (GHC.Prim.<# wild 0#) } in
-                 case GHC.Prim.quotInt# (GHC.Prim.-# 2# c1#) wild of wild
+                 case GHC.Prim.-# (GHC.Prim.quotInt# (GHC.Prim.-# 2# c1#) wild) c1#
+                 of ds2
                  { __DEFAULT ->
-                 GHC.Types.I# (GHC.Prim.-# wild c1#)
+                 GHC.Types.I# ds2
                  };
                0# -> GHC.Real.divZeroError @Int
              } #);
@@ -345,9 +348,10 @@ $wg1
                     Unf=Unf{Src=<vanilla>, TopLvl=False, Value=False, ConLike=False,
                             WorkFree=False, Expandable=False, Guidance=IF_ARGS [] 2 0}]
                    c1# = GHC.Prim.andI# 1# (GHC.Prim.<# wild 0#) } in
-                 case GHC.Prim.quotInt# (GHC.Prim.-# 2# c1#) wild of wild
+                 case GHC.Prim.-# (GHC.Prim.quotInt# (GHC.Prim.-# 2# c1#) wild) c1#
+                 of ds2
                  { __DEFAULT ->
-                 GHC.Types.I# (GHC.Prim.-# wild c1#)
+                 GHC.Types.I# ds2
                  };
                0# -> GHC.Real.divZeroError @Int
              } #);
diff --git a/testsuite/tests/stranal/should_compile/T18903.stderr b/testsuite/tests/stranal/should_compile/T18903.stderr
index e44edd8507..d237e7434f 100644
--- a/testsuite/tests/stranal/should_compile/T18903.stderr
+++ b/testsuite/tests/stranal/should_compile/T18903.stderr
@@ -70,9 +70,10 @@ h = \ (m :: Int) ->
                            c1# :: GHC.Prim.Int#
                            [LclId]
                            c1# = GHC.Prim.andI# 1# (GHC.Prim.<# wild1 0#) } in
-                         case GHC.Prim.quotInt# (GHC.Prim.-# 2# c1#) wild1 of wild2
+                         case GHC.Prim.-# (GHC.Prim.quotInt# (GHC.Prim.-# 2# c1#) wild1) c1#
+                         of ds2
                          { __DEFAULT ->
-                         GHC.Types.I# (GHC.Prim.-# wild2 c1#)
+                         GHC.Types.I# ds2
                          };
                        0# -> GHC.Real.divZeroError @Int
                      } #);