[Agda] memory eagerness

[Sergei Meshveliani]

Dear Agda developers,

  http://www.botik.ru/pub/local/Mechveliani/agdaNotes/rep3.zip

contains a certain algebra application in  
                                   Agda 2.3.2, MAlonzo, lib-0.7.

(this letter repeats its  readme.txt).

It declares various definitions:
  Set, Semigroup, ..., Ring, Field,
  Subset, Subsemigroup, ..., Ideal, 
  ResidueRing constructor.

The modules are:
  Nat2.agda          List2.agda        DPrelude.agda 
  AlgClasses01.agda  AlgClasses2.agda  AlgClasses1.agda    
  AlgClasses3.agda   ResidueI.agda
  Main.agda  

The longest one has about  250 lines  of a proper source code.

And it needs more than  6 Gb  memory to type check: 

  agda -c -i . -i $agdaStLib +RTS -K200m -M8000m -RTS Main.agda

(-M6000m  is not enough). 
   

This code does not describe any involved computation, these are 
only simple definitions of several known things
(and about 3 pages of proofs for simple things).
And Agda has only to "read and understand" them, no run-time evaluation 
is required at this stage.

  
* Please, can you look into this project and give an advice:
  what can be a way out?
  (because the project looks as being stuck).

* Is this due to the type checker or, may be, due to that I apply 
  a wrong programming style?

Earlier, the Agda team already listed 4-5 possible reasons for the
result code explosion.
But now the question is more concrete:  6 Gb is overfilled, the 
program is not large, and I do not know how to continue.


Concerning the style, I see the following points.


1. Record  vs  ordinary module
------------------------------

For example, the record  Group
has a parameter :  UpMonoid c l
and a single       field  totalInversion : ...

There are also several related auxiliary functions 
(defined via the parameter and  field  totalInversion)
and their proved lemmata:
  division,  proof for  inv (x * y) == (inv y) * (inv x),
  for  inv (inv x) == x,   and such.

And I put all them into this very record, so that it exports them
(because a record is also a module).

Their code size is about 20 times larger than the proper Group 
record part. And it can grow further several times, because 
there are many useful lemmata about groups.

I think, so far, that this is a natural style. Is it?

Another design may be:
to create
   module Group-related (G : Group ...) 
   where
   ...

and move there the above Group related items, so that the proper 
Group  record will become a small code.
Will this approach save much space in the type-check?

2. open, open - public
----------------------

There are many levels in this record hierarchy (may be, 15-20).
I apply  `open' and `open - public'  in order to have a shorter
path from the top level to an operation on a lower level.
For example, the path to reach  _+_  from  Field  is
  EuclideanRing   --> IntegralRing --> RingWithOne -->
  CommutativeRing --> Ring         --> Ringoid     -->  _+_
  
I do not know, may be something large is copied due to this 
nested `open' declarations
-- ?

Thank you advance for explanation,

------
Sergei