[Agda] type check performance

[Sergei Meshveliani]

Dear Agda developers,

it occurs that introducing call by need does not change any essentially
the type check performance -- on the DoCon-A. It is about 10% speed up.
And the minimal memory is 10 Gb.
I recall the approach of using `abstract'. 
In 2.5.3 in did not help. May it help in 2.5.4 ?

Are there ideas of how to optimize the type checker?

Regards,

------
Sergei