Demand: Let `Boxed` win in `lubBoxity` (#21119)

Previously, we let `Unboxed` win in `lubBoxity`, which is unsoundly optimistic
in terms ob Boxity analysis. "Unsoundly" in the sense that we sometimes unbox
parameters that we better shouldn't unbox. Examples are #18907 and T19871.absent.

Until now, we thought that this hack pulled its weight becuase it worked around
some shortcomings of the phase separation between Boxity analysis and CPR
analysis. But it is a gross hack which caused regressions itself that needed all
kinds of fixes and workarounds. See for example #20767. It became impossible to
work with in !7599, so I want to remove it.

For example, at the moment, `lubDmd B dmd` will not unbox `dmd`,
but `lubDmd A dmd` will. Given that `B` is supposed to be the bottom element of
the lattice, it's hardly justifiable to get a better demand when `lub`bing with
`A`.

The consequence of letting `Boxed` win in `lubBoxity` is that we *would* regress
 #2387, #16040 and parts of #5075 and T19871.sumIO, until Boxity and CPR
are able to communicate better. Fortunately, that is not the case since I could
tweak the other source of optimism in Boxity analysis that is described in
`Note [Unboxed demand on function bodies returning small products]` so that
we *recursively* assume unboxed demands on function bodies returning small
products. See the updated Note.

`Note [Boxity for bottoming functions]` describes why we need bottoming
functions to have signatures that say that they deeply unbox their arguments.
In so doing, I had to tweak `finaliseArgBoxities` so that it will never unbox
recursive data constructors. This is in line with our handling of them in CPR.
I updated `Note [Which types are unboxed?]` to reflect that.

In turn we fix #21119, #20767, #18907, T19871.absent and get a much simpler
implementation (at least to think about). We can also drop the very ad-hoc
definition of `deferAfterPreciseException` and its Note in favor of the
simple, intuitive definition we used to have.

Metric Decrease:
    T16875
    T18223
    T18698a
    T18698b
    hard_hole_fits
Metric Increase:
    LargeRecord
    MultiComponentModulesRecomp
    T15703
    T8095
    T9872d

Out of all the regresions, only the one in T9872d doesn't vanish in a perf
build, where the compiler is bootstrapped with -O2 and thus SpecConstr.
Reason for regressions:

  * T9872d is due to `ty_co_subst` taking its `LiftingContext` boxed.
    That is because the context is passed to a function argument, for
    example in `liftCoSubstTyVarBndrUsing`.
  * In T15703, LargeRecord and T8095, we get a bit more allocations in
    `expand_syn` and `piResultTys`, because a `TCvSubst` isn't unboxed.
    In both cases that guards against reboxing in some code paths.
  * The same is true for MultiComponentModulesRecomp, where we get less unboxing
    in `GHC.Unit.Finder.$wfindInstalledHomeModule`. In a perf build, allocations
    actually *improve* by over 4%!

Results on NoFib:

--------------------------------------------------------------------------------
        Program         Allocs    Instrs
--------------------------------------------------------------------------------
         awards          -0.4%     +0.3%
      cacheprof          -0.3%     +2.4%
            fft          -1.5%     -5.1%
       fibheaps          +1.2%     +0.8%
          fluid          -0.3%     -0.1%
            ida          +0.4%     +0.9%
   k-nucleotide          +0.4%     -0.1%
     last-piece         +10.5%    +13.9%
           lift          -4.4%     +3.5%
        mandel2         -99.7%    -99.8%
           mate          -0.4%     +3.6%
         parser          -1.0%     +0.1%
         puzzle         -11.6%     +6.5%
reverse-complem          -3.0%     +2.0%
            scs          -0.5%     +0.1%
         sphere          -0.4%     -0.2%
      wave4main          -8.2%     -0.3%
--------------------------------------------------------------------------------
Summary excludes mandel2 because of excessive bias
            Min         -11.6%     -5.1%
            Max         +10.5%    +13.9%
 Geometric Mean          -0.2%     +0.3%
--------------------------------------------------------------------------------

Not bad for a bug fix.

The regression in `last-piece` could become a win if SpecConstr would work on
non-recursive functions. The regression in `fibheaps` is due to
`Note [Reboxed crud for bottoming calls]`, e.g., #21128.

44 files changed, 618 insertions, 616 deletions

diff --git a/compiler/GHC/Core/Coercion.hs b/compiler/GHC/Core/Coercion.hs
index a5f2f34221..4cfdc3ee82 100644
--- a/compiler/GHC/Core/Coercion.hs
+++ b/compiler/GHC/Core/Coercion.hs
@@ -2057,7 +2057,9 @@ substForAllCoBndrUsingLC sym sco (LC subst lc_env) tv co
 ty_co_subst :: LiftingContext -> Role -> Type -> Coercion
 ty_co_subst !lc role ty
     -- !lc: making this function strict in lc allows callers to
-    -- pass its two components separately, rather than boxing them
+    -- pass its two components separately, rather than boxing them.
+    -- Unfortunately, Boxity Analysis concludes that we need lc boxed
+    -- because it's used that way in liftCoSubstTyVarBndrUsing.
   = go role ty
   where
     go :: Role -> Type -> Coercion
diff --git a/compiler/GHC/Core/Opt/DmdAnal.hs b/compiler/GHC/Core/Opt/DmdAnal.hs
index eea60eb976..93c7e38ef9 100644
--- a/compiler/GHC/Core/Opt/DmdAnal.hs
+++ b/compiler/GHC/Core/Opt/DmdAnal.hs
@@ -891,7 +891,7 @@ dmdAnalRhsSig
 -- to the Id, and augment the environment with the signature as well.
 -- See Note [NOINLINE and strictness]
 dmdAnalRhsSig top_lvl rec_flag env let_dmd id rhs
-  = -- pprTrace "dmdAnalRhsSig" (ppr id $$ ppr let_dmd $$ ppr sig $$ ppr lazy_fv) $
+  = -- pprTrace "dmdAnalRhsSig" (ppr id $$ ppr let_dmd $$ ppr rhs_dmds $$ ppr sig $$ ppr lazy_fv) $
     (final_env, lazy_fv, final_id, final_rhs)
   where
     rhs_arity = idArity id
@@ -904,15 +904,17 @@ dmdAnalRhsSig top_lvl rec_flag env let_dmd id rhs
       -- See Note [Demand analysis for join points]
       -- See Note [Invariants on join points] invariant 2b, in GHC.Core
       --     rhs_arity matches the join arity of the join point
-      = let_dmd
+      -- See Note [Unboxed demand on function bodies returning small products]
+      = unboxedWhenSmall env rec_flag (resultType_maybe id) let_dmd
       | otherwise
       -- See Note [Unboxed demand on function bodies returning small products]
-      = unboxedWhenSmall (ae_opts env) (unboxableResultWidth env id) topSubDmd
+      = unboxedWhenSmall env rec_flag (resultType_maybe id) topSubDmd
 
-    -- See Note [Do not unbox class dictionaries]
     WithDmdType rhs_dmd_ty rhs' = dmdAnal env rhs_dmd rhs
-    DmdType rhs_fv rhs_dmds rhs_div    = rhs_dmd_ty
-    (final_rhs_dmds, final_rhs) = finaliseArgBoxities env id rhs_arity rhs'
+    DmdType rhs_fv rhs_dmds rhs_div = rhs_dmd_ty
+    -- See Note [Do not unbox class dictionaries]
+    -- See Note [Boxity for bottoming functions]
+    (final_rhs_dmds, final_rhs) = finaliseArgBoxities env id rhs_arity rhs' rhs_div
                                   `orElse` (rhs_dmds, rhs')
 
     sig = mkDmdSigForArity rhs_arity (DmdType sig_fv final_rhs_dmds rhs_div)
@@ -942,25 +944,44 @@ dmdAnalRhsSig top_lvl rec_flag env let_dmd id rhs
     -- See Note [Lazy and unleashable free variables]
     !(!lazy_fv, !sig_fv) = partitionVarEnv isWeakDmd rhs_fv2
 
-unboxableResultWidth :: AnalEnv -> Id -> Maybe Arity
-unboxableResultWidth env id
+-- | The result type after applying 'idArity' many arguments. Returns 'Nothing'
+-- when the type doesn't have exactly 'idArity' many arrows.
+resultType_maybe :: Id -> Maybe Type
+resultType_maybe id
   | (pis,ret_ty) <- splitPiTys (idType id)
   , count (not . isNamedBinder) pis == idArity id
-  , Just (tc, _tc_args, _co) <- normSplitTyConApp_maybe (ae_fam_envs env) ret_ty
-  , Just dc <- tyConSingleAlgDataCon_maybe tc
-  , null (dataConExTyCoVars dc) -- Can't unbox results with existentials
-  = Just (dataConRepArity dc)
+  = Just $! ret_ty
   | otherwise
   = Nothing
 
-unboxedWhenSmall :: DmdAnalOpts -> Maybe Arity -> SubDemand -> SubDemand
+unboxedWhenSmall :: AnalEnv -> RecFlag -> Maybe Type -> SubDemand -> SubDemand
 -- See Note [Unboxed demand on function bodies returning small products]
-unboxedWhenSmall opts mb_n sd
-  | Just n <- mb_n
-  , n <= dmd_unbox_width opts
-  = unboxSubDemand sd
-  | otherwise
-  = sd
+unboxedWhenSmall _   _        Nothing       sd = sd
+unboxedWhenSmall env rec_flag (Just ret_ty) sd = go 1 ret_ty sd
+  where
+    -- | Magic constant, bounding the depth of optimistic 'Unboxed' flags. We
+    -- might want to minmax in the future.
+    max_depth | isRec rec_flag = 3 -- So we get at most something as deep as !P(L!P(L!L))
+              | otherwise      = 1 -- Otherwise be unbox too deep in T18109, T18174 and others and get a bunch of stack overflows
+    go :: Int -> Type -> SubDemand -> SubDemand
+    go depth ty sd
+      | depth <= max_depth
+      , Just (tc, tc_args, _co) <- normSplitTyConApp_maybe (ae_fam_envs env) ty
+      , Just dc <- tyConSingleAlgDataCon_maybe tc
+      , null (dataConExTyCoVars dc) -- Can't unbox results with existentials
+      , dataConRepArity dc <= dmd_unbox_width (ae_opts env)
+      , Just (_, ds) <- viewProd (dataConRepArity dc) sd
+      , arg_tys <- map scaledThing $ dataConInstArgTys dc tc_args
+      , equalLength ds arg_tys
+      = mkProd Unboxed $! strictZipWith (go_dmd (depth+1)) arg_tys ds
+      | otherwise
+      = sd
+
+    go_dmd :: Int -> Type -> Demand -> Demand
+    go_dmd depth ty dmd = case dmd of
+      AbsDmd  -> AbsDmd
+      BotDmd  -> BotDmd
+      n :* sd -> n :* go depth ty sd
 
 -- | If given the (local, non-recursive) let-bound 'Id', 'useLetUp' determines
 -- whether we should process the binding up (body before rhs) or down (rhs
@@ -1179,6 +1200,69 @@ Now f's optimised RHS will be \x.a, but if we change g to (error "..")
 (since it is apparently Absent) and then inline (\x. fst g) we get
 disaster.  But regardless, #18638 was a more complicated version of
 this, that actually happened in practice.
+
+Note [Boxity for bottoming functions]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+```hs
+indexError :: Show a => (a, a) -> a -> String -> b
+-- Str=<..><1!P(S,S)><1S><S>b
+indexError rng i s = error (show rng ++ show i ++ show s)
+
+get :: (Int, Int) -> Int -> [a] -> a
+get p@(l,u) i xs
+  | l <= i, i < u = xs !! (i-u)
+  | otherwise     = indexError p i "get"
+```
+The hot path of `get` certainly wants to unbox `p` as well as `l` and `u`, but
+the unimportant, diverging error path needs `l` and `u` boxed (although the
+wrapper for `indexError` *will* unbox `p`). This pattern often occurs in
+performance sensitive code that does bounds-checking.
+
+It would be a shame to let `Boxed` win for the fields! So here's what we do:
+While to summarising `indexError`'s boxity signature in `finaliseArgBoxities`,
+we `unboxDeeplyDmd` all its argument demands and are careful not to discard
+excess boxity in the `StopUnboxing` case, to get the signature
+`<1!P(!S,!S)><1!S><S!S>b`.
+
+Then worker/wrapper will not only unbox the pair passed to `indexError` (as it
+would do anyway), demand analysis will also pretend that `indexError` needs `l`
+and `u` unboxed (and the two other args). Which is a lie, because `indexError`'s
+type abstracts over their types and could never unbox them.
+
+The important change is at the *call sites* of `$windexError`: Boxity analysis
+will conclude to unbox `l` and `u`, which *will* incur reboxing of crud that
+should better float to the call site of `$windexError`. There we don't care
+much, because it's in the slow, diverging code path! And that floating often
+happens, but not always. See Note [Reboxed crud for bottoming calls].
+
+Note [Reboxed crud for bottoming calls]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+For functions like `get` in Note [Boxity for bottoming functions], it's clear
+that the reboxed crud will be floated inside to the call site of `$windexError`.
+But here's an example where that is not the case:
+```hs
+import GHC.Ix
+
+theresCrud :: Int -> Int -> Int
+theresCrud x y = go x
+  where
+    go 0 = index (0,y) 0
+    go 1 = index (x,y) 1
+    go n = go (n-1)
+    {-# NOINLINE theresCrud #-}
+```
+If you look at the Core, you'll see that `y` will be reboxed and used in the
+two exit join points for the `$windexError` calls, while `x` is only reboxed in the
+exit join point for `index (x,y) 1` (happens in lvl below):
+```
+$wtheresCrud = \ ww ww1 ->
+      let { y = I# ww1 } in
+      join { lvl2 = ... case lvl1 ww y of wild { }; ... } in
+      join { lvl3 = ... case lvl y of wild { }; ... } in
+      ...
+```
+This is currently a bug that we willingly accept and it's documented in #21128.
 -}
 
 {- *********************************************************************
@@ -1442,9 +1526,9 @@ incTopBudget (MkB n bg) = MkB (n+1) bg
 positiveTopBudget :: Budgets -> Bool
 positiveTopBudget (MkB n _) = n >= 0
 
-finaliseArgBoxities :: AnalEnv -> Id -> Arity -> CoreExpr
+finaliseArgBoxities :: AnalEnv -> Id -> Arity -> CoreExpr -> Divergence
                     -> Maybe ([Demand], CoreExpr)
-finaliseArgBoxities env fn arity rhs
+finaliseArgBoxities env fn arity rhs div
   | arity > count isId bndrs  -- Can't find enough binders
   = Nothing  -- This happens if we have   f = g
              -- Then there are no binders; we don't worker/wrapper; and we
@@ -1475,6 +1559,7 @@ finaliseArgBoxities env fn arity rhs
 
     mk_triple :: Id -> (Type,StrictnessMark,Demand)
     mk_triple bndr | is_cls_arg ty = (ty, NotMarkedStrict, trimBoxity dmd)
+                   | is_bot_fn     = (ty, NotMarkedStrict, unboxDeeplyDmd dmd)
                    | otherwise     = (ty, NotMarkedStrict, dmd)
                    where
                      ty  = idType bndr
@@ -1482,6 +1567,8 @@ finaliseArgBoxities env fn arity rhs
 
     -- is_cls_arg: see Note [Do not unbox class dictionaries]
     is_cls_arg arg_ty = is_inlinable_fn && isClassPred arg_ty
+    -- is_bot_fn:  see Note [Boxity for bottoming functions]
+    is_bot_fn         = div == botDiv
 
     go_args :: Budgets -> [(Type,StrictnessMark,Demand)] -> (Budgets, [Demand])
     go_args bg triples = mapAccumL go_arg bg triples
@@ -1489,8 +1576,11 @@ finaliseArgBoxities env fn arity rhs
     go_arg :: Budgets -> (Type,StrictnessMark,Demand) -> (Budgets, Demand)
     go_arg bg@(MkB bg_top bg_inner) (ty, str_mark, dmd@(n :* _))
       = case wantToUnboxArg False fam_envs ty dmd of
-          DropAbsent   -> (bg,                      dmd)
-          StopUnboxing -> (MkB (bg_top-1) bg_inner, trimBoxity dmd)
+          StopUnboxing
+            | not is_bot_fn
+                -- If bot: Keep deep boxity even though WW won't unbox
+                -- See Note [Boxity for bottoming functions]
+            -> (MkB (bg_top-1) bg_inner, trimBoxity dmd)
 
           Unbox DataConPatContext{dcpc_dc=dc, dcpc_tc_args=tc_args} dmds
             -> (MkB (bg_top-1) final_bg_inner, final_dmd)
@@ -1512,7 +1602,7 @@ finaliseArgBoxities env fn arity rhs
                   = (bg_inner', dmd')
                   | otherwise
                   = (bg_inner, trimBoxity dmd)
-          Unlift -> panic "No unlifting in DmdAnal"
+          _ -> (bg, dmd)
 
     add_demands :: [Demand] -> CoreExpr -> CoreExpr
     -- Attach the demands to the outer lambdas of this expression
diff --git a/compiler/GHC/Types/Demand.hs b/compiler/GHC/Types/Demand.hs
index a27667c21e..98db1c38b8 100644
--- a/compiler/GHC/Types/Demand.hs
+++ b/compiler/GHC/Types/Demand.hs
@@ -19,7 +19,7 @@ module GHC.Types.Demand (
     Boxity(..),
     Card(C_00, C_01, C_0N, C_10, C_11, C_1N), CardNonAbs, CardNonOnce,
     Demand(AbsDmd, BotDmd, (:*)),
-    SubDemand(Prod, Poly), mkProd, viewProd, unboxSubDemand,
+    SubDemand(Prod, Poly), mkProd, viewProd,
     -- ** Algebra
     absDmd, topDmd, botDmd, seqDmd, topSubDmd,
     -- *** Least upper bound
@@ -37,10 +37,13 @@ module GHC.Types.Demand (
     -- *** Demands used in PrimOp signatures
     lazyApply1Dmd, lazyApply2Dmd, strictOnceApply1Dmd, strictManyApply1Dmd,
     -- ** Other @Demand@ operations
-    oneifyCard, oneifyDmd, strictifyDmd, strictifyDictDmd, mkWorkerDemand,
+    oneifyCard, oneifyDmd, strictifyDmd, strictifyDictDmd, lazifyDmd,
     peelCallDmd, peelManyCalls, mkCalledOnceDmd, mkCalledOnceDmds,
+    mkWorkerDemand,
     -- ** Extracting one-shot information
     argOneShots, argsOneShots, saturatedByOneShots,
+    -- ** Manipulating Boxity of a Demand
+    unboxDeeplyDmd,
 
     -- * Demand environments
     DmdEnv, emptyDmdEnv,
@@ -182,7 +185,6 @@ demand analysis in order to determine whether the box of a strict argument is
 always discarded in the function body, in which case we can pass it unboxed
 without risking regressions such as in 'ann' above. But as soon as one use needs
 the box, we want Boxed to win over any Unboxed uses.
-(We don't adhere to that in 'lubBoxity', see Note [lubBoxity and plusBoxity].)
 
 The demand signature (cf. Note [Demand notation]) will say whether it uses
 its arguments boxed or unboxed. Indeed it does so for every sub-component of
@@ -212,8 +214,9 @@ Here are reasons for too much optimism:
    Note [Unboxed demand on function bodies returning small products] derives
    a heuristic from the former Note, pretending that all call sites of a
    function need returned small products Unboxed.
- * Note [lubBoxity and plusBoxity] describes why we optimistically let Unboxed
-   win when combining different case alternatives.
+ * Note [Boxity for bottoming functions] in DmdAnal makes all bottoming
+   functions unbox their arguments, incurring reboxing in code paths that will
+   diverge anyway. In turn we get more unboxing in hot code paths.
 
 Boxity analysis fixes a number of issues: #19871, #19407, #4267, #16859, #18907, #13331
 
@@ -296,7 +299,7 @@ flags (Options f x) = <huge> `seq` f
 and here we won't unbox 'f' because it has 5 fields (which is larger than the
 default -fdmd-unbox-width threshold).
 
-Why not focus on putting Unboxed demands on all recursive function?
+Why not focus on putting Unboxed demands on *all recursive* function?
 Then we'd unbox
 ```
 flags 0 (Options f x) = <huge> `seq` f
@@ -306,62 +309,77 @@ and that seems hardly useful.
 (NB: Similar to 'f' from Note [Preserving Boxity of results is rarely a win],
 but there we only had 2 fields.)
 
-Note [lubBoxity and plusBoxity]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Should 'Boxed' win in 'lubBoxity' and 'plusBoxity'?
-The first intuition is Yes, because that would be the conservative choice:
-Responding 'Boxed' when there's the slightest chance we might need the box means
-we'll never need to rebox a value.
-
-For 'plusBoxity' the choice of 'boxedWins' is clear: When we need a value to be
-Boxed and Unboxed /in the same trace/, then we clearly need it to be Boxed.
-
-But if we chose 'boxedWins' for 'lubBoxity', we'd regress T3586. Smaller example
+What about the Boxity of *fields* of a small, returned box? Consider
 ```
 sumIO :: Int -> Int -> IO Int
-sumIO 0 !z = return z
+sumIO 0 !z = return z     -- What DmdAnal sees: sumIO 0 z s = z `seq` (# s, z #)
 sumIO n !z = sumIO (n-1) (z+n)
 ```
 We really want 'z' to unbox here. Yet its use in the returned unboxed pair
 is fundamentally a Boxed one! CPR would manage to unbox it, but DmdAnal runs
 before that. There is an Unboxed use in the recursive call to 'go' though.
-So we choose 'unboxedWins' for 'lubBoxity' to collect this win.
-
-Choosing 'unboxedWins' is not conservative. There clearly is ample room for
-examples that get worse by our choice. Here's a simple one (from T19871):
-```
-data Huge = H { f1 :: Bool, ... many fields ... }
-update :: Huge -> (Bool, Huge)
-update h@(Huge{f1=True}) = (False, h{f1=False})
-update h                 = (True,  h)
-```
-Here, we decide to unbox 'h' because it's used Unboxed in the first branch.
-
-Another real-life example (c.f. !7182) is in the code compiled for
-GHC.Core.Unify.  Here the two mutually-recursive functions:
-  * `unify_ty` takes its UMEnv argument boxed, but
-  * `uVar` takes its UMEnv argument unboxed.
-So the UMEnv ends up getting reboxed every time around the loop.
+But 'IO Int' returns a small product, and 'Int' is a small product itself.
+So we'll put the RHS of 'sumIO' under sub-demand '!P(L,L!P(L))', indicating that
+*if* we evaluate 'z', we don't need the box later on. And indeed the bang will
+evaluate `z`, so we conclude with a total demand of `1!P(L)` on `z` and unbox
+it.
+
+Unlike for recursive functions, where we can often speed up the loop by
+unboxing at the cost of a bit of reboxing in the base case, the wins for
+non-recursive functions quickly turn into losses when unboxing too deeply.
+That happens in T11545, T18109 and T18174. Therefore, we deeply unbox recursive
+function bodies but only shallowly unbox non-recursive function bodies (governed
+by the max_depth variable).
+
+The implementation is in 'GHC.Core.Opt.DmdAnal.unboxWhenSmall'. It is quite
+vital, guarding for regressions in test cases like #2387, #3586, #16040, #5075
+and #19871.
 
 Note that this is fundamentally working around a phase problem, namely that the
 results of boxity analysis depend on CPR analysis (and vice versa, of course).
+
+Note [unboxedWins]
+~~~~~~~~~~~~~~~~~~
+We used to use '_unboxedWins' below in 'lubBoxity', which was too optimistic.
+
+While it worked around some shortcomings of the phase separation between Boxity
+analysis and CPR analysis, it was a gross hack which caused regressions itself
+that needed all kinds of fixes and workarounds. Examples (from #21119):
+
+  * As #20767 says, L and B were no longer top and bottom of our lattice
+  * In #20746 we unboxed huge Handle types that were never needed boxed in the
+    first place. See Note [deferAfterPreciseException].
+  * It also caused unboxing of huge records where we better shouldn't, for
+    example in T19871.absent.
+  * It became impossible to work with when implementing !7599, mostly due to the
+    chaos that results from #20767.
+
+Conclusion: We should use 'boxedWins' in 'lubBoxity', #21119.
+Fortunately, we could come up with a number of better mechanisms to make up for
+the sometimes huge regressions that would have otherwise incured:
+
+1. A beefed up Note [Unboxed demand on function bodies returning small products]
+   that works recursively fixes most regressions. It's a bit unsound, but
+   pretty well-behaved.
+2. We saw bottoming functions spoil boxity in some less severe cases and
+   countered that with Note [Boxity for bottoming functions].
+
 -}
 
 boxedWins :: Boxity -> Boxity -> Boxity
 boxedWins Unboxed Unboxed = Unboxed
 boxedWins _       !_      = Boxed
 
-unboxedWins :: Boxity -> Boxity -> Boxity
-unboxedWins Boxed Boxed = Boxed
-unboxedWins _     !_    = Unboxed
+_unboxedWins :: Boxity -> Boxity -> Boxity
+-- See Note [unboxedWins]
+_unboxedWins Boxed Boxed = Boxed
+_unboxedWins _     !_    = Unboxed
 
 lubBoxity :: Boxity -> Boxity -> Boxity
 -- See Note [Boxity analysis] for the lattice.
--- See Note [lubBoxity and plusBoxity].
-lubBoxity = unboxedWins
+lubBoxity = boxedWins
 
 plusBoxity :: Boxity -> Boxity -> Boxity
--- See Note [lubBoxity and plusBoxity].
 plusBoxity = boxedWins
 
 {-
@@ -674,11 +692,11 @@ data SubDemand
   = Poly !Boxity !CardNonOnce
   -- ^ Polymorphic demand, the denoted thing is evaluated arbitrarily deep,
   -- with the specified cardinality at every level. The 'Boxity' applies only
-  -- to the outer evaluation context; inner evaluation context can be regarded
-  -- as 'Boxed'. See Note [Boxity in Poly] for why we want it to carry 'Boxity'.
+  -- to the outer evaluation context as well as all inner evaluation context.
+  -- See Note [Boxity in Poly] for why we want it to carry 'Boxity'.
   -- Expands to 'Call' via 'viewCall' and to 'Prod' via 'viewProd'.
   --
-  -- @Poly b n@ is semantically equivalent to @Prod b [n :* Poly Boxed n, ...]@
+  -- @Poly b n@ is semantically equivalent to @Prod b [n :* Poly b n, ...]
   -- or @Call n (Poly Boxed n)@. 'viewCall' and 'viewProd' do these rewrites.
   --
   -- In Note [Demand notation]: @L  === P(L,L,...)@  and @L  === CL(L)@,
@@ -722,27 +740,28 @@ seqSubDmd = Poly Unboxed C_00
 
 -- | The uniform field demand when viewing a 'Poly' as a 'Prod', as in
 -- 'viewProd'.
-polyFieldDmd :: CardNonOnce -> Demand
-polyFieldDmd C_00 = AbsDmd
-polyFieldDmd C_10 = BotDmd
-polyFieldDmd C_0N = topDmd
-polyFieldDmd n    = C_1N :* Poly Boxed C_1N & assertPpr (isCardNonOnce n) (ppr n)
+polyFieldDmd :: Boxity -> CardNonOnce -> Demand
+polyFieldDmd _     C_00 = AbsDmd
+polyFieldDmd _     C_10 = BotDmd
+polyFieldDmd Boxed C_0N = topDmd
+polyFieldDmd b     n    = n :* Poly b n & assertPpr (isCardNonOnce n) (ppr n)
 
 -- | A smart constructor for 'Prod', applying rewrite rules along the semantic
 -- equality @Prod b [n :* Poly Boxed n, ...] === Poly b n@, simplifying to
 -- 'Poly' 'SubDemand's when possible. Examples:
 --
 --   * Rewrites @P(L,L)@ (e.g., arguments @Boxed@, @[L,L]@) to @L@
---   * Rewrites @!P(L,L)@ (e.g., arguments @Unboxed@, @[L,L]@) to @!L@
---   * Does not rewrite @P(1L)@, @P(L!L)@ or @P(L,A)@
+--   * Rewrites @!P(L!L,L!L)@ (e.g., arguments @Unboxed@, @[L!L,L!L]@) to @!L@
+--   * Does not rewrite @P(1L)@, @P(L!L)@, @!P(L)@ or @P(L,A)@
 --
 mkProd :: Boxity -> [Demand] -> SubDemand
 mkProd b ds
   | all (== AbsDmd) ds = Poly b C_00
   | all (== BotDmd) ds = Poly b C_10
-  | dmd@(n :* Poly Boxed m):_ <- ds  -- don't rewrite P(L!L)
-  , n == m                           -- don't rewrite P(1L)
-  , all (== dmd) ds                  -- don't rewrite P(L,A)
+  | dmd@(n :* Poly b2 m):_ <- ds
+  , n == m           -- don't rewrite P(SL)  to S
+  , b == b2          -- don't rewrite P(S!S) to !S
+  , all (== dmd) ds  -- don't rewrite P(L,A) to L
   = Poly b n
   | otherwise          = Prod b ds
 
@@ -756,7 +775,7 @@ viewProd n (Prod b ds)
 -- Note the strict application to replicate: This makes sure we don't allocate
 -- a thunk for it, inlines it and lets case-of-case fire at call sites.
 viewProd n (Poly b card)
-  | let !ds = replicate n $! polyFieldDmd card
+  | let !ds = replicate n $! polyFieldDmd b card
   = Just (b, ds)
 viewProd _ _
   = Nothing
@@ -785,11 +804,17 @@ absDmd = AbsDmd
 botDmd = BotDmd
 seqDmd = C_11 :* seqSubDmd
 
--- | Sets 'Boxity' to 'Unboxed' for non-'Call' sub-demands.
-unboxSubDemand :: SubDemand -> SubDemand
-unboxSubDemand (Poly _ n)  = Poly Unboxed n
-unboxSubDemand (Prod _ ds) = mkProd Unboxed ds
-unboxSubDemand sd@Call{}   = sd
+-- | Sets 'Boxity' to 'Unboxed' for non-'Call' sub-demands and recurses into 'Prod'.
+unboxDeeplySubDmd :: SubDemand -> SubDemand
+unboxDeeplySubDmd (Poly _ n)  = Poly Unboxed n
+unboxDeeplySubDmd (Prod _ ds) = mkProd Unboxed (strictMap unboxDeeplyDmd ds)
+unboxDeeplySubDmd call@Call{} = call
+
+-- | Sets 'Boxity' to 'Unboxed' for the 'Demand', recursing into 'Prod's.
+unboxDeeplyDmd :: Demand -> Demand
+unboxDeeplyDmd AbsDmd   = AbsDmd
+unboxDeeplyDmd BotDmd   = BotDmd
+unboxDeeplyDmd (D n sd) = D n (unboxDeeplySubDmd sd)
 
 -- | Denotes '∪' on 'SubDemand'.
 lubSubDmd :: SubDemand -> SubDemand -> SubDemand
@@ -798,7 +823,7 @@ 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 n2
+  | let !d = polyFieldDmd b2 n2
   = mkProd (lubBoxity b1 b2) (strictMap (lubDmd d) ds1)
 lubSubDmd (Prod b1 ds1) (Prod b2 ds2)
   | equalLength ds1 ds2
@@ -847,7 +872,7 @@ plusSubDmd (Poly Unboxed C_00) d2                  = d2
 plusSubDmd d1                  (Poly Unboxed C_00) = d1
 -- Handle Prod
 plusSubDmd (Prod b1 ds1) (Poly b2 n2)
-  | let !d = polyFieldDmd n2
+  | let !d = polyFieldDmd b2 n2
   = mkProd (plusBoxity b1 b2) (strictMap (plusDmd d) ds1)
 plusSubDmd (Prod b1 ds1) (Prod b2 ds2)
   | equalLength ds1 ds2
@@ -965,6 +990,18 @@ strictifyDictDmd ty (n :* Prod b ds)
       = Nothing
 strictifyDictDmd _  dmd = dmd
 
+-- | Make a 'Demand' lazy, setting all lower bounds (outside 'Call's) to 0.
+lazifyDmd :: Demand -> Demand
+lazifyDmd AbsDmd    = AbsDmd
+lazifyDmd BotDmd    = AbsDmd
+lazifyDmd (n :* sd) = multCard C_01 n :* lazifySubDmd sd
+
+-- | Make a 'SubDemand' lazy, setting all lower bounds (outside 'Call's) to 0.
+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
+
 -- | Wraps the 'SubDemand' with a one-shot call demand: @d@ -> @C1(d)@.
 mkCalledOnceDmd :: SubDemand -> SubDemand
 mkCalledOnceDmd sd = mkCall C_11 sd
@@ -1109,8 +1146,8 @@ To support Note [Boxity analysis], it makes sense that 'Prod' carries a
 express an unboxing demand?
 
 'botSubDmd' (B) needs to be the bottom of the lattice, so it needs to be an
-Unboxed demand. Similarly, 'seqSubDmd' (A) is an Unboxed demand.
-So why not say that Polys with absent cardinalities have Unboxed boxity?
+Unboxed demand (and deeply, at that). Similarly, 'seqSubDmd' (A) is an Unboxed
+demand. So why not say that Polys with absent cardinalities have Unboxed boxity?
 That doesn't work, because we also need the boxed equivalents. Here's an example
 for A (function 'absent' in T19871):
 ```
@@ -1124,7 +1161,6 @@ g a = a `seq` f a True
 h True  p       = g p -- SA on p (inherited from g)
 h False p@(x,y) = x+y -- S!P(1!L,1!L) on p
 ```
-(Caveat: Since Unboxed wins in lubBoxity, we'll unbox here anyway.)
 If A is treated as Unboxed, we get reboxing in the call site to 'g'.
 So we obviously would need a Boxed variant of A. Rather than introducing a lot
 of special cases, we just carry the Boxity in 'Poly'. Plus, we could most likely
@@ -1573,12 +1609,10 @@ isTopDmdType :: DmdType -> Bool
 isTopDmdType (DmdType env args div)
   = div == topDiv && null args && isEmptyVarEnv env
 
-{-   Unused
 -- | The demand type of an unspecified expression that is guaranteed to
 -- throw a (precise or imprecise) exception or diverge.
 exnDmdType :: DmdType
 exnDmdType = DmdType emptyDmdEnv [] exnDiv
--}
 
 dmdTypeDepth :: DmdType -> Arity
 dmdTypeDepth = length . dt_args
@@ -1648,23 +1682,7 @@ findIdDemand (DmdType fv _ res) id
 -- Why not 'nopDmdType'? Because then the result of 'e' can never be 'exnDiv'!
 -- That means failure to drop dead-ends, see #18086.
 deferAfterPreciseException :: DmdType -> DmdType
--- deferAfterPreciseException = lubDmdType exnDmdType
-deferAfterPreciseException (DmdType fvs ds r)
-  = DmdType (mapVarEnv defer fvs)
-            (map defer ds)
-            (r `lubDivergence` ExnOrDiv)
-  where
-    defer :: Demand -> Demand
-    defer AbsDmd = AbsDmd
-    defer BotDmd = AbsDmd
-    defer (D n sd) = lubCard n C_00 :* lubSubDmd sd (Poly Boxed C_00)
-
-    -- Roughly:  defer d = d `lubDmd` D C_00 (Poly Boxed C_00)
-    -- It is very important that we `lub` with `Boxed`; see
-    --     Note [deferAfterPreciseException]
-    -- But that formulation fails the assert in :*,
-    --     because (D C_00 (Poly Boxed C_00)) is not a legal demand
-    -- So we write defer out more explicitly here
+deferAfterPreciseException = lubDmdType exnDmdType
 
 -- | See 'keepAliveDmdEnv'.
 keepAliveDmdType :: DmdType -> VarSet -> DmdType
@@ -1686,19 +1704,19 @@ That is, the I/O operation might throw an exception, so that 'rhs' never
 gets reached.  For example, we don't want to be strict in the strict free
 variables of 'rhs'.
 
-So roughly speaking:
+So we have the simple definition
   deferAfterPreciseException = lubDmdType (DmdType emptyDmdEnv [] exnDiv)
 
-But that doesn't work quite right for boxity becasuse
+Historically, when we had `lubBoxity = _unboxedWins` (see Note [unboxedWins]),
+we had a more complicated definition for deferAfterPreciseException to make sure
+it preserved boxity in its argument. That was needed for code like
    case <I/O operation> of
       (# s', r) -> f x
 
-uses `x` *boxed*.  If we `lub` it with `(DmdType emptyDmdEnv [] exnDiv)`
-we'll get an *unboxed* demand on `x`, which led to #20746.  There is
-a fuller example in that ticket.
-
-TL;DR: deferAfterPreciseException is very careful to preserve boxity
-in its argument.
+which uses `x` *boxed*. If we `lub`bed it with `(DmdType emptyDmdEnv [] exnDiv)`
+we'd get an *unboxed* demand on `x` (because we let Unboxed win), which led to
+#20746.
+Nowadays with `lubBoxity = boxedWins` we don't need the complicated definition.
 
 Note [Demand type Divergence]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/testsuite/tests/arityanal/should_compile/Arity04.stderr b/testsuite/tests/arityanal/should_compile/Arity04.stderr
index 2adcacff39..cd50e21662 100644
--- a/testsuite/tests/arityanal/should_compile/Arity04.stderr
+++ b/testsuite/tests/arityanal/should_compile/Arity04.stderr
@@ -1,47 +1,40 @@
 
 ==================== Tidy Core ====================
-Result size of Tidy Core = {terms: 39, types: 24, coercions: 0, joins: 0/0}
+Result size of Tidy Core = {terms: 34, types: 17, coercions: 0, joins: 0/0}
 
 -- RHS size: {terms: 8, types: 3, coercions: 0, joins: 0/0}
 f4g :: Int -> Int
 [GblId,
  Arity=1,
- Str=<1!P(L)>,
+ Str=<1!L>,
  Cpr=1,
  Unf=Unf{Src=InlineStable, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=ALWAYS_IF(arity=1,unsat_ok=True,boring_ok=False)
          Tmpl= \ (y [Occ=Once1!] :: Int) -> case y of { GHC.Types.I# x [Occ=Once1] -> GHC.Types.I# (GHC.Prim.+# x 1#) }}]
 f4g = \ (y :: Int) -> case y of { GHC.Types.I# x -> GHC.Types.I# (GHC.Prim.+# x 1#) }
 
--- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
-lvl :: Int
-[GblId, Unf=OtherCon []]
-lvl = GHC.Types.I# 0#
-
 Rec {
--- RHS size: {terms: 13, types: 4, coercions: 0, joins: 0/0}
-F4.$wf4h [InlPrag=[2], Occ=LoopBreaker] :: (Int -> Int) -> GHC.Prim.Int# -> Int
-[GblId, Arity=2, Str=<1C1(L)><1L>, Unf=OtherCon []]
-F4.$wf4h
-  = \ (f :: Int -> Int) (ww :: GHC.Prim.Int#) ->
-      case ww of wild {
-        __DEFAULT -> F4.$wf4h f (GHC.Prim.-# wild 1#);
-        0# -> f lvl
+-- RHS size: {terms: 17, types: 6, coercions: 0, joins: 0/0}
+f4h [Occ=LoopBreaker] :: (Int -> Int) -> Int -> Int
+[GblId, Arity=2, Str=<1C1(L)><1P(SL)>, Unf=OtherCon []]
+f4h
+  = \ (f :: Int -> Int) (x :: Int) ->
+      case x of wild { GHC.Types.I# x1 ->
+      case x1 of wild1 {
+        __DEFAULT -> f4h f (GHC.Types.I# (GHC.Prim.-# wild1 1#));
+        0# -> f wild
+      }
       }
 end Rec }
 
--- RHS size: {terms: 8, types: 5, coercions: 0, joins: 0/0}
-f4h [InlPrag=[2]] :: (Int -> Int) -> Int -> Int
-[GblId,
- Arity=2,
- Str=<1C1(L)><1!P(1L)>,
- Unf=Unf{Src=InlineStable, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=ALWAYS_IF(arity=2,unsat_ok=True,boring_ok=False)
-         Tmpl= \ (f [Occ=Once1] :: Int -> Int) (x [Occ=Once1!] :: Int) -> case x of { GHC.Types.I# ww [Occ=Once1] -> F4.$wf4h f ww }}]
-f4h = \ (f :: Int -> Int) (x :: Int) -> case x of { GHC.Types.I# ww -> F4.$wf4h f ww }
+-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
+F4.f1 :: Int
+[GblId, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 10}]
+F4.f1 = GHC.Types.I# 9#
 
 -- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
 f4 :: Int
 [GblId, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=False, ConLike=False, WorkFree=False, Expandable=False, Guidance=IF_ARGS [] 30 0}]
-f4 = F4.$wf4h f4g 9#
+f4 = f4h f4g F4.f1
 
 
 
diff --git a/testsuite/tests/arityanal/should_compile/T18793.stderr b/testsuite/tests/arityanal/should_compile/T18793.stderr
index 6de3dea08a..13ca1c65f5 100644
--- a/testsuite/tests/arityanal/should_compile/T18793.stderr
+++ b/testsuite/tests/arityanal/should_compile/T18793.stderr
@@ -32,7 +32,7 @@ end Rec }
 T18793.f_go1 [InlPrag=[2]] :: [Int] -> Int -> Int
 [GblId,
  Arity=2,
- Str=<1L><1!L>,
+ Str=<1L><1!P(L)>,
  Cpr=1,
  Unf=Unf{Src=InlineStable, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=ALWAYS_IF(arity=2,unsat_ok=True,boring_ok=False)
          Tmpl= \ (ds [Occ=Once1] :: [Int]) (eta [Occ=Once1!] :: Int) -> case eta of { GHC.Types.I# ww [Occ=Once1] -> case T18793.$wgo1 ds ww of ww1 [Occ=Once1] { __DEFAULT -> GHC.Types.I# ww1 } }}]
@@ -50,7 +50,7 @@ T18793.f1 = stuff T18793.f2
 
 -- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
 f :: Int -> Int
-[GblId, Arity=1, Str=<1!L>, Cpr=1, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 20 60}]
+[GblId, Arity=1, Str=<1!P(L)>, Cpr=1, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 20 60}]
 f = T18793.f_go1 T18793.f1
 
 
diff --git a/testsuite/tests/cpranal/should_compile/T18174.hs b/testsuite/tests/cpranal/should_compile/T18174.hs
index bf1c02982c..69ca25a19e 100644
--- a/testsuite/tests/cpranal/should_compile/T18174.hs
+++ b/testsuite/tests/cpranal/should_compile/T18174.hs
@@ -41,7 +41,7 @@ dataConWrapper :: (Int, Int) -> Int -> (T, Int)
 dataConWrapper p x = (MkT x p, x+1)
 {-# NOINLINE dataConWrapper #-}
 
--- | Should not unbox the second component, because 'x' won't be available
+-- | Should not unbox the second component, because 'y' won't be available
 -- unboxed. It terminates, though.
 strictField :: T -> (Int, (Int, Int))
 strictField (MkT x y) = (x, y)
diff --git a/testsuite/tests/cpranal/sigs/RecDataConCPR.hs b/testsuite/tests/cpranal/sigs/RecDataConCPR.hs
index c26ae1264f..d934509448 100644
--- a/testsuite/tests/cpranal/sigs/RecDataConCPR.hs
+++ b/testsuite/tests/cpranal/sigs/RecDataConCPR.hs
@@ -95,7 +95,7 @@ type instance E (a,b) = (E a, E b)
 type instance E Char = Blub
 data Blah = Blah (E (Int, (Int, Int))) -- NonRec
 data Blub = Blub (E (Char, Int))       -- Rec
-data Blub2 = Blub2 (E (Bool, Int))       -- Rec, because stuck
+data Blub2 = Blub2 (E (Bool, Int))     -- Unsure, because stuck
 
 blah :: Int -> Blah
 blah n = Blah (chr n, (chr (n+1), chr (n+2)))
@@ -110,8 +110,8 @@ blub2 n = Blub2 (undefined :: E Bool, chr n)
 data BootNonRec1 = BootNonRec1 BootNonRec2 -- in RecDataConCPRa.hs-boot
 data BootRec1 = BootRec1 BootRec2 -- in RecDataConCPRa.hs-boot, recurses back
 
-bootNonRec :: Int -> BootNonRec2 -> BootNonRec1 -- Nothing, thus like NonRec
+bootNonRec :: Int -> BootNonRec2 -> BootNonRec1 -- Unsure, thus like NonRec
 bootNonRec x b2 = BootNonRec1 b2
 
-bootRec :: Int -> BootRec2 -> BootRec1 -- Nothing, thus like NonRec
+bootRec :: Int -> BootRec2 -> BootRec1 -- Unsure, thus like NonRec
 bootRec x b2 = BootRec1 b2
diff --git a/testsuite/tests/numeric/should_compile/T7116.stdout b/testsuite/tests/numeric/should_compile/T7116.stdout
index 3c30cf2e8b..90aeda659d 100644
--- a/testsuite/tests/numeric/should_compile/T7116.stdout
+++ b/testsuite/tests/numeric/should_compile/T7116.stdout
@@ -43,7 +43,7 @@ T7116.$trModule
 dr :: Double -> Double
 [GblId,
  Arity=1,
- Str=<1!L>,
+ Str=<1!P(L)>,
  Cpr=1,
  Unf=Unf{Src=InlineStable, TopLvl=True, Value=True, ConLike=True,
          WorkFree=True, Expandable=True,
@@ -60,7 +60,7 @@ dr
 dl :: Double -> Double
 [GblId,
  Arity=1,
- Str=<1!L>,
+ Str=<1!P(L)>,
  Cpr=1,
  Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
          WorkFree=True, Expandable=True,
@@ -71,7 +71,7 @@ dl = dr
 fr :: Float -> Float
 [GblId,
  Arity=1,
- Str=<1!L>,
+ Str=<1!P(L)>,
  Cpr=1,
  Unf=Unf{Src=InlineStable, TopLvl=True, Value=True, ConLike=True,
          WorkFree=True, Expandable=True,
@@ -90,7 +90,7 @@ fr
 fl :: Float -> Float
 [GblId,
  Arity=1,
- Str=<1!L>,
+ Str=<1!P(L)>,
  Cpr=1,
  Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
          WorkFree=True, Expandable=True,
diff --git a/testsuite/tests/simplCore/should_compile/T13143.stderr b/testsuite/tests/simplCore/should_compile/T13143.stderr
index a2c77f86ea..5ca8a9a503 100644
--- a/testsuite/tests/simplCore/should_compile/T13143.stderr
+++ b/testsuite/tests/simplCore/should_compile/T13143.stderr
@@ -98,7 +98,7 @@ end Rec }
 g [InlPrag=[2]] :: Bool -> Bool -> Int -> Int
 [GblId,
  Arity=3,
- Str=<1L><1L><1!L>,
+ Str=<1L><1L><1!P(L)>,
  Cpr=1,
  Unf=Unf{Src=InlineStable, TopLvl=True, Value=True, ConLike=True,
          WorkFree=True, Expandable=True,
diff --git a/testsuite/tests/simplCore/should_compile/T13543.stderr b/testsuite/tests/simplCore/should_compile/T13543.stderr
index 485f6fea41..94c0b76bfc 100644
--- a/testsuite/tests/simplCore/should_compile/T13543.stderr
+++ b/testsuite/tests/simplCore/should_compile/T13543.stderr
@@ -1,8 +1,8 @@
 
 ==================== Strictness signatures ====================
 Foo.$trModule:
-Foo.f: <1!P(1L)><1!L><1!L>
-Foo.g: <1!P(1!L,1!L)>
+Foo.f: <1!P(1L)><1!P(L)><1!P(L)>
+Foo.g: <1!P(1!P(L),1!P(L))>
 
 
 
@@ -15,7 +15,7 @@ Foo.g: 1
 
 ==================== Strictness signatures ====================
 Foo.$trModule:
-Foo.f: <1!P(1L)><1!L><1!L>
-Foo.g: <1!P(1!L,1!L)>
+Foo.f: <1!P(1L)><1!P(L)><1!P(L)>
+Foo.g: <1!P(1!P(L),1!P(L))>
 
 
diff --git a/testsuite/tests/simplCore/should_compile/T15056.stderr b/testsuite/tests/simplCore/should_compile/T15056.stderr
index 1ca9102d70..126bc10057 100644
--- a/testsuite/tests/simplCore/should_compile/T15056.stderr
+++ b/testsuite/tests/simplCore/should_compile/T15056.stderr
@@ -2,9 +2,7 @@ Rule fired: Class op - (BUILTIN)
 Rule fired: Class op + (BUILTIN)
 Rule fired: Class op + (BUILTIN)
 Rule fired: Class op + (BUILTIN)
-Rule fired: Class op enumFromTo (BUILTIN)
-Rule fired: Class op foldr (BUILTIN)
-Rule fired: Class op foldr (BUILTIN)
 Rule fired: +# (BUILTIN)
 Rule fired: Class op foldr (BUILTIN)
+Rule fired: Class op enumFromTo (BUILTIN)
 Rule fired: fold/build (GHC.Base)
diff --git a/testsuite/tests/simplCore/should_compile/T20103.stderr b/testsuite/tests/simplCore/should_compile/T20103.stderr
index f89fe3a8f0..7eea0f5fde 100644
--- a/testsuite/tests/simplCore/should_compile/T20103.stderr
+++ b/testsuite/tests/simplCore/should_compile/T20103.stderr
@@ -11,7 +11,7 @@ lvl = GHC.Types.I# 28#
 -- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
 lvl1 :: Int
 [GblId, Unf=OtherCon []]
-lvl1 = GHC.Types.I# 8#
+lvl1 = GHC.Types.I# 7#
 
 -- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
 lvl2 :: Int
@@ -75,7 +75,7 @@ lvl10 = GHC.Types.I# 12#
 -- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
 lvl11 :: Int
 [GblId, Unf=OtherCon []]
-lvl11 = GHC.Types.I# 7#
+lvl11 = GHC.Types.I# 8#
 
 -- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
 lvl12 :: Int
@@ -100,7 +100,7 @@ lvl15 = GHC.CString.unpackCString# lvl14
 
 -- RHS size: {terms: 6, types: 5, coercions: 4, joins: 0/0}
 lvl16 :: CallStack -> ([Char], SrcLoc)
-[GblId, Arity=1, Str=<S>b, Cpr=b, Unf=OtherCon []]
+[GblId, Arity=1, Str=<S!S>b, Cpr=b, Unf=OtherCon []]
 lvl16
   = \ (wild1 :: CallStack) ->
       GHC.List.head1
@@ -115,7 +115,7 @@ T20103.$wfoo [InlPrag=[2], Occ=LoopBreaker]
   :: HasCallStack => GHC.Prim.Int# -> GHC.Prim.Int#
 [GblId[StrictWorker([!, ~])],
  Arity=2,
- Str=<1L><1L>,
+ Str=<SL><1L>,
  Unf=OtherCon []]
 T20103.$wfoo
   = \ ($dIP
diff --git a/testsuite/tests/simplCore/should_compile/T3772.stdout b/testsuite/tests/simplCore/should_compile/T3772.stdout
index c63beeca95..dde2503f31 100644
--- a/testsuite/tests/simplCore/should_compile/T3772.stdout
+++ b/testsuite/tests/simplCore/should_compile/T3772.stdout
@@ -65,7 +65,7 @@ T3772.$wfoo
 foo [InlPrag=[final]] :: Int -> ()
 [GblId,
  Arity=1,
- Str=<1!L>,
+ Str=<1!P(L)>,
  Cpr=1,
  Unf=Unf{Src=InlineStable, TopLvl=True, Value=True, ConLike=True,
          WorkFree=True, Expandable=True,
diff --git a/testsuite/tests/simplCore/should_compile/T4930.stderr b/testsuite/tests/simplCore/should_compile/T4930.stderr
index b8d14764ce..413f892942 100644
--- a/testsuite/tests/simplCore/should_compile/T4930.stderr
+++ b/testsuite/tests/simplCore/should_compile/T4930.stderr
@@ -56,7 +56,7 @@ end Rec }
 foo [InlPrag=[2]] :: Int -> Int
 [GblId,
  Arity=1,
- Str=<1!L>,
+ Str=<1!P(L)>,
  Cpr=1,
  Unf=Unf{Src=InlineStable, TopLvl=True, Value=True, ConLike=True,
          WorkFree=True, Expandable=True,
diff --git a/testsuite/tests/simplCore/should_compile/spec-inline.stderr b/testsuite/tests/simplCore/should_compile/spec-inline.stderr
index 6ecc7340a2..7b99cc01ff 100644
--- a/testsuite/tests/simplCore/should_compile/spec-inline.stderr
+++ b/testsuite/tests/simplCore/should_compile/spec-inline.stderr
@@ -147,7 +147,7 @@ Roman.foo1 = GHC.Maybe.Just @Int Roman.foo2
 foo :: Int -> Int
 [GblId,
  Arity=1,
- Str=<1!L>,
+ Str=<1!P(L)>,
  Cpr=1,
  Unf=Unf{Src=InlineStable, TopLvl=True, Value=True, ConLike=True,
          WorkFree=True, Expandable=True,
diff --git a/testsuite/tests/stranal/should_compile/T18894.stderr b/testsuite/tests/stranal/should_compile/T18894.stderr
index 55fbd59939..ba4a213e4c 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!L,1!L)))]
+g2 [InlPrag=NOINLINE, Dmd=LCL(C1(!P(M!P(L),1!P(L))))]
   :: Int -> Int -> (Int, Int)
 [LclId,
  Arity=2,
@@ -56,7 +56,7 @@ g2 [InlPrag=NOINLINE, Dmd=LCL(C1(!P(M!L,1!L)))]
 g2
   = \ (m :: Int) (ds [Dmd=1!P(1L)] :: Int) ->
       case ds of { GHC.Types.I# ds [Dmd=1L] ->
-      case ds of ds [Dmd=M!L] {
+      case ds of ds [Dmd=ML] {
         __DEFAULT ->
           (case m of { GHC.Types.I# y -> GHC.Types.I# (GHC.Prim.*# 2# y) },
            case ds of wild {
@@ -102,19 +102,19 @@ lvl = GHC.Types.I# 0#
 h2 :: Int -> Int
 [LclIdX,
  Arity=1,
- Str=<1!P(SL)>,
+ Str=<1P(SL)>,
  Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
          WorkFree=True, Expandable=True, Guidance=IF_ARGS [20] 162 10}]
 h2
-  = \ (ds [Dmd=1!P(SL)] :: Int) ->
-      case ds of wild [Dmd=L!L] { GHC.Types.I# ds [Dmd=SL] ->
-      case ds of ds [Dmd=L!L] {
+  = \ (ds [Dmd=1P(SL)] :: Int) ->
+      case ds of wild { GHC.Types.I# ds [Dmd=SL] ->
+      case ds of ds {
         __DEFAULT ->
           case GHC.Prim.remInt# ds 2# of {
             __DEFAULT ->
-              case g2 wild lvl of { (ds1 [Dmd=A], y [Dmd=1!L]) -> y };
+              case g2 wild lvl of { (ds1 [Dmd=A], y [Dmd=1!P(L)]) -> y };
             0# ->
-              case g2 lvl wild of { (x [Dmd=1!L], ds [Dmd=1!L]) ->
+              case g2 lvl wild of { (x [Dmd=1!P(L)], ds [Dmd=1!P(L)]) ->
               case x of { GHC.Types.I# x ->
               case ds of { GHC.Types.I# y -> GHC.Types.I# (GHC.Prim.+# x y) }
               }
@@ -146,7 +146,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,L!L))] :: Int -> (Int, Int)
+g1 [InlPrag=NOINLINE, Dmd=LCL(!P(L,L))] :: Int -> (Int, Int)
 [LclId,
  Arity=1,
  Str=<1!P(1L)>,
@@ -155,7 +155,7 @@ g1 [InlPrag=NOINLINE, Dmd=LCL(!P(L!L,L!L))] :: Int -> (Int, Int)
 g1
   = \ (ds [Dmd=1!P(1L)] :: Int) ->
       case ds of { GHC.Types.I# ds [Dmd=1L] ->
-      case ds of ds [Dmd=L!L] {
+      case ds of ds {
         __DEFAULT ->
           (GHC.Types.I# (GHC.Prim.*# 2# ds),
            case ds of wild {
@@ -199,16 +199,16 @@ 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(M!L)] { GHC.Types.I# ds [Dmd=SL] ->
+      case ds of wild [Dmd=M!P(ML)] { GHC.Types.I# ds [Dmd=SL] ->
       case ds of {
         __DEFAULT ->
-          case g1 wild of { (x [Dmd=1!L], ds [Dmd=1!L]) ->
+          case g1 wild of { (x [Dmd=1!P(L)], ds [Dmd=1!P(L)]) ->
           case x of { GHC.Types.I# x ->
           case ds of { GHC.Types.I# y -> GHC.Types.I# (GHC.Prim.+# x y) }
           }
           };
         1# -> lvl;
-        2# -> case lvl of { (ds1 [Dmd=A], y [Dmd=1!L]) -> y }
+        2# -> case lvl of { (ds1 [Dmd=A], y [Dmd=1!P(L)]) -> y }
       }
       }
 
@@ -217,7 +217,7 @@ h1
 
 ==================== Demand analysis ====================
 Result size of Demand analysis
-  = {terms: 176, types: 114, coercions: 0, joins: 0/2}
+  = {terms: 171, types: 111, coercions: 0, joins: 0/2}
 
 -- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
 $trModule :: GHC.Prim.Addr#
@@ -262,7 +262,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!L,1!L)))]
+$wg2 [InlPrag=NOINLINE, Dmd=LCL(C1(!P(M!P(L),1!P(L))))]
   :: Int -> GHC.Prim.Int# -> (# Int, Int #)
 [LclId,
  Arity=2,
@@ -271,7 +271,7 @@ $wg2 [InlPrag=NOINLINE, Dmd=LCL(C1(!P(M!L,1!L)))]
          WorkFree=True, Expandable=True, Guidance=IF_ARGS [20 30] 76 20}]
 $wg2
   = \ (m :: Int) (ww [Dmd=1L] :: GHC.Prim.Int#) ->
-      case ww of ds [Dmd=M!L] {
+      case ww of ds [Dmd=ML] {
         __DEFAULT ->
           (# case m of { GHC.Types.I# y -> GHC.Types.I# (GHC.Prim.*# 2# y) },
              case ds of wild {
@@ -298,25 +298,23 @@ lvl :: Int
          WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 10}]
 lvl = GHC.Types.I# 2#
 
--- RHS size: {terms: 34, types: 21, coercions: 0, joins: 0/0}
-$wh2 [InlPrag=[2], Dmd=LCL(!L)] :: GHC.Prim.Int# -> Int
-[LclId,
+-- RHS size: {terms: 36, types: 23, coercions: 0, joins: 0/0}
+h2 :: Int -> Int
+[LclIdX,
  Arity=1,
- Str=<1L>,
+ Str=<1P(SL)>,
  Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
-         WorkFree=True, Expandable=True, Guidance=IF_ARGS [30] 162 10}]
-$wh2
-  = \ (ww [Dmd=1L] :: GHC.Prim.Int#) ->
-      case ww of ds [Dmd=L!L] {
+         WorkFree=True, Expandable=True, Guidance=IF_ARGS [20] 162 10}]
+h2
+  = \ (ds [Dmd=1P(SL)] :: Int) ->
+      case ds of wild { GHC.Types.I# ds [Dmd=SL] ->
+      case ds of ds {
         __DEFAULT ->
           case GHC.Prim.remInt# ds 2# of {
             __DEFAULT ->
-              case $wg2 (GHC.Types.I# ds) 2# of
-              { (# ww [Dmd=A], ww [Dmd=1!L] #) ->
-              ww
-              };
+              case $wg2 wild 2# of { (# ww [Dmd=A], ww [Dmd=1!P(L)] #) -> ww };
             0# ->
-              case $wg2 lvl ds of { (# ww [Dmd=1!L], ww [Dmd=1!L] #) ->
+              case $wg2 lvl ds of { (# ww [Dmd=1!P(L)], ww [Dmd=1!P(L)] #) ->
               case ww of { GHC.Types.I# x ->
               case ww of { GHC.Types.I# y -> GHC.Types.I# (GHC.Prim.+# x y) }
               }
@@ -324,23 +322,10 @@ $wh2
           };
         1# -> lvl
       }
-
--- RHS size: {terms: 6, types: 3, coercions: 0, joins: 0/0}
-h2 [InlPrag=[2]] :: Int -> Int
-[LclIdX,
- Arity=1,
- Str=<1!P(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)
-         Tmpl= \ (ds [Occ=Once1!, Dmd=S!P(SL)] :: Int) ->
-                 case ds of { GHC.Types.I# ww [Occ=Once1, Dmd=SL] -> $wh2 ww }}]
-h2
-  = \ (ds [Dmd=1!P(1L)] :: Int) ->
-      case ds of { GHC.Types.I# ww [Dmd=1L] -> $wh2 ww }
+      }
 
 -- RHS size: {terms: 34, types: 14, coercions: 0, joins: 0/1}
-$wg1 [InlPrag=NOINLINE, Dmd=LCL(!P(L,L!L))]
+$wg1 [InlPrag=NOINLINE, Dmd=LCL(!P(L,L))]
   :: GHC.Prim.Int# -> (# GHC.Prim.Int#, Int #)
 [LclId,
  Arity=1,
@@ -349,7 +334,7 @@ $wg1 [InlPrag=NOINLINE, Dmd=LCL(!P(L,L!L))]
          WorkFree=True, Expandable=True, Guidance=IF_ARGS [30] 56 20}]
 $wg1
   = \ (ww [Dmd=1L] :: GHC.Prim.Int#) ->
-      case ww of ds [Dmd=L!L] {
+      case ww of ds {
         __DEFAULT ->
           (# GHC.Prim.*# 2# ds,
              case ds of wild {
@@ -377,7 +362,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(!L)] :: GHC.Prim.Int# -> Int
+$wh1 [InlPrag=[2], Dmd=LCL(!P(L))] :: GHC.Prim.Int# -> Int
 [LclId,
  Arity=1,
  Str=<1L>,
@@ -385,13 +370,13 @@ $wh1 [InlPrag=[2], Dmd=LCL(!L)] :: GHC.Prim.Int# -> Int
          WorkFree=True, Expandable=True, Guidance=IF_ARGS [50] 91 10}]
 $wh1
   = \ (ww [Dmd=1L] :: GHC.Prim.Int#) ->
-      case ww of ds [Dmd=M!L] {
+      case ww of ds [Dmd=ML] {
         __DEFAULT ->
-          case $wg1 ds of { (# ww, ww [Dmd=1!L] #) ->
+          case $wg1 ds of { (# ww, ww [Dmd=1!P(L)] #) ->
           case ww of { GHC.Types.I# y -> GHC.Types.I# (GHC.Prim.+# ww y) }
           };
         1# -> lvl;
-        2# -> case lvl of { (ds1 [Dmd=A], y [Dmd=1!L]) -> y }
+        2# -> case lvl of { (ds1 [Dmd=A], y [Dmd=1!P(L)]) -> y }
       }
 
 -- RHS size: {terms: 6, types: 3, coercions: 0, joins: 0/0}
diff --git a/testsuite/tests/stranal/should_compile/T18903.stderr b/testsuite/tests/stranal/should_compile/T18903.stderr
index 8c0427b235..e44edd8507 100644
--- a/testsuite/tests/stranal/should_compile/T18903.stderr
+++ b/testsuite/tests/stranal/should_compile/T18903.stderr
@@ -50,13 +50,13 @@ T18903.h1 = GHC.Types.I# 0#
 h :: Int -> Int
 [GblId,
  Arity=1,
- Str=<1!P(SL)>,
+ Str=<1P(SL)>,
  Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
          WorkFree=True, Expandable=True, Guidance=IF_ARGS [20] 217 10}]
 h = \ (m :: Int) ->
       case m of wild { GHC.Types.I# ds ->
       let {
-        $wg [InlPrag=NOINLINE, Dmd=MCM(!P(M!L,1!L))]
+        $wg [InlPrag=NOINLINE, Dmd=MCM(!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/should_compile/T20746.stderr b/testsuite/tests/stranal/should_compile/T20746.stderr
deleted file mode 100644
index 6e7f56f625..0000000000
--- a/testsuite/tests/stranal/should_compile/T20746.stderr
+++ /dev/null
@@ -1,133 +0,0 @@
-
-==================== Tidy Core ====================
-Result size of Tidy Core
-  = {terms: 70, types: 113, coercions: 18, joins: 0/2}
-
--- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
-Foo.$trModule4 :: GHC.Prim.Addr#
-[GblId,
- Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
-         WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 20 0}]
-Foo.$trModule4 = "main"#
-
--- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
-Foo.$trModule3 :: GHC.Types.TrName
-[GblId,
- Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
-         WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 10}]
-Foo.$trModule3 = GHC.Types.TrNameS Foo.$trModule4
-
--- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
-Foo.$trModule2 :: GHC.Prim.Addr#
-[GblId,
- Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
-         WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 20 0}]
-Foo.$trModule2 = "Foo"#
-
--- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
-Foo.$trModule1 :: GHC.Types.TrName
-[GblId,
- Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
-         WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 10}]
-Foo.$trModule1 = GHC.Types.TrNameS Foo.$trModule2
-
--- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
-Foo.$trModule :: GHC.Types.Module
-[GblId,
- Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
-         WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 10}]
-Foo.$trModule = GHC.Types.Module Foo.$trModule3 Foo.$trModule1
-
--- RHS size: {terms: 5, types: 8, coercions: 0, joins: 0/0}
-Foo.f1 [InlPrag=NOINLINE]
-  :: Int
-     -> GHC.Prim.State# GHC.Prim.RealWorld
-     -> (# GHC.Prim.State# GHC.Prim.RealWorld, Int #)
-[GblId, Arity=2, Str=<L><L>, Cpr=1, Unf=OtherCon []]
-Foo.f1
-  = \ (n :: Int)
-      (s [OS=OneShot] :: GHC.Prim.State# GHC.Prim.RealWorld) ->
-      (# s, n #)
-
--- RHS size: {terms: 1, types: 0, coercions: 6, joins: 0/0}
-foogle [InlPrag=[final]] :: Int -> IO Int
-[GblId,
- Arity=2,
- Str=<L><L>,
- Cpr=1,
- Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
-         WorkFree=True, Expandable=True,
-         Guidance=ALWAYS_IF(arity=0,unsat_ok=True,boring_ok=True)}]
-foogle
-  = Foo.f1
-    `cast` (<Int>_R %<'Many>_N ->_R Sym (GHC.Types.N:IO[0] <Int>_R)
-            :: (Int
-                -> GHC.Prim.State# GHC.Prim.RealWorld
-                -> (# GHC.Prim.State# GHC.Prim.RealWorld, Int #))
-               ~R# (Int -> IO Int))
-
--- RHS size: {terms: 35, types: 38, coercions: 12, joins: 0/2}
-Foo.$wf [InlPrag=[2]]
-  :: forall {a}. Show a => a -> (# Int -> IO Int, Int -> IO Int #)
-[GblId,
- Arity=2,
- Str=<MP(A,MCM(L),A)><L>,
- Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
-         WorkFree=True, Expandable=True, Guidance=IF_ARGS [30 0] 181 10}]
-Foo.$wf
-  = \ (@a) ($dShow :: Show a) (x :: a) ->
-      let {
-        lvl :: String
-        [LclId]
-        lvl = show @a $dShow x } in
-      let {
-        g :: Int
-             -> GHC.Prim.State# GHC.Prim.RealWorld
-             -> (# GHC.Prim.State# GHC.Prim.RealWorld, Int #)
-        [LclId, Arity=2, Str=<1L><L>, Unf=OtherCon []]
-        g = \ (y :: Int) (s :: GHC.Prim.State# GHC.Prim.RealWorld) ->
-              case y of wild { GHC.Types.I# x1 ->
-              case GHC.Prim.># x1 2# of {
-                __DEFAULT -> Foo.f1 wild s;
-                1# ->
-                  case GHC.IO.Handle.Text.hPutStr2
-                         GHC.IO.Handle.FD.stdout lvl GHC.Types.True s
-                  of
-                  { (# ipv, ipv1 #) ->
-                  Foo.f1 wild ipv
-                  }
-              }
-              } } in
-      (# g
-         `cast` (<Int>_R %<'Many>_N ->_R Sym (GHC.Types.N:IO[0] <Int>_R)
-                 :: (Int
-                     -> GHC.Prim.State# GHC.Prim.RealWorld
-                     -> (# GHC.Prim.State# GHC.Prim.RealWorld, Int #))
-                    ~R# (Int -> IO Int)),
-         g
-         `cast` (<Int>_R %<'Many>_N ->_R Sym (GHC.Types.N:IO[0] <Int>_R)
-                 :: (Int
-                     -> GHC.Prim.State# GHC.Prim.RealWorld
-                     -> (# GHC.Prim.State# GHC.Prim.RealWorld, Int #))
-                    ~R# (Int -> IO Int)) #)
-
--- RHS size: {terms: 11, types: 26, coercions: 0, joins: 0/0}
-f [InlPrag=[2]]
-  :: forall {a}. Show a => a -> (Int -> IO Int, Int -> IO Int)
-[GblId,
- Arity=2,
- Str=<MP(A,MCM(L),A)><L>,
- Cpr=1,
- Unf=Unf{Src=InlineStable, TopLvl=True, Value=True, ConLike=True,
-         WorkFree=True, Expandable=True,
-         Guidance=ALWAYS_IF(arity=2,unsat_ok=True,boring_ok=False)
-         Tmpl= \ (@a) ($dShow [Occ=Once1] :: Show a) (x [Occ=Once1] :: a) ->
-                 case Foo.$wf @a $dShow x of
-                 { (# ww [Occ=Once1], ww1 [Occ=Once1] #) ->
-                 (ww, ww1)
-                 }}]
-f = \ (@a) ($dShow :: Show a) (x :: a) ->
-      case Foo.$wf @a $dShow x of { (# ww, ww1 #) -> (ww, ww1) }
-
-
-
diff --git a/testsuite/tests/stranal/should_compile/T20746.stderr-mingw32 b/testsuite/tests/stranal/should_compile/T20746.stderr-mingw32
deleted file mode 100644
index 65ad712056..0000000000
--- a/testsuite/tests/stranal/should_compile/T20746.stderr-mingw32
+++ /dev/null
@@ -1,132 +0,0 @@
-==================== Tidy Core ====================
-Result size of Tidy Core
-  = {terms: 70, types: 113, coercions: 18, joins: 0/2}
-
--- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
-Foo.$trModule4 :: GHC.Prim.Addr#
-[GblId,
- Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
-         WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 20 0}]
-Foo.$trModule4 = "main"#
-
--- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
-Foo.$trModule3 :: GHC.Types.TrName
-[GblId,
- Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
-         WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 10}]
-Foo.$trModule3 = GHC.Types.TrNameS Foo.$trModule4
-
--- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
-Foo.$trModule2 :: GHC.Prim.Addr#
-[GblId,
- Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
-         WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 20 0}]
-Foo.$trModule2 = "Foo"#
-
--- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
-Foo.$trModule1 :: GHC.Types.TrName
-[GblId,
- Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
-         WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 10}]
-Foo.$trModule1 = GHC.Types.TrNameS Foo.$trModule2
-
--- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
-Foo.$trModule :: GHC.Types.Module
-[GblId,
- Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
-         WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 10}]
-Foo.$trModule = GHC.Types.Module Foo.$trModule3 Foo.$trModule1
-
--- RHS size: {terms: 5, types: 8, coercions: 0, joins: 0/0}
-Foo.f1 [InlPrag=NOINLINE]
-  :: Int
-     -> GHC.Prim.State# GHC.Prim.RealWorld
-     -> (# GHC.Prim.State# GHC.Prim.RealWorld, Int #)
-[GblId, Arity=2, Str=<L><L>, Cpr=1, Unf=OtherCon []]
-Foo.f1
-  = \ (n :: Int)
-      (s [OS=OneShot] :: GHC.Prim.State# GHC.Prim.RealWorld) ->
-      (# s, n #)
-
--- RHS size: {terms: 1, types: 0, coercions: 6, joins: 0/0}
-foogle [InlPrag=[final]] :: Int -> IO Int
-[GblId,
- Arity=2,
- Str=<L><L>,
- Cpr=1,
- Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
-         WorkFree=True, Expandable=True,
-         Guidance=ALWAYS_IF(arity=0,unsat_ok=True,boring_ok=True)}]
-foogle
-  = Foo.f1
-    `cast` (<Int>_R %<'Many>_N ->_R Sym (GHC.Types.N:IO[0] <Int>_R)
-            :: (Int
-                -> GHC.Prim.State# GHC.Prim.RealWorld
-                -> (# GHC.Prim.State# GHC.Prim.RealWorld, Int #))
-               ~R# (Int -> IO Int))
-
--- RHS size: {terms: 35, types: 38, coercions: 12, joins: 0/2}
-Foo.$wf [InlPrag=[2]]
-  :: forall {a}. Show a => a -> (# Int -> IO Int, Int -> IO Int #)
-[GblId,
- Arity=2,
- Str=<MP(A,MCM(L),A)><L>,
- Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
-         WorkFree=True, Expandable=True, Guidance=IF_ARGS [30 0] 181 10}]
-Foo.$wf
-  = \ (@a) ($dShow :: Show a) (x :: a) ->
-      let {
-        lvl :: String
-        [LclId]
-        lvl = show @a $dShow x } in
-      let {
-        g :: Int
-             -> GHC.Prim.State# GHC.Prim.RealWorld
-             -> (# GHC.Prim.State# GHC.Prim.RealWorld, Int #)
-        [LclId, Arity=2, Str=<1L><L>, Unf=OtherCon []]
-        g = \ (y :: Int) (s :: GHC.Prim.State# GHC.Prim.RealWorld) ->
-              case y of wild { GHC.Types.I# x1 ->
-              case GHC.Prim.># x1 2# of {
-                __DEFAULT -> Foo.f1 wild s;
-                1# ->
-                  case GHC.IO.Handle.Text.hPutStr2
-                         GHC.IO.StdHandles.stdout lvl GHC.Types.True s
-                  of
-                  { (# ipv, ipv1 #) ->
-                  Foo.f1 wild ipv
-                  }
-              }
-              } } in
-      (# g
-         `cast` (<Int>_R %<'Many>_N ->_R Sym (GHC.Types.N:IO[0] <Int>_R)
-                 :: (Int
-                     -> GHC.Prim.State# GHC.Prim.RealWorld
-                     -> (# GHC.Prim.State# GHC.Prim.RealWorld, Int #))
-                    ~R# (Int -> IO Int)),
-         g
-         `cast` (<Int>_R %<'Many>_N ->_R Sym (GHC.Types.N:IO[0] <Int>_R)
-                 :: (Int
-                     -> GHC.Prim.State# GHC.Prim.RealWorld
-                     -> (# GHC.Prim.State# GHC.Prim.RealWorld, Int #))
-                    ~R# (Int -> IO Int)) #)
-
--- RHS size: {terms: 11, types: 26, coercions: 0, joins: 0/0}
-f [InlPrag=[2]]
-  :: forall {a}. Show a => a -> (Int -> IO Int, Int -> IO Int)
-[GblId,
- Arity=2,
- Str=<MP(A,MCM(L),A)><L>,
- Cpr=1,
- Unf=Unf{Src=InlineStable, TopLvl=True, Value=True, ConLike=True,
-         WorkFree=True, Expandable=True,
-         Guidance=ALWAYS_IF(arity=2,unsat_ok=True,boring_ok=False)
-         Tmpl= \ (@a) ($dShow [Occ=Once1] :: Show a) (x [Occ=Once1] :: a) ->
-                 case Foo.$wf @a $dShow x of
-                 { (# ww [Occ=Once1], ww1 [Occ=Once1] #) ->
-                 (ww, ww1)
-                 }}]
-f = \ (@a) ($dShow :: Show a) (x :: a) ->
-      case Foo.$wf @a $dShow x of { (# ww, ww1 #) -> (ww, ww1) }
-
-
-
diff --git a/testsuite/tests/stranal/should_compile/T20746b.stderr b/testsuite/tests/stranal/should_compile/T20746b.stderr
deleted file mode 100644
index 97f8496c4b..0000000000
--- a/testsuite/tests/stranal/should_compile/T20746b.stderr
+++ /dev/null
@@ -1,77 +0,0 @@
-
-==================== Tidy Core ====================
-Result size of Tidy Core
-  = {terms: 33, types: 78, coercions: 21, joins: 0/0}
-
--- RHS size: {terms: 5, types: 8, coercions: 0, joins: 0/0}
-T20746b.mightThrow1 [InlPrag=NOINLINE]
-  :: Int
-     -> GHC.Prim.State# GHC.Prim.RealWorld
-     -> (# GHC.Prim.State# GHC.Prim.RealWorld, Int #)
-[GblId, Arity=2, Str=<L><L>, Cpr=1, Unf=OtherCon []]
-T20746b.mightThrow1
-  = \ (n :: Int)
-      (s [OS=OneShot] :: GHC.Prim.State# GHC.Prim.RealWorld) ->
-      (# s, n #)
-
--- RHS size: {terms: 1, types: 0, coercions: 6, joins: 0/0}
-mightThrow [InlPrag=[final]] :: Int -> IO Int
-[GblId,
- Arity=2,
- Str=<L><L>,
- Cpr=1,
- Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
-         WorkFree=True, Expandable=True,
-         Guidance=ALWAYS_IF(arity=0,unsat_ok=True,boring_ok=True)}]
-mightThrow
-  = T20746b.mightThrow1
-    `cast` (<Int>_R %<'Many>_N ->_R Sym (GHC.Types.N:IO[0] <Int>_R)
-            :: (Int
-                -> GHC.Prim.State# GHC.Prim.RealWorld
-                -> (# GHC.Prim.State# GHC.Prim.RealWorld, Int #))
-               ~R# (Int -> IO Int))
-
-Rec {
--- RHS size: {terms: 22, types: 32, coercions: 0, joins: 0/0}
-T20746b.f1 [Occ=LoopBreaker]
-  :: Bool
-     -> (Int, Int, Int)
-     -> GHC.Prim.State# GHC.Prim.RealWorld
-     -> (# GHC.Prim.State# GHC.Prim.RealWorld, (Int, Int, Int) #)
-[GblId, Arity=3, Str=<1L><1L><L>, Cpr=1, Unf=OtherCon []]
-T20746b.f1
-  = \ (ds :: Bool)
-      (trp :: (Int, Int, Int))
-      (eta [OS=OneShot] :: GHC.Prim.State# GHC.Prim.RealWorld) ->
-      case ds of {
-        False -> T20746b.f1 GHC.Types.True trp eta;
-        True ->
-          case trp of wild1 { (a, b, c) ->
-          case T20746b.mightThrow1 a eta of { (# ipv, ipv1 #) ->
-          (# ipv, wild1 #)
-          }
-          }
-      }
-end Rec }
-
--- RHS size: {terms: 1, types: 0, coercions: 15, joins: 0/0}
-f :: Bool -> (Int, Int, Int) -> IO (Int, Int, Int)
-[GblId,
- Arity=3,
- Str=<1L><1L><L>,
- Cpr=1,
- Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
-         WorkFree=True, Expandable=True,
-         Guidance=ALWAYS_IF(arity=0,unsat_ok=True,boring_ok=True)}]
-f = T20746b.f1
-    `cast` (<Bool>_R
-            %<'Many>_N ->_R <(Int, Int, Int)>_R
-            %<'Many>_N ->_R Sym (GHC.Types.N:IO[0] <(Int, Int, Int)>_R)
-            :: (Bool
-                -> (Int, Int, Int)
-                -> GHC.Prim.State# GHC.Prim.RealWorld
-                -> (# GHC.Prim.State# GHC.Prim.RealWorld, (Int, Int, Int) #))
-               ~R# (Bool -> (Int, Int, Int) -> IO (Int, Int, Int)))
-
-
-
diff --git a/testsuite/tests/stranal/should_compile/T21128.hs b/testsuite/tests/stranal/should_compile/T21128.hs
new file mode 100644
index 0000000000..899adac49c
--- /dev/null
+++ b/testsuite/tests/stranal/should_compile/T21128.hs
@@ -0,0 +1,11 @@
+module T21128 where
+
+import T21128a
+
+theresCrud :: Int -> Int -> Int
+theresCrud x y = go x
+  where
+    go 0 = index 0 y 0
+    go 1 = index x y 1
+    go n = go (n-1)
+{-# NOINLINE theresCrud #-}
diff --git a/testsuite/tests/stranal/should_compile/T21128.stderr b/testsuite/tests/stranal/should_compile/T21128.stderr
new file mode 100644
index 0000000000..a64c1f1d5a
--- /dev/null
+++ b/testsuite/tests/stranal/should_compile/T21128.stderr
@@ -0,0 +1,133 @@
+
+==================== Tidy Core ====================
+Result size of Tidy Core
+  = {terms: 137, types: 92, coercions: 4, joins: 0/0}
+
+lvl = "error"#
+
+lvl1 = unpackCString# lvl
+
+$trModule4 = "main"#
+
+lvl2 = unpackCString# $trModule4
+
+$trModule2 = "T21128a"#
+
+lvl3 = unpackCString# $trModule2
+
+lvl4 = "./T21128a.hs"#
+
+lvl5 = unpackCString# lvl4
+
+lvl6 = I# 4#
+
+lvl7 = I# 20#
+
+lvl8 = I# 25#
+
+lvl9 = SrcLoc lvl2 lvl3 lvl5 lvl6 lvl7 lvl6 lvl8
+
+lvl10 = PushCallStack lvl1 lvl9 EmptyCallStack
+
+$windexError
+  = \ @a @b ww eta eta1 eta2 ->
+      error
+        (lvl10 `cast` <Co:4> :: CallStack ~R# (?callStack::CallStack))
+        (++ (ww eta) (++ (ww eta1) (ww eta2)))
+
+indexError
+  = \ @a @b $dShow eta eta1 eta2 ->
+      case $dShow of { C:Show ww ww1 ww2 ->
+      $windexError ww1 eta eta1 eta2
+      }
+
+$trModule3 = TrNameS $trModule4
+
+$trModule1 = TrNameS $trModule2
+
+$trModule = Module $trModule3 $trModule1
+
+$wlvl
+  = \ ww ww1 ww2 ->
+      $windexError $fShowInt_$cshow (I# ww2) (I# ww1) (I# ww)
+
+index
+  = \ l u i ->
+      case l of { I# x ->
+      case i of { I# y ->
+      case <=# x y of {
+        __DEFAULT -> case u of { I# ww -> $wlvl y ww x };
+        1# ->
+          case u of { I# y1 ->
+          case <# y y1 of {
+            __DEFAULT -> $wlvl y y1 x;
+            1# -> I# (-# y x)
+          }
+          }
+      }
+      }
+      }
+
+
+
+
+==================== Tidy Core ====================
+Result size of Tidy Core
+  = {terms: 108, types: 47, coercions: 0, joins: 3/4}
+
+$trModule4 = "main"#
+
+$trModule3 = TrNameS $trModule4
+
+$trModule2 = "T21128"#
+
+$trModule1 = TrNameS $trModule2
+
+$trModule = Module $trModule3 $trModule1
+
+i = I# 1#
+
+l = I# 0#
+
+lvl = \ y -> $windexError $fShowInt_$cshow l y l
+
+lvl1 = \ ww y -> $windexError $fShowInt_$cshow (I# ww) y i
+
+$wtheresCrud
+  = \ ww ww1 ->
+      let { y = I# ww1 } in
+      join {
+        lvl2
+          = case <=# ww 1# of {
+              __DEFAULT -> case lvl1 ww y of wild { };
+              1# ->
+                case <# 1# ww1 of {
+                  __DEFAULT -> case lvl1 ww y of wild { };
+                  1# -> -# 1# ww
+                }
+            } } in
+      join {
+        lvl3
+          = case <# 0# ww1 of {
+              __DEFAULT -> case lvl y of wild { };
+              1# -> 0#
+            } } in
+      joinrec {
+        $wgo ww2
+          = case ww2 of wild {
+              __DEFAULT -> jump $wgo (-# wild 1#);
+              0# -> jump lvl3;
+              1# -> jump lvl2
+            }; } in
+      jump $wgo ww
+
+theresCrud
+  = \ x y ->
+      case x of { I# ww ->
+      case y of { I# ww1 ->
+      case $wtheresCrud ww ww1 of ww2 { __DEFAULT -> I# ww2 }
+      }
+      }
+
+
+
diff --git a/testsuite/tests/stranal/should_compile/T21128a.hs b/testsuite/tests/stranal/should_compile/T21128a.hs
new file mode 100644
index 0000000000..89d4cd9699
--- /dev/null
+++ b/testsuite/tests/stranal/should_compile/T21128a.hs
@@ -0,0 +1,11 @@
+module T21128a where
+
+indexError :: Show a => a -> a -> a ->  b
+indexError a b c = error (show a ++ show b ++ show c)
+{-# NOINLINE indexError #-}
+
+index :: Int -> Int -> Int -> Int
+index l u i
+  | l <= i && i < u = i-l
+  | otherwise       = indexError l u i
+{-# INLINE index #-}
diff --git a/testsuite/tests/stranal/should_compile/all.T b/testsuite/tests/stranal/should_compile/all.T
index 042ee9dd44..2698a3a851 100644
--- a/testsuite/tests/stranal/should_compile/all.T
+++ b/testsuite/tests/stranal/should_compile/all.T
@@ -1,5 +1,6 @@
 # Only compile with optimisation
-setTestOpts( only_ways(['optasm']) )
+setTestOpts( only_ways(['optasm']))
+setTestOpts( extra_hc_opts('-dno-debug-output') )
 
 test('default', normal, compile, [''])
 test('fact', normal, compile, [''])
@@ -77,8 +78,8 @@ test('T19882b', normal, compile, [''])
 # We want that the 'go' joinrec in the unfolding has been worker/wrappered.
 # So we simply grep for 'jump $wgo' and hope we find more than 2 call sites:
 test('T20510', [ grep_errmsg(r'jump \$wgo') ], compile, ['-dsuppress-uniques -ddump-exitify'])
-test('T20746', normal, compile, ['-dsuppress-uniques -ddump-simpl'])
-test('T20746b', normal, compile, ['-dsuppress-uniques -ddump-simpl -dno-typeable-binds'])
 test('T20817', [ grep_errmsg(r'Str') ], compile, ['-dsuppress-uniques -ddump-stranal'])
 # T21150: Check that t{,1,2} haven't been inlined.
 test('T21150', [ grep_errmsg(r'( t\d? :: Int)') ], compile, ['-dsuppress-uniques -ddump-exitify'])
+# T21128: Check that y is not reboxed in $wtheresCrud
+test('T21128', [ grep_errmsg(r'let { y = I\#') ], multimod_compile, ['T21128', '-v0 -dsuppress-uniques -dsuppress-all -ddump-simpl'])
diff --git a/testsuite/tests/stranal/sigs/DmdAnalGADTs.stderr b/testsuite/tests/stranal/sigs/DmdAnalGADTs.stderr
index ea089c36be..2ed48eed70 100644
--- a/testsuite/tests/stranal/sigs/DmdAnalGADTs.stderr
+++ b/testsuite/tests/stranal/sigs/DmdAnalGADTs.stderr
@@ -9,7 +9,7 @@ DmdAnalGADTs.f: <1L>
 DmdAnalGADTs.f': <1L>
 DmdAnalGADTs.g: <1L>
 DmdAnalGADTs.hasCPR:
-DmdAnalGADTs.hasStrSig: <1!L>
+DmdAnalGADTs.hasStrSig: <1!P(L)>
 
 
 
@@ -37,6 +37,6 @@ DmdAnalGADTs.f: <1L>
 DmdAnalGADTs.f': <1L>
 DmdAnalGADTs.g: <1L>
 DmdAnalGADTs.hasCPR:
-DmdAnalGADTs.hasStrSig: <1!L>
+DmdAnalGADTs.hasStrSig: <1!P(L)>
 
 
diff --git a/testsuite/tests/stranal/sigs/HyperStrUse.stderr b/testsuite/tests/stranal/sigs/HyperStrUse.stderr
index 3e791439a1..08caf32af4 100644
--- a/testsuite/tests/stranal/sigs/HyperStrUse.stderr
+++ b/testsuite/tests/stranal/sigs/HyperStrUse.stderr
@@ -1,7 +1,7 @@
 
 ==================== Strictness signatures ====================
 HyperStrUse.$trModule:
-HyperStrUse.f: <1!P(1!L,A)><1L>
+HyperStrUse.f: <1!P(1!P(L),A)><1L>
 
 
 
@@ -13,6 +13,6 @@ HyperStrUse.f: 1
 
 ==================== Strictness signatures ====================
 HyperStrUse.$trModule:
-HyperStrUse.f: <1!P(1!L,A)><1L>
+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 8e6de7eb90..45bc691802 100644
--- a/testsuite/tests/stranal/sigs/NewtypeArity.stderr
+++ b/testsuite/tests/stranal/sigs/NewtypeArity.stderr
@@ -3,8 +3,8 @@
 Test.$tc'MkT:
 Test.$tcT:
 Test.$trModule:
-Test.t: <1!L><1!L>
-Test.t2: <1!L><1!L>
+Test.t: <1!P(L)><1!P(L)>
+Test.t2: <1!P(L)><1!P(L)>
 
 
 
@@ -21,7 +21,7 @@ Test.t2: 1
 Test.$tc'MkT:
 Test.$tcT:
 Test.$trModule:
-Test.t: <1!L><1!L>
-Test.t2: <1!L><1!L>
+Test.t: <1!P(L)><1!P(L)>
+Test.t2: <1!P(L)><1!P(L)>
 
 
diff --git a/testsuite/tests/stranal/sigs/T12370.stderr b/testsuite/tests/stranal/sigs/T12370.stderr
index a8bbcd0e4c..dc7dbdd2e5 100644
--- a/testsuite/tests/stranal/sigs/T12370.stderr
+++ b/testsuite/tests/stranal/sigs/T12370.stderr
@@ -1,8 +1,8 @@
 
 ==================== Strictness signatures ====================
 T12370.$trModule:
-T12370.bar: <1!L><1!L>
-T12370.foo: <1!P(1!L,1!L)>
+T12370.bar: <1!P(L)><1!P(L)>
+T12370.foo: <1!P(1!P(L),1!P(L))>
 
 
 
@@ -15,7 +15,7 @@ T12370.foo: 1
 
 ==================== Strictness signatures ====================
 T12370.$trModule:
-T12370.bar: <1!L><1!L>
-T12370.foo: <1!P(1!L,1!L)>
+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/T13380f.stderr b/testsuite/tests/stranal/sigs/T13380f.stderr
index ad68f821d8..4b17ceae85 100644
--- a/testsuite/tests/stranal/sigs/T13380f.stderr
+++ b/testsuite/tests/stranal/sigs/T13380f.stderr
@@ -1,9 +1,9 @@
 
 ==================== Strictness signatures ====================
 T13380f.$trModule:
-T13380f.f: <1!L><1!L><L>
-T13380f.g: <1!L><ML><L>
-T13380f.h: <1!L><ML><L>
+T13380f.f: <1!P(L)><1!P(L)><L>
+T13380f.g: <1!P(L)><ML><L>
+T13380f.h: <1!P(L)><ML><L>
 T13380f.interruptibleCall: <L>
 T13380f.safeCall: <L>
 T13380f.unsafeCall: <L>
@@ -23,9 +23,9 @@ T13380f.unsafeCall: 1(, 1)
 
 ==================== Strictness signatures ====================
 T13380f.$trModule:
-T13380f.f: <1!L><1!L><L>
-T13380f.g: <1!L><ML><L>
-T13380f.h: <1!L><ML><L>
+T13380f.f: <1!P(L)><1!P(L)><L>
+T13380f.g: <1!P(L)><ML><L>
+T13380f.h: <1!P(L)><ML><L>
 T13380f.interruptibleCall: <L>
 T13380f.safeCall: <L>
 T13380f.unsafeCall: <L>
diff --git a/testsuite/tests/stranal/sigs/T16197b.stderr b/testsuite/tests/stranal/sigs/T16197b.stderr
index 96481ec378..ec45df4202 100644
--- a/testsuite/tests/stranal/sigs/T16197b.stderr
+++ b/testsuite/tests/stranal/sigs/T16197b.stderr
@@ -5,7 +5,7 @@ T16197b.$tc'T:
 T16197b.$tcBox:
 T16197b.$tcT:
 T16197b.$trModule:
-T16197b.f: <1!L>
+T16197b.f: <1!P(L)>
 
 
 
@@ -25,6 +25,6 @@ T16197b.$tc'T:
 T16197b.$tcBox:
 T16197b.$tcT:
 T16197b.$trModule:
-T16197b.f: <1!L>
+T16197b.f: <1!P(L)>
 
 
diff --git a/testsuite/tests/stranal/sigs/T16859.stderr b/testsuite/tests/stranal/sigs/T16859.stderr
index 4e32752e35..37718134a2 100644
--- a/testsuite/tests/stranal/sigs/T16859.stderr
+++ b/testsuite/tests/stranal/sigs/T16859.stderr
@@ -7,12 +7,12 @@ T16859.$tcName:
 T16859.$tcNameSort:
 T16859.$trModule:
 T16859.bar: <1!A><L>
-T16859.baz: <1L><1!L><1C1(L)>
-T16859.buz: <1!L>
+T16859.baz: <1L><1!P(L)><1C1(L)>
+T16859.buz: <1!P(L,L)>
 T16859.foo: <1L><L>
-T16859.mkInternalName: <1!L><1L><1L>
+T16859.mkInternalName: <1!P(L)><1L><1L>
 T16859.n_loc: <1!P(A,A,A,1L)>
-T16859.n_occ: <1!P(A,1!L,A,A)>
+T16859.n_occ: <1!P(A,1!P(L,L),A,A)>
 T16859.n_sort: <1!P(1L,A,A,A)>
 T16859.n_uniq: <1!P(A,A,L,A)>
 
@@ -45,12 +45,12 @@ T16859.$tcName:
 T16859.$tcNameSort:
 T16859.$trModule:
 T16859.bar: <1!A><L>
-T16859.baz: <L><1!L><1C1(L)>
-T16859.buz: <1!L>
+T16859.baz: <L><1!P(L)><1C1(L)>
+T16859.buz: <1!P(L,L)>
 T16859.foo: <L><L>
-T16859.mkInternalName: <1!L><L><L>
+T16859.mkInternalName: <1!P(L)><L><L>
 T16859.n_loc: <1!P(A,A,A,1L)>
-T16859.n_occ: <1!P(A,1!L,A,A)>
+T16859.n_occ: <1!P(A,1!P(L,L),A,A)>
 T16859.n_sort: <1!P(1L,A,A,A)>
 T16859.n_uniq: <1!P(A,A,L,A)>
 
diff --git a/testsuite/tests/stranal/sigs/T18907.stderr b/testsuite/tests/stranal/sigs/T18907.stderr
index 2a1c84d3d5..9d9aff99c8 100644
--- a/testsuite/tests/stranal/sigs/T18907.stderr
+++ b/testsuite/tests/stranal/sigs/T18907.stderr
@@ -3,7 +3,7 @@
 T18907.$tc'H:
 T18907.$tcHuge:
 T18907.$trModule:
-T18907.f: <1!L>
+T18907.f: <1L>
 T18907.g: <1P(SL,L,L,L,L)>
 T18907.h: <1!A><1L>
 T18907.m: <1!B>b
@@ -14,7 +14,7 @@ T18907.m: <1!B>b
 T18907.$tc'H:
 T18907.$tcHuge:
 T18907.$trModule:
-T18907.f: 1
+T18907.f:
 T18907.g:
 T18907.h:
 T18907.m: b
@@ -25,7 +25,7 @@ T18907.m: b
 T18907.$tc'H:
 T18907.$tcHuge:
 T18907.$trModule:
-T18907.f: <1!L>
+T18907.f: <1L>
 T18907.g: <1P(SL,L,L,L,L)>
 T18907.h: <1!A><1L>
 T18907.m: <1!B>b
diff --git a/testsuite/tests/stranal/sigs/T18957.stderr b/testsuite/tests/stranal/sigs/T18957.stderr
index c1c09c6b4a..3d730ce9fc 100644
--- a/testsuite/tests/stranal/sigs/T18957.stderr
+++ b/testsuite/tests/stranal/sigs/T18957.stderr
@@ -1,10 +1,10 @@
 
 ==================== Strictness signatures ====================
 T18957.$trModule:
-T18957.g: <MCM(L)><1!L>
-T18957.h1: <SCM(L)><1!L>
-T18957.h2: <1CM(L)><1!L>
-T18957.h3: <L><1!L>
+T18957.g: <MCM(L)><1L>
+T18957.h1: <SCM(L)><1L>
+T18957.h2: <1CM(L)><1L>
+T18957.h3: <L><1L>
 T18957.seq': <1A><1L>
 
 
@@ -21,10 +21,10 @@ T18957.seq':
 
 ==================== Strictness signatures ====================
 T18957.$trModule:
-T18957.g: <MCM(L)><1!L>
-T18957.h1: <SCM(L)><1!L>
-T18957.h2: <1CM(L)><1!L>
-T18957.h3: <L><1!L>
+T18957.g: <MCM(L)><1L>
+T18957.h1: <SCM(L)><1L>
+T18957.h2: <1CM(L)><1L>
+T18957.h3: <L><1L>
 T18957.seq': <1A><1L>
 
 
diff --git a/testsuite/tests/stranal/sigs/T19407.stderr b/testsuite/tests/stranal/sigs/T19407.stderr
index c0cec03a4d..8d4045700a 100644
--- a/testsuite/tests/stranal/sigs/T19407.stderr
+++ b/testsuite/tests/stranal/sigs/T19407.stderr
@@ -8,7 +8,7 @@ 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.h: <1!P(1L,A)>
-T19407.n: <1!P(A,1!L)>
+T19407.n: <1!P(A,1!P(L))>
 
 
 
@@ -34,6 +34,6 @@ 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.h: <1!P(1L,A)>
-T19407.n: <1!P(A,1!L)>
+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 1afea4e841..f8f465fd82 100644
--- a/testsuite/tests/stranal/sigs/T19871.stderr
+++ b/testsuite/tests/stranal/sigs/T19871.stderr
@@ -3,7 +3,7 @@
 T19871.$tc'Huge:
 T19871.$tcHuge:
 T19871.$trModule:
-T19871.absent: <1!P(1L,ML,A,A,A,A,A,A,A,A,A,A)>
+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)>
 T19871.f10: <1!P(A,A,A,A,A,A,A,A,A,1L,A,A)>
@@ -18,7 +18,7 @@ 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.sumIO: <1!P(1L)><1!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)>
 
 
@@ -51,7 +51,7 @@ T19871.update: 1
 T19871.$tc'Huge:
 T19871.$tcHuge:
 T19871.$trModule:
-T19871.absent: <1!P(1L,ML,A,A,A,A,A,A,A,A,A,A)>
+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)>
 T19871.f10: <1!P(A,A,A,A,A,A,A,A,A,1L,A,A)>
@@ -66,7 +66,7 @@ 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.sumIO: <1!P(1L)><1!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/should_compile/T20746.hs b/testsuite/tests/stranal/sigs/T20746.hs
index 93496acd65..93496acd65 100644
--- a/testsuite/tests/stranal/should_compile/T20746.hs
+++ b/testsuite/tests/stranal/sigs/T20746.hs
diff --git a/testsuite/tests/stranal/sigs/T20746.stderr b/testsuite/tests/stranal/sigs/T20746.stderr
new file mode 100644
index 0000000000..b0656cd13d
--- /dev/null
+++ b/testsuite/tests/stranal/sigs/T20746.stderr
@@ -0,0 +1,21 @@
+
+==================== Strictness signatures ====================
+Foo.$trModule:
+Foo.f: <MP(A,MCM(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.foogle: <L><L>
+
+
diff --git a/testsuite/tests/stranal/should_compile/T20746b.hs b/testsuite/tests/stranal/sigs/T20746b.hs
index 6804fb4449..9ab7cc7d4b 100644
--- a/testsuite/tests/stranal/should_compile/T20746b.hs
+++ b/testsuite/tests/stranal/sigs/T20746b.hs
@@ -9,6 +9,6 @@ mightThrow n = return n
 -- we don't do worker/wrapper at all
 f :: Bool -> (Int, Int, Int) -> IO (Int, Int, Int)
 f False trp = f True trp
-f True trp@(a,b,c) = do
+f True trp@(~(a,b,c)) = do
   _ <- mightThrow a -- this potentially throwing IO action should not force unboxing of trp
-  return trp
+  return $! trp
diff --git a/testsuite/tests/stranal/sigs/T20746b.stderr b/testsuite/tests/stranal/sigs/T20746b.stderr
new file mode 100644
index 0000000000..bd23944c61
--- /dev/null
+++ b/testsuite/tests/stranal/sigs/T20746b.stderr
@@ -0,0 +1,21 @@
+
+==================== 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/T21119.hs b/testsuite/tests/stranal/sigs/T21119.hs
new file mode 100644
index 0000000000..7be2cf1788
--- /dev/null
+++ b/testsuite/tests/stranal/sigs/T21119.hs
@@ -0,0 +1,30 @@
+-- {-# OPTIONS_GHC -Wincomplete-patterns -fforce-recomp #-}
+-- {-# OPTIONS_GHC -O2 -fforce-recomp #-}
+-- {-# LANGUAGE PatternSynonyms #-}
+-- {-# LANGUAGE BangPatterns #-}
+-- {-# LANGUAGE MagicHash, UnboxedTuples #-}
+module T21119 where
+
+import Control.Exception
+
+indexError :: Show a => (a, a) -> a -> String -> b
+indexError rng i s = error (show rng ++ show i ++ show s)
+
+get :: (Int, Int) -> Int -> [a] -> a
+get p@(l,u) i xs
+  | l <= i, i < u = xs !! (i-u)
+  | otherwise     = indexError p i "get"
+
+-- Now the same with precise exceptions:
+
+throwIndexError :: Show a => (a, a) -> a -> String -> IO b
+throwIndexError rng i s = throwIO (userError (show rng ++ show i ++ show s))
+
+-- It's important that we don't unbox 'u' here.
+-- We may or may not unbox 'p' and 'l'.
+-- Last time I checked, we didn't unbox 'p' and 'l', because 'throwIndexError'
+-- isn't strict in them. That's fine.
+getIO :: (Int, Int) -> Int -> [a] -> IO a
+getIO p@(l,u) i xs
+  | l <= i, i < u = return $! xs !! (i-u)
+  | otherwise     = throwIndexError p i "get"
diff --git a/testsuite/tests/stranal/sigs/T21119.stderr b/testsuite/tests/stranal/sigs/T21119.stderr
new file mode 100644
index 0000000000..dfefcdea03
--- /dev/null
+++ b/testsuite/tests/stranal/sigs/T21119.stderr
@@ -0,0 +1,27 @@
+
+==================== Strictness signatures ====================
+T21119.$trModule:
+T21119.get: <1!P(S!P(L),S!P(L))><1!P(L)><1L>
+T21119.getIO: <1P(SL,L)><1L><ML><L>
+T21119.indexError: <S!P(SCS(C1(L)),1C1(L),B)><1!S><S!S><1!S>b
+T21119.throwIndexError: <LP(LCL(C1(L)),MCM(L),A)><ML><L><ML><L>x
+
+
+
+==================== Cpr signatures ====================
+T21119.$trModule:
+T21119.get:
+T21119.getIO: 1
+T21119.indexError: b
+T21119.throwIndexError: b
+
+
+
+==================== Strictness signatures ====================
+T21119.$trModule:
+T21119.get: <1!P(1!P(L),1!P(L))><1!P(L)><1L>
+T21119.getIO: <1P(SL,L)><1L><ML><L>
+T21119.indexError: <1P(SCS(C1(L)),1C1(L),B)><1!S><S!S><1!S>b
+T21119.throwIndexError: <LP(LCL(C1(L)),MCM(L),A)><ML><L><ML><L>x
+
+
diff --git a/testsuite/tests/stranal/sigs/T5075.stderr b/testsuite/tests/stranal/sigs/T5075.stderr
index 7652a16f0a..e367385d52 100644
--- a/testsuite/tests/stranal/sigs/T5075.stderr
+++ b/testsuite/tests/stranal/sigs/T5075.stderr
@@ -2,15 +2,15 @@
 ==================== 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.g: <1!L><S!L>
-T5075.h: <S!L>
+T5075.g: <1L><S!P(L)>
+T5075.h: <S!P(L)>
 
 
 
 ==================== Cpr signatures ====================
 T5075.$trModule:
 T5075.f: 1
-T5075.g: 2(1)
+T5075.g: 2
 T5075.h:
 
 
@@ -18,7 +18,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.g: <1!L><S!L>
-T5075.h: <1!L>
+T5075.g: <1L><S!P(L)>
+T5075.h: <1!P(L)>
 
 
diff --git a/testsuite/tests/stranal/sigs/T8598.stderr b/testsuite/tests/stranal/sigs/T8598.stderr
index e8813a0fc8..747c6a096b 100644
--- a/testsuite/tests/stranal/sigs/T8598.stderr
+++ b/testsuite/tests/stranal/sigs/T8598.stderr
@@ -1,7 +1,7 @@
 
 ==================== Strictness signatures ====================
 T8598.$trModule:
-T8598.fun: <1!L>
+T8598.fun: <1!P(L)>
 
 
 
@@ -13,6 +13,6 @@ T8598.fun: 1
 
 ==================== Strictness signatures ====================
 T8598.$trModule:
-T8598.fun: <1!L>
+T8598.fun: <1!P(L)>
 
 
diff --git a/testsuite/tests/stranal/sigs/all.T b/testsuite/tests/stranal/sigs/all.T
index 95065c2d23..59a4891f6d 100644
--- a/testsuite/tests/stranal/sigs/all.T
+++ b/testsuite/tests/stranal/sigs/all.T
@@ -29,3 +29,6 @@ test('T19871', normal, compile, [''])
 test('T16859', normal, compile, ['-package ghc'])
 test('T18907', normal, compile, [''])
 test('T13331', normal, compile, [''])
+test('T20746', normal, compile, [''])
+test('T20746b', normal, compile, [''])
+test('T21119', normal, compile, [''])