[Agda] Issue with sized types (max of two sizes less than i)

[Guillaume Brunerie]

Hello,
I am wondering why the program below does not typecheck (the error
being "Cannot solve size constraints" pointing at the [f l1 l2] term).
It seems fine to me, in the last line both l1 and l2 are of size
strictly smaller that i, so f l1 l2 should also be of size strictly
smaller than i, right?

It seems related to the following question: given j and k of type
Size< i, is j ⊔ˢ k also of type Size< i?

Best,
Guillaume


{-# BUILTIN SIZEUNIV SizeUniv #-} -- SizeUniv : SizeUniv
{-# BUILTIN SIZE Size #-} -- Size : SizeUniv
{-# BUILTIN SIZELT Size<_ #-} -- Size<_ : ..Size → SizeUniv
{-# BUILTIN SIZESUC ↑_ #-} -- ↑_ : Size → Size
{-# BUILTIN SIZEINF ∞ #-} -- ∞ : Size
{-# BUILTIN SIZEMAX _⊔ˢ_ #-} -- _⊔ˢ_ : Size → Size → Size

postulate A : Set

data List (i : Size) : Set where
nil : List i
cons : {j : Size< i} → A → List j → List i

f : {i : Size} → List i → List i → List i
f nil _ = nil
f (cons _ _) nil = nil
f (cons x l1) (cons _ l2) = cons x (f l1 l2)

[Nils Anders Danielsson]

Post by Guillaume Brunerie
It seems related to the following question: given j and k of type
Size< i, is j ⊔ˢ k also of type Size< i?

I tried giving the arguments explicitly:

f {i} (cons {j₁} x l1) (cons {j₂} _ l2) =
cons {i} {j₁ ⊔ˢ j₂} x (f {j₁ ⊔ˢ j₂} l1 l2)

Agda still complained. I suggest that you report this as a bug.