{-# LANGUAGE TypeFamilies, EmptyDataDecls, GADTs #-}

-- Type-level naturals
data Z
data S n

type family Add m n :: *
type instance Add Z n = n
type instance Add (S m) n = S (Add m n)

-- But we can still do this:

data Foo a where
    Bar :: Foo (Add (S Z) Int)

-- This is bad!

-- We'd much rather do this:

data Nat = Z | S Nat

type family Add (m:{Nat}) (n:{Nat}) :: {Nat}
type instance Add {Z} n = n
type instance Add {S m} n = {S (Add m n)}

-- now the preceding example will be a kind error.

-- Or even better:

add :: Nat -> Nat -> Nat
add Z n = n
add (S m) n = S (add m n)

-- and have this automatically lifted to the type level as well,
-- something like:

data Foo a where
    Bar :: Foo ({add (S Z) (S (S Z))})