<div dir="ltr"><div>Hi All,</div><div><br></div><div>I've created an open sum type with no runtime overhead (basically an int as a tag and an Any) and am now moving on to my next quest: open products (key/value pairs with differently-typed values). The general idea is to index a list-like structure with a (String, k) list (for remembering the types of the values per key). By mandating the list of keys(+types) to be statically known, code should be able to compile to int-indexed lookups/updates into an array (I know Agda doesn't have those, but I can postulate them to the compiler backends), which I simplify in the code below to just use lists.<br></div><div><br></div><div>To do this, I need some clever erasure and/or irrelevance annotations, so I've been trying to develop some intuition surrounding these and on how agda erases things for runtime use by itself.</div><div><br></div><div>Let's first show some code (for latest agda 2.6.1 from git):</div><div>```</div><div>open import Level using (Level; _⊔_)<br>open import Data.Fin using (Fin; zero; suc)<br>open import Data.List using (List; []; _∷_; length; lookup)<br>open import Data.Nat using (ℕ; zero; suc; _<_; ≤-pred)<br>open import Data.String using (String; _≟_)<br>open import Data.Product using (_×_; _,_; proj₁; proj₂)<br><br>module twt.IrrelevanceQuestions {ℓ₁ ℓ₂ : Level} {k : Set ℓ₁} where<br><br>variable<br>  f  : k → Set ℓ₂<br>  t  : k<br>  ts : List (String × k)<br><br>data OpenProduct (f : k → Set ℓ₂) : List (String × k) → Set (ℓ₁ ⊔ ℓ₂) where<br>  []    : OpenProduct f []<br>  _∶_∷_ : (key : String)<br>        → f t<br>        → OpenProduct f ts → OpenProduct f ((key , t) ∷ ts)<br><br>-- from standard-library, but with irrelevance<br>fromℕ< : ∀ {m n} → .(m < n) → Fin n<br>fromℕ< {zero}  {suc n} m≤n = zero<br>fromℕ< {suc m} {suc n} m≤n = suc (fromℕ< (≤-pred m≤n))<br><br>idx : (n : ℕ)<br>    → {@erased ts : List (String × k)}    -- (1)<br>    → (@erased p : n < length ts)         -- (2)<br>    → OpenProduct f ts<br>    → f (proj₂ (lookup ts (fromℕ< p)))<br>idx zero    _ (_ ∶ x ∷ _)  = x<br>idx (suc n) p (_ ∶ _ ∷ op) = idx n (≤-pred p) op<br></div><div>```</div><div><br></div><div>The OpenProduct nicely becomes: `data T18 = C22 | C26 AgdaAny T18` - in other words a list of unknown (at runtime) types. It's nice to see even the key (String) is automatically understood to be erasable (as it remains tracked in the type index)</div><div><br></div><div>Now, this version of `idx` works, but the road to get there was bumpy so I want to verify the behaviour I'm seeing before submitting potential bugs.</div><div><br></div><div>I started out with (1) and (2) just as normal (no @erased or implicit dot), in fact, I started out without (1) at all, as it is already declared in the variables section. However, I then found it compiled into `[MAlonzo.Code.Agda.Builtin.Sigma.T14] -> Integer -> T18 -> AgdaAny`. So that's question (A): why does agda insist on keeping `ts` around? The generated code doesn't really use it other than to traverse it (while traversing the openproduct itself) and never inspects the contents.</div><div><br></div><div>So I marked (1) irrelevant, but then (2) complains about using ts (which is true) so I mark (2) irrelevant as well, but the complaint remains. So question (B): shouldn't irrelevant arguments be allowed to depend on each other?</div><div><br></div><div>Then I @erased (1) and kept (2) irrelevant. Interesting error:</div><div>```</div><div>Failed to solve the following constraints:<br>  _n_66 = Data.List.foldr (λ _ → suc) 0 ts : ℕ<br>  Data.List.foldr (λ _ → suc) 0 ts = _n_66 : ℕ<br></div><div>```</div><div><br></div><div>question (C): why does this error happen? It seems to me that both `n` and `length ts` are known statically at call-time so the @erased attribute shouldn't mess this up, and besided... the result of the call to ≤-pred is irrelevant itself.</div><div><br></div><div>So I hope to get some insights into why (A) (B) and (C) happen. Are any of these described behaviours bugs I should file?</div><div><br></div><div>Kind regards,<br></div><div>Mathijs<br></div><div><br></div><div><br></div></div>