KnownNat-indexed vectors

As long as you don’t expose the constructor(s), all types are like interfaces rather than implementation. Backpack makes this distinction even clearer.