-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Type-level integers. Like KnownNat, but for integers.
--   
--   Type-level integers. Like KnownNat, but for integers.
@package kind-integer
@version 0.6.0


-- | This module provides a type-level representation for term-level
--   <a>Integer</a>s. This type-level representation is also named
--   <a>Integer</a>, So import this module qualified to avoid name
--   conflicts.
--   
--   <pre>
--   import <a>KindInteger</a> qualified as KI
--   </pre>
--   
--   The implementation details are similar to the ones for type-level
--   <a>Natural</a>s as of <tt>base-4.18</tt> and
--   <tt>singletons-base-3.1.1</tt>, and they will continue to evolve
--   together with <tt>base</tt> and <tt>singletons-base</tt>, trying to
--   more or less follow their API.
module KindInteger

-- | Type-level version of <a>Integer</a>, only used as a <i>kind</i>.
--   
--   <ul>
--   <li>Zero is represented as <a>Z</a>.</li>
--   <li>A positive number <i>+x</i> is represented as <tt><a>P</a>
--   x</tt>.</li>
--   <li>A negative number <i>-x</i> is represented as <tt><a>N</a>
--   x</tt>.</li>
--   </ul>
data Integer

-- | Zero is represented as <a>Z</a>.
type Z = 'Z :: Integer

-- | <pre>
--   <a>SZ</a> == <a>sing</a> @Z
--   </pre>
pattern SZ :: SInteger Z

-- | A negative number <i>-x</i> is represented as <tt><a>N</a> x</tt>.
--   
--   While a standalone <tt><a>N</a> 0</tt> type-checks, it is not
--   considered valid, so tools like <a>KnownInteger</a> or
--   <a>Normalized</a> will reject it. <tt><a>N</a> 0</tt> itself is not
--   rejected so that it can be used to pattern-match against
--   <a>Integer</a>s at the type-level if necessary.
type N (x :: Natural) = 'N x :: Integer

-- | <pre>
--   <a>SN</a> (<a>sing</a> @1) == <a>sing</a> @(N 1)
--   </pre>
pattern SN :: 0 < x => (KnownInteger (N x), KnownNat x) => Sing (x :: Natural) -> SInteger (N x)

-- | A positive number <i>+x</i> is represented as <tt><a>P</a> x</tt>.
--   
--   While a standalone <tt><a>P</a> 0</tt> type-checks, it is not
--   considered valid, so tools like <a>KnownInteger</a> or
--   <a>Normalized</a> will reject it. <tt><a>P</a> 0</tt> itself is not
--   rejected so that it can be used to pattern-match against
--   <a>Integer</a>s at the type-level if necessary.
type P (x :: Natural) = 'P x :: Integer

-- | <pre>
--   <a>SP</a> (<a>sing</a> @1) == <a>sing</a> @(P 1)
--   </pre>
pattern SP :: 0 < x => (KnownInteger (P x), KnownNat x) => Sing (x :: Natural) -> SInteger (P x)

-- | Construct a type-level <a>Integer</a> from a type-level
--   <a>Natural</a>.
type family FromNatural (x :: Natural) :: Integer

-- | Singleton version of <a>FromNatural</a>.
sFromNatural :: Sing (x :: Natural) -> SInteger (FromNatural x)

-- | <tt><a>Fold</a> z n p i</tt> evaluates to <tt>z</tt> if <tt>i</tt> is
--   zero, otherwise applies <tt>n</tt> to the absolute value of <tt>i</tt>
--   if negative, or <tt>p</tt> to the absolute value of <tt>i</tt> if
--   positive. <tt><a>N</a> 0</tt> and <tt><a>P</a> 0</tt> fail to
--   type-check.
type family Fold (z :: k) (n :: Natural ~> k) (p :: Natural ~> k) (i :: Integer) :: k

-- | Singleton version of <a>Fold</a>.
sFold :: SingKind k => Sing (z :: k) -> Sing (n :: Natural ~> k) -> Sing (p :: Natural ~> k) -> SInteger i -> Sing (Fold z n p i)

-- | Type-level <a>Integer</a>s satisfying <a>KnownInteger</a> can be
--   converted to <a>SInteger</a>s using <a>integerSing</a>. Every
--   <a>Integer</a> other than <tt><a>Integer</a> 0</tt> and
--   <tt><a>Integer</a> 0</tt> are <a>KnownInteger</a>s.
type KnownInteger (i :: Integer) = (KnownInteger_ i, Normalized i ~ i, KnownNat (Abs i))

-- | <tt><a>Normalized</a> i</tt> is an identity function that fails to
--   type-check if <tt>i</tt> is not in normalized form. That is,
--   <i>zero</i> is represented with <a>Z</a>, not with <tt><a>P</a> 0</tt>
--   or <tt> <a>N</a> 0</tt>.
type family Normalized (i :: Integer) :: Integer

-- | Convert an implicit <a>KnownInteger</a> to an explicit
--   <a>SInteger</a>.
integerSing :: KnownInteger i => SInteger i

-- | Term-level <a>Prelude</a>.<a>Integer</a> representation of the
--   type-level <a>Integer</a>.
integerVal :: forall i proxy. KnownInteger i => proxy i -> Integer

-- | Convert an explicit <tt><a>SInteger</a> i</tt> value into an implicit
--   <tt><a>KnownInteger</a> i</tt> constraint.
withKnownInteger :: forall i rep (x :: TYPE rep). SInteger i -> (KnownInteger i => x) -> x

-- | Term-level representation of an existentialized <a>KnownInteger</a>.
data SomeInteger
SomeInteger :: Proxy i -> SomeInteger

-- | Convert a term-level <a>Prelude</a>.<a>Integer</a> into an
--   extistentialized <a>KnownInteger</a> wrapped in <a>SomeInteger</a>.
someIntegerVal :: Integer -> SomeInteger

-- | Singleton type for a type-level <a>Integer</a> <tt>i</tt>.
data SInteger (i :: Integer)

-- | A explicitly bidirectional pattern synonym relating an <a>SInteger</a>
--   to a <a>KnownInteger</a> constraint.
--   
--   As an <b>expression</b>: Constructs an explicit <tt><a>SInteger</a>
--   i</tt> value from an implicit <tt><a>KnownInteger</a> i</tt>
--   constraint:
--   
--   <pre>
--   <a>SInteger</a> @i :: <a>KnownInteger</a> i =&gt; <a>SInteger</a> i
--   </pre>
--   
--   As a <b>pattern</b>: Matches on an explicit <tt><a>SInteger</a> i</tt>
--   value bringing an implicit <tt><a>KnownInteger</a> i</tt> constraint
--   into scope:
--   
--   <pre>
--   f :: <a>SInteger</a> i -&gt; ..
--   f si@<a>SInteger</a> = <i>... both (si :: <a>SInteger</a> i) and (<a>KnownInteger</a> i) in scope ...</i>
--   </pre>
pattern SInteger :: forall i. () => KnownInteger i => SInteger i

-- | Return the term-level <a>Prelude</a>.<a>Integer</a> number
--   corresponding to <tt>i</tt>.
fromSInteger :: SInteger i -> Integer

-- | Convert a <a>Prelude</a>.<a>Integer</a> number into an
--   <tt><a>SInteger</a> n</tt> value, where <tt>n</tt> is a fresh
--   type-level <a>Integer</a>.
withSomeSInteger :: forall rep (x :: TYPE rep). Integer -> (forall (i :: Integer). Sing i -> x) -> x

-- | Double negation is identity.
sNegateRefl :: SInteger i -> i :~: Negate (Negate i)

-- | Identity.
sZigZagRefl :: SInteger i -> i :~: ZagZig (ZigZag i)

-- | Identity.
sZagZigRefl :: Sing (n :: Natural) -> n :~: ZigZag (ZagZig n)

-- | Displays <tt>i</tt> as it would show literally as a type.
--   
--   <pre>
--   <a>ShowLit</a> ( <a>N</a> 1) ~ "P 1"
--   <a>ShowLit</a>   <a>Z</a>    ~ "Z"
--   <a>ShowLit</a> ( <a>P</a> 1) ~ "P 1"
--   </pre>
--   
--   <tt><a>N</a> 0</tt> and <tt><a>P</a> 0</tt> fail to type-check.
type ShowLit (i :: Integer) = ShowsLit i "" :: Symbol

-- | Demoted version of <a>ShowLit</a>.
showLit :: Integer -> String

-- | Singleton version of <a>ShowLit</a>.
--   
--   <pre>
--   <a>fromSing</a> @(<a>sShowLit</a> (<a>SN</a> (<a>sing</a> @1))) == "N 1"
--   <a>fromSing</a> @(<a>sShowLit</a> <a>SZ</a>)             == "Z"
--   <a>fromSing</a> @(<a>sShowLit</a> (<a>SP</a> (<a>sing</a> @1))) == "P 1"
--   </pre>
sShowLit :: SInteger i -> Sing (ShowLit i)

-- | Displays <tt>i</tt> as it would show literally as a type. See
--   'ShowLit. Behaves like <a>Shows</a>.
type ShowsLit (i :: Integer) (s :: Symbol) = ShowsPrecLit 0 i s :: Symbol

-- | Demoted version of <a>ShowsLit</a>.
showsLit :: Integer -> ShowS

-- | Singleton version of <a>ShowsLit</a>.
sShowsLit :: SInteger i -> Sing (s :: Symbol) -> Sing (ShowsLit i s)

-- | Displays <tt>i</tt> as it would show literally as a type. See
--   'ShowLit. Behaves like <a>ShowsPrec</a>.
type ShowsPrecLit p i s = ShowsPrecLit_ p (Normalized i) s

-- | Demoted version of <a>ShowsPrecLit</a>.
showsPrecLit :: Int -> Integer -> ShowS

-- | Singleton version of <a>ShowsPrecLit</a>.
sShowsPrecLit :: Sing (p :: Natural) -> SInteger i -> Sing (s :: Symbol) -> Sing (ShowsPrecLit p i s)

-- | Inverse of <a>showsPrecLit</a>.
readPrecLit :: ReadPrec Integer

-- | Exponentiation of type-level <a>Integer</a>s.
type (b :: Integer) ^ (p :: Natural) = Pow (Normalized b) p :: Integer
infixr 8 ^

-- | Singleton version of <a>^</a>.
(%^) :: Sing (b :: Integer) -> Sing (p :: Natural) -> Sing (b ^ p :: Integer)
infixr 8 %^

-- | Whether a type-level <a>Integer</a> is odd. <i>Zero</i> is not
--   considered odd.
type Odd (i :: Integer) = Mod (Abs i) 2 == 1 :: Bool

-- | Singleton version of <a>Odd</a>.
sOdd :: SInteger i -> Sing (Odd i :: Bool)

-- | Whether a type-level <a>Integer</a> is even. <i>Zero</i> is considered
--   even.
type Even (i :: Integer) = Mod (Abs i) 2 == 0 :: Bool

-- | Singleton version of <a>Even</a>.
sEven :: SInteger i -> Sing (Even i :: Bool)

-- | Absolute value of a type-level <a>Integer</a>, as a type-level
--   <a>Natural</a>.
type Abs (i :: Integer) = Fold 0 IdSym0 IdSym0 i :: Natural

-- | Singleton version of <a>Abs</a>.
sAbs :: SInteger i -> Sing (Abs i :: Natural)

-- | Greatest Common Divisor of type-level <a>Integer</a> numbers
--   <tt>a</tt> and <tt>b</tt>.
--   
--   Returns a <a>Natural</a>, since the Greatest Common Divisor is always
--   positive.
type GCD (a :: Integer) (b :: Integer) = NatGCD (Abs a) (Abs b) :: Natural

-- | Singleton version of <a>GCD</a>.
sGCD :: SInteger a -> SInteger b -> Sing (GCD a b :: Natural)

-- | Least Common Multiple of type-level <a>Integer</a> numbers <tt>a</tt>
--   and <tt>b</tt>.
--   
--   Returns a <a>Natural</a>, since the Least Common Multiple is always
--   positive.
type LCM (a :: Integer) (b :: Integer) = NatLCM (Abs a) (Abs b) :: Natural

-- | Singleton version of <a>LCM</a>.
sLCM :: SInteger a -> SInteger b -> Sing (LCM a b :: Natural)

-- | Log base 2 (<a>floor</a>ed) of type-level <a>Integer</a>s.
--   
--   <ul>
--   <li>Logarithm of <i>zero</i> doesn't type-check.</li>
--   <li>Logarithm of negative number doesn't type-check.</li>
--   </ul>
type Log2 (a :: Integer) = Fold (TypeError ('Text "Logarithm of zero.")) (ConstSym1 (TypeError ('Text "Logarithm of negative number."))) (Log2Sym0) a :: Natural

-- | Singleton version of <a>Log2</a>.
sLog2 :: SInteger i -> Sing (Log2 i :: Natural)

-- | Divide the type-level <a>Integer</a> <tt>a</tt> by <tt>b</tt>, using
--   the specified <a>Round</a>ing <tt>r</tt>.
--   
--   <ul>
--   <li>Division by <i>zero</i> doesn't type-check.</li>
--   </ul>
type Div (r :: Round) (a :: Integer) (b :: Integer) = Div_ r (Normalized a) (Normalized b) :: Integer
infixl 7 `Div`

-- | Singleton version of <a>Div</a>.
sDiv :: SRound r -> SInteger a -> SInteger b -> SInteger (Div r a b)

-- | Demoted version of <a>Div</a>.
--   
--   Throws <a>DivdeByZero</a> where <a>Div</a> would fail to type-check.
div :: Round -> Integer -> Integer -> Integer

-- | <a>Rem</a>ainder of the division of type-level <a>Integer</a>
--   <tt>a</tt> by <tt>b</tt>, using the specified <a>Round</a>ing
--   <tt>r</tt>.
--   
--   <pre>
--   forall (r :: <a>Round</a>) (a :: <a>Integer</a>) (b :: <a>Integer</a>).
--     (b <tt>/=</tt> 0) =&gt;
--       <a>Rem</a> r a b  <tt>==</tt>  a <a>-</a> b <a>*</a> <a>Div</a> r a b
--   </pre>
--   
--   <ul>
--   <li>Division by <i>zero</i> doesn't type-check.</li>
--   </ul>
type Rem (r :: Round) (a :: Integer) (b :: Integer) = Rem_ r (Normalized a) (Normalized b) :: Integer
infixl 7 `Rem`

-- | Singleton version of <a>Rem</a>.
sRem :: SRound r -> SInteger a -> SInteger b -> SInteger (Rem r a b)

-- | Demoted version of <a>Rem</a>.
--   
--   Throws <a>DivdeByZero</a> where <a>Div</a> would fail to type-check.
rem :: Round -> Integer -> Integer -> Integer

-- | Get both the quotient and the <a>Rem</a>ainder of the <a>Div</a>ision
--   of type-level <a>Integer</a>s <tt>a</tt> and <tt>b</tt> using the
--   specified <a>Round</a>ing <tt>r</tt>.
--   
--   <pre>
--   forall (r :: <a>Round</a>) (a :: <a>Integer</a>) (b :: <a>Integer</a>).
--     (b <tt>/=</tt> 0) =&gt;
--       <a>DivRem</a> r a b <tt>==</tt>  '(<a>Div</a> r a b, <a>Rem</a> r a b)
--   </pre>
type DivRem (r :: Round) (a :: Integer) (b :: Integer) = '(Div r a b, Rem r a b) :: (Integer, Integer)
infixl 7 `DivRem`

-- | Singleton version of <a>DivRem</a>.
sDivRem :: SRound r -> SInteger a -> SInteger b -> (SInteger (Div r a b), SInteger (Rem r a b))

-- | Demoted version of <a>DivRem</a>.
--   
--   Throws <a>DivdeByZero</a> where <a>Div</a> would fail to type-check.
divRem :: Round -> Integer -> Integer -> (Integer, Integer)

-- | Rounding strategy.
data Round

-- | Round <b>up</b> towards positive infinity.
RoundUp :: Round

-- | Round <b>down</b> towards negative infinity. Also known as
--   <a>Prelude</a>'s <a>floor</a>. This is the type of rounding used by
--   <a>Prelude</a>'s <a>div</a>, <a>mod</a>, <a>divMod</a>, <a>Div</a>,
--   <a>Mod</a>.
RoundDown :: Round

-- | Round towards <b>zero</b>. Also known as <a>Prelude</a>'s
--   <a>truncate</a>. This is the type of rounding used by <a>Prelude</a>'s
--   <a>quot</a>, <a>rem</a>, <a>quotRem</a>.
RoundZero :: Round

-- | Round <b>away</b> from zero.
RoundAway :: Round

-- | Round towards the closest integer. If <b>half</b>way between two
--   integers, round <b>up</b> towards positive infinity.
RoundHalfUp :: Round

-- | Round towards the closest integer. If <b>half</b>way between two
--   integers, round <b>down</b> towards negative infinity.
RoundHalfDown :: Round

-- | Round towards the closest integer. If <b>half</b>way between two
--   integers, round towards <b>zero</b>.
RoundHalfZero :: Round

-- | Round towards the closest integer. If <b>half</b>way between two
--   integers, round <b>away</b> from zero.
RoundHalfAway :: Round

-- | Round towards the closest integer. If <b>half</b>way between two
--   integers, round towards the closest <b>even</b> integer. Also known as
--   <a>Prelude</a>'s <a>round</a>.
RoundHalfEven :: Round

-- | Round towards the closest integer. If <b>half</b>way between two
--   integers, round towards the closest <b>odd</b> integer.
RoundHalfOdd :: Round
data SRound :: Round -> Type
[SRoundUp] :: SRound ('RoundUp :: Round)
[SRoundDown] :: SRound ('RoundDown :: Round)
[SRoundZero] :: SRound ('RoundZero :: Round)
[SRoundAway] :: SRound ('RoundAway :: Round)
[SRoundHalfUp] :: SRound ('RoundHalfUp :: Round)
[SRoundHalfDown] :: SRound ('RoundHalfDown :: Round)
[SRoundHalfZero] :: SRound ('RoundHalfZero :: Round)
[SRoundHalfAway] :: SRound ('RoundHalfAway :: Round)
[SRoundHalfEven] :: SRound ('RoundHalfEven :: Round)
[SRoundHalfOdd] :: SRound ('RoundHalfOdd :: Round)

-- | Like <a>sameInteger</a>, but if the type-level <a>Integer</a>s aren't
--   equal, this additionally provides proof of <a>LT</a> or <a>GT</a>.
cmpInteger :: forall a b proxy1 proxy2. (KnownInteger a, KnownInteger b) => proxy1 a -> proxy2 b -> OrderingI a b

-- | We either get evidence that this function was instantiated with the
--   same type-level <a>Integer</a>s, or <a>Nothing</a>.
sameInteger :: forall a b proxy1 proxy2. (KnownInteger a, KnownInteger b) => proxy1 a -> proxy2 b -> Maybe (a :~: b)

-- | ZigZag encoding of an <a>Integer</a>.
--   
--   <ul>
--   <li><i>0</i> is <i>0</i></li>
--   <li><i>-x</i> is <i>abs(x) * 2 - 1</i></li>
--   <li><i>+x</i> is <i>x * 2</i></li>
--   </ul>
type ZigZag (i :: Integer) = ZigZag_ (Normalized i) :: Natural

-- | Singleton version of <a>ZigZag</a>.
sZigZag :: SInteger i -> Sing (ZigZag i :: Natural)

-- | Inverse of <a>ZigZag</a>.
type ZagZig n = If (Mod n 2 == 1) (Negate (FromNatural (Div (n + 1) 2))) (FromNatural (Div n 2))

-- | Singleton version of <a>ZagZig</a>.
sZagZig :: Sing (n :: Natural) -> SInteger (ZagZig n)
type ZSym0 = Z
data NSym0 :: Natural ~> Integer
type NSym1 x = N x
data PSym0 :: Natural ~> Integer
type PSym1 x = P x
data FromNaturalSym0 :: Natural ~> Integer
type FromNaturalSym1 i = FromNatural i
data KnownIntegerSym0 :: Integer ~> Constraint
type KnownIntegerSym1 i = KnownInteger i
data NormalizedSym0 :: Integer ~> Integer
type NormalizedSym1 i = Normalized i
data FoldSym0 :: k ~> (Natural ~> k) ~> (Natural ~> k) ~> Integer ~> k
data FoldSym1 :: k -> (Natural ~> k) ~> (Natural ~> k) ~> Integer ~> k
data FoldSym2 :: k -> (Natural ~> k) -> (Natural ~> k) ~> Integer ~> k
data FoldSym3 :: k -> (Natural ~> k) -> (Natural ~> k) -> Integer ~> k
type FoldSym4 z n p i = Fold z n p i
data (^@#@$) :: Integer ~> Natural ~> Integer
data (^@#@$$) :: Integer -> Natural ~> Integer
type (^@#@$$$) b p = b ^ p
infixr 8 ^@#@$$$
data OddSym0 :: Integer ~> Bool
type OddSym1 i = Odd i
data EvenSym0 :: Integer ~> Bool
type EvenSym1 i = Even i
data GCDSym0 :: Integer ~> Integer ~> Natural
data GCDSym1 :: Integer -> Integer ~> Natural
data LCMSym0 :: Integer ~> Integer ~> Natural
data LCMSym1 :: Integer -> Integer ~> Natural
data Log2Sym0 :: Integer ~> Natural
type Log2Sym1 a = Log2 a
data DivSym0 :: Round ~> Integer ~> Integer ~> Integer
data DivSym1 :: Round -> Integer ~> Integer ~> Integer
data DivSym2 :: Round -> Integer -> Integer ~> Integer
type DivSym3 r a b = Div r a b
data RemSym0 :: Round ~> Integer ~> Integer ~> Integer
data RemSym1 :: Round -> Integer ~> Integer ~> Integer
data RemSym2 :: Round -> Integer -> Integer ~> Integer
type RemSym3 r a b = Rem r a b
data DivRemSym0 :: Round ~> Integer ~> Integer ~> (Integer, Integer)
data DivRemSym1 :: Round -> Integer ~> Integer ~> (Integer, Integer)
data DivRemSym2 :: Round -> Integer -> Integer ~> (Integer, Integer)
type DivRemSym3 r a b = DivRem r a b
data ShowLitSym0 :: Integer ~> Symbol
type ShowLitSym1 i = ShowLit i
data ShowsLitSym0 :: Integer ~> Symbol ~> Symbol
data ShowsLitSym1 :: Integer -> Symbol ~> Symbol
type ShowsLitSym2 i s = ShowsLit i s
data ShowsPrecLitSym0 :: Natural ~> Integer ~> Symbol ~> Symbol
data ShowsPrecLitSym1 :: Natural -> Integer ~> Symbol ~> Symbol
data ShowsPrecLitSym2 :: Natural -> Integer -> Symbol ~> Symbol
type ShowsPrecLitSym3 p i s = ShowsPrecLit p i s
type family RoundUpSym0 :: Round
type family RoundDownSym0 :: Round
type family RoundZeroSym0 :: Round
type family RoundAwaySym0 :: Round
type family RoundHalfUpSym0 :: Round
type family RoundHalfDownSym0 :: Round
type family RoundHalfZeroSym0 :: Round
type family RoundHalfAwaySym0 :: Round
type family RoundHalfEvenSym0 :: Round
type family RoundHalfOddSym0 :: Round
instance GHC.Classes.Eq KindInteger.SomeInteger
instance GHC.Classes.Ord KindInteger.SomeInteger
instance GHC.Show.Show KindInteger.SomeInteger
instance GHC.Read.Read KindInteger.SomeInteger
instance (KindInteger.KnownInteger (KindInteger.N n), n GHC.Types.~ KindInteger.Abs (KindInteger.N n)) => KindInteger.KnownInteger_ (KindInteger.N n)
instance (KindInteger.KnownInteger (KindInteger.P n), n GHC.Types.~ KindInteger.Abs (KindInteger.P n)) => KindInteger.KnownInteger_ (KindInteger.P n)
instance KindInteger.KnownInteger i => GHC.Read.Read (KindInteger.SInteger i)
instance KindInteger.KnownInteger i => Data.Singletons.SingI i
instance KindInteger.KnownInteger_ KindInteger.Z
instance GHC.Num.Singletons.SNum KindInteger.Integer
instance GHC.Classes.Eq (KindInteger.SInteger i)
instance GHC.Classes.Ord (KindInteger.SInteger i)
instance GHC.Show.Show (KindInteger.SInteger i)
instance Data.Type.Equality.TestEquality KindInteger.SInteger
instance Data.Type.Coercion.TestCoercion KindInteger.SInteger
instance GHC.Num.Singletons.PNum KindInteger.Integer
instance Text.Show.Singletons.PShow KindInteger.Integer
instance Text.Show.Singletons.SShow KindInteger.Integer
instance Data.Ord.Singletons.POrd KindInteger.Integer
instance Data.Ord.Singletons.SOrd KindInteger.Integer
instance Data.Eq.Singletons.PEq KindInteger.Integer
instance Data.Eq.Singletons.SEq KindInteger.Integer
instance Data.Singletons.SingKind KindInteger.Integer
instance Data.Singletons.Decide.SDecide KindInteger.Integer