{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# OPTIONS -fglasgow-exts #-}


data Zero = Zero
	deriving Show
 
data Succ a = Succ a
	deriving Show

type One = Succ Zero
type Two = Succ One


class Sum a b ab | a b -> ab, a ab -> b
instance Sum Zero b b
instance (Sum a b ab) => Sum (Succ a) b (Succ ab)

add :: Sum a b ab => a -> b -> ab
add = undefined
-- ghci:	:t add (undefined::One) (undefined::Two)


class ShowType a where
	showty :: a

instance ShowType Zero where
	showty = Zero

instance ShowType a => ShowType (Succ a) where
   showty = Succ showty

type family Sum' a b :: *
type instance Sum' Zero b = b
type instance Sum' (Succ a) b = Succ (Sum' a b)

add' ::  (ShowType a, ShowType b) => a -> b -> Sum' a b
add' = undefined

-- ghci:	:t showty (add' (undefined::One) (undefined::Two))