diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,9 +1,28 @@
+# Version 0.3
+
+* COMPILER ASSISTED BREAKING CHANGE: `TestEquality` and `TestCoercion`
+  don't `Normalize` inputs before making a decision anymore.
+
+* BREAKING CHANGE: The `Rational` inside `SRational` is not automatically
+  normalized anymore. This is so that `SDecide`, `TestEquality` and
+  `TestCoercion` behave as expected, treating `1/2` differently than `2/4`,
+  for example. This is mostly an internal change, but it can be observed in
+  the `Show` instance for `SRational`, for example.
+
+* Added role annotations to `SRational`.
+
+* Add dependency on `singletons` so that we can give a `Sing` and `SDecide`
+  instances for type-level `Rational`s.
+
+* Export `fromSRational'`.
+
 # Version 0.2
 
 * COMPILER ASSISTED BREAKING CHANGE: Removed `Mod`, `DivMod`, `mod`, `divMod`.
 
 * COMPILER ASSISTED BREAKING CHANGE: Renamed `Dif` to `Rem`, `DivDif` to
   `DivRem`, `mod` to `rem`, `divDif` to `divRem`.
+
 
 # Version 0.1
 
diff --git a/kind-rational.cabal b/kind-rational.cabal
--- a/kind-rational.cabal
+++ b/kind-rational.cabal
@@ -1,6 +1,6 @@
 cabal-version: 2.4
 name: kind-rational
-version: 0.2
+version: 0.3
 license: BSD-3-Clause
 license-file: LICENSE
 extra-source-files: README.md CHANGELOG.md
@@ -26,11 +26,13 @@
   build-depends:
     base ==4.*,
     kind-integer >=0.2,
+    singletons,
   default-extensions:
     DataKinds
     NoStarIsType
     LambdaCase
     PatternSynonyms
+    RoleAnnotations
     TypeFamilies
     TypeOperators
     ViewPatterns
@@ -38,7 +40,6 @@
 library
   import: basic
   hs-source-dirs: lib
-  build-depends: ghc-prim
   exposed-modules: KindRational
 
 test-suite test
diff --git a/lib/KindRational.hs b/lib/KindRational.hs
--- a/lib/KindRational.hs
+++ b/lib/KindRational.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE StrictData #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE UndecidableSuperClasses #-}
 
@@ -39,6 +40,7 @@
   , SRational
   , pattern SRational
   , fromSRational
+  , fromSRational'
   , withSomeSRational
   , withKnownRational
 
@@ -67,6 +69,7 @@
     -- * Comparisons
   , CmpRational
   , cmpRational
+  , eqRationalRep
 
     -- * Extra
     --
@@ -74,21 +77,22 @@
   , type (==?), type (==), type (/=?), type (/=)
   ) --}
   where
-
-import qualified Control.Exception as Ex
+import Control.Exception qualified as Ex
 import Control.Monad
 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.Read qualified as Read
 import GHC.Real qualified as P (Ratio(..), (%))
 import GHC.Show (appPrec, appPrec1)
 import GHC.TypeLits qualified as L
 import GHC.TypeNats qualified as N
-import GHC.Types (TYPE, Constraint)
 import KindInteger (Integer, N, P)
 import KindInteger (type (==?), type (==), type (/=?), type (/=))
 import KindInteger qualified as I
@@ -128,14 +132,14 @@
     -- or 'fromPrelude' instead.
     --
     -- * At the type-level, safely construct a 'Rational' using '/'.
+    --
+    -- * We keep the numerator and denominator unnormalized because we use them
+    -- to implement 'SDecide', 'TestEquality' and 'TestCoercion'. Even if “1/2”
+    -- and “2/4” mean the same, in 'SDecide' and friends we treat them as the
+    -- different types that they are.
     I.Integer :% Natural
 
-num :: Rational -> I.Integer
-num (n :% _) = n
-
-den :: Rational -> Natural
-den (_ :% d) = d
-
+-- | Arithmethic equality. That is, \(\frac{1}{2} == \frac{2}{4}\).
 instance Eq Rational where
   a == b = toPrelude a == toPrelude b
 
@@ -166,8 +170,8 @@
 -- 'showsPrecTypeLit' 0 ('rationalVal' ('Proxy' \@(1'/'2))) \"z\" == \"P 1 % 2z\"
 -- @
 showsPrecTypeLit :: Int -> Rational -> ShowS
-showsPrecTypeLit p r = showParen (p > appPrec) $
-  I.showsPrecTypeLit appPrec (num r) . showString " % " . shows (den r)
+showsPrecTypeLit p (n :% d) = showParen (p > appPrec) $
+  I.showsPrecTypeLit appPrec n . showString " % " . shows d
 
 -- | Make a term-level "KindRational" 'Rational' number, provided that
 -- the numerator is not @0@, and that its numerator and denominator are
@@ -176,7 +180,7 @@
 rational :: (Integral num, Integral den) => num -> den -> Maybe Rational
 rational = \(toInteger -> n) (toInteger -> d) -> do
     guard (d /= 0 && abs n <= max_ && abs d <= max_)
-    pure $ let n1 P.:% d1 = n P.% d
+    pure $ let n1 P.:% d1 = n P.% d -- 'P.%' normalizes
            in I.fromPrelude n1 :% fromInteger d1
   where
     max_ :: P.Integer -- Some big enough number. TODO: Pick good number.
@@ -200,9 +204,8 @@
     n P.:% d
      | d == 0 -> Ex.throw Ex.RatioZeroDenominator
      | abs n > max_ || abs d > max_ -> Ex.throw Ex.Overflow
-     | otherwise ->
-       let n1 P.:% d1 = n P.% d
-       in I.fromPrelude n1 :% fromInteger d1
+     | otherwise -> let n1 P.:% d1 = n P.% d -- 'P.%' normalizes
+                    in I.fromPrelude n1 :% fromInteger d1
   where
     max_ :: P.Integer -- Some big enough number. TODO: Pick good number.
     max_ = 10 ^ (1000 :: Int)
@@ -211,15 +214,12 @@
 unsafeCheckPrelude :: P.Rational -> P.Rational
 unsafeCheckPrelude = toPrelude . unsafeFromPrelude
 
--- | Convert a term-level "KindRational" 'Rational' into a term-level
--- "Prelude" 'P.Rational'.
+-- | Convert a term-level "KindRational" 'Rational' into a 'Normalized'
+-- term-level "Prelude" 'P.Rational'.
 --
--- @
--- 'fromPrelude' . 'toPrelude'      == 'Just'
--- 'fmap' 'toPrelude' . 'fromPrelude' == 'Just'
--- @
+-- @'fromPrelude' . 'toPrelude' == 'Just'@
 toPrelude :: Rational -> P.Rational
-toPrelude r = I.toPrelude (num r) P.:% toInteger (den r)
+toPrelude (n :% d) = I.toPrelude n P.% toInteger d -- 'P.%' normalizes.
 
 --------------------------------------------------------------------------------
 
@@ -239,7 +239,7 @@
 -- which not only accepts more polymorphic inputs, but also 'Normalize's
 -- the type-level 'Rational'. Also note that while @n '%' 0@ is a valid
 -- type, all tools in the "KindRational" will reject such input.
-type (n :: I.Integer) % (d :: Natural) = n ':% d :: Rational
+type (n :: I.Integer) % (d :: Natural) = n :% d :: Rational
 
 -- | Normalize a type-level 'Rational' so that a /0/ denominator fails to
 -- type-check, and that the 'Num'erator and denominator have no common factors.
@@ -490,7 +490,7 @@
 -- | Term-level version of the "Terminates" function.
 -- Takes a "KindRational" 'P.Rational' as input.
 terminates' :: Rational -> Bool
-terminates' = go . den
+terminates' = \(_ :% d) -> go d
   where
     go = \case
       5 -> True
@@ -519,13 +519,19 @@
 class KnownRational (r :: Rational) where
   rationalSing :: SRational r
 
+-- | This instance checks that @r@ 'Normalize's, but the obtained 'SRational' is
+-- not normalized. This is so that 'SDecide', 'TestEquality' and 'TestCoercion'
+-- behave as expected.  If you want a 'Normalize'd 'SRational', then use
+-- @'rationalSing' \@('Normalize' r)@.
 instance forall r n d.
   ( Normalize r ~ n % d
-  , I.KnownInteger n
-  , L.KnownNat d
+  , I.KnownInteger (Num_ r)
+  , L.KnownNat (Den_ r)
   ) => KnownRational r where
-  rationalSing = UnsafeSRational
-    (I.fromPrelude (I.integerVal (Proxy @n)) :% N.natVal (Proxy @d))
+  rationalSing =
+    let n = I.fromSInteger' (I.SInteger @(Num_ r))
+        d = N.natVal (Proxy @(Den_ r))
+    in UnsafeSRational (n :% d)
 
 -- | Term-level "KindRational" 'Rational' representation of the type-level
 -- 'Rational' @r@.
@@ -596,6 +602,7 @@
 
 -- | Singleton type for a type-level 'Rational' @r@.
 newtype SRational (r :: Rational) = UnsafeSRational Rational
+type role SRational nominal
 
 -- | A explicitly bidirectional pattern synonym relating an 'SRational' to a
 -- 'KnownRational' constraint.
@@ -632,19 +639,38 @@
   showsPrec p (UnsafeSRational r) = showParen (p > appPrec) $
     showString "SRational @" . showsPrecTypeLit appPrec1 r
 
+-- | Note that this checks for type equality, not arithmetic equality.
+-- That is, @'P' 1 '%' 2@ and @'P' 2 '%' 4@ are not equal types,
+-- even if they are arithmetically equal.
 instance TestEquality SRational where
-  testEquality (UnsafeSRational x) (UnsafeSRational y) = do
-    guard (toPrelude x P.== toPrelude y)
-    pure (unsafeCoerce Refl)
+  testEquality = decideEquality
+  {-# INLINE testEquality #-}
 
+-- | Note that this checks for type equality, not arithmetic equality.
+-- That is, @'P' 1 '%' 2@ and @'P' 2 '%' 4@ are not equal types,
+-- even if they are arithmetically equal.
 instance TestCoercion SRational where
-  testCoercion x y = fmap (\Refl -> Coercion) (testEquality x y)
+  testCoercion = decideCoercion
+  {-# INLINE testCoercion #-}
 
 -- | Return the term-level "Prelude" 'P.Rational' number corresponding
--- to @r@ in a @'SRational' r@ value.
+-- to @r@ in a @'SRational' r@ value. This 'P.Rational' is 'Normalize'd.
 fromSRational :: SRational r -> P.Rational
 fromSRational (UnsafeSRational r) = toPrelude r
 
+-- | Return the term-level "KindRational" 'Rational' number corresponding
+-- to @r@ in a @'SRational' r@ value. This 'Rational' is not 'Normalize'd.
+fromSRational' :: SRational r -> Rational
+fromSRational' (UnsafeSRational r) = r
+
+-- | Whether the internal representation of the 'Rational's are equal.
+--
+-- Note that this is not the same as '(==)'. Use '(==)' unless you
+-- know what you are doing.
+eqRationalRep :: Rational -> Rational -> Bool
+eqRationalRep (ln :% ld) (rn :% rd) = I.eqIntegerRep ln rn && ld P.== rd
+{-# INLINE eqRationalRep #-}
+
 -- | Convert an explicit @'SRational' r@ value into an implicit
 -- @'KnownRational' r@ constraint.
 withKnownRational
@@ -658,6 +684,19 @@
 withSomeSRational r k = k (UnsafeSRational r)
 -- It's very important to keep this NOINLINE! See the docs at "GHC.TypeNats"
 {-# NOINLINE withSomeSRational #-}
+
+--------------------------------------------------------------------------------
+
+type instance Sing = SRational
+
+-- | Note that this checks for type equality, not arithmetic equality.
+-- That is, @'P' 1 '%' 2@ and @'P' 2 '%' 4@ are not equal types,
+-- even if they are arithmetically equal.
+instance SDecide Rational where
+  UnsafeSRational l %~ UnsafeSRational r =
+    case eqRationalRep l r of
+      True  -> Proved (unsafeCoerce Refl)
+      False -> Disproved (\Refl -> error "SDecide.Rational")
 
 --------------------------------------------------------------------------------
 -- Extra stuff that doesn't belong here.
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.Proxy
+import Data.Type.Equality (TestEquality(..))
 import Data.Type.Ord (type (<=), type (<))
 import GHC.Exts (Constraint)
 import System.Exit
@@ -481,6 +482,59 @@
       in readMaybe @P.Rational str
             == fmap (\(K.SomeRational p) -> K.rationalVal p)
                     (readMaybe @K.SomeRational str)
+
+   -- TODO test TestEquality
+
+  , assert "TestEquality +0/1 +0/1" $
+     isJust (testEquality (K.SRational @(P 0 % 1)) (K.SRational @(P 0 % 1)))
+  , assert "TestEquality -0/1 -0/1" $
+     isJust (testEquality (K.SRational @(N 0 % 1)) (K.SRational @(N 0 % 1)))
+  , assert "TestEquality +1/2 +1/2" $
+     isJust (testEquality (K.SRational @(P 1 % 2)) (K.SRational @(P 1 % 2)))
+  , assert "TestEquality -1/2 -1/2" $
+     isJust (testEquality (K.SRational @(N 1 % 2)) (K.SRational @(N 1 % 2)))
+  , assert "TestEquality +0/1 -0/1" $
+     isNothing (testEquality (K.SRational @(P 0 % 1)) (K.SRational @(N 0 % 1)))
+  , assert "TestEquality -0/1 +0/1" $
+     isNothing (testEquality (K.SRational @(N 0 % 1)) (K.SRational @(P 0 % 1)))
+  , assert "TestEquality +0/1 +1/1" $
+     isNothing (testEquality (K.SRational @(P 0 % 1)) (K.SRational @(P 1 % 1)))
+  , assert "TestEquality +0/1 -1/1" $
+     isNothing (testEquality (K.SRational @(P 0 % 1)) (K.SRational @(N 1 % 1)))
+  , assert "TestEquality -0/1 +1/1" $
+     isNothing (testEquality (K.SRational @(N 0 % 1)) (K.SRational @(P 1 % 1)))
+  , assert "TestEquality -0/1 -1/1" $
+     isNothing (testEquality (K.SRational @(N 0 % 1)) (K.SRational @(N 1 % 1)))
+  , assert "TestEquality +1/1 +0/1" $
+     isNothing (testEquality (K.SRational @(P 1 % 1)) (K.SRational @(P 0 % 1)))
+  , assert "TestEquality +1/1 -0/1" $
+     isNothing (testEquality (K.SRational @(P 1 % 1)) (K.SRational @(N 0 % 1)))
+  , assert "TestEquality -1/1 +0/1" $
+     isNothing (testEquality (K.SRational @(N 1 % 1)) (K.SRational @(P 0 % 1)))
+  , assert "TestEquality -1/1 -0/1" $
+     isNothing (testEquality (K.SRational @(N 1 % 1)) (K.SRational @(N 0 % 1)))
+  , assert "TestEquality +1/2 +2/4" $
+     isNothing (testEquality (K.SRational @(P 1 % 2)) (K.SRational @(P 2 % 4)))
+  , assert "TestEquality -1/2 -2/4" $
+     isNothing (testEquality (K.SRational @(N 1 % 2)) (K.SRational @(N 2 % 4)))
+
+  , assert "Show Rational +0" $
+     "0 % 1" == show (K.fromSRational (K.SRational @(P 0 % 1)))
+  , assert "Show Rational -0" $
+     "0 % 1" == show (K.fromSRational (K.SRational @(N 0 % 1)))
+  , assert "Show Rational +1" $
+     "1 % 1" == show (K.fromSRational (K.SRational @(P 1 % 1)))
+  , assert "Show Rational -1" $
+     "(-1) % 1" == show (K.fromSRational (K.SRational @(N 1 % 1)))
+
+  , assert "Show SRational +0" $
+     "SRational @(P 0 % 1)" == show (K.SRational @(P 0 % 1))
+  , assert "Show SRational -0" $
+     "SRational @(N 0 % 1)" == show (K.SRational @(N 0 % 1))
+  , assert "Show SRational +1" $
+     "SRational @(P 1 % 1)" == show (K.SRational @(P 1 % 1))
+  , assert "Show SRational -1" $
+     "SRational @(N 1 % 1)" == show (K.SRational @(N 1 % 1))
 
   ] <> testsDivRem <> testsTerminating