<div dir="ltr">Hello, (not sure if I should post that here or on the bug tracker)<div><div><br></div><div>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.<br><br>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.<br><br>Now I noticed the following code in my project, there are many other similar pieces of code, but this is the simplest instance.<br><br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">record CCatwithUU (ccat : CCat) : Set₁ where<br>  no-eta-equality<br>  open CCat+ ccat renaming (Mor to MorC) </blockquote><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">  </blockquote><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">  field<br>    UUStr  : (i : ℕ) (Γ : Ob n) → Ob (suc n)<br>    UUStr= : {i : ℕ} {Γ : Ob n} → ft (UUStr i Γ) ≡ Γ<br>    UUStrNat' : {i : ℕ} (g : MorC n m) (Δ : Ob n) (g₀ : ∂₀ g ≡ Δ) (Γ : Ob m) (g₁ : ∂₁ g ≡ Γ)<br>             → star g (UUStr i Γ) UUStr= g₁ ≡ UUStr i Δ <br>  <br>  UUStrNat : {i : ℕ} {g : MorC n m} {Δ : Ob n} (g₀ : ∂₀ g ≡ Δ) {Γ : Ob m} {g₁ : ∂₁ g ≡ Γ}<br>             → star g (UUStr i Γ) UUStr= g₁ ≡ UUStr i Δ<br>  UUStrNat g₀ {g₁ = g₁} = UUStrNat' _ _ g₀ _ g₁<br></blockquote></div><div><br>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.<br><br>Could it be that this adds ~100 let-ins in the type of each of the fields?</div><div>I have quite a few (~30) similar records, more complicated than this one, and which often open each other, so that could quickly explode.<br></div><div><br></div><div>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.</div><div><br></div><div>Thanks,</div><div>Best,</div><div>Guillaume</div></div></div>