{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}

data Nat = Zero | Succ Nat deriving Show

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

data SNat n where
  SZ :: SNat 'Zero
  SS :: SNat n -> SNat ('Succ n)

repeatV :: SNat n -> a -> Vec a n
repeatV SZ     _ = Nil
repeatV (SS n) a = Cons a (repeatV n a)

instance (Show a) => Show (Vec a n) where
  show Nil = ""
  show (Cons a b) = show a ++ show b