[Agda] making a pair explodes

[Sergei Meshveliani]

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