[GHC] #16296: OccurAnal should not break the linter assumptions

[GHC]

#16296: OccurAnal should not break the linter assumptions
-------------------------------------+-------------------------------------
           Reporter:  aspiwack       |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.6.3
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 As discovered in #16288 (see in particular
 https://ghc.haskell.org/trac/ghc/ticket/16288#comment:2), the
 implementation of the binder-swap transformation in the occurrence
 analysis sometimes produces terms which would be refused by the linter.

 Specifically:

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

 Becomes

 {{{#!hs
 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.

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16296>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler