Abortion of fixed-point iteration in Demand Analyser discards sound results
Consider the following program:
-- Extracted from T4903
module Foo where
data Tree = Bin Tree Tree
tree :: Tree
tree = Bin tree tree
eq :: Tree -> Bool
eq (Bin l r) = eq l && eq req amounts to the following Core:
eq
= \ (ds_d20O :: Tree) ->
case ds_d20O of { Bin l_aY8 r_aY9 ->
case eq l_aY8 of {
False -> False;
True -> eq r_aY9
}
}It clearly diverges. That's also what pure strictness/termination/CPR analysis would find out. But because usage analysis can't find out in finite time (and that's fine) that eq uses its argument completely, we abort fixed-point iteration [1] and return nopSig, discarding useful and sound strictness information we found out along the way, like the fact that it diverges.
This isn't hard to fix: Just track which parts of the signature were still unsound during abortion and only zap them. I'm only recording this for posterity and as an argument in a discussion I'll maybe start in a few months of time...
[1] This is the ascending chain of demands on ds_d20O during fixed-point iteration:
H
U(1*H,1*H)
U(1*U(1*H,1*H),1*U(1*H,1*H))
...Trac metadata
| Trac field | Value |
|---|---|
| Version | 8.6.3 |
| Type | Task |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture |