Finite sets and safe list indexing

Index.hs

{-# LANGUAGE DataKinds, KindSignatures, GADTs #-}

data Nat = Zero | Succ Nat

-- Bounded naturals
data Fin :: Nat -> * where
    FZ :: Fin (Succ n)
    FS :: Fin n -> Fin (Succ n)

data Vect (n :: Nat) a where
    Nil :: Vect Zero a
    Cons :: a -> Vect n a -> Vect (Succ n) a

-- Type-safe list index lookup
(!) :: Vect n a -> Fin n -> a
(Cons x _) ! FZ = x
(Cons _ xs) ! (FS n) = xs ! n

*Main> (Cons 'f' . Cons 'o' . Cons 'o' $ Nil) ! FZ
'f'
*Main> (Cons 'f' . Cons 'o' . Cons 'o' $ Nil) ! (FS FZ)
'o'
*Main> (Cons 'f' . Cons 'o' . Cons 'o' $ Nil) ! (FS . FS $ FZ)
'o'
*Main> (Cons 'f' . Cons 'o' . Cons 'o' $ Nil) ! (FS . FS . FS $ FZ)

<interactive>:14:43:
    Couldn't match type 'Succ n0 with 'Zero
    Expected type: Fin ('Succ ('Succ ('Succ 'Zero)))
      Actual type: Fin ('Succ ('Succ ('Succ ('Succ n0))))
    In the second argument of `(!)', namely `(FS . FS . FS $ FZ)'
    In the expression:
      (Cons 'f' . Cons 'o' . Cons 'o' $ Nil) ! (FS . FS . FS $ FZ)
    In an equation for `it':
        it = (Cons 'f' . Cons 'o' . Cons 'o' $ Nil) ! (FS . FS . FS $ FZ)