Nat2.hs

{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}

data Nat :: * where
  Zero :: Nat
  Suc  :: Nat -> Nat

instance Eq Nat where
  Zero  == Zero   = True
  Suc n == Suc n' = n == n'
  _     == _      = False

instance Ord Nat where
  Zero  <= _      = True
  Suc n <= Suc n' = n <= n'
  _     <= _      = False

instance Enum Nat where
  fromEnum Zero        = 0
  fromEnum (Suc n)     = fromEnum n + 1
  toEnum n | n == 0    = Zero
           | n > 0     = Suc (toEnum (n - 1))
           | otherwise = error ("Cannot cast " ++ show n ++ " to Nat")

instance Show Nat where
  show = show . fromEnum