Vector (a :: *) (n :: Nat)

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

data Nat = Z | S Nat deriving (Show, Eq)

toInt Z = 0
toInt (S a) = 1 + toInt a

data Vector (a :: *) (n :: Nat)  where -- Vector a (n :: Nat)
  Nil  :: Vector a Z
  (:-) :: a -> Vector a n -> Vector a (S n)
  
infixr 5 :-

deriving instance Show a => Show (Vector a n)

vlength :: Vector a n -> Int
vlength = toInt . slength

slength :: Vector a n -> Nat
slength Nil = Z
slength (a :- b) = S (slength b)

type Two = S (S Z)

main = do 
    let vec = "Hello" :- "World" :- Nil :: Vector String Two
    print vec
    print $ slength vec
    print $ vlength vec