Assume at least one evaluation for nested SubDemands (#21081, #21133)wip/T21081

See the new `Note [SubDemand denotes at least one evaluation]`.

A demand `n :* sd` on a let binder `x=e` now means

> "`x` was evaluated `n` times and in any program trace it is evaluated, `e` is
>  evaluated deeply in sub-demand `sd`."

The "any time it is evaluated" premise is what this patch adds. As a result,
we get better nested strictness. For example (T21081)
```hs
f :: (Bool, Bool) -> (Bool, Bool)
f pr = (case pr of (a,b) -> a /= b, True)
-- before: <MP(L,L)>
-- after:  <MP(SL,SL)>

g :: Int -> (Bool, Bool)
g x = let y = let z = odd x in (z,z) in f y
```
The change in demand signature "before" to "after" allows us to case-bind `z`
here.

Similarly good things happen for the `sd` in call sub-demands `Cn(sd)`, which
allows for more eta-reduction (which is only sound with `-fno-pedantic-bottoms`,
albeit).

We also fix #21085, a surprising inconsistency with `Poly` to `Call` sub-demand
expansion.

In an attempt to fix a regression caused by less inlining due to eta-reduction
in T15426, I eta-expanded the definition of `elemIndex` and `elemIndices`, thus
fixing #21345 on the go.

The main point of this patch is that it fixes #21081 and #21133.

Annoyingly, I discovered that more precise demand signatures for join points can
transform a program into a lazier program if that join point gets floated to the
top-level, see #21392. There is no simple fix at the moment, but !5349 might.
Thus, we accept a ~5% regression in `MultiLayerModulesTH_OneShot`, where #21392
bites us in `addListToUniqDSet`. T21392 reliably reproduces the issue.

Surprisingly, ghc/alloc perf on Windows improves much more than on other jobs, by
0.4% in the geometric mean and by 2% in T16875.

Metric Increase:
    MultiLayerModulesTH_OneShot
Metric Decrease:
    T16875

53 files changed, 853 insertions, 488 deletions

diff --git a/compiler/GHC/Core/Opt/Arity.hs b/compiler/GHC/Core/Opt/Arity.hs
index 6c0729ec5b..7125397637 100644
--- a/compiler/GHC/Core/Opt/Arity.hs
+++ b/compiler/GHC/Core/Opt/Arity.hs
@@ -359,6 +359,9 @@ this transformation.  So we try to limit it as much as possible:
 
 Of course both (1) and (2) are readily defeated by disguising the bottoms.
 
+Another place where -fpedantic-bottoms comes up is during eta-reduction.
+See Note [Eta reduction soundness], the bit about -fpedantic-bottoms.
+
 4. Note [Newtype arity]
 ~~~~~~~~~~~~~~~~~~~~~~~~
 Non-recursive newtypes are transparent, and should not get in the way.
diff --git a/compiler/GHC/Core/Opt/DmdAnal.hs b/compiler/GHC/Core/Opt/DmdAnal.hs
index ca51fd5f4c..b01e6f502a 100644
--- a/compiler/GHC/Core/Opt/DmdAnal.hs
+++ b/compiler/GHC/Core/Opt/DmdAnal.hs
@@ -413,7 +413,7 @@ dmdAnal' env dmd (App fun arg)
 --         , text "arg dmd =" <+> ppr arg_dmd
 --         , text "arg dmd_ty =" <+> ppr arg_ty
 --         , text "res dmd_ty =" <+> ppr res_ty
---         , text "overall res dmd_ty =" <+> ppr (res_ty `bothDmdType` arg_ty) ])
+--         , text "overall res dmd_ty =" <+> ppr (res_ty `plusDmdType` arg_ty) ])
     WithDmdType (res_ty `plusDmdType` arg_ty) (App fun' arg')
 
 dmdAnal' env dmd (Lam var body)
@@ -447,7 +447,7 @@ dmdAnal' env dmd (Case scrut case_bndr ty [Alt alt bndrs rhs])
         -- What matters is its nested sub-demand!
         -- NB: If case_bndr_dmd is absDmd, boxity will say Unboxed, which is
         -- what we want, because then `seq` will put a `seqDmd` on its scrut.
-        (_ :* case_bndr_sd) = case_bndr_dmd
+        (_ :* case_bndr_sd) = strictifyDmd case_bndr_dmd
         -- Compute demand on the scrutinee
         -- FORCE the result, otherwise thunks will end up retaining the
         -- whole DmdEnv
@@ -520,7 +520,7 @@ dmdAnal' env dmd (Case scrut case_bndr ty alts)
     in
 --    pprTrace "dmdAnal:Case2" (vcat [ text "scrut" <+> ppr scrut
 --                                   , text "scrut_ty" <+> ppr scrut_ty
---                                   , text "alt_tys" <+> ppr alt_tys
+--                                   , text "alt_ty1" <+> ppr alt_ty1
 --                                   , text "alt_ty2" <+> ppr alt_ty2
 --                                   , text "res_ty" <+> ppr res_ty ]) $
     WithDmdType res_ty (Case scrut' case_bndr' ty alts')
@@ -576,7 +576,8 @@ dmdAnalSumAlt env dmd case_bndr (Alt con bndrs rhs)
         (!_scrut_sd, dmds') = addCaseBndrDmd case_bndr_sd dmds
         -- Do not put a thunk into the Alt
         !new_ids            = setBndrsDemandInfo bndrs dmds'
-  = WithDmdType alt_ty (Alt con new_ids rhs')
+  = -- pprTrace "dmdAnalSumAlt" (ppr con $$ ppr case_bndr $$ ppr dmd $$ ppr alt_ty) $
+    WithDmdType alt_ty (Alt con new_ids rhs')
 
 -- Precondition: The SubDemand is not a Call
 -- See Note [Demand on the scrutinee of a product case]
@@ -588,6 +589,7 @@ addCaseBndrDmd :: SubDemand -- On the case binder
                             -- and final demands for the components of the constructor
 addCaseBndrDmd case_sd fld_dmds
   | Just (_, ds) <- viewProd (length fld_dmds) scrut_sd
+  -- , pprTrace "addCaseBndrDmd" (ppr case_sd $$ ppr fld_dmds $$ ppr scrut_sd) True
   = (scrut_sd, ds)
   | otherwise
   = pprPanic "was a call demand" (ppr case_sd $$ ppr fld_dmds) -- See the Precondition
@@ -879,7 +881,8 @@ dmdTransform :: AnalEnv   -- ^ The analysis environment
 dmdTransform env var sd
   -- Data constructors
   | isDataConWorkId var
-  = dmdTransformDataConSig (idArity var) sd
+  = -- pprTraceWith "dmdTransform:DataCon" (\ty -> ppr var $$ ppr sd $$ ppr ty) $
+    dmdTransformDataConSig (idArity var) sd
   -- Dictionary component selectors
   -- Used to be controlled by a flag.
   -- See #18429 for some perf measurements.
@@ -1744,7 +1747,7 @@ dmdFix top_lvl env let_dmd orig_pairs
     -- annotation does not change any more.
     loop :: Int -> [(Id,CoreExpr)] -> (AnalEnv, DmdEnv, [(Id,CoreExpr)])
     loop n pairs = -- pprTrace "dmdFix" (ppr n <+> vcat [ ppr id <+> ppr (idDmdSig id)
-                   --                                     | (id,_)<- pairs]) $
+                   --                                   | (id,_) <- pairs]) $
                    loop' n pairs
 
     loop' n pairs
diff --git a/compiler/GHC/Core/Opt/Simplify/Utils.hs b/compiler/GHC/Core/Opt/Simplify/Utils.hs
index 1c0e228e79..ce69e35aea 100644
--- a/compiler/GHC/Core/Opt/Simplify/Utils.hs
+++ b/compiler/GHC/Core/Opt/Simplify/Utils.hs
@@ -1655,7 +1655,10 @@ mkLam env bndrs body cont
 
     -- See Note [Eta reduction based on evaluation context]
     -- NB: cont is never ApplyToVal, otherwise contEvalContext panics
-    eval_sd = contEvalContext cont
+    eval_sd dflags | gopt Opt_PedanticBottoms dflags = topSubDmd
+                       -- See Note [Eta reduction soundness], criterion (S)
+                       -- the bit about -fpedantic-bottoms
+                   | otherwise                       = contEvalContext cont
 
     mkLam' :: DynFlags -> [OutBndr] -> OutExpr -> SimplM OutExpr
     mkLam' dflags bndrs body@(Lam {})
@@ -1679,8 +1682,8 @@ mkLam env bndrs body cont
 
     mkLam' dflags bndrs body
       | gopt Opt_DoEtaReduction dflags
-      -- , pprTrace "try eta" (ppr bndrs $$ ppr body $$ ppr cont $$ ppr eval_sd) True
-      , Just etad_lam <- {-# SCC "tryee" #-} tryEtaReduce bndrs body eval_sd
+      -- , pprTrace "try eta" (ppr bndrs $$ ppr body $$ ppr cont $$ ppr (eval_sd dflags)) True
+      , Just etad_lam <- {-# SCC "tryee" #-} tryEtaReduce bndrs body (eval_sd dflags)
       = do { tick (EtaReduction (head bndrs))
            ; return etad_lam }
 
diff --git a/compiler/GHC/Core/Utils.hs b/compiler/GHC/Core/Utils.hs
index eea81d1502..b4c736bcdc 100644
--- a/compiler/GHC/Core/Utils.hs
+++ b/compiler/GHC/Core/Utils.hs
@@ -2409,13 +2409,20 @@ case where `e` is trivial):
     like `g (\x y z. e x y z)` to `g e`, because that diverges when
     `e = \x y. bot`.
 
-    Could we relax to "At least *one call in the same trace* is with n args"?
+    Could we relax to "*At least one call in the same trace* is with n args"?
+    (NB: Strictness analysis can only answer this relaxed question, not the
+     original formulation.)
     Consider what happens for
       ``g2 c = c True `seq` c False 42``
-    Here, `g2` will call `c` with 2 two arguments (if there is a call at all).
-    But it is unsafe to eta-reduce the arg in `g2 (\x y. e x y)` to `g2 e`
+    Here, `g2` will call `c` with 2 arguments (if there is a call at all).
+    But it is unsound to eta-reduce the arg in `g2 (\x y. e x y)` to `g2 e`
     when `e = \x. if x then bot else id`, because the latter will diverge when
     the former would not.
+    On the other hand, with `-fno-pendantic-bottoms` , we will have eta-expanded
+    the definition of `e` and then eta-reduction is sound
+    (see Note [Dealing with bottom]).
+    Consequence: We have to check that `-fpedantic-bottoms` is off; otherwise
+    eta-reduction based on demands is in fact unsound.
 
     See Note [Eta reduction based on evaluation context] for the implementation
     details. This criterion is tested extensively in T21261.
diff --git a/compiler/GHC/CoreToStg/Prep.hs b/compiler/GHC/CoreToStg/Prep.hs
index fa9496b4c5..7b52fd637b 100644
--- a/compiler/GHC/CoreToStg/Prep.hs
+++ b/compiler/GHC/CoreToStg/Prep.hs
@@ -1636,10 +1636,12 @@ tryEtaReducePrep bndrs expr@(App _ _)
   , exprIsHNF remaining_expr   -- Don't turn value into a non-value
                                -- else the behaviour with 'seq' changes
   =
-    -- pprTrace "prep-reduce" (
-    --   text "reduced:" <> ppr remaining_expr $$
-    --   ppr (remaining_args)
-    --   ) $
+    -- pprTrace "prep-reduce" (vcat
+    --   [ text "reduced:" <+> ppr expr
+    --   , text "from" <+> ppr (length args) <+> text "to" <+> ppr n_remaining
+    --   , (case f of Var v -> text "has strict worker:" <+> ppr (idCbvMarkArity v) <+> ppr n_remaining_vals; _ -> empty)
+    --   , ppr remaining_args
+    --   ]) $
     Just remaining_expr
   where
     (f, args) = collectArgs expr
diff --git a/compiler/GHC/Stg/InferTags/Rewrite.hs b/compiler/GHC/Stg/InferTags/Rewrite.hs
index e35f700377..8076507a1c 100644
--- a/compiler/GHC/Stg/InferTags/Rewrite.hs
+++ b/compiler/GHC/Stg/InferTags/Rewrite.hs
@@ -38,7 +38,6 @@ import GHC.Stg.Syntax as StgSyn
 
 import GHC.Data.Maybe
 import GHC.Utils.Panic
-import GHC.Utils.Panic.Plain
 
 import GHC.Utils.Outputable
 import GHC.Utils.Monad.State.Strict
@@ -425,7 +424,7 @@ rewriteApp _ (StgApp f args)
     | Just marks <- idCbvMarks_maybe f
     , relevant_marks <- dropWhileEndLE (not . isMarkedCbv) marks
     , any isMarkedCbv relevant_marks
-    = assert (length relevant_marks <= length args)
+    = assertPpr (length relevant_marks <= length args) (ppr f $$ ppr args $$ ppr relevant_marks)
       unliftArg relevant_marks
 
     where
diff --git a/compiler/GHC/Stg/Lift/Analysis.hs b/compiler/GHC/Stg/Lift/Analysis.hs
index 6fc116c8bc..6b46b5125c 100644
--- a/compiler/GHC/Stg/Lift/Analysis.hs
+++ b/compiler/GHC/Stg/Lift/Analysis.hs
@@ -326,7 +326,7 @@ tagSkeletonRhs bndr (StgRhsClosure fvs ccs upd bndrs body)
 rhsCard :: Id -> Card
 rhsCard bndr
   | is_thunk  = oneifyCard n
-  | otherwise = peelManyCalls (idArity bndr) cd
+  | otherwise = n `multCard` peelManyCalls (idArity bndr) cd
   where
     is_thunk = idArity bndr == 0
     -- Let's pray idDemandInfo is still OK after unarise...
diff --git a/compiler/GHC/Types/Demand.hs b/compiler/GHC/Types/Demand.hs
index 19d1938557..ad890ee31d 100644
--- a/compiler/GHC/Types/Demand.hs
+++ b/compiler/GHC/Types/Demand.hs
@@ -2,8 +2,6 @@
 {-# LANGUAGE BinaryLiterals #-}
 {-# LANGUAGE PatternSynonyms #-}
 
-{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
-
 {-
 (c) The University of Glasgow 2006
 (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
@@ -380,9 +378,6 @@ lubBoxity :: Boxity -> Boxity -> Boxity
 -- See Note [Boxity analysis] for the lattice.
 lubBoxity = boxedWins
 
-plusBoxity :: Boxity -> Boxity -> Boxity
-plusBoxity = boxedWins
-
 {-
 ************************************************************************
 *                                                                      *
@@ -477,6 +472,7 @@ here that says what they should compute.
       - Handy special cases:
           o 'plusCard C_10' bumps up the strictness of its argument, just like
             'lubCard C_00' lazifies it, without touching upper bounds.
+            See also 'strictifyCard'
           o Similarly, 'plusCard C_0N' discards usage information
             (incl. absence) but leaves strictness alone.
 
@@ -565,15 +561,22 @@ isCardNonOnce n = isAbs n || not (isUsedOnce n)
 
 -- | Intersect with [0,1].
 oneifyCard :: Card -> Card
-oneifyCard C_0N = C_01
-oneifyCard C_1N = C_11
-oneifyCard c    = c
+oneifyCard = glbCard C_01
+
+-- | Intersect with [1,n]. The same as @'plusCard' 'C_10'@.
+strictifyCard :: Card -> Card
+strictifyCard = glbCard C_1N
 
 -- | Denotes '∪' on 'Card'.
 lubCard :: Card -> Card -> Card
 -- See Note [Bit vector representation for Card]
 lubCard (Card a) (Card b) = Card (a .|. b) -- main point of the bit-vector encoding!
 
+-- | Denotes '∩' on 'Card'.
+glbCard :: Card -> Card -> Card
+-- See Note [Bit vector representation for Card]
+glbCard (Card a) (Card b) = Card (a .&. b)
+
 -- | Denotes '+' on lower and upper bounds of 'Card'.
 plusCard :: Card -> Card -> Card
 -- See Note [Algebraic specification for plusCard and multCard]
@@ -594,6 +597,26 @@ multCard (Card a) (Card b)
     bit1 = (a .&. b)                   .&. 0b010
     bitN = (a .|. b) .&. shiftL bit1 1 .&. 0b100
 
+-- | Denotes '∪' on lower and '+' on upper bounds of 'Card'.
+lubPlusCard :: Card -> Card -> Card
+-- See Note [Algebraic specification for plusCard and multCard]
+lubPlusCard (Card a) (Card b)
+  = Card (bit0 .|. bit1 .|. bitN)
+  where
+    bit0 =  (a .|. b)                         .&. 0b001
+    bit1 =  (a .|. b)                         .&. 0b010
+    bitN = ((a .|. b) .|. shiftL (a .&. b) 1) .&. 0b100
+
+-- | Denotes '+' on lower and '∪' on upper bounds of 'Card'.
+plusLubCard :: Card -> Card -> Card
+-- See Note [Algebraic specification for plusCard and multCard]
+plusLubCard (Card a) (Card b)
+  = Card (bit0 .|. bit1 .|. bitN)
+  where
+    bit0 = (a .&. b) .&. 0b001
+    bit1 = (a .|. b) .&. 0b010
+    bitN = (a .|. b) .&. 0b100
+
 {-
 ************************************************************************
 *                                                                      *
@@ -647,7 +670,7 @@ data Demand
 -- | Only meant to be used in the pattern synonym below!
 viewDmdPair :: Demand -> (Card, SubDemand)
 viewDmdPair BotDmd   = (C_10, botSubDmd)
-viewDmdPair AbsDmd   = (C_00, seqSubDmd)
+viewDmdPair AbsDmd   = (C_00, botSubDmd)
 viewDmdPair (D n sd) = (n, sd)
 
 -- | @c :* sd@ is a demand that says \"evaluated @c@ times, and each time it
@@ -667,27 +690,17 @@ viewDmdPair (D n sd) = (n, sd)
 pattern (:*) :: HasDebugCallStack => Card -> SubDemand -> Demand
 pattern n :* sd <- (viewDmdPair -> (n, sd)) where
   C_10 :* sd = BotDmd & assertPpr (sd == botSubDmd) (text "B /=" <+> ppr sd)
-  C_00 :* sd = AbsDmd & assertPpr (sd == seqSubDmd) (text "A /=" <+> ppr sd)
+  C_00 :* sd = AbsDmd & assertPpr (sd == botSubDmd) (text "A /=" <+> ppr sd)
   n    :* sd = D n sd & assertPpr (isCardNonAbs n)  (ppr n $$ ppr sd)
 {-# COMPLETE (:*) #-}
 
 -- | A sub-demand describes an /evaluation context/, e.g. how deep the
 -- denoted thing is evaluated. See 'Demand' for examples.
 --
--- The nested 'SubDemand' @d@ of a 'Call' @Cn(d)@ is /relative/ to a single such call.
--- E.g. The expression @f 1 2 + f 3 4@ puts call demand @SCS(C1(L))@ on @f@:
--- @f@ is called exactly twice (@S@), each time exactly once (@1@) with an
--- additional argument.
+-- See Note [SubDemand denotes at least one evaluation] for a more detailed
+-- description of what a sub-demand means.
 --
--- 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
--- described by the surrounding 'Demand'. E.g., @LP(ML)@ means that the
--- field of the denoted expression is used at most once, although the
--- entire expression might be used many times.
---
--- See Note [Call demands are relative]
--- and Note [Demand notation].
+-- See Note [Demand notation] for the extensively used short-hand notation.
 -- See also Note [Why Boxity in SubDemand and not in Demand?].
 data SubDemand
   = Poly !Boxity !CardNonOnce
@@ -702,7 +715,7 @@ data SubDemand
   --
   -- In Note [Demand notation]: @L  === P(L,L,...)@  and @L  === CL(L)@,
   --                            @B  === P(B,B,...)@  and @B  === CB(B)@,
-  --                            @!A === !P(A,A,...)@ and @!A === !CA(A)@,
+  --                            @!A === !P(A,A,...)@ and @!A === !CA(B)@,
   --                            and so on.
   --
   -- We'll only see 'Poly' with 'C_10' (B), 'C_00' (A), 'C_0N' (L) and sometimes
@@ -710,8 +723,10 @@ data SubDemand
   -- source code). Hence 'CardNonOnce', which is closed under 'lub' and 'plus'.
   | Call !CardNonAbs !SubDemand
   -- ^ @Call n sd@ describes the evaluation context of @n@ function
-  -- applications, where every individual result is evaluated according to @sd@.
-  -- @sd@ is /relative/ to a single call, see Note [Call demands are relative].
+  -- applications (with one argument), where the result of each call is
+  -- evaluated according to @sd@.
+  -- @sd@ describes program traces in which the denoted thing was called at all,
+  -- see Note [SubDemand denotes at least one evaluation].
   -- That Note also explains why it doesn't make sense for @n@ to be absent,
   -- hence we forbid it with 'CardNonAbs'. Absent call demands can still be
   -- expressed with 'Poly'.
@@ -784,19 +799,21 @@ viewProd _ _
                         -- for Arity. Otherwise, #18304 bites us.
 
 -- | A smart constructor for 'Call', applying rewrite rules along the semantic
--- equality @Call n (Poly n) === Poly n@, simplifying to 'Poly' 'SubDemand's
+-- equality @Call C_0N (Poly C_0N) === Poly C_0N@, simplifying to 'Poly' 'SubDemand's
 -- when possible.
 mkCall :: CardNonAbs -> SubDemand -> SubDemand
 mkCall C_1N sd@(Poly Boxed C_1N) = sd
 mkCall C_0N sd@(Poly Boxed C_0N) = sd
-mkCall n    cd               = assertPpr (isCardNonAbs n) (ppr n $$ ppr cd) $
-                               Call n cd
+mkCall n    sd                   = assertPpr (isCardNonAbs n) (ppr n $$ ppr sd) $
+                                   Call n sd
 
 -- | @viewCall sd@ interprets @sd@ as a 'Call', expanding 'Poly' subdemands as
 -- necessary.
 viewCall :: SubDemand -> Maybe (Card, SubDemand)
 viewCall (Call n sd) = Just (n :: Card, sd)
-viewCall (Poly _ n)  = Just (n :: Card, Poly Boxed n)
+viewCall (Poly _ n)
+  | isAbs n          = Just (n :: Card, botSubDmd)
+  | otherwise        = Just (n :: Card, Poly Boxed n)
 viewCall _           = Nothing
 
 topDmd, absDmd, botDmd, seqDmd :: Demand
@@ -817,37 +834,9 @@ unboxDeeplyDmd AbsDmd   = AbsDmd
 unboxDeeplyDmd BotDmd   = BotDmd
 unboxDeeplyDmd (D n sd) = D n (unboxDeeplySubDmd sd)
 
--- | Denotes '∪' on 'SubDemand'.
-lubSubDmd :: SubDemand -> SubDemand -> SubDemand
--- Handle botSubDmd (just an optimisation, the general case would do the same)
-lubSubDmd (Poly Unboxed C_10) d2                  = d2
-lubSubDmd d1                  (Poly Unboxed C_10) = d1
--- Handle Prod
-lubSubDmd (Prod b1 ds1) (Poly b2 n2)
-  | let !d = polyFieldDmd b2 n2
-  = mkProd (lubBoxity b1 b2) (strictMap (lubDmd d) ds1)
-lubSubDmd (Prod b1 ds1) (Prod b2 ds2)
-  | equalLength ds1 ds2
-  = mkProd (lubBoxity b1 b2) (strictZipWith lubDmd ds1 ds2)
--- Handle Call
-lubSubDmd (Call n1 sd1) sd2@(Poly _ n2)
-  -- See Note [Call demands are relative]
-  | isAbs n2  = mkCall (lubCard n2 n1) sd1
-  | otherwise = mkCall (lubCard n2 n1) (lubSubDmd sd1 sd2)
-lubSubDmd (Call n1 d1)  (Call n2 d2)
-  | otherwise = mkCall (lubCard n1 n2) (lubSubDmd d1 d2)
--- Handle Poly. Exploit reflexivity (so we'll match the Prod or Call cases again).
-lubSubDmd (Poly b1 n1)  (Poly b2 n2) = Poly (lubBoxity b1 b2) (lubCard n1 n2)
-lubSubDmd sd1@Poly{}    sd2          = lubSubDmd sd2 sd1
--- Otherwise (Call `lub` Prod) return Top
-lubSubDmd _             _            = topSubDmd
-
--- | Denotes '∪' on 'Demand'.
-lubDmd :: Demand -> Demand -> Demand
-lubDmd (n1 :* sd1) (n2 :* sd2) = lubCard n1 n2 :* lubSubDmd sd1 sd2
 
 multSubDmd :: Card -> SubDemand -> SubDemand
-multSubDmd C_11 sd           = sd
+multSubDmd C_11 sd           = sd -- An optimisation, for when sd is a deep Prod
 -- The following three equations don't have an impact on Demands, only on
 -- Boxity. They are needed so that we don't trigger the assertions in `:*`
 -- when called from `multDmd`.
@@ -855,45 +844,189 @@ multSubDmd C_00 _            = seqSubDmd -- Otherwise `multSubDmd A L == A /= !A
 multSubDmd C_10 (Poly _ n)   = if isStrict n then botSubDmd else seqSubDmd -- Otherwise `multSubDmd B L == B /= !B`
 multSubDmd C_10 (Call n _)   = if isStrict n then botSubDmd else seqSubDmd -- Otherwise we'd call `mkCall` with absent cardinality
 multSubDmd n    (Poly b m)   = Poly b (multCard n m)
-multSubDmd n    (Call n' sd) = mkCall (multCard n n') sd -- See Note [Call demands are relative]
+multSubDmd n    (Call n' sd) = mkCall (multCard n n') sd
 multSubDmd n    (Prod b ds)  = mkProd b (strictMap (multDmd n) ds)
 
 multDmd :: Card -> Demand -> Demand
--- The first two lines compute the same result as the last line, but won't
--- trigger the assertion in `:*` for input like `multDmd B 1L`, which would call
--- `B :* A`. We want to return `B` in these cases.
-multDmd C_10 (n :* _)    = if isStrict n then BotDmd else AbsDmd
-multDmd n    (C_10 :* _) = if isStrict n then BotDmd else AbsDmd
-multDmd n    (m :* sd)   = multCard n m :* multSubDmd n sd
+multDmd C_11 dmd       = dmd -- An optimisation
+-- The following four lines make sure that we rewrite to AbsDmd and BotDmd
+-- whenever the leading cardinality is absent (C_00 or C_10).
+-- Otherwise it may happen that the SubDemand is not 'botSubDmd', triggering
+-- the assertion in `:*`.
+-- Example: `multDmd B 1L = BA`, so with an inner `seqSubDmd`. Our lattice
+-- allows us to always rewrite this to proper BotDmd and we maintain the
+-- invariant that this is indeed the case.
+multDmd C_00 _        = AbsDmd
+multDmd _    AbsDmd   = AbsDmd
+multDmd C_10 (D n _)  = if isStrict n then BotDmd else AbsDmd
+multDmd n    BotDmd   = if isStrict n then BotDmd else AbsDmd
+-- See Note [SubDemand denotes at least one evaluation] for the strictifyCard
+multDmd n    (D m sd) = multCard n m :* multSubDmd (strictifyCard n) sd
+
+{- Note [Manual specialisation of lub*Dmd/plus*Dmd]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+As Note [SubDemand denotes at least one evaluation] points out, we need all 4
+different combinations of lub/plus demand operations on upper and lower bounds
+  lubDmd, plusDmd, lubPlusDmd, plusLubDmd
+and the same for lubSubDmd, etc. In order to share as much code as possible
+and for the programmer to see immediately how the operations differ, we have
+one implementation of opDmd (and opSubDmd) that dispatches on a 'OpMode'.
+
+For good perf, we specialise this one implementation to the four different
+modes. So ideally we'd write
+```
+lubSubDmd = opSubDmd (Lub, Lub)
+opSubDmd (l, u) = ... opSubDmd ...
+{-# RULES "lubSubDmd" opSubDmd (Lub, Lub) = lubSubDmd #-}
+```
+But unfortunately, 'opSubDmd' will be picked as a loop-breaker and thus never
+inline into 'lubSubDmd', so its body will never actually be specialised for
+the op mode `(Lub, Lub)`. So instead we write
+```
+lubSubDmd = opSubDmdInl (Lub, Lub)
+opSubDmdInl (l, u) = ... opSubDmd ...
+{-# INLINE opSubDmdInl #-}
+opSubDmd = opSubDmdInl
+{-# RULES "lubSubDmd" forall l r. opSubDmd (Lub, Lub) = lubSubDmd #-}
+```
+Here, 'opSubDmdInl' will not be picked as the loop-breaker and thus inline into
+'lubSubDmd' and 'opSubDmd'. Since the latter will never inline, we'll specialise
+all call sites of 'opSubDmd' for the proper op mode. A nice trick!
+-}
+
+data LubOrPlus = Lub | Plus deriving Show
+instance Outputable LubOrPlus where ppr = text . show
+
+-- | Determines whether to use 'LubOrPlus' for lower bounds and upper bounds,
+-- respectively. See Note [Manual specialisation of lub*Dmd/plus*Dmd].
+type OpMode = (LubOrPlus, LubOrPlus)
+
+-- | Denotes '∪' on 'SubDemand'.
+lubSubDmd :: SubDemand -> SubDemand -> SubDemand
+-- See Note [Manual specialisation of lub*Dmd/plus*Dmd]
+lubSubDmd l r = opSubDmdInl (Lub, Lub) l r
+
+-- | Denotes '∪' on 'Demand'.
+lubDmd :: Demand -> Demand -> Demand
+-- See Note [Manual specialisation of lub*Dmd/plus*Dmd]
+lubDmd l r = opDmdInl (Lub, Lub) l r
 
 -- | Denotes '+' on 'SubDemand'.
 plusSubDmd :: SubDemand -> SubDemand -> SubDemand
--- Handle seqSubDmd (just an optimisation, the general case would do the same)
-plusSubDmd (Poly Unboxed C_00) d2                  = d2
-plusSubDmd d1                  (Poly Unboxed C_00) = d1
+-- See Note [Manual specialisation of lub*Dmd/plus*Dmd]
+plusSubDmd l r = opSubDmdInl (Plus, Plus) l r
+
+-- | Denotes '+' on 'Demand'.
+plusDmd :: Demand -> Demand -> Demand
+-- See Note [Manual specialisation of lub*Dmd/plus*Dmd]
+plusDmd l r = opDmdInl (Plus, Plus) l r
+
+-- | Denotes '∪' on lower bounds and '+' on upper bounds on 'SubDemand'.
+lubPlusSubDmd :: SubDemand -> SubDemand -> SubDemand
+-- See Note [Manual specialisation of lub*Dmd/plus*Dmd]
+lubPlusSubDmd l r = opSubDmdInl (Lub, Plus) l r
+
+-- | Denotes '∪' on lower bounds and '+' on upper bounds on 'Demand'.
+lubPlusDmd :: Demand -> Demand -> Demand
+-- See Note [Manual specialisation of lub*Dmd/plus*Dmd]
+lubPlusDmd l r = opDmdInl (Lub, Plus) l r
+
+-- | Denotes '+' on lower bounds and '∪' on upper bounds on 'SubDemand'.
+plusLubSubDmd :: SubDemand -> SubDemand -> SubDemand
+-- See Note [Manual specialisation of lub*Dmd/plus*Dmd]
+plusLubSubDmd l r = opSubDmdInl (Plus, Lub) l r
+
+-- | Denotes '∪' on lower bounds and '+' on upper bounds on 'SubDemand'.
+plusLubDmd :: Demand -> Demand -> Demand
+-- See Note [Manual specialisation of lub*Dmd/plus*Dmd]
+plusLubDmd l r = opDmdInl (Plus, Lub) l r
+
+-- See Note [Manual specialisation of lub*Dmd/plus*Dmd]
+{-# RULES "lubSubDmd"     opSubDmd (Lub, Lub)   = lubSubDmd #-}
+{-# RULES "lubDmd"        opDmd (Lub, Lub)      = lubDmd #-}
+{-# RULES "plusSubDmd"    opSubDmd (Plus, Plus) = plusSubDmd #-}
+{-# RULES "plusDmd"       opDmd (Plus, Plus)    = plusDmd #-}
+{-# RULES "lubPlusSubDmd" opSubDmd (Lub, Plus)  = lubPlusSubDmd #-}
+{-# RULES "lubPlusDmd"    opDmd (Lub, Plus)     = lubPlusDmd #-}
+{-# RULES "plusLubSubDmd" opSubDmd (Plus, Lub)  = plusLubSubDmd #-}
+{-# RULES "plusLubDmd"    opDmd (Plus, Lub)     = plusLubDmd #-}
+
+--
+-- And now the actual implementation that is to be specialised:
+--
+
+neutralCard :: OpMode -> Card
+neutralCard (Lub, _)  = C_10
+neutralCard (Plus, _) = C_00
+{-# INLINE neutralCard #-}
+
+absorbingCard :: OpMode -> Card
+absorbingCard (Lub, _)  = C_0N
+absorbingCard (Plus, _) = C_1N
+{-# INLINE absorbingCard #-}
+
+opCard :: OpMode -> Card -> Card -> Card
+opCard (Lub,  Lub)  = lubCard
+opCard (Lub,  Plus) = lubPlusCard
+opCard (Plus, Lub)  = plusLubCard
+opCard (Plus, Plus) = plusCard
+{-# INLINE opCard #-}
+
+opDmdInl, opDmd :: OpMode -> Demand -> Demand -> Demand
+opDmdInl m       (n1 :* _)   dmd2        | n1 == neutralCard m = dmd2
+opDmdInl m       dmd1        (n2 :* _)   | n2 == neutralCard m = dmd1
+opDmdInl m@(l,u) (n1 :* sd1) (n2 :* sd2) = -- pprTraceWith "opDmd" (\it -> ppr l <+> ppr u $$ ppr (n1:*sd1) $$ ppr (n2:*sd2) $$ ppr it) $
+  opCard m n1 n2 :* case l of
+    Lub  -> opSubDmd m sd1 sd2
+    -- For Plus, there are four special cases due to strictness demands and
+    -- Note [SubDemand denotes at least one evaluation]:
+    Plus -> case (isStrict n1, isStrict n2) of
+      (True,  True)  -> opSubDmd (Plus, u) sd1 sd2                  -- (D1)
+      (True,  False) -> opSubDmd (Plus, u) sd1 (lazifySubDmd sd2)   -- (D2)
+      (False, True)  -> opSubDmd (Plus, u) (lazifySubDmd sd1) sd2   -- (D2)
+      (False, False) -> opSubDmd (Lub, u)  sd1 sd2                  -- (D3)
+
+-- See Note [Manual specialisation of lub*Dmd/plus*Dmd]
+opDmd = opDmdInl
+{-# INLINE opDmdInl #-}
+{-# NOINLINE opDmd #-}
+
+opSubDmdInl, opSubDmd :: OpMode -> SubDemand -> SubDemand -> SubDemand
+-- Shortcuts for neutral and absorbing elements.
+-- Below we assume that Boxed always wins.
+opSubDmdInl m (Poly Unboxed n)  sd                | n == neutralCard m   = sd
+opSubDmdInl m sd                (Poly Unboxed n)  | n == neutralCard m   = sd
+opSubDmdInl m sd@(Poly Boxed n) _                 | n == absorbingCard m = sd
+opSubDmdInl m _                 sd@(Poly Boxed n) | n == absorbingCard m = sd
 -- Handle Prod
-plusSubDmd (Prod b1 ds1) (Poly b2 n2)
+opSubDmdInl m (Prod b1 ds1) (Poly b2 n2)
   | let !d = polyFieldDmd b2 n2
-  = mkProd (plusBoxity b1 b2) (strictMap (plusDmd d) ds1)
-plusSubDmd (Prod b1 ds1) (Prod b2 ds2)
+  = mkProd (lubBoxity b1 b2) (strictMap (opDmd m d) ds1)
+opSubDmdInl m (Prod b1 ds1) (Prod b2 ds2)
   | equalLength ds1 ds2
-  = mkProd (plusBoxity b1 b2) (strictZipWith plusDmd ds1 ds2)
+  = mkProd (lubBoxity b1 b2) (strictZipWith (opDmd m) ds1 ds2)
 -- Handle Call
-plusSubDmd (Call n1 sd1) sd2@(Poly _ n2)
-  -- See Note [Call demands are relative]
-  | isAbs n2  = mkCall (plusCard n2 n1) sd1
-  | otherwise = mkCall (plusCard n2 n1) (lubSubDmd sd1 sd2)
-plusSubDmd (Call n1 sd1) (Call n2 sd2)
-  | otherwise = mkCall (plusCard n1 n2) (lubSubDmd sd1 sd2)
--- Handle Poly. Exploit reflexivity (so we'll match the Prod or Call cases again).
-plusSubDmd (Poly b1 n1) (Poly b2 n2) = Poly (plusBoxity b1 b2) (plusCard n1 n2)
-plusSubDmd sd1@Poly{}   sd2          = plusSubDmd sd2 sd1
--- Otherwise (Call `lub` Prod) return Top
-plusSubDmd _            _            = topSubDmd
-
--- | Denotes '+' on 'Demand'.
-plusDmd :: Demand -> Demand -> Demand
-plusDmd (n1 :* sd1) (n2 :* sd2) = plusCard n1 n2 :* plusSubDmd sd1 sd2
+opSubDmdInl m@(l, _) (Call n1 sd1) (viewCall -> Just (n2, sd2)) =
+  mkCall (opCard m n1 n2) $! case l of
+    Lub  -> opSubDmd (Lub, Lub) sd1 sd2
+    -- For Plus, there are four special cases due to strictness demands and
+    -- Note [SubDemand denotes at least one evaluation]. Usage is always lubbed:
+    Plus -> case (isStrict n1, isStrict n2) of
+      (True,  True)  -> opSubDmd (Plus, Lub) sd1 sd2                  -- (C3)
+      (False, True)  -> opSubDmd (Plus, Lub) (lazifySubDmd sd1) sd2   -- (C2)
+      (True,  False) -> opSubDmd (Plus, Lub) sd1 (lazifySubDmd sd2)   -- (C2)
+      (False, False) -> opSubDmd (Lub,  Lub) sd1 sd2                  -- (C1)
+-- Handle Poly
+opSubDmdInl m (Poly b1 n1) (Poly b2 n2) = Poly (lubBoxity b1 b2) (opCard m n1 n2)
+-- Other Poly case by commutativity
+opSubDmdInl m sd1@Poly{}   sd2          = opSubDmd m sd2 sd1
+-- Otherwise (Call `op` Prod) return Top
+opSubDmdInl _ _            _            = topSubDmd
+
+-- See Note [Manual specialisation of lub*Dmd/plus*Dmd]
+opSubDmd = opSubDmdInl
+{-# INLINE opSubDmdInl #-}
+{-# NOINLINE opSubDmd #-}
 
 -- | Used to suppress pretty-printing of an uninformative demand
 isTopDmd :: Demand -> Bool
@@ -931,7 +1064,7 @@ isWeakDmd dmd@(n :* _) = not (isStrict n) && is_plus_idem_dmd dmd
     -- is_plus_idem_sub_dmd sd = plusSubDmd sd sd == sd
     is_plus_idem_sub_dmd (Poly _ n)  = assert (isCardNonOnce n) True
     is_plus_idem_sub_dmd (Prod _ ds) = all is_plus_idem_dmd ds
-    is_plus_idem_sub_dmd (Call n _)  = is_plus_idem_card n -- See Note [Call demands are relative]
+    is_plus_idem_sub_dmd (Call n _)  = is_plus_idem_card n
 
 evalDmd :: Demand
 evalDmd = C_1N :* topSubDmd
@@ -964,9 +1097,7 @@ oneifyDmd (n :* sd) = oneifyCard n :* sd
 
 -- | Make a 'Demand' evaluated at-least-once (e.g. strict).
 strictifyDmd :: Demand -> Demand
-strictifyDmd AbsDmd    = seqDmd
-strictifyDmd BotDmd    = BotDmd
-strictifyDmd (n :* sd) = plusCard C_10 n :* sd
+strictifyDmd = plusDmd seqDmd
 
 -- | If the argument is a used non-newtype dictionary, give it strict demand.
 -- Also split the product type & demand and recur in order to similarly
@@ -991,17 +1122,14 @@ strictifyDictDmd ty (n :* Prod b ds)
       = Nothing
 strictifyDictDmd _  dmd = dmd
 
--- | Make a 'Demand' lazy, setting all lower bounds (outside 'Call's) to 0.
+-- | Make a 'Demand' lazy.
 lazifyDmd :: Demand -> Demand
-lazifyDmd AbsDmd    = AbsDmd
-lazifyDmd BotDmd    = AbsDmd
-lazifyDmd (n :* sd) = multCard C_01 n :* lazifySubDmd sd
+lazifyDmd = multDmd C_01
+
 
--- | Make a 'SubDemand' lazy, setting all lower bounds (outside 'Call's) to 0.
+-- | Make a 'SubDemand' lazy.
 lazifySubDmd :: SubDemand -> SubDemand
-lazifySubDmd (Poly b n)  = Poly b (multCard C_01 n)
-lazifySubDmd (Prod b sd) = mkProd b (strictMap lazifyDmd sd)
-lazifySubDmd (Call n sd) = mkCall (lubCard C_01 n) sd
+lazifySubDmd = multSubDmd C_01
 
 -- | Wraps the 'SubDemand' with a one-shot call demand: @d@ -> @C1(d)@.
 mkCalledOnceDmd :: SubDemand -> SubDemand
@@ -1022,7 +1150,6 @@ peelCallDmd sd = viewCall sd `orElse` (topCard, topSubDmd)
 -- See Note [Demands from unsaturated function calls].
 peelManyCalls :: Int -> SubDemand -> Card
 peelManyCalls 0 _                          = C_11
--- See Note [Call demands are relative]
 peelManyCalls n (viewCall -> Just (m, sd)) = m `multCard` peelManyCalls (n-1) sd
 peelManyCalls _ _                          = C_0N
 
@@ -1059,7 +1186,7 @@ argOneShots :: Demand          -- ^ depending on saturation
 argOneShots AbsDmd    = [] -- This defn conflicts with 'saturatedByOneShots',
 argOneShots BotDmd    = [] -- according to which we should return
                            -- @repeat OneShotLam@ here...
-argOneShots (_ :* sd) = go sd -- See Note [Call demands are relative]
+argOneShots (_ :* sd) = go sd
   where
     go (Call n sd)
       | isUsedOnce n = OneShotLam    : go sd
@@ -1096,42 +1223,134 @@ but it's really a bad idea to *ever* evaluate an absent argument.
 In #7319 we get
    T7319.exe: Oops!  Entered absent arg w_s1Hd{v} [lid] [base:GHC.Base.String{tc 36u}]
 
-Note [Call demands are relative]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-The expression @if b then 0 else f 1 2 + f 3 4@ uses @f@ according to the demand
-@LCL(C1(P(L)))@, meaning
-
-  "f is called multiple times or not at all (CL), but each time it
-   is called, it's called with *exactly one* (C1) more argument.
-   Whenever it is called with two arguments, we have no info on how often
-   the field of the product result is used (L)."
-
-So the 'SubDemand' nested in a 'Call' demand is relative to exactly one call.
-And that extends to the information we have how its results are used in each
-call site. Consider (#18903)
-
-  h :: Int -> Int
-  h m =
-    let g :: Int -> (Int,Int)
-        g 1 = (m, 0)
-        g n = (2 * n, 2 `div` n)
-        {-# NOINLINE g #-}
-    in case m of
-      1 -> 0
-      2 -> snd (g m)
-      _ -> uncurry (+) (g m)
-
-We want to give @g@ the demand @MCM(P(MP(L),1P(L)))@, 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'
-in 'plusSubDmd', but if you do the math it's just the right thing.
-
-There's one more subtlety: Since the nested demand is relative to exactly one
-call, in the case where we have *at most zero calls* (e.g. CA(...)), the premise
-is hurt and we can assume that the nested demand is 'botSubDmd'. That ensures
-that @g@ above actually gets the @1P(L)@ demand on its second pair component,
-rather than the lazy @MP(L)@ if we 'lub'bed with an absent demand.
+Note [SubDemand denotes at least one evaluation]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider a demand `n :* sd` on a binding `let x = e in <body>`.
+(Similarly, a call sub-demand `Cn(sd)` on a lambda `\_. e`).
+While `n` describes how *often* `x` had been evaluated in <body>,
+the sub-demand `sd` describes how *deep* `e` has been evaluated, under the
+following
+
+  PREMISE: *for all program traces where `x` had been evaluated at all*
+
+That is, `sd` disregards all program traces where `x` had not been evaluated,
+because it can't describe the depth of an evaluation that never happened.
+NB: The Premise only makes a difference for lower bounds/strictness.
+Upper bounds/usage are unaffected by adding or leaving out evaluations that
+never happen.
+
+So if `x` was demanded with `LP(1L)`, so perhaps `<body>` was
+  f1 x = (x `seq` case x of (a,b) -> a, True)
+then `x` will be evaluated lazily, but any time `x` is evaluated, `e` is
+evaluated with sub-demand `P(1L)`, e.g., the first field of `e` is evaluated
+strictly, too.
+
+How does the additional strictness help? The long version is in #21081.
+The short version is
+
+  * We get to take advantage of call-by-value/let-to-case in more situations.
+    See example "More let-to-case" below.
+  * Note [Eta reduction based on evaluation context] applies in more situations.
+    See example "More eta reduction" below.
+  * We get to unbox more results, see example "More CPR" below.
+  * We prevent annoying issues with `Poly` equalities, #21085. In short, we'd get
+    `L + S = S = CS(S) < CS(L) = C(L+S)(LuS) = L + CS(S)` although `S = CS(S)`.
+
+It seems like we don't give up anything in return. Indeed that is the case:
+
+  * If we dropped the Premise, then a lazy `n` in `nP(m..)` would always force
+    `m` to be lazy, too. That is quite redundant! It seems wasteful not to use
+    the lower bound of `m` for something more useful. So indeed we give up on
+    nothing in return for some nice wins.
+  * Even if `n` is absent (so the Premise does hold for no trace whatsoever),
+    it's pretty easy to describe how `e` was evaluated. Answer: 'botSubDmd'.
+    We use it when expanding 'Absent' and 'Bottom' demands in 'viewDmdPair' as
+    well as when expanding absent 'Poly's to 'Call' sub-demands in 'viewCall'.
+
+Of course, we now have to maintain the Premise when we unpack and rebuild
+SubDemands. For strict demands, we know that the Premise indeed always holds for
+any program trace abstracted over, whereas we have to be careful for lazy
+demands.
+That makes for a strange definition of `plusDmd`, where we use `plusSubDmd`
+throughout for upper bounds (every eval returns the same, memoised heap object),
+but what we do on lower bounds depends on the strictness of both arguments:
+
+ D1 `plusSubDmd` on the nested SubDemands if both args are strict.
+ D2 `plusSubDmd` on the nested SubDemands if one of them is lazy, which we
+    *lazify* before (that's new), so that e.g.
+      `LP(SL) + SP(L) = (L+S)P((M*SL)+L) = SP(L+L) = SP(L)`
+    Multiplying with `M`/`C_01` is the "lazify" part here.
+    Example proving that point:
+        d2 :: <LP(SL)><SP(A)>
+        d2 x y = y `seq` (case x of (a,b) -> a, True)
+        -- What is demand on x in (d2 x x)? NOT SP(SL)!!
+ D3 `lubPlusSubDmd` on the nested SubDemands if both args are lazy.
+    This new operation combines `lubSubDmd` on lower bounds with `plusSubDmd`
+    on upper bounds.
+    Examples proving that point:
+        d3 :: <LP(SL)><LP(A)>
+        d3 x y = (case x of (a,b) -> a, y `seq` ())
+        -- What is demand on x in `snd (d3 x x)`?
+        -- Not LP(SL)!!  d3 might evaluate second argument but not first.
+        -- Lub lower bounds because we might evaluate one OR the other.
+
+Similarly, in the handling of Call SubDemands `Cn(sd)` in `plusSubDmd`, we use
+`lub` for upper bounds (because every call returns a fresh heap object), but
+what we do for lower bounds depends on whether the outer `n`s are strict:
+
+ C1 `lubSubDmd` on the nested SubDemands if both args are lazy.
+ C2 `plusLubSubDmd` on the nested `sd`s if one of the `n`s is lazy. That one's
+    nested `sd` we *lazify*, so that e.g.
+      `CL(SL) + CS(L) = C(L+S)((M*SL)+L) = CS(L+L) = CS(L)`
+    `plusLubSubDmd` combines `plusSubDmd` on lower bounds with `lubSubDmd` on
+    upper bounds.
+ C3 `plusLubSubDmd` on the nested SubDemands if both args are strict.
+
+There are a couple of other examples in T21081.
+Here is a selection of examples demonstrating the
+usefulness of The Premise:
+
+  * "More let-to-case" (from testcase T21081):
+    ```hs
+    f :: (Bool, Bool) -> (Bool, Bool)
+    f pr = (case pr of (a,b) -> a /= b, True)
+    g :: Int -> (Bool, Bool)
+    g x = let y = let z = odd x in (z,z) in f y
+    ```
+    Although `f` is lazy in `pr`, we could case-bind `z` because it is always
+    evaluated when `y` is evaluated. So we give `pr` demand `LP(SL,SL)`
+    (most likely with better upper bounds/usage) and demand analysis then
+    infers a strict demand for `z`.
+
+  * "More eta reduction" (from testcase T21081):
+    ```hs
+    myfoldl :: (a -> b -> a) -> a -> [b] -> a
+    myfoldl f z [] = z
+    myfoldl f !z (x:xs) = myfoldl (\a b -> f a b) (f z x) xs
+    ```
+    Here, we can give `f` a demand of `LCS(C1(L))` (instead of the lazier
+    `LCL(C1(L))`) which says "Whenever `f` is evaluated (lazily), it is also
+    called with two arguments".
+    And Note [Eta reduction based on evaluation context] means we can rewrite
+    `\a b -> f a b` to `f` in the call site of `myfoldl`. Nice!
+
+  * "More CPR" (from testcase T18903):
+    ```hs
+    h :: Int -> Int
+    h m =
+      let g :: Int -> (Int,Int)
+          g 1 = (m, 0)
+          g n = (2 * n, 2 `div` n)
+          {-# NOINLINE g #-}
+      in case m of
+        1 -> 0
+        2 -> snd (g m)
+        _ -> uncurry (+) (g m)
+    ```
+    We want to give `g` the demand `MC1(P(MP(L),1P(L)))`, so we see that in each
+    call site of `g`, we are strict in the second component of the returned
+    pair. That in turn means that Nested CPR can unbox the result of the
+    division even though it might throw.
 
 Note [Computing one-shot info]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/libraries/base/Data/OldList.hs b/libraries/base/Data/OldList.hs
index 5ffdd84ad3..4859cac7ac 100644
--- a/libraries/base/Data/OldList.hs
+++ b/libraries/base/Data/OldList.hs
@@ -269,16 +269,16 @@ stripPrefix _ _ = Nothing
 --
 -- >>> elemIndex 4 [0..]
 -- Just 4
-elemIndex       :: Eq a => a -> [a] -> Maybe Int
-elemIndex x     = findIndex (x==)
+elemIndex      :: Eq a => a -> [a] -> Maybe Int
+elemIndex x xs = findIndex (x==) xs -- arity 2 so that we don't get a PAP; #21345
 
 -- | The 'elemIndices' function extends 'elemIndex', by returning the
 -- indices of all elements equal to the query element, in ascending order.
 --
 -- >>> elemIndices 'o' "Hello World"
 -- [4,7]
-elemIndices     :: Eq a => a -> [a] -> [Int]
-elemIndices x   = findIndices (x==)
+elemIndices      :: Eq a => a -> [a] -> [Int]
+elemIndices x xs = findIndices (x==) xs -- arity 2 so that we don't get a PAP; #21345
 
 -- | The 'find' function takes a predicate and a list and returns the
 -- first element in the list matching the predicate, or 'Nothing' if
diff --git a/testsuite/tests/arityanal/should_compile/Arity01.stderr b/testsuite/tests/arityanal/should_compile/Arity01.stderr
index c5c5a24a9a..40d65fe4ea 100644
--- a/testsuite/tests/arityanal/should_compile/Arity01.stderr
+++ b/testsuite/tests/arityanal/should_compile/Arity01.stderr
@@ -1,11 +1,11 @@
 
 ==================== Tidy Core ====================
-Result size of Tidy Core = {terms: 61, types: 43, coercions: 0, joins: 0/0}
+Result size of Tidy Core = {terms: 65, types: 41, coercions: 0, joins: 0/0}
 
--- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
+-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
 F1.f2 :: Integer
-[GblId, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 100 0}]
-F1.f2 = 1
+[GblId, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 10}]
+F1.f2 = GHC.Num.Integer.IS 1#
 
 Rec {
 -- RHS size: {terms: 18, types: 4, coercions: 0, joins: 0/0}
@@ -13,16 +13,16 @@ F1.f1_h1 [Occ=LoopBreaker] :: Integer -> Integer -> Integer -> Integer
 [GblId, Arity=3, Str=<SL><SL><SL>, Unf=OtherCon []]
 F1.f1_h1
   = \ (n :: Integer) (x :: Integer) (eta :: Integer) ->
-      case GHC.Num.Integer.integerLt# x n of {
-        __DEFAULT -> eta;
-        1# -> F1.f1_h1 n (GHC.Num.Integer.integerAdd x F1.f2) (GHC.Num.Integer.integerAdd x eta)
+      case GHC.Num.Integer.integerLt x n of {
+        False -> eta;
+        True -> F1.f1_h1 n (GHC.Num.Integer.integerAdd x F1.f2) (GHC.Num.Integer.integerAdd x eta)
       }
 end Rec }
 
--- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
+-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
 F1.f3 :: Integer
-[GblId, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 100 0}]
-F1.f3 = 5
+[GblId, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 10}]
+F1.f3 = GHC.Num.Integer.IS 5#
 
 -- RHS size: {terms: 4, types: 0, coercions: 0, joins: 0/0}
 f1 :: Integer
@@ -34,20 +34,20 @@ g :: Integer -> Integer -> Integer -> Integer -> Integer -> Integer
 [GblId, Arity=5, Str=<1L><SL><SL><SL><SL>, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [0 0 0 0 0] 120 0}]
 g = \ (x1 :: Integer) (x2 :: Integer) (x3 :: Integer) (x4 :: Integer) (x5 :: Integer) -> GHC.Num.Integer.integerAdd (GHC.Num.Integer.integerAdd (GHC.Num.Integer.integerAdd (GHC.Num.Integer.integerAdd x1 x2) x3) x4) x5
 
--- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
+-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
 F1.s1 :: Integer
-[GblId, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 100 0}]
-F1.s1 = 3
+[GblId, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 10}]
+F1.s1 = GHC.Num.Integer.IS 3#
 
--- RHS size: {terms: 8, types: 8, coercions: 0, joins: 0/0}
+-- RHS size: {terms: 8, types: 7, coercions: 0, joins: 0/0}
 s :: forall {t1} {t2}. Num t1 => (t1 -> t2) -> t2
-[GblId, Arity=2, Str=<MP(A,A,A,A,A,A,MCM(L))><1C1(L)>, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [30 60] 50 0}]
+[GblId, Arity=2, Str=<MP(A,A,A,A,A,A,1C1(L))><1C1(L)>, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [30 60] 50 0}]
 s = \ (@t) (@t1) ($dNum :: Num t) (f :: t -> t1) -> f (fromInteger @t $dNum F1.s1)
 
--- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
+-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
 F1.h1 :: Integer
-[GblId, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 100 0}]
-F1.h1 = 24
+[GblId, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 10}]
+F1.h1 = GHC.Num.Integer.IS 24#
 
 -- RHS size: {terms: 4, types: 1, coercions: 0, joins: 0/0}
 h :: Integer -> Integer
diff --git a/testsuite/tests/arityanal/should_compile/Arity05.stderr b/testsuite/tests/arityanal/should_compile/Arity05.stderr
index 7045daa0f1..91c909ecc6 100644
--- a/testsuite/tests/arityanal/should_compile/Arity05.stderr
+++ b/testsuite/tests/arityanal/should_compile/Arity05.stderr
@@ -1,44 +1,44 @@
 
 ==================== Tidy Core ====================
-Result size of Tidy Core = {terms: 54, types: 87, coercions: 0, joins: 0/0}
+Result size of Tidy Core = {terms: 56, types: 87, coercions: 0, joins: 0/0}
 
--- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
+-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
 F5.f5g1 :: Integer
-[GblId, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 100 0}]
-F5.f5g1 = 1
+[GblId, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 10}]
+F5.f5g1 = GHC.Num.Integer.IS 1#
 
 -- RHS size: {terms: 12, types: 9, coercions: 0, joins: 0/0}
 f5g :: forall {a} {t}. Num a => (t -> a) -> t -> a
 [GblId,
  Arity=3,
- Str=<SP(1C1(C1(L)),A,A,A,A,A,MCM(L))><MCM(L)><L>,
+ Str=<SP(1C1(C1(L)),A,A,A,A,A,MC1(L))><MC1(L)><L>,
  Unf=Unf{Src=InlineStable, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=ALWAYS_IF(arity=3,unsat_ok=True,boring_ok=False)
          Tmpl= \ (@a) (@t) ($dNum :: Num a) (h [Occ=Once1!] :: t -> a) (z [Occ=Once1] :: t) -> + @a $dNum (h z) (fromInteger @a $dNum F5.f5g1)}]
 f5g = \ (@a) (@t) ($dNum :: Num a) (h :: t -> a) (z :: t) -> + @a $dNum (h z) (fromInteger @a $dNum F5.f5g1)
 
 -- RHS size: {terms: 15, types: 12, coercions: 0, joins: 0/0}
 F5.$wf5h [InlPrag=[2]] :: forall {a} {t}. (a -> a -> a) -> (Integer -> a) -> (t -> a) -> t -> (t -> a) -> a
-[GblId, Arity=5, Str=<SCS(C1(L))><MCM(L)><MCM(L)><L><MCM(L)>, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [60 60 60 0 60] 120 0}]
-F5.$wf5h = \ (@a) (@t) (ww :: a -> a -> a) (ww1 :: Integer -> a) (w :: t -> a) (w1 :: t) (w2 :: t -> a) -> ww (w w1) (ww (w2 w1) (ww1 F5.f5g1))
+[GblId, Arity=5, Str=<SCS(C1(L))><MC1(L)><MC1(L)><L><MC1(L)>, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [60 60 60 0 60] 120 0}]
+F5.$wf5h = \ (@a) (@t) (ww :: a -> a -> a) (ww1 :: Integer -> a) (f :: t -> a) (x :: t) (g :: t -> a) -> ww (f x) (ww (g x) (ww1 F5.f5g1))
 
 -- RHS size: {terms: 15, types: 30, coercions: 0, joins: 0/0}
 f5h [InlPrag=[2]] :: forall {a} {t}. Num a => (t -> a) -> t -> (t -> a) -> a
 [GblId,
  Arity=4,
- Str=<1P(SCS(C1(L)),A,A,A,A,A,MCM(L))><MCM(L)><L><MCM(L)>,
+ Str=<1P(SCS(C1(L)),A,A,A,A,A,MC1(L))><MC1(L)><L><MC1(L)>,
  Unf=Unf{Src=InlineStable, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=ALWAYS_IF(arity=4,unsat_ok=True,boring_ok=False)
-         Tmpl= \ (@a) (@t) (w [Occ=Once1!] :: Num a) (w1 [Occ=Once1] :: t -> a) (w2 [Occ=Once1] :: t) (w3 [Occ=Once1] :: t -> a) -> case w of { GHC.Num.C:Num ww [Occ=Once1] _ [Occ=Dead] _ [Occ=Dead] _ [Occ=Dead] _ [Occ=Dead] _ [Occ=Dead] ww6 [Occ=Once1] -> F5.$wf5h @a @t ww ww6 w1 w2 w3 }}]
-f5h = \ (@a) (@t) (w :: Num a) (w1 :: t -> a) (w2 :: t) (w3 :: t -> a) -> case w of { GHC.Num.C:Num ww ww1 ww2 ww3 ww4 ww5 ww6 -> F5.$wf5h @a @t ww ww6 w1 w2 w3 }
+         Tmpl= \ (@a) (@t) ($dNum [Occ=Once1!] :: Num a) (f [Occ=Once1] :: t -> a) (x [Occ=Once1] :: t) (g [Occ=Once1] :: t -> a) -> case $dNum of { GHC.Num.C:Num ww [Occ=Once1] _ [Occ=Dead] _ [Occ=Dead] _ [Occ=Dead] _ [Occ=Dead] _ [Occ=Dead] ww6 [Occ=Once1] -> F5.$wf5h @a @t ww ww6 f x g }}]
+f5h = \ (@a) (@t) ($dNum :: Num a) (f :: t -> a) (x :: t) (g :: t -> a) -> case $dNum of { GHC.Num.C:Num ww ww1 ww2 ww3 ww4 ww5 ww6 -> F5.$wf5h @a @t ww ww6 f x g }
 
 -- RHS size: {terms: 4, types: 1, coercions: 0, joins: 0/0}
 f5y :: Integer -> Integer
 [GblId, Arity=1, Str=<1L>, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [0] 30 0}]
 f5y = \ (y :: Integer) -> GHC.Num.Integer.integerAdd y F5.f5g1
 
--- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
+-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
 f5 :: Integer
-[GblId, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 100 0}]
-f5 = 3
+[GblId, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 10}]
+f5 = GHC.Num.Integer.IS 3#
 
 
 
diff --git a/testsuite/tests/arityanal/should_compile/Arity08.stderr b/testsuite/tests/arityanal/should_compile/Arity08.stderr
index 406b5c6bdf..9885d5f158 100644
--- a/testsuite/tests/arityanal/should_compile/Arity08.stderr
+++ b/testsuite/tests/arityanal/should_compile/Arity08.stderr
@@ -1,10 +1,10 @@
 
 ==================== Tidy Core ====================
-Result size of Tidy Core = {terms: 23, types: 20, coercions: 0, joins: 0/0}
+Result size of Tidy Core = {terms: 24, types: 18, coercions: 0, joins: 0/0}
 
--- RHS size: {terms: 20, types: 11, coercions: 0, joins: 0/0}
+-- RHS size: {terms: 20, types: 10, coercions: 0, joins: 0/0}
 f8f :: forall {p}. Num p => Bool -> p -> p -> p
-[GblId, Arity=4, Str=<LP(LCL(C1(L)),A,MCM(C1(L)),A,A,A,A)><1L><L><L>, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [90 30 0 0] 140 0}]
+[GblId, Arity=4, Str=<LP(SCS(C1(L)),A,MC1(C1(L)),A,A,A,A)><1L><L><L>, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [90 30 0 0] 140 0}]
 f8f
   = \ (@p) ($dNum :: Num p) (b :: Bool) (x :: p) (y :: p) ->
       case b of {
@@ -12,10 +12,10 @@ f8f
         True -> y
       }
 
--- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
+-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
 f8 :: Integer
-[GblId, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 100 0}]
-f8 = 2
+[GblId, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 10}]
+f8 = GHC.Num.Integer.IS 2#
 
 
 
diff --git a/testsuite/tests/arityanal/should_compile/Arity11.stderr b/testsuite/tests/arityanal/should_compile/Arity11.stderr
index 48b37a13db..7c7451a6d7 100644
--- a/testsuite/tests/arityanal/should_compile/Arity11.stderr
+++ b/testsuite/tests/arityanal/should_compile/Arity11.stderr
@@ -1,59 +1,77 @@
 
 ==================== Tidy Core ====================
-Result size of Tidy Core = {terms: 129, types: 98, coercions: 0, joins: 0/5}
+Result size of Tidy Core = {terms: 149, types: 104, coercions: 0, joins: 2/7}
 
--- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
-F11.fib1 :: Integer
-[GblId, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 100 0}]
-F11.fib1 = 0
-
--- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
+-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
 F11.fib3 :: Integer
-[GblId, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 100 0}]
-F11.fib3 = 1
+[GblId, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 10}]
+F11.fib3 = GHC.Num.Integer.IS 1#
 
--- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
+-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
 F11.fib2 :: Integer
-[GblId, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 100 0}]
-F11.fib2 = 2
+[GblId, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 10}]
+F11.fib2 = GHC.Num.Integer.IS 2#
 
 Rec {
--- RHS size: {terms: 24, types: 3, coercions: 0, joins: 0/0}
+-- RHS size: {terms: 38, types: 13, coercions: 0, joins: 2/2}
 F11.f11_fib [Occ=LoopBreaker] :: Integer -> Integer
 [GblId, Arity=1, Str=<SL>, Unf=OtherCon []]
 F11.f11_fib
   = \ (ds :: Integer) ->
-      case GHC.Num.Integer.integerEq# ds F11.fib1 of {
-        __DEFAULT ->
-          case GHC.Num.Integer.integerEq# ds F11.fib3 of {
-            __DEFAULT -> GHC.Num.Integer.integerAdd (F11.f11_fib (GHC.Num.Integer.integerSub ds F11.fib3)) (F11.f11_fib (GHC.Num.Integer.integerSub ds F11.fib2));
-            1# -> F11.fib3
+      join {
+        $j [Dmd=ML] :: Integer
+        [LclId[JoinId(0)(Nothing)]]
+        $j
+          = join {
+              $j1 [Dmd=ML] :: Integer
+              [LclId[JoinId(0)(Nothing)]]
+              $j1 = GHC.Num.Integer.integerAdd (F11.f11_fib (GHC.Num.Integer.integerSub ds F11.fib3)) (F11.f11_fib (GHC.Num.Integer.integerSub ds F11.fib2)) } in
+            case ds of {
+              GHC.Num.Integer.IS x1 ->
+                case x1 of {
+                  __DEFAULT -> jump $j1;
+                  1# -> F11.fib3
+                };
+              GHC.Num.Integer.IP x1 -> jump $j1;
+              GHC.Num.Integer.IN x1 -> jump $j1
+            } } in
+      case ds of {
+        GHC.Num.Integer.IS x1 ->
+          case x1 of {
+            __DEFAULT -> jump $j;
+            0# -> F11.fib3
           };
-        1# -> F11.fib3
+        GHC.Num.Integer.IP x1 -> jump $j;
+        GHC.Num.Integer.IN x1 -> jump $j
       }
 end Rec }
 
--- RHS size: {terms: 52, types: 27, coercions: 0, joins: 0/5}
+-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
+F11.fib1 :: Integer
+[GblId, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 10}]
+F11.fib1 = GHC.Num.Integer.IS 0#
+
+-- RHS size: {terms: 52, types: 26, coercions: 0, joins: 0/5}
 F11.$wfib [InlPrag=[2]] :: forall {t} {a}. (t -> t -> Bool) -> (Num t, Num a) => t -> a
-[GblId, Arity=4, Str=<SCS(C1(L))><LP(A,LCL(C1(L)),A,A,A,A,L)><LP(LCL(C1(L)),A,A,A,A,A,MCM(L))><L>, 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=<SCS(C1(L))><LP(A,LCS(C1(L)),A,A,A,A,LCS(L))><LP(LCS(C1(L)),A,A,A,A,A,MC1(L))><L>, 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
-  = \ (@t) (@a) (ww :: t -> t -> Bool) (w :: Num t) (w1 :: Num a) (w2 :: t) ->
+  = \ (@t) (@a) (ww :: t -> t -> Bool) ($dNum :: Num t) ($dNum1 :: Num a) (eta :: t) ->
       let {
         lvl :: t
         [LclId]
-        lvl = fromInteger @t w F11.fib3 } in
+        lvl = fromInteger @t $dNum F11.fib3 } in
       let {
         lvl1 :: t
         [LclId]
-        lvl1 = fromInteger @t w F11.fib2 } in
+        lvl1 = fromInteger @t $dNum F11.fib2 } in
       let {
         lvl2 :: a
         [LclId]
-        lvl2 = fromInteger @a w1 F11.fib3 } in
+        lvl2 = fromInteger @a $dNum1 F11.fib3 } in
       let {
         lvl3 :: t
         [LclId]
-        lvl3 = fromInteger @t w F11.fib1 } in
+        lvl3 = fromInteger @t $dNum F11.fib1 } in
       letrec {
         fib4 [Occ=LoopBreaker, Dmd=SCS(L)] :: t -> a
         [LclId, Arity=1, Str=<L>, Unf=OtherCon []]
@@ -62,26 +80,26 @@ F11.$wfib
               case ww ds lvl3 of {
                 False ->
                   case ww ds lvl of {
-                    False -> + @a w1 (fib4 (- @t w ds lvl)) (fib4 (- @t w ds lvl1));
+                    False -> + @a $dNum1 (fib4 (- @t $dNum ds lvl)) (fib4 (- @t $dNum ds lvl1));
                     True -> lvl2
                   };
                 True -> lvl2
               }; } in
-      fib4 w2
+      fib4 eta
 
--- RHS size: {terms: 14, types: 20, coercions: 0, joins: 0/0}
+-- RHS size: {terms: 14, types: 19, coercions: 0, joins: 0/0}
 fib [InlPrag=[2]] :: forall {t} {a}. (Eq t, Num t, Num a) => t -> a
 [GblId,
  Arity=4,
- Str=<1!P(SCS(C1(L)),A)><LP(A,LCL(C1(L)),A,A,A,A,L)><LP(LCL(C1(L)),A,A,A,A,A,L)><L>,
+ Str=<1P(SCS(C1(L)),A)><LP(A,LCS(C1(L)),A,A,A,A,LCS(L))><LP(LCS(C1(L)),A,A,A,A,A,LCS(L))><L>,
  Unf=Unf{Src=InlineStable, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=ALWAYS_IF(arity=4,unsat_ok=True,boring_ok=False)
-         Tmpl= \ (@t) (@a) (w [Occ=Once1!] :: Eq t) (w1 [Occ=Once1] :: Num t) (w2 [Occ=Once1] :: Num a) (w3 [Occ=Once1] :: t) -> case w of { GHC.Classes.C:Eq ww [Occ=Once1] _ [Occ=Dead] -> F11.$wfib @t @a ww w1 w2 w3 }}]
-fib = \ (@t) (@a) (w :: Eq t) (w1 :: Num t) (w2 :: Num a) (w3 :: t) -> case w of { GHC.Classes.C:Eq ww ww1 -> F11.$wfib @t @a ww w1 w2 w3 }
+         Tmpl= \ (@t) (@a) ($dEq [Occ=Once1!] :: Eq t) ($dNum [Occ=Once1] :: Num t) ($dNum1 [Occ=Once1] :: Num a) (eta [Occ=Once1] :: t) -> case $dEq of { GHC.Classes.C:Eq ww [Occ=Once1] _ [Occ=Dead] -> F11.$wfib @t @a ww $dNum $dNum1 eta }}]
+fib = \ (@t) (@a) ($dEq :: Eq t) ($dNum :: Num t) ($dNum1 :: Num a) (eta :: t) -> case $dEq of { GHC.Classes.C:Eq ww ww1 -> F11.$wfib @t @a ww $dNum $dNum1 eta }
 
--- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
+-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
 F11.f3 :: Integer
-[GblId, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 100 0}]
-F11.f3 = 1000
+[GblId, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 10}]
+F11.f3 = GHC.Num.Integer.IS 1000#
 
 -- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
 F11.f11_x :: Integer
@@ -98,20 +116,20 @@ f11f :: forall {p}. p -> Integer -> Integer
 [GblId, Arity=2, Str=<A><SL>, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=ALWAYS_IF(arity=1,unsat_ok=True,boring_ok=True)}]
 f11f = \ (@p) _ [Occ=Dead] -> F11.f11f1
 
--- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
+-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
 F11.f5 :: Integer
-[GblId, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 100 0}]
-F11.f5 = 6
+[GblId, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 10}]
+F11.f5 = GHC.Num.Integer.IS 6#
 
 -- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
 F11.f4 :: Integer
 [GblId, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=False, ConLike=False, WorkFree=False, Expandable=False, Guidance=IF_ARGS [] 30 0}]
 F11.f4 = GHC.Num.Integer.integerAdd F11.f11_x F11.f5
 
--- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
+-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
 F11.f2 :: Integer
-[GblId, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 100 0}]
-F11.f2 = 8
+[GblId, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 10}]
+F11.f2 = GHC.Num.Integer.IS 8#
 
 -- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
 F11.f1 :: Integer
diff --git a/testsuite/tests/arityanal/should_compile/Arity14.stderr b/testsuite/tests/arityanal/should_compile/Arity14.stderr
index efd90363c6..fec1b63641 100644
--- a/testsuite/tests/arityanal/should_compile/Arity14.stderr
+++ b/testsuite/tests/arityanal/should_compile/Arity14.stderr
@@ -1,26 +1,26 @@
 
 ==================== Tidy Core ====================
-Result size of Tidy Core = {terms: 56, types: 87, coercions: 0, joins: 0/3}
+Result size of Tidy Core = {terms: 57, types: 81, coercions: 0, joins: 0/3}
 
--- RHS size: {terms: 3, types: 3, coercions: 0, joins: 0/0}
+-- RHS size: {terms: 3, types: 2, coercions: 0, joins: 0/0}
 F14.f1 :: forall {t}. t -> t
 [GblId, Arity=1, Str=<1L>, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=ALWAYS_IF(arity=1,unsat_ok=True,boring_ok=True)}]
 F14.f1 = \ (@t) (y :: t) -> y
 
--- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
+-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
 F14.f2 :: Integer
-[GblId, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 100 0}]
-F14.f2 = 1
+[GblId, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 10}]
+F14.f2 = GHC.Num.Integer.IS 1#
 
--- RHS size: {terms: 35, types: 24, coercions: 0, joins: 0/3}
+-- RHS size: {terms: 35, types: 23, coercions: 0, joins: 0/3}
 F14.$wf14 [InlPrag=[2]] :: forall {t}. (t -> t -> Bool) -> Num t => t -> t -> t -> t
-[GblId, Arity=4, Str=<SCS(C1(L))><LP(LCL(C1(L)),A,A,A,A,A,MCM(L))><L><L>, 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=<SCS(C1(L))><LP(LCS(C1(L)),A,A,A,A,A,MC1(L))><L><L>, 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) ->
+  = \ (@t) (ww :: t -> t -> Bool) ($dNum :: Num t) (eta :: t) (eta1 :: t) ->
       let {
         lvl :: t
         [LclId]
-        lvl = fromInteger @t w F14.f2 } in
+        lvl = fromInteger @t $dNum F14.f2 } in
       letrec {
         f3 [Occ=LoopBreaker, Dmd=SCS(C1(L))] :: t -> t -> t -> t
         [LclId, Arity=2, Str=<L><L>, Unf=OtherCon []]
@@ -30,21 +30,21 @@ F14.$wf14
                 False -> F14.f1 @t;
                 True ->
                   let {
-                    v :: t -> t
+                    v [Dmd=LCS(L)] :: t -> t
                     [LclId]
-                    v = f3 n (+ @t w x lvl) } in
-                  \ (y :: t) -> v (+ @t w x y)
+                    v = f3 n (+ @t $dNum x lvl) } in
+                  \ (y :: t) -> v (+ @t $dNum x y)
               }; } in
-      f3 w1 w2
+      f3 eta eta1
 
--- RHS size: {terms: 13, types: 34, coercions: 0, joins: 0/0}
+-- RHS size: {terms: 13, types: 33, coercions: 0, joins: 0/0}
 f14 [InlPrag=[2]] :: forall {t}. (Ord t, Num t) => t -> t -> t -> t
 [GblId,
  Arity=4,
- Str=<1!P(A,A,SCS(C1(L)),A,A,A,A,A)><LP(LCL(C1(L)),A,A,A,A,A,L)><L><L>,
+ Str=<1P(A,A,SCS(C1(L)),A,A,A,A,A)><LP(LCS(C1(L)),A,A,A,A,A,LCS(L))><L><L>,
  Unf=Unf{Src=InlineStable, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=ALWAYS_IF(arity=4,unsat_ok=True,boring_ok=False)
-         Tmpl= \ (@t) (w [Occ=Once1!] :: Ord t) (w1 [Occ=Once1] :: Num t) (w2 [Occ=Once1] :: t) (w3 [Occ=Once1] :: t) -> case w of { GHC.Classes.C:Ord _ [Occ=Dead] _ [Occ=Dead] ww2 [Occ=Once1] _ [Occ=Dead] _ [Occ=Dead] _ [Occ=Dead] _ [Occ=Dead] _ [Occ=Dead] -> F14.$wf14 @t ww2 w1 w2 w3 }}]
-f14 = \ (@t) (w :: Ord t) (w1 :: Num t) (w2 :: t) (w3 :: t) -> case w of { GHC.Classes.C:Ord ww ww1 ww2 ww3 ww4 ww5 ww6 ww7 -> F14.$wf14 @t ww2 w1 w2 w3 }
+         Tmpl= \ (@t) ($dOrd [Occ=Once1!] :: Ord t) ($dNum [Occ=Once1] :: Num t) (eta [Occ=Once1] :: t) (eta1 [Occ=Once1] :: t) -> case $dOrd of { GHC.Classes.C:Ord _ [Occ=Dead] _ [Occ=Dead] ww2 [Occ=Once1] _ [Occ=Dead] _ [Occ=Dead] _ [Occ=Dead] _ [Occ=Dead] _ [Occ=Dead] -> F14.$wf14 @t ww2 $dNum eta eta1 }}]
+f14 = \ (@t) ($dOrd :: Ord t) ($dNum :: Num t) (eta :: t) (eta1 :: t) -> case $dOrd of { GHC.Classes.C:Ord ww ww1 ww2 ww3 ww4 ww5 ww6 ww7 -> F14.$wf14 @t ww2 $dNum eta eta1 }
 
 
 
diff --git a/testsuite/tests/arityanal/should_compile/Arity16.stderr b/testsuite/tests/arityanal/should_compile/Arity16.stderr
index 8f750b6d04..eb9f0a5ffe 100644
--- a/testsuite/tests/arityanal/should_compile/Arity16.stderr
+++ b/testsuite/tests/arityanal/should_compile/Arity16.stderr
@@ -1,11 +1,11 @@
 
 ==================== Tidy Core ====================
-Result size of Tidy Core = {terms: 52, types: 75, coercions: 0, joins: 0/0}
+Result size of Tidy Core = {terms: 53, types: 71, coercions: 0, joins: 0/0}
 
 Rec {
 -- RHS size: {terms: 15, types: 15, coercions: 0, joins: 0/0}
 map2 [Occ=LoopBreaker] :: forall {t} {a}. (t -> a) -> [t] -> [a]
-[GblId, Arity=2, Str=<L><1L>, Unf=OtherCon []]
+[GblId, Arity=2, Str=<LCS(L)><1L>, Unf=OtherCon []]
 map2
   = \ (@t) (@a) (f :: t -> a) (ds :: [t]) ->
       case ds of {
@@ -19,26 +19,26 @@ lvl :: GHC.Prim.Addr#
 [GblId, Unf=OtherCon []]
 lvl = "Arity16.hs:(6,1)-(7,47)|function zipWith2"#
 
--- RHS size: {terms: 3, types: 4, coercions: 0, joins: 0/0}
-lvl1 :: forall {a}. [a]
+-- RHS size: {terms: 2, types: 2, coercions: 0, joins: 0/0}
+lvl1 :: ()
 [GblId, Str=b, Cpr=b]
-lvl1 = \ (@a) -> Control.Exception.Base.patError @'GHC.Types.LiftedRep @[a] lvl
+lvl1 = Control.Exception.Base.patError @GHC.Types.LiftedRep @() lvl
 
 Rec {
--- RHS size: {terms: 29, types: 32, coercions: 0, joins: 0/0}
+-- RHS size: {terms: 31, types: 32, coercions: 0, joins: 0/0}
 zipWith2 [Occ=LoopBreaker] :: forall {t1} {t2} {a}. (t1 -> t2 -> a) -> [t1] -> [t2] -> [a]
-[GblId, Arity=3, Str=<LCL(C1(L))><1L><1L>, Unf=OtherCon []]
+[GblId, Arity=3, Str=<LCS(C1(L))><1L><1L>, Unf=OtherCon []]
 zipWith2
   = \ (@t) (@t1) (@a) (f :: t -> t1 -> a) (ds :: [t]) (ds1 :: [t1]) ->
       case ds of {
         [] ->
           case ds1 of {
             [] -> GHC.Types.[] @a;
-            : ipv ipv1 -> lvl1 @a
+            : ipv ipv1 -> case lvl1 of wild2 { }
           };
         : a1 x ->
           case ds1 of {
-            [] -> lvl1 @a;
+            [] -> case lvl1 of wild2 { };
             : b y -> GHC.Types.: @a (f a1 b) (zipWith2 @t @t1 @a f x y)
           }
       }
diff --git a/testsuite/tests/simplCore/should_compile/OpaqueNoSpecialise.stderr b/testsuite/tests/simplCore/should_compile/OpaqueNoSpecialise.stderr
index b3d76cde24..a534137d14 100644
--- a/testsuite/tests/simplCore/should_compile/OpaqueNoSpecialise.stderr
+++ b/testsuite/tests/simplCore/should_compile/OpaqueNoSpecialise.stderr
@@ -12,7 +12,7 @@ lvl = GHC.Num.Integer.IS 1#
 f [InlPrag=OPAQUE] :: forall {t}. Num t => t -> [t]
 [GblId,
  Arity=2,
- Str=<LP(A,LCL(C1(L)),A,A,A,A,MCM(L))><L>,
+ Str=<LP(A,LCS(C1(L)),A,A,A,A,MC1(L))><L>,
  Unf=OtherCon []]
 f = \ (@t) ($dNum :: Num t) (eta :: t) ->
       let {
@@ -72,3 +72,6 @@ OpaqueNoSpecialise.$trModule :: GHC.Types.Module
 OpaqueNoSpecialise.$trModule
   = GHC.Types.Module
       OpaqueNoSpecialise.$trModule3 OpaqueNoSpecialise.$trModule1
+
+
+
diff --git a/testsuite/tests/simplCore/should_compile/T18013.stderr b/testsuite/tests/simplCore/should_compile/T18013.stderr
index fe48290c49..b94cec212b 100644
--- a/testsuite/tests/simplCore/should_compile/T18013.stderr
+++ b/testsuite/tests/simplCore/should_compile/T18013.stderr
@@ -138,7 +138,7 @@ mapMaybeRule [InlPrag=[2]]
   :: forall a b. Rule IO a b -> Rule IO (Maybe a) (Maybe b)
 [GblId,
  Arity=1,
- Str=<1!P(L,LCL(C1(C1(P(L,1L)))))>,
+ Str=<1!P(L,LCS(C1(C1(P(L,1L)))))>,
  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)
diff --git a/testsuite/tests/simplCore/should_compile/T21261.hs b/testsuite/tests/simplCore/should_compile/T21261.hs
index ae39c4b7d4..95fe678682 100644
--- a/testsuite/tests/simplCore/should_compile/T21261.hs
+++ b/testsuite/tests/simplCore/should_compile/T21261.hs
@@ -34,14 +34,18 @@ f5 c = Just (c 1 2 + c 3 4)
 yes2_lazy :: (Int -> Int -> Int) -> Maybe Int
 yes2_lazy c = f5 (\x y -> c x y)
 
-f6 :: (Int -> Int -> Int) -> Maybe Int
-f6 c = Just (c 1 `seq` c 3 4)
+-- These last two here are disallowed in T21261_pedantic.hs, which activates
+-- -fpedantic-bottoms. It would be unsound to eta reduce these bindings with
+-- -fpedantic-bottoms, but without it's fine to eta reduce:
+
+f6 :: (Int -> Int -> Int) -> Int
+f6 c = c 1 `seq` c 2 3
 {-# NOINLINE f6 #-}
-no2_lazy :: (Int -> Int -> Int) -> Maybe Int
-no2_lazy c = f6 (\x y -> c x y)
+yes_non_pedantic :: (Int -> Int -> Int) -> Int
+yes_non_pedantic c = f6 (\x y -> c x y)
 
-f7 :: (Int -> Int -> Int) -> Int
-f7 c = c 1 `seq` c 2 3
+f7 :: (Int -> Int -> Int) -> Maybe Int
+f7 c = Just (c 1 `seq` c 3 4)
 {-# NOINLINE f7 #-}
-not_quite_eta :: (Int -> Int -> Int) -> Int
-not_quite_eta c = f7 (\x y -> c x y)
+yes_non_pedantic_lazy :: (Int -> Int -> Int) -> Maybe Int
+yes_non_pedantic_lazy c = f7 (\x y -> c x y)
diff --git a/testsuite/tests/simplCore/should_compile/T21261.stderr b/testsuite/tests/simplCore/should_compile/T21261.stderr
index 779f769e43..691045b23a 100644
--- a/testsuite/tests/simplCore/should_compile/T21261.stderr
+++ b/testsuite/tests/simplCore/should_compile/T21261.stderr
@@ -1,7 +1,7 @@
 
 ==================== Tidy Core ====================
 Result size of Tidy Core
-  = {terms: 192, types: 201, coercions: 0, joins: 0/0}
+  = {terms: 166, types: 176, coercions: 0, joins: 0/0}
 
 lvl = I# 3#
 
@@ -27,16 +27,15 @@ no3
   = \ c ->
       case $wf4 (\ x y z -> c x y z) of ww { __DEFAULT -> I# ww }
 
-$wf6 = \ c -> (# case c lvl2 of { __DEFAULT -> c lvl lvl1 } #)
+f6 = \ c -> case c lvl2 of { __DEFAULT -> c lvl3 lvl }
 
-f6 = \ c -> case $wf6 c of { (# ww #) -> Just ww }
+yes_non_pedantic = f6
 
-no2_lazy
-  = \ c -> case $wf6 (\ x y -> c x y) of { (# ww #) -> Just ww }
+$wf7 = \ c -> (# case c lvl2 of { __DEFAULT -> c lvl lvl1 } #)
 
-f7 = \ c -> case c lvl2 of { __DEFAULT -> c lvl3 lvl }
+f7 = \ c -> case $wf7 c of { (# ww #) -> Just ww }
 
-not_quite_eta = \ c -> f7 (\ x y -> c x y)
+yes_non_pedantic_lazy = f7
 
 $wf5
   = \ c ->
@@ -46,8 +45,7 @@ $wf5
 
 f5 = \ c -> case $wf5 c of { (# ww #) -> Just ww }
 
-yes2_lazy
-  = \ c -> case $wf5 (\ x y -> c x y) of { (# ww #) -> Just ww }
+yes2_lazy = f5
 
 $wf3
   = \ c ->
diff --git a/testsuite/tests/simplCore/should_compile/T21261_pedantic.hs b/testsuite/tests/simplCore/should_compile/T21261_pedantic.hs
new file mode 100644
index 0000000000..b63d90558b
--- /dev/null
+++ b/testsuite/tests/simplCore/should_compile/T21261_pedantic.hs
@@ -0,0 +1,18 @@
+{-# OPTIONS_GHC -fpedantic-bottoms #-} -- This flag must inhibit eta reduction based on demands
+
+module T21261_pedantic where
+
+-- README: See T21261. These examples absolutely should not eta reduce with
+-- -fpedantic-bottoms.
+
+f1 :: (Int -> Int -> Int) -> Int
+f1 c = c 1 `seq` c 2 3
+{-# NOINLINE f1 #-}
+no2 :: (Int -> Int -> Int) -> Int
+no2 c = f1 (\x y -> c x y)
+
+f2 :: (Int -> Int -> Int) -> Maybe Int
+f2 c = Just (c 1 `seq` c 3 4)
+{-# NOINLINE f2 #-}
+no2_lazy :: (Int -> Int -> Int) -> Maybe Int
+no2_lazy c = f2 (\x y -> c x y)
diff --git a/testsuite/tests/simplCore/should_compile/T21261_pedantic.stderr b/testsuite/tests/simplCore/should_compile/T21261_pedantic.stderr
new file mode 100644
index 0000000000..fdd7de05df
--- /dev/null
+++ b/testsuite/tests/simplCore/should_compile/T21261_pedantic.stderr
@@ -0,0 +1,26 @@
+
+==================== Tidy Core ====================
+Result size of Tidy Core
+  = {terms: 59, types: 63, coercions: 0, joins: 0/0}
+
+lvl = I# 2#
+
+lvl1 = I# 3#
+
+lvl2 = I# 1#
+
+f1 = \ c -> case c lvl2 of { __DEFAULT -> c lvl lvl1 }
+
+no2 = \ c -> f1 (\ x y -> c x y)
+
+lvl3 = I# 4#
+
+$wf2 = \ c -> (# case c lvl2 of { __DEFAULT -> c lvl1 lvl3 } #)
+
+f2 = \ c -> case $wf2 c of { (# ww #) -> Just ww }
+
+no2_lazy
+  = \ c -> case $wf2 (\ x y -> c x y) of { (# ww #) -> Just ww }
+
+
+
diff --git a/testsuite/tests/simplCore/should_compile/T21392.hs b/testsuite/tests/simplCore/should_compile/T21392.hs
new file mode 100644
index 0000000000..8b60aba580
--- /dev/null
+++ b/testsuite/tests/simplCore/should_compile/T21392.hs
@@ -0,0 +1,37 @@
+module T21392 (f) where
+
+import Data.List (foldl', insertBy)
+import Data.Ord
+
+newtype Unique = U { unU :: Int }
+class Uniquable u where getKey :: u -> Unique
+instance Uniquable Int where getKey = U
+data UMap a = UMap { unS :: ![(Unique,a)], unI :: !Int }
+
+addOne :: Uniquable u => UMap a -> u -> a -> UMap a
+addOne (UMap set n) x v = UMap (insertBy (comparing (unU . fst)) (getKey x,v) set) (n+1)
+
+newtype USet u = USet (UMap u)
+
+insertOne :: Uniquable u => USet u -> u -> USet u
+insertOne (USet s) x = USet (addOne s x x)
+
+insertMany :: Uniquable u => USet u -> [u] -> USet u
+insertMany s vs = foldl' insertOne s (reverse (reverse vs))
+
+seq' = seq
+{-# NOINLINE seq' #-}
+
+blah s@(USet m) = unS m `seq'` s
+{-# NOINLINE blah #-}
+
+end (USet m) = unS m
+{-# NOINLINE end #-}
+
+f :: USet Int -> [Int] -> [(Unique,Int)]
+f !xs ys
+  | length ys == 13 = end $ blah t
+  | length ys == 23 = reverse $ end $ blah t
+  | otherwise       = []
+  where
+    t = insertMany xs (reverse $ reverse $ reverse $ reverse ys)
diff --git a/testsuite/tests/simplCore/should_compile/T4908.stderr b/testsuite/tests/simplCore/should_compile/T4908.stderr
index 9cfd79d1e0..307c9fb728 100644
--- a/testsuite/tests/simplCore/should_compile/T4908.stderr
+++ b/testsuite/tests/simplCore/should_compile/T4908.stderr
@@ -59,7 +59,7 @@ end Rec }
 f [InlPrag=[2]] :: Int -> (Int, Int) -> Bool
 [GblId,
  Arity=2,
- Str=<1!P(1L)><MP(A,MP(ML))>,
+ Str=<1!P(1L)><MP(A,1P(1L))>,
  Cpr=2,
  Unf=Unf{Src=InlineStable, TopLvl=True, Value=True, ConLike=True,
          WorkFree=True, Expandable=True,
diff --git a/testsuite/tests/simplCore/should_compile/all.T b/testsuite/tests/simplCore/should_compile/all.T
index 3b78531e5e..0c52c80480 100644
--- a/testsuite/tests/simplCore/should_compile/all.T
+++ b/testsuite/tests/simplCore/should_compile/all.T
@@ -394,15 +394,17 @@ test('T21144',  normal, compile, ['-O'])
 # Key here is that the argument to ifoldl' is eta-reduced in Core to
 #   `/\m. f @(S m)`
 # which will erase completely in STG
-test('T20040', [ grep_errmsg(r'ifoldl\''), expect_broken(20040) ], compile, ['-O -ddump-stg-final -dno-typeable-binds -dsuppress-all -dsuppress-uniques'])
+test('T20040', [ grep_errmsg(r'ifoldl\'') ], compile, ['-O -ddump-stg-final -dno-typeable-binds -dsuppress-all -dsuppress-uniques'])
 
 # Key here is that yes* become visibly trivial due to eta-reduction, while no* are not eta-reduced.
-test('T21261', [ grep_errmsg(r'^(yes|no)') ], compile, ['-O -ddump-simpl -dno-typeable-binds -dsuppress-all -dsuppress-uniques'])
+test('T21261',          [ grep_errmsg(r'^(yes|no)') ], compile, ['-O -ddump-simpl -dno-typeable-binds -dsuppress-all -dsuppress-uniques'])
+test('T21261_pedantic', [ grep_errmsg(r'^(yes|no)') ], compile, ['-O -ddump-simpl -dno-typeable-binds -dsuppress-all -dsuppress-uniques'])
 
 # We expect to see a SPEC rule for $cm
 test('T17966',  [ grep_errmsg(r'SPEC') ], compile, ['-O -ddump-spec'])
 # We expect to see a SPEC rule for $cm
 test('T19644',  [ grep_errmsg(r'SPEC') ], compile, ['-O -ddump-spec'])
-
 test('T21391', normal, compile, ['-O -dcore-lint'])
 test('T21391a', normal, compile, ['-O -dcore-lint'])
+# We don't want to see a thunk allocation for the insertBy expression after CorePrep.
+test('T21392', [ grep_errmsg(r'sat.* :: \[\(.*Unique, .*Int\)\]'), expect_broken(21392) ], compile, ['-O -ddump-prep -dno-typeable-binds -dsuppress-uniques'])
diff --git a/testsuite/tests/stranal/should_compile/T18894.stderr b/testsuite/tests/stranal/should_compile/T18894.stderr
index 22888e53a2..6027112cb4 100644
--- a/testsuite/tests/stranal/should_compile/T18894.stderr
+++ b/testsuite/tests/stranal/should_compile/T18894.stderr
@@ -46,7 +46,7 @@ lvl :: Int
 lvl = GHC.Types.I# 0#
 
 -- RHS size: {terms: 42, types: 15, coercions: 0, joins: 0/1}
-g2 [InlPrag=NOINLINE, Dmd=LCL(C1(!P(M!P(L),1!P(L))))]
+g2 [InlPrag=NOINLINE, Dmd=LCS(C1(!P(M!P(L),1!P(L))))]
   :: Int -> Int -> (Int, Int)
 [LclId,
  Arity=2,
@@ -147,7 +147,7 @@ lvl :: (Int, Int)
 lvl = (lvl, lvl)
 
 -- RHS size: {terms: 36, types: 10, coercions: 0, joins: 0/1}
-g1 [InlPrag=NOINLINE, Dmd=LCL(!P(L,L))] :: Int -> (Int, Int)
+g1 [InlPrag=NOINLINE, Dmd=LCS(!P(L,L))] :: Int -> (Int, Int)
 [LclId,
  Arity=1,
  Str=<1!P(1L)>,
@@ -201,7 +201,7 @@ h1 :: Int -> Int
          WorkFree=True, Expandable=True, Guidance=IF_ARGS [20] 111 10}]
 h1
   = \ (ds [Dmd=1!P(SL)] :: Int) ->
-      case ds of wild [Dmd=M!P(ML)] { GHC.Types.I# ds [Dmd=SL] ->
+      case ds of wild [Dmd=M!P(1L)] { GHC.Types.I# ds [Dmd=SL] ->
       case ds of {
         __DEFAULT ->
           case g1 wild of { (x [Dmd=1!P(L)], ds [Dmd=1!P(L)]) ->
@@ -264,7 +264,7 @@ lvl :: Int
 lvl = GHC.Types.I# 0#
 
 -- RHS size: {terms: 39, types: 17, coercions: 0, joins: 0/1}
-$wg2 [InlPrag=NOINLINE, Dmd=LCL(C1(!P(M!P(L),1!P(L))))]
+$wg2 [InlPrag=NOINLINE, Dmd=LCS(C1(!P(M!P(L),1!P(L))))]
   :: Int -> GHC.Prim.Int# -> (# Int, Int #)
 [LclId,
  Arity=2,
@@ -328,7 +328,7 @@ h2
       }
 
 -- RHS size: {terms: 34, types: 14, coercions: 0, joins: 0/1}
-$wg1 [InlPrag=NOINLINE, Dmd=LCL(!P(L,L))]
+$wg1 [InlPrag=NOINLINE, Dmd=LCS(!P(L,L))]
   :: GHC.Prim.Int# -> (# GHC.Prim.Int#, Int #)
 [LclId,
  Arity=1,
@@ -366,7 +366,7 @@ lvl :: (Int, Int)
 lvl = case $wg1 2# of { (# ww, ww #) -> (GHC.Types.I# ww, ww) }
 
 -- RHS size: {terms: 22, types: 16, coercions: 0, joins: 0/0}
-$wh1 [InlPrag=[2], Dmd=LCL(!P(L))] :: GHC.Prim.Int# -> Int
+$wh1 [InlPrag=[2], Dmd=LCS(!P(L))] :: GHC.Prim.Int# -> Int
 [LclId,
  Arity=1,
  Str=<1L>,
diff --git a/testsuite/tests/stranal/should_compile/T18903.stderr b/testsuite/tests/stranal/should_compile/T18903.stderr
index d237e7434f..8110312a8b 100644
--- a/testsuite/tests/stranal/should_compile/T18903.stderr
+++ b/testsuite/tests/stranal/should_compile/T18903.stderr
@@ -56,7 +56,7 @@ h :: Int -> Int
 h = \ (m :: Int) ->
       case m of wild { GHC.Types.I# ds ->
       let {
-        $wg [InlPrag=NOINLINE, Dmd=MCM(!P(M!P(L),1!P(L)))]
+        $wg [InlPrag=NOINLINE, Dmd=MC1(!P(M!P(L),1!P(L)))]
           :: GHC.Prim.Int# -> (# Int, Int #)
         [LclId, Arity=1, Str=<1L>, Unf=OtherCon []]
         $wg
diff --git a/testsuite/tests/stranal/sigs/BottomFromInnerLambda.stderr b/testsuite/tests/stranal/sigs/BottomFromInnerLambda.stderr
index 075a819db8..1c944f8520 100644
--- a/testsuite/tests/stranal/sigs/BottomFromInnerLambda.stderr
+++ b/testsuite/tests/stranal/sigs/BottomFromInnerLambda.stderr
@@ -1,20 +1,17 @@
 
 ==================== Strictness signatures ====================
-BottomFromInnerLambda.$trModule:
 BottomFromInnerLambda.expensive: <1!P(SL)>
 BottomFromInnerLambda.f: <1!P(SL)>
 
 
 
 ==================== Cpr signatures ====================
-BottomFromInnerLambda.$trModule:
 BottomFromInnerLambda.expensive: 1
 BottomFromInnerLambda.f:
 
 
 
 ==================== Strictness signatures ====================
-BottomFromInnerLambda.$trModule:
 BottomFromInnerLambda.expensive: <1!P(1L)>
 BottomFromInnerLambda.f: <1!P(1L)>
 
diff --git a/testsuite/tests/stranal/sigs/DmdAnalGADTs.stderr b/testsuite/tests/stranal/sigs/DmdAnalGADTs.stderr
index 2ed48eed70..2f7b6376f0 100644
--- a/testsuite/tests/stranal/sigs/DmdAnalGADTs.stderr
+++ b/testsuite/tests/stranal/sigs/DmdAnalGADTs.stderr
@@ -1,9 +1,5 @@
 
 ==================== Strictness signatures ====================
-DmdAnalGADTs.$tc'A:
-DmdAnalGADTs.$tc'B:
-DmdAnalGADTs.$tcD:
-DmdAnalGADTs.$trModule:
 DmdAnalGADTs.diverges: b
 DmdAnalGADTs.f: <1L>
 DmdAnalGADTs.f': <1L>
@@ -14,10 +10,6 @@ DmdAnalGADTs.hasStrSig: <1!P(L)>
 
 
 ==================== Cpr signatures ====================
-DmdAnalGADTs.$tc'A:
-DmdAnalGADTs.$tc'B:
-DmdAnalGADTs.$tcD:
-DmdAnalGADTs.$trModule:
 DmdAnalGADTs.diverges: b
 DmdAnalGADTs.f:
 DmdAnalGADTs.f': 1
@@ -28,10 +20,6 @@ DmdAnalGADTs.hasStrSig: 1
 
 
 ==================== Strictness signatures ====================
-DmdAnalGADTs.$tc'A:
-DmdAnalGADTs.$tc'B:
-DmdAnalGADTs.$tcD:
-DmdAnalGADTs.$trModule:
 DmdAnalGADTs.diverges: b
 DmdAnalGADTs.f: <1L>
 DmdAnalGADTs.f': <1L>
diff --git a/testsuite/tests/stranal/sigs/HyperStrUse.stderr b/testsuite/tests/stranal/sigs/HyperStrUse.stderr
index 08caf32af4..23c437158e 100644
--- a/testsuite/tests/stranal/sigs/HyperStrUse.stderr
+++ b/testsuite/tests/stranal/sigs/HyperStrUse.stderr
@@ -1,18 +1,15 @@
 
 ==================== Strictness signatures ====================
-HyperStrUse.$trModule:
 HyperStrUse.f: <1!P(1!P(L),A)><1L>
 
 
 
 ==================== Cpr signatures ====================
-HyperStrUse.$trModule:
 HyperStrUse.f: 1
 
 
 
 ==================== Strictness signatures ====================
-HyperStrUse.$trModule:
 HyperStrUse.f: <1!P(1!P(L),A)><1L>
 
 
diff --git a/testsuite/tests/stranal/sigs/NewtypeArity.stderr b/testsuite/tests/stranal/sigs/NewtypeArity.stderr
index 45bc691802..7190bedc35 100644
--- a/testsuite/tests/stranal/sigs/NewtypeArity.stderr
+++ b/testsuite/tests/stranal/sigs/NewtypeArity.stderr
@@ -1,26 +1,17 @@
 
 ==================== Strictness signatures ====================
-Test.$tc'MkT:
-Test.$tcT:
-Test.$trModule:
 Test.t: <1!P(L)><1!P(L)>
 Test.t2: <1!P(L)><1!P(L)>
 
 
 
 ==================== Cpr signatures ====================
-Test.$tc'MkT:
-Test.$tcT:
-Test.$trModule:
 Test.t: 1
 Test.t2: 1
 
 
 
 ==================== Strictness signatures ====================
-Test.$tc'MkT:
-Test.$tcT:
-Test.$trModule:
 Test.t: <1!P(L)><1!P(L)>
 Test.t2: <1!P(L)><1!P(L)>
 
diff --git a/testsuite/tests/stranal/sigs/StrAnalExample.stderr b/testsuite/tests/stranal/sigs/StrAnalExample.stderr
index 80855b392e..08485e735a 100644
--- a/testsuite/tests/stranal/sigs/StrAnalExample.stderr
+++ b/testsuite/tests/stranal/sigs/StrAnalExample.stderr
@@ -1,18 +1,15 @@
 
 ==================== Strictness signatures ====================
-StrAnalExample.$trModule:
 StrAnalExample.foo: <1L>
 
 
 
 ==================== Cpr signatures ====================
-StrAnalExample.$trModule:
 StrAnalExample.foo:
 
 
 
 ==================== Strictness signatures ====================
-StrAnalExample.$trModule:
 StrAnalExample.foo: <1L>
 
 
diff --git a/testsuite/tests/stranal/sigs/T12370.stderr b/testsuite/tests/stranal/sigs/T12370.stderr
index dc7dbdd2e5..3070069a1a 100644
--- a/testsuite/tests/stranal/sigs/T12370.stderr
+++ b/testsuite/tests/stranal/sigs/T12370.stderr
@@ -1,20 +1,17 @@
 
 ==================== Strictness signatures ====================
-T12370.$trModule:
 T12370.bar: <1!P(L)><1!P(L)>
 T12370.foo: <1!P(1!P(L),1!P(L))>
 
 
 
 ==================== Cpr signatures ====================
-T12370.$trModule:
 T12370.bar: 1
 T12370.foo: 1
 
 
 
 ==================== Strictness signatures ====================
-T12370.$trModule:
 T12370.bar: <1!P(L)><1!P(L)>
 T12370.foo: <1!P(1!P(L),1!P(L))>
 
diff --git a/testsuite/tests/stranal/sigs/T13331.stderr b/testsuite/tests/stranal/sigs/T13331.stderr
index 78cccb7fe4..feebb4eaa1 100644
--- a/testsuite/tests/stranal/sigs/T13331.stderr
+++ b/testsuite/tests/stranal/sigs/T13331.stderr
@@ -1,27 +1,15 @@
 
 ==================== Strictness signatures ====================
-T13331.$tc'Bin:
-T13331.$tc'Tip:
-T13331.$tcMap:
-T13331.$trModule:
 T13331.naiveInsertInt: <1L><L><1L>
 
 
 
 ==================== Cpr signatures ====================
-T13331.$tc'Bin:
-T13331.$tc'Tip:
-T13331.$tcMap:
-T13331.$trModule:
 T13331.naiveInsertInt:
 
 
 
 ==================== Strictness signatures ====================
-T13331.$tc'Bin:
-T13331.$tc'Tip:
-T13331.$tcMap:
-T13331.$trModule:
 T13331.naiveInsertInt: <1L><L><1L>
 
 
diff --git a/testsuite/tests/stranal/sigs/T13380f.stderr b/testsuite/tests/stranal/sigs/T13380f.stderr
index 4b17ceae85..1da38aeeee 100644
--- a/testsuite/tests/stranal/sigs/T13380f.stderr
+++ b/testsuite/tests/stranal/sigs/T13380f.stderr
@@ -1,6 +1,5 @@
 
 ==================== Strictness signatures ====================
-T13380f.$trModule:
 T13380f.f: <1!P(L)><1!P(L)><L>
 T13380f.g: <1!P(L)><ML><L>
 T13380f.h: <1!P(L)><ML><L>
@@ -11,7 +10,6 @@ T13380f.unsafeCall: <L>
 
 
 ==================== Cpr signatures ====================
-T13380f.$trModule:
 T13380f.f: 1(, 1)
 T13380f.g: 1(, 1)
 T13380f.h: 1(, 1)
@@ -22,7 +20,6 @@ T13380f.unsafeCall: 1(, 1)
 
 
 ==================== Strictness signatures ====================
-T13380f.$trModule:
 T13380f.f: <1!P(L)><1!P(L)><L>
 T13380f.g: <1!P(L)><ML><L>
 T13380f.h: <1!P(L)><ML><L>
diff --git a/testsuite/tests/stranal/sigs/T16197b.stderr b/testsuite/tests/stranal/sigs/T16197b.stderr
index ec45df4202..d4c250b44a 100644
--- a/testsuite/tests/stranal/sigs/T16197b.stderr
+++ b/testsuite/tests/stranal/sigs/T16197b.stderr
@@ -1,30 +1,15 @@
 
 ==================== Strictness signatures ====================
-T16197b.$tc'Box:
-T16197b.$tc'T:
-T16197b.$tcBox:
-T16197b.$tcT:
-T16197b.$trModule:
 T16197b.f: <1!P(L)>
 
 
 
 ==================== Cpr signatures ====================
-T16197b.$tc'Box:
-T16197b.$tc'T:
-T16197b.$tcBox:
-T16197b.$tcT:
-T16197b.$trModule:
 T16197b.f: 1
 
 
 
 ==================== Strictness signatures ====================
-T16197b.$tc'Box:
-T16197b.$tc'T:
-T16197b.$tcBox:
-T16197b.$tcT:
-T16197b.$trModule:
 T16197b.f: <1!P(L)>
 
 
diff --git a/testsuite/tests/stranal/sigs/T16859.stderr b/testsuite/tests/stranal/sigs/T16859.stderr
index 37718134a2..6dd199c07c 100644
--- a/testsuite/tests/stranal/sigs/T16859.stderr
+++ b/testsuite/tests/stranal/sigs/T16859.stderr
@@ -1,11 +1,5 @@
 
 ==================== Strictness signatures ====================
-T16859.$tc'External:
-T16859.$tc'Internal:
-T16859.$tc'Name:
-T16859.$tcName:
-T16859.$tcNameSort:
-T16859.$trModule:
 T16859.bar: <1!A><L>
 T16859.baz: <1L><1!P(L)><1C1(L)>
 T16859.buz: <1!P(L,L)>
@@ -19,12 +13,6 @@ T16859.n_uniq: <1!P(A,A,L,A)>
 
 
 ==================== Cpr signatures ====================
-T16859.$tc'External:
-T16859.$tc'Internal:
-T16859.$tc'Name:
-T16859.$tcName:
-T16859.$tcNameSort:
-T16859.$trModule:
 T16859.bar: 1
 T16859.baz: 1
 T16859.buz: 1
@@ -38,12 +26,6 @@ T16859.n_uniq: 1
 
 
 ==================== Strictness signatures ====================
-T16859.$tc'External:
-T16859.$tc'Internal:
-T16859.$tc'Name:
-T16859.$tcName:
-T16859.$tcNameSort:
-T16859.$trModule:
 T16859.bar: <1!A><L>
 T16859.baz: <L><1!P(L)><1C1(L)>
 T16859.buz: <1!P(L,L)>
diff --git a/testsuite/tests/stranal/sigs/T17932.stderr b/testsuite/tests/stranal/sigs/T17932.stderr
index dadd60b491..52b365bcc2 100644
--- a/testsuite/tests/stranal/sigs/T17932.stderr
+++ b/testsuite/tests/stranal/sigs/T17932.stderr
@@ -1,30 +1,15 @@
 
 ==================== Strictness signatures ====================
-T17932.$tc'Options:
-T17932.$tc'X:
-T17932.$tcOptions:
-T17932.$tcX:
-T17932.$trModule:
 T17932.flags: <1!P(1L,1L)>
 
 
 
 ==================== Cpr signatures ====================
-T17932.$tc'Options:
-T17932.$tc'X:
-T17932.$tcOptions:
-T17932.$tcX:
-T17932.$trModule:
 T17932.flags:
 
 
 
 ==================== Strictness signatures ====================
-T17932.$tc'Options:
-T17932.$tc'X:
-T17932.$tcOptions:
-T17932.$tcX:
-T17932.$trModule:
 T17932.flags: <1!P(1L,1L)>
 
 
diff --git a/testsuite/tests/stranal/sigs/T18086.stderr b/testsuite/tests/stranal/sigs/T18086.stderr
index 1748a0c145..ce14711025 100644
--- a/testsuite/tests/stranal/sigs/T18086.stderr
+++ b/testsuite/tests/stranal/sigs/T18086.stderr
@@ -1,20 +1,17 @@
 
 ==================== Strictness signatures ====================
-T18086.$trModule:
 T18086.m: <L>x
 T18086.panic: <L>x
 
 
 
 ==================== Cpr signatures ====================
-T18086.$trModule:
 T18086.m: b
 T18086.panic: b
 
 
 
 ==================== Strictness signatures ====================
-T18086.$trModule:
 T18086.m: <L>x
 T18086.panic: <L>x
 
diff --git a/testsuite/tests/stranal/sigs/T18907.stderr b/testsuite/tests/stranal/sigs/T18907.stderr
index 9d9aff99c8..235872a8eb 100644
--- a/testsuite/tests/stranal/sigs/T18907.stderr
+++ b/testsuite/tests/stranal/sigs/T18907.stderr
@@ -1,8 +1,5 @@
 
 ==================== Strictness signatures ====================
-T18907.$tc'H:
-T18907.$tcHuge:
-T18907.$trModule:
 T18907.f: <1L>
 T18907.g: <1P(SL,L,L,L,L)>
 T18907.h: <1!A><1L>
@@ -11,9 +8,6 @@ T18907.m: <1!B>b
 
 
 ==================== Cpr signatures ====================
-T18907.$tc'H:
-T18907.$tcHuge:
-T18907.$trModule:
 T18907.f:
 T18907.g:
 T18907.h:
@@ -22,9 +16,6 @@ T18907.m: b
 
 
 ==================== Strictness signatures ====================
-T18907.$tc'H:
-T18907.$tcHuge:
-T18907.$trModule:
 T18907.f: <1L>
 T18907.g: <1P(SL,L,L,L,L)>
 T18907.h: <1!A><1L>
diff --git a/testsuite/tests/stranal/sigs/T18957.hs b/testsuite/tests/stranal/sigs/T18957.hs
index 8f4550696d..b49ed1a4b8 100644
--- a/testsuite/tests/stranal/sigs/T18957.hs
+++ b/testsuite/tests/stranal/sigs/T18957.hs
@@ -28,5 +28,7 @@ h1 f x = f `seq'` if x < 100 then f x else 200
 h2 :: (Int -> Int) -> Int -> Int
 h2 f x = f `seq` if x < 100 then f x else 200
 
+-- | The first argument is evaluated lazily and multiple times, but called every
+-- time it's evaluated.
 h3 :: (Int -> Int) -> Int -> Int
 h3 f x = if x < 100 then f x + f (x+1) else 200
diff --git a/testsuite/tests/stranal/sigs/T18957.stderr b/testsuite/tests/stranal/sigs/T18957.stderr
index 3d730ce9fc..04937d4028 100644
--- a/testsuite/tests/stranal/sigs/T18957.stderr
+++ b/testsuite/tests/stranal/sigs/T18957.stderr
@@ -1,16 +1,14 @@
 
 ==================== Strictness signatures ====================
-T18957.$trModule:
-T18957.g: <MCM(L)><1L>
+T18957.g: <MC1(L)><1L>
 T18957.h1: <SCM(L)><1L>
 T18957.h2: <1CM(L)><1L>
-T18957.h3: <L><1L>
+T18957.h3: <LCS(L)><1L>
 T18957.seq': <1A><1L>
 
 
 
 ==================== Cpr signatures ====================
-T18957.$trModule:
 T18957.g:
 T18957.h1:
 T18957.h2:
@@ -20,11 +18,10 @@ T18957.seq':
 
 
 ==================== Strictness signatures ====================
-T18957.$trModule:
-T18957.g: <MCM(L)><1L>
+T18957.g: <MC1(L)><1L>
 T18957.h1: <SCM(L)><1L>
 T18957.h2: <1CM(L)><1L>
-T18957.h3: <L><1L>
+T18957.h3: <LCS(L)><1L>
 T18957.seq': <1A><1L>
 
 
diff --git a/testsuite/tests/stranal/sigs/T19407.stderr b/testsuite/tests/stranal/sigs/T19407.stderr
index 8d4045700a..a855d89810 100644
--- a/testsuite/tests/stranal/sigs/T19407.stderr
+++ b/testsuite/tests/stranal/sigs/T19407.stderr
@@ -1,23 +1,13 @@
 
 ==================== Strictness signatures ====================
-T19407.$tc'Huge:
-T19407.$tc'T:
-T19407.$tcHuge:
-T19407.$tcT:
-T19407.$trModule:
 T19407.f: <SP(1P(1L,A,A,A,A,A,A,A,A,A,A,A,A,A,A,A,A,A,A,A,A,A),ML)>
-T19407.g: <1!P(1L,A,A,A,A,A,A,A,A,A,A,A,A,A,A,A,A,A,A,A,A,A)><MP(A,ML)>
+T19407.g: <1!P(1L,A,A,A,A,A,A,A,A,A,A,A,A,A,A,A,A,A,A,A,A,A)><MP(A,1L)>
 T19407.h: <1!P(1L,A)>
 T19407.n: <1!P(A,1!P(L))>
 
 
 
 ==================== Cpr signatures ====================
-T19407.$tc'Huge:
-T19407.$tc'T:
-T19407.$tcHuge:
-T19407.$tcT:
-T19407.$trModule:
 T19407.f:
 T19407.g:
 T19407.h:
@@ -26,13 +16,8 @@ T19407.n: 1
 
 
 ==================== Strictness signatures ====================
-T19407.$tc'Huge:
-T19407.$tc'T:
-T19407.$tcHuge:
-T19407.$tcT:
-T19407.$trModule:
 T19407.f: <1P(1P(1L,A,A,A,A,A,A,A,A,A,A,A,A,A,A,A,A,A,A,A,A,A),ML)>
-T19407.g: <1!P(1L,A,A,A,A,A,A,A,A,A,A,A,A,A,A,A,A,A,A,A,A,A)><MP(A,ML)>
+T19407.g: <1!P(1L,A,A,A,A,A,A,A,A,A,A,A,A,A,A,A,A,A,A,A,A,A)><MP(A,1L)>
 T19407.h: <1!P(1L,A)>
 T19407.n: <1!P(A,1!P(L))>
 
diff --git a/testsuite/tests/stranal/sigs/T19871.stderr b/testsuite/tests/stranal/sigs/T19871.stderr
index f8f465fd82..13e67a2805 100644
--- a/testsuite/tests/stranal/sigs/T19871.stderr
+++ b/testsuite/tests/stranal/sigs/T19871.stderr
@@ -1,8 +1,5 @@
 
 ==================== Strictness signatures ====================
-T19871.$tc'Huge:
-T19871.$tcHuge:
-T19871.$trModule:
 T19871.absent: <1P(1L,ML,A,A,A,A,A,A,A,A,A,A)>
 T19871.ann: <1P(SL,L,L,L,L,L,L,L,L,L,L,L)>
 T19871.f1: <1!P(1L,A,A,A,A,A,A,A,A,A,A,A)>
@@ -17,16 +14,13 @@ T19871.f6: <1!P(A,A,A,A,A,1L,A,A,A,A,A,A)>
 T19871.f7: <1!P(A,A,A,A,A,A,1L,A,A,A,A,A)>
 T19871.f8: <1!P(A,A,A,A,A,A,A,1L,A,A,A,A)>
 T19871.f9: <1!P(A,A,A,A,A,A,A,A,1L,A,A,A)>
-T19871.guarded: <MCM(L)><1P(SL,L,L,L,L,L,L,L,L,L,L,L)>
+T19871.guarded: <MC1(L)><1P(SL,L,L,L,L,L,L,L,L,L,L,L)>
 T19871.sumIO: <1!P(1L)><1!P(L)><L>
 T19871.update: <1P(SL,L,L,L,L,L,L,L,L,L,L,L)>
 
 
 
 ==================== Cpr signatures ====================
-T19871.$tc'Huge:
-T19871.$tcHuge:
-T19871.$trModule:
 T19871.absent: 1
 T19871.ann: 1
 T19871.f1:
@@ -48,9 +42,6 @@ T19871.update: 1
 
 
 ==================== Strictness signatures ====================
-T19871.$tc'Huge:
-T19871.$tcHuge:
-T19871.$trModule:
 T19871.absent: <1P(1L,ML,A,A,A,A,A,A,A,A,A,A)>
 T19871.ann: <1P(SL,L,L,L,L,L,L,L,L,L,L,L)>
 T19871.f1: <1!P(1L,A,A,A,A,A,A,A,A,A,A,A)>
@@ -65,7 +56,7 @@ T19871.f6: <1!P(A,A,A,A,A,1L,A,A,A,A,A,A)>
 T19871.f7: <1!P(A,A,A,A,A,A,1L,A,A,A,A,A)>
 T19871.f8: <1!P(A,A,A,A,A,A,A,1L,A,A,A,A)>
 T19871.f9: <1!P(A,A,A,A,A,A,A,A,1L,A,A,A)>
-T19871.guarded: <MCM(L)><1P(SL,L,L,L,L,L,L,L,L,L,L,L)>
+T19871.guarded: <MC1(L)><1P(SL,L,L,L,L,L,L,L,L,L,L,L)>
 T19871.sumIO: <1!P(1L)><1!P(L)><L>
 T19871.update: <1P(SL,L,L,L,L,L,L,L,L,L,L,L)>
 
diff --git a/testsuite/tests/stranal/sigs/T20746.stderr b/testsuite/tests/stranal/sigs/T20746.stderr
index b0656cd13d..5be614867a 100644
--- a/testsuite/tests/stranal/sigs/T20746.stderr
+++ b/testsuite/tests/stranal/sigs/T20746.stderr
@@ -1,21 +1,18 @@
 
 ==================== Strictness signatures ====================
-Foo.$trModule:
-Foo.f: <MP(A,MCM(L),A)><L>
+Foo.f: <MP(A,1C1(L),A)><L>
 Foo.foogle: <L><L>
 
 
 
 ==================== Cpr signatures ====================
-Foo.$trModule:
 Foo.f: 1
 Foo.foogle: 1
 
 
 
 ==================== Strictness signatures ====================
-Foo.$trModule:
-Foo.f: <MP(A,MCM(L),A)><L>
+Foo.f: <MP(A,1C1(L),A)><L>
 Foo.foogle: <L><L>
 
 
diff --git a/testsuite/tests/stranal/sigs/T20746b.stderr b/testsuite/tests/stranal/sigs/T20746b.stderr
index bd23944c61..7e6fada4e5 100644
--- a/testsuite/tests/stranal/sigs/T20746b.stderr
+++ b/testsuite/tests/stranal/sigs/T20746b.stderr
@@ -1,20 +1,17 @@
 
 ==================== Strictness signatures ====================
-T20746b.$trModule:
 T20746b.f: <1L><L><L>
 T20746b.mightThrow: <L><L>
 
 
 
 ==================== Cpr signatures ====================
-T20746b.$trModule:
 T20746b.f: 1
 T20746b.mightThrow: 1
 
 
 
 ==================== Strictness signatures ====================
-T20746b.$trModule:
 T20746b.f: <1L><L><L>
 T20746b.mightThrow: <L><L>
 
diff --git a/testsuite/tests/stranal/sigs/T21081.hs b/testsuite/tests/stranal/sigs/T21081.hs
new file mode 100644
index 0000000000..e07ec410bc
--- /dev/null
+++ b/testsuite/tests/stranal/sigs/T21081.hs
@@ -0,0 +1,123 @@
+{-# LANGUAGE BangPatterns #-}
+
+module T21081 where
+
+-- | Should put demand `MP(SL,SL)` or `MP(1L,1L)` on `pr`, telling us that `f`
+-- will evaluate both components of `pr` whenever it evaluates `pr` lazily.
+f :: (Bool, Bool) -> (Bool, Bool)
+f pr = (case pr of (a,b) -> a /= b, True)
+{-# NOINLINE f #-}
+-- | If `f` gets the correct signature, we can case-bind `z` here (not tested)
+g :: Int -> (Bool, Bool)
+g x = let y = let z = odd x in (z,z) in f y
+
+-- | Should put demand `LCS(C1(L))` on `f`, telling us that whenever `myfoldl`
+-- evaluates `f`, it will also call it at least once (`S`) and then always call
+-- it with a second argument (`1`).
+-- This in turn allows us to eta-reduce `(\a b -> f a b)` to `f` (not tested,
+-- but there's T20040 which tests an even more complicated case).
+myfoldl :: (a -> b -> a) -> a -> [b] -> a
+myfoldl f z [] = z
+myfoldl f !z (x:xs) = myfoldl (\a b -> f a b) (f z x) xs
+
+-- | Should put demand `LCL(C1(L))` on `f`
+blah :: (Int -> Int -> Int) -> Int -> Int
+blah f 0 = 0
+blah f 1 = f `seq` 1
+blah f x = f (x+1) (x+2) + f (x+3) (x+4)
+{-# NOINLINE blah #-}
+-- | It's not safe to eta-reduce the lambda here, because `do_blah undefined`
+-- would crash.
+do_blah :: (Int -> Int -> Int) -> Int
+do_blah f = blah (\a b -> f a b) 1
+
+-- | Should put demand `MP(ML,ML)` on `p`, not `MP(L,L)`.
+h :: (Int, Int) -> Int -> Int
+h p 0 = 0
+h p 1 = fst p
+h p y = snd p + y
+{-# NOINLINE h #-}
+-- | We want to use call-by-name for `a` and `b`, justified by the used-once
+-- info on `p` in `h`.
+blurg :: Int -> Int
+blurg x =
+  let a = sum [0..x]
+      b = sum [1..x]
+  in h (a,b) x
+
+-- | But we still need `p` to have demand `MP(L,L)` or simply `L` here.
+-- NOT `MP(ML,ML)`. This demonstrates that product usage demands stay absolute.
+h2 :: (Int, Int) -> Int -> Int
+h2 p y = h p y + h p (y+1)
+{-# NOINLINE h2 #-}
+-- | Otherwise we'd use call-by-name for `a` and `b` here, although they are
+-- evaluated multiple times in `h2`.
+blurg2 :: Int -> Int
+blurg2 x =
+  let a = sum [0..x]
+      b = sum [1..x]
+  in h2 (a,b) x
+
+-- | Must not put demand `MP(1L,1L)` on `x` (e.g., strict in the components).
+-- This demonstrates that `plusDmd` must fall back to `lubSubDemand` when both
+-- Demands are lazy.
+i :: Bool -> Bool -> (Int, Int) -> Int
+i b b' x = (if b then fst x else 3) + (if b' then snd x else 4)
+
+fst' :: (a,b) -> a
+fst' (x,_) = x
+{-# NOINLINE fst' #-}
+
+snd' :: (a,b) -> b
+snd' (_,x) = x
+{-# NOINLINE snd' #-}
+
+-- | We want `SP(1L,1L)`, even if neither `fst'` nor `snd'` are strict in both
+-- components. This dictates that `plusDmd` has to do `plusSubDemand` when both
+-- Demands are strict. Which differs in a crucial way from the situation in `i`!
+j :: (Integer, Integer) -> Integer
+j p = fst' p + snd' p
+
+
+-- A few examples from a call between Simon and me
+
+call1 :: (Bool,Bool) -> (Bool, Bool)
+call1 x = (x `seq` case x of (a,b) -> a, True)
+--  call1 :: <MP(1L,A)>
+-- x may not be evald at all, but
+--   if `x` is evaluated at all, then
+--   then `a` is evaluated exactly once (in total)
+
+call2 :: (Bool,Bool) -> (Bool, Bool)
+call2 x = (x `seq` case x of (a,b) -> a, case x of (a,b) -> a)
+--  call2 :: LP(SL,A)
+-- If x is evaluated, then `a` is (in total) evaluated
+-- maybe as much as twice
+
+call3 :: (Bool,Bool) -> (Bool, ())
+call3 x = (x `seq` case x of (a,b) -> a, x `seq` ())
+--  call3 :: LP(ML,A)
+-- If x is evaluated, then `a` may not be evaluated at all.
+
+call4 :: (Bool,Bool) -> Bool -> (Bool, Bool)
+call4 x y = y `seq` (case x of (a,b) -> a, True)
+--  call4 :: <MP(1L,A)><1A>
+-- What is demand on x in (call4 x x)?
+-- NOT SP(1L,A)!!
+
+call5 :: (Bool,Bool) -> Bool -> (Bool, ())
+call5 x y = (case x of (a,b) -> a, y `seq` ())
+--  call5 :: <MP(1L,A)><MA>
+-- What is demand on x in `snd (call5 x x)`?
+-- Not LP(1L,A)!!  call5 might evaluate second argument but not first
+-- Lub because we might evaluate one OR the other.
+
+call6 :: (Int,Int) -> (Int,Int) -> Bool -> Int
+call6 x y True  = 42
+call6 x y False = case y of (a, _) -> case x of (b, _) -> a + b
+--  call6 :: <MP(1L)><MP(1L)><1L>
+-- What is demand on x in `call6 x x`?
+-- Not LP(1L)!! It's LP(SL)
+-- call6 might evaluate both its arguments and, in each case
+-- evaluate the component once.  So the component of x
+-- gets evaluated twice.
diff --git a/testsuite/tests/stranal/sigs/T21081.stderr b/testsuite/tests/stranal/sigs/T21081.stderr
new file mode 100644
index 0000000000..ec7e776ca8
--- /dev/null
+++ b/testsuite/tests/stranal/sigs/T21081.stderr
@@ -0,0 +1,69 @@
+
+==================== Strictness signatures ====================
+T21081.blah: <LCL(C1(L))><1!P(1L)>
+T21081.blurg: <S!P(SL)>
+T21081.blurg2: <S!P(SL)>
+T21081.call1: <MP(1L,A)>
+T21081.call2: <LP(SL,A)>
+T21081.call3: <LP(ML,A)>
+T21081.call4: <MP(1L,A)><1A>
+T21081.call5: <MP(1L,A)><MA>
+T21081.call6: <MP(1L,A)><MP(1L,A)><1L>
+T21081.do_blah: <LCS(C1(L))>
+T21081.f: <MP(SL,SL)>
+T21081.fst': <1!P(1L,A)>
+T21081.g: <ML>
+T21081.h: <MP(ML,ML)><1!P(1L)>
+T21081.h2: <L><S!P(SL)>
+T21081.i: <1L><1L><MP(ML,ML)>
+T21081.j: <S!P(1L,1L)>
+T21081.myfoldl: <LCS(C1(L))><1L><1L>
+T21081.snd': <1!P(A,1L)>
+
+
+
+==================== Cpr signatures ====================
+T21081.blah: 1
+T21081.blurg:
+T21081.blurg2: 1
+T21081.call1: 1(, 2)
+T21081.call2: 1
+T21081.call3: 1
+T21081.call4: 1(, 2)
+T21081.call5: 1
+T21081.call6: 1
+T21081.do_blah: 1
+T21081.f: 1(, 2)
+T21081.fst':
+T21081.g: 1(, 2)
+T21081.h:
+T21081.h2: 1
+T21081.i: 1
+T21081.j:
+T21081.myfoldl:
+T21081.snd':
+
+
+
+==================== Strictness signatures ====================
+T21081.blah: <LCL(C1(L))><1!P(1L)>
+T21081.blurg: <1!P(SL)>
+T21081.blurg2: <1!P(SL)>
+T21081.call1: <MP(1L,A)>
+T21081.call2: <LP(SL,A)>
+T21081.call3: <LP(ML,A)>
+T21081.call4: <MP(1L,A)><1A>
+T21081.call5: <MP(1L,A)><MA>
+T21081.call6: <MP(1L,A)><MP(1L,A)><1L>
+T21081.do_blah: <LCS(C1(L))>
+T21081.f: <MP(SL,SL)>
+T21081.fst': <1!P(1L,A)>
+T21081.g: <ML>
+T21081.h: <MP(ML,ML)><1!P(1L)>
+T21081.h2: <L><1!P(SL)>
+T21081.i: <1L><1L><MP(ML,ML)>
+T21081.j: <1!P(1L,1L)>
+T21081.myfoldl: <LCS(C1(L))><1L><1L>
+T21081.snd': <1!P(A,1L)>
+
+
diff --git a/testsuite/tests/stranal/sigs/T21119.stderr b/testsuite/tests/stranal/sigs/T21119.stderr
index 0a398888d0..dade4dc2a6 100644
--- a/testsuite/tests/stranal/sigs/T21119.stderr
+++ b/testsuite/tests/stranal/sigs/T21119.stderr
@@ -2,22 +2,16 @@
 ==================== Strictness signatures ====================
 T21119.$fMyShow(,): <1!A>
 T21119.$fMyShowInt: <1!A>
-T21119.$tc'C:MyShow:
-T21119.$tcMyShow:
-T21119.$trModule:
 T21119.get: <1!P(1!P(L),1!P(L))><1!P(L)><1L>
 T21119.getIO: <1P(1L,ML)><1L><ML><L>
-T21119.indexError: <1C1(L)><1!B><S!S><S!S>b
-T21119.throwIndexError: <MCM(L)><MA><L><L><L>x
+T21119.indexError: <1C1(S)><1!B><S!S><S!S>b
+T21119.throwIndexError: <MC1(L)><MA><L><L><L>x
 
 
 
 ==================== Cpr signatures ====================
 T21119.$fMyShow(,):
 T21119.$fMyShowInt:
-T21119.$tc'C:MyShow:
-T21119.$tcMyShow:
-T21119.$trModule:
 T21119.get:
 T21119.getIO: 1
 T21119.indexError: b
@@ -28,12 +22,9 @@ T21119.throwIndexError: b
 ==================== Strictness signatures ====================
 T21119.$fMyShow(,): <1!A>
 T21119.$fMyShowInt: <1!A>
-T21119.$tc'C:MyShow:
-T21119.$tcMyShow:
-T21119.$trModule:
 T21119.get: <1!P(1!P(L),1!P(L))><1!P(L)><1L>
 T21119.getIO: <1P(1L,ML)><1L><ML><L>
-T21119.indexError: <1C1(L)><1!B><S!S><S!S>b
-T21119.throwIndexError: <MCM(L)><MA><L><L><L>x
+T21119.indexError: <1C1(S)><1!B><S!S><S!S>b
+T21119.throwIndexError: <MC1(L)><MA><L><L><L>x
 
 
diff --git a/testsuite/tests/stranal/sigs/T5075.stderr b/testsuite/tests/stranal/sigs/T5075.stderr
index e367385d52..9bc8301440 100644
--- a/testsuite/tests/stranal/sigs/T5075.stderr
+++ b/testsuite/tests/stranal/sigs/T5075.stderr
@@ -1,14 +1,12 @@
 
 ==================== Strictness signatures ====================
-T5075.$trModule:
-T5075.f: <S!P(A,A,SCS(C1(L)),A,A,A,A,A)><LP(A,A,LCL(C1(L)),A,A,A,L)><L>
+T5075.f: <S!P(A,A,SCS(C1(L)),A,A,A,A,A)><LP(A,A,LCS(C1(L)),A,A,A,LCS(L))><L>
 T5075.g: <1L><S!P(L)>
 T5075.h: <S!P(L)>
 
 
 
 ==================== Cpr signatures ====================
-T5075.$trModule:
 T5075.f: 1
 T5075.g: 2
 T5075.h:
@@ -16,8 +14,7 @@ T5075.h:
 
 
 ==================== Strictness signatures ====================
-T5075.$trModule:
-T5075.f: <1P(A,A,SCS(C1(L)),A,A,A,A,A)><LP(A,A,LCL(C1(L)),A,A,A,L)><L>
+T5075.f: <1P(A,A,SCS(C1(L)),A,A,A,A,A)><LP(A,A,LCS(C1(L)),A,A,A,LCS(L))><L>
 T5075.g: <1L><S!P(L)>
 T5075.h: <1!P(L)>
 
diff --git a/testsuite/tests/stranal/sigs/T8569.stderr b/testsuite/tests/stranal/sigs/T8569.stderr
index 187047e612..0330cc6b61 100644
--- a/testsuite/tests/stranal/sigs/T8569.stderr
+++ b/testsuite/tests/stranal/sigs/T8569.stderr
@@ -1,27 +1,15 @@
 
 ==================== Strictness signatures ====================
-T8569.$tc'Rdata:
-T8569.$tc'Rint:
-T8569.$tcRep:
-T8569.$trModule:
 T8569.addUp: <1L><L>
 
 
 
 ==================== Cpr signatures ====================
-T8569.$tc'Rdata:
-T8569.$tc'Rint:
-T8569.$tcRep:
-T8569.$trModule:
 T8569.addUp:
 
 
 
 ==================== Strictness signatures ====================
-T8569.$tc'Rdata:
-T8569.$tc'Rint:
-T8569.$tcRep:
-T8569.$trModule:
 T8569.addUp: <1L><L>
 
 
diff --git a/testsuite/tests/stranal/sigs/T8598.stderr b/testsuite/tests/stranal/sigs/T8598.stderr
index 747c6a096b..00542be668 100644
--- a/testsuite/tests/stranal/sigs/T8598.stderr
+++ b/testsuite/tests/stranal/sigs/T8598.stderr
@@ -1,18 +1,15 @@
 
 ==================== Strictness signatures ====================
-T8598.$trModule:
 T8598.fun: <1!P(L)>
 
 
 
 ==================== Cpr signatures ====================
-T8598.$trModule:
 T8598.fun: 1
 
 
 
 ==================== Strictness signatures ====================
-T8598.$trModule:
 T8598.fun: <1!P(L)>
 
 
diff --git a/testsuite/tests/stranal/sigs/UnsatFun.stderr b/testsuite/tests/stranal/sigs/UnsatFun.stderr
index a9c3ca340a..c659311b22 100644
--- a/testsuite/tests/stranal/sigs/UnsatFun.stderr
+++ b/testsuite/tests/stranal/sigs/UnsatFun.stderr
@@ -1,18 +1,16 @@
 
 ==================== Strictness signatures ====================
-UnsatFun.$trModule:
 UnsatFun.f: <1!S><B>b
 UnsatFun.g: <1!S>b
-UnsatFun.g': <ML>
+UnsatFun.g': <MS>
 UnsatFun.g3: <A>
 UnsatFun.h: <1C1(L)>
-UnsatFun.h2: <1L><MCM(L)>
+UnsatFun.h2: <1L><MC1(L)>
 UnsatFun.h3: <1C1(A)>
 
 
 
 ==================== Cpr signatures ====================
-UnsatFun.$trModule:
 UnsatFun.f: b
 UnsatFun.g:
 UnsatFun.g':
@@ -24,13 +22,12 @@ UnsatFun.h3: 1
 
 
 ==================== Strictness signatures ====================
-UnsatFun.$trModule:
 UnsatFun.f: <1!S><B>b
 UnsatFun.g: <1!S>b
-UnsatFun.g': <ML>
+UnsatFun.g': <MS>
 UnsatFun.g3: <A>
 UnsatFun.h: <1C1(L)>
-UnsatFun.h2: <1L><MCM(L)>
+UnsatFun.h2: <1L><MC1(L)>
 UnsatFun.h3: <1C1(A)>
 
 
diff --git a/testsuite/tests/stranal/sigs/all.T b/testsuite/tests/stranal/sigs/all.T
index 876d2242d8..3782fa97a6 100644
--- a/testsuite/tests/stranal/sigs/all.T
+++ b/testsuite/tests/stranal/sigs/all.T
@@ -1,7 +1,7 @@
 # This directory contains tests where we annotate functions with expected
 # type signatures, and verify that these actually those found by the compiler
 
-setTestOpts(extra_hc_opts('-ddump-str-signatures -ddump-cpr-signatures'))
+setTestOpts(extra_hc_opts('-ddump-str-signatures -ddump-cpr-signatures -dno-typeable-binds'))
 
 # We are testing the result of an optimization, so no use
 # running them in various runtimes
@@ -31,5 +31,5 @@ test('T18907', normal, compile, [''])
 test('T13331', normal, compile, [''])
 test('T20746', normal, compile, [''])
 test('T20746b', normal, compile, [''])
-
+test('T21081', normal, compile, [''])
 test('T21119', normal, compile, [''])