[Agda] Avoiding η-contraction

[Andreas Abel]

Hi Andres,

eta-contraction is also used in instantiateFull:

bodrum:Agda abel$ findhs etaOnce
./TypeChecking/EtaContract.hs:etaContract = traverseTermM etaOnce
./TypeChecking/EtaContract.hs:etaOnce :: Term -> TCM Term
./TypeChecking/EtaContract.hs:etaOnce v = do
./TypeChecking/Reduce.hs:    instantiateFull v = etaOnce =<< do -- 
Andreas, 2010-11-12 DONT ETA!! eta-reduction breaks subject reduction
./TypeChecking/Reduce.hs:-- but removing etaOnce now breaks everything

Eta-contraction is discussed in connection with issue 361

   https://code.google.com/p/agda/issues/detail?id=361

When I tried to shut off eta-contraction, some examples in the std-lib 
did not type-check any more.  However, for just some toy examples, you 
might be lucky.

Cheers,
Andreas

On 03.03.13 4:42 PM, Andrés Sicard-Ramírez wrote:
> 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,
>

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/