KnownNat-indexed vectors

I’d imagine a typelit approach would be better if syntax is what you’re after. Especially with required type arguments, you’ll barely notice as a user.