[Agda] type check cost

[mechvel at scico.botik.ru]

Dear Agda developers,

Currently I use  Agda 2.4.2.4  to develop my algebraic library called 
DoCon-A.
And it cannot type-check on a machine of  16 Gb RAM.

First, I had an impression that Agda 2.4.2.4 spends 3 times less space 
(on DoCon-A)
than the previous version.
Now, it looks like this factor is about  1.3.
Small additions have been done to a couple of modules in the project, 
and the type check space
grows to 16 Gb.

The type checker has  n^2,  or may be an exponent, somewhere in it.
You have observed a simple example on this subject, and generally, you 
have a more clear idea
about the source of this effect.

Currently I am not stuck with the DoCon-A library, because I have an 
access to a 24 Gb machine.
But as the type checker has at least n^2 inside, this `currently' will 
hardly last more than 6 months
of the project development.

Also you understand that even 2 Gb is unnaturally large space for 
type-checking it.
This library is currently only a toy application, it has not any 
advanced methods, so far,
it has only some definitions taken from textbooks on algebra.

It is evident that some radical improvements are desirable for the type 
check method.

Regards,

------
Sergei