{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, FlexibleContexts, UndecidableInstances, EmptyDataDecls #-}

-- Type-level naturals
data Z
data S n

class Add a b c | a b -> c

instance Add Z n n
instance Add n m r => Add (S n) m (S r)