diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,13 @@
 # Changelog for the [`ghc-typelits-natnormalise`](http://hackage.haskell.org/package/ghc-typelits-natnormalise) package
 
+## Unreleased
+
+## 0.9.4 *March 19th 2026*
+* Fixes [#116](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/113) Compile-time loop when processing Given constraints.
+* Fixes [#119](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/119) solving constraints involving type families applied to normalised Nat expressions (e.g. `Foo (a + b)`).
+* Fixes [#120](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/120) stop emitting Assert (a <=? b) msg ~ (() :: Constraint) constraints
+* Fixed regression [#124](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/124) involving unification of summands.
+
 ## 0.9.3 *December 2nd 2025*
 * Fixes [#114](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/113) Poor error message in plugin version 0.8 and higher
 * Fixes [#113](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/113) Wanted contraints rewrites to itself, leading to infinite solver iterations
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.9.3
+version:             0.9.4
 synopsis:            GHC typechecker plugin for types of kind GHC.TypeLits.Nat
 description:
   A type checker plugin for GHC that can solve /equalities/ and /inequalities/
@@ -46,7 +46,7 @@
                                  2017-2018, QBayLogic B.V.
 category:            Type System
 build-type:          Simple
-extra-source-files:  README.md
+extra-doc-files:     README.md
                      CHANGELOG.md
 tested-with:         GHC == 8.8.4, GHC == 8.10.7, GHC == 9.0.2, GHC == 9.2.8,
                      GHC == 9.4.8, GHC == 9.6.7, GHC == 9.8.4, GHC == 9.10.2,
@@ -70,7 +70,7 @@
   build-depends:       base                >=4.9   && <5,
                        containers          >=0.5.7.1 && <0.9,
                        ghc                 >=8.8.1 && <9.15,
-                       ghc-tcplugin-api    >=0.18.0 && <0.19,
+                       ghc-tcplugin-api    >=0.18.2 && <0.19,
                        transformers        >=0.5.2.0 && < 0.7
   if impl(ghc >= 9.0.0)
     build-depends:     ghc-bignum >=1.0 && <1.5
@@ -100,23 +100,26 @@
 test-suite unit-tests
   type:                exitcode-stdio-1.0
   main-is:             Tests.hs
-  Other-Modules:       ErrorTests
+  Other-Modules:       ShouldError
+                       ShouldError.Tasty
   build-depends:       base >=4.8 && <5,
                        ghc-typelits-natnormalise,
+                       interpolate,
+                       process,
                        tasty >= 0.10,
                        tasty-hunit >= 0.9,
-                       template-haskell >= 2.11.0.0
+                       temporary
   if impl(ghc >= 9.4)
     build-depends:     ghc-prim >= 0.9
   hs-source-dirs:      tests
+  ghc-options:         -Wall
   default-language:    Haskell2010
   other-extensions:    DataKinds
                        GADTs
                        KindSignatures
                        NoImplicitPrelude
-                       TemplateHaskell
                        TypeFamilies
                        TypeOperators
                        ScopedTypeVariables
   if flag(deverror)
-    ghc-options:       -dcore-lint
+    ghc-options:       -Werror -dcore-lint
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
@@ -300,26 +300,43 @@
       simplifyNats opts tcs [] $
         concatMap (toNatEquality opts tcs givensTyConSubst) redGivens
 
-    -- Only enter actual new evidence into the solver loop, i.e. we could derive
-    -- a new given in our solver loop for which there already is existing evidence.
-    -- We have no use for two different proofs of the same fact.
-    let givensPreds = map (CType . ctEvPred . ctEvidence) givens
-        actuallyNewGivens =
-          filter ((`notElem` givensPreds) . CType . ctEvPred . ctEvidence) newGivens
-    -- For now, only admit improved givens in the form of `n ~ L`, where `n` is
-    -- a type variable and `L` is a numeric literal.
-    let simplNewGivens = filter
-          ( \case {EqPred NomEq t1 t2 -> isTyVarTy t1 && isJust (isNumLitTy t2); _ -> False}
-          . classifyPredType
-          . ctEvPred
-          . ctEvidence
-          ) actuallyNewGivens
+    -- Only add new Givens that are genuinely new, i.e. that GHC doesn't
+    -- already know.
+    --
+    -- For example, in #116 we had: [G] m ~ n, [G] n ~ 0. Recalling that
+    -- the inert set in GHC is a /not necessarily idempotent/ terminating
+    -- generalised substitution (see Note [The KickOut Criteria] in GHC.Tc.Solver.InertSet),
+    -- we don't want to emit a new Given [G] m ~ 0: GHC already knows this, and
+    -- if we repeatedly emit this Given we will cause a typechecker loop (as in #116).
+    let
+      isSolvedGiven subst ct =
+        case classifyPredType $ substTy subst (ctPred ct) of
+          EqPred _rel t1 t2 -> t1 `eqType` t2
+          _ -> False
+      tyEqLit ct =
+        case classifyPredType (ctPred ct) of
+          EqPred NomEq t1 t2 -> isTyVarTy t1 && isJust (isNumLitTy t2)
+          _ -> False
+      givensSubst = ctsSubst givens -- Computes the idempotent substitution from the Givens
+      actuallyNewGivens =
+        filter
+          (\ ct ->
+            tyEqLit ct
+              -- For now, only admit improved Givens in the form of `n ~ L`,
+              -- where `n` is a type variable and `L` is a numeric literal.
+              &&
+            not (isSolvedGiven givensSubst ct)
+              -- Ensure this Given is genuinely new information to GHC, to
+              -- avoid repeatedly emitting facts that GHC already knows,
+              -- which can cause the typechecker to loop (#116).
+          )
+          newGivens
 
     tcPluginTrace "decideEqualSOP Givens }" $
       vcat [ text "givens:" <+> ppr givens
            , text "simpls:" <+> ppr simplifiedWanteds
            , text "contra:" <+> ppr contradictions
-           , text "new:" <+> ppr simplNewGivens
+           , text "new:" <+> ppr actuallyNewGivens
            ]
     return $
       mkTcPluginSolveResult
@@ -329,7 +346,7 @@
         []
 #endif
         [] -- no solved Givens
-        simplNewGivens
+        actuallyNewGivens
 
 -- Solving phase.
 -- Solves in/equalities on Nats and simplifiable constraints
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
@@ -140,14 +140,7 @@
 -- | The constraint @(a <= b)@.
 mkLEqNat :: LookedUpTyCons -> Type -> Type -> PredType
 mkLEqNat tcs a b =
-#if MIN_VERSION_ghc(9,3,0)
-  -- Starting from GHC 9.3, (a <= b) turns into 'Assert (a <=? b) msg'.
-  -- We prefer to emit 'Assert (a <=? b) msg ~ (() :: Constraint)',
-  -- in order to avoid creating an Irred constraint.
-  mkEqPredRole Nominal
-    (mkTyConApp (leqTyCon tcs) [natKind, a, b])
-    (mkTyConTy $ c0TyCon tcs)
-#elif MIN_VERSION_ghc(9,1,0)
+#if MIN_VERSION_ghc(9,1,0)
   mkTyConApp (leqTyCon tcs) [natKind, a, b]
 #else
   mkTyConApp (leqNatTyCon tcs) [a, b]
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
@@ -106,12 +106,7 @@
 type CoreProduct = Product TyVar CType
 type CoreSymbol  = Symbol TyVar CType
 
--- | Convert a type of /kind/ 'GHC.TypeLits.Nat' to an 'SOP' term, but
--- only when the type is constructed out of:
---
--- * literals
--- * type variables
--- * Applications of the arithmetic operators @(+,-,*,^)@
+-- | Convert a type of /kind/ 'GHC.TypeLits.Nat' to an 'SOP' term
 normaliseNat :: Type -> Writer [(Type,Type)] (CoreSOP, [Coercion])
 normaliseNat ty
   | Just (tc, xs) <- splitTyConApp_maybe ty
@@ -143,7 +138,8 @@
              (y', cos2) <- normaliseNat y
              return (normaliseExp x' y', cos1 ++ cos2)
       goTyConApp tc xs
-        = return (S [P [C (CType $ mkTyConApp tc xs)]], [])
+        = do (xs', cos') <- fmap unzip (traverse normaliseSimplifyNat xs)
+             return (S [P [C (CType (mkTyConApp tc xs'))]], concat cos')
 
 knownTyCons :: [TyCon]
 knownTyCons = [typeNatExpTyCon, typeNatMulTyCon, typeNatSubTyCon, typeNatAddTyCon]
@@ -592,6 +588,8 @@
 --
 -- NB: this also handles situations such as (2 + x) ~ 5 ==> [x := 3].
 unifiers' ct s1@(S ps1) s2@(S ps2)
+  | not $ null psx
+  = unifiers' ct (S ps1'') (S ps2'')
   | Just (s1',s2',_) <- simplifyIneq (s1, s2, True)
   = unifiers' ct s1' s2'
   | Just term_unifs <- termByTerm ct ps1 ps2
@@ -604,8 +602,6 @@
   | null psx
   , isGiven (ctEvidence ct)
   = unifiers'' ct (S ps1) (S ps2)
-  | not $ null psx
-  = unifiers' ct (S ps1'') (S ps2'')
   where
     ps1'  = ps1 \\ psx
     ps2'  = ps2 \\ psx
diff --git a/tests/ErrorTests.hs b/tests/ErrorTests.hs
deleted file mode 100644
--- a/tests/ErrorTests.hs
+++ /dev/null
@@ -1,612 +0,0 @@
-{-# LANGUAGE CPP                 #-}
-{-# LANGUAGE ConstraintKinds     #-}
-{-# LANGUAGE DataKinds           #-}
-{-# LANGUAGE FlexibleContexts    #-}
-{-# LANGUAGE GADTs               #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE StandaloneDeriving  #-}
-{-# LANGUAGE TemplateHaskell     #-}
-{-# LANGUAGE TypeApplications    #-}
-{-# LANGUAGE TypeFamilies        #-}
-{-# LANGUAGE TypeOperators       #-}
-{-# LANGUAGE UndecidableInstances#-}
-
-#if __GLASGOW_HASKELL__ >= 805
-{-# LANGUAGE NoStarIsType        #-}
-#endif
-
-{-# OPTIONS_GHC -fdefer-type-errors #-}
-{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}
-module ErrorTests where
-
-import Data.Proxy
-import GHC.TypeLits
-#if __GLASGOW_HASKELL__ >= 903
-import GHC.Types
-#endif
-
-import GHC.IO.Encoding            (getLocaleEncoding, textEncodingName, utf8)
-import Language.Haskell.TH        (litE, stringL)
-import Language.Haskell.TH.Syntax (runIO)
-#if __GLASGOW_HASKELL__ >= 901
-import qualified Data.Type.Ord
-#endif
-
-#if __GLASGOW_HASKELL__ >= 901
-import qualified Data.Type.Ord
-#endif
-
-testProxy1 :: Proxy (x + 1) -> Proxy (2 + x)
-testProxy1 = id
-
-testProxy1Errors =
-#if __GLASGOW_HASKELL__ >= 914
-  ["Expected: Proxy (2 + x)"
-  ,"  Actual: Proxy (x + 1)"
-  ]
-#elif __GLASGOW_HASKELL__ >= 900
-  ["Expected: Proxy (x + 1) -> Proxy (2 + x)"
-  ,"  Actual: Proxy (x + 1) -> Proxy (x + 1)"
-  ]
-#else
-  ["Expected type: Proxy (x + 1) -> Proxy (2 + x)"
-  ,"Actual type: Proxy (2 + x) -> Proxy (2 + x)"
-  ]
-#endif
-
-type family GCD (x :: Nat) (y :: Nat) :: Nat
-type instance GCD 6 8 = 2
-type instance GCD 9 6 = 3
-
-testProxy2 :: Proxy (GCD 6 8 + x) -> Proxy (x + GCD 9 6)
-testProxy2 = id
-
-testProxy2Errors =
-#if __GLASGOW_HASKELL__ >= 914
-  ["Expected: Proxy (x + GCD 9 6)"
-  ,"  Actual: Proxy (2 + x)"
-  ]
-#elif __GLASGOW_HASKELL__ >= 900
-  ["Expected: Proxy (GCD 6 8 + x) -> Proxy (x + GCD 9 6)"
-  ,"  Actual: Proxy (2 + x) -> Proxy (2 + x)"
-  ]
-#else
-  ["Expected type: Proxy (GCD 6 8 + x) -> Proxy (x + GCD 9 6)"
-  ,"Actual type: Proxy (x + 3) -> Proxy (x + 3)"
-  ]
-#endif
-
-proxyFun3 :: Proxy (x + x + x) -> ()
-proxyFun3 = const ()
-
-testProxy3 :: Proxy 8 -> ()
-testProxy3 = proxyFun3
-
-testProxy3Errors =
-#if __GLASGOW_HASKELL__ >= 914
-  ["Expected: Proxy ((x0 + x0) + x0)"
-  ,"  Actual: Proxy 8"
-  ]
-#elif __GLASGOW_HASKELL__ >= 900
-  ["Expected: Proxy 8 -> ()"
-  ,"  Actual: Proxy ((x0 + x0) + x0) -> ()"
-  ]
-#else
-  ["Expected type: Proxy 8 -> ()"
-  ,"Actual type: Proxy ((x0 + x0) + x0) -> ()"
-  ]
-#endif
-
-proxyFun4 :: Proxy ((2*y)+4) -> ()
-proxyFun4 = const ()
-
-testProxy4 :: Proxy 2 -> ()
-testProxy4 = proxyFun4
-
-testProxy4Errors =
-#if __GLASGOW_HASKELL__ >= 914
-  ["Expected: Proxy ((2 * y0) + 4)"
-  ,"  Actual: Proxy 2"
-  ]
-#elif __GLASGOW_HASKELL__ >= 900
-  ["Expected: Proxy 2 -> ()"
-  ,"  Actual: Proxy ((2 * y0) + 4) -> ()"
-  ]
-#else
-  ["Expected type: Proxy 2 -> ()"
-  ,"Actual type: Proxy ((2 * y0) + 4) -> ()"
-  ]
-#endif
-
-testProxy5 :: Proxy 7 -> ()
-testProxy5 = proxyFun4
-
-testProxy5Errors =
-#if __GLASGOW_HASKELL__ >= 914
-  ["Expected: Proxy ((2 * y1) + 4)"
-  ,"  Actual: Proxy 7"
-  ]
-#elif __GLASGOW_HASKELL__ >= 900
-  ["Expected: Proxy 7 -> ()"
-  ,"  Actual: Proxy ((2 * y1) + 4) -> ()"
-  ]
-#else
-  ["Expected type: Proxy 7 -> ()"
-  ,"Actual type: Proxy ((2 * y1) + 4) -> ()"
-  ]
-#endif
-
-proxyFun6 :: Proxy (2^k) -> Proxy (2^k)
-proxyFun6 = const Proxy
-
-testProxy6 :: Proxy 7
-testProxy6 = proxyFun6 (Proxy :: Proxy 7)
-
-testProxy6Errors =
-#if __GLASGOW_HASKELL__ >= 902
-  ["Expected: Proxy 7"
-  ,"  Actual: Proxy (2 ^ k0)"
-  ]
-#elif __GLASGOW_HASKELL__ >= 900
-  ["Expected: Proxy (2 ^ k0)"
-  ,"  Actual: Proxy 7"
-  ]
-#else
-  ["Expected type: Proxy (2 ^ k0)"
-  ,"Actual type: Proxy 7"
-  ]
-#endif
-
-proxyFun7 :: Proxy (2^k) -> Proxy k
-proxyFun7 = const Proxy
-
-testProxy8 :: Proxy x -> Proxy (y + x)
-testProxy8 = id
-
-testProxy8Errors =
-#if __GLASGOW_HASKELL__ >= 914
-  ["Expected: Proxy (y + x)"
-  ,"  Actual: Proxy x"
-  ]
-#elif __GLASGOW_HASKELL__ >= 900
-  ["Expected: Proxy x -> Proxy (y + x)"
-  ,"  Actual: Proxy x -> Proxy x"
-  ]
-#else
-  ["Expected type: Proxy x -> Proxy (y + x)"
-  ,"Actual type: Proxy x -> Proxy x"
-  ]
-#endif
-
-#if __GLASGOW_HASKELL__ >= 904
-proxyInEq :: ((a <= b) ~ (() :: Constraint)) => Proxy (a :: Nat) -> Proxy b -> ()
-#else
-proxyInEq :: (a <= b) => Proxy (a :: Nat) -> Proxy b -> ()
-#endif
-proxyInEq _ _ = ()
-
-proxyInEq' :: ((a <=? b) ~ 'False) => Proxy (a :: Nat) -> Proxy b -> ()
-proxyInEq' _ _ = ()
-
-testProxy9 :: Proxy (a + 1) -> Proxy a -> ()
-testProxy9 = proxyInEq
-
-testProxy9Errors =
-#if __GLASGOW_HASKELL__ >= 904
-  ["Cannot satisfy: a + 1 <= a"]
-#elif __GLASGOW_HASKELL__ >= 902
-  [$(do localeEncoding <- runIO (getLocaleEncoding)
-        if textEncodingName localeEncoding == textEncodingName utf8
-          then litE $ stringL "Couldn't match type ‘Data.Type.Ord.OrdCond"
-          else litE $ stringL "Couldn't match type `Data.Type.Ord.OrdCond"
-    )
-  ,$(do localeEncoding <- runIO (getLocaleEncoding)
-        if textEncodingName localeEncoding == textEncodingName utf8
-          then litE $ stringL "(CmpNat (a + 1) a) 'True 'True 'False’"
-          else litE $ stringL "(CmpNat (a + 1) a) 'True 'True 'False'"
-    )
-  ,$(do localeEncoding <- runIO (getLocaleEncoding)
-        if textEncodingName localeEncoding == textEncodingName utf8
-          then litE $ stringL "with ‘'True’"
-          else litE $ stringL "with 'True"
-    )
-  ]
-#else
-  [$(do localeEncoding <- runIO (getLocaleEncoding)
-        if textEncodingName localeEncoding == textEncodingName utf8
-          then litE $ stringL "Couldn't match type ‘(a + 1) <=? a’ with ‘'True’"
-          else litE $ stringL "Couldn't match type `(a + 1) <=? a' with 'True"
-    )]
-#endif
-
-testProxy10 :: Proxy (a :: Nat) -> Proxy (a + 2) -> ()
-testProxy10 = proxyInEq'
-
-testProxy10Errors =
-#if __GLASGOW_HASKELL__ >= 910
-  [$(do localeEncoding <- runIO (getLocaleEncoding)
-        if textEncodingName localeEncoding == textEncodingName utf8
-          then litE $ stringL "Couldn't match type ‘Data.Type.Ord.OrdCond"
-          else litE $ stringL "Couldn't match type `Data.Type.Ord.OrdCond"
-    )
-  ,$(do localeEncoding <- runIO (getLocaleEncoding)
-        if textEncodingName localeEncoding == textEncodingName utf8
-          then litE $ stringL "(CmpNat a (a + 2)) True True False’"
-          else litE $ stringL "(CmpNat a (a + 2)) True True False'"
-    )
-  ,$(do localeEncoding <- runIO (getLocaleEncoding)
-        if textEncodingName localeEncoding == textEncodingName utf8
-          then litE $ stringL "with ‘False"
-          else litE $ stringL "with `False"
-    )
-  ]
-#elif __GLASGOW_HASKELL__ >= 906
-  [$(do localeEncoding <- runIO (getLocaleEncoding)
-        if textEncodingName localeEncoding == textEncodingName utf8
-          then litE $ stringL "Couldn't match type ‘Data.Type.Ord.OrdCond"
-          else litE $ stringL "Couldn't match type `Data.Type.Ord.OrdCond"
-    )
-  ,$(do localeEncoding <- runIO (getLocaleEncoding)
-        if textEncodingName localeEncoding == textEncodingName utf8
-          then litE $ stringL "(CmpNat a (a + 2)) True True False’"
-          else litE $ stringL "(CmpNat a (a + 2)) True True False'"
-    )
-  ,$(do localeEncoding <- runIO (getLocaleEncoding)
-        if textEncodingName localeEncoding == textEncodingName utf8
-          then litE $ stringL "with ‘False"
-          else litE $ stringL "with False"
-    )
-  ]
-#elif __GLASGOW_HASKELL__ >= 902
-  [$(do localeEncoding <- runIO (getLocaleEncoding)
-        if textEncodingName localeEncoding == textEncodingName utf8
-          then litE $ stringL "Couldn't match type ‘Data.Type.Ord.OrdCond"
-          else litE $ stringL "Couldn't match type `Data.Type.Ord.OrdCond"
-    )
-  ,$(do localeEncoding <- runIO (getLocaleEncoding)
-        if textEncodingName localeEncoding == textEncodingName utf8
-          then litE $ stringL "(CmpNat a (a + 2)) 'True 'True 'False’"
-          else litE $ stringL "(CmpNat a (a + 2)) 'True 'True 'False'"
-    )
-  ,$(do localeEncoding <- runIO (getLocaleEncoding)
-        if textEncodingName localeEncoding == textEncodingName utf8
-          then litE $ stringL "with ‘'False"
-          else litE $ stringL "with 'False"
-    )
-  ]
-#else
-  [$(do localeEncoding <- runIO (getLocaleEncoding)
-        if textEncodingName localeEncoding == textEncodingName utf8
-          then litE $ stringL "Couldn't match type ‘a <=? (a + 2)’ with ‘'False’"
-          else litE $ stringL "Couldn't match type `a <=? (a + 2)' with 'False"
-    )]
-#endif
-
-testProxy11 :: Proxy (a :: Nat) -> Proxy a -> ()
-testProxy11 = proxyInEq'
-
-testProxy11Errors =
-  [$(do localeEncoding <- runIO (getLocaleEncoding)
-        if textEncodingName localeEncoding == textEncodingName utf8
-#if __GLASGOW_HASKELL__ >= 910
-          then litE $ stringL "Couldn't match type ‘True’ with ‘False’"
-          else litE $ stringL "Couldn't match type `True' with `False'"
-#elif __GLASGOW_HASKELL__ >= 906
-          then litE $ stringL "Couldn't match type ‘True’ with ‘False’"
-          else litE $ stringL "Couldn't match type True with False"
-#else
-          then litE $ stringL "Couldn't match type ‘'True’ with ‘'False’"
-          else litE $ stringL "Couldn't match type 'True with 'False"
-#endif
-    )]
-
-testProxy12 :: Proxy (a + b) -> Proxy (a + c) -> ()
-testProxy12 = proxyInEq
-
-testProxy12Errors =
-#if __GLASGOW_HASKELL__ >= 904
-  ["Cannot satisfy: a + b <= a + c"]
-#elif __GLASGOW_HASKELL__ >= 902
-  [$(do localeEncoding <- runIO (getLocaleEncoding)
-        if textEncodingName localeEncoding == textEncodingName utf8
-          then litE $ stringL "Couldn't match type ‘Data.Type.Ord.OrdCond"
-          else litE $ stringL "Couldn't match type `Data.Type.Ord.OrdCond"
-    )
-  ,$(do localeEncoding <- runIO (getLocaleEncoding)
-        if textEncodingName localeEncoding == textEncodingName utf8
-          then litE $ stringL "(CmpNat (a + b) (a + c)) 'True 'True 'False’"
-          else litE $ stringL "(CmpNat (a + b) (a + c)) 'True 'True 'False'"
-    )
-  ,$(do localeEncoding <- runIO (getLocaleEncoding)
-        if textEncodingName localeEncoding == textEncodingName utf8
-          then litE $ stringL "with ‘'True’"
-          else litE $ stringL "with 'True"
-    )
-  ]
-#else
-  [$(do localeEncoding <- runIO (getLocaleEncoding)
-        if textEncodingName localeEncoding == textEncodingName utf8
-          then litE $ stringL "Couldn't match type ‘(a + b) <=? (a + c)’ with ‘'True’"
-          else litE $ stringL "Couldn't match type `(a + b) <=? (a + c)' with 'True"
-    )]
-#endif
-
-testProxy13 :: Proxy (4*a) -> Proxy (2*a) ->()
-testProxy13 = proxyInEq
-
-testProxy13Errors =
-#if __GLASGOW_HASKELL__ >= 904
-  ["Cannot satisfy: 4 * a <= 2 * a"]
-#elif __GLASGOW_HASKELL__ >= 902
-  [$(do localeEncoding <- runIO (getLocaleEncoding)
-        if textEncodingName localeEncoding == textEncodingName utf8
-          then litE $ stringL "Couldn't match type ‘Data.Type.Ord.OrdCond"
-          else litE $ stringL "Couldn't match type `Data.Type.Ord.OrdCond"
-    )
-  ,$(do localeEncoding <- runIO (getLocaleEncoding)
-        if textEncodingName localeEncoding == textEncodingName utf8
-          then litE $ stringL "(CmpNat (4 * a) (2 * a)) 'True 'True 'False’"
-          else litE $ stringL "(CmpNat (4 * a) (2 * a)) 'True 'True 'False'"
-    )
-  ,$(do localeEncoding <- runIO (getLocaleEncoding)
-        if textEncodingName localeEncoding == textEncodingName utf8
-          then litE $ stringL "with ‘'True’"
-          else litE $ stringL "with 'True"
-    )
-  ]
-#else
-  [$(do localeEncoding <- runIO (getLocaleEncoding)
-        if textEncodingName localeEncoding == textEncodingName utf8
-          then litE $ stringL "Couldn't match type ‘(4 * a) <=? (2 * a)’ with ‘'True’"
-          else litE $ stringL "Couldn't match type `(4 * a) <=? (2 * a)' with 'True"
-    )]
-#endif
-
-testProxy14 :: Proxy (2*a) -> Proxy (4*a) -> ()
-testProxy14 = proxyInEq'
-
-testProxy14Errors =
-#if __GLASGOW_HASKELL__ >= 910
-  [$(do localeEncoding <- runIO (getLocaleEncoding)
-        if textEncodingName localeEncoding == textEncodingName utf8
-          then litE $ stringL "Couldn't match type ‘Data.Type.Ord.OrdCond"
-          else litE $ stringL "Couldn't match type `Data.Type.Ord.OrdCond"
-    )
-  ,$(do localeEncoding <- runIO (getLocaleEncoding)
-        if textEncodingName localeEncoding == textEncodingName utf8
-          then litE $ stringL "(CmpNat (2 * a) (4 * a)) True True False’"
-          else litE $ stringL "(CmpNat (2 * a) (4 * a)) True True False'"
-    )
-  ,$(do localeEncoding <- runIO (getLocaleEncoding)
-        if textEncodingName localeEncoding == textEncodingName utf8
-          then litE $ stringL "with ‘False"
-          else litE $ stringL "with `False"
-    )
-  ]
-#elif __GLASGOW_HASKELL__ >= 906
-  [$(do localeEncoding <- runIO (getLocaleEncoding)
-        if textEncodingName localeEncoding == textEncodingName utf8
-          then litE $ stringL "Couldn't match type ‘Data.Type.Ord.OrdCond"
-          else litE $ stringL "Couldn't match type `Data.Type.Ord.OrdCond"
-    )
-  ,$(do localeEncoding <- runIO (getLocaleEncoding)
-        if textEncodingName localeEncoding == textEncodingName utf8
-          then litE $ stringL "(CmpNat (2 * a) (4 * a)) True True False’"
-          else litE $ stringL "(CmpNat (2 * a) (4 * a)) True True False'"
-    )
-  ,$(do localeEncoding <- runIO (getLocaleEncoding)
-        if textEncodingName localeEncoding == textEncodingName utf8
-          then litE $ stringL "with ‘False"
-          else litE $ stringL "with False"
-    )
-  ]
-#elif __GLASGOW_HASKELL__ >= 902
-  [$(do localeEncoding <- runIO (getLocaleEncoding)
-        if textEncodingName localeEncoding == textEncodingName utf8
-          then litE $ stringL "Couldn't match type ‘Data.Type.Ord.OrdCond"
-          else litE $ stringL "Couldn't match type `Data.Type.Ord.OrdCond"
-    )
-  ,$(do localeEncoding <- runIO (getLocaleEncoding)
-        if textEncodingName localeEncoding == textEncodingName utf8
-          then litE $ stringL "(CmpNat (2 * a) (4 * a)) 'True 'True 'False’"
-          else litE $ stringL "(CmpNat (2 * a) (4 * a)) 'True 'True 'False'"
-    )
-  ,$(do localeEncoding <- runIO (getLocaleEncoding)
-        if textEncodingName localeEncoding == textEncodingName utf8
-          then litE $ stringL "with ‘'False"
-          else litE $ stringL "with 'False"
-    )
-  ]
-#else
-  [$(do localeEncoding <- runIO (getLocaleEncoding)
-        if textEncodingName localeEncoding == textEncodingName utf8
-          then litE $ stringL "Couldn't match type ‘(2 * a) <=? (4 * a)’ with ‘'False’"
-          else litE $ stringL "Couldn't match type `(2 * a) <=? (4 * a)' with 'False"
-    )]
-#endif
-
-type family CLog (b :: Nat) (x :: Nat) :: Nat
-type instance CLog 2 2 = 1
-
-testProxy15 :: (CLog 2 (2 ^ n) ~ n, (1 <=? n) ~ True) => Proxy n -> Proxy (n+d)
-testProxy15 = id
-
-testProxy15Errors =
-#if __GLASGOW_HASKELL__ >= 914
-  ["Expected: Proxy (n + d)"
-  ,"  Actual: Proxy n"
-  ]
-#elif __GLASGOW_HASKELL__ >= 900
-  ["Expected: Proxy n -> Proxy (n + d)"
-  ,"  Actual: Proxy n -> Proxy n"
-  ]
-#else
-  ["Expected type: Proxy n -> Proxy (n + d)"
-  ,"Actual type: Proxy n -> Proxy n"
-  ]
-#endif
-
-data Fin (n :: Nat) where
-  FZ :: Fin (n + 1)
-  FS :: Fin n -> Fin (n + 1)
-
-test16 :: forall n . Integer -> Fin n
-test16 n = case n of
-  0 -> FZ
-  x -> FS (test16 @(n-1) (x-1))
-
-test16Errors =
-#if __GLASGOW_HASKELL__ >= 904
-  ["Cannot satisfy: 1 <= n"]
-#elif __GLASGOW_HASKELL__ >= 902
-  [$(do localeEncoding <- runIO (getLocaleEncoding)
-        if textEncodingName localeEncoding == textEncodingName utf8
-          then litE $ stringL "Couldn't match type ‘Data.Type.Ord.OrdCond"
-          else litE $ stringL "Couldn't match type `Data.Type.Ord.OrdCond"
-    )
-  ,$(do localeEncoding <- runIO (getLocaleEncoding)
-        if textEncodingName localeEncoding == textEncodingName utf8
-          then litE $ stringL "(CmpNat 1 n) 'True 'True 'False’"
-          else litE $ stringL "(CmpNat 1 n) 'True 'True 'False'"
-    )
-  ,$(do localeEncoding <- runIO (getLocaleEncoding)
-        if textEncodingName localeEncoding == textEncodingName utf8
-          then litE $ stringL "with ‘'True’"
-          else litE $ stringL "with 'True"
-    )
-  ]
-#else
-  [$(do localeEncoding <- runIO (getLocaleEncoding)
-        if textEncodingName localeEncoding == textEncodingName utf8
-          then litE $ stringL "Couldn't match type ‘1 <=? n’ with ‘'True’"
-          else litE $ stringL "Couldn't match type `1 <=? n' with 'True"
-    )]
-#endif
-
-data Dict c where
-  Dict :: c => Dict c
-deriving instance Show (Dict c)
-data Boo (n :: Nat) = Boo
-
-test17 :: Show (Boo n) => Proxy n -> Boo (n - 1 + 1) -> String
-test17 = const show
-
-testProxy17 :: String
-
-testProxy17 = test17 (Proxy :: Proxy 17) Boo
-test17Errors = test16Errors
-
-#if __GLASGOW_HASKELL__ >= 904
-test19f :: ((1 <= n) ~ (() :: Constraint))
-#else
-test19f :: (1 <= n)
-#endif
-  => Proxy n -> Proxy n
-test19f = id
-
-testProxy19 :: (1 <= m, m <= rp)
-  => Proxy m
-  -> Proxy rp
-  -> Proxy (rp - m)
-  -> Proxy (rp - m)
-testProxy19 _ _ = test19f
-
-test19Errors =
-#if __GLASGOW_HASKELL__ >= 904
-  [ "Cannot satisfy: 1 <= rp - m" ]
-#elif __GLASGOW_HASKELL__ >= 902
-  [ "Could not deduce: Data.Type.Ord.OrdCond"
-  , "(CmpNat 1 (rp - m)) 'True 'True 'False"
-  , "~ 'True"
-  ]
-#else
-  ["Could not deduce: (1 <=? (rp - m)) ~ 'True"]
-#endif
-
-testProxy20 :: Proxy 1 -> Proxy (m ^ 2) -> ()
-testProxy20 = proxyInEq
-
-testProxy20Errors =
-#if __GLASGOW_HASKELL__ >= 904
-  ["Cannot satisfy: 1 <= m ^ 2"]
-#elif __GLASGOW_HASKELL__ >= 902
-  [$(do localeEncoding <- runIO (getLocaleEncoding)
-        if textEncodingName localeEncoding == textEncodingName utf8
-          then litE $ stringL "Couldn't match type ‘Data.Type.Ord.OrdCond"
-          else litE $ stringL "Couldn't match type `Data.Type.Ord.OrdCond"
-    )
-  ,$(do localeEncoding <- runIO (getLocaleEncoding)
-        if textEncodingName localeEncoding == textEncodingName utf8
-          then litE $ stringL "(CmpNat 1 (m ^ 2)) 'True 'True 'False’"
-          else litE $ stringL "(CmpNat 1 (m ^ 2)) 'True 'True 'False'"
-    )
-  ,$(do localeEncoding <- runIO (getLocaleEncoding)
-        if textEncodingName localeEncoding == textEncodingName utf8
-          then litE $ stringL "with ‘'True’"
-          else litE $ stringL "with 'True"
-    )
-  ]
-#else
-  [$(do localeEncoding <- runIO (getLocaleEncoding)
-        if textEncodingName localeEncoding == textEncodingName utf8
-          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
-
-t113 :: Proxy a -> Proxy b -> Proxy ((2 * a) + b) -> Proxy 5
-t113 _ _ = id
-
-t113_errors =
-#if __GLASGOW_HASKELL__ >= 914
-  ["Expected: Proxy 5"
-  ,"  Actual: Proxy ((2 * a) + b)"
-  ]
-#elif __GLASGOW_HASKELL__ >= 900
-  ["Expected: Proxy ((2 * a) + b) -> Proxy 5"
-  ,"  Actual: Proxy 5 -> Proxy 5"
-  ]
-#else
-  ["Expected type: Proxy ((2 * a) + b) -> Proxy 5"
-  ,"Actual type: Proxy 5 -> Proxy 5"
-  ]
-#endif
diff --git a/tests/ShouldError.hs b/tests/ShouldError.hs
new file mode 100644
--- /dev/null
+++ b/tests/ShouldError.hs
@@ -0,0 +1,597 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE QuasiQuotes #-}
+
+module ShouldError (tests) where
+
+import Data.String.Interpolate (i)
+import ShouldError.Tasty (assertCompileError)
+import Test.Tasty (TestTree, testGroup)
+import Test.Tasty.HUnit (testCase)
+
+tests :: TestTree
+tests = testGroup "ShouldError"
+    [ test1
+    , test2
+    , test3
+    , test4
+    , test5
+    , test6
+    , test7
+    , test8
+    , test9
+    , test10
+    , test11
+    , testIssue126
+    , inequalityTests
+    ]
+
+preamble :: String
+preamble = [i|
+import Data.Kind (Constraint)
+import Data.Proxy
+import GHC.TypeLits
+|] <> "\n"
+
+source1 :: String
+source1 = preamble <> [i|
+test :: Proxy (x + 1) -> Proxy (2 + x)
+test = id
+|]
+
+expected1 :: [String]
+expected1 =
+#if __GLASGOW_HASKELL__ >= 914
+  ["Expected: Proxy (2 + x)"
+  ,"  Actual: Proxy (x + 1)"
+  ]
+#elif __GLASGOW_HASKELL__ >= 900
+  ["Expected: Proxy (x + 1) -> Proxy (2 + x)"
+  ,"  Actual: Proxy (x + 1) -> Proxy (x + 1)"
+  ]
+#else
+  ["Expected type: Proxy (x + 1) -> Proxy (2 + x)"
+  ,"Actual type: Proxy (2 + x) -> Proxy (2 + x)"
+  ]
+#endif
+
+test1 :: TestTree
+test1 = testCase "x + 1 /~ 2 + x" $ assertCompileError source1 expected1
+
+source2 :: String
+source2 = preamble <> [i|
+type family GCD (x :: Nat) (y :: Nat) :: Nat
+type instance GCD 6 8 = 2
+type instance GCD 9 6 = 3
+
+test :: Proxy (GCD 6 8 + x) -> Proxy (x + GCD 9 6)
+test = id
+|]
+
+expected2 :: [String]
+expected2 =
+#if __GLASGOW_HASKELL__ >= 914
+  ["Expected: Proxy (x + GCD 9 6)"
+  ,"  Actual: Proxy (2 + x)"
+  ]
+#elif __GLASGOW_HASKELL__ >= 900
+  ["Expected: Proxy (GCD 6 8 + x) -> Proxy (x + GCD 9 6)"
+  ,"  Actual: Proxy (2 + x) -> Proxy (2 + x)"
+  ]
+#else
+  ["Expected type: Proxy (GCD 6 8 + x) -> Proxy (x + GCD 9 6)"
+  ,"Actual type: Proxy (x + 3) -> Proxy (x + 3)"
+  ]
+#endif
+
+test2 :: TestTree
+test2 = testCase "GCD 6 8 + x /~ x + GCD 9 6" $ assertCompileError source2 expected2
+
+source3 :: String
+source3 = preamble <> [i|
+proxyFun :: Proxy (x + x + x) -> ()
+proxyFun = const ()
+
+test :: Proxy 8 -> ()
+test = proxyFun
+|]
+
+expected3 :: [String]
+expected3 =
+#if __GLASGOW_HASKELL__ >= 914
+  ["Expected: Proxy ((x0 + x0) + x0)"
+  ,"  Actual: Proxy 8"
+  ]
+#elif __GLASGOW_HASKELL__ >= 900
+  ["Expected: Proxy 8 -> ()"
+  ,"  Actual: Proxy ((x0 + x0) + x0) -> ()"
+  ]
+#else
+  ["Expected type: Proxy 8 -> ()"
+  ,"Actual type: Proxy ((x0 + x0) + x0) -> ()"
+  ]
+#endif
+
+test3 :: TestTree
+test3 = testCase "Unify \"x + x + x\" with \"8\"" $ assertCompileError source3 expected3
+
+source4 :: String
+source4 = preamble <> [i|
+proxyFun :: Proxy ((2*y)+4) -> ()
+proxyFun = const ()
+
+test :: Proxy 2 -> ()
+test = proxyFun
+|]
+
+expected4 :: [String]
+expected4 =
+#if __GLASGOW_HASKELL__ >= 914
+  ["Expected: Proxy ((2 * y0) + 4)"
+  ,"  Actual: Proxy 2"
+  ]
+#elif __GLASGOW_HASKELL__ >= 900
+  ["Expected: Proxy 2 -> ()"
+  ,"  Actual: Proxy ((2 * y0) + 4) -> ()"
+  ]
+#else
+  ["Expected type: Proxy 2 -> ()"
+  ,"Actual type: Proxy ((2 * y0) + 4) -> ()"
+  ]
+#endif
+
+test4 :: TestTree
+test4 = testCase "Unify \"(2*x)+4\" with \"2\"" $ assertCompileError source4 expected4
+
+source5 :: String
+source5 = preamble <> [i|
+proxyFun :: Proxy ((2*y)+4) -> ()
+proxyFun = const ()
+
+test :: Proxy 7 -> ()
+test = proxyFun
+|]
+
+expected5 :: [String]
+expected5 =
+#if __GLASGOW_HASKELL__ >= 914
+  ["Expected: Proxy ((2 * y"
+  ,"Actual: Proxy 7"
+  ]
+#elif __GLASGOW_HASKELL__ >= 900
+  ["Expected: Proxy 7 -> ()"
+  ,"Actual: Proxy ((2 * y"
+  ]
+#else
+  ["Expected type: Proxy 7 -> ()"
+  ,"Actual type: Proxy ((2 * y"
+  ]
+#endif
+
+test5 :: TestTree
+test5 = testCase "Unify \"(2*x)+4\" with \"7\"" $ assertCompileError source5 expected5
+
+source6 :: String
+source6 = preamble <> [i|
+proxyFun :: Proxy (2^k) -> Proxy (2^k)
+proxyFun = const Proxy
+
+test :: Proxy 7
+test = proxyFun (Proxy :: Proxy 7)
+|]
+
+expected6 :: [String]
+expected6 =
+#if __GLASGOW_HASKELL__ >= 902
+  ["Expected: Proxy 7"
+  ,"  Actual: Proxy (2 ^ k0)"
+  ]
+#elif __GLASGOW_HASKELL__ >= 900
+  ["Expected: Proxy (2 ^ k0)"
+  ,"  Actual: Proxy 7"
+  ]
+#else
+  ["Expected type: Proxy (2 ^ k0)"
+  ,"Actual type: Proxy 7"
+  ]
+#endif
+
+test6 :: TestTree
+test6 = testCase "Unify \"2^k\" with \"7\"" $ assertCompileError source6 expected6
+
+source7 :: String
+source7 = preamble <> [i|
+test :: Proxy x -> Proxy (y + x)
+test = id
+|]
+
+expected7 :: [String]
+expected7 =
+#if __GLASGOW_HASKELL__ >= 914
+  ["Expected: Proxy (y + x)"
+  ,"  Actual: Proxy x"
+  ]
+#elif __GLASGOW_HASKELL__ >= 900
+  ["Expected: Proxy x -> Proxy (y + x)"
+  ,"  Actual: Proxy x -> Proxy x"
+  ]
+#else
+  ["Expected type: Proxy x -> Proxy (y + x)"
+  ,"Actual type: Proxy x -> Proxy x"
+  ]
+#endif
+
+test7 :: TestTree
+test7 = testCase "x /~ y + x" $ assertCompileError source7 expected7
+
+source8 :: String
+source8 = preamble <> [i|
+type family CLog (b :: Nat) (x :: Nat) :: Nat
+type instance CLog 2 2 = 1
+
+test :: (CLog 2 (2 ^ n) ~ n, (1 <=? n) ~ True) => Proxy n -> Proxy (n+d)
+test = id
+|]
+
+expected8 :: [String]
+expected8 =
+#if __GLASGOW_HASKELL__ >= 914
+  ["Expected: Proxy (n + d)"
+  ,"  Actual: Proxy n"
+  ]
+#elif __GLASGOW_HASKELL__ >= 900
+  ["Expected: Proxy n -> Proxy (n + d)"
+  ,"  Actual: Proxy n -> Proxy n"
+  ]
+#else
+  ["Expected type: Proxy n -> Proxy (n + d)"
+  ,"Actual type: Proxy n -> Proxy n"
+  ]
+#endif
+
+test8 :: TestTree
+test8 = testCase "(CLog 2 (2 ^ n) ~ n, (1 <=? n) ~ True) => n /~ n + d" $
+  assertCompileError source8 expected8
+
+source9 :: String
+source9 = preamble <> [i|
+data Fin (n :: Nat) where
+  FZ :: Fin (n + 1)
+  FS :: Fin n -> Fin (n + 1)
+
+test :: forall n . Integer -> Fin n
+test n = case n of
+  0 -> FZ
+  x -> FS (test @(n-1) (x-1))
+|]
+
+expected9 :: [String]
+expected9 =
+#if __GLASGOW_HASKELL__ >= 904
+  ["Cannot satisfy: 1 <= n"]
+#elif __GLASGOW_HASKELL__ >= 902
+  [ "Couldn't match type Data.Type.Ord.OrdCond"
+  , "(CmpNat 1 n) True True False"
+  , "with True"
+  ]
+#else
+  [ "Couldn't match type 1 <=? n with True" ]
+#endif
+
+test9 :: TestTree
+test9 = testCase "(n - 1) + 1 ~ n implies (1 <= n)" $ assertCompileError source9 expected9
+
+source10 :: String
+source10 = preamble <> [i|
+type family Drop (n :: Nat) (xs :: [Nat]) :: [Nat] where
+  Drop 0 xs = xs
+  Drop n (x ': xs) = Drop (n-1) xs
+  Drop n '[] = '[]
+
+test :: Proxy ns -> Proxy (Drop 1 ns) -> Proxy (Drop 2 ns)
+test _ px = px
+|]
+
+expected10 :: [String]
+expected10 =
+#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)"
+  , "Drop is a non-injective type family"
+  ]
+#else
+  [ "Couldn't match type Drop 1 ns with Drop 2 ns"
+  , "Expected type: Proxy (Drop 2 ns)"
+  , "  Actual type: Proxy (Drop 1 ns)"
+  , "Drop is a non-injective type family"
+  ]
+#endif
+
+test10 :: TestTree
+test10 = testCase "Do not unify in non-injective positions" $ assertCompileError source10 expected10
+
+source11 :: String
+source11 = preamble <> [i|
+test :: Proxy a -> Proxy b -> Proxy ((2 * a) + b) -> Proxy 5
+test _ _ = id
+|]
+
+expected11 :: [String]
+expected11 =
+#if __GLASGOW_HASKELL__ >= 914
+  ["Expected: Proxy 5"
+  ,"  Actual: Proxy ((2 * a) + b)"
+  ]
+#elif __GLASGOW_HASKELL__ >= 900
+  ["Expected: Proxy ((2 * a) + b) -> Proxy 5"
+  ,"  Actual: Proxy 5 -> Proxy 5"
+  ]
+#else
+  ["Expected type: Proxy ((2 * a) + b) -> Proxy 5"
+  ,"Actual type: Proxy 5 -> Proxy 5"
+  ]
+#endif
+
+test11 :: TestTree
+test11 = testCase "Do not rewrite constraint to itself" $ assertCompileError source11 expected11
+
+-- ((3 * (n - 1)) + 1) simplifies to (3 * n - 2), so
+-- the equality would require b0 ~ -2, which is impossible at kind Nat.
+sourceIssue126 :: String
+sourceIssue126 = preamble <> [i|
+data Index (n :: Nat) = Index
+
+truncateB :: Index (a + b) -> Index a
+truncateB = undefined
+
+mul :: Index 4 -> Index n -> Index ((3 * (n - 1)) + 1)
+mul _ _ = Index
+
+zeroExtendTimesThree :: (1 <= n) => Index n -> Index (n * 3)
+zeroExtendTimesThree = truncateB . (mul Index)
+|]
+
+expectedIssue126 :: [String]
+expectedIssue126 =
+#if __GLASGOW_HASKELL__ >= 906
+  [ "Could not deduce ((n * 3) + b0) ~ ((3 * (n - 1)) + 1)"
+#elif __GLASGOW_HASKELL__ >= 904
+  [ "Could not deduce (((n * 3) + b0) ~ ((3 * (n - 1)) + 1))"
+#elif __GLASGOW_HASKELL__ >= 902
+  [ "Could not deduce: ((n * 3) + b0) ~ ((3 * (n - 1)) + 1)"
+#else
+  [ "Could not deduce: ((3 * (n - 1)) + 1) ~ ((n * 3) + b0)"
+#endif
+  , "from the context: 1 <= n"
+  ]
+
+
+
+testIssue126 :: TestTree
+testIssue126 =
+  testCase "Issue 126 regression reproducer" $
+    assertCompileError sourceIssue126 expectedIssue126
+
+proxyInEqDef :: String
+proxyInEqDef =
+#if __GLASGOW_HASKELL__ >= 904
+  [i|
+proxyInEq :: ((a <= b) ~ (() :: Constraint)) => Proxy (a :: Nat) -> Proxy b -> ()
+proxyInEq _ _ = ()
+|]
+#else
+  [i|
+proxyInEq :: (a <= b) => Proxy (a :: Nat) -> Proxy b -> ()
+proxyInEq _ _ = ()
+|]
+#endif
+
+proxyInEq'Def :: String
+proxyInEq'Def = [i|
+proxyInEq' :: ((a <=? b) ~ 'False) => Proxy (a :: Nat) -> Proxy b -> ()
+proxyInEq' _ _ = ()
+|]
+
+source12 :: String
+source12 = preamble <> proxyInEqDef <> proxyInEq'Def <> [i|
+test :: Proxy (a + 1) -> Proxy a -> ()
+test = proxyInEq
+|]
+
+expected12 :: [String]
+expected12 =
+#if __GLASGOW_HASKELL__ >= 904
+  ["Cannot satisfy: a + 1 <= a"]
+#elif __GLASGOW_HASKELL__ >= 902
+  [ "Couldn't match type Data.Type.Ord.OrdCond"
+  , "(CmpNat (a + 1) a) True True False"
+  , "with True"
+  ]
+#else
+  [ "Couldn't match type (a + 1) <=? a with True" ]
+#endif
+
+test12 :: TestTree
+test12 = testCase "a+1 <= a" $ assertCompileError source12 expected12
+
+source13 :: String
+source13 = preamble <> proxyInEqDef <> proxyInEq'Def <> [i|
+test :: Proxy (a :: Nat) -> Proxy (a + 2) -> ()
+test = proxyInEq'
+|]
+
+expected13 :: [String]
+expected13 =
+#if __GLASGOW_HASKELL__ >= 902
+  [ "Data.Type.Ord.OrdCond"
+  , "(CmpNat a (a + 2)) True True False"
+  , "with False"
+  ]
+#else
+  [ "Couldn't match type a <=? (a + 2) with False" ]
+#endif
+
+test13 :: TestTree
+test13 = testCase "(a <=? a+1) ~ False" $ assertCompileError source13 expected13
+
+source14 :: String
+source14 = preamble <> proxyInEqDef <> proxyInEq'Def <> [i|
+test :: Proxy (a :: Nat) -> Proxy a -> ()
+test = proxyInEq'
+|]
+
+expected14 :: [String]
+expected14 = [ "Couldn't match type True with False" ]
+
+test14 :: TestTree
+test14 = testCase "(a <=? a) ~ False" $ assertCompileError source14 expected14
+
+source15 :: String
+source15 = preamble <> proxyInEqDef <> proxyInEq'Def <> [i|
+test :: Proxy (a + b) -> Proxy (a + c) -> ()
+test = proxyInEq
+|]
+
+expected15 :: [String]
+expected15 =
+#if __GLASGOW_HASKELL__ >= 904
+  ["Cannot satisfy: a + b <= a + c"]
+#elif __GLASGOW_HASKELL__ >= 902
+  [ "Couldn't match type Data.Type.Ord.OrdCond"
+  , "(CmpNat (a + b) (a + c)) True True False"
+  , "with True"
+  ]
+#else
+  [ "Couldn't match type (a + b) <=? (a + c) with True" ]
+#endif
+
+test15 :: TestTree
+test15 = testCase "() => (a+b <= a+c)" $ assertCompileError source15 expected15
+
+source16 :: String
+source16 = preamble <> proxyInEqDef <> proxyInEq'Def <> [i|
+test :: Proxy (4*a) -> Proxy (2*a) -> ()
+test = proxyInEq
+|]
+
+expected16 :: [String]
+expected16 =
+#if __GLASGOW_HASKELL__ >= 904
+  ["Cannot satisfy: 4 * a <= 2 * a"]
+#elif __GLASGOW_HASKELL__ >= 902
+  [ "Couldn't match type Data.Type.Ord.OrdCond"
+  , "(CmpNat (4 * a) (2 * a)) True True False"
+  , "with True"
+  ]
+#else
+  [ "Couldn't match type (4 * a) <=? (2 * a) with True" ]
+#endif
+
+test16 :: TestTree
+test16 = testCase "4a <= 2a" $ assertCompileError source16 expected16
+
+source17 :: String
+source17 = preamble <> proxyInEqDef <> proxyInEq'Def <> [i|
+test :: Proxy (2*a) -> Proxy (4*a) -> ()
+test = proxyInEq'
+|]
+
+expected17 :: [String]
+expected17 =
+#if __GLASGOW_HASKELL__ >= 902
+  [ "Data.Type.Ord.OrdCond"
+  , "(CmpNat (2 * a) (4 * a)) True True False"
+  , "with False"
+  ]
+#else
+  [ "Couldn't match type (2 * a) <=? (4 * a) with False" ]
+#endif
+
+test17 :: TestTree
+test17 = testCase "2a <=? 4a ~ False" $ assertCompileError source17 expected17
+
+source18 :: String
+source18 = preamble <> [i|
+data Boo (n :: Nat) = Boo
+
+test :: Show (Boo n) => Proxy n -> Boo (n - 1 + 1) -> String
+test = const show
+|]
+
+expected18 :: [String]
+expected18 = expected9
+
+test18 :: TestTree
+test18 = testCase "Show (Boo n) => Show (Boo (n - 1 + 1))" $ assertCompileError source18 expected18
+
+test19fDef :: String
+test19fDef =
+#if __GLASGOW_HASKELL__ >= 904
+  [i|
+test19f :: ((1 <= n) ~ (() :: Constraint)) => Proxy n -> Proxy n
+test19f = id
+|]
+#else
+  [i|
+test19f :: (1 <= n) => Proxy n -> Proxy n
+test19f = id
+|]
+#endif
+
+source19 :: String
+source19 = preamble <> test19fDef <> [i|
+test :: (1 <= m, m <= rp) => Proxy m -> Proxy rp -> Proxy (rp - m) -> Proxy (rp - m)
+test _ _ = test19f
+|]
+
+expected19 :: [String]
+expected19 =
+#if __GLASGOW_HASKELL__ >= 904
+  [ "Cannot satisfy: 1 <= rp - m" ]
+#elif __GLASGOW_HASKELL__ >= 902
+  [ "Could not deduce: Data.Type.Ord.OrdCond"
+  , "(CmpNat 1 (rp - m)) True True False"
+  , "~ True"
+  ]
+#else
+  [ "Could not deduce: (1 <=? (rp - m)) ~ True" ]
+#endif
+
+test19 :: TestTree
+test19 = testCase "1 <= m, m <= rp implies 1 <= rp - m" $ assertCompileError source19 expected19
+
+source20 :: String
+source20 = preamble <> proxyInEqDef <> [i|
+test :: Proxy 1 -> Proxy (m ^ 2) -> ()
+test = proxyInEq
+|]
+
+expected20 :: [String]
+expected20 =
+#if __GLASGOW_HASKELL__ >= 904
+  ["Cannot satisfy: 1 <= m ^ 2"]
+#elif __GLASGOW_HASKELL__ >= 902
+  [ "Couldn't match type Data.Type.Ord.OrdCond"
+  , "(CmpNat 1 (m ^ 2)) True True False"
+  , "with True"
+  ]
+#else
+  [ "Couldn't match type 1 <=? (m ^ 2) with True" ]
+#endif
+
+test20 :: TestTree
+test20 = testCase "Vacuously: 1 <= m ^ 2 ~ True" $ assertCompileError source20 expected20
+
+inequalityTests :: TestTree
+inequalityTests = testGroup "Inequality"
+  [ test12
+  , test13
+  , test14
+  , test15
+  , test16
+  , test17
+  , test18
+  , test19
+  , test20
+  ]
diff --git a/tests/ShouldError/Tasty.hs b/tests/ShouldError/Tasty.hs
new file mode 100644
--- /dev/null
+++ b/tests/ShouldError/Tasty.hs
@@ -0,0 +1,58 @@
+{-# LANGUAGE CPP #-}
+
+module ShouldError.Tasty where
+
+import Data.List (isInfixOf)
+import Data.Maybe (fromMaybe)
+import System.Environment (lookupEnv)
+import System.Exit
+import System.IO
+import System.IO.Temp
+import System.Process
+import Test.Tasty.HUnit
+
+-- | Assert that a Haskell code snippet fails to compile with expected error messages
+assertCompileError :: String -> [String] -> Assertion
+assertCompileError source expectedErrors = do
+  -- XXX: This will pick the wrong GHC if the HC environment variable (as seen on CI)
+  --      isn't set and the test suite is compiled with a GHC compiler other than the
+  --      system's default.
+  hc <- fromMaybe "ghc" <$> lookupEnv "HC"
+  withSystemTempFile "ShouldError.hs" $ \tempFile tempHandle -> do
+    hPutStr tempHandle source
+    hClose tempHandle
+    (exitCode, _, stderrOutput) <- readProcessWithExitCode hc
+      [ "-XCPP"
+      , "-XAllowAmbiguousTypes"
+      , "-XConstraintKinds"
+      , "-XDataKinds"
+      , "-XFlexibleContexts"
+      , "-XGADTs"
+      , "-XScopedTypeVariables"
+      , "-XStandaloneDeriving"
+      , "-XTypeApplications"
+      , "-XTypeFamilies"
+      , "-XTypeOperators"
+      , "-XUndecidableInstances"
+      , "-XNoStarIsType"
+      , "-fno-code"
+      , "-fplugin", "GHC.TypeLits.Normalise"
+      , tempFile
+      ] ""
+    case exitCode of
+      ExitSuccess -> assertFailure "Expected compilation to fail but it succeeded"
+      ExitFailure _ ->
+        let cleanedStderr = removeProblemChars stderrOutput
+            cleanedExpected = map removeProblemChars expectedErrors
+        in if all (`isInfixOf` cleanedStderr) cleanedExpected
+           then return ()
+           else assertFailure $ "Error message mismatch:\n" ++
+                               "Expected substrings: " ++ show expectedErrors ++ "\n" ++
+                               "Actual output:\n" ++ stderrOutput
+
+-- | Remove problematic characters that vary depending on locale
+-- The kind and amount of quotes in GHC error messages changes depending on
+-- whether or not our locale supports unicode.
+removeProblemChars :: String -> String
+removeProblemChars = filter (`notElem` problemChars)
+  where problemChars = "‘’`'"
diff --git a/tests/Tests.hs b/tests/Tests.hs
--- a/tests/Tests.hs
+++ b/tests/Tests.hs
@@ -37,14 +37,13 @@
 import Data.Type.Ord
 #endif
 
-import Data.Kind (Type)
-import Data.List (isInfixOf)
+import Data.Kind (Type, Constraint)
 import Data.Proxy
-import Control.Exception
+import Data.Type.Equality ((:~:)(..))
 import Test.Tasty
 import Test.Tasty.HUnit
 
-import ErrorTests
+import qualified ShouldError
 
 data Vec :: Nat -> Type -> Type where
   Nil  :: Vec 0 a
@@ -308,6 +307,15 @@
   a' -> B0 a'
 predBNat (B0 x)  = B1 (predBNat x)
 
+proxyFun3 :: Proxy (x + x + x) -> ()
+proxyFun3 = const ()
+
+proxyFun4 :: Proxy ((2*y)+4) -> ()
+proxyFun4 = const ()
+
+proxyFun7 :: Proxy (2^k) -> Proxy k
+proxyFun7 = const Proxy
+
 -- issue 52 begin
 type role Signal nominal representational
 data Signal (dom :: Symbol) a = a :- Signal dom a
@@ -325,6 +333,12 @@
 issue52 = bundle
 -- issue 52 end
 
+proxyInEq :: (a <= b) => Proxy (a :: Nat) -> Proxy b -> ()
+proxyInEq _ _ = ()
+
+proxyInEq' :: ((a <=? b) ~ 'False) => Proxy (a :: Nat) -> Proxy b -> ()
+proxyInEq' _ _ = ()
+
 proxyInEq1 :: Proxy a -> Proxy (a+1) -> ()
 proxyInEq1 = proxyInEq
 
@@ -453,6 +467,14 @@
 succAtMost :: AtMost n -> AtMost (n + 1)
 succAtMost (AtMost (Proxy :: Proxy a)) = AtMost (Proxy :: Proxy a)
 
+data Dict c where
+  Dict :: c => Dict c
+
+instance Show (Dict c) where
+  show Dict = "Dict"
+
+data Boo (n :: Nat) = Boo
+
 eqReduceForward
   :: Eq (Boo (n + 1))
   => Dict (Eq (Boo (n + 2 - 1)))
@@ -473,6 +495,9 @@
   => Dict (Eq (Boo (m + 3)))
 eqReduceBackward' = Dict
 
+type family CLog (b :: Nat) (x :: Nat) :: Nat
+type instance CLog 2 2 = 1
+
 proxyInEq8fun
   :: (1 <= (n + CLog 2 n))
   => Proxy n
@@ -512,6 +537,11 @@
     go :: 1 <= b => Proxy a -> Proxy a
     go = id
 
+type family Drop (n :: Nat) (xs :: [Nat]) :: [Nat] where
+  Drop 0 xs = xs
+  Drop n (x ': xs) = Drop (n-1) xs
+  Drop n '[] = '[]
+
 isOkay ::
   forall x y sh .
   Proxy x ->
@@ -628,47 +658,9 @@
       show (oneLtPowSubst (Proxy :: Proxy 0)) @?=
       "Proxy"
     ]
-  , testGroup "errors"
-    [ testCase "x + 2 ~ 3 + x" $ testProxy1 `throws` testProxy1Errors
-    , testCase "GCD 6 8 + x ~ x + GCD 9 6" $ testProxy2 `throws` testProxy2Errors
-    , testCase "Unify \"x + x + x\" with \"8\"" $ testProxy3 `throws` testProxy3Errors
-    , testCase "Unify \"(2*x)+4\" with \"2\"" $ testProxy4 `throws` testProxy4Errors
-    , testCase "Unify \"(2*x)+4\" with \"7\"" $ testProxy5 `throws` testProxy5Errors
-    , testCase "Unify \"2^k\" with \"7\"" $ testProxy6 `throws` testProxy6Errors
-    , testCase "x ~ y + x" $ testProxy8 `throws` testProxy8Errors
-    , 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
-    , testCase "Do not rewrite constraint to itself" $ t113 `throws` t113_errors
-    , testGroup "Inequality"
-      [ testCase "a+1 <= a" $ testProxy9 `throws` testProxy9Errors
-      , testCase "(a <=? a+1) ~ False" $ testProxy10 `throws` testProxy10Errors
-      , testCase "(a <=? a) ~ False" $ testProxy11 `throws` testProxy11Errors
-      , testCase "() => (a+b <= a+c)" $ testProxy12 `throws` testProxy12Errors
-      , testCase "4a <= 2a" $ testProxy13 `throws` testProxy13Errors
-      , testCase "2a <=? 4a ~ False" $ testProxy14 `throws` testProxy14Errors
-      , testCase "Show (Boo n) => Show (Boo (n - 1 + 1))" $
-          testProxy17 `throws` test17Errors
-      , testCase "1 <= m, m <= rp implies 1 <= rp - m" $ (testProxy19 (Proxy @1) (Proxy @1)) `throws` test19Errors
-      , testCase "Vacuously: 1 <= m ^ 2 ~ True" $ testProxy20 `throws` testProxy20Errors
-      ]
-    ]
+  , ShouldError.tests
   ]
 
--- | Assert that evaluation of the first argument (to WHNF) will throw
--- an exception whose string representation contains the given
--- substrings.
-throws :: a -> [String] -> Assertion
-throws v xs = do
-  result <- try (evaluate v)
-  case result of
-    Right _ -> assertFailure "No exception!"
-    Left (TypeError msg) ->
-      if all (`isInfixOf` msg) xs
-         then return ()
-         else assertFailure msg
-
 showFin :: forall n. KnownNat n => Fin n -> String
 showFin f = mconcat [
   show (finToInt f)
@@ -680,6 +672,10 @@
 finToInt FZ      = 0
 finToInt (FS fn) = finToInt fn + 1
 
+data Fin (n :: Nat) where
+  FZ :: Fin (n + 1)
+  FS :: Fin n -> Fin (n + 1)
+
 predFin :: Fin (n + 2) -> Fin (n + 1)
 predFin (FS fn) = fn
 predFin FZ      = FZ
@@ -798,3 +794,44 @@
      )
   => Proxy n -> Proxy m -> ()
 t97b _ _ = ()
+
+-- Test for https://github.com/clash-lang/ghc-typelits-natnormalise/issues/116
+t116 :: forall n m l. m :~: n -> n :~: 0 -> l :~: 1 -> Float
+t116 a b c =
+  case a of
+    Refl ->
+      case b of
+        Refl ->
+          case c of
+            Refl ->
+              3.0
+
+type family Foo (n :: Nat) :: Nat
+
+t119a :: Proxy n -> Proxy (Foo (n + 2)) -> Proxy (Foo (2 + n))
+t119a _ = id
+
+--Only applicable for GHC >= 9.4 as prior InEq constraints are of the form `a <=? b ~ 'True`
+#if __GLASGOW_HASKELL__ >= 904
+t119b ::
+  (1 <= a) =>
+  (1 <= Foo (a + 1)) =>
+  Proxy a ->
+  Proxy a
+t119b a = go a
+  where
+    go ::
+      ((1 <= Foo (c + 1)) ~ (() :: Constraint)) =>
+      Proxy c ->
+      Proxy c
+    go _ = Proxy
+#endif
+
+data NatPhantom (n :: Nat) = NatPhantom
+
+-- Test for https://github.com/clash-lang/ghc-typelits-natnormalise/issues/124
+t124 :: 1 <= n => NatPhantom m -> NatPhantom (m + n - 1)
+t124 x = go x
+  where
+    go :: NatPhantom a -> NatPhantom (b + a)
+    go _ = NatPhantom