This fixes a minor soundness/safety issue in the Indexing module.
The domain of vectors is reflected at the type-level to guarantee, at compile-time, that accesses are safe.
A (n, a) vector has a value of type a for each value in the set n cardinal.
However, the empty vector is given a type polymorphic in its domain: Vector.empty : (_, _) vector.
Thus, the empty vector can be used with any domain, which breaks the guarantee above.