Sized data type analysis brittle, does not reduce size

[andreasabel]

This should work, but Agda does not reduce i + 1 to ↑ i when analysing Nat. Subtyping fails silently.

open import Agda.Builtin.Size
open import Agda.Builtin.Nat using (suc) renaming (Nat to ℕ)

_+_ : Size → ℕ → Size
s + 0 = s
s + suc n = ↑ (s + n)

data Nat : Size → Set where
  zero  :  ∀ i → Nat (i + 1)
  suc   :  ∀ i → Nat i → Nat (i + 1)

pred : ∀ i → Nat i → Nat i
pred .(i + 1) (zero i)   =  zero i
pred .(i + 1) (suc i x)  =  x

[asr]

From closing issues via commit messages:

To close an issue in the same repository, use one of the keywords in the list below followed by a reference to the issue number in the commit message.

@andreasabel, the commit message "Fixed issue #2477" didn't follow the above instructions, so I'm manually closing the issue.

[andreasabel]

Ah, yes that was stupid of me. It was late in the evening...