[Agda] agda slow

[Nils Anders Danielsson]

On 2015-06-02 18:44, Andrea Vezzosi wrote:
> One hacky way would be to declare them coinductive, that would disable
> eta but also pattern matching.
>
> record Foo .. : Set where
>     coinductive
>     field
>        bar : ...

Another hack:

   record Σ (A : Set) (B : A → Set) : Set where
     inductive
     field
       fst   : A
       snd   : B fst
       dummy : ⊥ → Σ A B

And another one:

   Make-Agda-believe-that-the-type-is-recursive : Set → Bool → Set
   Make-Agda-believe-that-the-type-is-recursive _ true  = ⊤
   Make-Agda-believe-that-the-type-is-recursive A false = A

   record Σ (A : Set) (B : A → Set) : Set where
     inductive
     constructor internal-Σ-constructor
     field
       fst    : A
       snd    : B fst
       dummy₁ : Bool
       dummy₂ : dummy₁ ≡ true
       dummy₃ : Make-Agda-believe-that-the-type-is-recursive
                  (Σ A B) dummy₁

   pattern _,_ x y = internal-Σ-constructor x y true refl _

More seriously, I think there used to be an undocumented pragma that
turned off η-equality, but it seems to have been removed.

> On Tue, Jun 2, 2015 at 6:03 PM, Thorsten Altenkirch
> <Thorsten.Altenkirch at nottingham.ac.uk> wrote:
>> I was just starting to use some records to restructure some code we
>> are working on and the memory goes through the roof.

Can you report this on the bug tracker? Please include the two versions
of the code (one with lower memory consumption, and one with higher).

-- 
/NAD