[Agda] Performance: opening parameterized modules before the fields of a record

[Guillaume Brunerie]

Hello, (not sure if I should post that here or on the bug tracker)

I’m trying to figure out why some project that I have been working on
requires as much memory as it does, and I have a specific question about
opening parameterized modules inside records.

I know that inserting definitions between/before fields in a record results
to them being translated to let-ins in all the subsequent fields, and I
have learned recently (from issue #4331) that applying parameterized
modules simply generate a bunch of new functions for everything exported by
the module.

Now I noticed the following code in my project, there are many other
similar pieces of code, but this is the simplest instance.

record CCatwithUU (ccat : CCat) : Set₁ where
>   no-eta-equality
>   open CCat+ ccat renaming (Mor to MorC)



  field
>     UUStr  : (i : ℕ) (Γ : Ob n) → Ob (suc n)
>     UUStr= : {i : ℕ} {Γ : Ob n} → ft (UUStr i Γ) ≡ Γ
>     UUStrNat' : {i : ℕ} (g : MorC n m) (Δ : Ob n) (g₀ : ∂₀ g ≡ Δ) (Γ : Ob
> m) (g₁ : ∂₁ g ≡ Γ)
>              → star g (UUStr i Γ) UUStr= g₁ ≡ UUStr i Δ
>
>   UUStrNat : {i : ℕ} {g : MorC n m} {Δ : Ob n} (g₀ : ∂₀ g ≡ Δ) {Γ : Ob m}
> {g₁ : ∂₁ g ≡ Γ}
>              → star g (UUStr i Γ) UUStr= g₁ ≡ UUStr i Δ
>   UUStrNat g₀ {g₁ = g₁} = UUStrNat' _ _ g₀ _ g₁
>

It’s not very important what everything means, but the thing that I’m
worried about is that I apply and open the parameterized module CCat+
(which is a rather big module, with ~100 definitions) before the fields of
the record.

Could it be that this adds ~100 let-ins in the type of each of the fields?
I have quite a few (~30) similar records, more complicated than this one,
and which often open each other, so that could quickly explode.

As a test, I duplicated the "open CCat+ ccat …" line 10 times inside the
record, and it took much longer to type check (5 seconds as opposed to less
than half a second), most of it on positivity checking.

Thanks,
Best,
Guillaume
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200519/61406f1f/attachment.html>