[Agda] [2.6.1] erasure and irrelevance unpredictable

[Mathijs Kwik]

Hi All,

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.

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.

Let's first show some code (for latest agda 2.6.1 from git):
```
open import Level using (Level; _⊔_)
open import Data.Fin using (Fin; zero; suc)
open import Data.List using (List; []; _∷_; length; lookup)
open import Data.Nat using (ℕ; zero; suc; _<_; ≤-pred)
open import Data.String using (String; _≟_)
open import Data.Product using (_×_; _,_; proj₁; proj₂)

module twt.IrrelevanceQuestions {ℓ₁ ℓ₂ : Level} {k : Set ℓ₁} where

variable
  f  : k → Set ℓ₂
  t  : k
  ts : List (String × k)

data OpenProduct (f : k → Set ℓ₂) : List (String × k) → Set (ℓ₁ ⊔ ℓ₂) where
  []    : OpenProduct f []
  _∶_∷_ : (key : String)
        → f t
        → OpenProduct f ts → OpenProduct f ((key , t) ∷ ts)

-- from standard-library, but with irrelevance
fromℕ< : ∀ {m n} → .(m < n) → Fin n
fromℕ< {zero}  {suc n} m≤n = zero
fromℕ< {suc m} {suc n} m≤n = suc (fromℕ< (≤-pred m≤n))

idx : (n : ℕ)
    → {@erased ts : List (String × k)}    -- (1)
    → (@erased p : n < length ts)         -- (2)
    → OpenProduct f ts
    → f (proj₂ (lookup ts (fromℕ< p)))
idx zero    _ (_ ∶ x ∷ _)  = x
idx (suc n) p (_ ∶ _ ∷ op) = idx n (≤-pred p) op
```

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)

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.

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.

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?

Then I @erased (1) and kept (2) irrelevant. Interesting error:
```
Failed to solve the following constraints:
  _n_66 = Data.List.foldr (λ _ → suc) 0 ts : ℕ
  Data.List.foldr (λ _ → suc) 0 ts = _n_66 : ℕ
```

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.

So I hope to get some insights into why (A) (B) and (C) happen. Are any of
these described behaviours bugs I should file?

Kind regards,
Mathijs
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200202/72e0d6e9/attachment.html>