[Agda] no-eta-equality

[Sergei Meshveliani]

On Tue, 2016-09-27 at 15:00 +0200, Andrea Vezzosi wrote:
> No, doing that wouldn't be enough to see major improvements.
> 
> You have to change definitions that build elements of Foo into ones
> that do so by copatterns.


Consider the example:

  {-# OPTIONS --copatterns #-}
  record Rd (A : Set) : Set where no-eta-equality
                                  constructor rd
                                  field fl1 : A
                                        fl2 : ℕ
  open Rd

  sucRd :  {A : Set} → Rd A → Rd A
  sucRd (rd a n) =  rd a (suc n)

Suppose that I need to reduce the type check expense for a further
program that contains many functions that build elements of the type
family  Rd A.

Then I need to add the function 
 
  rd' :  {A : Set} → A → ℕ → Rd A  
  fl1 (rd' a _) = a
  fl2 (rd' _ n) = n

(where rd' looks like another version of the constructor  rd)

and to replace the function  sucRd  with 

  suc'Rd :  {A : Set} → Rd A → Rd A
  suc'Rd (rd a n) =  rd' a (suc n)

and to replace in a similar way other functions that build values of the
type family  Rd A. 

Do I understand this correct?
What things in this example will be compared "by name" rather than
structurally? 

Thank you in advance for explanation,

------
Sergei