[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)