diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,12 @@
 # Changelog for the [`ghc-typelits-natnormalise`](http://hackage.haskell.org/package/ghc-typelits-natnormalise) package
 
+## 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
+* Fixes [#96](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/96) Unification fails when variables occur on both LHS and RHS
+* Fixes [#99](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/99) ghc-typelits-natnormalise erroneously unifies under type families
+* Fixes [100](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/100) stack space overflow with ghc-typelits-natnormalize 0.8
+
 ## 0.8 *September 8th 2025*
 * Uses https://hackage.haskell.org/package/ghc-tcplugin-api to make supporting new GHC versions easier
 * Support for GHC versions older than 8.8 is dropped
diff --git a/ghc-typelits-natnormalise.cabal b/ghc-typelits-natnormalise.cabal
--- a/ghc-typelits-natnormalise.cabal
+++ b/ghc-typelits-natnormalise.cabal
@@ -1,40 +1,40 @@
 cabal-version:       3.0
 name:                ghc-typelits-natnormalise
-version:             0.8.0
+version:             0.8.1
 synopsis:            GHC typechecker plugin for types of kind GHC.TypeLits.Nat
 description:
   A type checker plugin for GHC that can solve /equalities/ and /inequalities/
   of types of kind @Nat@, where these types are either:
-  .
+
   * Type-level naturals
-  .
+
   * Type variables
-  .
+
   * Applications of the arithmetic expressions @(+,-,*,^)@.
-  .
+
   It solves these equalities by normalising them to /sort-of/ @SOP@
   (Sum-of-Products) form, and then perform a simple syntactic equality.
-  .
+
   For example, this solver can prove the equality between:
-  .
+
   @
   (x + 2)^(y + 2)
   @
-  .
+
   and
-  .
+
   @
   4*x*(2 + x)^y + 4*(2 + x)^y + (2 + x)^y*x^2
   @
-  .
+
   Because the latter is actually the @SOP@ normal form of the former.
-  .
+
   To use the plugin, add the
-  .
+
   @
   OPTIONS_GHC -fplugin GHC.TypeLits.Normalise
   @
-  .
+
   Pragma to the header of your file.
 homepage:            http://www.clash-lang.org/
 bug-reports:         http://github.com/clash-lang/ghc-typelits-natnormalise/issues
@@ -70,7 +70,7 @@
   build-depends:       base                >=4.9   && <5,
                        containers          >=0.5.7.1 && <0.8,
                        ghc                 >=8.8.1 && <9.15,
-                       ghc-tcplugin-api    >=0.17.0 && <0.18,
+                       ghc-tcplugin-api    >=0.18.0 && <0.19,
                        transformers        >=0.5.2.0 && < 0.7
   if impl(ghc >= 9.0.0)
     build-depends:     ghc-bignum >=1.0 && <1.5
@@ -83,6 +83,7 @@
         , TyCon      as GHC.Core.TyCon
         , TysWiredIn as GHC.Builtin.Types
         , Unique     as GHC.Types.Unique
+        , Util       as GHC.Utils.Misc
         )
 
   hs-source-dirs:      src
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
@@ -143,6 +143,7 @@
 where /n-l/ is a negative number.
 -}
 
+{-# LANGUAGE BangPatterns          #-}
 {-# LANGUAGE DataKinds             #-}
 {-# LANGUAGE ExplicitNamespaces    #-}
 {-# LANGUAGE FlexibleContexts      #-}
@@ -169,9 +170,9 @@
   ( WriterT(runWriterT), runWriter )
 import Data.Either
   ( rights, partitionEithers )
+import Data.Foldable
 import Data.List
-  ( stripPrefix, find, partition )
-import qualified Data.List.NonEmpty as NE
+  ( stripPrefix, partition )
 import Data.Maybe
   ( mapMaybe, catMaybes, fromMaybe )
 import Data.Traversable
@@ -184,21 +185,28 @@
   ( Set )
 import qualified Data.Set as Set
   ( elems, empty )
+import Data.Map.Strict
+  ( Map )
+import qualified Data.Map.Strict as Map
+  ( empty, insertWith, traverseWithKey )
 
 -- ghc
 import GHC.Builtin.Names
   ( knownNatClassName )
 import GHC.Builtin.Types.Literals
   ( typeNatAddTyCon, typeNatExpTyCon, typeNatMulTyCon, typeNatSubTyCon )
+import GHC.Core.TyCon
+  ( Injectivity (..), tyConInjectivityInfo, tyConArity )
+import GHC.Utils.Misc
+  ( filterByList )
 
 -- ghc-tcplugin-api
 import GHC.TcPlugin.API
 import GHC.TcPlugin.API.TyConSubst
-  ( TyConSubst, mkTyConSubst, splitTyConApp_upTo )
+  ( TyConSubst, mkTyConSubst )
 import GHC.Plugins
   ( Plugin(..), defaultPlugin, purePlugin )
 import GHC.Utils.Outputable
-  ( ($$), (<+>), text, vcat )
 
 -- ghc-typelits-natnormalise
 import GHC.TypeLits.Normalise.Compat
@@ -273,30 +281,26 @@
 -- @Unbox (1 + n)@!
 decideEqualSOP opts (ExtraDefs { tyCons = tcs }) givens [] =
    do
-    let givensTyConSubst = mkTyConSubst givens
-        reds =
-          filter
-            (\(_,(_,_,v)) -> null v || negNumbers opts) $
-              reduceGivens opts tcs (mkTyConSubst givens) givens
+    let
+      givensTyConSubst = mkTyConSubst givens
+    (redGivens, _) <- reduceGivens False opts tcs givensTyConSubst givens
 
     tcPluginTrace "decideEqualSOP Givens {" $
       vcat [ text "givens:" <+> ppr givens ]
 
-    newGivens <- for reds $ \(origCt, (pred', evTerm, _)) ->
-      mkNonCanonical <$> newGiven (ctLoc origCt) pred' evTerm
     -- Try to find contradictory Givens, to improve pattern match warnings.
-    sr <- simplifyNats opts tcs [] $ concatMap (toNatEquality tcs givensTyConSubst) (givens ++ newGivens)
-    case sr of
-      Impossible eq -> do
-        let contra = fromNatEquality eq
-        tcPluginTrace "decideEqualSOP Givens (FAIL) }" $
-          vcat [ text "givens:" <+> ppr givens
-               , text "contra:" <+> ppr contra  ]
-        return $ TcPluginContradiction [contra]
-      Simplified {} -> do
-        tcPluginTrace "decideEqualSOP Givens (OK) }" $
-          vcat [ text "givens:" <+> ppr givens ]
-        return $ TcPluginOk [] []
+    SimplifyResult _simpls contras <-
+      simplifyNats opts tcs [] $
+        concatMap (toNatEquality tcs givensTyConSubst) redGivens
+    tcPluginTrace "decideEqualSOP Givens }" $
+      vcat [ text "givens:" <+> ppr givens
+           , text "simpls:" <+> ppr _simpls
+           , text "contra:" <+> ppr contras ]
+    return $
+      mkTcPluginSolveResult
+        ( map fromNatEquality contras )
+        [] -- no solved Givens
+        [] -- no new Givens
 
 -- Solving phase.
 -- Solves in/equalities on Nats and simplifiable constraints
@@ -313,18 +317,16 @@
                         . ctEvPred
                         . ctEvidence )
                  wanteds
-    let newRedGs = reduceGivens opts tcs givensTyConSubst givens
-    redGivens <- for newRedGs $ \(origCt, (pred', evExpr, _)) ->
-      mkNonCanonical <$> newGiven (ctLoc origCt) pred' evExpr
+
+    (redGivens, negWanteds) <- reduceGivens True opts tcs givensTyConSubst givens
     reducible_wanteds
       <- catMaybes <$> mapM (\ct -> fmap (ct,) <$>
-                                    reduceNatConstr givensTyConSubst (givens ++ redGivens) ct)
+                                    reduceNatConstr givensTyConSubst redGivens ct)
                             nonEqs
 
     tcPluginTrace "decideEqualSOP Wanteds {" $
        vcat [ text "givens:" <+> ppr givens
             , text "new reduced givens:" <+> ppr redGivens
-            , text "newRedGs:" <+> ppr newRedGs
             , text $ replicate 80 '-'
             , text "wanteds:" <+> ppr wanteds
             , text "unit_wanteds:" <+> ppr unit_wanteds0
@@ -337,61 +339,67 @@
         -- subterms, we have to make sure appropriate inequalities to hold.
         -- Here, we generate such additional inequalities for reduction
         -- that is to be added to new [W]anteds.
-        ineqForRedWants <- fmap concat $ for newRedGs $ \(ct, (_,_, ws)) -> for ws $
-          fmap mkNonCanonical . newWanted (ctLoc ct)
-        let unit_givens = concatMap (toNatEquality tcs givensTyConSubst) givens
+        let mkNegWanted ( CType wtdPred ) loc = mkNonCanonical <$> newWanted loc wtdPred
+        ineqForRedWants <- Map.traverseWithKey mkNegWanted negWanteds
+        let unit_givens = concatMap (toNatEquality tcs givensTyConSubst) redGivens
             unit_wanteds = unit_wanteds0 ++ concatMap (toNatEquality tcs givensTyConSubst) ineqForRedWants
-        sr <- simplifyNats opts tcs unit_givens unit_wanteds
+        sr@(SimplifyResult evs contras) <- simplifyNats opts tcs unit_givens unit_wanteds
         tcPluginTrace "normalised" (ppr sr)
         reds <- for reducible_wanteds $ \(origCt,(term, ws, wDicts)) -> do
           wants <- evSubtPreds (ctLoc origCt) $ subToPred opts tcs ws
           return ((term, origCt), wDicts ++ wants)
-        case sr of
-          Simplified evs -> do
-            let simpld = filter (not . isGiven . ctEvidence . (\((_,x),_) -> x)) evs
-                -- Only solve a Derived when there are Wanteds in play
-                simpld1 = case filter (isWanted . ctEvidence . (\((_,x),_) -> x)) evs ++ reds of
-                            [] -> []
-                            _  -> simpld
-                (solved,newWanteds) = second concat (unzip $ simpld1 ++ reds)
-
-            tcPluginTrace "decideEqualSOP Wanteds }" $
-               vcat [ text "givens:" <+> ppr givens
-                    , text "new reduced givens:" <+> ppr redGivens
-                    , text "newRedGs:" <+> ppr newRedGs
-                    , text $ replicate 80 '-'
-                    , text "wanteds:" <+> ppr wanteds
-                    , text "ineqForRedWants:" <+> ppr ineqForRedWants
-                    , text "unit_wanteds0:" <+> ppr (map (toNatEquality tcs givensTyConSubst) wanteds)
-                    , text "unit_wanteds:" <+> ppr unit_wanteds
-                    , text "reducible_wanteds:" <+> ppr reducible_wanteds
-                    , text $ replicate 80 '='
-                    , text "solved:" <+> ppr solved
-                    , text "newWanteds:" <+> ppr newWanteds
-                    ]
+        let simpld = filter (not . isGiven . ctEvidence . (\((_,x),_) -> x)) evs
+            -- Only solve a Derived when there are Wanteds in play
+            simpld1 = case filter (isWanted . ctEvidence . (\((_,x),_) -> x)) evs ++ reds of
+                        [] -> []
+                        _  -> simpld
+            (solved,newWanteds) = second concat (unzip $ simpld1 ++ reds)
 
-            return (TcPluginOk solved $ newWanteds)
-          Impossible eq -> return (TcPluginContradiction [fromNatEquality eq])
+        tcPluginTrace "decideEqualSOP Wanteds }" $
+           vcat [ text "givens:" <+> ppr givens
+                , text "new reduced givens:" <+> ppr redGivens
+                , text "unit givens:" <+> ppr unit_givens
+                , text $ replicate 80 '-'
+                , text "wanteds:" <+> ppr wanteds
+                , text "ineqForRedWants:" <+> ppr ineqForRedWants
+                , text "unit_wanteds:" <+> ppr unit_wanteds
+                , text "reducible_wanteds:" <+> ppr reducible_wanteds
+                , text $ replicate 80 '='
+                , text "solved:" <+> ppr solved
+                , text "newWanteds:" <+> ppr newWanteds
+                ]
+        return $
+          mkTcPluginSolveResult
+            (map fromNatEquality contras)
+            solved
+            newWanteds
 
 type NatEquality   = (Ct,CoreSOP,CoreSOP)
 type NatInEquality = (Ct,(CoreSOP,CoreSOP,Bool))
 
-reduceGivens :: Opts -> LookedUpTyCons
-             -> TyConSubst
-             -> [Ct] -> [(Ct, (Type, EvTerm, [PredType]))]
-reduceGivens opts tcs givensTyConSubst givens =
-  let nonEqs =
-        [ ct
-        | ct <- givens
-        , let ev = ctEvidence ct
-              prd = ctEvPred ev
-        , isGiven ev
-        , not $ (\p -> isEqPred p || isEqClassPred p ) prd
-        ]
-  in mapMaybe
-      (\ct -> (ct,) <$> tryReduceGiven opts tcs givensTyConSubst givens ct)
-      nonEqs
+reduceGivens :: Bool -- ^ allow generating new "non-negative" Wanteds
+             -> Opts -> LookedUpTyCons -> TyConSubst
+             -> [Ct]
+             -> TcPluginM Solve ([Ct], Map CType CtLoc)
+reduceGivens gen_wanteds opts tcs givensTyConSubst 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
+        Just ( pred', evExpr, ws )
+          | gen_wanteds || null ws || negNumbers opts
+          -> do
+            let loc = ctLoc g
+            g' <- mkNonCanonical <$> newGiven loc pred' evExpr
+            let !acc' = foldl' (insertWanted loc) acc_ws ws
+            go ( g' : rev_acc_gs ) acc' gs
+        _ ->
+          go ( g : rev_acc_gs ) acc_ws gs
 
+    insertWanted :: CtLoc -> Map CType CtLoc -> Type -> Map CType CtLoc
+    insertWanted loc acc w =
+      Map.insertWith (\ _new old -> old) (CType w) loc acc
+
 tryReduceGiven
   :: Opts -> LookedUpTyCons
   -> TyConSubst
@@ -403,11 +411,15 @@
           ctEvPred $ ctEvidence ct
         ws' = [ p
               | p <- subToPred opts tcs ws
-              , all (not . (`eqType` p). ctEvPred . ctEvidence) simplGivens
+              , all (not . (`eqType` p) . ctEvPred . ctEvidence) simplGivens
               ]
         -- deps = unitDVarSet (ctEvId ct)
     (pred', deps) <- mans
-    return (pred', toReducedDict (ctEvidence ct) pred' deps, ws')
+    case classifyPredType pred' of
+      EqPred _ l r
+        | l `eqType` r
+        -> Nothing
+      _ -> return (pred', toReducedDict (ctEvidence ct) pred' deps, ws')
 
 fromNatEquality :: Either NatEquality NatInEquality -> Ct
 fromNatEquality (Left  (ct, _, _)) = ct
@@ -458,12 +470,15 @@
   in EvExpr ev
 
 data SimplifyResult
-  = Simplified [((EvTerm,Ct),[Ct])]
-  | Impossible (Either NatEquality NatInEquality)
+  = SimplifyResult
+     { simplified :: [((EvTerm,Ct),[Ct])]
+     , impossible :: [Either NatEquality NatInEquality]
+     }
 
 instance Outputable SimplifyResult where
-  ppr (Simplified evs) = text "Simplified" $$ ppr evs
-  ppr (Impossible eq)  = text "Impossible" <+> ppr eq
+  ppr (SimplifyResult { simplified, impossible }) =
+    text "SimplifyResult { simplified =" <+> ppr simplified
+                <+> text ", impossible =" <+> ppr impossible <+> text "}"
 
 type NatCt = (Either NatEquality NatInEquality, [(Type,Type)], [Coercion])
 
@@ -494,7 +509,7 @@
           tcPluginTrace "simplifyNats" (ppr eqs)
           simples [] [] [] [] [] eqs
 
-        pure (foldr findFirstSimpliedWanted (Simplified []) allSimplified)
+        pure (foldr findFirstSimpliedWanted (SimplifyResult [] []) allSimplified)
   where
     simples :: [Coercion]
             -> [CoreUnify]
@@ -503,7 +518,7 @@
             -> [NatCt]
             -> [NatCt]
             -> TcPluginM Solve SimplifyResult
-    simples _ _subst evs _leqsG _xs [] = return (Simplified evs)
+    simples _ _subst evs _leqsG _xs [] = return (SimplifyResult evs [])
     simples deps subst evs leqsG xs (eq@(lr@(Left (ct,u,v)),k,deps2):eqs') = do
       let u' = substsSOP subst u
           v' = substsSOP subst v
@@ -512,10 +527,14 @@
       case ur of
         Win -> do
           evs' <- maybe evs (:evs) <$> evMagic tcs ct (deps ++ deps2) Set.empty (subToPred opts tcs k)
+          tcPluginTrace "unifyNats Win" $
+            vcat [ text "evs:" <+> ppr evs
+                 , text "evs':" <+> ppr evs'
+                 , text "ct:" <+> ppr ct
+                 ]
           simples deps subst evs' leqsG [] (xs ++ eqs')
-        Lose -> if null evs && null eqs'
-                   then return (Impossible lr)
-                   else simples deps subst evs leqsG xs eqs'
+        Lose ->
+          addContra lr <$> simples deps subst evs leqsG xs eqs'
         Draw [] -> simples deps subst evs [] (eq:xs) eqs'
         Draw subst' -> do
           evM <- evMagic tcs ct deps Set.empty (map unifyItemToPredType subst' ++
@@ -552,7 +571,8 @@
           evs' <- maybe evs (:evs) <$> evMagic tcs ct deps knW (subToPred opts tcs k)
           simples deps subst evs' leqsG' xs eqs'
 
-        Just (False,_) | null k -> return (Impossible lr)
+        Just (False,_) | null k ->
+          addContra lr <$> simples deps subst evs leqsG xs eqs'
         _ -> do
           let solvedIneq = mapMaybe runWriterT
                  -- it is an inequality that can be instantly solved, such as
@@ -621,13 +641,16 @@
       (Left (ct,S [P [V v2]], S [P [V v1]]), ps, deps)
     swapVar _ = error "internal error"
 
-    findFirstSimpliedWanted (Impossible e)   _  = Impossible e
-    findFirstSimpliedWanted (Simplified evs) s2
-      | any (isWanted . ctEvidence . snd . fst) evs
-      = Simplified evs
+    findFirstSimpliedWanted s1@(SimplifyResult evs imposs) s2
+      |  not (null imposs)
+      || any (isWanted . ctEvidence . snd . fst) evs
+      = s1
       | otherwise
       = s2
 
+addContra :: Either NatEquality NatInEquality -> SimplifyResult -> SimplifyResult
+addContra contra sr = sr { impossible = contra : impossible sr }
+
 -- If we allow negated numbers we simply do not emit the inequalities
 -- derived from the subtractions that are converted to additions with a
 -- negated operand
@@ -657,6 +680,13 @@
   = case classifyPredType pred0 of
       EqPred NomEq t1 t2
         -> goNomEq t1 t2
+      ClassPred kn [x]
+        -- From [G] KnownNat blah, also produce [G] 0 <= blah
+        -- 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)
+        -> [(Right (ct0, (S [], x', True)), ks, cos0)]
       _ -> []
   where
     pred0 = ctPred ct0
@@ -665,16 +695,20 @@
     goNomEq lhs rhs
       -- Recur into a TyCon application for TyCons that we **do not** rewrite,
       -- e.g. peek inside the Maybe in 'Maybe (x + y) ~ Maybe (y + x)'.
-      | Just tcApps1 <- splitTyConApp_upTo givensTyConSubst lhs
-      , Just tcApps2 <- splitTyConApp_upTo givensTyConSubst rhs
-      , let tcAppsMap1 = listToUniqMap $ map (\ (tc, tys, deps) -> (tc, (tys, deps))) $ NE.toList tcApps1
-            tcAppsMap2 = listToUniqMap $ map (\ (tc, tys, deps) -> (tc, (tys, deps))) $ NE.toList tcApps2
-            tcAppPairs = intersectUniqMap_C (,) tcAppsMap1 tcAppsMap2
-      , (tc, ((xs, cos1), (ys, cos2))):_ <- nonDetUniqMapToList tcAppPairs
+      | Just (tc , xs) <- splitTyConApp_maybe lhs
+      , Just (tc', ys) <- splitTyConApp_maybe rhs
+      , tc == tc'
       , not $ tc `elem` [typeNatAddTyCon, typeNatSubTyCon, typeNatMulTyCon, typeNatExpTyCon]
-      , let subs = filter (not . uncurry eqType) (zip xs ys)
-      = (\ (eq, ws, deps) -> (eq, ws, cos1 ++ cos2 ++ deps)) <$>
-          concatMap (uncurry rewrite) subs
+      , let xys = zip xs ys
+      -- Make sure not to recur into non-injective positions of type families,
+      -- e.g. if we know 'F n ~ F m' that doesn't mean 'n ~ m'.
+            subs  =
+              filter (not . uncurry eqType) $
+                case tyConInjectivityInfo tc of
+                  Injective inj ->
+                    filterByList (inj ++ repeat True) xys
+                  _ -> drop (tyConArity tc) xys
+      = concatMap (uncurry rewrite) subs
       | otherwise
       = rewrite lhs rhs
 
diff --git a/src/GHC/TypeLits/Normalise/Compat.hs b/src/GHC/TypeLits/Normalise/Compat.hs
--- a/src/GHC/TypeLits/Normalise/Compat.hs
+++ b/src/GHC/TypeLits/Normalise/Compat.hs
@@ -23,6 +23,8 @@
 
   , UniqMap, intersectUniqMap_C, listToUniqMap, nonDetUniqMapToList
 
+  , mkTcPluginSolveResult
+
   ) where
 
 -- base
@@ -242,6 +244,9 @@
 isNatRel tcs givensTyConSubst ty0
   | EqPred NomEq x y <- classifyPredType ty0
   = if
+      -- (expr1 :: Nat) ~ (expr2 :: Nat)
+      | all ( ( `eqType` natKind ) . typeKind ) [ x, y ]
+      -> Just $ ( ( ( x, y ), Nothing ), [] )
       -- (b :: Bool) ~ y
       | Just ( b, cos1 ) <- boolean_maybe givensTyConSubst x
       -> second ( ++ cos1 ) <$> booleanRel b y
@@ -360,6 +365,7 @@
     maybe [] NE.toList $ splitTyConApp_upTo givensTyConSubst ty
 
 --------------------------------------------------------------------------------
+
 #if !MIN_VERSION_ghc(9,7,0)
 
 newtype UniqMap k a = UniqMap ( UniqFM k (k, a) )
@@ -379,3 +385,22 @@
 {-# INLINE nonDetUniqMapToList #-}
 
 #endif
+
+--------------------------------------------------------------------------------
+
+mkTcPluginSolveResult :: [Ct] -> [(EvTerm, Ct)] -> [Ct]
+                      -> TcPluginSolveResult
+#if MIN_VERSION_ghc(9,3,0)
+mkTcPluginSolveResult = TcPluginSolveResult
+#else
+mkTcPluginSolveResult contras solved new =
+  -- On GHC 9.2 and below, it's not possible to return
+  -- both contradictions and solved/new constraints.
+  --
+  -- In general, we prefer returning solved constraints over contradictions.
+  if null solved && not (null contras)
+  then TcPluginContradiction contras
+  else TcPluginOk solved new
+#endif
+
+--------------------------------------------------------------------------------
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
@@ -11,7 +11,6 @@
 {-# LANGUAGE RecordWildCards            #-}
 {-# LANGUAGE TupleSections              #-}
 
-
 {-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-}
 
 module GHC.TypeLits.Normalise.Unify
@@ -39,6 +38,7 @@
   , ineqToSubst
   , instantSolveIneq
   , solvedInEqSmallestConstraint
+  , negateProd
     -- * Properties
   , isNatural
   )
@@ -47,19 +47,14 @@
 -- base
 import Control.Arrow
   ( first, second )
-import Control.Monad.Trans.Writer.Strict
-  ( Writer, WriterT(..), runWriter, tell )
-import Data.Foldable
-  ( asum )
-import Data.Function
-  ( on )
+import Control.Monad
+  ( guard, zipWithM )
+import Data.Either
+  ( partitionEithers )
 import Data.List
   ( (\\), intersect, nub )
-import qualified Data.List.NonEmpty as NE
 import Data.Maybe
   ( fromMaybe, mapMaybe, isJust )
-import Data.Traversable
-  ( for )
 import GHC.Base
   ( (==#), isTrue# )
 import GHC.Integer
@@ -79,17 +74,23 @@
 import GHC.Types.Unique.Set
   ( UniqSet
   , emptyUniqSet, unionManyUniqSets, unionUniqSets, unitUniqSet
+  , nonDetEltsUniqSet, elementOfUniqSet
   )
-import GHC.Utils.Outputable
-  ( ($$), (<+>), text )
 
 -- ghc-tcplugin-api
 import GHC.TcPlugin.API
-import GHC.TcPlugin.API.TyConSubst (TyConSubst, splitTyConApp_upTo)
+import GHC.TcPlugin.API.TyConSubst
+  ( TyConSubst )
+import GHC.Utils.Outputable
 
+
 -- ghc-typelits-natnormalise
 import GHC.TypeLits.Normalise.SOP
 
+-- transformers
+import Control.Monad.Trans.Writer.Strict
+  ( Writer, WriterT(..), runWriter, tell )
+
 --------------------------------------------------------------------------------
 
 newtype CType = CType { unCType :: Type }
@@ -114,9 +115,8 @@
 -- * Applications of the arithmetic operators @(+,-,*,^)@
 normaliseNat :: TyConSubst -> Type -> Writer [(Type,Type)] (CoreSOP, [Coercion])
 normaliseNat givensTyConSubst ty
-  | Just tc_apps <- splitTyConApp_upTo givensTyConSubst ty
-  , (tc, xs, cos0) : _ <- NE.filter (( \ ( tc, _, _) -> tc `elem` knownTyCons)) tc_apps
-  = second ( ++ cos0 ) <$> goTyConApp tc xs
+  | Just (tc, xs) <- splitTyConApp_maybe ty
+  = goTyConApp tc xs
   | Just i <- isNumLitTy ty
   = return (S [P [I i]], [])
   | Just v <- getTyVar_maybe ty
@@ -143,8 +143,8 @@
           do (x', cos1) <- normaliseNat givensTyConSubst x
              (y', cos2) <- normaliseNat givensTyConSubst y
              return (normaliseExp x' y', cos1 ++ cos2)
-      goTyConApp tc xs =
-        return (S [P [C (CType $ mkTyConApp tc xs)]], [])
+      goTyConApp tc xs
+        = return (S [P [C (CType $ mkTyConApp tc xs)]], [])
 
 knownTyCons :: [TyCon]
 knownTyCons = [typeNatExpTyCon, typeNatMulTyCon, typeNatSubTyCon, typeNatAddTyCon]
@@ -166,20 +166,24 @@
 -- the same as input, returns @'Nothing'@.
 normaliseNatEverywhere :: TyConSubst -> Type -> Writer [(Type, Type)] (Maybe (Type, [Coercion]))
 normaliseNatEverywhere givensTyConSubst ty0
-  | Just tc_apps <- splitTyConApp_upTo givensTyConSubst ty0
-  = fmap asum $ for tc_apps $ \ (tc, fields, cos1) ->
-      if tc `elem` knownTyCons
+  | Just (tc, fields) <- splitTyConApp_maybe ty0
+  =   if tc `elem` knownTyCons
       then do
         -- Normalize under current type constructor application. 'go' skips all
         -- known type constructors.
         ty1M <- maybeRunWriter (go tc fields)
-        let (ty1, cos2) = fromMaybe (ty0, []) ty1M
+        let (ty1, cos1) = fromMaybe (ty0, []) ty1M
         -- Normalize (subterm-normalized) type given to 'normaliseNatEverywhere'
-        (ty2, cos3) <- normaliseSimplifyNat givensTyConSubst ty1
+        (ty2, cos2) <- normaliseSimplifyNat givensTyConSubst ty1
         -- TODO: 'normaliseNat' could keep track whether it changed anything. That's
         -- TODO: probably cheaper than checking for equality here.
-        pure (if ty2 `eqType` ty1 then second ((cos1 ++ cos2) ++) <$> ty1M else Just (ty2, cos1 ++ cos2 ++ cos3))
-      else go tc fields
+        pure $
+          if ty2 `eqType` ty1
+          then second (cos1 ++) <$> ty1M
+          else Just (ty2, cos1 ++ cos2)
+      else
+        go tc fields
+
   | otherwise
   = pure Nothing
  where
@@ -188,17 +192,18 @@
   go :: TyCon -> [Type] -> Writer [(Type, Type)] (Maybe (Type, [Coercion]))
   go tc_ fields0_ = do
     fields1_ <- mapM (maybeRunWriter . cont) fields0_
-    if any isJust fields1_ then
+    if any isJust fields1_
+    then do
       let cos' = concat $ mapMaybe (fmap snd) fields1_
-      in
-         pure (Just (mkTyConApp tc_ (zipWith (\ f0 f1 -> maybe f0 fst f1) fields0_ fields1_), cos'))
+          ty' = mkTyConApp tc_ (zipWith (\ f0 f1 -> maybe f0 fst f1) fields0_ fields1_)
+      pure (Just (ty', cos'))
     else
       pure Nothing
    where
     cont ty'
       | tc_ `elem` knownTyCons
-      , Just tc_apps' <- splitTyConApp_upTo givensTyConSubst ty'
-      = asum <$> traverse ( \ (tc', flds', cos') -> fmap (second (cos' ++)) <$> go tc' flds') tc_apps'
+      , Just (tc', flds') <- splitTyConApp_maybe ty'
+      = go tc' flds'
       | otherwise
       = normaliseNatEverywhere givensTyConSubst ty'
 
@@ -291,43 +296,60 @@
                                          ,reifySOP (S s2)
                                          ]
 
+-- | Simplify an inequality by first calling 'subtractIneq', producing a SOP
+-- term, and then creating a new inequality by moving all the terms with
+-- negative coefficients to one side.
+--
+-- Returns 'Nothing' if it is not able to simplify the original inequality.
+simplifyIneq :: Ineq -> Maybe Ineq
+simplifyIneq ineq@(x, y, isLE)
+  = if x' == x && y' == y
+    then Nothing
+    else Just (x', y', isLE)
+  where
+    S ps = subtractIneq ineq
+    (neg, pos) = partitionEithers $ map classify ps
+    (x', y') =
+      if isLE
+      then ( S neg, S pos )
+      else ( S pos, S neg )
+    classify :: CoreProduct -> Either CoreProduct CoreProduct
+    classify p@(P (I i : _))
+      | i < 0
+      = Left $ negateProd p
+    classify prod
+      = Right prod
+
+negateProd :: CoreProduct -> CoreProduct
+negateProd (P (I i : r)) =
+  -- preserve normal form
+  if i == (-1)
+  then
+    if null r
+    then P [I 1]
+    else P r
+  else P $ I (negate i) : r
+negateProd (P r) = P $ I (-1) : r
+
 -- | Subtract an inequality, in order to either:
 --
 -- * See if the smallest solution is a natural number
 -- * Cancel sums, i.e. monotonicity of addition
 --
 -- @
--- subtractIneq (2*y <=? 3*x ~ True)  = (-2*y + 3*x)
--- subtractIneq (2*y <=? 3*x ~ False) = (-3*x + (-1) + 2*y)
+-- subtractIneq (2*y <=? 3*x ~ True)  = 3*x + (-2)*y
+-- subtractIneq (2*y <=? 3*x ~ False) = -3*x + (-2)*y
 -- @
 subtractIneq
   :: (CoreSOP, CoreSOP, Bool)
   -> CoreSOP
 subtractIneq (x,y,isLE)
   | isLE
-  = mergeSOPAdd y (mergeSOPMul (S [P [I (-1)]]) x)
+  -- NB: keep orientations
+  = mergeSOPAdd (mergeSOPMul (S [P [I (-1)]]) x) y
   | otherwise
   = mergeSOPAdd x (mergeSOPMul (S [P [I (-1)]]) (mergeSOPAdd y (S [P [I 1]])))
 
--- | Try to reverse the process of 'subtractIneq'
---
--- E.g.
---
--- @
--- subtractIneq (2*y <=? 3*x ~ True) = (-2*y + 3*x)
--- sopToIneq (-2*y+3*x) = Just (2*x <=? 3*x ~ True)
--- @
-sopToIneq
-  :: CoreSOP
-  -> Maybe Ineq
-sopToIneq (S [P ((I i):l),r])
-  | i < 0
-  = Just (mergeSOPMul (S [P [I (negate i)]]) (S [P l]),S [r],True)
-sopToIneq (S [r,P ((I i:l))])
-  | i < 0
-  = Just (mergeSOPMul (S [P [I (negate i)]]) (S [P l]),S [r],True)
-sopToIneq _ = Nothing
-
 -- | Give the smallest solution for an inequality
 ineqToSubst
   :: Ineq
@@ -361,7 +383,7 @@
 substsSOP ((UnifyItem {}):s)   u = substsSOP s u
 
 substSOP :: (Outputable v, Outputable c, Ord v, Ord c) => v -> SOP v c -> SOP v c -> SOP v c
-substSOP tv e = foldr1 mergeSOPAdd . map (substProduct tv e) . unS
+substSOP tv e = foldr mergeSOPAdd (S []) . map (substProduct tv e) . unS
 
 substProduct :: (Outputable v, Outputable c, Ord v, Ord c) => v -> SOP v c -> Product v c -> SOP v c
 substProduct tv e = foldr1 mergeSOPMul . map (substSymbol tv e) . unP
@@ -406,20 +428,25 @@
 
 unifyNats' :: Ct -> CoreSOP -> CoreSOP -> UnifyResult
 unifyNats' ct u v
-  = if eqFV u v
-       then if containsConstants u || containsConstants v
-               then if u == v
-                       then Win
-                       else Draw (filter diffFromConstraint (unifiers ct u v))
-               else if u == v
-                       then Win
-                       else Lose
-       else Draw (filter diffFromConstraint (unifiers ct u v))
+  | u == v
+  = Win
+  | Just unifs <- unifiers ct u v
+  , let newUnifs = if isGiven (ctEvidence ct)
+                   then unifs
+                   else filter diffFromConstraint unifs
+  = Draw newUnifs
+  | otherwise
+  = Lose
   where
-    -- A unifier is only a unifier if differs from the original constraint
+
+    -- A unifier is only a unifier if it differs from the original constraint
     diffFromConstraint (UnifyItem x y) = not (x == u && y == v)
-    diffFromConstraint (SubstItem x y) = not (S [P [V x]] == u && y == v)
 
+    -- SubstItems can be in different orders
+    diffFromConstraint (SubstItem x y) =
+      not $ (S [P [V x]] == u && y == v)
+         || (S [P [V x]] == v && y == u)
+
 -- | Find unifiers for two SOP terms
 --
 -- Can find the following unifiers:
@@ -453,46 +480,40 @@
 -- @
 -- [a := b]
 -- @
-unifiers :: Ct -> CoreSOP -> CoreSOP -> [CoreUnify]
+unifiers :: Ct -> CoreSOP -> CoreSOP -> Maybe [CoreUnify]
 unifiers ct u@(S [P [V x]]) v
-  = case classifyPredType $ ctEvPred $ ctEvidence ct of
-      EqPred NomEq t1 _
-        | CType (reifySOP u) /= CType t1 || isGiven (ctEvidence ct)
-        -> [SubstItem x v]
-      _ -> []
+  | EqPred NomEq t1 _ <- classifyPredType $ ctEvPred $ ctEvidence ct
+  , CType (reifySOP u) /= CType t1 || isGiven (ctEvidence ct)
+  = return [SubstItem x v]
 unifiers ct u v@(S [P [V x]])
-  = case classifyPredType $ ctEvPred $ ctEvidence ct of
-      EqPred NomEq _ t2
-        | CType (reifySOP v) /= CType t2 || isGiven (ctEvidence ct)
-        -> [SubstItem x u]
-      _ -> []
+  | EqPred NomEq _ t2 <- classifyPredType $ ctEvPred $ ctEvidence ct
+  , CType (reifySOP v) /= CType t2 || isGiven (ctEvidence ct)
+  = return [SubstItem x u]
 unifiers ct u@(S [P [C _]]) v
-  = case classifyPredType $ ctEvPred $ ctEvidence ct of
-      EqPred NomEq t1 t2
-        | CType (reifySOP u) /= CType t1 || CType (reifySOP v) /= CType t2
-        -> [UnifyItem u v]
-      _ -> []
+  | EqPred NomEq t1 t2 <- classifyPredType $ ctEvPred $ ctEvidence ct
+  , CType (reifySOP u) /= CType t1 || CType (reifySOP v) /= CType t2
+  = return [UnifyItem u v]
 unifiers ct u v@(S [P [C _]])
-  = case classifyPredType $ ctEvPred $ ctEvidence ct of
-      EqPred NomEq t1 t2
-        | CType (reifySOP u) /= CType t1 || CType (reifySOP v) /= CType t2
-        -> [UnifyItem u v]
-      _ -> []
+  | EqPred NomEq t1 t2 <- classifyPredType $ ctEvPred $ ctEvidence ct
+  , CType (reifySOP u) /= CType t1 || CType (reifySOP v) /= CType t2
+  = return [UnifyItem u v]
 unifiers ct u v             = unifiers' ct u v
 
-unifiers' :: Ct -> CoreSOP -> CoreSOP -> [CoreUnify]
-unifiers' _ct (S [])        (S [])        = []
-
-unifiers' _ct (S [P [V x]]) (S [])        = [SubstItem x (S [P [I 0]])]
-unifiers' _ct (S [])        (S [P [V x]]) = [SubstItem x (S [P [I 0]])]
-
-unifiers' _ct (S [P [V x]]) s             = [SubstItem x s]
-unifiers' _ct s             (S [P [V x]]) = [SubstItem x s]
+unifiers' :: Ct -> CoreSOP -> CoreSOP -> Maybe [CoreUnify]
+unifiers' _ct (S [])        (S [])        = return []
 
-unifiers' _ct (S [P [C {}]])   (S [P [C {}]])   = []
-unifiers' _ct s1@(S [P [C _]]) s2               = [UnifyItem s1 s2]
-unifiers' _ct s1               s2@(S [P [C _]]) = [UnifyItem s1 s2]
+unifiers' _ct (S [P [V x]]) (S [])        = return [SubstItem x (S [P [I 0]])]
+unifiers' _ct (S [])        (S [P [V x]]) = return [SubstItem x (S [P [I 0]])]
 
+unifiers' _ct (S [P [V x]]) s = do
+  guard $ canBeNatural s
+  return [SubstItem x s]
+unifiers' _ct s (S [P [V x]]) = do
+  guard $ canBeNatural s
+  return [SubstItem x s]
+unifiers' _ct s1@(S [P [C {}]]) s2@(S [P [C {}]])
+  | s1 == s2
+  = return []
 
 -- (z ^ a) ~ (z ^ b) ==> [a := b]
 unifiers' ct (S [P [E s1 p1]]) (S [P [E s2 p2]])
@@ -503,13 +524,13 @@
   | all (`elem` p2) s1
   = let base = intersect s1 p2
         diff = p2 \\ s1
-    in  unifiers ct (S [P diff]) (S [P [E (S [P base]) (P [I (-1)]),E (S [P base]) p1]])
+    in  unifiers' ct (S [P diff]) (S [P [E (S [P base]) (P [I (-1)]),E (S [P base]) p1]])
 
 unifiers' ct (S [P p2]) (S [P [E (S [P s1]) p1]])
   | all (`elem` p2) s1
   = let base = intersect s1 p2
         diff = p2 \\ s1
-    in  unifiers ct (S [P [E (S [P base]) (P [I (-1)]),E (S [P base]) p1]]) (S [P diff])
+    in  unifiers' ct (S [P [E (S [P base]) (P [I (-1)]),E (S [P base]) p1]]) (S [P diff])
 
 -- (i ^ a) ~ j ==> [a := round (logBase i j)], when `i` and `j` are integers,
 -- and `ceiling (logBase i j) == floor (logBase i j)`
@@ -558,36 +579,25 @@
           | otherwise = ps2'
     psx  = intersect ps1 ps2
 
--- (2 + a) ~ 5 ==> [a := 3]
-unifiers' ct (S ((P [I i]):ps1)) (S ((P [I j]):ps2))
-  = case compare i j of
-       EQ -> unifiers' ct (S ps1) (S ps2)
-       LT -> unifiers' ct (S ps1) (S ((P [I (j-i)]):ps2))
-       GT -> unifiers' ct (S ((P [I (i-j)]):ps1)) (S ps2)
-
 -- (a + c) ~ (b + c) ==> [a := b]
+--
+-- NB: this also handles situations such as (2 + x) ~ 5 ==> [x := 3].
 unifiers' ct s1@(S ps1) s2@(S ps2)
-  | Just (s1',s2',_) <- sopToIneq k1
-  , s1' /= s1 || s2' /= s2
-  , maybe True (uncurry (&&) . second Set.null) (runWriterT (isNatural s1'))
-  , maybe True (uncurry (&&) . second Set.null) (runWriterT (isNatural s2'))
+  | Just (s1',s2',_) <- simplifyIneq (s1, s2, True)
   = unifiers' ct s1' s2'
-  | null psx
-  , length ps1 == length ps2
-  , length ps1 > 1
-  , let unifs = nub $ concat (zipWith (\x y -> unifiers' ct (S [x]) (S [y])) ps1 ps2)
-  , length unifs <= 1
-  = case unifs of
-        []  -> unifiers'' ct (S ps1) (S ps2)
-        [k] -> [k]
-        _   -> error "impossible"
+  | Just term_unifs <- termByTerm ct ps1 ps2
+  = Just term_unifs
+  -- If there are only two variables, try to collect them on either side.
+  -- This makes 'termByTerm' more likely to succeed.
+  | Just (S coll1, S coll2) <- partitionTerms ps1 ps2
+  , Just term_unifs <- termByTerm ct coll1 coll2
+  = Just term_unifs
   | null psx
   , isGiven (ctEvidence ct)
   = unifiers'' ct (S ps1) (S ps2)
   | not $ null psx
   = unifiers' ct (S ps1'') (S ps2'')
   where
-    k1 = subtractIneq (s1,s2,True)
     ps1'  = ps1 \\ psx
     ps2'  = ps2 \\ psx
     ps1'' | null ps1' = [P [I 0]]
@@ -596,14 +606,82 @@
           | otherwise = ps2'
     psx = intersect ps1 ps2
 
-unifiers' _ s1 s2 = [UnifyItem s1 s2]
+unifiers' _ s1 s2 = return [UnifyItem s1 s2]
 
-unifiers'' :: Ct -> CoreSOP -> CoreSOP -> [CoreUnify]
+-- | Try to match the two expressions term-by-term.
+-- If this produces a **single unifier**, then we succeed.
+--
+-- Example: x + 3^(x+2) ~ 2*y - 3^(2*(y+1))
+--
+-- We recur on each pair, (x, 2*y), (3^(x+2),3^(2*(y+1))).
+-- This produces a single unifier "x ~ 2*y", so we proceed.
+--
+-- NB: this is somewhat fragile: if one moves the terms with negative
+-- coefficients to the other side, due to the variable ordering x < y,
+-- we would get:
+--
+--   x + 3^(2*(y+1)) ~ 3^(x+2) + 2*y
+--
+-- for which the same approach fails. So we use 'partitionTerms' as a heuristic
+-- in the case there are only two free variables.
+-- See https://github.com/clash-lang/ghc-typelits-natnormalise/issues/96.
+termByTerm :: Ct -> [CoreProduct] -> [CoreProduct] -> Maybe [CoreUnify]
+termByTerm ct ps1 ps2
+  | length ps1 == length ps2
+  , length ps1 > 1
+  , Just u@[_] <- unifs
+  = Just u
+  | otherwise
+  = Nothing
+  where
+    unifs = fmap (nub . concat) (zipWithM (\x y -> unifiers' ct (S [x]) (S [y])) ps1 ps2)
+
+-- | If an equality only contains two free variables, try to collect
+-- terms with either FV on either side of the equality.
+--
+-- This makes 'termByTerm' more likely to succeed.
+partitionTerms :: [CoreProduct] -> [CoreProduct] -> Maybe (CoreSOP, CoreSOP)
+partitionTerms lhs rhs
+  | [fv1, fv2] <- fvs
+  , Just (lhs1, lhs2) <- mbPairs fv1 fv2 lhs
+  , Just (rhs1, rhs2) <- mbPairs fv1 fv2 rhs
+  = Just $
+      let (lhs', rhs') =
+            if length rhs1 + length lhs2 <= length lhs1 + length rhs2
+            then (lhs1 ++ map negateProd rhs1, map negateProd lhs2 ++ rhs2)
+            else (map negateProd lhs1 ++ rhs1, lhs2 ++ map negateProd rhs2)
+      in (simplifySOP (S lhs'), simplifySOP (S rhs'))
+  | otherwise
+  = Nothing
+  where
+    fvs :: [TyVar]
+    fvs = nonDetEltsUniqSet $ fvSOP (S $ lhs ++ rhs)
+
+    mbPairs :: TyVar -> TyVar -> [CoreProduct] -> Maybe ([CoreProduct], [CoreProduct])
+    mbPairs fv1 fv2 x = partitionEithers <$> traverse ( collect fv1 fv2 ) x
+
+    collect :: TyVar -> TyVar -> CoreProduct -> Maybe (Either CoreProduct CoreProduct)
+    collect fv1 fv2 tm =
+      let tmFvs = fvProduct tm
+      in case (fv1 `elementOfUniqSet` tmFvs, fv2 `elementOfUniqSet` tmFvs) of
+           (True, False) -> Just $ Left  tm
+           (False, True) -> Just $ Right tm
+           _             -> Nothing
+
+unifiers'' :: Ct -> CoreSOP -> CoreSOP -> Maybe [CoreUnify]
 unifiers'' ct (S [P [I i],P [V v]]) s2
-  | isGiven (ctEvidence ct) = [SubstItem v (mergeSOPAdd s2 (S [P [I (negate i)]]))]
+  | isGiven (ctEvidence ct)
+  , let s' = mergeSOPAdd s2 (S [P [I (negate i)]])
+  = if canBeNatural s'
+    then Just [SubstItem v s']
+    else Nothing
 unifiers'' ct s1 (S [P [I i],P [V v]])
-  | isGiven (ctEvidence ct) = [SubstItem v (mergeSOPAdd s1 (S [P [I (negate i)]]))]
-unifiers'' _ _ _ = []
+  | isGiven (ctEvidence ct)
+  , let s' = mergeSOPAdd s1 (S [P [I (negate i)]])
+  = if canBeNatural s'
+    then Just [SubstItem v s']
+    else Nothing
+unifiers'' _ _ _ = Just []
 
 collectBases :: CoreProduct -> Maybe ([CoreSOP],[CoreProduct])
 collectBases = fmap unzip . traverse go . unP
@@ -624,18 +702,6 @@
 fvSymbol (V v)   = unitUniqSet v
 fvSymbol (E s p) = fvSOP s `unionUniqSets` fvProduct p
 
-eqFV :: CoreSOP -> CoreSOP -> Bool
-eqFV = (==) `on` fvSOP
-
-containsConstants :: CoreSOP -> Bool
-containsConstants =
-  any (any symbolContainsConstant . unP) . unS
-  where
-    symbolContainsConstant c = case c of
-      C {} -> True
-      E s p -> containsConstants s || containsConstants (S [p])
-      _ -> False
-
 safeDiv :: Integer -> Integer -> Maybe Integer
 safeDiv i j
   | j == 0    = Just 0
@@ -655,12 +721,38 @@
          else Just (smallInteger z1)
 integerLogBase _ _ = Nothing
 
+-- | Might this be a natural number?
+--
+-- Equivalently: it is not the case that this is definitely not a natural number.
+--
+-- For example, @-1@ is definitely not a natural number, while @α@ or
+-- @-2 * β@ could both be natural numbers (where @α, β@ are metavariables).
+canBeNatural :: CoreSOP -> Bool
+canBeNatural = maybe True fst . runWriterT . isNatural
+
+-- | Is this a natural number?
+--
+--  - @Just True@ <=> definitely a natural number
+--  - @Just False@ <=> definitely not a natural number
+--  - @Nothing@ <=> not sure
+--
+-- The 'Set CType' writer accumulator returns inner types that must also be
+-- positive for the overall 'CoreSOP' to be positive.
 isNatural :: CoreSOP -> WriterT (Set CType) Maybe Bool
 isNatural (S [])           = return True
 isNatural (S [P []])       = return True
-isNatural (S [P (I i:ps)])
-  | i >= 0    = isNatural (S [P ps])
-  | otherwise = return False
+isNatural (S [P (I i:ps)]) =
+  case compare i 0 of
+    EQ -> return True
+    GT ->
+      -- NB: assumes the SOP term has been normalised, so no possibly of
+      -- a second negative constant factor to cancel out this one.
+      isNatural (S [P ps])
+    LT ->
+      -- '-1 * ty' can be a natural number if 'ty' ends up being zero
+      if any canBeZero ps
+      then WriterT Nothing
+      else return False
 isNatural (S [P (V _:ps)]) = isNatural (S [P ps])
 isNatural (S [P (E s p:ps)]) = do
   sN <- isNatural s
@@ -683,6 +775,23 @@
     -- if one is natural and the other isn't, then their sum *might* be natural,
     -- but we simply cant be sure.
 
+-- | Can this 'CoreSymbol' be zero?
+--
+-- Examples:
+--
+--  - the literal '0',
+--  - a metavariable,
+--  - a type family application.
+canBeZero :: CoreSymbol -> Bool
+canBeZero (I i) = i == 0
+canBeZero (C {}) = True -- e.g. 'F 3' where 'F' is a type family
+canBeZero (E (S es) _)
+  | [P bs] <- es
+  = any canBeZero bs
+  | otherwise
+  = True
+canBeZero (V {}) = True -- e.g. 'tau' where 'tau' is an unfilled metavariable
+
 -- | Try to solve inequalities
 solveIneq
   :: Word
@@ -802,14 +911,12 @@
 -- * SOP version: -2 + x
 -- * Convert back to inequality: 2 <= x
 plusMonotone :: IneqRule
-plusMonotone want have
-  | Just want' <- sopToIneq (subtractIneq want)
-  , want' /= want
-  = pure [(want',have)]
-  | Just have' <- sopToIneq (subtractIneq have)
-  , have' /= have
-  = pure [(want,have')]
-plusMonotone _ _ = noRewrite
+plusMonotone want have =
+  case (simplifyIneq want, simplifyIneq have) of
+    (Just want', Just have') -> pure [(want', have')]
+    (Just want', _         ) -> pure [(want', have )]
+    (_         , Just have') -> pure [(want , have')]
+    _ -> noRewrite
 
 -- | Make the `a` of a given `a <= b` smaller
 haveSmaller :: IneqRule
diff --git a/tests/ErrorTests.hs b/tests/ErrorTests.hs
--- a/tests/ErrorTests.hs
+++ b/tests/ErrorTests.hs
@@ -9,6 +9,7 @@
 {-# LANGUAGE TypeApplications    #-}
 {-# LANGUAGE TypeFamilies        #-}
 {-# LANGUAGE TypeOperators       #-}
+{-# LANGUAGE UndecidableInstances#-}
 
 #if __GLASGOW_HASKELL__ >= 805
 {-# LANGUAGE NoStarIsType        #-}
@@ -523,4 +524,43 @@
           then litE $ stringL "Couldn't match type ‘1 <=? (m ^ 2)’ with ‘'True’"
           else litE $ stringL "Couldn't match type `1 <=? (m ^ 2)' with 'True"
     )]
+#endif
+
+type family Drop (n :: Nat) (xs :: [Nat]) :: [Nat] where
+    Drop 0 xs = xs
+    Drop n (x ': xs) = Drop (n-1) xs
+    Drop n '[] = '[]
+
+t99 :: Proxy ns -> Proxy ( Drop 1 ns ) -> Proxy ( Drop 2 ns )
+t99 _ px = px
+
+-- Don't want an error of the form 'Couldn't match 1 with 0'
+-- because that means the plugin turned [W] Drop 1 ns ~ Drop 2 ns
+-- into 1 ~ 2, which is not valid as Drop is not injective.
+t99_errors =
+#if __GLASGOW_HASKELL__ >= 811
+  [ "Couldn't match type: Drop 1 ns"
+  , "               with: Drop 2 ns"
+  , "Expected: Proxy (Drop 2 ns)"
+  , "  Actual: Proxy (Drop 1 ns)"
+  , $(do localeEncoding <- runIO (getLocaleEncoding)
+         if textEncodingName localeEncoding == textEncodingName utf8
+           then litE $ stringL "‘Drop’ is a non-injective type family"
+           else litE $ stringL "`Drop' is a non-injective type family"
+     )
+  ]
+#else
+  [ $(do localeEncoding <- runIO (getLocaleEncoding)
+         if textEncodingName localeEncoding == textEncodingName utf8
+           then litE $ stringL "Couldn't match type ‘Drop 1 ns’ with ‘Drop 2 ns’"
+           else litE $ stringL "Couldn't match type `Drop 1 ns' with `Drop 2 ns'"
+    )
+  , "Expected type: Proxy (Drop 2 ns)"
+  , "  Actual type: Proxy (Drop 1 ns)"
+  , $(do localeEncoding <- runIO (getLocaleEncoding)
+         if textEncodingName localeEncoding == textEncodingName utf8
+           then litE $ stringL "‘Drop’ is a non-injective type family"
+           else litE $ stringL "`Drop' is a non-injective type family"
+     )
+  ]
 #endif
diff --git a/tests/Tests.hs b/tests/Tests.hs
--- a/tests/Tests.hs
+++ b/tests/Tests.hs
@@ -363,7 +363,7 @@
    . ((x + 1) ~ (2 * y), 1 <= y)
   => Proxy x
   -> Proxy y
-  -> Proxy (((2 * (y - 1)) + 1))
+  -> Proxy ((2 * (y - 1)) + 1)
   -> Proxy x
 proxyEq3 _ _ x = x
 
@@ -627,6 +627,7 @@
     , testCase "(CLog 2 (2 ^ n) ~ n, (1 <=? n) ~ True) => n ~ (n+d)" $
         testProxy15 (Proxy :: Proxy 1) `throws` testProxy15Errors
     , testCase "(n - 1) + 1 ~ n implies (1 <= n)" $ test16 `throws` test16Errors
+    , testCase "Do not unify in non-injective positions" $ t99 `throws` t99_errors
     , testGroup "Inequality"
       [ testCase "a+1 <= a" $ testProxy9 `throws` testProxy9Errors
       , testCase "(a <=? a+1) ~ False" $ testProxy10 `throws` testProxy10Errors
@@ -723,13 +724,28 @@
 #endif
 
 -- Test for https://github.com/clash-lang/ghc-typelits-natnormalise/issues/71
-t1 :: (((1 + m1) + n1) ~ (1 + (m2 + n2))) => Proxy '(m1, n1, m2, n2) -> ()
-t1 _ = ()
-t2 :: ((m1 + n1) ~ (m2 + n2)) => Proxy '(m1, n1, m2, n2) -> ()
-t2 px = t1 px
+t71_aux :: (((1 + m1) + n1) ~ (1 + (m2 + n2))) => Proxy '(m1, n1, m2, n2) -> ()
+t71_aux _ = ()
+t71 :: ((m1 + n1) ~ (m2 + n2)) => Proxy '(m1, n1, m2, n2) -> ()
+t71 px = t71_aux px
 
+-- Test for https://github.com/clash-lang/ghc-typelits-natnormalise/issues/94
+t94 ::
+  (KnownNat n, KnownNat m, KnownNat s, s ~ (m - n)) =>
+  Proxy m -> Proxy n -> Proxy (s + 2) -> Proxy (s + 2)
+t94 _ _ = t94_aux
 
+t94_aux :: (1 <= n) => Proxy n -> Proxy n
+t94_aux px = px
 
+-- Test for https://github.com/clash-lang/ghc-typelits-natnormalise/issues/96
+t96
+  :: ( 2 <= x, 2 <= y
+     , ( 4 * x + 2 * 2^y ) ~ ( 4 * y + 2 * 2^x )
+     )
+  => Proxy x -> Proxy y
+t96 x = x
+
 type family TF (a :: Nat) (b :: Nat) :: Nat
 
 proxyEq5
@@ -747,3 +763,25 @@
     -> Proxy b
     -> Proxy (3 * TF (3 * a) b)
   theProxy _ _ = Proxy
+
+type family Rank sh where
+  Rank '[] = 0
+  Rank (_ : sh) = Rank sh + 1
+foo :: ( ( 1 + Rank sh ) ~ ( 1 + n ) )
+    => Proxy sh -> Proxy n -> Proxy (Rank sh) -> Proxy n
+foo _ _ px = px
+
+noContra :: ((Rank sh + 2) <= 2) => Proxy sh -> ()
+noContra _ = ()
+
+-- Test for https://github.com/clash-lang/ghc-typelits-natnormalise/issues/97
+t97 :: ( (1 + n) ~ m, ( m - 1 ) ~ n ) => Proxy m -> Proxy n -> ()
+t97  _ _ = ()
+
+t97b
+  :: ( n ~ (m - 2)
+     , (n + 1) ~ (m - 1)
+     , m ~ (n + 2)
+     )
+  => Proxy n -> Proxy m -> ()
+t97b _ _ = ()