[Agda] type check cost

[Sergei Meshveliani]

Dear Agda developers,

Please, investigate the possibility to reduce the type check cost
for Agda programs.


Example of application
----------------------

The library DoCon-A-0.04.1 needs the minimum of  8 Gb 
heap to type-check at a single command,
and for -M8G, the time is  60 minutes  for a 3 GHz machine.

DoCon-A-2.00  needs the minimum of  11 Gb,  and it takes  70 minutes.

DoCon-A-2.00  adds several methods. But there is only one of them 
that may pretend to complicate type-checking. This is a proof for 
an optimized method for fraction addition. There is a hierarchy of 
parametrized modules. The method does not bring any new structures or 
new parametrized module, but it uses several instances of existing 
modules.

In both programs, the longest type-check place is the module    
                                                      Int.Integer2
(1/5 of all the time).
This is because it uses certain instances of almost all the generic 
structures and imports certain instances of all parametric modules
implemented in the DoCon-A library.

Now, each step in developing the library will probably increase the 
memory requirement on somewhat 1/4.

On the other hand, DoCon-A-2.00 supports only about 1/100 of the methods
in the DoCon library written in Haskell in 1990-ies
(but it contains many definitions and proofs which are not in DoCon).



This is not my personal problem
-------------------------------
I expect that anyone who tries to implement any essential generic 
mathematical library in Agda will be stopped by this barrier.


Main problem
------------
Probably, this is an internal type representation that does not really 
use sharing, so that large subterms are copied many times.


I also have a specific question
-------------------------------

I wrote earlier of the example, when type-checking  (s , t)  costs
infinitely much, while adding the type declaration for this pair makes
it cost small. And I expect that in the first variant the result is
going to be "unsolved metas".

DoCon-A-2.00 takes 70 minutes to type-check for the -M11G option.
May it happen so that adding a type declaration somewhere in a lucky
place will reduces the cost essentially?

Regards,

------
Sergei