Comment by thesz

Arithmetic inside the types not necessarily introduces undecidability. One example is telescopes for indices:

  data N where
    Z :: N
    O :: N -> N
  data T (n :: N) where
    TZ :: T (O n)
    TO :: T n -> T (O n)

To safely access an element in array you have to provide a proof that a telescope can be constructed for given index range.