You'd need GHC extensions to pull that off, Greg, but it could be done. Something like
data Vect (size :: Nat) (a :: *) where
Cons :: a -> Vect n a -> Vect (Succ n) a
Nil :: Vect Zero a
data NatUpTo (n :: Nat) where
Here :: NatUpTo n -- "Here" means 0
There :: NatUpTo n -> NatUpTo (S n) -- "There x" means 1 + x
vectIndex :: Vect (S n) a -> NatUpTo n -> a
vectIndex (Cons x _) Here = a
vectIndex (Cons _ xs) (There i) = vectIndex xs i
class (Enum a) => EnumSize (size :: Nat) a where
enumerateAll :: Vect size a
-- law: (enumerateAll `asTypeOf` [x]) `vectIndex` unsafeIntToNatUpTo (fromEnum x)
It gets tedious, though, dealing with all of that safety. LiquidHaskell is perhaps a more viable option for such a thing. It would be nice to have standard libraries written with LiquidHaskell so that we have a more rigorously proven code base.