Simplest useful type-level programming

vecconcat.hs

{-# LANGUAGE TypeFamilies, GADTs #-}
{-# LANGUAGE StandaloneDeriving, EmptyDataDecls #-}
data Z
data S n

data Vec n a where
    Nil :: Vec Z a
    Cons :: a -> Vec n a -> Vec (S n) a

deriving instance Show a => Show (Vec n a)
deriving instance Eq a => Eq (Vec n a)
deriving instance Ord a => Ord (Vec n a)

type family Plus m n :: * where
    Plus Z n = n
    Plus (S m) n = S (Plus m n)

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