TODO improve this solution

safe-index.hs

data Vector (n :: Nat) (a :: Type) where
  VNil  :: Vector 'Z a
  VCons :: a -> Vector n a -> Vector ('S n) a

data SmallerThan (limit :: Nat) where
  SmallerThanZ :: SmallerThan ('S 'Z)
  SmallerThanN :: SmallerThan n -> SmallerThan ('S n)

(!!!) :: Vector n a -> SmallerThan n -> a
(!!!) (VCons a _) SmallerThanZ = a
(!!!) (VCons _ v) (SmallerThanN n) = v !!! n
-- let vector = VCons 1 (VCons 2 VNil)
-- >>> vector !!! (SmallerThanN SmallerThanZ)
-- 2
-- >>> vector !!! (SmallerThanN (SmallerThanN SmallerThanZ))
-- • Couldn't match type ‘'S 'Z’ with ‘'Z’