[Agda] no-eta-equality

[Sergei Meshveliani]

People,
I am trying to use the  no-eta-equality  key in order to reduce space
eagerness of the type checker.

And there arise several questions.

1. Currently the project is successfully type-checked by
   agda $agdaLibOpt +RTS ... -RTS TypeCheckAll.agda

Now, I set  {-# OPTIONS --no-eta-equality #-} 
to the head of each .agda file.

Then, several files are type-checked, and others are not. 
Is this a bug in Agda? 

2. Does the above {-# OPTIONS --no-eta-equality #-} apply only to
records, or to all functions?

3. I understand eta-equality as that Agda converts 
   lambda x.(f x) --> f,  everywhere where x does not occur in the
lambda term f
-- is Agda so?   
Also record is internally related to a lambda term, where the above x is
matched against the record labels
-- is this so?

4. In my program,  Semigroup, Group, Ring ... (many of them) are records
in which one structure is often a field value for another structure.
Do I need to set  --no-eta-equality  not to the whole files but
individually to each record declaration of Semigroup, Group, Ring ...,
and not to touch other parts?

Thanks,

------
Sergei