Buggy binder swap in occurrence analysis
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:
- it is pointless
- 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
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.