Eta-reduction based on Demand

This is a play on #20040 (closed), although a bit simpler and thus well within reach without #21081 (closed). Consider

f :: (Int -> Int -> Int) -> Int
f c = c 1 2 + c 3 4
{-# NOINLINE f #-}
-- Demand signature of f : <SCS(C1(L))>

g :: (Int -> Int -> Int) -> Int
g c = f (\x y -> c x y)

Today, we get the following Core for g:

g :: (Int -> Int -> Int) -> Int
[GblId, Arity=1, Unf=OtherCon []]
g = \ (c_awQ :: Int -> Int -> Int) ->
      f (\ (x_awR :: Int) (y_awS :: Int) -> c_awQ x_awR y_awS)

E.g., the lambda (\x y -> c x y) is not eta-reduced, although in theory it could be: From f's demand signature <SCS(C1(L))> we know that whenever f evaluates its parameter g, there is also at least one call to g with 2 arguments. Thus, eta-reducing to c is sound, even if evaluating c diverges, simply because the call to f would evaluate c either way.