Note [Eta reduction makes sense]

GHC's eta reduction transforms
   \x y. <fun> x y  --->  <fun>
We discuss when this is /sound/ in Note [Eta reduction soundness].
But even assuming it is sound, when is it /desirable/.  That
is what we discuss here.

This test is made by `ok_fun` in tryEtaReduce.

1. We want to eta-reduce only if we get all the way to a trivial
   expression; we don't want to remove extra lambdas unless we are
   going to avoid allocating this thing altogether.

   Trivial means *including* casts and type lambdas:
     * `\x. f x |> co  -->  f |> (ty(x) -> co)` (provided `co` doesn't mention `x`)
     * `/\a. \x. f @(Maybe a) x -->  /\a. f @(Maybe a)`
   See Note [Do not eta reduce PAPs] for why we insist on a trivial head.

Of course, eta reduction is not always sound. See Note [Eta reduction soundness]
for when it is.

When there are multiple arguments, we might get multiple eta-redexes. Example:
   \x y. e x y
   ==> { reduce \y. (e x) y in context \x._ }
   \x. e x
   ==> { reduce \x. e x in context _ }
   e
And (1) implies that we never want to stop with `\x. e x`, because that is not a
trivial expression. So in practice, the implementation works by considering a
whole group of leading lambdas to reduce.

These delicacies are why we don't simply use 'exprIsTrivial' and 'exprIsHNF'
in 'tryEtaReduce'. Alas.