[Agda] making a pair explodes

[Sergei Meshveliani]

On Mon, 2017-04-17 at 13:22 +0200, Andrea Vezzosi wrote:
> A couple of questions:
> 
> - Does it help if you provide the type signature for "rR∣?"  ?
> - What about doing putting the local definitions in a "where" clause
> rather than a "let"?


Great!  
Adding the type signature for rR∣? helps.
Under 3 Gb heap,  it takes 74 seconds to type-check.  

The type check cost reduces probably more than 100 times.

Thank you very much. 

I could suspect this effect with the type signature, but I have
forgotten to try it.
 
This is indeed a relief. 
Because during last four years this is the main example in my project
for dependent types in computer algebra. This example was tried two
years earlier; its type check has failed in the same way. 
Now it is time to revisit it. And it occurs that it is sufficient to add
a single type signature.

Can you, please, give a hint: how does this occur that without this
signature the checker spends this much computation? 

Further: the whole project needs the minimum of 10 Gb to check, and is
checked in 64 minutes. 
And it is highly desirable to reduce this to 7 Gb, or even better, to 
3 Gb.
And there are many places where I skip type signatures (in order to make
the code looking shorter).
Suppose that I add some type signatures to the modules that take most of
the cost to check. Does this worth trying? 

Thanks,

------
Sergei


> On Mon, Apr 17, 2017 at 1:00 PM, Sergei Meshveliani <mechvel at botik.ru> wrote:
> > Dear Agda developers,
> >
> > The following fragment shows a certain remarkable detail:
> >
> >   f :  (b : C) → IsPrime b → Domain _ _
> >   f b prime-b =
> >               let open ForPrime b prime-b using (rFoo; ...)
> >                   rIR   = proj₁ rFoo
> >                   _∣r?_ = proj₂ rFoo
> >                   rR    = Foo.ring rIR
> >                   rR∣?  = (rR , _∣r?_)    -- **
> >               in
> >               anything
> >
> > Here  ForPrime  is a paramtric module,  Foo is a record.
> > All the needed previous .agda files have been checked earlier,
> > within about  10 Gb heap and 50 minutes.
> > And checking this  f  explodes:  for  26 Gb  3 hours is not enough, so I
> > have interrupted it.
> >
> > I set `anything' there in order to see which part of let-in makes the
> > checker explode.
> >
> > And it occurs that commenting out the last line in let-in makes f
> > checked in a small time:
> >
> > Finished Foo
> > Total                      62,991ms
> > Miscellaneous                 360ms
> > Deserialization            53,299ms
> > Serialization               4,772ms (9,012ms)
> > Serialization.BinaryEncode  4,072ms
> > Serialization.Sort             88ms
> > Serialization.Compress         76ms
> > Import                        156ms
> > Typing                         84ms    (88ms)
> > DeadCode                       60ms
> > Scoping                        12ms
> > ModuleName                     12ms
> >
> >
> > So:  rR  and  _∣r?_  are checked in a small time,
> > while composing them into a pair gives explosion.
> >
> > I know about the effect of large terms being substituted into a
> > parametric module - the effect produced by a certain lack of data
> > sharing in the type representation.
> >
> > But: really only composing this pair must lead to this explosion?
> > Can you guess and tell what may be happening there?
> >
> > I can provide the full code.
> > But it is large, and needs about 10 Gb heap to type-check.
> >
> > Thanks,
> >
> > -------
> > Sergei
> >
> >
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
>