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

    {-# LANGUAGE DeriveDataTypeable    #-}
    {-# LANGUAGE GADTs                 #-}
    {-# LANGUAGE RankNTypes            #-}
    {-# LANGUAGE EmptyDataDecls        #-}
    {-# LANGUAGE FlexibleInstances     #-}
    {-# LANGUAGE FlexibleContexts      #-}
    {-# LANGUAGE UndecidableInstances  #-}
    {-# LANGUAGE MultiParamTypeClasses #-}
    {-# LANGUAGE TypeFamilies          #-}
    {-# LANGUAGE TemplateHaskell       #-}
    {-# LANGUAGE ScopedTypeVariables   #-}
    -- |
    -- Module      : TypeLevel.Number.Int
    -- Copyright   : Alexey Khudyakov
    -- License     : BSD3-style (see LICENSE)
    --
    -- Maintainer  : Alexey Khudyakov <alexey.skladnoy@gmail.com>
    -- Stability   : unstable
    -- Portability : unportable (GHC only)
    --
    -- Type level signed integer numbers are implemented using balanced
    -- ternary encoding much in the same way as natural numbers.
    --
    -- Currently following operations are supported: Next, Prev, Add, Sub,
    -- Mul.
    module TypeLevel.Number.Int ( -- * Integer numbers
                              ZZ
                            , Dn
                            , D0
                            , D1
                            , IntT(..)
                              -- ** Lifting
                            , SomeInt
                            , withInt
                              -- * Template haskell utilities
                            , intT
                            , module TypeLevel.Number.Classes
                            ) where

    import Data.Typeable (Typeable)
    import Language.Haskell.TH

    import TypeLevel.Number.Classes
    import TypeLevel.Number.Int.Types
    import TypeLevel.Util

    splitToTrits :: Integer -> [Int]
    splitToTrits :: Integer -> [Int]
    splitToTrits Integer
    0 = []
    splitToTrits Integer
    x | Integer
    n Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    0 =  Int
    0 Int -> [Int] -> [Int]
    forall a. a -> [a] -> [a]
    : Integer -> [Int]
    splitToTrits  Integer
    rest
                   | Integer
    n Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    1 =  Int
    1 Int -> [Int] -> [Int]
    forall a. a -> [a] -> [a]
    : Integer -> [Int]
    splitToTrits  Integer
    rest
                   | Integer
    n Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    2 = -Int
    1 Int -> [Int] -> [Int]
    forall a. a -> [a] -> [a]
    : Integer -> [Int]
    splitToTrits (Integer
    rest Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    1)
                   where
                     (Integer
    rest,Integer
    n) = Integer -> Integer -> (Integer, Integer)
    forall a. Integral a => a -> a -> (a, a)
    divMod Integer
    x Integer
    3
    splitToTrits Integer
    _ = [Char] -> [Int]
    forall a. HasCallStack => [Char] -> a
    error [Char]
    "Internal error"

    -- | Generate type for integer number.
    intT :: Integer -> TypeQ
    intT :: Integer -> TypeQ
    intT = (TypeQ -> TypeQ -> TypeQ) -> TypeQ -> [TypeQ] -> TypeQ
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr TypeQ -> TypeQ -> TypeQ
    forall (m :: * -> *). Quote m => m Type -> m Type -> m Type
    appT (Name -> TypeQ
    forall (m :: * -> *). Quote m => Name -> m Type
    conT ''ZZ) ([TypeQ] -> TypeQ) -> (Integer -> [TypeQ]) -> Integer -> TypeQ
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Int -> TypeQ) -> [Int] -> [TypeQ]
    forall a b. (a -> b) -> [a] -> [b]
    map Int -> TypeQ
    forall {a} {m :: * -> *}.
    (Eq a, Num a, Quote m, Show a) =>
    a -> m Type
    con ([Int] -> [TypeQ]) -> (Integer -> [Int]) -> Integer -> [TypeQ]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> [Int]
    splitToTrits
      where
        con :: a -> m Type
    con (-1) = Name -> m Type
    forall (m :: * -> *). Quote m => Name -> m Type
    conT ''Dn
        con   a
    0  = Name -> m Type
    forall (m :: * -> *). Quote m => Name -> m Type
    conT ''D0
        con   a
    1  = Name -> m Type
    forall (m :: * -> *). Quote m => Name -> m Type
    conT ''D1
        con   a
    x  = [Char] -> m Type
    forall a. HasCallStack => [Char] -> a
    error ([Char] -> m Type) -> [Char] -> m Type
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Strange trit: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ a -> [Char]
    forall a. Show a => a -> [Char]
    show a
    x

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

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

    instance IntT     ZZ  where toInt :: forall i. Integral i => ZZ -> i
    toInt ZZ
    _ =  i
    0
    instance IntT (D1 ZZ) where toInt :: forall i. Integral i => D1 ZZ -> i
    toInt D1 ZZ
    _ =  i
    1
    instance IntT (Dn ZZ) where toInt :: forall i. Integral i => Dn ZZ -> i
    toInt Dn ZZ
    _ = -i
    1

    instance IntT (Dn n) => IntT (Dn (Dn n)) where toInt :: forall i. Integral i => Dn (Dn n) -> i
    toInt Dn (Dn n)
    n = -i
    1 i -> i -> i
    forall a. Num a => a -> a -> a
    + i
    3 i -> i -> i
    forall a. Num a => a -> a -> a
    * Dn (Dn n) -> i
    forall n i (t :: * -> *). (IntT n, Integral i) => t n -> i
    toInt' Dn (Dn n)
    n
    instance IntT (Dn n) => IntT (D0 (Dn n)) where toInt :: forall i. Integral i => D0 (Dn n) -> i
    toInt D0 (Dn n)
    n =  i
    0 i -> i -> i
    forall a. Num a => a -> a -> a
    + i
    3 i -> i -> i
    forall a. Num a => a -> a -> a
    * D0 (Dn n) -> i
    forall n i (t :: * -> *). (IntT n, Integral i) => t n -> i
    toInt' D0 (Dn n)
    n
    instance IntT (Dn n) => IntT (D1 (Dn n)) where toInt :: forall i. Integral i => D1 (Dn n) -> i
    toInt D1 (Dn n)
    n =  i
    1 i -> i -> i
    forall a. Num a => a -> a -> a
    + i
    3 i -> i -> i
    forall a. Num a => a -> a -> a
    * D1 (Dn n) -> i
    forall n i (t :: * -> *). (IntT n, Integral i) => t n -> i
    toInt' D1 (Dn n)
    n
    instance IntT (D0 n) => IntT (Dn (D0 n)) where toInt :: forall i. Integral i => Dn (D0 n) -> i
    toInt Dn (D0 n)
    n = -i
    1 i -> i -> i
    forall a. Num a => a -> a -> a
    + i
    3 i -> i -> i
    forall a. Num a => a -> a -> a
    * Dn (D0 n) -> i
    forall n i (t :: * -> *). (IntT n, Integral i) => t n -> i
    toInt' Dn (D0 n)
    n
    instance IntT (D0 n) => IntT (D0 (D0 n)) where toInt :: forall i. Integral i => D0 (D0 n) -> i
    toInt D0 (D0 n)
    n =  i
    0 i -> i -> i
    forall a. Num a => a -> a -> a
    + i
    3 i -> i -> i
    forall a. Num a => a -> a -> a
    * D0 (D0 n) -> i
    forall n i (t :: * -> *). (IntT n, Integral i) => t n -> i
    toInt' D0 (D0 n)
    n
    instance IntT (D0 n) => IntT (D1 (D0 n)) where toInt :: forall i. Integral i => D1 (D0 n) -> i
    toInt D1 (D0 n)
    n =  i
    1 i -> i -> i
    forall a. Num a => a -> a -> a
    + i
    3 i -> i -> i
    forall a. Num a => a -> a -> a
    * D1 (D0 n) -> i
    forall n i (t :: * -> *). (IntT n, Integral i) => t n -> i
    toInt' D1 (D0 n)
    n
    instance IntT (D1 n) => IntT (Dn (D1 n)) where toInt :: forall i. Integral i => Dn (D1 n) -> i
    toInt Dn (D1 n)
    n = -i
    1 i -> i -> i
    forall a. Num a => a -> a -> a
    + i
    3 i -> i -> i
    forall a. Num a => a -> a -> a
    * Dn (D1 n) -> i
    forall n i (t :: * -> *). (IntT n, Integral i) => t n -> i
    toInt' Dn (D1 n)
    n
    instance IntT (D1 n) => IntT (D0 (D1 n)) where toInt :: forall i. Integral i => D0 (D1 n) -> i
    toInt D0 (D1 n)
    n =  i
    0 i -> i -> i
    forall a. Num a => a -> a -> a
    + i
    3 i -> i -> i
    forall a. Num a => a -> a -> a
    * D0 (D1 n) -> i
    forall n i (t :: * -> *). (IntT n, Integral i) => t n -> i
    toInt' D0 (D1 n)
    n
    instance IntT (D1 n) => IntT (D1 (D1 n)) where toInt :: forall i. Integral i => D1 (D1 n) -> i
    toInt D1 (D1 n)
    n =  i
    1 i -> i -> i
    forall a. Num a => a -> a -> a
    + i
    3 i -> i -> i
    forall a. Num a => a -> a -> a
    * D1 (D1 n) -> i
    forall n i (t :: * -> *). (IntT n, Integral i) => t n -> i
    toInt' D1 (D1 n)
    n

    toInt' :: (IntT n, Integral i) => t n -> i
    toInt' :: forall n i (t :: * -> *). (IntT n, Integral i) => t n -> i
    toInt' = n -> i
    forall i. Integral i => n -> i
    forall n i. (IntT n, Integral i) => n -> i
    toInt (n -> i) -> (t n -> n) -> t n -> i
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . t n -> n
    forall (t :: * -> *) a. t a -> a
    cdr

    instance                Show    ZZ  where show :: ZZ -> [Char]
    show ZZ
    _ = [Char]
    "[0:Z]"
    instance IntT (Dn n) => Show (Dn n) where show :: Dn n -> [Char]
    show Dn n
    n = [Char]
    "["[Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++Integer -> [Char]
    forall a. Show a => a -> [Char]
    show (Dn n -> Integer
    forall i. Integral i => Dn n -> i
    forall n i. (IntT n, Integral i) => n -> i
    toInt Dn n
    n :: Integer)[Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++[Char]
    ":Z]"
    instance IntT (D0 n) => Show (D0 n) where show :: D0 n -> [Char]
    show D0 n
    n = [Char]
    "["[Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++Integer -> [Char]
    forall a. Show a => a -> [Char]
    show (D0 n -> Integer
    forall i. Integral i => D0 n -> i
    forall n i. (IntT n, Integral i) => n -> i
    toInt D0 n
    n :: Integer)[Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++[Char]
    ":Z]"
    instance IntT (D1 n) => Show (D1 n) where show :: D1 n -> [Char]
    show D1 n
    n = [Char]
    "["[Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++Integer -> [Char]
    forall a. Show a => a -> [Char]
    show (D1 n -> Integer
    forall i. Integral i => D1 n -> i
    forall n i. (IntT n, Integral i) => n -> i
    toInt D1 n
    n :: Integer)[Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++[Char]
    ":Z]"

    -- | Some natural number
    data SomeInt where
      SomeInt :: IntT n => n -> SomeInt
      deriving Typeable

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

    -- | Apply function which could work with any 'Nat' value only know at runtime.
    withInt :: forall i a. (Integral i) => (forall n. IntT n => n -> a) -> i -> a
    withInt :: forall i a. Integral i => (forall n. IntT n => n -> a) -> i -> a
    withInt forall n. IntT n => n -> a
    f i
    i0
      | i
    i0 i -> i -> Bool
    forall a. Eq a => a -> a -> Bool
    == i
    0   = ZZ -> a
    forall n. IntT n => n -> a
    f (ZZ
    forall a. HasCallStack => a
    undefined :: ZZ)
      | Bool
    otherwise = Integer
    -> (forall n m. (IntT n, n ~ Dn m) => n -> a)
    -> (forall n m. (IntT n, n ~ D0 m) => n -> a)
    -> (forall n m. (IntT n, n ~ D1 m) => n -> a)
    -> a
    cont (i -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral i
    i0) n -> a
    forall n. IntT n => n -> a
    forall n m. (IntT n, n ~ Dn m) => n -> a
    f n -> a
    forall n. IntT n => n -> a
    forall n m. (IntT n, n ~ D0 m) => n -> a
    f n -> a
    forall n. IntT n => n -> a
    forall n m. (IntT n, n ~ D1 m) => n -> a
    f
      where
        cont :: Integer -> (forall n m. (IntT n, n ~ Dn m) => n -> a)
                        -> (forall n m. (IntT n, n ~ D0 m) => n -> a)
                        -> (forall n m. (IntT n, n ~ D1 m) => n -> a) -> a
        cont :: Integer
    -> (forall n m. (IntT n, n ~ Dn m) => n -> a)
    -> (forall n m. (IntT n, n ~ D0 m) => n -> a)
    -> (forall n m. (IntT n, n ~ D1 m) => n -> a)
    -> a
    cont (-1) forall n m. (IntT n, n ~ Dn m) => n -> a
    kN forall n m. (IntT n, n ~ D0 m) => n -> a
    _  forall n m. (IntT n, n ~ D1 m) => n -> a
    _  = Dn ZZ -> a
    forall n m. (IntT n, n ~ Dn m) => n -> a
    kN (Dn ZZ
    forall a. HasCallStack => a
    undefined :: Dn ZZ)
        cont   Integer
    1  forall n m. (IntT n, n ~ Dn m) => n -> a
    _  forall n m. (IntT n, n ~ D0 m) => n -> a
    _  forall n m. (IntT n, n ~ D1 m) => n -> a
    k1 = D1 ZZ -> a
    forall n m. (IntT n, n ~ D1 m) => n -> a
    k1 (D1 ZZ
    forall a. HasCallStack => a
    undefined :: D1 ZZ)
        cont   Integer
    i  forall n m. (IntT n, n ~ Dn m) => n -> a
    kN forall n m. (IntT n, n ~ D0 m) => n -> a
    k0 forall n m. (IntT n, n ~ D1 m) => n -> a
    k1 = Integer
    -> (forall n m. (IntT n, n ~ Dn m) => n -> a)
    -> (forall n m. (IntT n, n ~ D0 m) => n -> a)
    -> (forall n m. (IntT n, n ~ D1 m) => n -> a)
    -> a
    cont Integer
    i' n -> a
    forall n m. (IntT n, n ~ Dn m) => n -> a
    kN' n -> a
    forall n m. (IntT n, n ~ D0 m) => n -> a
    k0' n -> a
    forall n m. (IntT n, n ~ D1 m) => n -> a
    k1'
          where
            (Integer
    i',Integer
    bit) = case Integer -> Integer -> (Integer, Integer)
    forall a. Integral a => a -> a -> (a, a)
    divMod Integer
    i Integer
    3 of
                         (Integer
    x,Integer
    2) -> (Integer
    xInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    +Integer
    1,-Integer
    1)
                         (Integer, Integer)
    x     -> (Integer, Integer)
    x
            kN' :: forall n m. (IntT n, n ~ Dn m) => n -> a
            kN' :: forall n m. (IntT n, n ~ Dn m) => n -> a
    kN' n
    _ | Integer
    bit Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == -Integer
    1 = Dn n -> a
    forall n m. (IntT n, n ~ Dn m) => n -> a
    kN (Dn n
    forall a. HasCallStack => a
    undefined :: Dn n)
                  | Integer
    bit Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    ==  Integer
    0 = D0 n -> a
    forall n m. (IntT n, n ~ D0 m) => n -> a
    k0 (D0 n
    forall a. HasCallStack => a
    undefined :: D0 n)
                  | Bool
    otherwise = D1 n -> a
    forall n m. (IntT n, n ~ D1 m) => n -> a
    k1 (D1 n
    forall a. HasCallStack => a
    undefined :: D1 n)
            k0' :: forall n m. (IntT n, n ~ D0 m) => n -> a
            k0' :: forall n m. (IntT n, n ~ D0 m) => n -> a
    k0' n
    _ | Integer
    bit Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == -Integer
    1 = Dn n -> a
    forall n m. (IntT n, n ~ Dn m) => n -> a
    kN (Dn n
    forall a. HasCallStack => a
    undefined :: Dn n)
                  | Integer
    bit Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    ==  Integer
    0 = D0 n -> a
    forall n m. (IntT n, n ~ D0 m) => n -> a
    k0 (D0 n
    forall a. HasCallStack => a
    undefined :: D0 n)
                  | Bool
    otherwise = D1 n -> a
    forall n m. (IntT n, n ~ D1 m) => n -> a
    k1 (D1 n
    forall a. HasCallStack => a
    undefined :: D1 n)

            k1' :: forall n m. (IntT n, n ~ D1 m) => n -> a
            k1' :: forall n m. (IntT n, n ~ D1 m) => n -> a
    k1' n
    _ | Integer
    bit Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == -Integer
    1 = Dn n -> a
    forall n m. (IntT n, n ~ Dn m) => n -> a
    kN (Dn n
    forall a. HasCallStack => a
    undefined :: Dn n)
                  | Integer
    bit Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    ==  Integer
    0 = D0 n -> a
    forall n m. (IntT n, n ~ D0 m) => n -> a
    k0 (D0 n
    forall a. HasCallStack => a
    undefined :: D0 n)
                  | Bool
    otherwise = D1 n -> a
    forall n m. (IntT n, n ~ D1 m) => n -> a
    k1 (D1 n
    forall a. HasCallStack => a
    undefined :: D1 n)

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

    type family   AddBit n :: *
    type instance AddBit    ZZ = ZZ
    type instance AddBit (Dn a) = D0 (Dn a)
    type instance AddBit (D0 a) = D0 (D0 a)
    type instance AddBit (D1 a) = D0 (D1 a)

    type instance Normalized     ZZ = ZZ
    type instance Normalized (Dn n) = Dn     (Normalized n)
    type instance Normalized (D0 n) = AddBit (Normalized n)
    type instance Normalized (D1 n) = D1     (Normalized n)

    ----------------------------------------------------------------
    -- Next Number
    type instance Next     ZZ = D1 ZZ
    type instance Next (Dn n) = Normalized (D0 n)
    type instance Next (D0 n) = D1 n
    type instance Next (D1 n) = Normalized (Dn (Next n))

    ----------------------------------------------------------------
    -- Previous number
    type instance Prev     ZZ = Dn ZZ
    type instance Prev (Dn n) = Normalized (D1 (Prev n))
    type instance Prev (D0 n) = Dn n
    type instance Prev (D1 n) = Normalized (D0 n)

    ----------------------------------------------------------------
    -- Negate number
    type instance Negate    ZZ  = ZZ
    type instance Negate (Dn n) = D1 (Negate n)
    type instance Negate (D0 n) = D0 (Negate n)
    type instance Negate (D1 n) = Dn (Negate n)

    ----------------------------------------------------------------
    -- Addition

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

    data CarryN
    data Carry0
    data Carry1

    -- Special cases with ZZ
    type instance Add'     ZZ     ZZ Carry0 = ZZ
    type instance Add'     ZZ (Dn n) Carry0 = (Dn n)
    type instance Add'     ZZ (D0 n) Carry0 = (D0 n)
    type instance Add'     ZZ (D1 n) Carry0 = (D1 n)
    type instance Add' (Dn n)     ZZ Carry0 = (Dn n)
    type instance Add' (D0 n)     ZZ Carry0 = (D0 n)
    type instance Add' (D1 n)     ZZ Carry0 = (D1 n)
    --
    type instance Add'     ZZ     ZZ CarryN = Dn ZZ
    type instance Add'     ZZ (Dn n) CarryN = Prev (Dn n)
    type instance Add'     ZZ (D0 n) CarryN = (Dn n)
    type instance Add'     ZZ (D1 n) CarryN = (D0 n)
    type instance Add' (Dn n)     ZZ CarryN = Prev (Dn n)
    type instance Add' (D0 n)     ZZ CarryN = (Dn n)
    type instance Add' (D1 n)     ZZ CarryN = (D0 n)
    --
    type instance Add'     ZZ     ZZ Carry1 = D1 ZZ
    type instance Add'     ZZ (Dn n) Carry1 = (D0 n)
    type instance Add'     ZZ (D0 n) Carry1 = (D1 n)
    type instance Add'     ZZ (D1 n) Carry1 = Next (D1 n)
    type instance Add' (Dn n)     ZZ Carry1 = (D0 n)
    type instance Add' (D0 n)     ZZ Carry1 = (D1 n)
    type instance Add' (D1 n)     ZZ Carry1 = Next (D1 n)

    -- == General recursion ==
    -- No carry
    type instance Add' (Dn n) (Dn m) Carry0 = D1 (Add' n m CarryN)
    type instance Add' (D0 n) (Dn m) Carry0 = Dn (Add' n m Carry0)
    type instance Add' (D1 n) (Dn m) Carry0 = D0 (Add' n m Carry0)
    --
    type instance Add' (Dn n) (D0 m) Carry0 = Dn (Add' n m Carry0)
    type instance Add' (D0 n) (D0 m) Carry0 = D0 (Add' n m Carry0)
    type instance Add' (D1 n) (D0 m) Carry0 = D1 (Add' n m Carry0)
    --
    type instance Add' (Dn n) (D1 m) Carry0 = D0 (Add' n m Carry0)
    type instance Add' (D0 n) (D1 m) Carry0 = D1 (Add' n m Carry0)
    type instance Add' (D1 n) (D1 m) Carry0 = Dn (Add' n m Carry1)
    -- Carry '-'
    type instance Add' (Dn n) (Dn m) CarryN = D0 (Add' n m CarryN)
    type instance Add' (D0 n) (Dn m) CarryN = D1 (Add' n m CarryN)
    type instance Add' (D1 n) (Dn m) CarryN = Dn (Add' n m Carry0)
    --
    type instance Add' (Dn n) (D0 m) CarryN = D1 (Add' n m CarryN)
    type instance Add' (D0 n) (D0 m) CarryN = Dn (Add' n m Carry0)
    type instance Add' (D1 n) (D0 m) CarryN = D0 (Add' n m Carry0)
    --
    type instance Add' (Dn n) (D1 m) CarryN = Dn (Add' n m Carry0)
    type instance Add' (D0 n) (D1 m) CarryN = D0 (Add' n m Carry0)
    type instance Add' (D1 n) (D1 m) CarryN = D1 (Add' n m Carry0)
    -- Carry '+'
    type instance Add' (Dn n) (Dn m) Carry1 = Dn (Add' n m Carry0)
    type instance Add' (D0 n) (Dn m) Carry1 = D0 (Add' n m Carry0)
    type instance Add' (D1 n) (Dn m) Carry1 = D1 (Add' n m Carry0)
    --
    type instance Add' (Dn n) (D0 m) Carry1 = D0 (Add' n m Carry0)
    type instance Add' (D0 n) (D0 m) Carry1 = D1 (Add' n m Carry0)
    type instance Add' (D1 n) (D0 m) Carry1 = Dn (Add' n m Carry1)
    --
    type instance Add' (Dn n) (D1 m) Carry1 = D1 (Add' n m Carry0)
    type instance Add' (D0 n) (D1 m) Carry1 = Dn (Add' n m Carry1)
    type instance Add' (D1 n) (D1 m) Carry1 = D0 (Add' n m Carry1)

    -- Instances for AddN
    type instance Add     ZZ     ZZ = ZZ
    type instance Add     ZZ (Dn n) = Normalized (Dn n)
    type instance Add     ZZ (D0 n) = Normalized (D0 n)
    type instance Add     ZZ (D1 n) = Normalized (D1 n)
    type instance Add (Dn n)     ZZ = Normalized (Dn n)
    type instance Add (D0 n)     ZZ = Normalized (D0 n)
    type instance Add (D1 n)     ZZ = Normalized (D1 n)
    --
    type instance Add (Dn n) (Dn m) = Normalized (Add' (Dn n) (Dn m) Carry0)
    type instance Add (D0 n) (Dn m) = Normalized (Add' (D0 n) (Dn m) Carry0)
    type instance Add (D1 n) (Dn m) = Normalized (Add' (D1 n) (Dn m) Carry0)
    --
    type instance Add (Dn n) (D0 m) = Normalized (Add' (Dn n) (D0 m) Carry0)
    type instance Add (D0 n) (D0 m) = Normalized (Add' (D0 n) (D0 m) Carry0)
    type instance Add (D1 n) (D0 m) = Normalized (Add' (D1 n) (D0 m) Carry0)
    --
    type instance Add (Dn n) (D1 m) = Normalized (Add' (Dn n) (D1 m) Carry0)
    type instance Add (D0 n) (D1 m) = Normalized (Add' (D0 n) (D1 m) Carry0)
    type instance Add (D1 n) (D1 m) = Normalized (Add' (D1 n) (D1 m) Carry0)

    ----------------------------------------------------------------
    -- Subtraction.
    --
    -- Subtraction is much easier since is ise defined using
    -- addition and negation

    type instance Sub     ZZ     ZZ = ZZ
    type instance Sub     ZZ (Dn n) = Negate (Dn n)
    type instance Sub     ZZ (D0 n) = Negate (D0 n)
    type instance Sub     ZZ (D1 n) = Negate (D1 n)
    type instance Sub (Dn n)     ZZ = (Dn n)
    type instance Sub (D0 n)     ZZ = (D0 n)
    type instance Sub (D1 n)     ZZ = (D1 n)

    type instance Sub (Dn n) (Dn m) = Add (Dn n) (Negate (Dn m))
    type instance Sub (D0 n) (Dn m) = Add (D0 n) (Negate (Dn m))
    type instance Sub (D1 n) (Dn m) = Add (D1 n) (Negate (Dn m))
    --
    type instance Sub (Dn n) (D0 m) = Add (Dn n) (Negate (D0 m))
    type instance Sub (D0 n) (D0 m) = Add (D0 n) (Negate (D0 m))
    type instance Sub (D1 n) (D0 m) = Add (D1 n) (Negate (D0 m))
    --
    type instance Sub (Dn n) (D1 m) = Add (Dn n) (Negate (D1 m))
    type instance Sub (D0 n) (D1 m) = Add (D0 n) (Negate (D1 m))
    type instance Sub (D1 n) (D1 m) = Add (D1 n) (Negate (D1 m))

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

    type instance Mul n    ZZ  = ZZ
    type instance Mul n (Dn m) = Normalized (Add' (Negate n) (D0 (Mul n m)) Carry0)
    type instance Mul n (D0 m) = Normalized (D0 (Mul n m))
    type instance Mul n (D1 m) = Normalized (Add'         n  (D0 (Mul n m)) Carry0)