[Agda] type check performance

[Sergei Meshveliani]

On Wed, 2015-08-12 at 23:55 -0400, Wolfram Kahl wrote:
> On Thu, Aug 13, 2015 at 01:09:29AM +0400, Sergei Meshveliani wrote:
> > I am writing in Agda a library for algebra. And the project is (mainly)
> > stuck due to that  Agda 2.4.2.3  takes too much space and time to
> > type-check the current module.
> > 
> > [...]
> >  
> > There are many modules in the project, and the (currently) last module
> > Foo.agda  has only about 130 nonempty lines. 
> > All the previous modules are type-checked in 1-2 hours.
> > After this, to type check  Foo.agda  takes 
> >                     40 minutes  under the options of  -M14G -H14G.
> >  
> > And under  -M9G -H9G,  it does not finish in 4 hours (and I have
> > interrupted it). 


> If less than 129 of the non-empty lines of your module are import statement,
> I would recommend experimenting with splitting the module --- this can lead
> to dramatic improvments. (My developments are full of small modules
> split only for that reason.)


Among its 130 lines about 50 are of `import' or of `open'.

Can you point at the reason of why splitting to small modules often
reduces the type check cost?

Can it happen so that splitting some other .agda file into two reduces 
the type check cost for the last .agda file?

Regards,

------
Sergei