[Agda] making a pair explodes

[Andrea Vezzosi]

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"?


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