[Agda] type check performance

[Sergei Meshveliani]

Dear Agda developers.

I have a certain middle-size project, call it "FooLib library".
I am going to publish it soon, but first it would have sense to try to 
reduce its space eagerness.
And I wonder how to reduce.

Its type check in  Agda 2.4.2.2  takes
     
    9G byte memory and  10 minutes  (on a 2 GHz machine),

    the further compilation (by MAlonzo, ghc-7.8.3 etc.) takes  
                                                         37 minutes.

Then, after all the FooLib is compiled,
type check and compilation of a small Main module 
(which imports almost all modules of Foo) takes  
                      10 minutes  and again,  9 Gb memory.

Please, how to reduce this  9 Gb requirement?

I know about the possibilities of 
1) with --> case,
2) using `private' for some proof pieces.
Also the project meaning is so that `private' has sense to apply to 
almost all proofs in FooLib, and this makes it more than 9/10 of the
source.

But 
1) with --> case  is often difficult to arrange,
   (in programming, `with' is friendly, `case' often struggles 
    against), 
2) `private' fails almost everywhere, because it is allowed only at the 
   top level in a module.

Can you please, observe the source and suggest concrete corrections that
reduce the memory eagerness (first, in type check)
?
If yes, then, please, write, to which address to send the project
privately.

Thanks,

------
Sergei