{-# LANGUAGE GADTs, KindSignatures, DataKinds #-}

import Prelude hiding (Bounded, succ)
import Control.Applicative
import Data.Maybe

data Nat = Z | S Nat

data Bounded (n :: Nat) where
	BZ :: Bounded n
	BS :: Bounded n -> Bounded (S n)

instance Show (Bounded n) where
	show  BZ     = "BZ"
	show (BS bn) = "BS (" ++ show bn ++ ")"

instance Eq (Bounded n) where
	BZ    == BZ    = True
	BS bn == BS bm = bn == bm
	_     == _     = False

zero :: Bounded (S (S Z))
zero = BZ

one :: Bounded (S (S Z))
one = BS BZ

two :: Bounded (S (S Z))
two = BS (BS BZ)

data Natty (n :: Nat) where
	Zy :: Natty Z
	Sy :: Natty n -> Natty (S n)

class NATTY (n :: Nat) where
	natty :: Natty n

instance NATTY Z where
	natty = Zy

instance NATTY n => NATTY (S n) where
	natty = Sy natty

succ :: NATTY n => Bounded n -> Bounded n
succ bn = fromMaybe BZ $ go natty bn where
	go :: Natty n -> Bounded n -> Maybe (Bounded n)
	go  Zy      BZ     = Nothing
	go (Sy ny)  BZ     = Just (BS BZ)
	go (Sy ny) (BS bn) = BS <$> go ny bn

main = do
	print $ succ zero == zero -- False
	print $ succ zero == one  -- True
	print $ succ one  == two  -- True
	print $ succ two  == zero -- True