KnownNat-indexed vectors

I meant mainly for the use of fromInteger, to avoid explicitly converting to Finite each time one wants to index the vector. Also given a known Nat the compiler should be able to produce a warning/error if a literal falls outside of the Finite bounds, similarly to the checked-literals plugin. Right now using Finite types is too clumsy.