Consider a demand `n :* sd` on a binding `let x = e in <body>`.
(Similarly, a call sub-demand `Cn(sd)` on a lambda `\_. e`).
While `n` describes how *often* `x` had been evaluated in <body>,
the sub-demand `sd` describes how *deep* `e` has been evaluated, under the
following
PREMISE: *for all program traces where `x` had been evaluated at all*
That is, `sd` disregards all program traces where `x` had not been evaluated,
because it can't describe the depth of an evaluation that never happened.
NB: The Premise only makes a difference for lower bounds/strictness.
Upper bounds/usage are unaffected by adding or leaving out evaluations that
never happen.
The Premise comes into play when we have lazy Demands. For example, if `x` was
demanded with `LP(SL,A)`, so perhaps the full expression was
let x = (e1, e2) in (x `seq` fun y `seq` case x of (a,b) -> a, True)
then `x` will be evaluated lazily, but in any trace in which `x` is evaluated,
the pair in its RHS will ultimately be evaluated deeply with sub-demand
`P(SL,A)`. That means that `e1` is ultimately evaluated strictly, even though
evaluation of the field does not directly follow the eval of `x` due to the
intermittent call `fun y`.
How does the additional strictness help? The long version is the list of
examples at the end of this Note (as procured in #21081 and #18903).
The short version is
* We get to take advantage of call-by-value/let-to-case in more situations,
as for e1 above. See example "More let-to-case" below.
* Note [Eta reduction based on evaluation context] applies in more situations.
See example "More eta reduction" below.
* We get to unbox more results, see example "More CPR" below.
It seems like we don't give up anything in return. Indeed that is the case:
* If we dropped the Premise, then a lazy `n` in `nP(m..)` would always force
`m` to be lazy, too. That is quite redundant! It seems wasteful not to use
the lower bound of `m` for something more useful. So indeed we give up on
nothing in return for some nice wins.
* Even if `n` is absent (so the Premise does hold for no trace whatsoever),
it's pretty easy to describe how `e` was evaluated. Answer: 'botSubDmd'.
We use it when expanding 'Absent' and 'Bottom' demands in 'viewDmdPair' as
well as when expanding absent 'Poly's to 'Call' sub-demands in 'viewCall'.
Of course, we now have to maintain the Premise when we unpack and rebuild
Demands. For strict demands, we know that the Premise indeed always holds for
any program trace abstracted over, whereas we have to be careful for lazy
demands.
In particular, when doing `plusDmd` we have to *lazify* the nested SubDemand
if the outer cardinality is lazy. E.g.,
LP(SL) + SP(L) = (L+S)P((M*SL)+L) = SP(L+L) = SP(L)
Multiplying with `M`/`C_01` is the "lazify" part here and is implemented in
`lazifyIfStrict`. Example proving that point:
d2 :: <LP(SL)><SP(A)>
d2 x y = y `seq` (case x of (a,b) -> a, True)
What is the demand on x in (d2 x x)? NOT SP(SL)!!
We used to apply the same reasoning to Call SubDemands `Cn(sd)` in `plusSubDmd`,
but that led to #21717, because different calls return different heap objects.
See Note [Call SubDemand vs. evaluation Demand].
There are a couple more examples that improve in T21081.
Here is a selection of those examples demonstrating the usefulness of The
Premise:
* "More let-to-case" (from testcase T21081):
```hs
f :: (Bool, Bool) -> (Bool, Bool)
f pr = (case pr of (a,b) -> a /= b, True)
g :: Int -> (Bool, Bool)
g x = let y = let z = odd x in (z,z) in f y
```
Although `f` is lazy in `pr`, we could case-bind `z` because it is always
evaluated when `y` is evaluated. So we give `pr` demand `LP(SL,SL)`
(most likely with better upper bounds/usage) and demand analysis then
infers a strict demand for `z`.
* "More eta reduction" (from testcase T21081):
```hs
myfoldl :: (a -> b -> a) -> a -> [b] -> a
myfoldl f z [] = z
myfoldl f !z (x:xs) = myfoldl (\a b -> f a b) (f z x) xs
```
Here, we can give `f` a demand of `LC(S,C(1,L))` (instead of the lazier
`LC(L,C(1,L))`) which says "Whenever `f` is evaluated (lazily), it is also
called with two arguments".
And Note [Eta reduction based on evaluation context] means we can rewrite
`\a b -> f a b` to `f` in the call site of `myfoldl`. Nice!
* "More CPR" (from testcase T18903):
```hs
h :: Int -> Int
h m =
let g :: Int -> (Int,Int)
g 1 = (m, 0)
g n = (2 * n, 2 `div` n)
{-# NOINLINE g #