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