{-# 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 (
I
, O
, Z
, Nat(..)
, SomeNat(..)
, withNat
, 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
class Nat n where
toInt :: Integral i => n -> i
class Pos n
instance Nat Z where toInt :: Z -> i
toInt Z
_ = i
0
instance Nat (I Z) where toInt :: I Z -> i
toInt I Z
_ = i
1
instance Nat (O n) => Nat (O (O n)) where toInt :: 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 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 :: 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 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 :: 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 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 :: 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 n i. (Nat n, Integral i) => n -> i
toInt (I n
forall a. HasCallStack => a
undefined :: (I n))
class Number_Is_Denormalized a
instance (Number_Is_Denormalized Z) => Nat (O Z) where
toInt :: O Z -> i
toInt = [Char] -> O Z -> i
forall a. HasCallStack => [Char] -> a
error [Char]
"quench warning"
instance (Nat n, Positive n) => Pos n
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 n i. (Nat n, Integral i) => n -> i
toInt n
n :: Integer)
withNat :: forall i a. (Integral i) => (forall n. Nat n => n -> a) -> i -> a
withNat :: (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) forall n. Nat n => n -> a
forall n m. (Nat n, n ~ O m) => n -> a
f 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) forall n m. (Nat n, n ~ O m) => n -> a
k0' forall n m. (Nat n, n ~ I m) => n -> a
k1'
where
k0' :: forall n m. (Nat n, n ~ O m) => n -> a
k0' :: 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' :: 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)
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 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 n i. (Nat n, Integral i) => n -> i
toInt (I n
forall a. HasCallStack => a
undefined :: I n)
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 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 n i. (Nat n, Integral i) => n -> i
toInt (I n
forall a. HasCallStack => a
undefined :: I n)
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 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 n i. (Nat n, Integral i) => n -> i
toInt (I n
forall a. HasCallStack => a
undefined :: I n)
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 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 n i. (Nat n, Integral i) => n -> i
toInt (I n
forall a. HasCallStack => a
undefined :: I n)
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 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 n i. (Nat n, Integral i) => n -> i
toInt (I n
forall a. HasCallStack => a
undefined :: I n)
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 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 n i. (Nat n, Integral i) => n -> i
toInt (I n
forall a. HasCallStack => a
undefined :: I n)
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 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 n i. (Nat n, Integral i) => n -> i
toInt (I n
forall a. HasCallStack => a
undefined :: I n)
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 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 n i. (Nat n, Integral i) => n -> i
toInt (I n
forall a. HasCallStack => a
undefined :: I n)
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 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 n i. (Nat n, Integral i) => n -> i
toInt (I n
forall a. HasCallStack => a
undefined :: I n)
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 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 n i. (Nat n, Integral i) => n -> i
toInt (I n
forall a. HasCallStack => a
undefined :: I n)
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)
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 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 n i. (Nat n, Integral i) => n -> i
toInt I n
n :: Integer)[Char] -> ShowS
forall a. [a] -> [a] -> [a]
++[Char]
":N]"
type instance Next Z = I Z
type instance Next (I n) = O (Next n)
type instance Next (O n) = I n
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)
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
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
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)
data Carry
data NoCarry
type family Add' n m c :: *
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
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
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)
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)
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)
data Borrow
data NoBorrow
type family Sub' n m c :: *
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
type instance Sub' (O n) Z Borrow = I (Sub' n Z Borrow)
type instance Sub' (I n) Z Borrow = O n
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)
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)
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)
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)