[GHC] #9440: Buggy binder swap in occurrence analysis

[GHC]

#9440: Buggy binder swap in occurrence analysis
-------------------------------------+-------------------------------------
       Reporter:  afarmer            |                   Owner:
           Type:  bug                |                  Status:  new
       Priority:  normal             |               Milestone:
      Component:  Compiler           |                 Version:  7.8.3
       Keywords:                     |        Operating System:
   Architecture:  Unknown/Multiple   |  Unknown/Multiple
     Difficulty:  Unknown            |         Type of failure:
     Blocked By:                     |  None/Unknown
Related Tickets:                     |               Test Case:
                                     |                Blocking:
                                     |  Differential Revisions:
-------------------------------------+-------------------------------------
 Occurrence analysis on case alternatives performs a "binder swap", whereby
 occurrences of the scrutinee in alternative RHSs are replaced by the case
 binder when the scrutinee is a variable or a casted variable.

 {{{
 case x of w
   C vs -> rhs
 ===
 case x of w
   C vs -> let x = w in rhs
 }}}

 This should check two conditions, mentioned in Note [Binder swap].

   (a) x is free in `C vs -> rhs`, otherwise one of two bad things happen:
         1) it is pointless
         2) new binding of x would capture one of the alternative binders
 (vs)
   (b) w is not in vs

 Neither of these conditions is actually being checked.

 Additionally, the binder swap happens in the presence of casts:

 {{{
 case x |> co of w
   C vs -> rhs
 ===
 case x |> co of w
   C vs -> let x = w |> sym co in rhs
 }}}

 But the analysis is not returning usage info for free coercion variables
 in co.

 Condition (a) bit us in HERMIT when running `occurAnalyseExpr` on the
 following expression resulting from unfolding nested calls to `fst`:

 {{{
 case x_X11b of wild_a3YB
   (,) x_a3YD ds1_a3YE ->
     case x_a3YD of wild_a3YB
       (,) x_a3YD ds1_a3YE -> x_a3YD
 }}}

 The analysis would erroneously result in:

 {{{
 case x_X11b of wild_a3YB
   (,) x_a3YD ds1_a3YE ->
     case x_a3YD of wild_a3YB
       (,) x_a3YD ds1_a3YE -> let x_a3YD = wild_a3YB in x_a3YD
 }}}

 which is clearly Not Good.

 Patch forthcoming via Phabricator. Unfortunately, I don't have a good test
 case that doesn't involve HERMIT, but can confirm this patch fixes the
 problem above.

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