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.

Trac metadata

Trac field	Value
Version	7.8.3
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture