Variable occurrences can have at least arity 1
Consider
f x y = case x of
True -> y
False -> \z u -> z u
Can we eta-expand to
f1 x y z = case x of
True -> y z
False -> \u -> z u
Yes! We are pushing y
under that \z
, but that's ok: evaluating y
multiple times won't lose any sharing; it's cheap to do so. But currently we aren't, because y
is lambda-bound and thus assumed to have arity 0.
But eta-expanding f1
once more, we get
f2 x y z u = case x of
True -> y z u
False -> z u
And that is not OK, because we'd be pushing a potential redex (y z)
under a lambda (\u
).
It seems that variable occurrences, even of let-bound identifiers, can assumed to always have at least arity 1 and we should see if exploiting that is beneficial.