[Agda] Equalities between elements of different sizes

[Guillaume Brunerie]

Hi all,

I am trying to use sized types to do some definitions and proofs and I
have an issue (full code below).

I define lists using sized types, and concatenation of lists (which
has List ∞ for both domains and the codomain, as there is no addition
of sizes). Then I want to prove that l ++ [] is equal to l by
structural induction. But the obvious proof doesn’t typecheck, because
for the induction case, the right-hand side l is in List j whereas the
left-hand-side l ++ [] is in List ∞, but they are supposed to be in
the same type.
If I remove all sized types, then the proof goes through, but in my
actual code I need to use sized types somewhere while also needing to
prove something like l ++ [] = l somewhere else.

Is there a workaround to that?

Best,
Guillaume


open import Agda.Builtin.Size
open import Agda.Builtin.Equality

postulate
  A : Set

data List (i : Size) : Set where
  [] : List i
  _∷_ : {j : Size< i} → A → List j → List i

_++_ : List ∞ → List ∞ → List ∞
[] ++ l = l
(a ∷ l) ++ l' = a ∷ (l ++ l')

cong : {i : Size} {x : A} {l l' : List i} → l ≡ l' → x ∷ l ≡ x ∷ l'
cong refl = refl

test : (l : List ∞) → l ++ [] ≡ l
test [] = refl
test (x ∷ l) = cong (test l)