{-# OPTIONS -fglasgow-exts #-}

module Add where

data Zero
data Succ n

class Add n m s | n m -> s

instance Add Zero m m
instance Add n m s => Add (Succ n) m (Succ s)

seven :: Add (Succ (Succ (Succ Zero))) (Succ (Succ (Succ (Succ Zero)))) a => a
seven = undefined