Opened 7 months ago

Last modified 7 months ago

#16296 new bug

OccurAnal should not break the linter assumptions

Reported by: aspiwack Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.6.3
Keywords: Simplifier Cc: monoidal, simonpj
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:


As discovered in #16288 (see in particular, the implementation of the binder-swap transformation in the occurrence analysis sometimes produces terms which would be refused by the linter.


case A.x of u { pat -> rhs }


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 has shown, this is not always the case! (specifically, in #16288, 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.

Change History (3)

comment:1 Changed 7 months ago by simonpj

Keywords: Simplifier added

comment:2 Changed 7 months ago by simonpj

I wrote a quick fix, which has now landed as]

But it's not the Right Solution; it's messy, and it loses some useful optimisations, namely

case Imported.x of
  True -> .....(case Imported.x of { True -> e1; False -> e2 })......
  False -> ...

We'd like the inner case to disappear, but now it won't.

I think the right solution is as outlined in the Description.

comment:3 Changed 7 months ago by Matthew Pickering <matthewtpickering@…>

In 0eb7cf03/ghc:

Don't do binder-swap for GlobalIds

This patch disables the binder-swap transformation in the
(relatively rare) case when the scrutinee is a GlobalId.
Reason: we are getting Lint errors so that GHC doesn't
even validate.  Trac #16346.

This is NOT the final solution -- it's just a stop-gap
to get us running again.

The final solution is in Trac #16296
Note: See TracTickets for help on using tickets.