[Agda] type check performance

[Sergei Meshveliani]

Dear Agda developers,
I have the following question about the type check performance.

Last summer I talked to a person who is experienced in programming
proofs in Coq. I asked him about the type check performance.
He said that the only source of an unnatural type check cost with Coq
can be not of the language/compiler/interpreter itself, but due to
unlucky usage of proof _tactics_ in the user program.
Of course, one can apply a proof tactic in a terrible way. 

With Agda, I currently use (sometimes) only one tactic, it is of the
Standard library: bringing to normal form by SemiringSolver. 
And this cannot involve any inefficiency.
So, the question is: 
what is this that makes Agda type check performance cost much more than
Coq's ?  

Regards,

------
Sergei