diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,22 @@
+# Version 0.4
+
+* COMPILER ASSISTED BREAKING CHANGE: `TestEquality` and `TestCoercion` consider
+  `N 0` and `P 0` to be different.
+
+* BREAKING CHANGE: The `Integer` inside `SInteger`s is not automatically
+  normalized anymore. This is so that `SDecide`, `TestEquality` and
+  `TestCoercion` behave as expected, treating `N 0` and `P 0` differently.
+  This is mostly an internal change, but it can be observed in the `Show`
+  instance for `SInteger`, for example.
+
+* Added role annotations to `SInteger`.
+
+* Add dependency on `singletons` so that we can give a `Sing` and `SDecide`
+  instances for type-level `Integer`s.
+
+* Export `fromSInteger'`, `eqIntegerRep`.
+
+
 # Version 0.3
 
 * COMPILER ASSISTED BREAKING CHANGE: Renamed `Mod` to `Rem`, `DivMod` to
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.3
+version: 0.4
 license: BSD-3-Clause
 license-file: LICENSE
 extra-source-files: README.md CHANGELOG.md
@@ -28,6 +28,7 @@
     DataKinds
     MultiWayIf
     NoStarIsType
+    RoleAnnotations
     PatternSynonyms
     TypeFamilies
     TypeOperators
@@ -35,8 +36,8 @@
 
 library
   import: basic
+  build-depends: singletons
   hs-source-dirs: lib
-  build-depends: ghc-prim
   exposed-modules: KindInteger
 
 test-suite test
diff --git a/lib/KindInteger.hs b/lib/KindInteger.hs
--- a/lib/KindInteger.hs
+++ b/lib/KindInteger.hs
@@ -34,6 +34,7 @@
   , SInteger
   , pattern SInteger
   , fromSInteger
+  , fromSInteger'
   , withSomeSInteger
   , withKnownInteger
 
@@ -54,6 +55,7 @@
     -- * Comparisons
   , CmpInteger
   , cmpInteger
+  , eqIntegerRep
 
     -- * Extra
   , type (==?), type (==), type (/=?), type (/=)
@@ -63,15 +65,17 @@
 import Control.Exception qualified as Ex
 import Data.Bits
 import Data.Proxy
+import Data.Singletons
+import Data.Singletons.Decide
 import Data.Type.Bool (If)
 import Data.Type.Coercion
-import Data.Type.Equality (TestEquality(..), (:~:)(..))
+import Data.Type.Equality (TestEquality(..))
 import Data.Type.Ord
 import GHC.Base (WithDict(..))
+import GHC.Exts (TYPE, Constraint)
 import GHC.Real qualified as P
 import GHC.Show (appPrec, appPrec1)
 import GHC.TypeLits qualified as L
-import GHC.Types (TYPE, Constraint)
 import Numeric.Natural (Natural)
 import Prelude hiding (Integer, (==), (/=), div, rem)
 import Prelude qualified as P
@@ -179,15 +183,21 @@
 
 -- | Positive numbers and zero.
 instance L.KnownNat x => KnownInteger (P x) where
-  integerSing = UnsafeSInteger (L.natVal (Proxy @x))
+  integerSing = UnsafeSInteger (P_ (fromInteger (L.natVal (Proxy @x))))
 
 -- | Negative numbers and zero.
+--
+-- Implementation note: Notice that @'N' 0@ will not be 'Normalize'd to
+-- @'P' 0@. This is so that 'SDecide', 'TestEquality' and 'TestCoercion'
+-- behave as expected. If you want a 'Normalize'd 'SInteger', then use
+-- @'integerSing' \@('Normalize' i)@.
 instance L.KnownNat x => KnownInteger (N x) where
-  integerSing = UnsafeSInteger (negate (L.natVal (Proxy @x)))
+  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 -> x
+integerVal _ = case integerSing :: SInteger i of
+                 UnsafeSInteger x -> toPrelude x
 
 -- | This type represents unknown type-level 'Integer'.
 data SomeInteger = forall n. KnownInteger n => SomeInteger (Proxy n)
@@ -464,7 +474,8 @@
 --------------------------------------------------------------------------------
 
 -- | Singleton type for a type-level 'Integer' @i@.
-newtype SInteger (i :: Integer) = UnsafeSInteger P.Integer
+newtype SInteger (i :: Integer) = UnsafeSInteger Integer
+type role SInteger representational
 
 -- | A explicitly bidirectional pattern synonym relating an 'SInteger' to a
 -- 'KnownInteger' constraint.
@@ -499,22 +510,44 @@
 
 instance Show (SInteger i) where
   showsPrec p (UnsafeSInteger i) = showParen (p > appPrec) $
-    showString "SInteger @" .
-    showsPrec appPrec1 (fromPrelude i)
+    showString "SInteger @" . showsPrecTypeLit appPrec1 i
 
+-- | 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
+-- "KindInteger".
 instance TestEquality SInteger where
-  testEquality (UnsafeSInteger x) (UnsafeSInteger y)
-    | x P.== y  = Just (unsafeCoerce Refl)
-    | otherwise = Nothing
+  testEquality = decideEquality
+  {-# INLINE testEquality #-}
 
+-- | 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
+-- "KindInteger".
 instance TestCoercion SInteger where
-  testCoercion x y = fmap (\Refl -> Coercion) (testEquality x y)
+  testCoercion = decideCoercion
+  {-# INLINE testCoercion #-}
 
--- | Return the term-level 'P.Integer' number corresponding to @i@ in
--- a @'SInteger' i@ value.
+-- | Return the term-level "Prelude" 'P.Integer' number corresponding to @i@
+-- in a @'SInteger' i@ value.
 fromSInteger :: SInteger i -> P.Integer
-fromSInteger (UnsafeSInteger i) = i
+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' #-}
+
+-- | Whether the internal representation of the 'Integer's are equal.
+--
+-- Note that this is not the same as '(==)'. Use '(==)' unless you
+-- know what you are doing.
+eqIntegerRep :: Integer -> Integer -> Bool
+eqIntegerRep (N_ l) (N_ r) = l P.== r
+eqIntegerRep (P_ l) (P_ r) = l P.== r
+eqIntegerRep _      _      = False
+{-# INLINE eqIntegerRep #-}
+
 -- | Convert an explicit @'SInteger' i@ value into an implicit
 -- @'KnownInteger' i@ constraint.
 withKnownInteger
@@ -525,9 +558,22 @@
 -- fresh type-level 'Integer'.
 withSomeSInteger
   :: forall rep (r :: TYPE rep). P.Integer -> (forall n. SInteger n -> r) -> r
-withSomeSInteger n k = k (UnsafeSInteger n)
+withSomeSInteger n k = k (UnsafeSInteger (fromPrelude n))
 -- It's very important to keep this NOINLINE! See the docs at "GHC.TypeNats"
 {-# NOINLINE withSomeSInteger #-}
+
+--------------------------------------------------------------------------------
+
+type instance Sing = SInteger
+
+-- | 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
+-- "KindInteger".
+instance SDecide Integer where
+  UnsafeSInteger l %~ UnsafeSInteger r =
+    case eqIntegerRep l r of
+      True  -> Proved (unsafeCoerce Refl)
+      False -> Disproved (\Refl -> error "SDecide.Integer")
 
 --------------------------------------------------------------------------------
 
diff --git a/test/Main.hs b/test/Main.hs
--- a/test/Main.hs
+++ b/test/Main.hs
@@ -9,6 +9,7 @@
 import Data.List qualified as List
 import Data.Maybe
 import Data.Ratio as P
+import Data.Type.Equality (TestEquality(..))
 import Data.Type.Ord (type (<=))
 import GHC.Exts (Constraint)
 import Prelude hiding (Integer)
@@ -366,6 +367,49 @@
       in readMaybe @P.Integer str
             == fmap (\(K.SomeInteger p) -> K.integerVal p)
                     (readMaybe @K.SomeInteger str)
+
+  , assert "TestEquality +0 +0" $
+     isJust (testEquality (K.SInteger @(P 0)) (K.SInteger @(P 0)))
+  , assert "TestEquality -0 -0" $
+     isJust (testEquality (K.SInteger @(N 0)) (K.SInteger @(N 0)))
+  , assert "TestEquality +0 -0" $
+     isNothing (testEquality (K.SInteger @(P 0)) (K.SInteger @(N 0)))
+  , assert "TestEquality -0 +0" $
+     isNothing (testEquality (K.SInteger @(N 0)) (K.SInteger @(P 0)))
+  , assert "TestEquality +0 +1" $
+     isNothing (testEquality (K.SInteger @(P 0)) (K.SInteger @(P 1)))
+  , assert "TestEquality +0 -1" $
+     isNothing (testEquality (K.SInteger @(P 0)) (K.SInteger @(N 1)))
+  , assert "TestEquality -0 +1" $
+     isNothing (testEquality (K.SInteger @(N 0)) (K.SInteger @(P 1)))
+  , assert "TestEquality -0 -1" $
+     isNothing (testEquality (K.SInteger @(N 0)) (K.SInteger @(N 1)))
+  , assert "TestEquality +1 +0" $
+     isNothing (testEquality (K.SInteger @(P 1)) (K.SInteger @(P 0)))
+  , assert "TestEquality +1 -0" $
+     isNothing (testEquality (K.SInteger @(P 1)) (K.SInteger @(N 0)))
+  , assert "TestEquality -1 +0" $
+     isNothing (testEquality (K.SInteger @(N 1)) (K.SInteger @(P 0)))
+  , assert "TestEquality -1 -0" $
+     isNothing (testEquality (K.SInteger @(N 1)) (K.SInteger @(N 0)))
+
+  , assert "Show Integer +0" $
+     "0" == show (K.fromSInteger (K.SInteger @(P 0)))
+  , assert "Show Integer -0" $
+     "0" == show (K.fromSInteger (K.SInteger @(N 0)))
+  , assert "Show Integer +1" $
+     "1" == show (K.fromSInteger (K.SInteger @(P 1)))
+  , assert "Show Integer -1" $
+     "-1" == show (K.fromSInteger (K.SInteger @(N 1)))
+
+  , assert "Show SInteger +0" $
+     "SInteger @(P 0)" == show (K.SInteger @(P 0))
+  , assert "Show SInteger -0" $
+     "SInteger @(N 0)" == show (K.SInteger @(N 0))
+  , assert "Show SInteger +1" $
+     "SInteger @(P 1)" == show (K.SInteger @(P 1))
+  , assert "Show SInteger -1" $
+     "SInteger @(N 1)" == show (K.SInteger @(N 1))
 
   ] <> testsDivRem