[Agda] no-eta-equality

[Sergei Meshveliani]

To my question on --no-eta-equality

> > Now, if  "fst x , snd x" and "x"  are only going to be 
> > propositionally equal,  why does this reduce the memory size when >
> > type-checking?


On Mon, 2016-09-26 at 15:01 +0200, Andrea Vezzosi wrote:

> As far as I'm aware the biggest benefit comes in combination with
> copatterns, and it's because more things will be compared "by name"
> rather than structurally, so there's less reduction and possibly less
> expansion of terms going on.
> 

I looked into 
         https://gist.github.com/puffnfresh/8960574

to find out of what is a copattern:

  {-# OPTIONS --copatterns #-}

  record _×_ (A B : Set) : Set where
    constructor _,_
    field
      fst : A
      snd : B
  open _×_

  pair : {A B : Set} → A → B → A × B
  fst (pair a b) = a                     -- (1)
  snd (pair a b) = b                     -- (2)

Probably, this implements the function `pair' on types by saying that it
satisfies the equations (1) and (2). 
(?)

Now, my program declares many records (a hierarchy of algebraic
structures). For example (contrived):

  record Foo (A : Set) : Set where  
                             constructor foo
                             field f1  : A
                                   nat : Nat
  open Foo

And in order to reduce the type checking cost, it has sense 
1) to prefix the files with
   {-# OPTIONS --copatterns #-},

2) to set there  no-eta-equality  before `constructor',

3) to add the functions like

  makeFoo : {A : Set} → A → Foo A 
  f1  (makeFoo a _) = a                    
  nat (makeFoo _ n) = n,

that is to add the projection equation for each record field.

And after this, the type check cost for this program has a chance to
reduce essentially
(no matter of whether  makeFoo  is used anywhere or not?).

(The program will be so that it defines the projection equations without
explicitly using them anywhere).

Do I understand correct?

Thank you for explanations,

------
Sergei