[Haskell-cafe] Can eta-reduction of (\xs -> augment (flip (flip . foldr) xs)) typecheck?

[Viktor Dukhovni]

With both `augment` and `foldr` from GHC.Base:

    augment :: (forall b. (a -> b -> b) -> b -> b) -> [a] -> [a]
    augment g = g (:)

    foldr :: (a -> b -> b) -> b -> [a] -> b
    ...

The function:

    \xs -> augment (g xs) where g xs c z = foldr c z xs
    -- pointfree: g == flip (flip . foldr)

typechecks (it is in fact just (++))

    λ> let g xs c z = foldr c z xs
    λ> :t \xs -> augment (g xs)
    \xs -> augment (g xs) :: [a] -> [a] -> [a]

Is it possible to explicitly type annotate some `g'` so that the
function:

    (\xs -> (augment . g') xs) :: [a] -> [a] -> [a]

is also just (++).  That is, basically `g'` is the same as g, but with
an explicit type signature that makes the type checker accept the
eta-reduced composition?  A completely naive attempt, with no
type annotations yields:

    λ> let g xs c z = foldr c z xs
    λ> :t g
    g :: [a] -> (a -> b -> b) -> b -> b
    λ> :t (augment . g)

    <interactive>:1:2: error:
        • Couldn't match type: forall b. (a1 -> b -> b) -> b -> b
                         with: (a -> b0 -> b0) -> b0 -> b0
          Expected: ((a -> b0 -> b0) -> b0 -> b0) -> [a1] -> [a1]
            Actual: (forall b. (a1 -> b -> b) -> b -> b) -> [a1] -> [a1]
        • In the first argument of ‘(.)’, namely ‘augment’
          In the expression: augment . g

I haven't found any variant type signatures for "g" that make this go.

I think this may require impredicative polymorphism, and so can't be
done until perhaps QuickLook lands (don't know whether that'll be
enough).

-- 
    Viktor.