[Agda] type check explosion

[Sergei Meshveliani]

Dear Agda developers,

the issue 1041 on the bug tracker presents a full code showing a type
check explosion.

Main.agda  builds a certain table of pairs, which key type is a certain
record  R  defined in a complex way, and including other nested records.

The  value  field in each table item is of   Dec (RightQuotient ...)
-- a result of a certain partial division.

Now, 
(1) let the final test function only  map  isYes  to the value parts 
    in this table.
    Then  Main is type checked in
                                   1 sec.   

(2) Let the test only convert each value part from  (Dec ...)  into  
    Maybe R  in a simplest way.
    Then  Main is type checked in
                                   680 sec.   

(3) Let the test build a similar table where a key  has type 
                                                        R \times R 
    and the result pairs are then summed into one pair.   

    After  4500 seconds  the checker reports that  11 Gb space is not 
    enough.

(1) and (2) are presented on the tracker.
And (3) is a real example -- I could provide it, if asked.  


There is no code complexity difference in these programs except this:

  adding one constructor of  \times,
  adding a pattern 
                   f (x , yes (y ,_)) = .. just y.,   for  x y : R

-- small type changes in the main test, in Main.agda only.

It looks like each such additional constructor makes the  type check
cost  increase 5-20 times.  

Main.agda  demonstrates the cases  (1) and (2).

Can you, please, look into the code, and advise me how to essentially
reduce the type check expense in (2) ?

If I know how to optimize (2), then I could hope to also get the example
of (3) into the machine memory.  

For: how can I continue the project if I cannot type-check real
examples?


About module size
-----------------
People could say that I need to make the modules smaller.
But I suspect that they still are all right. 
(?)
Because
a) Euclidean1.agda  uses intensively all the others (except Main), 
   and still it is type-checked in a moment,
b) Main  is small,
c) each module is type-checked in a moment -- except Main.

But the type check cost seems depending in 5-20 times on each additional
constructor  (\times, Maybe ...)  and its related _pattern_  used in the
Main test.

Ulf Norell has demonstrated that a dummy record wrapper over R, reduces
the type-check cost about 100 times -- in my first example.
But 
* I failed to apply this approach to the example of (2),
* I do not think that this can be a regular programming style.

Please, advise,

------
Sergei