diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,3 @@
+# Version 0.1
+
+* Initial version.
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,27 @@
+Copyright (c) 2023, Renzo Carbonara.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are
+met:
+
+1. Redistributions of source code must retain the above copyright
+notice, this list of conditions and the following disclaimer.
+
+2. Redistributions in binary form must reproduce the above copyright
+notice, this list of conditions and the following disclaimer in the
+documentation and/or other materials provided with the distribution.
+
+3. Neither the name of the copyright holder nor the names of its
+contributors may be used to endorse or promote products derived from
+this software without specific prior written permission.  THIS SOFTWARE
+IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY
+EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR
+PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR
+CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,4 @@
+# kind-integer
+
+Haskell type-level `Integer`s. Like `KnownNat`, but for `Integer`s.
+
diff --git a/kind-integer.cabal b/kind-integer.cabal
new file mode 100644
--- /dev/null
+++ b/kind-integer.cabal
@@ -0,0 +1,46 @@
+cabal-version: 2.4
+name: kind-integer
+version: 0.1
+license: BSD-3-Clause
+license-file: LICENSE
+extra-source-files: README.md CHANGELOG.md
+author: Renzo Carbonara
+maintainer: renλren.zone
+copyright: Copyright (c) Renzo Carbonara 2023
+category: Types
+build-type: Simple
+synopsis: Type-level integers. Like KnownNat, but for integers.
+description: Type-level integers. Like KnownNat, but for integers.
+homepage: https://github.com/k0001/hs-kind
+bug-reports: https://github.com/k0001/hs-kind/issues
+tested-with: GHC ==9.2.5, GHC ==9.4.3
+
+source-repository head
+  type: git
+  location: https://github.com/k0001/hs-kind
+  subdir: kind-integer
+
+common basic
+  default-language: GHC2021
+  ghc-options: -O2 -Wall -Werror=incomplete-patterns
+  build-depends: base ==4.*
+  default-extensions:
+    DataKinds
+    NoStarIsType
+    PatternSynonyms
+    TypeFamilies
+    TypeOperators
+    ViewPatterns
+
+library
+  import: basic
+  hs-source-dirs: lib
+  build-depends: ghc-prim
+  exposed-modules: KindInteger
+
+test-suite test
+  import: basic
+  type: exitcode-stdio-1.0
+  hs-source-dirs: test
+  main-is: Main.hs
+  build-depends: kind-integer
diff --git a/lib/KindInteger.hs b/lib/KindInteger.hs
new file mode 100644
--- /dev/null
+++ b/lib/KindInteger.hs
@@ -0,0 +1,404 @@
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+-- | This module provides a type-level representation for term-level
+-- 'P.Integer's. This type-level representation is also named 'P.Integer',
+-- So import this module qualified to avoid name conflicts.
+--
+-- @
+-- import "KindInteger" qualified as K
+-- @
+--
+-- The implementation details are the same as the ones for type-level 'Natural's
+-- in "GHC.TypeNats" as of @base-4.18@, and it will continue to evolve together
+-- with @base@, trying to follow its API as much as possible until the day
+-- @base@ provides its own type-level integer, making this module redundant.
+module KindInteger
+  ( -- * Integer Kind
+    Integer
+  , type P
+  , type N
+  , Normalize
+
+    -- * Linking type and value level
+  , KnownInteger(integerSing), integerVal, integerVal'
+  , SomeInteger(..)
+  , someIntegerVal
+  , sameInteger
+
+    -- ** Singleton values
+  , SInteger
+  , pattern SInteger
+  , fromSInteger
+  , withSomeSInteger
+  , withKnownInteger
+
+    -- * Arithmethic
+  , type (+), type (*), type (^), type (-)
+  , Negate, Div, Mod, Quot, Rem, Log2
+
+    -- * Comparisons
+  , CmpInteger
+  , cmpInteger
+  , type (==?), type (==), type (/=?), type (/=)
+  ) where
+
+import GHC.Base (WithDict(..))
+import GHC.Types (TYPE, Constraint)
+import GHC.Show (appPrec, appPrec1)
+import GHC.Prim (Proxy#)
+import GHC.TypeLits qualified as L
+import Data.Proxy
+import Data.Type.Coercion
+import Data.Type.Equality (TestEquality(..), (:~:)(..))
+import Data.Type.Bool (If)
+import Data.Type.Ord
+import Numeric.Natural (Natural)
+import Prelude hiding (Integer, (==), (/=))
+import Prelude qualified as P
+import Unsafe.Coerce(unsafeCoerce)
+
+--------------------------------------------------------------------------------
+
+-- | Type-level version of 'P.Integer', only ever used as a /kind/
+-- for 'P' and 'N'
+--
+-- * A positive number /+x/ is represented as @'P' x@.
+--
+-- * A negative number /-x/ is represented as @'N' x@.
+--
+-- * /Zero/ can be represented as @'P' 0@ or @'N' 0@. For consistency, all
+-- /zero/ outputs from type families in this "KindInteger" module use the
+-- @'P' 0@, but don't assume that this will be the case elsewhere. So, if you
+-- need to treat /zero/ specially in some situation, be sure to handle both the
+-- @'P' 0@ and @'N' 0@ cases.
+data Integer
+  = Positive Natural
+  | Negative Natural
+
+-- | * A positive number /+x/ is represented as @'P' x@.
+--
+-- * /Zero/ can be represented as @'P' 0@ (see notes at 'Integer').
+type P (x :: Natural) = 'Positive x :: Integer
+
+-- | * A negative number /-x/ is represented as @'N' x@.
+--
+-- * /Zero/ can be represented as @'N' 0@ (but often isn't, see notes at 'Integer').
+type N (x :: Natural) = 'Negative x :: Integer
+
+-- Not used:
+--
+-- typeIntegerToTermInteger :: Integer -> P.Integer
+-- typeIntegerToTermInteger (P n) = toInteger n
+-- typeIntegerToTermInteger (N n) = negate (toInteger n)
+
+termIntegerToTypeInteger :: P.Integer -> Integer
+termIntegerToTypeInteger i = let n = fromInteger i
+                             in  if i >= 0 then Positive n else Negative n
+
+-- | We are not interested in giving any instance to type-level 'Integer's,
+-- so we implement 'showsPrec' here.
+showsPrecInteger :: Int -> Integer -> ShowS
+showsPrecInteger p i = showParen (p > appPrec) $ case i of
+  Positive x -> showString "P " . shows x
+  Negative x -> showString "N " . shows x
+
+--------------------------------------------------------------------------------
+
+-- | This class gives the integer associated with a type-level integer.
+-- There are instances of the class for every integer.
+class KnownInteger (i :: Integer) where
+  integerSing :: SInteger i
+
+-- | Positive numbers and zero.
+instance L.KnownNat x => KnownInteger (P x) where
+  integerSing = UnsafeSInteger (L.natVal (Proxy @x))
+
+-- | Negative numbers and zero.
+instance L.KnownNat x => KnownInteger (N x) where
+  integerSing = UnsafeSInteger (negate (L.natVal (Proxy @x)))
+
+-- | Term-level 'P.Integer' representation of the type-level 'Integer' @i@.
+integerVal :: forall i proxy. KnownInteger i => proxy i -> P.Integer
+integerVal _ = case integerSing :: SInteger i of UnsafeSInteger x -> x
+
+-- | Term-level 'P.Integer' representation of the type-level 'Integer' @i@.
+integerVal' :: forall i. KnownInteger i => Proxy# i -> P.Integer
+integerVal' _ = case integerSing :: SInteger i of UnsafeSInteger x -> x
+
+-- | This type represents unknown type-level 'Integer'.
+data SomeInteger = forall n. KnownInteger n => SomeInteger (Proxy n)
+
+-- | Convert a term-level 'P.Integer' into an unknown type-level 'Integer'.
+someIntegerVal :: P.Integer -> SomeInteger
+someIntegerVal i = withSomeSInteger i (\(si :: SInteger i) ->
+                   withKnownInteger si (SomeInteger @i Proxy))
+
+instance Eq SomeInteger where
+  SomeInteger x == SomeInteger y = integerVal x P.== integerVal y
+
+instance Ord SomeInteger where
+  compare (SomeInteger x) (SomeInteger y) =
+    compare (integerVal x) (integerVal y)
+
+instance Show SomeInteger where
+  showsPrec p (SomeInteger x) = showsPrec p (integerVal x)
+
+instance Read SomeInteger where
+  readsPrec p xs = do (a, ys) <- readsPrec p xs
+                      [(someIntegerVal a, ys)]
+
+--------------------------------------------------------------------------------
+-- Within this module, we use these “normalization” tools to make sure that
+-- /zero/ is always represented as @'P' 0@. We don't export any of these
+-- normalization tools to end-users because it seems like we can't make them
+-- reliable enough so as to offer a decent user experience. So, we just tell
+-- users to deal with the fact that both @'P' 0@ and @'N' 0@ mean /zero/.
+
+-- | Make sure /zero/ is represented as @'P' 0@, not as @'N' 0@
+--
+-- Notice that all the tools in the "KindInteger" can readily handle
+-- non-'Normalize'd inputs. This 'Normalize' type-family is offered offered
+-- only as a convenience in case you want to simplify /your/ dealing with
+-- /zeros/.
+type family Normalize (i :: Integer) :: Integer where
+  Normalize (N 0) = P 0
+  Normalize i     = i
+
+-- | Construct a 'Normalize'd 'N'egative type-level 'Integer'.
+--
+-- To be used for producing all negative outputs in this module.
+type NN (a :: Natural) = Normalize (N a) :: Integer
+
+--------------------------------------------------------------------------------
+
+infixl 6 +, -
+infixl 7 *, `Div`, `Mod`, `Quot`, `Rem`
+infixr 8 ^
+
+-- | Negation of type-level 'Integer's.
+type family Negate (x :: Integer) :: Integer where
+  Negate (P 0) = P 0
+  Negate (P x) = N x
+  Negate (N x) = P x
+
+-- | Addition of type-level 'Integer's.
+type (a :: Integer) + (b :: Integer) = Add_ (Normalize a) (Normalize b) :: Integer
+type family Add_ (a :: Integer) (b :: Integer) :: Integer where
+  Add_ (P a) (P b) = P (a L.+ b)
+  Add_ (N a) (N b) = NN (a L.+ b)
+  Add_ (P a) (N b) = If (b <=? a) (P (a L.- b)) (NN (b L.- a))
+  Add_ (N a) (P b) = Add_ (P b) (N a)
+
+-- | Multiplication of type-level 'Integer's.
+type (a :: Integer) * (b :: Integer) = Mul_ (Normalize a) (Normalize b) :: Integer
+type family Mul_ (a :: Integer) (b :: Integer) :: Integer where
+  Mul_ (P a) (P b) = P (a L.* b)
+  Mul_ (N a) (N b) = Mul_ (P a) (P b)
+  Mul_ (P a) (N b) = NN (a L.* b)
+  Mul_ (N a) (P b) = Mul_ (P a) (N b)
+
+-- | Exponentiation of type-level 'Integer's.
+--
+-- * Exponentiation by negative 'Integer' doesn't type-check.
+type (a :: Integer) ^ (b :: Integer) = Pow_ (Normalize a) (Normalize b) :: Integer
+type family Pow_ (a :: Integer) (b :: Integer) :: Integer where
+  Pow_ (P a) (P b) = P (a L.^ b)
+  Pow_ (N a) (P b) = NN (a L.^ b)
+  Pow_ _     (N _) = L.TypeError ('L.Text "KindInteger.(^): Negative exponent")
+
+-- | Subtraction of type-level 'Integer's.
+type (a :: Integer) - (b :: Integer) = a + Negate b :: Integer
+
+-- | Division ('floor'ed) of type-level 'Integer's.
+--
+-- @
+-- forall (a :: 'Integer') (b :: 'Integer').
+--   /such that/ (b '/=' 0).
+--     a  '=='  'Div' a b '*' 'Negate' b '+' 'Mod' a b
+-- @
+--
+-- * Division by /zero/ doesn't type-check.
+type Div (a :: Integer) (b :: Integer) = Div_ (Normalize a) (Normalize b) :: Integer
+type family Div_ (a :: Integer) (b :: Integer) :: Integer where
+  Div_ _ (P 0) = L.TypeError ('L.Text "KindInteger.Div: Division by zero")
+  Div_ (P a) (P b) = P (L.Div a b)
+  Div_ (N a) (N b) = Div_ (P a) (P b)
+  Div_ (P a) (N b) = NN (If (b L.* (L.Div a b) ==? a) (L.Div a b) (L.Div a b L.+ 1))
+  Div_ (N a) (P b) = Div_ (P a) (N b)
+
+-- | Modulus ('floor'ed division) of type-level 'Integer's.
+--
+-- @
+-- forall (a :: 'Integer') (b :: 'Integer').
+--   /such that/ (b '/=' 0).
+--     a  '=='  'Div' a b '*' 'Negate' b '+' 'Mod' a b
+-- @
+--
+-- * Modulus by /zero/ doesn't type-check.
+type Mod (a :: Integer) (b :: Integer) = Div a b * Negate b + a :: Integer
+
+-- | Division ('truncate'd) of type-level 'Integer's.
+--
+-- @
+-- forall (a :: 'Integer') (b :: 'Integer').
+--   /such that/ (b '/=' 0).
+--     a  '=='  'Quot' a b '*' 'Negate' b '+' 'Rem' a b
+-- @
+--
+-- * Division by /zero/ doesn't type-check.
+type Quot (a :: Integer) (b :: Integer) = Quot_ (Normalize a) (Normalize b) :: Integer
+type family Quot_ (a :: Integer) (b :: Integer) :: Integer where
+  Quot_ _ (P 0) = L.TypeError ('L.Text "KindInteger.Quot: Division by zero")
+  Quot_ (P a) (P b) = P (L.Div a b)
+  Quot_ (N a) (N b) = Quot_ (P a) (P b)
+  Quot_ (P a) (N b) = Negate (Quot_ (P a) (P b))
+  Quot_ (N a) (P b) = Quot_ (P a) (N b)
+
+-- | Remulus ('truncate'd division) of type-level 'Integer's.
+--
+-- @
+-- forall (a :: 'Integer') (b :: 'Integer').
+--   /such that/ (b '/=' 0).
+--     a  '=='  'Quot' a b '*' 'Negate' b '+' 'Rem' a b
+-- @
+--
+-- * Remulus by /zero/ doesn't type-check.
+type Rem (a :: Integer) (b :: Integer) = Quot a b * Negate b + a :: Integer
+
+-- | Log base 2 ('floor'ed) of integer numbers.
+--
+-- * Logarithm of /zero/ doesn't type-check.
+--
+-- * Logarithm of negative number doesn't type-check.
+type Log2 (a :: Integer) = Log2_ (Normalize a) :: Integer
+type family Log2_ (a :: Integer) :: Integer where
+  Log2_ (P 0) = L.TypeError ('L.Text "KindInteger.Log2: Logarithm of zero")
+  Log2_ (P a) = P (L.Log2 a)
+  Log2_ (N a) = L.TypeError ('L.Text "KindInteger.Log2: Logarithm of negative number")
+
+-- | Comparison of type-level integers, as a function.
+type CmpInteger (a :: Integer) (b :: Integer) = CmpInteger_ (Normalize a) (Normalize b) :: Ordering
+type family CmpInteger_ (a :: Integer) (b :: Integer) :: Ordering where
+  CmpInteger_ a a = 'EQ
+  CmpInteger_ (P a) (P b) = Compare a b
+  CmpInteger_ (N a) (N b) = Compare b a
+  CmpInteger_ (N _) (P _) = 'LT
+  CmpInteger_ (P _) (N _) = 'GT
+
+-- | "Data.Type.Ord" support for type-level 'Integer's.
+type instance Compare (a :: Integer) (b :: Integer) = CmpInteger a b :: Ordering
+
+--------------------------------------------------------------------------------
+
+-- | We either get evidence that this function was instantiated with the
+-- same type-level 'Integer's, or 'Nothing'.
+sameInteger
+  :: forall a b proxy1 proxy2
+  .  (KnownInteger a, KnownInteger b)
+  => proxy1 a
+  -> proxy2 b
+  -> Maybe (a :~: b)
+sameInteger _ _ = testEquality (integerSing @a) (integerSing @b)
+
+-- | Like 'sameInteger', but if the type-level 'Integer's aren't equal, this
+-- additionally provides proof of 'LT' or 'GT'.
+cmpInteger
+  :: forall a b proxy1 proxy2
+  .  (KnownInteger a, KnownInteger b)
+  => proxy1 a
+  -> proxy2 b
+  -> OrderingI a b
+cmpInteger x y = case compare (integerVal x) (integerVal y) of
+  EQ -> case unsafeCoerce (Refl, Refl) :: (CmpInteger a b :~: 'EQ, a :~: b) of
+    (Refl, Refl) -> EQI
+  LT -> case unsafeCoerce Refl :: (CmpInteger a b :~: 'LT) of
+    Refl -> LTI
+  GT -> case unsafeCoerce Refl :: (CmpInteger a b :~: 'GT) of
+    Refl -> GTI
+
+--------------------------------------------------------------------------------
+
+-- | Singleton type for a type-level 'Integer' @i@.
+newtype SInteger (i :: Integer) = UnsafeSInteger P.Integer
+
+-- | A explicitly bidirectional pattern synonym relating an 'SInteger' to a
+-- 'KnownInteger' constraint.
+--
+-- As an __expression__: Constructs an explicit @'SInteger' i@ value from an
+-- implicit @'KnownInteger' i@ constraint:
+--
+-- @
+-- 'SInteger' @i :: 'KnownInteger' i => 'SInteger' i
+-- @
+--
+-- As a __pattern__: Matches on an explicit @'SInteger' i@ value bringing
+-- an implicit @'KnownInteger' i@ constraint into scope:
+--
+-- @
+-- f :: 'SInteger' i -> ..
+-- f SInteger = {- SInteger i in scope -}
+-- @
+pattern SInteger :: forall i. () => KnownInteger i => SInteger i
+pattern SInteger <- (knownIntegerInstance -> KnownIntegeregerInstance)
+  where SInteger = integerSing
+
+-- | An internal data type that is only used for defining the 'SInteger' pattern
+-- synonym.
+data KnownIntegeregerInstance (i :: Integer) where
+  KnownIntegeregerInstance :: KnownInteger i => KnownIntegeregerInstance i
+
+-- | An internal function that is only used for defining the 'SInteger' pattern
+-- synonym.
+knownIntegerInstance :: SInteger i -> KnownIntegeregerInstance i
+knownIntegerInstance si = withKnownInteger si KnownIntegeregerInstance
+
+instance Show (SInteger i) where
+  showsPrec p (UnsafeSInteger i) = showParen (p > appPrec) $
+    showString "SInteger @" .
+    showsPrecInteger appPrec1 (termIntegerToTypeInteger i)
+
+instance TestEquality SInteger where
+  testEquality (UnsafeSInteger x) (UnsafeSInteger y)
+    | x P.== y  = Just (unsafeCoerce Refl)
+    | otherwise = Nothing
+
+instance TestCoercion SInteger where
+  testCoercion x y = fmap (\Refl -> Coercion) (testEquality x y)
+
+-- | Return the type-level 'P.Integer' number corresponding to @i@ in
+-- a @'SInteger' i@ value.
+fromSInteger :: SInteger i -> P.Integer
+fromSInteger (UnsafeSInteger i) = i
+
+-- | Convert an explicit @'SInteger' i@ value into an implicit
+-- @'KnownInteger' i@ constraint.
+withKnownInteger
+  :: forall i rep (r :: TYPE rep). SInteger i -> (KnownInteger i => r) -> r
+withKnownInteger = withDict @(KnownInteger i)
+
+-- | Convert a 'P.Integer' number into an @'SInteger' n@ value, where @n@ is a
+-- fresh type-level 'Integer'.
+withSomeSInteger
+  :: forall rep (r :: TYPE rep). P.Integer -> (forall n. SInteger n -> r) -> r
+withSomeSInteger n k = k (UnsafeSInteger n)
+-- It's very important to keep this NOINLINE! See the docs at "GHC.TypeNats"
+{-# NOINLINE withSomeSInteger #-}
+
+--------------------------------------------------------------------------------
+-- Extras
+
+infixr 4 /=, /=?, ==, ==?
+
+-- | This should be exported by 'Data.Type.Ord'.
+type (a :: k) ==? (b :: k) = OrdCond (Compare a b) 'False 'True 'False :: Bool
+
+-- | This should be exported by 'Data.Type.Ord'.
+type (a :: k) == (b :: k) = (a ==? b) ~ 'True :: Constraint
+
+-- | This should be exported by 'Data.Type.Ord'.
+type (a :: k) /=? (b :: k) = OrdCond (Compare a b) 'True 'False 'True :: Bool
+
+-- | This should be exported by 'Data.Type.Ord'.
+type (a :: k) /= (b :: k) = (a /=? b) ~ 'True :: Constraint
+
diff --git a/test/Main.hs b/test/Main.hs
new file mode 100644
--- /dev/null
+++ b/test/Main.hs
@@ -0,0 +1,374 @@
+{-# LANGUAGE MagicHash #-}
+module Main (main) where
+
+import Control.Applicative
+import Data.Maybe
+import Data.Proxy
+import Data.Type.Ord (type (<=))
+import GHC.Exts (Constraint, proxy#)
+import System.Exit
+import Text.Read
+
+import KindInteger (P, N)
+import KindInteger qualified as K
+
+--------------------------------------------------------------------------------
+
+data Dict (c :: Constraint) where
+  Dict :: c => Dict c
+
+--------------------------------------------------------------------------------
+
+_testEq =  Dict
+_testEq :: Dict
+  ( P 0 K.== P 0,   'True ~ (P 0 K.==? P 0)
+  , N 0 K.== N 0,   'True ~ (N 0 K.==? N 0)
+  , P 0 K.== N 0,   'True ~ (P 0 K.==? N 0)
+  , N 0 K.== P 0,   'True ~ (N 0 K.==? P 0)
+
+  , P 0 K./= P 1,   'True ~ (P 0 K./=? P 1)
+  , P 0 K./= N 1,   'True ~ (P 0 K./=? N 1)
+
+  , N 0 K./= N 1,   'True ~ (N 0 K./=? N 1)
+  , N 0 K./= N 1,   'True ~ (N 0 K./=? N 1)
+
+  , P 1 K./= P 0,   'True ~ (P 1 K./=? P 0)
+  , P 1 K./= N 0,   'True ~ (P 1 K./=? N 0)
+
+  , N 1 K./= N 0,   'True ~ (N 1 K./=? N 0)
+  , N 1 K./= N 0,   'True ~ (N 1 K./=? N 0)
+  )
+
+_testCmp =  Dict
+_testCmp :: Dict
+  ( P 0 <= P 0
+  , P 0 <= N 0
+  , N 0 <= P 0
+  , N 0 <= N 0
+
+  , N 2 <= N 1
+  , N 1 <= N 0
+  , N 0 <= P 1
+
+  , P 0 <= P 1
+  , P 1 <= P 2
+  )
+
+_testAdd  = Dict
+_testAdd :: Dict
+  ( P 0 ~ P 0 K.+ P 0
+  , P 0 ~ N 0 K.+ N 0
+  , P 0 ~ P 0 K.+ N 0
+  , P 0 ~ N 0 K.+ P 0
+
+  , P 1 ~ P 1 K.+ P 0
+  , N 1 ~ N 1 K.+ N 0
+  , P 1 ~ P 1 K.+ N 0
+  , N 1 ~ N 1 K.+ P 0
+
+  , P 1 ~ P 0 K.+ P 1
+  , N 1 ~ N 0 K.+ N 1
+  , N 1 ~ P 0 K.+ N 1
+  , P 1 ~ N 0 K.+ P 1
+
+  , P 2 ~ P 1 K.+ P 1
+  , N 2 ~ N 1 K.+ N 1
+  , P 0 ~ P 1 K.+ N 1
+  , P 0 ~ N 1 K.+ P 1
+  )
+
+_testMul  = Dict
+_testMul :: Dict
+  ( P 0 ~ P 0 K.* P 0
+  , P 0 ~ N 0 K.* N 0
+  , P 0 ~ P 0 K.* N 0
+  , P 0 ~ N 0 K.* P 0
+
+  , P 0 ~ P 1 K.* P 0
+  , P 0 ~ N 1 K.* N 0
+  , P 0 ~ P 1 K.* N 0
+  , P 0 ~ N 1 K.* P 0
+
+  , P 0 ~ P 0 K.* P 1
+  , P 0 ~ N 0 K.* N 1
+  , P 0 ~ P 0 K.* N 1
+  , P 0 ~ N 0 K.* P 1
+
+  , P 1 ~ P 1 K.* P 1
+  , P 1 ~ N 1 K.* N 1
+  , N 1 ~ P 1 K.* N 1
+  , N 1 ~ N 1 K.* P 1
+
+  , P 2 ~ P 2 K.* P 1
+  , P 2 ~ N 2 K.* N 1
+  , N 2 ~ P 2 K.* N 1
+  , N 2 ~ N 2 K.* P 1
+
+  , P 6 ~ P 2 K.* P 3
+  , P 6 ~ N 2 K.* N 3
+  , N 6 ~ P 2 K.* N 3
+  , N 6 ~ N 2 K.* P 3
+  )
+
+_testDiv  = Dict
+_testDiv :: Dict
+  ( P 0 ~ P 0 `K.Div` P 1
+  , P 0 ~ N 0 `K.Div` N 1
+  , P 0 ~ P 0 `K.Div` N 1
+  , P 0 ~ N 0 `K.Div` P 1
+
+  , P 1 ~ P 1 `K.Div` P 1
+  , P 1 ~ N 1 `K.Div` N 1
+  , N 1 ~ P 1 `K.Div` N 1
+  , N 1 ~ N 1 `K.Div` P 1
+
+  , P 2 ~ P 2 `K.Div` P 1
+  , P 2 ~ N 2 `K.Div` N 1
+  , N 2 ~ P 2 `K.Div` N 1
+  , N 2 ~ N 2 `K.Div` P 1
+
+  , P 1 ~ P 2 `K.Div` P 2
+  , P 1 ~ N 2 `K.Div` N 2
+  , N 1 ~ P 2 `K.Div` N 2
+  , N 1 ~ N 2 `K.Div` P 2
+
+  , P 1 ~ P 3 `K.Div` P 2
+  , P 1 ~ N 3 `K.Div` N 2
+  , N 2 ~ P 3 `K.Div` N 2
+  , N 2 ~ N 3 `K.Div` P 2
+
+  , P 0 ~ P 0 `K.Div` P 1
+  , P 0 ~ N 0 `K.Div` N 1
+  , P 0 ~ P 0 `K.Div` N 1
+  , P 0 ~ N 0 `K.Div` P 1
+
+  , P 0 ~ P 1 `K.Div` P 2
+  , P 0 ~ N 1 `K.Div` N 2
+  , N 1 ~ P 1 `K.Div` N 2
+  , N 1 ~ N 1 `K.Div` P 2
+  )
+
+_testMod  = Dict
+_testMod :: Dict
+  ( P 0 ~ P 0 `K.Mod` P 1
+  , P 0 ~ N 0 `K.Mod` N 1
+  , P 0 ~ P 0 `K.Mod` N 1
+  , P 0 ~ N 0 `K.Mod` P 1
+
+  , P 0 ~ P 1 `K.Mod` P 1
+  , P 0 ~ N 1 `K.Mod` N 1
+  , P 0 ~ P 1 `K.Mod` N 1
+  , P 0 ~ N 1 `K.Mod` P 1
+
+  , P 0 ~ P 2 `K.Mod` P 1
+  , P 0 ~ N 2 `K.Mod` N 1
+  , P 0 ~ P 2 `K.Mod` N 1
+  , P 0 ~ N 2 `K.Mod` P 1
+
+  , P 0 ~ P 2 `K.Mod` P 2
+  , P 0 ~ N 2 `K.Mod` N 2
+  , P 0 ~ P 2 `K.Mod` N 2
+  , P 0 ~ N 2 `K.Mod` P 2
+
+  , P 1 ~ P 3 `K.Mod` P 2
+  , N 1 ~ N 3 `K.Mod` N 2
+  , N 1 ~ P 3 `K.Mod` N 2
+  , P 1 ~ N 3 `K.Mod` P 2
+
+  , P 0 ~ P 0 `K.Mod` P 1
+  , P 0 ~ N 0 `K.Mod` N 1
+  , P 0 ~ P 0 `K.Mod` N 1
+  , P 0 ~ N 0 `K.Mod` P 1
+
+  , P 1 ~ P 1 `K.Mod` P 2
+  , N 1 ~ N 1 `K.Mod` N 2
+  , N 1 ~ P 1 `K.Mod` N 2
+  , P 1 ~ N 1 `K.Mod` P 2
+  )
+
+_testQuot  = Dict
+_testQuot :: Dict
+  ( P 0 ~ P 0 `K.Quot` P 1
+  , P 0 ~ N 0 `K.Quot` N 1
+  , P 0 ~ P 0 `K.Quot` N 1
+  , P 0 ~ N 0 `K.Quot` P 1
+
+  , P 1 ~ P 1 `K.Quot` P 1
+  , P 1 ~ N 1 `K.Quot` N 1
+  , N 1 ~ P 1 `K.Quot` N 1
+  , N 1 ~ N 1 `K.Quot` P 1
+
+  , P 2 ~ P 2 `K.Quot` P 1
+  , P 2 ~ N 2 `K.Quot` N 1
+  , N 2 ~ P 2 `K.Quot` N 1
+  , N 2 ~ N 2 `K.Quot` P 1
+
+  , P 1 ~ P 2 `K.Quot` P 2
+  , P 1 ~ N 2 `K.Quot` N 2
+  , N 1 ~ P 2 `K.Quot` N 2
+  , N 1 ~ N 2 `K.Quot` P 2
+
+  , P 1 ~ P 3 `K.Quot` P 2
+  , P 1 ~ N 3 `K.Quot` N 2
+  , N 1 ~ P 3 `K.Quot` N 2
+  , N 1 ~ N 3 `K.Quot` P 2
+
+  , P 0 ~ P 0 `K.Quot` P 1
+  , P 0 ~ N 0 `K.Quot` N 1
+  , P 0 ~ P 0 `K.Quot` N 1
+  , P 0 ~ N 0 `K.Quot` P 1
+
+  , P 0 ~ P 1 `K.Quot` P 2
+  , P 0 ~ N 1 `K.Quot` N 2
+  , P 0 ~ P 1 `K.Quot` N 2
+  , P 0 ~ N 1 `K.Quot` P 2
+  )
+
+_testRem  = Dict
+_testRem :: Dict
+  ( P 0 ~ P 0 `K.Rem` P 1
+  , P 0 ~ N 0 `K.Rem` N 1
+  , P 0 ~ P 0 `K.Rem` N 1
+  , P 0 ~ N 0 `K.Rem` P 1
+
+  , P 0 ~ P 1 `K.Rem` P 1
+  , P 0 ~ N 1 `K.Rem` N 1
+  , P 0 ~ P 1 `K.Rem` N 1
+  , P 0 ~ N 1 `K.Rem` P 1
+
+  , P 0 ~ P 2 `K.Rem` P 1
+  , P 0 ~ N 2 `K.Rem` N 1
+  , P 0 ~ P 2 `K.Rem` N 1
+  , P 0 ~ N 2 `K.Rem` P 1
+
+  , P 0 ~ P 2 `K.Rem` P 2
+  , P 0 ~ N 2 `K.Rem` N 2
+  , P 0 ~ P 2 `K.Rem` N 2
+  , P 0 ~ N 2 `K.Rem` P 2
+
+  , P 1 ~ P 3 `K.Rem` P 2
+  , N 1 ~ N 3 `K.Rem` N 2
+  , P 1 ~ P 3 `K.Rem` N 2
+  , N 1 ~ N 3 `K.Rem` P 2
+
+  , P 0 ~ P 0 `K.Rem` P 1
+  , P 0 ~ N 0 `K.Rem` N 1
+  , P 0 ~ P 0 `K.Rem` N 1
+  , P 0 ~ N 0 `K.Rem` P 1
+
+  , P 1 ~ P 1 `K.Rem` P 2
+  , N 1 ~ N 1 `K.Rem` N 2
+  , P 1 ~ P 1 `K.Rem` N 2
+  , N 1 ~ N 1 `K.Rem` P 2
+  )
+
+_testLog2 =  Dict
+_testLog2 :: Dict
+  ( P 0 ~ K.Log2 (P 1)
+  , P 1 ~ K.Log2 (P 2)
+  , P 1 ~ K.Log2 (P 3)
+  , P 2 ~ K.Log2 (P 4)
+  , P 2 ~ K.Log2 (P 5)
+  , P 2 ~ K.Log2 (P 6)
+  , P 2 ~ K.Log2 (P 7)
+  , P 3 ~ K.Log2 (P 8)
+  , P 3 ~ K.Log2 (P 9)
+  , P 3 ~ K.Log2 (P 10)
+  , P 3 ~ K.Log2 (P 11)
+  , P 3 ~ K.Log2 (P 12)
+  , P 3 ~ K.Log2 (P 13)
+  , P 3 ~ K.Log2 (P 14)
+  , P 3 ~ K.Log2 (P 15)
+  , P 4 ~ K.Log2 (P 16)
+  , P 4 ~ K.Log2 (P 17)
+  , P 4 ~ K.Log2 (P 18)
+  , P 4 ~ K.Log2 (P 19)
+  , P 4 ~ K.Log2 (P 20)
+  , P 4 ~ K.Log2 (P 21)
+  , P 4 ~ K.Log2 (P 22)
+  , P 4 ~ K.Log2 (P 23)
+  , P 4 ~ K.Log2 (P 24)
+  , P 4 ~ K.Log2 (P 25)
+  , P 4 ~ K.Log2 (P 26)
+  , P 4 ~ K.Log2 (P 27)
+  , P 4 ~ K.Log2 (P 28)
+  , P 4 ~ K.Log2 (P 29)
+  , P 4 ~ K.Log2 (P 30)
+  , P 4 ~ K.Log2 (P 31)
+  , P 5 ~ K.Log2 (P 32)
+  )
+
+--------------------------------------------------------------------------------
+
+assert
+  :: String  -- ^ Test name
+  -> Bool    -- ^ Successful is true
+  -> IO Bool -- ^ Return the same 'Bool' given as input.
+assert n x = do
+  putStrLn ((if x then "[OK] " else "[FAIL] ") <> n)
+  pure x
+
+testsMain :: [IO Bool] -> IO a
+testsMain xs = do
+  oks <- sequence xs
+  if and oks
+     then do putStrLn "All tests passed successfully."
+             exitSuccess
+     else do putStrLn "Some tests failed."
+             exitFailure
+
+main :: IO ()
+main = testsMain
+  [ assert "integerVal . someIntegerVal == id" $
+    flip all [-5 .. 5] $ \a ->
+      case K.someIntegerVal a of
+        K.SomeInteger pa ->
+          a == K.integerVal pa
+
+  , assert "integerVal' . someIntegerVal == id" $
+    flip all [-5 .. 5] $ \a ->
+      case K.someIntegerVal a of
+        K.SomeInteger (_ :: Proxy a) ->
+          a == K.integerVal' (proxy# @a)
+
+  , assert "sameIntegerVal a a" $
+    flip all [-5 .. 5] $ \a ->
+      case K.someIntegerVal a of
+        K.SomeInteger pa ->
+          isJust (K.sameInteger pa pa)
+
+  , assert "sameIntegerVal a a'" $
+    flip all [-5 .. 5] $ \a ->
+      case (K.someIntegerVal a, K.someIntegerVal a) of
+        (K.SomeInteger pa1, K.SomeInteger pa2) ->
+          isJust (K.sameInteger pa1 pa2)
+
+  , assert "sameIntegerVal a b" $
+    flip all (liftA2 (,) [-5 .. 5] [-5 .. 5])$ \(a, b) ->
+      case (K.someIntegerVal a, K.someIntegerVal b) of
+        (K.SomeInteger pa, K.SomeInteger pb)
+          | a == b    -> isJust    (K.sameInteger pa pb)
+          | otherwise -> isNothing (K.sameInteger pa pb)
+
+  , assert "Eq SomeInteger" $
+    flip all (liftA2 (,) [-5 .. 5] [-5 .. 5])$ \(a, b) ->
+      (a == b) == (K.someIntegerVal a == K.someIntegerVal b)
+
+  , assert "Ord SomeInteger" $
+    flip all (liftA2 (,) [-5 .. 5] [-5 .. 5])$ \(a, b) ->
+      (a `compare` b) == (K.someIntegerVal a `compare` K.someIntegerVal b)
+
+  , assert "Show SomeInteger" $
+    flip all [-5 .. 5] $ \i ->
+      show i == show (K.someIntegerVal i)
+
+  , assert "Read SomeInteger" $
+    flip all [-5 .. 5] $ \i ->
+      let str = show (i :: Integer)
+      in readMaybe @Integer str
+            == fmap (\(K.SomeInteger p) -> K.integerVal p)
+                    (readMaybe @K.SomeInteger str)
+
+  ]
+
+