[Agda] Agda takes a long time to type check.

[Vilius Naudziunas]

Hi,

I am new to Agda (started using it a two months ago). I am trying to use 
it for developing typing system with algebraic properties. All was 
working well until trying to prove that the lexicographic product of 
commutative and idempotent semigroup on the left and monoid on the right 
forms a semigroup. It is a long proof consisting of 256 case splits 
(using 'with ...' syntax). I have generated it using some ocaml code, 
and I think it is correct.
The problem is that it takes a really long time for Agda to type check 
it. First I got stack overflow error. Fixed it by calling Adga with 
'+RTS -K100000000'. Afterwards I left it to type check over weekend, but 
it didn't finish by Monday.

Could you tell me what kind of constructions in Agda could be causing 
such behaviour? Maybe I could avoid them by generating code differently.

Best regards,
Vilius Naudziunas