[Agda] result code explosion

[Serge D. Mechveliani]

Dear Agda developers,

there is a certain problem with the memory expenses, intermediate and 
final code explosion.

Do you consider the ways to reduce the produced code size?

I do understand that 
* Agda is not Haskell; checking dependent types looks like an heavy 
  problem, there may be even a fundamental reason of why it may take a 
  lot of memory/time,
* it may occur that my application code can be optimized many times 
  with respect to memory (this is my first experience with dependent 
  types).

But let me describe the situation, just to inform you of what is 
happining, for any occasion.

When type-checking my module  AlgClasses2.agda,
Agda-2.3.2 MAlonzo (lib-0.7, ghc-7.6.2)
takes about 800 Mb memory.
On 1 Gb machine, the system starts swapping at this and slows down 
considerably.
All right, we have extended RAM, and this example is passed.

Now consider the type checker memory eagerness. 
The module has about  400 lines of Agda source 
-- counting without comments and empty lines.
This is quite large. So, one who got used to Haskell, would expect that 
its processing would take the miminum of, say, 40 Mb.
My impression is that the type checker spends somewhat  20 times more
of memory than the GHC compiler spends for the Haskell code of the same 
size. 

Concerning the code size:
                         1.034.755 b   AlgClasses2.agdai

                         2.862.400 b   AlgClasses2.hi
                         1.073.333 b   AlgClasses2.hs  -- 23413 lines
                         2.927.256 b   AlgClasses2.o

400 lines of Agda  have converted to  23413 lines of the Haskell code. 

The executable has about  14 M byte.
My DoCon has about 100 times larger Haskell code for the demo program, 
and GHC produces the executable of about  13 M byte.

So far, I never tried  to run  this AlgClasses2 executable, I expect 
adventures at run time
(it has many nested `classes', but for really running it, I need to add
implementation for various instances). 

All right, Agda is not Haskell, and I expected the effect of this kind. 

But: may be something can be done?

About this particular application
---------------------------------
It describes the algebraic `classes' from  DSet  to  Ring, GCDRing,
                                  FactorizationRing, EuclidanRing, Field.   
Also it describes  
        Subset, Subsemigroup, ..., Subring, Ideal, ReductionIdeal.

This makes it many  records,  some of which are nested to the depth of 
about 15 -- 20 levels. Typically such a record has 2 fields and also 
exports about 8 items which are implemented via these fields. Such a 
record looks almost like an usual program module, but has a couple of 
fields.

I do not know, may be there is a particular reason of why this all 
causes a certain Haskell code explosion. 

But at least it is compiled (!), and I hope to reach running examples, 
and to see further.

Regards,

------
Sergei