OccurAnal should not break the linter assumptions
As discovered in #16288 (closed) (see in particular #16288 (closed)##16296 (closed)), the implementation of the binder-swap transformation in the occurrence analysis sometimes produces terms which would be refused by the linter.
Specifically:
case A.x of u { pat -> rhs }Becomes
case A.x of u { pat -> let x = u in rhs }Crucially, here, A.x (which is a global id) and x (which is a local id) have the same unique. This is so that x shadows A.x in rhs and captures all the occurrences of A.x in rhs. Which are now bound by x. But all these occurrences of A.x (which are now occurrences of x) are still marked as global ids. This is rejected by the linter.
The occurrence analysis is counting on the fact that there will be a simplifier step before the next linter fires, which will inline x and replace it by u everywhere.
As #16288 (closed) has shown, this is not always the case! (specifically, in #16288 (closed), occurrence analysis happens in an unfolding, but is not followed by a simplifier pass).
It's easy to fix such bugs: turn off binder-swap in occurrence analysis when not followed by the simplifier. But it is very fragile. So the longer term solution would be to never produce term which break the linter.
The entire reason for this let x = u is to avoid carrying a substitution in the occurrence analysis (and offload the work of actually doing the substitution to the simplifier). But the occurrence analysis will work through the entire rhs anyway. So it should be able to, at very little cost, propagate a substitution.
Trac metadata
| Trac field | Value |
|---|---|
| Version | 8.6.3 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | monoidal, simonpj |
| Operating system | |
| Architecture |