Agda internally eta-reduces when it shouldn't

[omelkonian]

A sub-bug of #273 is that Agda is performing an η-reduction that creates a mismatch between what the user wrote and what the user gets on the Haskell side, e.g.

open import Haskell.Prelude

postulate f : Int → Int

test : Int → Int
test x = f x
{-# COMPILE AGDA2HS test #-}

test :: Int -> Int
test = f

We could investigate how to either instruct Agda not to do these, or reverse the effect if that's impossible in Agda internals.