[Agda] unnatural check cost

[Sergei Meshveliani]

Dear Agda developers,

please, see the issue 1041 on the bug tracker. 

I have attached the full code to the tracker.

The question is:
    how does this occur that 
    1) all the complex generic structures in various modules are  
       type-checked in a small time
    2) and a small specialization thing in Main is not type-checked in 
       any reasonable time
    ?

(so that I am stuck).

See there  README.agda.

Thanks,

------
Sergei