Re: [Agda] Avoiding η-contraction

[Andrés Sicard-Ramírez]

On Mon, Mar 4, 2013 at 1:59 AM, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:
> 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
>
>
> 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.
>

Thanks Andreas! Removing etaOnce worked for my toy examples.

Best,
-- 
Andrés