    {-# OPTIONS_GHC  -fno-warn-orphans #-}

    {-# LANGUAGE GADTs                 #-}
    {-# LANGUAGE EmptyDataDecls        #-}
    {-# LANGUAGE FlexibleInstances     #-}
    {-# LANGUAGE FlexibleContexts      #-}
    {-# LANGUAGE UndecidableInstances  #-}
    {-# LANGUAGE MultiParamTypeClasses #-}
    {-# LANGUAGE TypeFamilies          #-}
    {-# LANGUAGE TemplateHaskell       #-}
    {-# LANGUAGE ScopedTypeVariables   #-}
    {-# LANGUAGE TypeOperators         #-}
    {-# LANGUAGE RankNTypes            #-}
    {-# LANGUAGE DeriveDataTypeable    #-}
    -- |
    -- Module      : TypeLevel.Number.Nat
    -- Copyright   : Alexey Khudyakov
    -- License     : BSD3-style (see LICENSE)
    --
    -- Maintainer  : Alexey Khudyakov <alexey.skladnoy@gmail.com>
    -- Stability   : unstable
    -- Portability : unportable (GHC only)
    --
    --
    -- This is type level natural numbers. They are represented using
    -- binary encoding which means that reasonable large numbers could be
    -- represented. With default context stack depth (20) maximal number
    -- is 2^18-1 (262143).
    --
    -- > Z           = 0
    -- > I Z         = 1
    -- > O (I Z)     = 2
    -- > I (I Z)     = 3
    -- > O (O (I Z)) = 4
    -- > ...
    --
    -- It's easy to see that representation for each number is not
    -- unique. One could add any numbers of leading zeroes:
    --
    -- > I Z = I (O Z) = I (O (O Z)) = 1
    --
    -- In order to enforce uniqueness of representation only numbers
    -- without leading zeroes are members of Nat type class. This means
    -- than types are equal if and only if numbers are equal.
    --
    -- Natural numbers support comparison and following operations: Next,
    -- Prev, Add, Sub, Mul. All operations on numbers return normalized
    -- numbers.
    --
    -- Interface type classes are reexported from TypeLevel.Number.Classes
    module TypeLevel.Number.Nat ( -- * Natural numbers
                              I
                            , O
                            , Z
                            , Nat(..)
                              -- ** Lifting
                            , SomeNat(..)
                            , withNat
                              -- * Template haskell utilities
                              -- $TH
                            , natT
                            , nat
                            , module TypeLevel.Number.Classes
                            ) where

    import Data.Word     (Word8,Word16,Word32,Word64)
    import Data.Int      (Int8, Int16, Int32, Int64 )
    import Data.Typeable (Typeable)

    import TypeLevel.Number.Classes
    import TypeLevel.Number.Nat.Types
    import TypeLevel.Number.Nat.TH
    import TypeLevel.Reify

    -- $TH
    -- Here is usage example for natT:
    --
    -- > n123 :: $(natT 123)
    -- > n123 = undefined

    ----------------------------------------------------------------

    -- | Type class for natural numbers. Only numbers without leading
    -- zeroes are members of this type class.
    class Nat n where
      -- | Convert natural number to integral value. It's not checked
      -- whether value could be represented.
      toInt :: Integral i => n -> i

    -- | Type class for positive natural numbers. It's synonym for
    -- Positive and Nat.
    class Pos n

    instance              Nat       Z   where toInt :: forall i. Integral i => Z -> i
    toInt Z
    _ = i
    0
    instance              Nat    (I Z)  where toInt :: forall i. Integral i => I Z -> i
    toInt I Z
    _ = i
    1
    instance Nat (O n) => Nat (O (O n)) where toInt :: forall i. Integral i => O (O n) -> i
    toInt O (O n)
    _ = i
    0 i -> i -> i
    forall a. Num a => a -> a -> a
    + i
    2 i -> i -> i
    forall a. Num a => a -> a -> a
    * O n -> i
    forall i. Integral i => O n -> i
    forall n i. (Nat n, Integral i) => n -> i
    toInt (O n
    forall a. HasCallStack => a
    undefined :: (O n))
    instance Nat (O n) => Nat (I (O n)) where toInt :: forall i. Integral i => I (O n) -> i
    toInt I (O n)
    _ = i
    1 i -> i -> i
    forall a. Num a => a -> a -> a
    + i
    2 i -> i -> i
    forall a. Num a => a -> a -> a
    * O n -> i
    forall i. Integral i => O n -> i
    forall n i. (Nat n, Integral i) => n -> i
    toInt (O n
    forall a. HasCallStack => a
    undefined :: (O n))
    instance Nat (I n) => Nat (O (I n)) where toInt :: forall i. Integral i => O (I n) -> i
    toInt O (I n)
    _ = i
    0 i -> i -> i
    forall a. Num a => a -> a -> a
    + i
    2 i -> i -> i
    forall a. Num a => a -> a -> a
    * I n -> i
    forall i. Integral i => I n -> i
    forall n i. (Nat n, Integral i) => n -> i
    toInt (I n
    forall a. HasCallStack => a
    undefined :: (I n))
    instance Nat (I n) => Nat (I (I n)) where toInt :: forall i. Integral i => I (I n) -> i
    toInt I (I n)
    _ = i
    1 i -> i -> i
    forall a. Num a => a -> a -> a
    + i
    2 i -> i -> i
    forall a. Num a => a -> a -> a
    * I n -> i
    forall i. Integral i => I n -> i
    forall n i. (Nat n, Integral i) => n -> i
    toInt (I n
    forall a. HasCallStack => a
    undefined :: (I n))
    -- Error reporting. Stop for denormalized numbers
    class    Number_Is_Denormalized a
    instance (Number_Is_Denormalized Z) => Nat (O Z) where
      toInt :: forall i. Integral i => O Z -> i
    toInt = [Char] -> O Z -> i
    forall a. HasCallStack => [Char] -> a
    error [Char]
    "quench warning"

    -- Synonym for positive
    instance (Nat n, Positive n) => Pos n

    -- | Some natural number
    data SomeNat where
      SomeNat :: Nat n => n -> SomeNat
      deriving Typeable

    instance Show SomeNat where
      showsPrec :: Int -> SomeNat -> ShowS
    showsPrec Int
    d (SomeNat n
    n) = Bool -> ShowS -> ShowS
    showParen (Int
    d Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    10) (ShowS -> ShowS) -> ShowS -> ShowS
    forall a b. (a -> b) -> a -> b
    $
        [Char] -> ShowS
    showString [Char]
    "withNat SomeNat " ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> ShowS
    forall a. Show a => a -> ShowS
    shows (n -> Integer
    forall i. Integral i => n -> i
    forall n i. (Nat n, Integral i) => n -> i
    toInt n
    n :: Integer)

    -- | Apply function which could work with any 'Nat' value only know at runtime.
    withNat :: forall i a. (Integral i) => (forall n. Nat n => n -> a) -> i -> a
    withNat :: forall i a. Integral i => (forall n. Nat n => n -> a) -> i -> a
    withNat forall n. Nat n => n -> a
    f i
    i0
      | i
    i0 i -> i -> Bool
    forall a. Ord a => a -> a -> Bool
    <  i
    0   = [Char] -> a
    forall a. HasCallStack => [Char] -> a
    error [Char]
    "TypeLevel.Number.Nat.withNat: negative number"
      | i
    i0 i -> i -> Bool
    forall a. Eq a => a -> a -> Bool
    == i
    0   = Z -> a
    forall n. Nat n => n -> a
    f (Z
    forall a. HasCallStack => a
    undefined :: Z)
      | Bool
    otherwise = Integer
    -> (forall n m. (Nat n, n ~ O m) => n -> a)
    -> (forall n m. (Nat n, n ~ I m) => n -> a)
    -> a
    cont (i -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral i
    i0) n -> a
    forall n. Nat n => n -> a
    forall n m. (Nat n, n ~ O m) => n -> a
    f n -> a
    forall n. Nat n => n -> a
    forall n m. (Nat n, n ~ I m) => n -> a
    f
      where
        cont :: Integer -> (forall n m. (Nat n, n ~ O m) => n -> a)
                        -> (forall n m. (Nat n, n ~ I m) => n -> a) -> a
        cont :: Integer
    -> (forall n m. (Nat n, n ~ O m) => n -> a)
    -> (forall n m. (Nat n, n ~ I m) => n -> a)
    -> a
    cont Integer
    1 forall n m. (Nat n, n ~ O m) => n -> a
    _  forall n m. (Nat n, n ~ I m) => n -> a
    k1 = I Z -> a
    forall n m. (Nat n, n ~ I m) => n -> a
    k1 (I Z
    forall a. HasCallStack => a
    undefined :: I Z)
        cont Integer
    i forall n m. (Nat n, n ~ O m) => n -> a
    k0 forall n m. (Nat n, n ~ I m) => n -> a
    k1 = Integer
    -> (forall n m. (Nat n, n ~ O m) => n -> a)
    -> (forall n m. (Nat n, n ~ I m) => n -> a)
    -> a
    cont (Integer
    i Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `quot` Integer
    2) n -> a
    forall n m. (Nat n, n ~ O m) => n -> a
    k0' n -> a
    forall n m. (Nat n, n ~ I m) => n -> a
    k1'
          where
            k0' :: forall n m. (Nat n, n ~ O m) => n -> a
            k0' :: forall n m. (Nat n, n ~ O m) => n -> a
    k0' n
    _ | Integer -> Bool
    forall a. Integral a => a -> Bool
    odd Integer
    i     = I n -> a
    forall n m. (Nat n, n ~ I m) => n -> a
    k1 (I n
    forall a. HasCallStack => a
    undefined :: I n)
                  | Bool
    otherwise = O n -> a
    forall n m. (Nat n, n ~ O m) => n -> a
    k0 (O n
    forall a. HasCallStack => a
    undefined :: O n)
            k1' :: forall n m. (Nat n, n ~ I m) => n -> a
            k1' :: forall n m. (Nat n, n ~ I m) => n -> a
    k1' n
    _ | Integer -> Bool
    forall a. Integral a => a -> Bool
    odd Integer
    i     = I n -> a
    forall n m. (Nat n, n ~ I m) => n -> a
    k1 (I n
    forall a. HasCallStack => a
    undefined :: I n)
                  | Bool
    otherwise = O n -> a
    forall n m. (Nat n, n ~ O m) => n -> a
    k0 (O n
    forall a. HasCallStack => a
    undefined :: O n)

    ----------------------------------------------------------------
    -- Data conversion

    -- To Integer
    instance                Reify    Z  Integer where witness :: Witness Z Integer
    witness = Integer -> Witness Z Integer
    forall t a. a -> Witness t a
    Witness Integer
    0
    instance (Nat (O n)) => Reify (O n) Integer where witness :: Witness (O n) Integer
    witness = Integer -> Witness (O n) Integer
    forall t a. a -> Witness t a
    Witness (Integer -> Witness (O n) Integer)
    -> Integer -> Witness (O n) Integer
    forall a b. (a -> b) -> a -> b
    $ O n -> Integer
    forall i. Integral i => O n -> i
    forall n i. (Nat n, Integral i) => n -> i
    toInt (O n
    forall a. HasCallStack => a
    undefined :: O n)
    instance (Nat (I n)) => Reify (I n) Integer where witness :: Witness (I n) Integer
    witness = Integer -> Witness (I n) Integer
    forall t a. a -> Witness t a
    Witness (Integer -> Witness (I n) Integer)
    -> Integer -> Witness (I n) Integer
    forall a b. (a -> b) -> a -> b
    $ I n -> Integer
    forall i. Integral i => I n -> i
    forall n i. (Nat n, Integral i) => n -> i
    toInt (I n
    forall a. HasCallStack => a
    undefined :: I n)

    -- To Int
    instance                Reify    Z  Int where witness :: Witness Z Int
    witness = Int -> Witness Z Int
    forall t a. a -> Witness t a
    Witness Int
    0
    instance (Nat (O n)) => Reify (O n) Int where witness :: Witness (O n) Int
    witness = Int -> Witness (O n) Int
    forall t a. a -> Witness t a
    Witness (Int -> Witness (O n) Int) -> Int -> Witness (O n) Int
    forall a b. (a -> b) -> a -> b
    $ O n -> Int
    forall i. Integral i => O n -> i
    forall n i. (Nat n, Integral i) => n -> i
    toInt (O n
    forall a. HasCallStack => a
    undefined :: O n)
    instance (Nat (I n)) => Reify (I n) Int where witness :: Witness (I n) Int
    witness = Int -> Witness (I n) Int
    forall t a. a -> Witness t a
    Witness (Int -> Witness (I n) Int) -> Int -> Witness (I n) Int
    forall a b. (a -> b) -> a -> b
    $ I n -> Int
    forall i. Integral i => I n -> i
    forall n i. (Nat n, Integral i) => n -> i
    toInt (I n
    forall a. HasCallStack => a
    undefined :: I n)

    -- To Word8
    instance                                              Reify    Z  Word8 where witness :: Witness Z Word8
    witness = Word8 -> Witness Z Word8
    forall t a. a -> Witness t a
    Witness Word8
    0
    instance (Nat (O n), (O n) `Lesser` $(natT 0x100)) => Reify (O n) Word8 where witness :: Witness (O n) Word8
    witness = Word8 -> Witness (O n) Word8
    forall t a. a -> Witness t a
    Witness (Word8 -> Witness (O n) Word8) -> Word8 -> Witness (O n) Word8
    forall a b. (a -> b) -> a -> b
    $ O n -> Word8
    forall i. Integral i => O n -> i
    forall n i. (Nat n, Integral i) => n -> i
    toInt (O n
    forall a. HasCallStack => a
    undefined :: O n)
    instance (Nat (I n), (I n) `Lesser` $(natT 0x100)) => Reify (I n) Word8 where witness :: Witness (I n) Word8
    witness = Word8 -> Witness (I n) Word8
    forall t a. a -> Witness t a
    Witness (Word8 -> Witness (I n) Word8) -> Word8 -> Witness (I n) Word8
    forall a b. (a -> b) -> a -> b
    $ I n -> Word8
    forall i. Integral i => I n -> i
    forall n i. (Nat n, Integral i) => n -> i
    toInt (I n
    forall a. HasCallStack => a
    undefined :: I n)

    -- To Word16
    instance                                                Reify    Z  Word16 where witness :: Witness Z Word16
    witness = Word16 -> Witness Z Word16
    forall t a. a -> Witness t a
    Witness Word16
    0
    instance (Nat (O n), (O n) `Lesser` $(natT 0x10000)) => Reify (O n) Word16 where witness :: Witness (O n) Word16
    witness = Word16 -> Witness (O n) Word16
    forall t a. a -> Witness t a
    Witness (Word16 -> Witness (O n) Word16) -> Word16 -> Witness (O n) Word16
    forall a b. (a -> b) -> a -> b
    $ O n -> Word16
    forall i. Integral i => O n -> i
    forall n i. (Nat n, Integral i) => n -> i
    toInt (O n
    forall a. HasCallStack => a
    undefined :: O n)
    instance (Nat (I n), (I n) `Lesser` $(natT 0x10000)) => Reify (I n) Word16 where witness :: Witness (I n) Word16
    witness = Word16 -> Witness (I n) Word16
    forall t a. a -> Witness t a
    Witness (Word16 -> Witness (I n) Word16) -> Word16 -> Witness (I n) Word16
    forall a b. (a -> b) -> a -> b
    $ I n -> Word16
    forall i. Integral i => I n -> i
    forall n i. (Nat n, Integral i) => n -> i
    toInt (I n
    forall a. HasCallStack => a
    undefined :: I n)

    -- To Word32 (No checks. Won't to default centext stack length)
    instance                Reify    Z  Word32 where witness :: Witness Z Word32
    witness = Word32 -> Witness Z Word32
    forall t a. a -> Witness t a
    Witness Word32
    0
    instance (Nat (O n)) => Reify (O n) Word32 where witness :: Witness (O n) Word32
    witness = Word32 -> Witness (O n) Word32
    forall t a. a -> Witness t a
    Witness (Word32 -> Witness (O n) Word32) -> Word32 -> Witness (O n) Word32
    forall a b. (a -> b) -> a -> b
    $ O n -> Word32
    forall i. Integral i => O n -> i
    forall n i. (Nat n, Integral i) => n -> i
    toInt (O n
    forall a. HasCallStack => a
    undefined :: O n)
    instance (Nat (I n)) => Reify (I n) Word32 where witness :: Witness (I n) Word32
    witness = Word32 -> Witness (I n) Word32
    forall t a. a -> Witness t a
    Witness (Word32 -> Witness (I n) Word32) -> Word32 -> Witness (I n) Word32
    forall a b. (a -> b) -> a -> b
    $ I n -> Word32
    forall i. Integral i => I n -> i
    forall n i. (Nat n, Integral i) => n -> i
    toInt (I n
    forall a. HasCallStack => a
    undefined :: I n)

    -- To Word64 (No checks. Won't to default centext stack length)
    instance                Reify    Z  Word64 where witness :: Witness Z Word64
    witness = Word64 -> Witness Z Word64
    forall t a. a -> Witness t a
    Witness Word64
    0
    instance (Nat (O n)) => Reify (O n) Word64 where witness :: Witness (O n) Word64
    witness = Word64 -> Witness (O n) Word64
    forall t a. a -> Witness t a
    Witness (Word64 -> Witness (O n) Word64) -> Word64 -> Witness (O n) Word64
    forall a b. (a -> b) -> a -> b
    $ O n -> Word64
    forall i. Integral i => O n -> i
    forall n i. (Nat n, Integral i) => n -> i
    toInt (O n
    forall a. HasCallStack => a
    undefined :: O n)
    instance (Nat (I n)) => Reify (I n) Word64 where witness :: Witness (I n) Word64
    witness = Word64 -> Witness (I n) Word64
    forall t a. a -> Witness t a
    Witness (Word64 -> Witness (I n) Word64) -> Word64 -> Witness (I n) Word64
    forall a b. (a -> b) -> a -> b
    $ I n -> Word64
    forall i. Integral i => I n -> i
    forall n i. (Nat n, Integral i) => n -> i
    toInt (I n
    forall a. HasCallStack => a
    undefined :: I n)

    -- To Int8
    instance                                             Reify    Z  Int8 where witness :: Witness Z Int8
    witness = Int8 -> Witness Z Int8
    forall t a. a -> Witness t a
    Witness Int8
    0
    instance (Nat (O n), (O n) `Lesser` $(natT 0x80)) => Reify (O n) Int8 where witness :: Witness (O n) Int8
    witness = Int8 -> Witness (O n) Int8
    forall t a. a -> Witness t a
    Witness (Int8 -> Witness (O n) Int8) -> Int8 -> Witness (O n) Int8
    forall a b. (a -> b) -> a -> b
    $ O n -> Int8
    forall i. Integral i => O n -> i
    forall n i. (Nat n, Integral i) => n -> i
    toInt (O n
    forall a. HasCallStack => a
    undefined :: O n)
    instance (Nat (I n), (I n) `Lesser` $(natT 0x80)) => Reify (I n) Int8 where witness :: Witness (I n) Int8
    witness = Int8 -> Witness (I n) Int8
    forall t a. a -> Witness t a
    Witness (Int8 -> Witness (I n) Int8) -> Int8 -> Witness (I n) Int8
    forall a b. (a -> b) -> a -> b
    $ I n -> Int8
    forall i. Integral i => I n -> i
    forall n i. (Nat n, Integral i) => n -> i
    toInt (I n
    forall a. HasCallStack => a
    undefined :: I n)

    -- To Int16
    instance                                               Reify    Z  Int16 where witness :: Witness Z Int16
    witness = Int16 -> Witness Z Int16
    forall t a. a -> Witness t a
    Witness Int16
    0
    instance (Nat (O n), (O n) `Lesser` $(natT 0x8000)) => Reify (O n) Int16 where witness :: Witness (O n) Int16
    witness = Int16 -> Witness (O n) Int16
    forall t a. a -> Witness t a
    Witness (Int16 -> Witness (O n) Int16) -> Int16 -> Witness (O n) Int16
    forall a b. (a -> b) -> a -> b
    $ O n -> Int16
    forall i. Integral i => O n -> i
    forall n i. (Nat n, Integral i) => n -> i
    toInt (O n
    forall a. HasCallStack => a
    undefined :: O n)
    instance (Nat (I n), (I n) `Lesser` $(natT 0x8000)) => Reify (I n) Int16 where witness :: Witness (I n) Int16
    witness = Int16 -> Witness (I n) Int16
    forall t a. a -> Witness t a
    Witness (Int16 -> Witness (I n) Int16) -> Int16 -> Witness (I n) Int16
    forall a b. (a -> b) -> a -> b
    $ I n -> Int16
    forall i. Integral i => I n -> i
    forall n i. (Nat n, Integral i) => n -> i
    toInt (I n
    forall a. HasCallStack => a
    undefined :: I n)

    -- To Int32 (No checks. Won't to default centext stack length)
    instance                Reify    Z  Int32 where witness :: Witness Z Int32
    witness = Int32 -> Witness Z Int32
    forall t a. a -> Witness t a
    Witness Int32
    0
    instance (Nat (O n)) => Reify (O n) Int32 where witness :: Witness (O n) Int32
    witness = Int32 -> Witness (O n) Int32
    forall t a. a -> Witness t a
    Witness (Int32 -> Witness (O n) Int32) -> Int32 -> Witness (O n) Int32
    forall a b. (a -> b) -> a -> b
    $ O n -> Int32
    forall i. Integral i => O n -> i
    forall n i. (Nat n, Integral i) => n -> i
    toInt (O n
    forall a. HasCallStack => a
    undefined :: O n)
    instance (Nat (I n)) => Reify (I n) Int32 where witness :: Witness (I n) Int32
    witness = Int32 -> Witness (I n) Int32
    forall t a. a -> Witness t a
    Witness (Int32 -> Witness (I n) Int32) -> Int32 -> Witness (I n) Int32
    forall a b. (a -> b) -> a -> b
    $ I n -> Int32
    forall i. Integral i => I n -> i
    forall n i. (Nat n, Integral i) => n -> i
    toInt (I n
    forall a. HasCallStack => a
    undefined :: I n)

    -- To Int64 (No checks. Won't to default centext stack length)
    instance                Reify    Z  Int64 where witness :: Witness Z Int64
    witness = Int64 -> Witness Z Int64
    forall t a. a -> Witness t a
    Witness Int64
    0
    instance (Nat (O n)) => Reify (O n) Int64 where witness :: Witness (O n) Int64
    witness = Int64 -> Witness (O n) Int64
    forall t a. a -> Witness t a
    Witness (Int64 -> Witness (O n) Int64) -> Int64 -> Witness (O n) Int64
    forall a b. (a -> b) -> a -> b
    $ O n -> Int64
    forall i. Integral i => O n -> i
    forall n i. (Nat n, Integral i) => n -> i
    toInt (O n
    forall a. HasCallStack => a
    undefined :: O n)
    instance (Nat (I n)) => Reify (I n) Int64 where witness :: Witness (I n) Int64
    witness = Int64 -> Witness (I n) Int64
    forall t a. a -> Witness t a
    Witness (Int64 -> Witness (I n) Int64) -> Int64 -> Witness (I n) Int64
    forall a b. (a -> b) -> a -> b
    $ I n -> Int64
    forall i. Integral i => I n -> i
    forall n i. (Nat n, Integral i) => n -> i
    toInt (I n
    forall a. HasCallStack => a
    undefined :: I n)

    ----------------------------------------------------------------
    -- Number normalization

    -- Add trailing zero bit to number. It's added only if number is not
    -- equal to zero. Actual normalization is done here.
    type family   Add0Bit n :: *
    type instance Add0Bit    Z  = Z
    type instance Add0Bit (O n) = (O (O n))
    type instance Add0Bit (I n) = (O (I n))

    type instance Normalized    Z  = Z
    type instance Normalized (I n) = I (Normalized n)
    type instance Normalized (O n) = Add0Bit (Normalized n)

    ----------------------------------------------------------------
    -- Show instances.
    -- Nat contexts are used to ensure correctness of numbers.
    instance              Show    Z  where show :: Z -> [Char]
    show Z
    _ = [Char]
    "[0:N]"
    instance Nat (O n) => Show (O n) where show :: O n -> [Char]
    show O n
    n = [Char]
    "["[Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++Integer -> [Char]
    forall a. Show a => a -> [Char]
    show (O n -> Integer
    forall i. Integral i => O n -> i
    forall n i. (Nat n, Integral i) => n -> i
    toInt O n
    n :: Integer)[Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++[Char]
    ":N]"
    instance Nat (I n) => Show (I n) where show :: I n -> [Char]
    show I n
    n = [Char]
    "["[Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++Integer -> [Char]
    forall a. Show a => a -> [Char]
    show (I n -> Integer
    forall i. Integral i => I n -> i
    forall n i. (Nat n, Integral i) => n -> i
    toInt I n
    n :: Integer)[Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++[Char]
    ":N]"

    ----------------------------------------------------------------
    -- Next number.
    -- Number normalization is not required.
    type instance Next    Z  = I Z
    type instance Next (I n) = O (Next n)
    type instance Next (O n) = I n

    ----------------------------------------------------------------
    -- Previous number.
    -- Normalization isn't requred too. It's done manually in (I Z) case.
    type instance Prev    (I Z)   = Z
    type instance Prev (O (O n))  = I (Prev (O n))
    type instance Prev (I (O n))  = O (O n)
    type instance Prev (O (I n))  = I (Prev (I n))
    type instance Prev (I (I n))  = O (I n)

    ----------------------------------------------------------------
    -- Comparison

    -- Join compare results. a is result of comparison of low digits b is
    -- result of comparion of higher digits.
    type family Join a b :: *

    type instance Join IsLesser  IsEqual   = IsLesser
    type instance Join IsEqual   IsEqual   = IsEqual
    type instance Join IsGreater IsEqual   = IsGreater
    type instance Join a         IsLesser  = IsLesser
    type instance Join a         IsGreater = IsGreater

    -- Instances for comparison
    type instance Compare    Z     Z  = IsEqual
    type instance Compare (O n)    Z  = IsGreater
    type instance Compare (I n)    Z  = IsGreater
    type instance Compare    Z  (O n) = IsLesser
    type instance Compare    Z  (I n) = IsLesser

    type instance Compare (O n) (O m) = Compare n m
    type instance Compare (O n) (I m) = Join IsLesser  (Compare n m)
    type instance Compare (I n) (O m) = Join IsGreater (Compare n m)
    type instance Compare (I n) (I m) = Compare n m

    ----------------------------------------------------------------
    -- Positive and Non-zero numbers

    instance Nat (I n) => Positive (I n)
    instance Nat (O n) => Positive (O n)

    instance Nat (I n) => NonZero (I n)
    instance Nat (O n) => NonZero (O n)

    ----------------------------------------------------------------
    -- Addition
    data Carry      -- Designate carry bit
    data NoCarry    -- No carry bit in addition

    -- Type family which actually implement addtition of natural numbers
    type family Add' n m c :: *

    -- Recursion termination without carry bit. Full enumeration is
    -- required to avoid overlapping instances
    type instance Add'    Z     Z  NoCarry = Z
    type instance Add' (O n)    Z  NoCarry = O n
    type instance Add' (I n)    Z  NoCarry = I n
    type instance Add'    Z  (O n) NoCarry = O n
    type instance Add'    Z  (I n) NoCarry = I n
    -- Recursion termination with carry bit
    type instance Add'    Z   Z      Carry = I Z
    type instance Add' (O n)  Z      Carry = I n
    type instance Add' (I n)  Z      Carry = Add' (I n) (I Z) NoCarry
    type instance Add'    Z  (O n)   Carry = I n
    type instance Add'    Z  (I n)   Carry = Add' (I n) (I Z) NoCarry
    -- Generic recursion (No carry)
    type instance Add' (O n) (O m) NoCarry = O (Add' n m NoCarry)
    type instance Add' (I n) (O m) NoCarry = I (Add' n m NoCarry)
    type instance Add' (O n) (I m) NoCarry = I (Add' n m NoCarry)
    type instance Add' (I n) (I m) NoCarry = O (Add' n m   Carry)
    -- Generic recursion (with carry)
    type instance Add' (O n) (O m)   Carry = I (Add' n m NoCarry)
    type instance Add' (I n) (O m)   Carry = O (Add' n m   Carry)
    type instance Add' (O n) (I m)   Carry = O (Add' n m   Carry)
    type instance Add' (I n) (I m)   Carry = I (Add' n m   Carry)

    -- Enumeration of all possible instances heads is required to avoid
    -- overlapping.
    type instance Add (O n) (O m) = Normalized (Add' (O n) (O m) NoCarry)
    type instance Add (I n) (O m) = Normalized (Add' (I n) (O m) NoCarry)
    type instance Add (O n) (I m) = Normalized (Add' (O n) (I m) NoCarry)
    type instance Add (I n) (I m) = Normalized (Add' (I n) (I m) NoCarry)
    type instance Add (O n)    Z  = Normalized (Add' (O n)    Z  NoCarry)
    type instance Add (I n)    Z  = Normalized (Add' (I n)    Z  NoCarry)
    type instance Add    Z  (O n) = Normalized (Add'    Z  (O n) NoCarry)
    type instance Add    Z  (I n) = Normalized (Add'    Z  (I n) NoCarry)
    type instance Add    Z     Z  = Normalized (Add'    Z     Z  NoCarry)

    ----------------------------------------------------------------
    -- Subtraction
    data Borrow     -- Borrow bit
    data NoBorrow   -- Do not borrow bit

    -- Type class which actually implement addtition of natural numbers
    type family Sub' n m c :: *

    -- Recursion termination without carry bit. Full enumeration is
    -- required to avoid overlapping instances
    type instance Sub'    Z     Z  NoBorrow = Z
    type instance Sub' (O n)    Z  NoBorrow = O n
    type instance Sub' (I n)    Z  NoBorrow = I n
    -- Recursion termination with carry bit
    type instance Sub' (O n)  Z      Borrow = I (Sub' n Z Borrow)
    type instance Sub' (I n)  Z      Borrow = O n
    -- Generic recursion (No carry)
    type instance Sub' (O n) (O m) NoBorrow = O (Sub' n m NoBorrow)
    type instance Sub' (I n) (O m) NoBorrow = I (Sub' n m NoBorrow)
    type instance Sub' (O n) (I m) NoBorrow = I (Sub' n m   Borrow)
    type instance Sub' (I n) (I m) NoBorrow = O (Sub' n m NoBorrow)
    -- -- Generic recursion (with carry)
    type instance Sub' (O n) (O m)   Borrow = I (Sub' n m   Borrow)
    type instance Sub' (I n) (O m)   Borrow = O (Sub' n m NoBorrow)
    type instance Sub' (O n) (I m)   Borrow = O (Sub' n m   Borrow)
    type instance Sub' (I n) (I m)   Borrow = I (Sub' n m   Borrow)

    -- Enumeration of all possible instances heads is required to avoid
    -- overlapping.
    type instance Sub (O n) (O m) = Normalized (Sub' (O n) (O m) NoBorrow)
    type instance Sub (I n) (O m) = Normalized (Sub' (I n) (O m) NoBorrow)
    type instance Sub (O n) (I m) = Normalized (Sub' (O n) (I m) NoBorrow)
    type instance Sub (I n) (I m) = Normalized (Sub' (I n) (I m) NoBorrow)
    type instance Sub (O n)    Z  = Normalized (Sub' (O n)    Z  NoBorrow)
    type instance Sub (I n)    Z  = Normalized (Sub' (I n)    Z  NoBorrow)
    type instance Sub    Z     Z  = Normalized (Sub'    Z     Z  NoBorrow)

    ----------------------------------------------------------------
    -- Multiplication
    ----------------------------------------------------------------

    type instance Mul n    Z  = Z
    type instance Mul n (O m) = Normalized (O (Mul n m))
    type instance Mul n (I m) = Normalized (Add' n (O (Mul n m)) NoCarry)