KnownNat-indexed vectors

Are there Num instances for any of these Finite types? I have used some before for studying finite topological spaces but it seems indexing would be a pain, having to convert things to Finites in order to do it properly. This approach has the advantage that it doesn’t “segfault” if indexing past the length, it just returns whatever the value at the largest index is.