{-# OPTIONS_GHC -fglasgow-exts #-}

data Zero = Z
data Succ n = S n

class Add n m r | n m -> r where
    add :: n -> m -> r
    add = undefined

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

class ToInteger n where toI :: n -> Integer
instance (ToInteger n) => ToInteger (Succ n) where toI ~(S x) = 1 + toI x
instance ToInteger Zero where toI = const 0

instance Show Zero where show = show . toI
instance (ToInteger n) => Show (Succ n) where show = show . toI

class Fibo n r | n -> r where fibo :: n -> r; fibo = undefined
instance Fibo (Succ Zero) (Succ Zero)
instance Fibo Zero Zero
instance (Fibo n r1, Fibo (Succ n) r2, Add r1 r2 r3) => Fibo (Succ (Succ n)) r3

{-# OPTIONS_GHC -fglasgow-exts #-}

data Zero = Z
data Succ n = S n

class Add n m r | n m -> r where
    add :: n -> m -> r
    add = undefined

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

class ToInteger n where toI :: n -> Integer
instance (ToInteger n) => ToInteger (Succ n) where toI ~(S x) = 1 + toI x
instance ToInteger Zero where toI = const 0

instance Show Zero where show = show . toI
instance (ToInteger n) => Show (Succ n) where show = show . toI

class Fibo n r | n -> r where fibo :: n -> r; fibo = undefined
instance Fibo (Succ Zero) (Succ Zero)
instance Fibo Zero Zero
instance (Fibo n r1, Fibo (Succ n) r2, Add r1 r2 r3) => Fibo (Succ (Succ n)) r3

-- now, let's encode this function in type classes
f x y 0 = x
f x y n = f y (x + y) (n - 1)

class Fibo2 x y n r | x y n -> r where fiboAcc :: x -> y -> n -> r
instance Fibo2 x y Zero x
instance (Add x y z, Fibo2 y z n r) => Fibo2 x y (Succ n) r
fibo2 :: (Fibo2 Zero (Succ Zero) n r) => n -> r
fibo2 = fiboAcc Z (S Z)