[Agda] type check performance

[Sergei Meshveliani]

Dear Agda developers,

I am writing in Agda a library for algebra. And the project is (mainly)
stuck due to that  Agda 2.4.2.3  takes too much space and time to
type-check the current module.

While the project was developing, it was first sufficient  7 Gb space,
then it required  9 Gb,  and now it requires 14 Gb. 

If I continue this way, then very soon it will overfill 16 Gb,
and there will arise the problem of upgrading my computer.
May be, it can be upgraded, I do not know. But this space eagerness
looks very unnatural.
 
There are many modules in the project, and the (currently) last module
Foo.agda  has only about 130 nonempty lines. 
All the previous modules are type-checked in 1-2 hours.
After this, to type check  Foo.agda  takes 
                    40 minutes  under the options of  -M14G -H14G.
 
And under  -M9G -H9G,  it does not finish in 4 hours (and I have
interrupted it). 

The current aim of the project is to see of whether it is practically
possible to program in Agda a certain essential piece of the classical
computational algebra. It follows textbooks on algebra, only full formal
proofs need to be provided.
1) Currently, it describes the classical structures, from DecidableSet 
   and Semigroup up to UniqueFactorizationRing.
2) It proves many simple statements about these structures.
3) Factorization  in an  IntegralRing R  uses a Multiset over prime  
   assoc-classes as keys. An assoc-class [a] consists of the elements
which differ from  a \in R  in an invertible factor. And assoc-classes
for all nonzero  a \in R  form an  UniqueFactorizationMonoid UFM.
4) This  UFM  is used to define what is a  UniqueFactorizationRing.
5) Only simple classical statements are proved, the ones known from
textbooks. 

Finally,  Foo.agda  defines this  UniqueFactorizationRing.

This all constitutes less than 1/100 of any reasonable algebraic
library.

First, I thought of that composing Agda proofs takes too much effort.
Then, after a certain initial library part (mainly, lists and
association lists) has been done, composing proofs has become easier.

And now the project is stuck not due to the difficulties with formal
profs, but just due to the memory eagerness of Agda.

May I send the source privately to someone in the Agda team?

I mean that, may be, you can tell what is the matter with this
Foo.agda,  may be, you can tell how to squeeze its type check space. 
(As usual, I am going to put the source public after the current release
is ready). 

1) `with --> case_of_'  is often difficult to arrange, I have given up.
2) Almost all of the proofs can be set under `abstract'.
   But `abstract' is applicable only at the top level, and this prevents
   almost all cases where it can be applied.

Is the main type check inefficiency due to call by name in the
normalizer?

Regards,

------
Sergei