Demand: Nested strict product demands (#18885)wip/T18885

Fixing #18903 gives us enough expressiveness to tackle #18885, where we
have

```hs
f :: Int -> Int
f y =
  let x
       | expensive y == 1 = (expensive (y+1), expensive (y+2))
       | otherwise        = (expensive (y+3), expensive (y+4))
  in case () of
       _ | expensive (y+5) == 42 -> fst x
       _ | expensive (y+6) == 41 -> fst x + snd x
       _ | otherwise             -> 0
```

Here, we used to give `x` demand `1P(1P(U),1P(U))`. The outer `1`
is because `x` is used lazily and the inner `1`s are redundant with
that fact. That leaves some expressiveness on the table. After this
change, we infer `1P(SP(U),1P(U))`, meaning that *whenever we evaluate
`x`*, we evaluate its first component strictly, effectively making
strictness product demands apply *relatively*. Usage product demands
still apply absolutely, though.

More details on how we could exploit the new language in
`Note [Absent sub-demands]`.

Fixes #18885.

There's a single remaining regression in `T9630`, which increases +16%
in residency but decreases slightly in total allocations. I checked
the heap profile, which doesn't suggest any obvious regressions.
Ticky doesn't point to the reason either, because total allocations
actually improved. I think it's OK to just accept it.

Metric Increase:
    T9630

18 files changed, 320 insertions, 37 deletions

diff --git a/compiler/GHC/Core/Opt/DmdAnal.hs b/compiler/GHC/Core/Opt/DmdAnal.hs
index 4869fb1fa9..ae8aab18a8 100644
--- a/compiler/GHC/Core/Opt/DmdAnal.hs
+++ b/compiler/GHC/Core/Opt/DmdAnal.hs
@@ -233,9 +233,10 @@ dmdAnal' env dmd (Case scrut case_bndr ty [(alt, bndrs, rhs)])
         (rhs_ty, rhs')           = dmdAnal env dmd rhs
         (alt_ty1, dmds)          = findBndrsDmds env rhs_ty bndrs
         (alt_ty2, case_bndr_dmd) = findBndrDmd env False alt_ty1 case_bndr
-        -- Evaluation cardinality on the case binder is irrelevant and a no-op.
-        -- What matters is its nested sub-demand!
-        (_ :* case_bndr_sd)      = case_bndr_dmd
+        -- The peelDmd below will lazify the relative sub-demands if the
+        -- case_bndr_dmd had lazy evaluation cardinality.
+        -- See Note [Absent sub-demand] in GHC.Types.Demand
+        case_bndr_sd             = peelDmd case_bndr_dmd
         -- Compute demand on the scrutinee
         (bndrs', scrut_sd)
           | DataAlt _ <- alt
@@ -388,9 +389,10 @@ dmdAnalSumAlt :: AnalEnv -> SubDemand -> Id -> Alt Var -> (DmdType, Alt Var)
 dmdAnalSumAlt env dmd case_bndr (con,bndrs,rhs)
   | (rhs_ty, rhs') <- dmdAnal env dmd rhs
   , (alt_ty, dmds) <- findBndrsDmds env rhs_ty bndrs
-  , let (_ :* case_bndr_sd) = findIdDemand alt_ty case_bndr
+  , let case_bndr_dmd = findIdDemand alt_ty case_bndr
         -- See Note [Demand on scrutinee of a product case]
-        id_dmds             = addCaseBndrDmd case_bndr_sd dmds
+        -- See Note [Absent sub-demand] in GHC.Types.Demand
+        id_dmds       = addCaseBndrDmd (peelDmd case_bndr_dmd) dmds
   = (alt_ty, (con, setBndrsDemandInfo bndrs id_dmds, rhs'))
 
 {-
diff --git a/compiler/GHC/Types/Demand.hs b/compiler/GHC/Types/Demand.hs
index 2ebc2222b4..fe9a3eec9f 100644
--- a/compiler/GHC/Types/Demand.hs
+++ b/compiler/GHC/Types/Demand.hs
@@ -35,7 +35,7 @@ module GHC.Types.Demand (
     -- ** Other @Demand@ operations
     oneifyCard, oneifyDmd, strictifyDmd, strictifyDictDmd, mkWorkerDemand,
     peelCallDmd, peelManyCalls, mkCallDmd, mkCallDmds,
-    addCaseBndrDmd,
+    peelDmd, addCaseBndrDmd,
     -- ** Extracting one-shot information
     argOneShots, argsOneShots, saturatedByOneShots,
 
@@ -231,8 +231,9 @@ multCard _    _    = C_0N
 --   * '$' puts demand @SCS(U)@ on its first argument: It calls (@C@) the
 --     argument function with one argument, exactly once (@S@). No info
 --     on how the result of that call is evaluated (@U@).
---   * 'maybe' puts demand @1C1(U)@ on its second argument: It evaluates
---     the argument function lazily and calls it once when it is evaluated.
+--   * 'maybe' puts demand @1CS(U)@ on its second argument: It evaluates
+--     the argument function lazily, but calls it exactly once when it is
+--     evaluated.
 --   * @fst p + fst p@ puts demand @MP(MU,A)@ on @p@: It's @SP(SU,A)@
 --     multiplied by two, so we get @M@ (used at least once, possibly multiple
 --     times).
@@ -252,6 +253,7 @@ data Demand
 -- @f@ is called exactly twice (@M@), each time exactly once (@S@) with an
 -- additional argument.
 --
+-- TODO: update following paragraph with intuition from #18885.
 -- The nested 'Demand's @dn@ of a 'Prod' @P(d1,d2,...)@ apply /absolutely/:
 -- If @dn@ is a used once demand (cf. 'isUsedOnce'), then that means that
 -- the denoted sub-expression is used once in the entire evaluation context
@@ -367,6 +369,9 @@ lubSubDmd _          _         = topSubDmd
 
 -- | Denotes '∪' on 'Demand'.
 lubDmd :: Demand -> Demand -> Demand
+-- See Note [Absent sub-demand] for the first two special cases
+lubDmd (C_00 :* _) (n2 :* sd2) = lubCard C_00 n2   :* lubSubDmd botSubDmd sd2
+lubDmd (n1 :* sd1) (C_00 :* _) = lubCard n1   C_00 :* lubSubDmd sd1       botSubDmd
 lubDmd (n1 :* sd1) (n2 :* sd2) = lubCard n1   n2   :* lubSubDmd sd1       sd2
 
 -- | Denotes '+' on 'SubDemand'.
@@ -459,20 +464,20 @@ evalDmd = C_1N :* topSubDmd
 strictOnceApply1Dmd :: Demand
 strictOnceApply1Dmd = C_11 :* Call C_11 topSubDmd
 
--- | First argument of 'GHC.Exts.atomically#': @MCM(U)@.
+-- | First argument of 'GHC.Exts.atomically#': @CM(U)@.
 -- Called at least once, possibly many times.
 strictManyApply1Dmd :: Demand
 strictManyApply1Dmd = C_1N :* Call C_1N topSubDmd
 
--- | First argument of catch#: @1C1(U)@.
+-- | First argument of catch#: @1CS(U)@.
 -- Evaluates its arg lazily, but then applies it exactly once to one argument.
 lazyApply1Dmd :: Demand
 lazyApply1Dmd = C_01 :* Call C_01 topSubDmd
 
--- | Second argument of catch#: @1C1(CS(U))@.
--- Calls its arg lazily, but then applies it exactly once to an additional argument.
+-- | Second argument of catch#: @1CS(CS(U))@.
+-- Evaluates its arg lazily, but then applies it exactly once to two arguments.
 lazyApply2Dmd :: Demand
-lazyApply2Dmd = C_01 :* Call C_01 (Call C_11 topSubDmd)
+lazyApply2Dmd = C_01 :* Call C_11 (Call C_11 topSubDmd)
 
 -- | Make a 'Demand' evaluated at-most-once.
 oneifyDmd :: Demand -> Demand
@@ -511,6 +516,14 @@ strictifyDictDmd ty (n :* Prod ds)
       = Nothing
 strictifyDictDmd _  dmd = dmd
 
+-- | Peels the evaluation cardinality of a 'Demand' and multiplies it with
+-- the relative parts of the 'SubDemand'. See Note [Absent sub-demand].
+peelDmd :: Demand -> SubDemand
+peelDmd (n :* sd)
+  | isAbs n    = seqSubDmd
+  | isStrict n = sd
+  | otherwise  = C_01 `multSubDmd` sd
+
 -- | Wraps the 'SubDemand' with a one-shot call demand: @d@ -> @CS(d)@.
 mkCallDmd :: SubDemand -> SubDemand
 mkCallDmd sd = Call C_11 sd
@@ -568,7 +581,7 @@ argsOneShots (StrictSig (DmdType _ arg_ds _)) n_val_args
 argOneShots :: Demand          -- ^ depending on saturation
             -> [OneShotInfo]
 -- ^ See Note [Computing one-shot info]
-argOneShots (_ :* sd) = go sd -- See Note [Call demands are relative]
+argOneShots (n :* sd) = go (multSubDmd n sd) -- See Note [Call demands are relative]
   where
     go (Call n sd)
       | isUsedOnce n = OneShotLam    : go sd
@@ -605,9 +618,9 @@ In #7319 we get
 Note [Call demands are relative]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 The expression @if b then 0 else f 1 2 + f 3 4@ uses @f@ according to the demand
-@UCU(CS(P(U)))@, meaning
+@UCM(CS(P(U)))@, meaning
 
-  "f is called multiple times or not at all (CU), but each time it
+  "f is called multiple times (CM) or not at all (U), but each time it
    is called, it's called with *exactly one* (CS) more argument.
    Whenever it is called with two arguments, we have no info on how often
    the field of the product result is used (U)."
@@ -627,7 +640,7 @@ call site. Consider (#18903)
       2 -> snd (g m)
       _ -> uncurry (+) (g m)
 
-We want to give @g@ the demand @1C1(P(1P(U),SP(U)))@, so we see that in each call
+We want to give @g@ the demand @1CS(P(1P(U),SP(U)))@, so we see that in each call
 site of @g@, we are strict in the second component of the returned pair.
 
 This relative cardinality leads to an otherwise unexpected call to 'lubSubDmd'
@@ -639,6 +652,67 @@ is hurt and we can assume that the nested demand is 'botSubDmd'. That ensures
 that @g@ above actually gets the @SP(U)@ demand on its second pair component,
 rather than the lazy @1P(U)@ if we 'lub'bed with an absent demand.
 
+Note [Absent sub-demand]
+~~~~~~~~~~~~~~~~~~~~~~~~
+What is does the sub-demand of an absent demand tell us? There's no sense in
+telling *how deep* something was evaluated if it was not evaluated *at all*!
+Since the upper bound on evaluation cardinality is 0, we are free to choose
+whatever sub-demand we want.
+
+In case of 'lubDmd', we want that sub-demand to be 'botSubDmd', for similar
+reasons as we want 'botSubDmd' in Note [Call demands are relative]. Here's
+an example (T18885):
+
+  f :: Int -> Int
+  f y =
+    let x
+         | expensive y == 1 = (expensive (y+1), expensive (y+2))
+         | otherwise        = (expensive (y+3), expensive (y+4))
+    in case () of
+         _ | expensive (y+5) == 42 -> fst x
+         _ | expensive (y+6) == 41 -> fst x + snd x
+         _ | otherwise             -> 0
+
+Without the 'botSubDmd' special case, the demand on @x@ is 1P(1P(U),1P(U)).
+The outer evaluation cardinality is lazy and recursively makes all field
+demands lazy, too, so there's plenty of syntactic structure in our product
+demand language we leave unused.
+But note how everytime we evaluate @x@ to WHNF, we also evaluate its first
+pair component! We could say @1P(SP(U),1P(U))@ to encode that and the
+'botSubDmd' special case gives us exactly the means to infer that!
+
+We could then go on to exploit the nested strictness by transforming @x@ to
+
+    let x
+         | expensive y == 1 = case expensive (y+1) of !n -> (n, expensive (y+2))
+         | otherwise        = case expensive (y+3) of !n -> (n, expensive (y+4))
+
+which would save allocation of a thunk. Unfortunately, we haven't written that
+transformation yet.
+
+But now we say (T18885b) that @test@ in
+
+  force :: (Int, Int) -> (Int, Int)
+  force p@(!x, !y) = p
+  {-# NOINLINE force #-}
+
+  test :: (Int, Int) -> Int -> (Int, Int)
+  test p z = case p of p'
+    (x, y) | odd z     -> force p
+           | otherwise -> (1, 2)
+
+has strictness signature <SP(SP(U),SP(U))><SP(U)>, which is wrong! @test@
+is not strict in the fields of @p@. The problem is that the case binder @p'@
+has demand 1P(SP(U),SP(U)) from the call to @force@. When we apply the field
+demands to the alt binders ('addCaseBndrDmd'), we get strict demands on @x@
+and @y@, which is wrong.
+The solution is that we have to multiply the vase binders evaluation
+cardinality onto its field demands when we unwrap it! The field demands are
+relative to one evaluation, so similarly to dmdAnalStar the field demands
+have to lazified if the evaluation cardinality wasn't strict.
+(But we have to leave the usage alone, because it's already absolute.)
+Hence we do 'peelDmd' before calling 'addCaseBndrDmd'.
+
 Demand on case-alternative binders]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 The demand on a binder in a case alternative comes
diff --git a/docs/users_guide/using-optimisation.rst b/docs/users_guide/using-optimisation.rst
index 8fec4f1a7b..8bb5870adc 100644
--- a/docs/users_guide/using-optimisation.rst
+++ b/docs/users_guide/using-optimisation.rst
@@ -1268,11 +1268,13 @@ by saying ``-fno-wombat``.
      maybe n _ Nothing  = n
      maybe _ s (Just a) = s a
 
-    We give it demand signature ``<U><1C1(U)><SU>``.  The ``C1(U)`` is a *call
-    sub-demand* that says "Called at most once, where the result is used
-    according to ``U``". The expression ``f `seq` f 1 2`` puts ``f`` under
-    demand ``MCS(U)`` and serves as an example where the upper bound on
-    evaluation cardinality doesn't conincide with that of the call cardinality.
+    We give it demand signature ``<U><1CS(U)><SU>``.  The ``CS(U)`` is a
+    *call sub-demand* that applies when the surrounding demand is evaluated
+    at all. It says "If evaluated, the thing is called exactly once, where
+    the result is used according to ``U``". The expression ``f `seq` f 1 2``
+    puts ``f`` under demand ``MCS(U)`` and serves as an example where the
+    upper bound on evaluation cardinality doesn't conincide with that of
+    the call cardinality.
 
     Cardinality is always relative to the enclosing call cardinality, so
     ``g 1 2 + g 3 4`` puts ``g`` under demand ``MCM(CS(U))``, which says
diff --git a/testsuite/tests/arityanal/should_compile/Arity11.stderr b/testsuite/tests/arityanal/should_compile/Arity11.stderr
index 77c790ae7b..82385e12f7 100644
--- a/testsuite/tests/arityanal/should_compile/Arity11.stderr
+++ b/testsuite/tests/arityanal/should_compile/Arity11.stderr
@@ -35,7 +35,7 @@ end Rec }
 
 -- RHS size: {terms: 52, types: 28, coercions: 0, joins: 0/5}
 F11.$wfib [InlPrag=[2]] :: forall {a} {p}. (a -> a -> Bool) -> (Num a, Num p) => a -> p
-[GblId, Arity=4, Str=<MCM(CS(U))><UP(A,UCU(CS(U)),A,A,A,A,UCU(U))><UP(UCU(CS(U)),A,A,A,A,A,1C1(U))><U>, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [60 150 60 0] 460 0}]
+[GblId, Arity=4, Str=<MCM(CS(U))><UP(A,UCU(CS(U)),A,A,A,A,UCM(U))><UP(MCM(CS(U)),A,A,A,A,A,1CS(U))><U>, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [60 150 60 0] 460 0}]
 F11.$wfib
   = \ (@a) (@p) (ww :: a -> a -> Bool) (w :: Num a) (w1 :: Num p) (w2 :: a) ->
       let {
diff --git a/testsuite/tests/arityanal/should_compile/Arity14.stderr b/testsuite/tests/arityanal/should_compile/Arity14.stderr
index 1a5fdc38c3..0727a56a5f 100644
--- a/testsuite/tests/arityanal/should_compile/Arity14.stderr
+++ b/testsuite/tests/arityanal/should_compile/Arity14.stderr
@@ -18,7 +18,7 @@ F14.f2 = 1
 
 -- RHS size: {terms: 35, types: 24, coercions: 0, joins: 0/3}
 F14.$wf14 [InlPrag=[2]] :: forall {t}. (t -> t -> Bool) -> Num t => t -> t -> t -> t
-[GblId, Arity=4, Str=<MCM(CS(U))><UP(UCU(CS(U)),A,A,A,A,A,1C1(U))><U><U>, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [60 90 0 0] 300 0}]
+[GblId, Arity=4, Str=<MCM(CS(U))><UP(UCU(CS(U)),A,A,A,A,A,1CS(U))><U><U>, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [60 90 0 0] 300 0}]
 F14.$wf14
   = \ (@t) (ww :: t -> t -> Bool) (w :: Num t) (w1 :: t) (w2 :: t) ->
       let {
diff --git a/testsuite/tests/simplCore/should_compile/T4908.stderr b/testsuite/tests/simplCore/should_compile/T4908.stderr
index 5db6bc8506..3aed9e3c3c 100644
--- a/testsuite/tests/simplCore/should_compile/T4908.stderr
+++ b/testsuite/tests/simplCore/should_compile/T4908.stderr
@@ -59,7 +59,7 @@ end Rec }
 T4908.$wf [InlPrag=[2]] :: Int# -> (Int, Int) -> Bool
 [GblId,
  Arity=2,
- Str=<SU><1P(A,1P(1U))>,
+ Str=<SU><1P(A,SP(SU))>,
  Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
          WorkFree=True, Expandable=True, Guidance=IF_ARGS [30 20] 101 20}]
 T4908.$wf
diff --git a/testsuite/tests/stranal/should_compile/T18885.hs b/testsuite/tests/stranal/should_compile/T18885.hs
new file mode 100644
index 0000000000..99b1f788ee
--- /dev/null
+++ b/testsuite/tests/stranal/should_compile/T18885.hs
@@ -0,0 +1,17 @@
+{-# OPTIONS_GHC -O2 -fforce-recomp #-}
+
+module T18885 where
+
+expensive :: Int -> Int
+expensive n = sum [0..n]
+{-# NOINLINE expensive #-}
+
+f :: Int -> Int
+f y =
+  let x
+       | expensive y == 1 = (expensive (y+1), expensive (y+2))
+       | otherwise        = (expensive (y+3), expensive (y+4))
+  in case () of
+       _ | expensive (y+5) == 42 -> fst x
+       _ | expensive (y+6) == 41 -> fst x + snd x
+       _ | otherwise             -> 0
diff --git a/testsuite/tests/stranal/should_compile/T18885.stderr b/testsuite/tests/stranal/should_compile/T18885.stderr
new file mode 100644
index 0000000000..d30f14cde8
--- /dev/null
+++ b/testsuite/tests/stranal/should_compile/T18885.stderr
@@ -0,0 +1,151 @@
+
+==================== Tidy Core ====================
+Result size of Tidy Core
+  = {terms: 143, types: 59, coercions: 0, joins: 1/2}
+
+-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
+T18885.$trModule4 :: GHC.Prim.Addr#
+[GblId,
+ Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
+         WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 20 0}]
+T18885.$trModule4 = "main"#
+
+-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
+T18885.$trModule3 :: GHC.Types.TrName
+[GblId,
+ Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
+         WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 10}]
+T18885.$trModule3 = GHC.Types.TrNameS T18885.$trModule4
+
+-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
+T18885.$trModule2 :: GHC.Prim.Addr#
+[GblId,
+ Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
+         WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 30 0}]
+T18885.$trModule2 = "T18885"#
+
+-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
+T18885.$trModule1 :: GHC.Types.TrName
+[GblId,
+ Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
+         WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 10}]
+T18885.$trModule1 = GHC.Types.TrNameS T18885.$trModule2
+
+-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
+T18885.$trModule :: GHC.Types.Module
+[GblId,
+ Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
+         WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 10}]
+T18885.$trModule
+  = GHC.Types.Module T18885.$trModule3 T18885.$trModule1
+
+-- RHS size: {terms: 30, types: 8, coercions: 0, joins: 1/1}
+T18885.$wexpensive [InlPrag=NOINLINE]
+  :: GHC.Prim.Int# -> GHC.Prim.Int#
+[GblId, Arity=1, Str=<U>, Unf=OtherCon []]
+T18885.$wexpensive
+  = \ (ww :: GHC.Prim.Int#) ->
+      case GHC.Prim.># 0# ww of {
+        __DEFAULT ->
+          joinrec {
+            $wgo9 [InlPrag=[2], Occ=LoopBreaker]
+              :: GHC.Prim.Int# -> GHC.Prim.Int# -> GHC.Prim.Int#
+            [LclId[JoinId(2)], Arity=2, Str=<U><U>, Unf=OtherCon []]
+            $wgo9 (w :: GHC.Prim.Int#) (ww1 :: GHC.Prim.Int#)
+              = case GHC.Prim.==# w ww of {
+                  __DEFAULT -> jump $wgo9 (GHC.Prim.+# w 1#) (GHC.Prim.+# ww1 w);
+                  1# -> GHC.Prim.+# ww1 w
+                }; } in
+          jump $wgo9 0# 0#;
+        1# -> 0#
+      }
+
+-- RHS size: {terms: 10, types: 4, coercions: 0, joins: 0/0}
+expensive [InlPrag=[final]] :: Int -> Int
+[GblId,
+ Arity=1,
+ Str=<SP(U)>,
+ Cpr=m1,
+ Unf=Unf{Src=InlineStable, TopLvl=True, Value=True, ConLike=True,
+         WorkFree=True, Expandable=True,
+         Guidance=ALWAYS_IF(arity=1,unsat_ok=True,boring_ok=False)
+         Tmpl= \ (w [Occ=Once1!] :: Int) ->
+                 case w of { GHC.Types.I# ww1 [Occ=Once1] ->
+                 case T18885.$wexpensive ww1 of ww2 [Occ=Once1] { __DEFAULT ->
+                 GHC.Types.I# ww2
+                 }
+                 }}]
+expensive
+  = \ (w :: Int) ->
+      case w of { GHC.Types.I# ww1 ->
+      case T18885.$wexpensive ww1 of ww2 { __DEFAULT ->
+      GHC.Types.I# ww2
+      }
+      }
+
+-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
+T18885.f1 :: Int
+[GblId,
+ Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
+         WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 10}]
+T18885.f1 = GHC.Types.I# 0#
+
+-- RHS size: {terms: 76, types: 30, coercions: 0, joins: 0/1}
+T18885.$wf [InlPrag=[2]] :: GHC.Prim.Int# -> Int
+[GblId,
+ Arity=1,
+ Str=<U>,
+ Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
+         WorkFree=True, Expandable=True, Guidance=IF_ARGS [0] 377 10}]
+T18885.$wf
+  = \ (ww :: GHC.Prim.Int#) ->
+      case T18885.$wexpensive (GHC.Prim.+# ww 5#) of ww1 { __DEFAULT ->
+      let {
+        x [Dmd=1P(SP(U),1P(U))] :: (Int, Int)
+        [LclId]
+        x = case T18885.$wexpensive ww of {
+              __DEFAULT ->
+                (case T18885.$wexpensive (GHC.Prim.+# ww 3#) of ww3 { __DEFAULT ->
+                 GHC.Types.I# ww3
+                 },
+                 case T18885.$wexpensive (GHC.Prim.+# ww 4#) of ww3 { __DEFAULT ->
+                 GHC.Types.I# ww3
+                 });
+              1# ->
+                (case T18885.$wexpensive (GHC.Prim.+# ww 1#) of ww3 { __DEFAULT ->
+                 GHC.Types.I# ww3
+                 },
+                 case T18885.$wexpensive (GHC.Prim.+# ww 2#) of ww3 { __DEFAULT ->
+                 GHC.Types.I# ww3
+                 })
+            } } in
+      case ww1 of {
+        __DEFAULT ->
+          case T18885.$wexpensive (GHC.Prim.+# ww 6#) of {
+            __DEFAULT -> T18885.f1;
+            41# ->
+              case x of { (x1, ds1) ->
+              case x1 of { GHC.Types.I# x2 ->
+              case ds1 of { GHC.Types.I# y -> GHC.Types.I# (GHC.Prim.+# x2 y) }
+              }
+              }
+          };
+        42# -> case x of { (x1, ds1) -> x1 }
+      }
+      }
+
+-- RHS size: {terms: 6, types: 3, coercions: 0, joins: 0/0}
+f [InlPrag=[2]] :: Int -> Int
+[GblId,
+ Arity=1,
+ Str=<SP(U)>,
+ Unf=Unf{Src=InlineStable, TopLvl=True, Value=True, ConLike=True,
+         WorkFree=True, Expandable=True,
+         Guidance=ALWAYS_IF(arity=1,unsat_ok=True,boring_ok=False)
+         Tmpl= \ (w [Occ=Once1!] :: Int) ->
+                 case w of { GHC.Types.I# ww1 [Occ=Once1] -> T18885.$wf ww1 }}]
+f = \ (w :: Int) ->
+      case w of { GHC.Types.I# ww1 -> T18885.$wf ww1 }
+
+
+
diff --git a/testsuite/tests/stranal/should_compile/T18903.stderr b/testsuite/tests/stranal/should_compile/T18903.stderr
index 4adbdd566c..983d1c0184 100644
--- a/testsuite/tests/stranal/should_compile/T18903.stderr
+++ b/testsuite/tests/stranal/should_compile/T18903.stderr
@@ -63,7 +63,7 @@ T18903.$wh [InlPrag=[2]] :: GHC.Prim.Int# -> Int
 T18903.$wh
   = \ (ww :: GHC.Prim.Int#) ->
       let {
-        $wg [InlPrag=NOINLINE, Dmd=1C1(P(1P(U),SP(U)))]
+        $wg [InlPrag=NOINLINE, Dmd=1CS(P(1P(U),SP(U)))]
           :: GHC.Prim.Int# -> (# Int, Int #)
         [LclId, Arity=1, Str=<SU>, Unf=OtherCon []]
         $wg
diff --git a/testsuite/tests/stranal/should_compile/all.T b/testsuite/tests/stranal/should_compile/all.T
index 1262ad426e..d756f91d3c 100644
--- a/testsuite/tests/stranal/should_compile/all.T
+++ b/testsuite/tests/stranal/should_compile/all.T
@@ -58,3 +58,5 @@ test('T18122',  [ grep_errmsg(r'wfoo =') ], compile, ['-ddump-simpl'])
 
 # We care about the call demand on $wg
 test('T18903',  [ grep_errmsg(r'Dmd=\S+C\S+') ], compile, ['-ddump-simpl -dsuppress-uniques'])
+# We care about the nested strict product demand on x
+test('T18885',  [ grep_errmsg(r'Dmd=1P\(SP\(\S+') ], compile, ['-ddump-simpl -dsuppress-uniques'])
diff --git a/testsuite/tests/stranal/sigs/CaseBinderCPR.stderr b/testsuite/tests/stranal/sigs/CaseBinderCPR.stderr
index ca6d3015ff..6366e23584 100644
--- a/testsuite/tests/stranal/sigs/CaseBinderCPR.stderr
+++ b/testsuite/tests/stranal/sigs/CaseBinderCPR.stderr
@@ -1,7 +1,7 @@
 
 ==================== Strictness signatures ====================
 CaseBinderCPR.$trModule:
-CaseBinderCPR.f_list_cmp: <UCU(CS(P(MU)))><SU><SU>
+CaseBinderCPR.f_list_cmp: <UCM(CS(P(MU)))><SU><SU>
 
 
 
diff --git a/testsuite/tests/stranal/sigs/T18086.stderr b/testsuite/tests/stranal/sigs/T18086.stderr
index 0ac4c846ee..1d9b036d00 100644
--- a/testsuite/tests/stranal/sigs/T18086.stderr
+++ b/testsuite/tests/stranal/sigs/T18086.stderr
@@ -2,7 +2,7 @@
 ==================== Strictness signatures ====================
 T18086.$trModule:
 T18086.m: <U>x
-T18086.panic: <U>x
+T18086.panic: <UM>x
 
 
 
@@ -16,6 +16,6 @@ T18086.panic:
 ==================== Strictness signatures ====================
 T18086.$trModule:
 T18086.m: <U>x
-T18086.panic: <U>x
+T18086.panic: <UM>x
 
 
diff --git a/testsuite/tests/stranal/sigs/T18885b.hs b/testsuite/tests/stranal/sigs/T18885b.hs
new file mode 100644
index 0000000000..556dcd5d76
--- /dev/null
+++ b/testsuite/tests/stranal/sigs/T18885b.hs
@@ -0,0 +1,13 @@
+{-# OPTIONS_GHC -O2 -fforce-recomp #-}
+{-# LANGUAGE BangPatterns #-}
+
+module T18885b where
+
+force :: (Int, Int) -> (Int, Int)
+force p@(!x, !y) = p
+{-# NOINLINE force #-}
+
+test :: (Int, Int) -> Int -> (Int, Int)
+test p z = case p of
+  (x, y) | odd z     -> force p
+         | otherwise -> (1, 2)
diff --git a/testsuite/tests/stranal/sigs/T18885b.stderr b/testsuite/tests/stranal/sigs/T18885b.stderr
new file mode 100644
index 0000000000..717c6c074d
--- /dev/null
+++ b/testsuite/tests/stranal/sigs/T18885b.stderr
@@ -0,0 +1,21 @@
+
+==================== Strictness signatures ====================
+T18885b.$trModule:
+T18885b.force: <SP(MU,MU)>
+T18885b.test: <SP(U,U)><SP(U)>
+
+
+
+==================== Cpr signatures ====================
+T18885b.$trModule:
+T18885b.force: m1
+T18885b.test: m1
+
+
+
+==================== Strictness signatures ====================
+T18885b.$trModule:
+T18885b.force: <SP(SP(U),SP(U))>
+T18885b.test: <SP(1P(U),1P(U))><SP(U)>
+
+
diff --git a/testsuite/tests/stranal/sigs/T18957.stderr b/testsuite/tests/stranal/sigs/T18957.stderr
index c536410e0a..863a6a51a9 100644
--- a/testsuite/tests/stranal/sigs/T18957.stderr
+++ b/testsuite/tests/stranal/sigs/T18957.stderr
@@ -1,10 +1,10 @@
 
 ==================== Strictness signatures ====================
 T18957.$trModule:
-T18957.g: <1C1(U)><SP(U)>
-T18957.h1: <MC1(U)><SP(U)>
+T18957.g: <1CS(U)><SP(U)>
+T18957.h1: <MCS(U)><SP(U)>
 T18957.h2: <SC1(U)><SP(U)>
-T18957.h3: <UCU(P(U))><SP(U)>
+T18957.h3: <UCM(P(U))><SP(U)>
 T18957.seq': <SA><SU>
 
 
@@ -21,10 +21,10 @@ T18957.seq':
 
 ==================== Strictness signatures ====================
 T18957.$trModule:
-T18957.g: <1C1(U)><SP(U)>
+T18957.g: <1CS(U)><SP(U)>
 T18957.h1: <MC1(U)><SP(U)>
 T18957.h2: <SC1(U)><SP(U)>
-T18957.h3: <UCU(P(U))><SP(U)>
+T18957.h3: <UCM(P(U))><SP(U)>
 T18957.seq': <SA><SU>
 
 
diff --git a/testsuite/tests/stranal/sigs/T5075.stderr b/testsuite/tests/stranal/sigs/T5075.stderr
index 64a78d05ec..b7f1edd744 100644
--- a/testsuite/tests/stranal/sigs/T5075.stderr
+++ b/testsuite/tests/stranal/sigs/T5075.stderr
@@ -1,7 +1,7 @@
 
 ==================== Strictness signatures ====================
 T5075.$trModule:
-T5075.loop: <MP(A,A,MCM(CS(U)),A,A,A,A,A)><UP(A,A,UCU(CS(U)),A,A,A,UCU(U))><U>
+T5075.loop: <MP(A,A,MCM(CS(U)),A,A,A,A,A)><UP(A,A,UCU(CS(U)),A,A,A,UCM(U))><U>
 
 
 
diff --git a/testsuite/tests/stranal/sigs/UnsatFun.stderr b/testsuite/tests/stranal/sigs/UnsatFun.stderr
index 18723bad40..cf15cb8120 100644
--- a/testsuite/tests/stranal/sigs/UnsatFun.stderr
+++ b/testsuite/tests/stranal/sigs/UnsatFun.stderr
@@ -6,7 +6,7 @@ UnsatFun.g: <SP(M)>b
 UnsatFun.g': <1P(U)>
 UnsatFun.g3: <A>
 UnsatFun.h: <SCS(U)>
-UnsatFun.h2: <SU><1C1(U)>
+UnsatFun.h2: <SU><1CS(U)>
 UnsatFun.h3: <SCS(A)>
 
 
@@ -30,7 +30,7 @@ UnsatFun.g: <SP(M)>b
 UnsatFun.g': <1P(U)>
 UnsatFun.g3: <A>
 UnsatFun.h: <SCS(U)>
-UnsatFun.h2: <SU><1C1(U)>
+UnsatFun.h2: <SU><1CS(U)>
 UnsatFun.h3: <SCS(A)>
 
 
diff --git a/testsuite/tests/stranal/sigs/all.T b/testsuite/tests/stranal/sigs/all.T
index 07cc815823..a93c0078e5 100644
--- a/testsuite/tests/stranal/sigs/all.T
+++ b/testsuite/tests/stranal/sigs/all.T
@@ -23,4 +23,5 @@ test('T17932', normal, compile, [''])
 test('T13380c', expect_broken('!3014'), compile, [''])
 test('T13380f', normal, compile, [''])
 test('T18086', normal, compile, ['-package ghc'])
+test('T18885b', normal, compile, [''])
 test('T18957', normal, compile, [''])