Could not deduce n~0 from the context n<=0

[int-index]

Since we're dealing with natural numbers, which are by definition non-negative, we must be able to conclude n~0 from n<=0. However, the following code does not compile:

natLeqZero :: (n <= 0) => n :~: 0
natLeqZero = Refl