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.