{-# 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

ey0jIExBTkdVQUdFIEdBRFRzLCBLaW5kU2lnbmF0dXJlcywgRGF0YUtpbmRzICMtfQoKaW1wb3J0IFByZWx1ZGUgaGlkaW5nIChCb3VuZGVkLCBzdWNjKQppbXBvcnQgQ29udHJvbC5BcHBsaWNhdGl2ZQppbXBvcnQgRGF0YS5NYXliZQoKZGF0YSBOYXQgPSBaIHwgUyBOYXQKCmRhdGEgQm91bmRlZCAobiA6OiBOYXQpIHdoZXJlCglCWiA6OiBCb3VuZGVkIG4KCUJTIDo6IEJvdW5kZWQgbiAtPiBCb3VuZGVkIChTIG4pCgppbnN0YW5jZSBTaG93IChCb3VuZGVkIG4pIHdoZXJlCglzaG93ICBCWiAgICAgPSAiQloiCglzaG93IChCUyBibikgPSAiQlMgKCIgKysgc2hvdyBibiArKyAiKSIKCmluc3RhbmNlIEVxIChCb3VuZGVkIG4pIHdoZXJlCglCWiAgICA9PSBCWiAgICA9IFRydWUKCUJTIGJuID09IEJTIGJtID0gYm4gPT0gYm0KCV8gICAgID09IF8gICAgID0gRmFsc2UKCnplcm8gOjogQm91bmRlZCAoUyAoUyBaKSkKemVybyA9IEJaCgpvbmUgOjogQm91bmRlZCAoUyAoUyBaKSkKb25lID0gQlMgQloKCnR3byA6OiBCb3VuZGVkIChTIChTIFopKQp0d28gPSBCUyAoQlMgQlopCgpkYXRhIE5hdHR5IChuIDo6IE5hdCkgd2hlcmUKCVp5IDo6IE5hdHR5IFoKCVN5IDo6IE5hdHR5IG4gLT4gTmF0dHkgKFMgbikKCmNsYXNzIE5BVFRZIChuIDo6IE5hdCkgd2hlcmUKCW5hdHR5IDo6IE5hdHR5IG4KCmluc3RhbmNlIE5BVFRZIFogd2hlcmUKCW5hdHR5ID0gWnkKCmluc3RhbmNlIE5BVFRZIG4gPT4gTkFUVFkgKFMgbikgd2hlcmUKCW5hdHR5ID0gU3kgbmF0dHkKCnN1Y2MgOjogTkFUVFkgbiA9PiBCb3VuZGVkIG4gLT4gQm91bmRlZCBuCnN1Y2MgYm4gPSBmcm9tTWF5YmUgQlogJCBnbyBuYXR0eSBibiB3aGVyZQoJZ28gOjogTmF0dHkgbiAtPiBCb3VuZGVkIG4gLT4gTWF5YmUgKEJvdW5kZWQgbikKCWdvICBaeSAgICAgIEJaICAgICA9IE5vdGhpbmcKCWdvIChTeSBueSkgIEJaICAgICA9IEp1c3QgKEJTIEJaKQoJZ28gKFN5IG55KSAoQlMgYm4pID0gQlMgPCQ+IGdvIG55IGJuCgptYWluID0gZG8KCXByaW50ICQgc3VjYyB6ZXJvID09IHplcm8gLS0gRmFsc2UKCXByaW50ICQgc3VjYyB6ZXJvID09IG9uZSAgLS0gVHJ1ZQoJcHJpbnQgJCBzdWNjIG9uZSAgPT0gdHdvICAtLSBUcnVlCglwcmludCAkIHN1Y2MgdHdvICA9PSB6ZXJvIC0tIFRydWU=