KnownNat-indexed vectors

mixphix:

Are there libraries where this kind of vector has been implemented?

There exist several packages that define a family of finite types indexed by type-level naturals, e.g. finite-typelits, data-fin, fin-int or fin. For each natural number n, there is a type Finite n that has exactly n elements. Then you can define

newtype V n x = V (Finite n -> x)

and derive a lot of instances via Reader (Finite n). You certainly want memoization for performance.

By the way, it is fun to define matrices this way. Conal Elliott gave a talk about this at least once.