More improvements to worker/wrapperwip/T21888

This patch fixes #21888, and simplifies finaliseArgBoxities
by eliminating the (recently introduced) data type FinalDecision.

A delicate interaction meant that this patch
   commit d1c25a48154236861a413e058ea38d1b8320273f
   Date:   Tue Jul 12 16:33:46 2022 +0100
   Refactor wantToUnboxArg a bit

make worker/wrapper go into an infinite loop.  This patch
fixes it by narrowing the handling of case (B) of
Note [Boxity for bottoming functions], to deal only the
arguemnts that are type variables.  Only then do we drop
the trimBoxity call, which is what caused the bug.

I also
* Added documentation of case (B), which was previously
  completely un-mentioned.  And a regression test,
  T21888a, to test it.

* Made unboxDeeplyDmd stop at lazy demands.  It's rare anyway
  for a bottoming function to have a lazy argument (mainly when
  the data type is recursive and then we don't want to unbox
  deeply).  Plus there is Note [No lazy, Unboxed demands in
  demand signature]

* Refactored the Case equation for dmdAnal a bit, to do less
  redundant pattern matching.

12 files changed, 310 insertions, 154 deletions

diff --git a/compiler/GHC/Core/Opt/DmdAnal.hs b/compiler/GHC/Core/Opt/DmdAnal.hs
index add2c922e4..c3fd09c6e0 100644
--- a/compiler/GHC/Core/Opt/DmdAnal.hs
+++ b/compiler/GHC/Core/Opt/DmdAnal.hs
@@ -432,35 +432,38 @@ dmdAnal' env dmd (Lam var body)
     in
     WithDmdType new_dmd_type (Lam var' body')
 
-dmdAnal' env dmd (Case scrut case_bndr ty [Alt alt bndrs rhs])
+dmdAnal' env dmd (Case scrut case_bndr ty [Alt alt_con bndrs rhs])
   -- Only one alternative.
   -- If it's a DataAlt, it should be the only constructor of the type and we
   -- can consider its field demands when analysing the scrutinee.
-  | want_precise_field_dmds alt
+  | want_precise_field_dmds alt_con
   = let
         WithDmdType rhs_ty rhs'           = dmdAnal env dmd rhs
         WithDmdType alt_ty1 fld_dmds      = findBndrsDmds env rhs_ty bndrs
         WithDmdType alt_ty2 case_bndr_dmd = findBndrDmd env alt_ty1 case_bndr
         !case_bndr'                       = setIdDemandInfo case_bndr case_bndr_dmd
+
         -- Evaluation cardinality on the case binder is irrelevant and a no-op.
         -- 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) = strictifyDmd case_bndr_dmd
+
         -- Compute demand on the scrutinee
         -- FORCE the result, otherwise thunks will end up retaining the
         -- whole DmdEnv
         !(!bndrs', !scrut_sd)
-          | DataAlt _ <- alt
+          | DataAlt _ <- alt_con
           -- See Note [Demand on the scrutinee of a product case]
           -- See Note [Demand on case-alternative binders]
           , (!scrut_sd, fld_dmds') <- addCaseBndrDmd case_bndr_sd fld_dmds
           , let !bndrs' = setBndrsDemandInfo bndrs fld_dmds'
           = (bndrs', scrut_sd)
           | otherwise
-          -- __DEFAULT and literal alts. Simply add demands and discard the
-          -- evaluation cardinality, as we evaluate the scrutinee exactly once.
+          -- DEFAULT alts. Simply add demands and discard the evaluation
+          -- cardinality, as we evaluate the scrutinee exactly once.
           = assert (null bndrs) (bndrs, case_bndr_sd)
+
         alt_ty3
           -- See Note [Precise exceptions and strictness analysis] in "GHC.Types.Demand"
           | exprMayThrowPreciseException (ae_fam_envs env) scrut
@@ -478,35 +481,27 @@ dmdAnal' env dmd (Case scrut case_bndr ty [Alt alt bndrs rhs])
 --                                   , text "scrut_ty" <+> ppr scrut_ty
 --                                   , text "alt_ty" <+> ppr alt_ty2
 --                                   , text "res_ty" <+> ppr res_ty ]) $
-    WithDmdType res_ty (Case scrut' case_bndr' ty [Alt alt bndrs' rhs'])
+    WithDmdType res_ty (Case scrut' case_bndr' ty [Alt alt_con bndrs' rhs'])
     where
-      want_precise_field_dmds alt = case alt of
-        (DataAlt dc)
-          | Nothing <- tyConSingleAlgDataCon_maybe $ dataConTyCon dc -> False
-          | DefinitelyRecursive <- ae_rec_dc env dc                  -> False
-              -- See Note [Demand analysis for recursive data constructors]
-        _                                                            -> True
-
-
-
+      want_precise_field_dmds (DataAlt dc)
+        | Nothing <- tyConSingleAlgDataCon_maybe $ dataConTyCon dc
+        = False    -- Not a product type, even though this is the
+                   -- only remaining possible data constructor
+        | DefinitelyRecursive <- ae_rec_dc env dc
+        = False     -- See Note [Demand analysis for recursive data constructors]
+        | otherwise
+        = True
+      want_precise_field_dmds (LitAlt {}) = False  -- Like the non-product datacon above
+      want_precise_field_dmds DEFAULT     = True
 
 dmdAnal' env dmd (Case scrut case_bndr ty alts)
   = let      -- Case expression with multiple alternatives
-        WithDmdType alt_ty alts'     = combineAltDmds alts
-
-        combineAltDmds [] = WithDmdType botDmdType []
-        combineAltDmds (a:as) =
-          let
-            WithDmdType cur_ty a' = dmdAnalSumAlt env dmd case_bndr a
-            WithDmdType rest_ty as' = combineAltDmds as
-          in WithDmdType (lubDmdType cur_ty rest_ty) (a':as')
+        WithDmdType scrut_ty scrut' = dmdAnal env topSubDmd scrut
 
         WithDmdType alt_ty1 case_bndr_dmd = findBndrDmd env alt_ty case_bndr
         !case_bndr'                       = setIdDemandInfo case_bndr case_bndr_dmd
-        WithDmdType scrut_ty scrut'       = dmdAnal env topSubDmd scrut
-                               -- NB: Base case is botDmdType, for empty case alternatives
-                               --     This is a unit for lubDmdType, and the right result
-                               --     when there really are no alternatives
+        WithDmdType alt_ty alts'          = dmdAnalSumAlts env dmd case_bndr alts
+
         fam_envs             = ae_fam_envs env
         alt_ty2
           -- See Note [Precise exceptions and strictness analysis] in "GHC.Types.Demand"
@@ -564,7 +559,20 @@ forcesRealWorld fam_envs ty
   | otherwise
   = False
 
-dmdAnalSumAlt :: AnalEnv -> SubDemand -> Id -> Alt Var -> WithDmdType (Alt Var)
+dmdAnalSumAlts :: AnalEnv -> SubDemand -> Id -> [CoreAlt] -> WithDmdType [CoreAlt]
+
+dmdAnalSumAlts _ _ _ [] = WithDmdType botDmdType []
+  -- Base case is botDmdType, for empty case alternatives
+  -- This is a unit for lubDmdType, and the right result
+  -- when there really are no alternatives
+dmdAnalSumAlts env dmd case_bndr (alt:alts)
+  = let
+      WithDmdType cur_ty  alt'  = dmdAnalSumAlt env dmd case_bndr alt
+      WithDmdType rest_ty alts' = dmdAnalSumAlts env dmd case_bndr alts
+    in WithDmdType (lubDmdType cur_ty rest_ty) (alt':alts')
+
+
+dmdAnalSumAlt :: AnalEnv -> SubDemand -> Id -> CoreAlt -> WithDmdType CoreAlt
 dmdAnalSumAlt env dmd case_bndr (Alt con bndrs rhs)
   | WithDmdType rhs_ty rhs' <- dmdAnal env dmd rhs
   , WithDmdType alt_ty dmds <- findBndrsDmds env rhs_ty bndrs
@@ -752,10 +760,13 @@ T11545 features a single-product, recursive data type
 Naturally, `(==)` is deeply strict in `A` and in fact will never terminate. That
 leads to very large (exponential in the depth) demand signatures and fruitless
 churn in boxity analysis, demand analysis and worker/wrapper.
-So we detect `A` as a recursive data constructor
-(see Note [Detecting recursive data constructors]) analysing `case x of A ...`
+
+So we detect `A` as a recursive data constructor (see
+Note [Detecting recursive data constructors]) analysing `case x of A ...`
 and simply assume L for the demand on field binders, which is the same code
-path as we take for sum types.
+path as we take for sum types. This code happens in want_precise_field_dmds
+in the Case equation for dmdAnal.
+
 Combined with the B demand on the case binder, we get the very small demand
 signature <1S><1S>b on `(==)`. This improves ghc/alloc performance on T11545
 tenfold! See also Note [CPR for recursive data constructors] which describes the
@@ -1267,38 +1278,67 @@ 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 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].
+Consider (A)
+    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::a` and `u::a`
+boxed, since `indexError` can't unbox them because they are polymorphic.
+This pattern often occurs in performance sensitive code that does
+bounds-checking.
+
+So we want to give `indexError` a signature like `<1!P(!S,!S)><1!S><S!S>b`
+where the !S (meaning Poly Unboxed C1N) says that the polymorphic arguments
+are unboxed (recursively).  The wrapper for `indexError` won't /acutally/
+unbox them (because their polymorphic type doesn't allow that) but when
+demand-analysing /callers/, we'll behave as if that call needs the args
+unboxed.
+
+Then at call sites of `indexError`, we will end up doing some
+reboxing, because `$windexError` still takes boxed arguments. This
+reboxing should usually float into the slow, diverging code path; but
+sometimes (sadly) it doesn't: see Note [Reboxed crud for bottoming calls].
+
+Here is another important case (B):
+    f x = Just x  -- Suppose f is not inlined for some reason
+                  -- Main point: f takes its argument boxed
+
+    wombat x = error (show (f x))
+
+    g :: Bool -> Int -> a
+    g True  x = x+1
+    g False x = wombat x
+
+Again we want `wombat` to pretend to take its Int-typed argument unboxed,
+even though it has to pass it boxed to `f`, so that `g` can take its
+arugment unboxed (and rebox it before calling `wombat`).
+
+So here's what we do: while summarising `indexError`'s boxity signature in
+`finaliseArgBoxities`:
+
+* To address (B), for bottoming functions, we start by using `unboxDeeplyDmd`
+  to make all its argument demands unboxed, right to the leaves; regardless
+  of what the analysis said.
+
+* To address (A), for bottoming functions, in the DontUnbox case when the
+  argument is a type variable, we /refrain/ from using trimBoxity.
+  (Remember the previous bullet: we have already doen `unboxDeeplyDmd`.)
+
+Wrinkle:
+
+* Remember Note [No lazy, Unboxed demands in demand signature]. So
+  unboxDeeplyDmd doesn't recurse into lazy demands.  It's extremely unusual
+  to have lazy demands in the arguments of a bottoming function anyway.
+  But it can happen, when the demand analyser gives up because it
+  encounters a recursive data type; see Note [Demand analysis for recursive
+  data constructors].
 
 Note [Reboxed crud for bottoming calls]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1617,7 +1657,11 @@ finaliseArgBoxities env fn arity rhs div
              -- simply want to give f the same demand signature as g
 
   | otherwise
-  = Just (arg_dmds', add_demands arg_dmds' rhs)
+  = -- pprTrace "finaliseArgBoxities" (
+    --   vcat [text "function:" <+> ppr fn
+    --        , text "dmds before:" <+> ppr (map idDemandInfo (filter isId bndrs))
+    --        , text "dmds after: " <+>  ppr arg_dmds' ]) $
+    Just (arg_dmds', add_demands arg_dmds' rhs)
     -- add_demands: we must attach the final boxities to the lambda-binders
     -- of the function, both because that's kosher, and because CPR analysis
     -- uses the info on the binders directly.
@@ -1649,7 +1693,7 @@ finaliseArgBoxities env fn arity rhs div
         -- NB: even for bottoming functions, don't unbox dictionaries
 
       | is_bot_fn = unboxDeeplyDmd dmd
-        -- See Note [Boxity for bottoming functions]
+        -- See Note [Boxity for bottoming functions], case (B)
 
       | is_opaque = trimBoxity dmd
         -- See Note [OPAQUE pragma]
@@ -1669,19 +1713,15 @@ finaliseArgBoxities env fn arity rhs div
     go_arg :: Budgets -> (Type,StrictnessMark,Demand) -> (Budgets, Demand)
     go_arg bg@(MkB bg_top bg_inner) (ty, str_mark, dmd@(n :* _))
       = case wantToUnboxArg env ty str_mark dmd of
-          FD_Absent -> (bg, dmd)
+          DropAbsent -> (bg, dmd)
 
-          FD_Box | is_bot_fn -> (decremented_bg, dmd)
-                 | otherwise -> (decremented_bg, trimBoxity dmd)
+          DontUnbox | is_bot_fn, isTyVarTy ty -> (decremented_bg, dmd)
+                    | otherwise               -> (decremented_bg, trimBoxity dmd)
             -- If bot: Keep deep boxity even though WW won't unbox
-            -- See Note [Boxity for bottoming functions]
+            -- See Note [Boxity for bottoming functions] case (A)
             -- trimBoxity: see Note [No lazy, Unboxed demands in demand signature]
 
-          FD_RecBox -> (decremented_bg, trimBoxity dmd)
-            -- Important: must do trimBoxity for FD_RecBox, even for bottoming fns,
-            -- else we unbox infinitely (simpl019, T11545, T18304, T4903)
-
-          FD_Unbox triples -> (MkB (bg_top-1) final_bg_inner, final_dmd)
+          DoUnbox triples -> (MkB (bg_top-1) final_bg_inner, final_dmd)
             where
               (bg_inner', dmds') = go_args (incTopBudget bg_inner) triples
                      -- incTopBudget: give one back for the arg we are unboxing
@@ -1715,57 +1755,34 @@ finaliseLetBoxity env ty dmd
     go :: (Type,StrictnessMark,Demand) -> Demand
     go (ty, str, dmd@(n :* _)) =
       case wantToUnboxArg env ty str dmd of
-        FD_Absent        -> dmd
-        FD_Box           -> trimBoxity dmd
-        FD_RecBox        -> trimBoxity dmd
-        FD_Unbox triples -> n :* (mkProd Unboxed $! map go triples)
+        DropAbsent      -> dmd
+        DontUnbox       -> trimBoxity dmd
+        DoUnbox triples -> n :* (mkProd Unboxed $! map go triples)
 
--- The data type `FinalDecision` is entirely local to this one module,
--- and is used only to express the result of `wantToUnboxArg`.
---
--- `FinalDecision` is a bit like WorkWrap.Utils.UnboxingDecision, but
--- not quite the same, notably because of the need for FD_RecBox.  But
--- I decided make `FinalDecision` do just what was needed, rather than
--- to attempt to generalise `UnboxingDecision`, or make it GADT-ish or
--- something.
-data FinalDecision
-  = FD_Absent
-  | FD_Box        -- Keep this argument boxed
-  | FD_RecBox     -- Special case of a strict recursive product!  Take care!
-  | FD_Unbox [(Type, StrictnessMark, Demand)]
-
-wantToUnboxArg :: AnalEnv -> Type -> StrictnessMark -> Demand -> FinalDecision
+wantToUnboxArg :: AnalEnv -> Type -> StrictnessMark -> Demand
+               -> UnboxingDecision [(Type, StrictnessMark, Demand)]
 wantToUnboxArg env ty str_mark dmd@(n :* _)
-  | isAbs n
-  = FD_Absent
-
-  | not (isStrict n || isMarkedStrict str_mark)
-  = FD_Box -- Don't unbox a lazy field
-    -- isMarkedStrict: see Note [Unboxing evaluated arguments] in DmdAnal
-
-  | otherwise
   = case canUnboxArg (ae_fam_envs env) ty dmd of
-      DropAbsent -> FD_Absent
-        -- The earlier isAbs guard means this case won't happen, in fact;
-        -- but it does no harm.  We can't drop the isAbs guard or we'd
-        -- wrongly return StopUnboxing for absent args.
+      DropAbsent -> DropAbsent
+      DontUnbox  -> DontUnbox
 
-      StopUnboxing -> FD_Box
-
-      Unbox (DataConPatContext{ dcpc_dc      = dc
-                              , dcpc_tc_args = tc_args
-                              , dcpc_args    = dmds })
+      DoUnbox (DataConPatContext{ dcpc_dc      = dc
+                                , dcpc_tc_args = tc_args
+                                , dcpc_args    = dmds })
        -- OK, so we /can/ unbox it; but do we /want/ to?
+       | not (isStrict n || isMarkedStrict str_mark)   -- Don't unbox a lazy field
+         -- isMarkedStrict: see Note [Unboxing evaluated arguments] in DmdAnal
+       -> DontUnbox
+
        | DefinitelyRecursive <- ae_rec_dc env dc
          -- See Note [Which types are unboxed?]
          -- and Note [Demand analysis for recursive data constructors]
-       -> FD_RecBox
-
-       | otherwise
-       -> FD_Unbox (zip3 (dubiousDataConInstArgTys dc tc_args)
-                         (dataConRepStrictness dc)
-                         dmds)
+       -> DontUnbox
 
+       | otherwise  -- Bad cases dealt with: we want to unbox!
+       -> DoUnbox (zip3 (dubiousDataConInstArgTys dc tc_args)
+                        (dataConRepStrictness dc)
+                        dmds)
 
 {- *********************************************************************
 *                                                                      *
diff --git a/compiler/GHC/Core/Opt/WorkWrap/Utils.hs b/compiler/GHC/Core/Opt/WorkWrap/Utils.hs
index f23384d134..d3f3928f7a 100644
--- a/compiler/GHC/Core/Opt/WorkWrap/Utils.hs
+++ b/compiler/GHC/Core/Opt/WorkWrap/Utils.hs
@@ -224,7 +224,8 @@ mkWwBodies opts fun_id arg_vars res_ty demands res_cpr
               init_str_marks = map (const NotMarkedStrict) cloned_arg_vars
 
         ; (useful1, work_args_str, wrap_fn_str, fn_args)
-             <- mkWWstr opts cloned_arg_vars init_str_marks
+             <- -- pprTrace "mkWWbodies" (ppr fun_id $$ ppr (arg_vars `zip` cloned_arg_vars) $$ ppr demands) $
+                mkWWstr opts cloned_arg_vars init_str_marks
 
         ; let (work_args, work_marks) = unzip work_args_str
 
@@ -567,13 +568,10 @@ data DataConPatContext s
 -- | Describes the outer shape of an argument to be unboxed or left as-is
 -- Depending on how @s@ is instantiated (e.g., 'Demand' or 'Cpr').
 data UnboxingDecision unboxing_info
-  = StopUnboxing
-  -- ^ We ran out of strictness info. Leave untouched.
-  | DropAbsent
-  -- ^ The argument/field was absent. Drop it.
-  | Unbox !unboxing_info
-  -- ^ The argument is used strictly or the returned product
-  -- was constructed, so unbox it.
+  = DontUnbox               -- ^ We ran out of strictness info. Leave untouched.
+  | DoUnbox !unboxing_info  -- ^ The argument is used strictly or the
+                            -- returned product was constructed, so unbox it.
+  | DropAbsent              -- ^ The argument/field was absent. Drop it.
 
 -- Do we want to create workers just for unlifting?
 wwForUnlifting :: WwOpts -> Bool
@@ -612,11 +610,11 @@ canUnboxArg fam_envs ty (n :* sd)
   , let arity = dataConRepArity dc
   , Just (Unboxed, dmds) <- viewProd arity sd -- See Note [Boxity analysis]
   , dmds `lengthIs` dataConRepArity dc
-  = Unbox (DataConPatContext { dcpc_dc = dc, dcpc_tc_args = tc_args
-                             , dcpc_co = co, dcpc_args = dmds })
+  = DoUnbox (DataConPatContext { dcpc_dc = dc, dcpc_tc_args = tc_args
+                               , dcpc_co = co, dcpc_args = dmds })
 
   | otherwise
-  = StopUnboxing
+  = DontUnbox
 
 
 -- | Unboxing strategy for constructed results.
@@ -638,11 +636,11 @@ canUnboxResult fam_envs ty cpr
   -- Deactivates CPR worker/wrapper splits on constructors with non-linear
   -- arguments, for the moment, because they require unboxed tuple with variable
   -- multiplicity fields.
-  = Unbox (DataConPatContext { dcpc_dc = dc, dcpc_tc_args = tc_args
-                             , dcpc_co = co, dcpc_args = arg_cprs })
+  = DoUnbox (DataConPatContext { dcpc_dc = dc, dcpc_tc_args = tc_args
+                               , dcpc_co = co, dcpc_args = arg_cprs })
 
   | otherwise
-  = StopUnboxing
+  = DontUnbox
 
   where
     -- See Note [non-algebraic or open body type warning]
@@ -809,7 +807,8 @@ mkWWstr :: WwOpts
                                          -- original RHS. Corresponds one-to-one
                                          -- with the wrapper arg vars
 mkWWstr opts args str_marks
-  = go args str_marks
+  = -- pprTrace "mkWWstr" (ppr args) $
+    go args str_marks
   where
     go [] _ = return (badWorker, [], nop_fn, [])
     go (arg : args) (str:strs)
@@ -833,29 +832,32 @@ mkWWstr_one :: WwOpts
             -> StrictnessMark
             -> UniqSM (Bool, [(Var,StrictnessMark)], CoreExpr -> CoreExpr, CoreExpr)
 mkWWstr_one opts arg str_mark =
+  -- pprTrace "mkWWstr_one" (ppr arg <+> (if isId arg then ppr arg_ty  $$ ppr arg_dmd else text "type arg")) $
   case canUnboxArg fam_envs arg_ty arg_dmd of
     _ | isTyVar arg -> do_nothing
 
     DropAbsent
       | Just absent_filler <- mkAbsentFiller opts arg str_mark
-         -- Absent case.  Dropt the argument from the worker.
+         -- Absent case.  Drop the argument from the worker.
          -- We can't always handle absence for arbitrary
          -- unlifted types, so we need to choose just the cases we can
          -- (that's what mkAbsentFiller does)
       -> return (goodWorker, [], nop_fn, absent_filler)
+      | otherwise -> do_nothing
 
-    Unbox dcpc -> unbox_one_arg opts arg dcpc
+    DoUnbox dcpc -> -- pprTrace "mkWWstr_one:1" (ppr (dcpc_dc dcpc) <+> ppr (dcpc_tc_args dcpc) $$ ppr (dcpc_args dcpc)) $
+                    unbox_one_arg opts arg dcpc
 
-    _ | isStrictDmd arg_dmd || isMarkedStrict str_mark
-      , wwForUnlifting opts
+    DontUnbox
+      | isStrictDmd arg_dmd || isMarkedStrict str_mark
+      , wwForUnlifting opts  -- See Note [CBV Function Ids]
       , not (isFunTy arg_ty)
       , not (isUnliftedType arg_ty) -- Already unlifted!
         -- NB: function arguments have a fixed RuntimeRep,
         -- so it's OK to call isUnliftedType here
-      -> -- See Note [CBV Function Ids]
-         return  (goodWorker, [(arg, MarkedStrict)], nop_fn, varToCoreExpr arg )
+      -> return  (goodWorker, [(arg, MarkedStrict)], nop_fn, varToCoreExpr arg )
 
-    _ -> do_nothing -- Other cases, like StopUnboxing
+      | otherwise -> do_nothing
 
   where
     fam_envs   = wo_fam_envs opts
@@ -954,7 +956,7 @@ function is worthy for splitting:
 
 2. If the argument is evaluated strictly (or known to be eval'd),
    we can take a view into the product demand ('viewProd'). In accordance
-   with Note [Boxity analysis], 'canUnboxArg' will say 'Unbox'.
+   with Note [Boxity analysis], 'canUnboxArg' will say 'DoUnbox'.
    'mkWWstr_one' then follows suit it and recurses into the fields of the
    product demand. For example
 
@@ -976,7 +978,7 @@ function is worthy for splitting:
      $gw c a b = if c then a else b
 
 2a But do /not/ unbox if Boxity Analysis said "Boxed".
-   In this case, 'canUnboxArg' returns 'StopUnboxing'.
+   In this case, 'canUnboxArg' returns 'DontUnbox'.
    Otherwise we risk decomposing and reboxing a massive
    tuple which is barely used. Example:
 
@@ -997,7 +999,7 @@ function is worthy for splitting:
 3. In all other cases (e.g., lazy, used demand and not eval'd),
    'finaliseArgBoxities' will have cleared the Boxity flag to 'Boxed'
    (see Note [Finalising boxity for demand signatures] in GHC.Core.Opt.DmdAnal)
-   and 'canUnboxArg' returns 'StopUnboxing' so that 'mkWWstr_one'
+   and 'canUnboxArg' returns 'DontUnbox' so that 'mkWWstr_one'
    stops unboxing.
 
 Note [Worker/wrapper for bottoming functions]
@@ -1391,7 +1393,7 @@ mkWWcpr_one :: WwOpts -> Id -> Cpr -> UniqSM CprWwResultOne
 -- ^ See if we want to unbox the result and hand off to 'unbox_one_result'.
 mkWWcpr_one opts res_bndr cpr
   | assert (not (isTyVar res_bndr) ) True
-  , Unbox dcpc <- canUnboxResult (wo_fam_envs opts) (idType res_bndr) cpr
+  , DoUnbox dcpc <- canUnboxResult (wo_fam_envs opts) (idType res_bndr) cpr
   = unbox_one_result opts res_bndr dcpc
   | otherwise
   = return (badWorker, unitOL res_bndr, varToCoreExpr res_bndr, nop_fn)
diff --git a/compiler/GHC/Types/Demand.hs b/compiler/GHC/Types/Demand.hs
index 9bd29a5a37..d4c8a5533d 100644
--- a/compiler/GHC/Types/Demand.hs
+++ b/compiler/GHC/Types/Demand.hs
@@ -830,11 +830,13 @@ unboxDeeplySubDmd (Prod _ ds) = mkProd Unboxed (strictMap unboxDeeplyDmd ds)
 unboxDeeplySubDmd call@Call{} = call
 
 -- | Sets 'Boxity' to 'Unboxed' for the 'Demand', recursing into 'Prod's.
+-- Don't recurse into lazy arguments; see GHC.Core.Opt.DmdAnal
+--    Note [No lazy, Unboxed demands in demand signature]
 unboxDeeplyDmd :: Demand -> Demand
 unboxDeeplyDmd AbsDmd   = AbsDmd
 unboxDeeplyDmd BotDmd   = BotDmd
-unboxDeeplyDmd (D n sd) = D n (unboxDeeplySubDmd sd)
-
+unboxDeeplyDmd dmd@(D n sd) | isStrict n = D n (unboxDeeplySubDmd sd)
+                            | otherwise  = dmd
 
 multSubDmd :: Card -> SubDemand -> SubDemand
 multSubDmd C_11 sd           = sd -- An optimisation, for when sd is a deep Prod
@@ -2619,7 +2621,7 @@ instance Outputable Demand where
 
 -- | See Note [Demand notation]
 instance Outputable SubDemand where
-  ppr (Poly b sd) = pp_boxity b <> ppr sd
+  ppr (Poly b n)  = pp_boxity b <> ppr n
   ppr (Call n sd) = char 'C' <> ppr n <> parens (ppr sd)
   ppr (Prod b ds) = pp_boxity b <> char 'P' <> parens (fields ds)
     where
diff --git a/testsuite/tests/simplCore/should_compile/T20103.stderr b/testsuite/tests/simplCore/should_compile/T20103.stderr
index 2f246eb985..c0f04a0ead 100644
--- a/testsuite/tests/simplCore/should_compile/T20103.stderr
+++ b/testsuite/tests/simplCore/should_compile/T20103.stderr
@@ -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!S>b, Cpr=b, Unf=OtherCon []]
+[GblId, Arity=1, Str=<S>b, Cpr=b, Unf=OtherCon []]
 lvl16
   = \ (wild1 :: CallStack) ->
       GHC.List.head1
diff --git a/testsuite/tests/stranal/sigs/BottomFromInnerLambda.stderr b/testsuite/tests/stranal/sigs/BottomFromInnerLambda.stderr
index 8784af67b7..953727a119 100644
--- a/testsuite/tests/stranal/sigs/BottomFromInnerLambda.stderr
+++ b/testsuite/tests/stranal/sigs/BottomFromInnerLambda.stderr
@@ -1,7 +1,7 @@
 
 ==================== Strictness signatures ====================
 BottomFromInnerLambda.expensive: <1!P(SL)>
-BottomFromInnerLambda.f: <1!S><1!S>b
+BottomFromInnerLambda.f: <1!P(S)><1!P(S)>b
 
 
 
@@ -13,6 +13,6 @@ BottomFromInnerLambda.f: b
 
 ==================== Strictness signatures ====================
 BottomFromInnerLambda.expensive: <1!P(1L)>
-BottomFromInnerLambda.f: <1!P(1!S)><1!S>b
+BottomFromInnerLambda.f: <1!P(1S)><1!P(S)>b
 
 
diff --git a/testsuite/tests/stranal/sigs/T21119.stderr b/testsuite/tests/stranal/sigs/T21119.stderr
index dade4dc2a6..ca60a36995 100644
--- a/testsuite/tests/stranal/sigs/T21119.stderr
+++ b/testsuite/tests/stranal/sigs/T21119.stderr
@@ -4,7 +4,7 @@ T21119.$fMyShow(,): <1!A>
 T21119.$fMyShowInt: <1!A>
 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(S)><1!B><S!S><S!S>b
+T21119.indexError: <1C1(S)><1!B><S!S><S>b
 T21119.throwIndexError: <MC1(L)><MA><L><L><L>x
 
 
@@ -24,7 +24,7 @@ T21119.$fMyShow(,): <1!A>
 T21119.$fMyShowInt: <1!A>
 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(S)><1!B><S!S><S!S>b
+T21119.indexError: <1C1(S)><1!B><S!S><S>b
 T21119.throwIndexError: <MC1(L)><MA><L><L><L>x
 
 
diff --git a/testsuite/tests/stranal/sigs/T21888.hs b/testsuite/tests/stranal/sigs/T21888.hs
new file mode 100644
index 0000000000..7b7daec85b
--- /dev/null
+++ b/testsuite/tests/stranal/sigs/T21888.hs
@@ -0,0 +1,63 @@
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+module Data.MemoTrie (HasTrie(..)) where
+
+import Control.Arrow (Arrow(first))
+import Data.Bits (Bits((.|.), shiftL))
+import Data.Kind (Type)
+
+infixr 0 :->:
+
+class HasTrie a where
+    data (:->:) a :: Type -> Type
+    enumerate :: (a :->: b) -> [(a,b)]
+
+instance HasTrie () where
+  newtype () :->: a = UnitTrie a
+  enumerate (UnitTrie a) = [((),a)]
+
+instance HasTrie Bool where
+  data Bool :->: x = BoolTrie x x
+  enumerate (BoolTrie f t) = [(False,f),(True,t)]
+
+instance (HasTrie a, HasTrie b) => HasTrie (Either a b) where
+  data (Either a b) :->: x = EitherTrie (a :->: x) (b :->: x)
+  enumerate (EitherTrie s t) = enum' Left s `weave` enum' Right t
+
+enum' :: (HasTrie a) => (a -> a') -> (a :->: b) -> [(a', b)]
+enum' f = (fmap.first) f . enumerate
+
+weave :: [a] -> [a] -> [a]
+[] `weave` as = as
+as `weave` [] = as
+(a:as) `weave` bs = a : (bs `weave` as)
+
+instance (HasTrie a, HasTrie b) => HasTrie (a,b) where
+  newtype (a,b) :->: x = PairTrie (a :->: (b :->: x))
+  enumerate (PairTrie tt) =
+    [ ((a,b),x) | (a,t) <- enumerate tt , (b,x) <- enumerate t ]
+
+instance HasTrie x => HasTrie [x] where
+  newtype [x] :->: a = ListTrie (Either () (x,[x]) :->: a)
+  enumerate (ListTrie t) = enum' list t
+
+list :: Either () (x,[x]) -> [x]
+list = either (const []) (uncurry (:))
+
+unbit :: Num t => Bool -> t
+unbit False = 0
+unbit True  = 1
+
+unbits :: (Num t, Bits t) => [Bool] -> t
+unbits [] = 0
+unbits (x:xs) = unbit x .|. shiftL (unbits xs) 1
+
+instance HasTrie Integer where
+  newtype Integer :->: a = IntegerTrie ((Bool,[Bool]) :->: a)
+  enumerate (IntegerTrie t) = enum' unbitsZ t
+
+unbitsZ :: (Num n, Bits n) => (Bool,[Bool]) -> n
+unbitsZ (positive,bs) = sig (unbits bs)
+ where
+   sig | positive  = id
+       | otherwise = negate
diff --git a/testsuite/tests/stranal/sigs/T21888.stderr b/testsuite/tests/stranal/sigs/T21888.stderr
new file mode 100644
index 0000000000..26681355f0
--- /dev/null
+++ b/testsuite/tests/stranal/sigs/T21888.stderr
@@ -0,0 +1,30 @@
+
+==================== Strictness signatures ====================
+Data.MemoTrie.$fHasTrie(): <L>
+Data.MemoTrie.$fHasTrie(,): <1C1(L)><LCS(L)><L>
+Data.MemoTrie.$fHasTrieBool: <1!P(L,L)>
+Data.MemoTrie.$fHasTrieEither: <1C1(L)><1C1(L)><1!P(L,L)>
+Data.MemoTrie.$fHasTrieInteger: <1!P(1!P(S,1!P(1!P(S,1L),1!P(S,1L))),1!P(S,1!P(1!P(S,1L),1!P(S,1L))))>b
+Data.MemoTrie.$fHasTrieList: <SCS(L)><1!P(L,L)>
+
+
+
+==================== Cpr signatures ====================
+Data.MemoTrie.$fHasTrie():
+Data.MemoTrie.$fHasTrie(,):
+Data.MemoTrie.$fHasTrieBool:
+Data.MemoTrie.$fHasTrieEither:
+Data.MemoTrie.$fHasTrieInteger:
+Data.MemoTrie.$fHasTrieList:
+
+
+
+==================== Strictness signatures ====================
+Data.MemoTrie.$fHasTrie(): <L>
+Data.MemoTrie.$fHasTrie(,): <1C1(L)><LCS(L)><L>
+Data.MemoTrie.$fHasTrieBool: <1!P(L,L)>
+Data.MemoTrie.$fHasTrieEither: <1C1(L)><1C1(L)><1!P(L,L)>
+Data.MemoTrie.$fHasTrieInteger: <1!P(1!P(B,1!P(1!P(B,1!P(L,L)),1!P(B,1!P(L,L)))),1!P(B,1!P(1!B,1!B)))>b
+Data.MemoTrie.$fHasTrieList: <SCS(L)><1!P(L,L)>
+
+
diff --git a/testsuite/tests/stranal/sigs/T21888a.hs b/testsuite/tests/stranal/sigs/T21888a.hs
new file mode 100644
index 0000000000..6a72d89ec1
--- /dev/null
+++ b/testsuite/tests/stranal/sigs/T21888a.hs
@@ -0,0 +1,19 @@
+module T21888a where
+
+-- This tests case (B) of
+-- Note [No lazy, Unboxed demands in demand signature]
+-- in GHC.Core.Opt.DmdAnal
+
+-- We should get a worker-wrapper split on g
+-- and on wombat, even though f uses x unboxed
+
+{-# NOINLINE f #-}
+f x = Just x
+
+wombat :: Int -> a
+wombat x = error (show (f x))
+
+g :: Bool -> Int -> Int
+g True x  | x>0 = g True (x-1)
+          | otherwise = x+1
+g False x = wombat x
diff --git a/testsuite/tests/stranal/sigs/T21888a.stderr b/testsuite/tests/stranal/sigs/T21888a.stderr
new file mode 100644
index 0000000000..21127cc2a5
--- /dev/null
+++ b/testsuite/tests/stranal/sigs/T21888a.stderr
@@ -0,0 +1,21 @@
+
+==================== Strictness signatures ====================
+T21888a.f: <L>
+T21888a.g: <1L><S!P(L)>
+T21888a.wombat: <S!P(S)>b
+
+
+
+==================== Cpr signatures ====================
+T21888a.f: 2
+T21888a.g: 1
+T21888a.wombat: b
+
+
+
+==================== Strictness signatures ====================
+T21888a.f: <L>
+T21888a.g: <1L><1!P(L)>
+T21888a.wombat: <1!P(S)>b
+
+
diff --git a/testsuite/tests/stranal/sigs/UnsatFun.stderr b/testsuite/tests/stranal/sigs/UnsatFun.stderr
index c659311b22..cb606f5c02 100644
--- a/testsuite/tests/stranal/sigs/UnsatFun.stderr
+++ b/testsuite/tests/stranal/sigs/UnsatFun.stderr
@@ -1,7 +1,7 @@
 
 ==================== Strictness signatures ====================
-UnsatFun.f: <1!S><B>b
-UnsatFun.g: <1!S>b
+UnsatFun.f: <1!P(S)><B>b
+UnsatFun.g: <1!P(S)>b
 UnsatFun.g': <MS>
 UnsatFun.g3: <A>
 UnsatFun.h: <1C1(L)>
@@ -22,8 +22,8 @@ UnsatFun.h3: 1
 
 
 ==================== Strictness signatures ====================
-UnsatFun.f: <1!S><B>b
-UnsatFun.g: <1!S>b
+UnsatFun.f: <1!P(S)><B>b
+UnsatFun.g: <1!P(S)>b
 UnsatFun.g': <MS>
 UnsatFun.g3: <A>
 UnsatFun.h: <1C1(L)>
diff --git a/testsuite/tests/stranal/sigs/all.T b/testsuite/tests/stranal/sigs/all.T
index 3ebfe287ec..211cbda94d 100644
--- a/testsuite/tests/stranal/sigs/all.T
+++ b/testsuite/tests/stranal/sigs/all.T
@@ -33,3 +33,5 @@ test('T20746', normal, compile, [''])
 test('T20746b', normal, compile, [''])
 test('T21081', normal, compile, [''])
 test('T21119', normal, compile, [''])
+test('T21888', normal, compile, [''])
+test('T21888a', normal, compile, [''])