[Agda] Avoiding η-contraction

[Andrés Sicard-Ramírez]

Hi,

Given for example

postulate
  D   : Set
  A   : D → Set
  ∃   : (A : D → Set) → Set
  foo : ∀ d → A d → ∃ (λ e → A e)
  bar : ∀ d → A d → ∃ A

I know that the *internal* representation of foo and bar are the same
because Agda η-contracts the types.

For debugging my program, I need to avoid the η-contraction performed
by Agda, so I replaced in the module Agda.TypeChecking.EtaContract the
function

etaContract :: TermLike a => a -> TCM a
etaContract = traverseTermM etaOnce

by

etaContract = return

but it didn't avoid the η-contraction.

How can I avoid the η-contraction on the internal representation?

Thanks,

-- 
Andrés