diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,10 @@
 # Changelog for the [`ghc-typelits-extra`](http://hackage.haskell.org/package/ghc-typelits-extra) package
 
+# 0.5.3 *March 19th 2026*
+* Do not require equality to unit constraint for wanted InEqs for `CLog` and `CLogWZ`.
+* Fix wrong reification from `CLogWZ` to `CLog` causing GHC panic. [#71](https://github.com/clash-lang/ghc-typelits-extra/issues/71)
+* Do not emit new wanteds for given `CLogWZ ~ CLog` equalities. [#73](https://github.com/clash-lang/ghc-typelits-extra/issues/73)
+
 # 0.5.2 *December 3rd 2025*
 * Add `CLogWZ`, an extension of 'CLog', which returns the additional third argument in case the second argument is zero
 * Add rewrite rules for `Min`, `Max`, `FLog`, `CLog`, and `Log`
diff --git a/ghc-typelits-extra.cabal b/ghc-typelits-extra.cabal
--- a/ghc-typelits-extra.cabal
+++ b/ghc-typelits-extra.cabal
@@ -1,6 +1,6 @@
 cabal-version:       3.0
 name:                ghc-typelits-extra
-version:             0.5.2
+version:             0.5.3
 synopsis:            Additional type-level operations on GHC.TypeLits.Nat
 description:
   Additional type-level operations on @GHC.TypeLits.Nat@:
@@ -47,7 +47,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.6, GHC == 9.8.4, GHC == 9.10.3,
@@ -73,10 +73,10 @@
   build-depends:       base                      >= 4.8      && <5,
                        containers                >= 0.5.7.1  && <0.9,
                        ghc                       >= 8.8      && <9.17,
-                       ghc-prim                  >= 0.5      && <1.0,
+                       ghc-prim                  >= 0.5      && <1,
                        ghc-tcplugin-api          >= 0.18.1.0 && <0.19,
                        ghc-typelits-knownnat     >= 0.7.2    && <0.9,
-                       ghc-typelits-natnormalise >= 0.9.3    && <0.10,
+                       ghc-typelits-natnormalise >= 0.9.5    && <0.10,
                        transformers              >= 0.4.2.0  && <0.7,
                        template-haskell          >= 2.15     && <2.25
   if impl(ghc >= 9.0.0)
@@ -125,16 +125,23 @@
 test-suite test-ghc-typelits-extra
   type:                exitcode-stdio-1.0
   main-is:             Main.hs
-  Other-Modules:       ErrorTests
-  build-depends:       base                      >= 4.8 && <5,
+  Other-Modules:       ShouldError
+                       ShouldError.Tasty
+  build-depends:       base,
+                       directory,
+                       filepath,
                        ghc-typelits-extra,
-                       ghc-typelits-knownnat     >= 0.8.2,
-                       ghc-typelits-natnormalise >= 0.9.0,
+                       ghc-typelits-knownnat,
+                       ghc-typelits-natnormalise,
+                       process,
+                       interpolate,
                        tasty                     >= 0.10,
-                       tasty-hunit               >= 0.9
+                       tasty-hunit               >= 0.9,
+                       temporary
   hs-source-dirs:      tests
+  ghc-options:         -Wall
   default-language:    Haskell2010
   other-extensions:    DataKinds
                        TypeOperators
   if flag(deverror)
-    ghc-options:       -dcore-lint
+    ghc-options:       -Werror -dcore-lint
diff --git a/src/GHC/TypeLits/Extra.hs b/src/GHC/TypeLits/Extra.hs
--- a/src/GHC/TypeLits/Extra.hs
+++ b/src/GHC/TypeLits/Extra.hs
@@ -84,9 +84,6 @@
 import Data.Proxy             (Proxy (..))
 import Data.Type.Bool         (If)
 import GHC.Base               (Int#,isTrue#,(==#),(+#))
-#if MIN_VERSION_ghc(9,4,0)
-import GHC.Base               (Constraint)
-#endif
 import GHC.Integer.Logarithms (integerLogBase#)
 #if MIN_VERSION_ghc(8,2,0)
 import GHC.Magic              (noinline)
@@ -185,11 +182,7 @@
 type family CLog (base :: Nat) (value :: Nat) :: Nat where
   CLog 2 1 = 0 -- Additional equations are provided by the custom solver
 
-#if MIN_VERSION_ghc(9,4,0)
-instance (KnownNat x, KnownNat y, (2 <= x) ~ (() :: Constraint), 1 <= y) => KnownNat2 $(nameToSymbol ''CLog) x y where
-#else
 instance (KnownNat x, KnownNat y, 2 <= x, 1 <= y) => KnownNat2 $(nameToSymbol ''CLog) x y where
-#endif
   natSing2 = let x  = natVal (Proxy @x)
                  y  = natVal (Proxy @y)
                  z1 = integerLogBase# x y
@@ -204,11 +197,7 @@
   CLogWZ _ 0 z = z
   CLogWZ b v _ = CLog b v
 
-#if MIN_VERSION_ghc(9,4,0)
-instance (KnownNat x, KnownNat y, KnownNat z, (2 <= x) ~ (() :: Constraint)) => KnownNat3 $(nameToSymbol ''CLogWZ) x y z where
-#else
 instance (KnownNat x, KnownNat y, KnownNat z, 2 <= x) => KnownNat3 $(nameToSymbol ''CLogWZ) x y z where
-#endif
   natSing3 = let x  = natVal (Proxy @x)
                  y  = natVal (Proxy @y)
                  z  = natVal (Proxy @z)
diff --git a/src/GHC/TypeLits/Extra/Solver.hs b/src/GHC/TypeLits/Extra/Solver.hs
--- a/src/GHC/TypeLits/Extra/Solver.hs
+++ b/src/GHC/TypeLits/Extra/Solver.hs
@@ -220,13 +220,13 @@
                  (CLog a' b', CLogWZ a b _) | a == a' && b == b' -> Just b
                  _ -> Nothing
       case wz of
-        Just x -> do
+        Just x | isWantedCt ct -> do
           let x' = reifyEOP defs x
               one = reifyEOP defs (I 1)
           ev <- newWanted (ctLoc ct) $ mkLEqNat (ordTyCons defs) one x'
           let newCt = mkNonCanonical ev
           simples (fmap (,ct) evM:evs) (newCt:news) eqs'
-        Nothing -> do
+        _ -> do
           ur <- unifyExtra ct u v
           tcPluginTrace "unifyExtra result" (ppr ur)
           case ur of
diff --git a/src/GHC/TypeLits/Extra/Solver/Operations.hs b/src/GHC/TypeLits/Extra/Solver/Operations.hs
--- a/src/GHC/TypeLits/Extra/Solver/Operations.hs
+++ b/src/GHC/TypeLits/Extra/Solver/Operations.hs
@@ -119,7 +119,7 @@
   Div x y      -> mkTyConApp (divTyCon defs)  $ reifyEOP defs <$> [x, y]
   Mod x y      -> mkTyConApp (modTyCon defs)  $ reifyEOP defs <$> [x, y]
   CLog x y     -> mkTyConApp (clogTyCon defs) $ reifyEOP defs <$> [x, y]
-  CLogWZ x y z -> mkTyConApp (clogTyCon defs) $ reifyEOP defs <$> [x, y, z]
+  CLogWZ x y z -> mkTyConApp (clogWZTyCon defs) $ reifyEOP defs <$> [x, y, z]
   FLog x y     -> mkTyConApp (flogTyCon defs) $ reifyEOP defs <$> [x, y]
   Log x y      -> mkTyConApp (logTyCon defs)  $ reifyEOP defs <$> [x, y]
   GCD x y      -> mkTyConApp (gcdTyCon defs)  $ reifyEOP defs <$> [x, y]
diff --git a/tests/ErrorTests.hs b/tests/ErrorTests.hs
deleted file mode 100644
--- a/tests/ErrorTests.hs
+++ /dev/null
@@ -1,305 +0,0 @@
-{-# LANGUAGE CPP, DataKinds, TypeOperators, TypeApplications, TypeFamilies #-}
-#if __GLASGOW_HASKELL__ >= 805
-{-# LANGUAGE NoStarIsType #-}
-#endif
-{-# OPTIONS_GHC -fdefer-type-errors #-}
-{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}
-{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}
-{-# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver #-}
-
-module ErrorTests where
-
-import Data.Proxy
-import GHC.TypeLits
-import GHC.TypeLits.Extra
-#if __GLASGOW_HASKELL__ >= 901
-import qualified Data.Type.Ord
-#endif
-
-testFail1 :: Proxy (GCD 6 8) -> Proxy 4
-testFail1 = id
-
-testFail2 :: Proxy ((GCD 6 8) + x) -> Proxy (x + (GCD 6 9))
-testFail2 = id
-
-testFail3 :: Proxy (CLog 3 10) -> Proxy 2
-testFail3 = id
-
-testFail4 :: Proxy ((CLog 3 10) + x) -> Proxy (x + (CLog 2 9))
-testFail4 = id
-
-testFail5 :: Proxy (CLog 0 4) -> Proxy 100
-testFail5 = id
-
-testFail6 :: Proxy (CLog 1 4) -> Proxy 100
-testFail6 = id
-
-testFail7 :: Proxy (CLog 4 0) -> Proxy 0
-testFail7 = id
-
-testFail8 :: Proxy (CLog 1 (1^y)) -> Proxy y
-testFail8 = id
-
-testFail9 :: Proxy (CLog 0 (0^y)) -> Proxy y
-testFail9 = id
-
-testFail10 :: Integer
-testFail10 = natVal (Proxy :: Proxy (CLog 1 4))
-
-testFail11 :: Integer
-testFail11 = natVal (Proxy :: Proxy ((CLog 4 4) - (CLog 2 4)))
-
-testFail12 :: Proxy (Div 4 0) -> Proxy 4
-testFail12 = id
-
-testFail13 :: Proxy (Mod 4 0) -> Proxy 4
-testFail13 = id
-
-testFail14 :: Proxy (FLog 0 4) -> Proxy 100
-testFail14 = id
-
-testFail15 :: Proxy (FLog 1 4) -> Proxy 100
-testFail15 = id
-
-testFail16 :: Proxy (FLog 4 0) -> Proxy 0
-testFail16 = id
-
-testFail17 :: Proxy (LCM 6 8) -> Proxy 48
-testFail17 = id
-
-testFail18 :: Proxy ((LCM 6 8) + x) -> Proxy (x + (LCM 6 9))
-testFail18 = id
-
-testFail19 :: Integer
-testFail19 = natVal (Proxy :: Proxy (Log 3 0))
-
-testFail20 :: Integer
-testFail20 = natVal (Proxy :: Proxy (Log 3 10))
-
-testFail21 :: Proxy a -> Proxy b -> Proxy (Min a (a*b)) -> Proxy a
-testFail21 _ _ = id
-
-testFail22 :: Proxy a -> Proxy b -> Proxy (Max a (a*b)) -> Proxy (a*b)
-testFail22 _ _ = id
-
-testFail23' :: ((1 <=? Div l r) ~ False) => Proxy l -> Proxy r -> ()
-testFail23' _ _ = ()
-
-testFail23 :: ()
-testFail23 = testFail23' (Proxy @18) (Proxy @3)
-
-testFail24 :: Proxy x -> Proxy y -> Proxy z -> Proxy (z <=? Max x y) -> Proxy True
-testFail24 _ _ _ = id
-
-testFail25 :: Proxy x -> Proxy y -> Proxy (x+1 <=? Max x y) -> Proxy True
-testFail25 _ _ = id
-
--- While n ~ (Max x y) implies x <= n (see test46), the reverse is not true.
-testFail26' :: ((x <=? n) ~ True)  => Proxy x -> Proxy y -> Proxy n -> Proxy ((Max x y)) -> Proxy n
-testFail26' _ _ _ = id
-
-testFail26 = testFail26' (Proxy @4) (Proxy @6) (Proxy @6)
-
-testFail27 :: Proxy n -> Proxy (n + 2 <=? Max (n + 1) 1) -> Proxy True
-testFail27 _ = id
-
-testFail1Errors =
-  ["Proxy (GCD 6 8) -> Proxy 4"
-  ,"Proxy 4 -> Proxy 4"
-  ]
-
-testFail2Errors =
-#if __GLASGOW_HASKELL__ >= 904
-  ["Proxy (GCD 6 8 + x) -> Proxy (x + GCD 6 9)"
-  ,"Proxy (2 + x) -> Proxy (2 + x)"
-  ]
-#elif __GLASGOW_HASKELL__ >= 900
-  ["Proxy (GCD 6 8 + x) -> Proxy (x + GCD 6 9)"
-  ,"Proxy (GCD 6 8 + x) -> Proxy (GCD 6 8 + x)"
-  ]
-#else
-  ["Expected type: Proxy (GCD 6 8 + x) -> Proxy (x + GCD 6 9)"
-  ,"Actual type: Proxy (x + GCD 6 9) -> Proxy (x + GCD 6 9)"
-  ]
-#endif
-
-testFail3Errors =
-  ["Proxy (CLog 3 10) -> Proxy 2"
-  ,"Proxy 2 -> Proxy 2"
-  ]
-
-testFail4Errors =
-#if __GLASGOW_HASKELL__ >= 904
-  ["Proxy (CLog 3 10 + x) -> Proxy (x + CLog 2 9)"
-  ,"Proxy (3 + x) -> Proxy (3 + x)"
-  ]
-#elif __GLASGOW_HASKELL__ >= 900
-  ["Proxy (CLog 3 10 + x) -> Proxy (x + CLog 2 9)"
-  ,"Proxy (CLog 3 10 + x) -> Proxy (CLog 3 10 + x)"
-  ]
-#else
-  ["Proxy (CLog 3 10 + x) -> Proxy (x + CLog 2 9)"
-  ,"Proxy (x + CLog 2 9) -> Proxy (x + CLog 2 9)"
-  ]
-#endif
-
-testFail5Errors =
-  ["Proxy (CLog 0 4) -> Proxy 100"
-  ,"Proxy 100 -> Proxy 100"
-  ]
-
-testFail6Errors =
-  ["Proxy (CLog 1 4) -> Proxy 100"
-  ,"Proxy 100 -> Proxy 100"
-  ]
-
-testFail7Errors =
-  ["Proxy (CLog 4 0) -> Proxy 0"
-  ,"Proxy 0 -> Proxy 0"
-  ]
-
-testFail8Errors =
-  ["Proxy (CLog 1 (1 ^ y)) -> Proxy y"
-  ,"Proxy y -> Proxy y"
-  ]
-
-testFail9Errors =
-  ["Proxy (CLog 0 (0 ^ y)) -> Proxy y"
-  ,"Proxy y -> Proxy y"
-  ]
-
-testFail10Errors =
-#if __GLASGOW_HASKELL__ >= 904
-  ["Cannot satisfy: 2 <= 1"]
-#else
-  ["Couldn't match type ‘'False’ with ‘'True’"]
-#endif
-
-testFail11Errors =
-#if __GLASGOW_HASKELL__ >= 904
-  ["Cannot satisfy: 2 <= 1"]
-#else
-  ["Couldn't match type ‘'False` with ‘'True’"]
-#endif
-
-testFail12Errors =
-  ["Proxy (Div 4 0) -> Proxy 4"
-  ,"Proxy 4 -> Proxy 4"
-  ]
-
-testFail13Errors =
-  ["Proxy (Mod 4 0) -> Proxy 4"
-  ,"Proxy 4 -> Proxy 4"
-  ]
-
-testFail14Errors =
-  ["Proxy (FLog 0 4) -> Proxy 100"
-  ,"Proxy 100 -> Proxy 100"
-  ]
-
-testFail15Errors =
-  ["Proxy (FLog 1 4) -> Proxy 100"
-  ,"Proxy 100 -> Proxy 100"
-  ]
-
-testFail16Errors =
-  ["Proxy (FLog 4 0) -> Proxy 0"
-  ,"Proxy 0 -> Proxy 0"
-  ]
-
-testFail17Errors =
-  ["Proxy (LCM 6 8) -> Proxy 48"
-  ,"Proxy 48 -> Proxy 48"
-  ]
-
-testFail18Errors =
-#if __GLASGOW_HASKELL__ >= 904
-  ["Proxy (LCM 6 8 + x) -> Proxy (x + LCM 6 9)"
-  ,"Proxy (24 + x) -> Proxy (24 + x)"
-  ]
-#elif __GLASGOW_HASKELL__ >= 900
-  ["Proxy (LCM 6 8 + x) -> Proxy (x + LCM 6 9)"
-  ,"Proxy (LCM 6 8 + x) -> Proxy (LCM 6 8 + x)"
-  ]
-#else
-  ["Proxy (LCM 6 8 + x) -> Proxy (x + LCM 6 9)"
-  ,"Proxy (x + LCM 6 9) -> Proxy (x + LCM 6 9)"
-  ]
-#endif
-
-testFail19Errors =
-#if __GLASGOW_HASKELL__ >= 900
-  ["Couldn't match type: FLog 3 0"
-  ,"               with: CLog 3 0"]
-#else
-  ["Couldn't match type ‘FLog 3 0’ with ‘CLog 3 0’"]
-#endif
-
-testFail20Errors =
-#if __GLASGOW_HASKELL__ >= 904
-  ["Couldn't match type ‘2’ with ‘3’"]
-#elif __GLASGOW_HASKELL__ >= 900
-  ["Couldn't match type: FLog 3 10"
-  ,"               with: CLog 3 10"]
-#else
-  ["Couldn't match type ‘FLog 3 10’ with ‘CLog 3 10’"]
-#endif
-
-testFail21Errors =
-  ["Proxy (Min a (a * b)) -> Proxy a"
-  ,"Proxy a -> Proxy a"
-  ]
-
-testFail22Errors =
-#if __GLASGOW_HASKELL__ >= 900
-  ["Proxy (Max a (a * b)) -> Proxy (a * b)"
-  ,"Proxy (Max a (a * b)) -> Proxy (Max a (a * b))"]
-#else
-  ["Proxy (Max a (a * b)) -> Proxy (a * b)"
-  ,"Proxy (a * b) -> Proxy (a * b)"]
-#endif
-
-testFail23Errors =
-#if __GLASGOW_HASKELL__ >= 804
-  ["Couldn't match type ‘'True’ with ‘'False’"]
-#else
-  ["Couldn't match type ‘1 <=? Div 18 3’ with ‘'False’"]
-#endif
-
-testFail24Errors =
-#if __GLASGOW_HASKELL__ >= 902
-  ["Couldn't match type ‘Data.Type.Ord.OrdCond"
-  ,"(CmpNat z (Max x y)) 'True 'True 'False’"
-  ,"with ‘'True’"]
-#else
-  ["Couldn't match type ‘z <=? Max x y’ with ‘'True’"]
-#endif
-
-testFail25Errors =
-#if __GLASGOW_HASKELL__ >= 902
-  ["Couldn't match type ‘Data.Type.Ord.OrdCond"
-  ,"(CmpNat (x + 1) (Max x y)) 'True 'True 'False’"
-  ,"with ‘'True’"]
-#else
-  ["Couldn't match type ‘(x + 1) <=? Max x y’ with ‘'True’"]
-#endif
-
-testFail26Errors =
-#if __GLASGOW_HASKELL__ >= 906
-  ["Could not deduce ‘Max x y ~ n’"
-  ,"from the context: (x <=? n) ~ True"
-  ]
-#elif __GLASGOW_HASKELL__ <= 902
-  ["Could not deduce: Max x y ~ n"
-  ,"from the context: (x <=? n) ~ 'True"
-  ]
-#else
-  ["Could not deduce (Max x y ~ n)"
-  ,"from the context: (x <=? n) ~ 'True"
-  ]
-#endif
-
-testFail27Errors =
-  ["Proxy ((n + 2) <=? Max (n + 1) 1) -> Proxy 'True"
-  ,"Proxy 'True -> Proxy 'True"
-  ]
diff --git a/tests/Main.hs b/tests/Main.hs
--- a/tests/Main.hs
+++ b/tests/Main.hs
@@ -12,19 +12,22 @@
 {-# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver #-}
 #endif
 
+-- Even though binders are not used, they're compiled and that's what we're after.
+{-# OPTIONS_GHC -Wno-unused-top-binds #-}
 
-import Data.List (isInfixOf)
+-- Only applies to old GHCs.
+{-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-}
+
 import Data.Proxy
-import Data.Type.Bool
-import Control.Exception
+import Data.Type.Equality
 import Test.Tasty
 import Test.Tasty.HUnit
 
-import ErrorTests
-
 import GHC.TypeLits
 import GHC.TypeLits.Extra
 
+import qualified ShouldError
+
 test1 :: Proxy (GCD 6 8) -> Proxy 2
 test1 = id
 
@@ -275,6 +278,12 @@
 test69 :: 1 <= n => Proxy n -> Proxy (CLogWZ 2 n 0) -> Proxy (CLog 2 n)
 test69 _ = id
 
+-- Regression test for: https://github.com/clash-lang/ghc-typelits-extra/issues/73
+test70 :: (CLog 2 n ~ CLogWZ 2 n 0) => Proxy n -> Proxy n
+test70 _ =
+  case (Refl :: Max (n + 1) 1 :~: (1 + n)) of
+    Refl -> Proxy
+
 main :: IO ()
 main = defaultMain tests
 
@@ -485,53 +494,9 @@
     , testCase "1 <= n => CLogWZ 2 n 0 ~ CLog 2 n" $
       show (test69 (Proxy :: Proxy 3) Proxy) @?=
       "Proxy"
-    ]
-  , testGroup "errors"
-    [ testCase "GCD 6 8 /~ 4" $ testFail1 `throws` testFail1Errors
-    , testCase "GCD 6 8 + x /~ x + GCD 9 6" $ testFail2 `throws` testFail2Errors
-    , testCase "CLog 3 10 /~ 2" $ testFail3 `throws` testFail3Errors
-    , testCase "CLog 3 10 + x /~ x + CLog 2 9" $ testFail4 `throws` testFail4Errors
-    , testCase "CLog 0 4 /~ 100" $ testFail5 `throws` testFail5Errors
-    , testCase "CLog 1 4 /~ 100" $ testFail5 `throws` testFail5Errors
-    , testCase "CLog 4 0 /~ 0" $ testFail7 `throws` testFail7Errors
-    , testCase "CLog 1 (1^y) /~ y" $ testFail8 `throws` testFail8Errors
-    , testCase "CLog 0 (0^y) /~ y" $ testFail9 `throws` testFail9Errors
-    , testCase "No instance (KnownNat (CLog 1 4))" $ testFail10 `throws` testFail10Errors
-    , testCase "No instance (KnownNat (CLog 4 4 - CLog 2 4))" $ testFail11 `throws` testFail11Errors
-    , testCase "Div 4 0 /~ 4" $ testFail12 `throws` testFail12Errors
-    , testCase "Mod 4 0 /~ 4" $ testFail13 `throws` testFail13Errors
-    , testCase "FLog 0 4 /~ 100" $ testFail14 `throws` testFail14Errors
-    , testCase "FLog 1 4 /~ 100" $ testFail15 `throws` testFail15Errors
-    , testCase "FLog 4 0 /~ 0" $ testFail16 `throws` testFail16Errors
-    , testCase "GCD 6 8 /~ 4" $ testFail17 `throws` testFail17Errors
-    , testCase "GCD 6 8 + x /~ x + GCD 9 6" $ testFail18 `throws` testFail18Errors
-    , testCase "No instance (KnownNat (Log 3 0))" $ testFail19 `throws` testFail19Errors
-    , testCase "No instance (KnownNat (Log 3 10))" $ testFail20 `throws` testFail20Errors
-    , testCase "Min a (a*b) /~ a" $ testFail21 `throws` testFail21Errors
-    , testCase "Max a (a*b) /~ (a*b)" $ testFail22 `throws` testFail22Errors
-    , testCase "(1 <=? Div 18 6) ~ False" $ testFail23 `throws` testFail23Errors
-    , testCase "(z <=? Max x y) /~ True" $ testFail24 `throws` testFail24Errors
-    , testCase "(x+1 <=? Max x y) /~ True" $ testFail25 `throws` testFail25Errors
-    , testCase "(x <= n) /=> (Max x y) ~ n" $ testFail26 `throws` testFail26Errors
-    , testCase "n + 2 <=? Max (n + 1) 1 /~ True" $ testFail27 `throws` testFail27Errors
+    , testCase "CLogWZ ~ CLog given does not loop" $
+      show (test70 (Proxy :: Proxy 1)) @?=
+      "Proxy"
     ]
+  , 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` (removeProblemChars msg)) $ map removeProblemChars xs
-         then return ()
-         else assertFailure msg
-
--- The kind and amount of quotes in GHC error messages changes depending on
--- whether or not our locale supports unicode.
--- Remove the problematic characters to enable comparison of errors.
-removeProblemChars = filter (`notElem` problemChars)
-  where problemChars = "‘’`'"
diff --git a/tests/ShouldError.hs b/tests/ShouldError.hs
new file mode 100644
--- /dev/null
+++ b/tests/ShouldError.hs
@@ -0,0 +1,574 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE QuasiQuotes #-}
+{-# LANGUAGE TemplateHaskell #-}
+
+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
+    , test12
+    , test13
+    , test14
+    , test15
+    , test16
+    , test17
+    , test18
+    , test19
+    , test20
+    , test21
+    , test22
+    , test23
+    , test24
+    , test25
+    , test26
+    , test27
+    , test28
+    ]
+
+preamble :: String
+preamble = [i|
+import Data.Proxy
+import GHC.TypeLits
+import GHC.TypeLits.Extra
+|] <> "\n"
+
+source1 :: String
+source1 = preamble <> [i|
+test :: Proxy (GCD 6 8) -> Proxy 4
+test = id
+|]
+
+expected1 :: [String]
+expected1 =
+  ["Proxy (GCD 6 8) -> Proxy 4"
+  ,"Proxy 4 -> Proxy 4"
+  ]
+
+test1 :: TestTree
+test1 = testCase "GCD 6 8 /~ 4" $ assertCompileError source1 expected1
+
+source2 :: String
+source2 = preamble <> [i|
+test :: Proxy ((GCD 6 8) + x) -> Proxy (x + (GCD 6 9))
+test = id
+|]
+
+expected2 :: [String]
+expected2 =
+#if __GLASGOW_HASKELL__ >= 904
+  ["Proxy (GCD 6 8 + x) -> Proxy (x + GCD 6 9)"
+  ,"Proxy (2 + x) -> Proxy (2 + x)"
+  ]
+#elif __GLASGOW_HASKELL__ >= 900
+  ["Proxy (GCD 6 8 + x) -> Proxy (x + GCD 6 9)"
+  ,"Proxy (GCD 6 8 + x) -> Proxy (GCD 6 8 + x)"
+  ]
+#else
+  ["Expected type: Proxy (GCD 6 8 + x) -> Proxy (x + GCD 6 9)"
+  ,"Actual type: Proxy (x + GCD 6 9) -> Proxy (x + GCD 6 9)"
+  ]
+#endif
+
+test2 :: TestTree
+test2 = testCase "GCD 6 8 + x /~ x + GCD 9 6" $ assertCompileError source2 expected2
+
+source3 :: String
+source3 = preamble <> [i|
+test :: Proxy (CLog 3 10) -> Proxy 2
+test = id
+|]
+
+expected3 :: [String]
+expected3 =
+  ["Proxy (CLog 3 10) -> Proxy 2"
+  ,"Proxy 2 -> Proxy 2"
+  ]
+
+test3 :: TestTree
+test3 = testCase "CLog 3 10 /~ 2" $ assertCompileError source3 expected3
+
+source4 :: String
+source4 = preamble <> [i|
+test :: Proxy ((CLog 3 10) + x) -> Proxy (x + (CLog 2 9))
+test = id
+|]
+
+expected4 :: [String]
+expected4 =
+#if __GLASGOW_HASKELL__ >= 904
+  ["Proxy (CLog 3 10 + x) -> Proxy (x + CLog 2 9)"
+  ,"Proxy (3 + x) -> Proxy (3 + x)"
+  ]
+#elif __GLASGOW_HASKELL__ >= 900
+  ["Proxy (CLog 3 10 + x) -> Proxy (x + CLog 2 9)"
+  ,"Proxy (CLog 3 10 + x) -> Proxy (CLog 3 10 + x)"
+  ]
+#else
+  ["Proxy (CLog 3 10 + x) -> Proxy (x + CLog 2 9)"
+  ,"Proxy (x + CLog 2 9) -> Proxy (x + CLog 2 9)"
+  ]
+#endif
+
+test4 :: TestTree
+test4 = testCase "CLog 3 10 + x /~ x + CLog 2 10" $ assertCompileError source4 expected4
+
+source5 :: String
+source5 = preamble <> [i|
+test :: Proxy (CLog 0 4) -> Proxy 100
+test = id
+|]
+
+expected5 :: [String]
+expected5 =
+  ["Proxy (CLog 0 4) -> Proxy 100"
+  ,"Proxy 100 -> Proxy 100"
+  ]
+
+test5 :: TestTree
+test5 = testCase "CLog 0 4 /~ 100" $ assertCompileError source5 expected5
+
+source6 :: String
+source6 = preamble <> [i|
+test :: Proxy (CLog 1 4) -> Proxy 100
+test = id
+|]
+
+expected6 :: [String]
+expected6 =
+  ["Proxy (CLog 1 4) -> Proxy 100"
+  ,"Proxy 100 -> Proxy 100"
+  ]
+
+test6 :: TestTree
+test6 = testCase "CLog 1 4 /~ 100" $ assertCompileError source6 expected6
+
+source7 :: String
+source7 = preamble <> [i|
+test :: Proxy (CLog 4 0) -> Proxy 0
+test = id
+|]
+
+expected7 :: [String]
+expected7 =
+  ["Proxy (CLog 4 0) -> Proxy 0"
+  ,"Proxy 0 -> Proxy 0"
+  ]
+
+test7 :: TestTree
+test7 = testCase "CLog 4 0 /~ 0" $ assertCompileError source7 expected7
+
+source8 :: String
+source8 = preamble <> [i|
+test :: Proxy (CLog 1 (1^y)) -> Proxy y
+test = id
+|]
+
+expected8 :: [String]
+expected8 =
+  ["Proxy (CLog 1 (1 ^ y)) -> Proxy y"
+  ,"Proxy y -> Proxy y"
+  ]
+
+test8 :: TestTree
+test8 = testCase "CLog 1 (1^y) /~ y" $ assertCompileError source8 expected8
+
+source9 :: String
+source9 = preamble <> [i|
+test :: Proxy (CLog 0 (0^y)) -> Proxy y
+test = id
+|]
+
+expected9 :: [String]
+expected9 =
+  ["Proxy (CLog 0 (0 ^ y)) -> Proxy y"
+  ,"Proxy y -> Proxy y"
+  ]
+
+test9 :: TestTree
+test9 = testCase "CLog 0 (0^y) /~ y" $ assertCompileError source9 expected9
+
+source10 :: String
+source10 = [i|
+{-# LANGUAGE TypeApplications #-}
+|] <> preamble <> [i|
+test :: Integer
+test = natVal (Proxy :: Proxy (CLog 1 4))
+|]
+
+expected10 :: [String]
+expected10 =
+#if __GLASGOW_HASKELL__ >= 904
+  ["Cannot satisfy: 2 <= 1"]
+#else
+  ["Couldn't match type ''False' with ''True'"]
+#endif
+
+test10 :: TestTree
+test10 = testCase "No instance (KnownNat (CLog 1 4))" $ assertCompileError source10 expected10
+
+source11 :: String
+source11 = [i|
+{-# LANGUAGE TypeApplications #-}
+|] <> preamble <> [i|
+test :: Integer
+test = natVal (Proxy :: Proxy ((CLog 4 4) - (CLog 2 4)))
+|]
+
+expected11 :: [String]
+expected11 =
+#if __GLASGOW_HASKELL__ >= 904
+  ["Cannot satisfy: 2 <= 1"]
+#else
+  ["Couldn't match type ''False` with ''True'"]
+#endif
+
+test11 :: TestTree
+test11 = testCase "No instance (KnownNat (CLog 4 4 - CLog 2 4))" $ assertCompileError source11 expected11
+
+source12 :: String
+source12 = preamble <> [i|
+test :: Proxy (Div 4 0) -> Proxy 4
+test = id
+|]
+
+expected12 :: [String]
+expected12 =
+  ["Proxy (Div 4 0) -> Proxy 4"
+  ,"Proxy 4 -> Proxy 4"
+  ]
+
+test12 :: TestTree
+test12 = testCase "Div 4 0 /~ 4" $ assertCompileError source12 expected12
+
+source13 :: String
+source13 = preamble <> [i|
+test :: Proxy (Mod 4 0) -> Proxy 4
+test = id
+|]
+
+expected13 :: [String]
+expected13 =
+  ["Proxy (Mod 4 0) -> Proxy 4"
+  ,"Proxy 4 -> Proxy 4"
+  ]
+
+test13 :: TestTree
+test13 = testCase "Mod 4 0 /~ 4" $ assertCompileError source13 expected13
+
+source14 :: String
+source14 = preamble <> [i|
+test :: Proxy (FLog 0 4) -> Proxy 100
+test = id
+|]
+
+expected14 :: [String]
+expected14 =
+  ["Proxy (FLog 0 4) -> Proxy 100"
+  ,"Proxy 100 -> Proxy 100"
+  ]
+
+test14 :: TestTree
+test14 = testCase "FLog 0 4 /~ 100" $ assertCompileError source14 expected14
+
+source15 :: String
+source15 = preamble <> [i|
+test :: Proxy (FLog 1 4) -> Proxy 100
+test = id
+|]
+
+expected15 :: [String]
+expected15 =
+  ["Proxy (FLog 1 4) -> Proxy 100"
+  ,"Proxy 100 -> Proxy 100"
+  ]
+
+test15 :: TestTree
+test15 = testCase "FLog 1 4 /~ 100" $ assertCompileError source15 expected15
+
+source16 :: String
+source16 = preamble <> [i|
+test :: Proxy (FLog 4 0) -> Proxy 0
+test = id
+|]
+
+expected16 :: [String]
+expected16 =
+  ["Proxy (FLog 4 0) -> Proxy 0"
+  ,"Proxy 0 -> Proxy 0"
+  ]
+
+test16 :: TestTree
+test16 = testCase "FLog 4 0 /~ 0" $ assertCompileError source16 expected16
+
+source17 :: String
+source17 = preamble <> [i|
+test :: Proxy (LCM 6 8) -> Proxy 48
+test = id
+|]
+
+expected17 :: [String]
+expected17 =
+  ["Proxy (LCM 6 8) -> Proxy 48"
+  ,"Proxy 48 -> Proxy 48"
+  ]
+
+test17 :: TestTree
+test17 = testCase "LCM 6 8 /~ 48" $ assertCompileError source17 expected17
+
+source18 :: String
+source18 = preamble <> [i|
+test :: Proxy ((LCM 6 8) + x) -> Proxy (x + (LCM 6 9))
+test = id
+|]
+
+expected18 :: [String]
+expected18 =
+#if __GLASGOW_HASKELL__ >= 904
+  ["Proxy (LCM 6 8 + x) -> Proxy (x + LCM 6 9)"
+  ,"Proxy (24 + x) -> Proxy (24 + x)"
+  ]
+#elif __GLASGOW_HASKELL__ >= 900
+  ["Proxy (LCM 6 8 + x) -> Proxy (x + LCM 6 9)"
+  ,"Proxy (LCM 6 8 + x) -> Proxy (LCM 6 8 + x)"
+  ]
+#else
+  ["Proxy (LCM 6 8 + x) -> Proxy (x + LCM 6 9)"
+  ,"Proxy (x + LCM 6 9) -> Proxy (x + LCM 6 9)"
+  ]
+#endif
+
+test18 :: TestTree
+test18 = testCase "LCM 6 8 + x /~ x + LCM 6 9" $ assertCompileError source18 expected18
+
+source19 :: String
+source19 = [i|
+{-# LANGUAGE TypeApplications #-}
+|] <> preamble <> [i|
+test :: Integer
+test = natVal (Proxy :: Proxy (Log 3 0))
+|]
+
+expected19 :: [String]
+expected19 =
+#if __GLASGOW_HASKELL__ >= 900
+  ["Couldn't match type: FLog 3 0"
+  ,"               with: CLog 3 0"]
+#else
+  ["Couldn't match type 'FLog 3 0' with 'CLog 3 0'"]
+#endif
+
+test19 :: TestTree
+test19 = testCase "No instance (KnownNat (Log 3 0))" $ assertCompileError source19 expected19
+
+source20 :: String
+source20 = [i|
+{-# LANGUAGE TypeApplications #-}
+|] <> preamble <> [i|
+test :: Integer
+test = natVal (Proxy :: Proxy (Log 3 10))
+|]
+
+expected20 :: [String]
+expected20 =
+#if __GLASGOW_HASKELL__ >= 904
+  ["Couldn't match type '2' with '3'"]
+#elif __GLASGOW_HASKELL__ >= 900
+  ["Couldn't match type: FLog 3 10"
+  ,"               with: CLog 3 10"]
+#else
+  ["Couldn't match type 'FLog 3 10' with 'CLog 3 10'"]
+#endif
+
+test20 :: TestTree
+test20 = testCase "No instance (KnownNat (Log 3 10))" $ assertCompileError source20 expected20
+
+source21 :: String
+source21 = preamble <> [i|
+test :: Proxy a -> Proxy b -> Proxy (Min a (a * b)) -> Proxy a
+test _ _ = id
+|]
+
+expected21 :: [String]
+expected21 =
+  ["Proxy (Min a (a * b)) -> Proxy a"
+  ,"Proxy a -> Proxy a"
+  ]
+
+test21 :: TestTree
+test21 = testCase "Min a (a*b) /~ a" $ assertCompileError source21 expected21
+
+source22 :: String
+source22 = preamble <> [i|
+test :: Proxy a -> Proxy b -> Proxy (Max a (a * b)) -> Proxy (a * b)
+test _ _ = id
+|]
+
+expected22 :: [String]
+expected22 =
+#if __GLASGOW_HASKELL__ >= 900
+  ["Proxy (Max a (a * b)) -> Proxy (a * b)"
+  ,"Proxy (Max a (a * b)) -> Proxy (Max a (a * b))"]
+#else
+  ["Proxy (Max a (a * b)) -> Proxy (a * b)"
+  ,"Proxy (a * b) -> Proxy (a * b)"]
+#endif
+
+test22 :: TestTree
+test22 = testCase "Max a (a*b) /~ (a*b)" $ assertCompileError source22 expected22
+
+source23 :: String
+source23 = [i|
+{-# LANGUAGE TypeApplications #-}
+|] <> preamble <> [i|
+test' :: ((1 <=? Div l r) ~ False) => Proxy l -> Proxy r -> ()
+test' _ _ = ()
+
+test :: ()
+test = test' (Proxy @18) (Proxy @3)
+|]
+
+expected23 :: [String]
+expected23 =
+#if __GLASGOW_HASKELL__ >= 804
+  ["Couldn't match type ''True' with ''False'"]
+#else
+  ["Couldn't match type '1 <=? Div 18 3' with ''False'"]
+#endif
+
+test23 :: TestTree
+test23 = testCase "(1 <=? Div 18 3) ~ False" $ assertCompileError source23 expected23
+
+source24 :: String
+source24 = [i|
+{-# LANGUAGE CPP #-}
+|] <> preamble <> [i|
+#if __GLASGOW_HASKELL__ >= 901
+import qualified Data.Type.Ord
+#endif
+
+test :: Proxy x -> Proxy y -> Proxy z -> Proxy (z <=? Max x y) -> Proxy True
+test _ _ _ = id
+|]
+
+expected24 :: [String]
+expected24 =
+#if __GLASGOW_HASKELL__ >= 902
+  ["Couldn't match type 'Data.Type.Ord.OrdCond"
+  ,"(CmpNat z (Max x y)) 'True 'True 'False'"
+  ,"with ''True'"]
+#else
+  ["Couldn't match type 'z <=? Max x y' with ''True'"]
+#endif
+
+test24 :: TestTree
+test24 = testCase "(z <=? Max x y) /~ True" $ assertCompileError source24 expected24
+
+source25 :: String
+source25 = [i|
+{-# LANGUAGE CPP #-}
+|] <> preamble <> [i|
+#if __GLASGOW_HASKELL__ >= 901
+import qualified Data.Type.Ord
+#endif
+
+test :: Proxy x -> Proxy y -> Proxy (x+1 <=? Max x y) -> Proxy True
+test _ _ = id
+|]
+
+expected25 :: [String]
+expected25 =
+#if __GLASGOW_HASKELL__ >= 902
+  ["Couldn't match type 'Data.Type.Ord.OrdCond"
+  ,"(CmpNat (x + 1) (Max x y)) 'True 'True 'False'"
+  ,"with ''True'"]
+#else
+  ["Couldn't match type '(x + 1) <=? Max x y' with ''True'"]
+#endif
+
+test25 :: TestTree
+test25 = testCase "(x+1 <=? Max x y) /~ True" $ assertCompileError source25 expected25
+
+source26 :: String
+source26 = [i|
+{-# LANGUAGE TypeApplications #-}
+|] <> preamble <> [i|
+
+-- While n ~ (Max x y) implies x <= n (see test46), the reverse is not true.
+test' :: ((x <=? n) ~ True)  => Proxy x -> Proxy y -> Proxy n -> Proxy ((Max x y)) -> Proxy n
+test' _ _ _ = id
+
+test = test' (Proxy @4) (Proxy @6) (Proxy @6)
+|]
+
+expected26 :: [String]
+expected26 =
+#if __GLASGOW_HASKELL__ >= 906
+  ["Could not deduce 'Max x y ~ n'"
+  ,"from the context: (x <=? n) ~ True"
+  ]
+#elif __GLASGOW_HASKELL__ <= 902
+  ["Could not deduce: Max x y ~ n"
+  ,"from the context: (x <=? n) ~ 'True"
+  ]
+#else
+  ["Could not deduce (Max x y ~ n)"
+  ,"from the context: (x <=? n) ~ 'True"
+  ]
+#endif
+
+test26 :: TestTree
+test26 = testCase "(x <= n) /=> (Max x y) ~ n" $ assertCompileError source26 expected26
+
+source27 :: String
+source27 = preamble <> [i|
+test :: Proxy n -> Proxy (n + 2 <=? Max (n + 1) 1) -> Proxy True
+test _ = id
+|]
+
+expected27 :: [String]
+expected27 =
+  ["Proxy ((n + 2) <=? Max (n + 1) 1) -> Proxy 'True"
+  ,"Proxy 'True -> Proxy 'True"
+  ]
+
+test27 :: TestTree
+test27 = testCase "n + 2 <=? Max (n + 1) 1 /~ True" $ assertCompileError source27 expected27
+
+source28 :: String
+source28 = [i|
+{-# LANGUAGE KindSignatures #-}
+|] <> preamble <> [i|
+type Size (n :: Nat) = Max 0 (CLogWZ 2 n 0)
+
+pack :: Proxy n -> Proxy (Size n)
+pack _ = Proxy
+
+repro :: Proxy (Size 1)
+repro = pack (undefined :: Proxy (n :: Nat))
+|]
+
+expected28 :: [String]
+expected28 =
+  ["CLogWZ 2 n"
+  ,"ambiguous"
+  ]
+
+test28 :: TestTree
+test28 = testCase "CLogWZ reify with Max 0 (type synonym) doesn't panic" $
+  assertCompileError source28 expected28
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,53 @@
+{-# 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"
+      , "-XDataKinds"
+      , "-XTypeOperators"
+      , "-XTypeApplications"
+      , "-XTypeFamilies"
+      , "-XNoStarIsType"
+      , "-fno-code"
+      , "-fplugin", "GHC.TypeLits.Normalise"
+      , "-fplugin", "GHC.TypeLits.KnownNat.Solver"
+      , "-fplugin", "GHC.TypeLits.Extra.Solver"
+      , 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 = "‘’`'"