Type Families Vector (a :: *) (n :: Nat) Plus

{-# Language TypeFamilies, DataKinds, KindSignatures, GADTs, UndecidableInstances #-}

data Nat = Z | S Nat

type family Plus (x :: Nat) (y :: Nat) :: Nat where
  Plus 'Z y = y
  Plus ('S x) y = 'S (Plus x y)
  
type family Pred (x :: Nat) :: Nat where
  Pred 'Z = 'Z
  Pred ('S x) = x

data Vec (n :: Nat) (a :: *) where -- Nat -> * -> * where
  Nil :: Vec Z a
  (:-) :: a -> Vec n a -> Vec ('S n) a

infixr 5 :-

instance Show a => Show (Vec n a) where
  show Nil = "Nil"
  show (a :- v) = show a ++ " :- " ++ show v

append :: Vec m a -> Vec n a -> Vec (Plus m n) a
append Nil ys = ys
append (x :- xs) ys = x :- (append xs ys)

vtail :: Vec m a -> Vec (Pred m) a
vtail Nil = Nil
vtail (x :- xs) = xs

main = do
  let v1 = 2 :- Nil
  let v2 = 5 :- 4 :- 3 :- Nil
  putStrLn $ show (v2 `append` v1)
  putStrLn $ show (vtail v2)