Indexing: Empty vector has empty domain

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.