diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,10 @@
 # Changelog for the [`ghc-typelits-natnormalise`](http://hackage.haskell.org/package/ghc-typelits-natnormalise) package
 
+## 0.9.0 *October 17th 2025*
+* Drop `TyConSubst` argument from `normaliseNat`, `normaliseNatEverywhere` and `normaliseSimplifyNat`.
+* Expose `GHC.TypeLits.Normalise.Compat`
+* Report contractions for equations such as `1 + k <= n; n ~ 0` in "solve givens" phase
+
 ## 0.8.1 *October 1st 2025*
 * Fixes [#85](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/85) Deriving equalities from inequalities produces a misleading error message
 * Fixes [#94](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/94) Normalization fails when adding an equality constraint with substraction
diff --git a/ghc-typelits-natnormalise.cabal b/ghc-typelits-natnormalise.cabal
--- a/ghc-typelits-natnormalise.cabal
+++ b/ghc-typelits-natnormalise.cabal
@@ -1,6 +1,6 @@
 cabal-version:       3.0
 name:                ghc-typelits-natnormalise
-version:             0.8.1
+version:             0.9.0
 synopsis:            GHC typechecker plugin for types of kind GHC.TypeLits.Nat
 description:
   A type checker plugin for GHC that can solve /equalities/ and /inequalities/
@@ -64,9 +64,9 @@
 
 library
   exposed-modules:     GHC.TypeLits.Normalise,
+                       GHC.TypeLits.Normalise.Compat,
                        GHC.TypeLits.Normalise.SOP,
                        GHC.TypeLits.Normalise.Unify
-  other-modules:       GHC.TypeLits.Normalise.Compat
   build-depends:       base                >=4.9   && <5,
                        containers          >=0.5.7.1 && <0.8,
                        ghc                 >=8.8.1 && <9.15,
diff --git a/src/GHC/TypeLits/Normalise.hs b/src/GHC/TypeLits/Normalise.hs
--- a/src/GHC/TypeLits/Normalise.hs
+++ b/src/GHC/TypeLits/Normalise.hs
@@ -283,7 +283,7 @@
    do
     let
       givensTyConSubst = mkTyConSubst givens
-    (redGivens, _) <- reduceGivens False opts tcs givensTyConSubst givens
+    (redGivens, _) <- reduceGivens False opts tcs givens
 
     tcPluginTrace "decideEqualSOP Givens {" $
       vcat [ text "givens:" <+> ppr givens ]
@@ -318,10 +318,10 @@
                         . ctEvidence )
                  wanteds
 
-    (redGivens, negWanteds) <- reduceGivens True opts tcs givensTyConSubst givens
+    (redGivens, negWanteds) <- reduceGivens True opts tcs givens
     reducible_wanteds
       <- catMaybes <$> mapM (\ct -> fmap (ct,) <$>
-                                    reduceNatConstr givensTyConSubst redGivens ct)
+                                    reduceNatConstr redGivens ct)
                             nonEqs
 
     tcPluginTrace "decideEqualSOP Wanteds {" $
@@ -378,14 +378,14 @@
 type NatInEquality = (Ct,(CoreSOP,CoreSOP,Bool))
 
 reduceGivens :: Bool -- ^ allow generating new "non-negative" Wanteds
-             -> Opts -> LookedUpTyCons -> TyConSubst
+             -> Opts -> LookedUpTyCons
              -> [Ct]
              -> TcPluginM Solve ([Ct], Map CType CtLoc)
-reduceGivens gen_wanteds opts tcs givensTyConSubst origGivens = go [] Map.empty origGivens
+reduceGivens gen_wanteds opts tcs origGivens = go [] Map.empty origGivens
   where
     go rev_acc_gs acc_ws [] = return ( reverse rev_acc_gs, acc_ws )
     go rev_acc_gs acc_ws (g:gs) =
-      case tryReduceGiven opts tcs givensTyConSubst origGivens g of
+      case tryReduceGiven opts tcs origGivens g of
         Just ( pred', evExpr, ws )
           | gen_wanteds || null ws || negNumbers opts
           -> do
@@ -402,12 +402,11 @@
 
 tryReduceGiven
   :: Opts -> LookedUpTyCons
-  -> TyConSubst
   -> [Ct] -> Ct
   -> Maybe (PredType, EvTerm, [PredType])
-tryReduceGiven opts tcs givensTyConSubst simplGivens ct = do
+tryReduceGiven opts tcs simplGivens ct = do
     let (mans, ws) =
-          runWriter $ normaliseNatEverywhere givensTyConSubst $
+          runWriter $ normaliseNatEverywhere $
           ctEvPred $ ctEvidence ct
         ws' = [ p
               | p <- subToPred opts tcs ws
@@ -425,10 +424,10 @@
 fromNatEquality (Left  (ct, _, _)) = ct
 fromNatEquality (Right (ct, _))    = ct
 
-reduceNatConstr :: TyConSubst -> [Ct] -> Ct -> TcPluginM Solve (Maybe (EvTerm, [(Type, Type)], [Ct]))
-reduceNatConstr givensTyConSubst givens ct = do
+reduceNatConstr :: [Ct] -> Ct -> TcPluginM Solve (Maybe (EvTerm, [(Type, Type)], [Ct]))
+reduceNatConstr givens ct = do
   let pred0 = ctEvPred $ ctEvidence ct
-      (mans, tests) = runWriter $ normaliseNatEverywhere givensTyConSubst pred0
+      (mans, tests) = runWriter $ normaliseNatEverywhere pred0
 
       -- Even if we didn't rewrite the Wanted,
       -- we may still be able to solve it from a (rewritten) Given.
@@ -666,8 +665,8 @@
 toNatEquality tcs givensTyConSubst ct0
   | Just (((x,y), mbLTE), cos0) <- isNatRel tcs givensTyConSubst pred0
   , let
-      ((x', cos1),k1) = runWriter (normaliseNat givensTyConSubst x)
-      ((y', cos2),k2) = runWriter (normaliseNat givensTyConSubst y)
+      ((x', cos1),k1) = runWriter (normaliseNat x)
+      ((y', cos2),k2) = runWriter (normaliseNat y)
       ks      = k1 ++ k2
   = case mbLTE of
       Nothing ->
@@ -685,7 +684,7 @@
         -- See https://github.com/clash-lang/ghc-typelits-natnormalise/issues/94.
         | isGiven (ctEvidence ct0)
         , className kn == knownNatClassName
-        , let ((x', cos0), ks) = runWriter (normaliseNat givensTyConSubst x)
+        , let ((x', cos0), ks) = runWriter (normaliseNat x)
         -> [(Right (ct0, (S [], x', True)), ks, cos0)]
       _ -> []
   where
@@ -716,8 +715,8 @@
     rewrite x y
       | isNatKind (typeKind x)
       , isNatKind (typeKind y)
-      , let ((x', cos1),k1) = runWriter (normaliseNat givensTyConSubst x)
-      , let ((y', cos2),k2) = runWriter (normaliseNat givensTyConSubst y)
+      , let ((x', cos1),k1) = runWriter (normaliseNat x)
+      , let ((y', cos2),k2) = runWriter (normaliseNat y)
       = [(Left (ct0,x',y'),k1 ++ k2, cos1 ++ cos2)]
       | otherwise
       = []
diff --git a/src/GHC/TypeLits/Normalise/SOP.hs b/src/GHC/TypeLits/Normalise/SOP.hs
--- a/src/GHC/TypeLits/Normalise/SOP.hs
+++ b/src/GHC/TypeLits/Normalise/SOP.hs
@@ -128,7 +128,8 @@
   (S ps1) == (S ps2)      = ps1 == ps2
 
 instance (Outputable v, Outputable c) => Outputable (SOP v c) where
-  ppr = hcat . punctuate (text " + ") . map ppr . unS
+  ppr (S []) = integer 0
+  ppr (S s) = hcat . punctuate (text " + ") . map ppr $ s
 
 instance (Outputable v, Outputable c) => Outputable (Product v c) where
   ppr = hcat . punctuate (text " * ") . map ppr . unP
diff --git a/src/GHC/TypeLits/Normalise/Unify.hs b/src/GHC/TypeLits/Normalise/Unify.hs
--- a/src/GHC/TypeLits/Normalise/Unify.hs
+++ b/src/GHC/TypeLits/Normalise/Unify.hs
@@ -79,8 +79,6 @@
 
 -- ghc-tcplugin-api
 import GHC.TcPlugin.API
-import GHC.TcPlugin.API.TyConSubst
-  ( TyConSubst )
 import GHC.Utils.Outputable
 
 
@@ -113,8 +111,8 @@
 -- * literals
 -- * type variables
 -- * Applications of the arithmetic operators @(+,-,*,^)@
-normaliseNat :: TyConSubst -> Type -> Writer [(Type,Type)] (CoreSOP, [Coercion])
-normaliseNat givensTyConSubst ty
+normaliseNat :: Type -> Writer [(Type,Type)] (CoreSOP, [Coercion])
+normaliseNat ty
   | Just (tc, xs) <- splitTyConApp_maybe ty
   = goTyConApp tc xs
   | Just i <- isNumLitTy ty
@@ -127,21 +125,21 @@
       goTyConApp :: TyCon -> [Type] -> Writer [(Type,Type)] (CoreSOP, [Coercion])
       goTyConApp tc [x,y]
         | tc == typeNatAddTyCon =
-            do (x', cos1) <- normaliseNat givensTyConSubst x
-               (y', cos2) <- normaliseNat givensTyConSubst y
+            do (x', cos1) <- normaliseNat x
+               (y', cos2) <- normaliseNat y
                return (mergeSOPAdd x' y', cos1 ++ cos2)
         | tc == typeNatSubTyCon = do
-          (x', cos1) <- normaliseNat givensTyConSubst x
-          (y', cos2) <- normaliseNat givensTyConSubst y
+          (x', cos1) <- normaliseNat x
+          (y', cos2) <- normaliseNat y
           tell [(reifySOP $ simplifySOP x', reifySOP $ simplifySOP y')]
           return (mergeSOPAdd x' (mergeSOPMul (S [P [I (-1)]]) y'), cos1 ++ cos2)
         | tc == typeNatMulTyCon =
-          do (x', cos1) <- normaliseNat givensTyConSubst x
-             (y', cos2) <- normaliseNat givensTyConSubst y
+          do (x', cos1) <- normaliseNat x
+             (y', cos2) <- normaliseNat y
              return (mergeSOPMul x' y', cos1 ++ cos2)
         | tc == typeNatExpTyCon =
-          do (x', cos1) <- normaliseNat givensTyConSubst x
-             (y', cos2) <- normaliseNat givensTyConSubst y
+          do (x', cos1) <- normaliseNat x
+             (y', cos2) <- normaliseNat y
              return (normaliseExp x' y', cos1 ++ cos2)
       goTyConApp tc xs
         = return (S [P [C (CType $ mkTyConApp tc xs)]], [])
@@ -164,8 +162,8 @@
 -- | Applies 'normaliseNat' and 'simplifySOP' to type or predicates to reduce
 -- any occurrences of sub-terms of /kind/ 'GHC.TypeLits.Nat'. If the result is
 -- the same as input, returns @'Nothing'@.
-normaliseNatEverywhere :: TyConSubst -> Type -> Writer [(Type, Type)] (Maybe (Type, [Coercion]))
-normaliseNatEverywhere givensTyConSubst ty0
+normaliseNatEverywhere :: Type -> Writer [(Type, Type)] (Maybe (Type, [Coercion]))
+normaliseNatEverywhere ty0
   | Just (tc, fields) <- splitTyConApp_maybe ty0
   =   if tc `elem` knownTyCons
       then do
@@ -174,7 +172,7 @@
         ty1M <- maybeRunWriter (go tc fields)
         let (ty1, cos1) = fromMaybe (ty0, []) ty1M
         -- Normalize (subterm-normalized) type given to 'normaliseNatEverywhere'
-        (ty2, cos2) <- normaliseSimplifyNat givensTyConSubst ty1
+        (ty2, cos2) <- normaliseSimplifyNat ty1
         -- TODO: 'normaliseNat' could keep track whether it changed anything. That's
         -- TODO: probably cheaper than checking for equality here.
         pure $
@@ -205,12 +203,12 @@
       , Just (tc', flds') <- splitTyConApp_maybe ty'
       = go tc' flds'
       | otherwise
-      = normaliseNatEverywhere givensTyConSubst ty'
+      = normaliseNatEverywhere ty'
 
-normaliseSimplifyNat :: TyConSubst -> Type -> Writer [(Type, Type)] (Type, [Coercion])
-normaliseSimplifyNat givensTyConSubst ty
+normaliseSimplifyNat :: Type -> Writer [(Type, Type)] (Type, [Coercion])
+normaliseSimplifyNat ty
   | typeKind ty `eqType` natKind = do
-      (ty', cos1) <- normaliseNat givensTyConSubst ty
+      (ty', cos1) <- normaliseNat ty
       return $ (reifySOP $ simplifySOP ty', cos1)
   | otherwise = return (ty, [])
 
@@ -790,7 +788,7 @@
   = any canBeZero bs
   | otherwise
   = True
-canBeZero (V {}) = True -- e.g. 'tau' where 'tau' is an unfilled metavariable
+canBeZero (V v) = isMetaTyVar v -- e.g. 'tau' where 'tau' is an unfilled metavariable
 
 -- | Try to solve inequalities
 solveIneq