diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,14 @@
+# Version 0.5
+
+* COMPILER ASSISTED BREAKING CHANGE: `integerVal`, `someIntegerVal`,
+  `fromSInteger` and `withSomeSInteger` now deal with `KindInteger`'s
+  `Integer`s, rather than `Prelude`'s `Integer`s.
+
+* COMPILER ASSISTED BREAKING CHANGE: Removed `fromSInteger'`.
+
+* Added `SingI` and `SingKind` instances.
+
+
 # Version 0.4
 
 * COMPILER ASSISTED BREAKING CHANGE: `TestEquality` and `TestCoercion` consider
diff --git a/kind-integer.cabal b/kind-integer.cabal
--- a/kind-integer.cabal
+++ b/kind-integer.cabal
@@ -1,6 +1,6 @@
 cabal-version: 2.4
 name: kind-integer
-version: 0.4
+version: 0.5
 license: BSD-3-Clause
 license-file: LICENSE
 extra-source-files: README.md CHANGELOG.md
diff --git a/lib/KindInteger.hs b/lib/KindInteger.hs
--- a/lib/KindInteger.hs
+++ b/lib/KindInteger.hs
@@ -34,7 +34,6 @@
   , SInteger
   , pattern SInteger
   , fromSInteger
-  , fromSInteger'
   , withSomeSInteger
   , withKnownInteger
 
@@ -83,8 +82,7 @@
 
 --------------------------------------------------------------------------------
 
--- | Type-level version of 'P.Integer', only ever used as a /kind/
--- for 'P' and 'N'
+-- | Type-level version of 'P.Integer', mostly used as a /kind/ for 'P' and 'N'.
 --
 -- * A positive number /+x/ is represented as @'P' x@.
 --
@@ -102,11 +100,16 @@
 -- at the term-level is so that you embed it in larger data-types (for example,
 -- the "KindRational" module from the
 -- [@kind-rational@](https://hackage.haskell.org/package/kind-rational)
--- library embeds this 'I.Integer' in its 'KindRational.Rational' type)
+-- library embeds this 'I.Integer' in its 'KindRational.Rational' type).
+-- Contrary to "Prelude"'s 'P.Integer', "KindInteger"'s 'Integer' preserves
+-- the internal distinction between @'P' 0@ and @'N' 0@, this is why functions
+-- such as 'fromSInteger' prefer to use "KindInteger"'s 'Integer' rather
+-- than "Prelude"'s 'P.Integer'.
 data Integer
   = P_ Natural
   | N_ Natural
 
+-- | Note that @'P' 0 '==' 'N' 0@.
 instance Eq Integer where
   a == b = toPrelude a P.== toPrelude b
 
@@ -194,19 +197,21 @@
 instance L.KnownNat x => KnownInteger (N x) where
   integerSing = UnsafeSInteger (N_ (fromInteger (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 -> toPrelude x
+-- | Term-level "KindRational" 'Integer' representation of the type-level
+-- 'Integer' @i@.
+integerVal :: forall i proxy. KnownInteger i => proxy i -> 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))
+-- | Convert a term-level "KindInteger" 'Integer' into an unknown
+-- type-level 'Integer'.
+someIntegerVal :: Integer -> SomeInteger
+someIntegerVal i = withSomeSInteger i $ \(si :: SInteger i) ->
+                   withKnownInteger si (SomeInteger @i Proxy)
 
+-- | Note that @'P' 0 '==' 'N' 0@.
 instance Eq SomeInteger where
   SomeInteger x == SomeInteger y = integerVal x P.== integerVal y
 
@@ -526,21 +531,15 @@
   testCoercion = decideCoercion
   {-# INLINE testCoercion #-}
 
--- | Return the term-level "Prelude" 'P.Integer' number corresponding to @i@
--- in a @'SInteger' i@ value.
-fromSInteger :: SInteger i -> P.Integer
-fromSInteger (UnsafeSInteger i) = toPrelude i
-{-# INLINE fromSInteger #-}
-
 -- | Return the term-level "KindInteger" 'Integer' number corresponding to @i@
 -- in a @'SInteger' i@ value.
-fromSInteger' :: SInteger i -> Integer
-fromSInteger' (UnsafeSInteger i) = i
-{-# INLINE fromSInteger' #-}
+fromSInteger :: SInteger i -> Integer
+fromSInteger (UnsafeSInteger i) = i
+{-# INLINE fromSInteger #-}
 
 -- | Whether the internal representation of the 'Integer's are equal.
 --
--- Note that this is not the same as '(==)'. Use '(==)' unless you
+-- Note that this is not the same as '(P.==)'. Use '(P.==)' unless you
 -- know what you are doing.
 eqIntegerRep :: Integer -> Integer -> Bool
 eqIntegerRep (N_ l) (N_ r) = l P.== r
@@ -554,17 +553,31 @@
   :: 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'.
+-- | Convert a "KindIiteger" '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 (fromPrelude n))
+  :: forall rep (r :: TYPE rep). 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 #-}
 
 --------------------------------------------------------------------------------
 
 type instance Sing = SInteger
+
+instance KnownInteger i => SingI (i :: Integer) where
+  sing = integerSing
+  {-# INLINE sing #-}
+
+-- | 'Demote' refers to "KindInteger"'s 'Integer' rather than "Prelude"'s
+-- 'Integer' so that the 'SInteger''s internal representation is preserved.
+-- Use 'toPrelude' and 'fromPrelude' as necessary.
+instance SingKind Integer where
+  type Demote Integer = Integer
+  fromSing = fromSInteger
+  {-# INLINE fromSing #-}
+  toSing i = withSomeSInteger i SomeSing
+  {-# INLINE toSing #-}
 
 -- | Note that this checks for type equality. That is, @'P' 0@ and @'N' 0@
 -- are not equal types, even if they are treated equally elsewhere in
diff --git a/test/Main.hs b/test/Main.hs
--- a/test/Main.hs
+++ b/test/Main.hs
@@ -308,28 +308,33 @@
 
   , assert "integerVal . someIntegerVal == id" $
     flip all [-5 .. 5] $ \a ->
-      case K.someIntegerVal a of
-        K.SomeInteger pa ->
-          a == K.integerVal pa
+      let a' = K.fromPrelude a
+      in case K.someIntegerVal a' of
+           K.SomeInteger pa ->
+             a' == K.integerVal pa
 
   , assert "sameIntegerVal a a" $
     flip all [-5 .. 5] $ \a ->
-      case K.someIntegerVal a of
-        K.SomeInteger pa ->
-          isJust (K.sameInteger pa pa)
+      let a' = K.fromPrelude a
+      in 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)
+      let a' = K.fromPrelude a
+      in 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)
+      let a' = K.fromPrelude a
+          b' = K.fromPrelude b
+      in 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 fromPrelude" $
     flip all (liftA2 (,) [-5 .. 5] [-5 .. 5])$ \(a, b) ->
@@ -351,21 +356,26 @@
 
   , assert "Eq SomeInteger" $
     flip all (liftA2 (,) [-5 .. 5] [-5 .. 5])$ \(a, b) ->
-      (a == b) == (K.someIntegerVal a == K.someIntegerVal b)
+      let a' = K.fromPrelude a
+          b' = K.fromPrelude b
+      in (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)
+      compare a b ==
+         compare (K.someIntegerVal (K.fromPrelude a))
+                 (K.someIntegerVal (K.fromPrelude b))
 
   , assert "Show SomeInteger" $
-    flip all [-5 .. 5] $ \i ->
-      show i == show (K.someIntegerVal i)
+    flip all [-5 .. 5] $ \a ->
+      let a' = K.fromPrelude a
+      in show a == show (K.someIntegerVal a')
 
   , assert "Read SomeInteger" $
     flip all [-5 .. 5] $ \i ->
       let str = show (i :: P.Integer)
       in readMaybe @P.Integer str
-            == fmap (\(K.SomeInteger p) -> K.integerVal p)
+            == fmap (\(K.SomeInteger p) -> K.toPrelude (K.integerVal p))
                     (readMaybe @K.SomeInteger str)
 
   , assert "TestEquality +0 +0" $