Demand analysis can produce unsound signatures
Consider
f :: Bool -> (Int, Int)
f True = (n,error "m")
f False = (error "m",n)
g :: (Bool -> (Int, Int)) -> Int
-- Inferred strictness <SCS(P(1L,1L))>
g h = fst (h True) + snd (h False)
{-# NOINLINE g #-}
The idea here is to call g
with f
at the top-level. We can see that it just barely plays out and we don't evaluate any of the error
s, because g
switches from fst
to snd
at the same time as it flips the boolean flag.
This is the signature we infer for g
:
<SCS(P(1L,1L))>
Note the P(1L,1L)
. This is wrong, because it says that g
calls its argment (more than once), and that g
evaluates both components of the result of each call.
The whole demand says "g's arg is called multiple times and we'll evalauate both components of the result". That is unfortunately unsound! Not every call evaluates both components and as f
shows, what is stored in the components may vary from call to call.
Fortunately, I can't find a way to make GHC exploit the unsoundness. But one idea for the future (!5349) is to analyse f
's RHS assuming the demand it is put on in its body. If g f
is the only use of f
, we may put P(1L,1L)
on (n,error "m")
and crash on every call to f
. Urgh!
The fix is to Lub sd1
and sd2
when we have plusSubDmd C(n1:*sd1) C(n2:*sd2)
. Currently, we Plus them if n1
and n2
are strict.