diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,9 @@
 # Changelog for the [`ghc-typelits-natnormalise`](http://hackage.haskell.org/package/ghc-typelits-natnormalise) package
 
+## 0.5.1 *September 29th 2016*
+* Fixes bugs:
+  * Cannot solve an equality for the second time in a definition group
+
 ## 0.5 *August 17th 2016*
 * Solve simple inequalities, i.e.:
   * `a  <= a + 1`
diff --git a/ghc-typelits-natnormalise.cabal b/ghc-typelits-natnormalise.cabal
--- a/ghc-typelits-natnormalise.cabal
+++ b/ghc-typelits-natnormalise.cabal
@@ -1,5 +1,5 @@
 name:                ghc-typelits-natnormalise
-version:             0.5
+version:             0.5.1
 synopsis:            GHC typechecker plugin for types of kind GHC.TypeLits.Nat
 description:
   A type checker plugin for GHC that can solve /equalities/ of types of kind
@@ -84,13 +84,15 @@
   build-depends:       base >=4.8 && <5,
                        ghc-typelits-natnormalise >= 0.4,
                        tasty >= 0.10,
-                       tasty-hunit >= 0.9
+                       tasty-hunit >= 0.9,
+                       template-haskell >= 2.11.0.0
   hs-source-dirs:      tests
   default-language:    Haskell2010
   other-extensions:    DataKinds
                        GADTs
                        KindSignatures
                        NoImplicitPrelude
+                       TemplateHaskell
                        TypeFamilies
                        TypeOperators
                        ScopedTypeVariables
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
@@ -50,26 +50,26 @@
 
 -- external
 import Control.Arrow       (second)
-import Data.IORef          (IORef, newIORef,readIORef, modifyIORef)
+import Control.Monad       (replicateM)
 import Data.List           (intersect)
-import Data.Maybe          (catMaybes, mapMaybe)
+import Data.Maybe          (mapMaybe)
 import GHC.TcPluginM.Extra (tracePlugin)
 
 -- GHC API
 import Outputable (Outputable (..), (<+>), ($$), text)
 import Plugins    (Plugin (..), defaultPlugin)
 import TcEvidence (EvTerm (..))
-import TcPluginM  (TcPluginM, tcPluginIO, tcPluginTrace, zonkCt)
+import TcPluginM  (TcPluginM, tcPluginTrace, zonkCt)
 import TcRnTypes  (Ct, TcPlugin (..), TcPluginResult(..), ctEvidence, ctEvPred,
-                   ctPred, isWanted, mkNonCanonical)
-import Type       (EqRel (NomEq), Kind, PredTree (EqPred), PredType, TyVar,
+                   isWanted, mkNonCanonical)
+import Type       (EqRel (NomEq), Kind, PredTree (EqPred), PredType,
                    classifyPredType, eqType, getEqPredTys, mkTyVarTy)
 import TysWiredIn (typeNatKind)
 
 import Coercion   (CoercionHole, Role (..), mkForAllCos, mkHoleCo, mkInstCo,
                    mkNomReflCo, mkUnivCo)
 import TcPluginM  (newCoercionHole, newFlexiTyVar)
-import TcRnTypes  (CtEvidence (..), TcEvDest (..), ctLoc)
+import TcRnTypes  (CtEvidence (..), CtLoc, TcEvDest (..), ctLoc)
 import TyCoRep    (UnivCoProvenance (..))
 import Type       (mkPrimEqPred)
 import TcType     (typeKind)
@@ -96,15 +96,15 @@
 
 normalisePlugin :: TcPlugin
 normalisePlugin = tracePlugin "ghc-typelits-natnormalise"
-  TcPlugin { tcPluginInit  = tcPluginIO $ newIORef []
-           , tcPluginSolve = decideEqualSOP
+  TcPlugin { tcPluginInit  = return ()
+           , tcPluginSolve = const decideEqualSOP
            , tcPluginStop  = const (return ())
            }
 
-decideEqualSOP :: IORef [Ct] -> [Ct] -> [Ct] -> [Ct]
+decideEqualSOP :: [Ct] -> [Ct] -> [Ct]
                -> TcPluginM TcPluginResult
-decideEqualSOP _          _givens _deriveds []      = return (TcPluginOk [] [])
-decideEqualSOP discharged givens  _deriveds wanteds = do
+decideEqualSOP _givens _deriveds []      = return (TcPluginOk [] [])
+decideEqualSOP givens  _deriveds wanteds = do
     -- GHC 7.10.1 puts deriveds with the wanteds, so filter them out
     let wanteds' = filter (isWanted . ctEvidence) wanteds
     let unit_wanteds = mapMaybe toNatEquality wanteds'
@@ -115,61 +115,12 @@
         sr <- simplifyNats (unit_givens ++ unit_wanteds)
         tcPluginTrace "normalised" (ppr sr)
         case sr of
-          Simplified _subst evs -> do
-            let solved     = filter (isWanted . ctEvidence . (\(_,x,_) -> x)) evs
-            discharedWanteds <- tcPluginIO (readIORef discharged)
-            let existingWanteds = wanteds' ++ discharedWanteds
-            -- Create new wanted constraints
-            (solved',newWanteds) <- (second concat . unzip . catMaybes) <$>
-                                    mapM (evItemToCt existingWanteds) solved
-            -- update set of discharged wanteds
-            tcPluginIO (modifyIORef discharged (++ newWanteds))
-            -- return
+          Simplified evs -> do
+            let solved = filter (isWanted . ctEvidence . (\((_,x),_) -> x)) evs
+                (solved',newWanteds) = second concat (unzip solved)
             return (TcPluginOk solved' newWanteds)
           Impossible eq -> return (TcPluginContradiction [fromNatEquality eq])
 
-evItemToCt :: [Ct] -- ^ Existing wanteds
-           -> (EvTerm,Ct,CoreUnify CoreNote)
-           -> TcPluginM (Maybe ((EvTerm,Ct),[Ct]))
-evItemToCt existingWanteds (ev,ct,subst)
-    | null newWanteds = return (Just ((ev,ct),[]))
-    | otherwise = do
-        newWanteds' <- catMaybes <$> mapM (substItemToCt existingWanteds) newWanteds
-        -- only allow new (conditional) evidence if conditional wanted constraints
-        -- can be added as new work
-        if length newWanteds == length newWanteds'
-           then return (Just ((ev,ct),newWanteds'))
-           else return Nothing
-  where
-    newWanteds = filter (isWanted . ctEvidence . snd . siNote) subst
-
-substItemToCt :: [Ct] -- ^ Existing wanteds wanted
-              -> UnifyItem TyVar CType CoreNote
-              -> TcPluginM (Maybe Ct)
-substItemToCt existingWanteds si
-  | CType predicate  `notElem` wantedPreds
-  , CType predicateS `notElem` wantedPreds
-  = return (Just (mkNonCanonical (CtWanted predicate (HoleDest ev) (ctLoc ct))))
-  | otherwise
-  = return Nothing
-  where
-    predicate     = unifyItemToPredType si
-    (ty1,ty2)     = getEqPredTys predicate
-    predicateS    = mkPrimEqPred ty2 ty1
-    ((ev,_,_),ct) = siNote si
-    wantedPreds   = map (CType . ctPred) existingWanteds
-
-unifyItemToPredType :: UnifyItem TyVar CType a -> PredType
-unifyItemToPredType ui =
-    mkPrimEqPred ty1 ty2
-  where
-    ty1 = case ui of
-            SubstItem {..} -> mkTyVarTy siVar
-            UnifyItem {..} -> reifySOP siLHS
-    ty2 = case ui of
-            SubstItem {..} -> reifySOP siSOP
-            UnifyItem {..} -> reifySOP siRHS
-
 type NatEquality   = (Ct,CoreSOP,CoreSOP)
 type NatInEquality = (Ct,CoreSOP)
 
@@ -177,14 +128,12 @@
 fromNatEquality (Left  (ct, _, _)) = ct
 fromNatEquality (Right (ct, _))    = ct
 
-type CoreNote = ((CoercionHole,TyVar,PredType), Ct)
-
 data SimplifyResult
-  = Simplified (CoreUnify CoreNote) [(EvTerm,Ct,CoreUnify CoreNote)]
+  = Simplified [((EvTerm,Ct),[Ct])]
   | Impossible (Either NatEquality NatInEquality)
 
 instance Outputable SimplifyResult where
-  ppr (Simplified subst evs) = text "Simplified" $$ ppr subst $$ ppr evs
+  ppr (Simplified evs) = text "Simplified" $$ ppr evs
   ppr (Impossible eq)  = text "Impossible" <+> ppr eq
 
 simplifyNats :: [Either NatEquality NatInEquality]
@@ -192,33 +141,35 @@
 simplifyNats eqs =
     tcPluginTrace "simplifyNats" (ppr eqs) >> simples [] [] [] eqs
   where
-    simples :: CoreUnify CoreNote
-            -> [Maybe (EvTerm, Ct, CoreUnify CoreNote)]
+    simples :: [CoreUnify]
+            -> [((EvTerm, Ct), [Ct])]
             -> [Either NatEquality NatInEquality]
             -> [Either NatEquality NatInEquality]
             -> TcPluginM SimplifyResult
-    simples subst evs _xs [] = return (Simplified subst (catMaybes evs))
+    simples _subst evs _xs [] = return (Simplified evs)
     simples subst evs xs (eq@(Left (ct,u,v)):eqs') = do
       ur <- unifyNats ct (substsSOP subst u) (substsSOP subst v)
       tcPluginTrace "unifyNats result" (ppr ur)
       case ur of
-        Win         -> simples subst (((,,) <$> evMagic ct [] <*> pure ct <*> pure []):evs) []
-                               (xs ++ eqs')
-        Lose        -> return (Impossible eq)
-        Draw []     -> simples subst evs (eq:xs) eqs'
+        Win -> do
+          evs' <- maybe evs (:evs) <$> evMagic ct []
+          simples subst evs' [] (xs ++ eqs')
+        Lose -> return (Impossible eq)
+        Draw [] -> simples subst evs (eq:xs) eqs'
         Draw subst' -> do
-          newEvs <- mapM (\si -> (,,) <$> newCoercionHole
-                                      <*> newFlexiTyVar typeNatKind
-                                      <*> pure (unifyItemToPredType si))
-                         subst'
-          let subst'' = zipWith (\si ev -> si {siNote = (ev,siNote si)})
-                                subst' newEvs
-          simples (substsSubst subst'' subst ++ subst'')
-            (((,,) <$> evMagic ct newEvs <*> pure ct <*> pure subst''):evs)
-            [] (xs ++ eqs')
-    simples subst evs xs (eq@(Right (ct,u)):eqs') =
-      case isNatural u of
-        Just True  -> simples subst (((,,) <$> evMagic ct [] <*> pure ct <*> pure []):evs) xs eqs'
+          evM <- evMagic ct (map unifyItemToPredType subst')
+          case evM of
+            Nothing -> simples subst evs xs eqs'
+            Just ev ->
+              simples (substsSubst subst' subst ++ subst')
+                      (ev:evs) [] (xs ++ eqs')
+    simples subst evs xs (eq@(Right (ct,u)):eqs') = do
+      let u' = substsSOP subst u
+      tcPluginTrace "unifyNats(ineq) results" (ppr (ct,u'))
+      case isNatural u' of
+        Just True  -> do
+          evs' <- maybe evs (:evs) <$> evMagic ct []
+          simples subst evs' xs eqs'
         Just False -> return (Impossible eq)
         Nothing    -> simples subst evs (eq:xs) eqs'
 
@@ -254,15 +205,33 @@
     isNatKind :: Kind -> Bool
     isNatKind = (`eqType` typeNatKind)
 
-evMagic :: Ct -> [(CoercionHole, TyVar, PredType)] -> Maybe EvTerm
-evMagic ct evs = case classifyPredType $ ctEvPred $ ctEvidence ct of
-  EqPred NomEq t1 t2 ->
-    let ctEv = mkUnivCo (PluginProv "ghc-typelits-natnormalise") Nominal t1 t2
-        (holes,tvs,preds) = unzip3 evs
-        holeEvs = zipWith (\h p -> uncurry (mkHoleCo h Nominal) (getEqPredTys p))
-                          holes preds
+unifyItemToPredType :: CoreUnify -> PredType
+unifyItemToPredType ui =
+    mkPrimEqPred ty1 ty2
+  where
+    ty1 = case ui of
+            SubstItem {..} -> mkTyVarTy siVar
+            UnifyItem {..} -> reifySOP siLHS
+    ty2 = case ui of
+            SubstItem {..} -> reifySOP siSOP
+            UnifyItem {..} -> reifySOP siRHS
+
+evMagic :: Ct -> [PredType] -> TcPluginM (Maybe ((EvTerm, Ct), [Ct]))
+evMagic ct preds = case classifyPredType $ ctEvPred $ ctEvidence ct of
+  EqPred NomEq t1 t2 -> do
+    holes <- replicateM (length preds) newCoercionHole
+    let newWanted = zipWith (unifyItemToCt (ctLoc ct)) preds holes
+        ctEv      = mkUnivCo (PluginProv "ghc-typelits-natnormalise") Nominal t1 t2
+        holeEvs   = zipWith (\h p -> uncurry (mkHoleCo h Nominal) (getEqPredTys p)) holes preds
         natReflCo = mkNomReflCo typeNatKind
-        forallEv = mkForAllCos (map (,natReflCo) tvs) ctEv
-        finalEv = foldl mkInstCo forallEv holeEvs
-    in  Just (EvCoercion finalEv)
-  _ -> Nothing
+        natCoBndr = (,natReflCo) <$> (newFlexiTyVar typeNatKind)
+    forallEv <- mkForAllCos <$> (replicateM (length preds) natCoBndr) <*> pure ctEv
+    let finalEv = foldl mkInstCo forallEv holeEvs
+    return (Just ((EvCoercion finalEv, ct),newWanted))
+  _ -> return Nothing
+
+unifyItemToCt :: CtLoc
+              -> PredType
+              -> CoercionHole
+              -> Ct
+unifyItemToCt loc pred_type hole = mkNonCanonical (CtWanted pred_type (HoleDest hole) loc)
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
@@ -22,7 +22,6 @@
   , reifySOP
     -- * Substitution on 'SOP' terms
   , UnifyItem (..)
-  , TyUnify
   , CoreUnify
   , substsSOP
   , substsSubst
@@ -168,25 +167,21 @@
 -- | A substitution is essentially a list of (variable, 'SOP') pairs,
 -- but we keep the original 'Ct' that lead to the substitution being
 -- made, for use when turning the substitution back into constraints.
-type CoreUnify a = TyUnify TyVar CType a
-
-type TyUnify v c n = [UnifyItem v c n]
+type CoreUnify = UnifyItem TyVar CType
 
-data UnifyItem v c n = SubstItem { siVar  :: v
-                                 , siSOP  :: SOP v c
-                                 , siNote :: n
-                                 }
-                     | UnifyItem { siLHS  :: SOP v c
-                                 , siRHS  :: SOP v c
-                                 , siNote :: n
-                                 }
+data UnifyItem v c = SubstItem { siVar  :: v
+                               , siSOP  :: SOP v c
+                               }
+                   | UnifyItem { siLHS  :: SOP v c
+                               , siRHS  :: SOP v c
+                               }
 
-instance (Outputable v, Outputable c) => Outputable (UnifyItem v c n) where
+instance (Outputable v, Outputable c) => Outputable (UnifyItem v c) where
   ppr (SubstItem {..}) = ppr siVar <+> text " := " <+> ppr siSOP
   ppr (UnifyItem {..}) = ppr siLHS <+> text " :~ " <+> ppr siRHS
 
 -- | Apply a substitution to a single normalised 'SOP' term
-substsSOP :: (Ord v, Ord c) => TyUnify v c n -> SOP v c -> SOP v c
+substsSOP :: (Ord v, Ord c) => [UnifyItem v c] -> SOP v c -> SOP v c
 substsSOP []                   u = u
 substsSOP ((SubstItem {..}):s) u = substsSOP s (substSOP siVar siSOP u)
 substsSOP ((UnifyItem {}):s)   u = substsSOP s u
@@ -206,7 +201,7 @@
 substSymbol tv e (E s p) = normaliseExp (substSOP tv e s) (substProduct tv e p)
 
 -- | Apply a substitution to a substitution
-substsSubst :: (Ord v, Ord c) => TyUnify v c n -> TyUnify v c n -> TyUnify v c n
+substsSubst :: (Ord v, Ord c) => [UnifyItem v c] -> [UnifyItem v c] -> [UnifyItem v c]
 substsSubst s = map subt
   where
     subt si@(SubstItem {..}) = si {siSOP = substsSOP s siSOP}
@@ -216,9 +211,9 @@
 -- | Result of comparing two 'SOP' terms, returning a potential substitution
 -- list under which the two terms are equal.
 data UnifyResult
-  = Win            -- ^ Two terms are equal
-  | Lose           -- ^ Two terms are /not/ equal
-  | Draw (CoreUnify Ct) -- ^ Two terms are only equal if the given substitution holds
+  = Win              -- ^ Two terms are equal
+  | Lose             -- ^ Two terms are /not/ equal
+  | Draw [CoreUnify] -- ^ Two terms are only equal if the given substitution holds
 
 instance Outputable UnifyResult where
   ppr Win          = text "Win"
@@ -241,11 +236,15 @@
        then if containsConstants u || containsConstants v
                then if u == v
                        then Win
-                       else Draw (unifiers ct u v)
+                       else Draw (filter diffFromConstraint (unifiers ct u v))
                else if u == v
                        then Win
                        else Lose
-       else Draw (unifiers ct u v)
+       else Draw (filter diffFromConstraint (unifiers ct u v))
+  where
+    -- A unifier is only a unifier if differs from the original constraint
+    diffFromConstraint (UnifyItem x y) = not (x == u && y == v)
+    diffFromConstraint _               = True
 
 -- | Find unifiers for two SOP terms
 --
@@ -280,38 +279,38 @@
 -- @
 -- [a := b]
 -- @
-unifiers :: Ct -> CoreSOP -> CoreSOP -> CoreUnify Ct
+unifiers :: Ct -> CoreSOP -> CoreSOP -> [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 ct]
+        | CType (reifySOP u) /= CType t1 || isGiven (ctEvidence ct) -> [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 ct]
+        | CType (reifySOP v) /= CType t2 || isGiven (ctEvidence ct) -> [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 ct]
+        | CType (reifySOP u) /= CType t1 || CType (reifySOP v) /= CType t2 -> [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 ct]
+        | CType (reifySOP u) /= CType t1 || CType (reifySOP v) /= CType t2 -> [UnifyItem u v]
       _ -> []
 unifiers ct u v             = unifiers' ct u v
 
-unifiers' :: Ct -> CoreSOP -> CoreSOP -> CoreUnify Ct
-unifiers' ct (S [P [V x]]) (S [])        = [SubstItem x (S [P [I 0]]) ct]
-unifiers' ct (S [])        (S [P [V x]]) = [SubstItem x (S [P [I 0]]) ct]
+unifiers' :: Ct -> CoreSOP -> CoreSOP -> [CoreUnify]
+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 ct]
-unifiers' ct s             (S [P [V x]]) = [SubstItem x s ct]
+unifiers' _ct (S [P [V x]]) s             = [SubstItem x s]
+unifiers' _ct s             (S [P [V x]]) = [SubstItem x s]
 
-unifiers' ct s1@(S [P [C _]]) s2               = [UnifyItem s1 s2 ct]
-unifiers' ct s1               s2@(S [P [C _]]) = [UnifyItem s1 s2 ct]
+unifiers' _ct s1@(S [P [C _]]) s2               = [UnifyItem s1 s2]
+unifiers' _ct s1               s2@(S [P [C _]]) = [UnifyItem s1 s2]
 
 
 -- (z ^ a) ~ (z ^ b) ==> [a := b]
@@ -400,11 +399,11 @@
           | otherwise = ps2'
     psx = intersect ps1 ps2
 
-unifiers'' :: Ct -> CoreSOP -> CoreSOP -> CoreUnify Ct
+unifiers'' :: Ct -> CoreSOP -> CoreSOP -> [CoreUnify]
 unifiers'' ct (S [P [I i],P [V v]]) s2
-  | isGiven (ctEvidence ct) = [SubstItem v (mergeSOPAdd s2 (S [P [I (negate i)]])) ct]
+  | isGiven (ctEvidence ct) = [SubstItem v (mergeSOPAdd s2 (S [P [I (negate i)]]))]
 unifiers'' ct s1 (S [P [I i],P [V v]])
-  | isGiven (ctEvidence ct) = [SubstItem v (mergeSOPAdd s1 (S [P [I (negate i)]])) ct]
+  | isGiven (ctEvidence ct) = [SubstItem v (mergeSOPAdd s1 (S [P [I (negate i)]]))]
 unifiers'' _ _ _ = []
 
 collectBases :: CoreProduct -> Maybe ([CoreSOP],[CoreProduct])
diff --git a/tests/ErrorTests.hs b/tests/ErrorTests.hs
--- a/tests/ErrorTests.hs
+++ b/tests/ErrorTests.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE DataKinds, KindSignatures, TypeFamilies, TypeOperators #-}
+{-# LANGUAGE DataKinds, KindSignatures, TemplateHaskell, TypeFamilies, TypeOperators #-}
 
 {-# OPTIONS_GHC -fdefer-type-errors #-}
 {-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}
@@ -7,6 +7,10 @@
 import Data.Proxy
 import GHC.TypeLits
 
+import GHC.IO.Encoding            (getLocaleEncoding, textEncodingName, utf8)
+import Language.Haskell.TH        (litE, stringL)
+import Language.Haskell.TH.Syntax (runIO)
+
 testProxy1 :: Proxy (x + 1) -> Proxy (2 + x)
 testProxy1 = id
 
@@ -89,40 +93,69 @@
 testProxy9 = proxyInEq
 
 testProxy9Errors =
-  ["Couldn't match type ‘(a + 1) <=? a’ with ‘'True’"
-  ]
+  [$(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"
+    )]
 
 testProxy10 :: Proxy (a :: Nat) -> Proxy (a + 2) -> ()
 testProxy10 = proxyInEq'
 
 testProxy10Errors =
-  ["Couldn't match type ‘a <=? (a + 2)’ with ‘'False’"
-  ]
+  [$(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"
+    )]
 
 testProxy11 :: Proxy (a :: Nat) -> Proxy a -> ()
 testProxy11 = proxyInEq'
 
 testProxy11Errors =
-  ["Couldn't match type ‘'True’ with ‘'False’"
-  ]
+  [$(do localeEncoding <- runIO (getLocaleEncoding)
+        if textEncodingName localeEncoding == textEncodingName utf8
+          then litE $ stringL "Couldn't match type ‘'True’ with ‘'False’"
+          else litE $ stringL "Couldn't match type 'True with 'False"
+    )]
 
 testProxy12 :: Proxy (a + b) -> Proxy (a + c) -> ()
 testProxy12 = proxyInEq
 
 testProxy12Errors =
-  ["Couldn't match type ‘(a + b) <=? (a + c)’ with ‘'True’"
-  ]
+  [$(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"
+    )]
 
 testProxy13 :: Proxy (4*a) -> Proxy (2*a) ->()
 testProxy13 = proxyInEq
 
 testProxy13Errors =
-  ["Couldn't match type ‘(4 * a) <=? (2 * a)’ with ‘'True’"
-  ]
+  [$(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"
+    )]
 
 testProxy14 :: Proxy (2*a) -> Proxy (4*a) -> ()
 testProxy14 = proxyInEq'
 
 testProxy14Errors =
-  ["Couldn't match type ‘(2 * a) <=? (4 * a)’ with ‘'False’"
+  [$(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"
+    )]
+
+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 =
+  ["Expected type: Proxy n -> Proxy (n + d)"
+  ,"Actual type: Proxy n -> Proxy n"
   ]
diff --git a/tests/Tests.hs b/tests/Tests.hs
--- a/tests/Tests.hs
+++ b/tests/Tests.hs
@@ -310,6 +310,7 @@
     , 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
     , testGroup "Inequality"
       [ testCase "a+1 <= a" $ testProxy9 `throws` testProxy9Errors
       , testCase "(a <=? a+1) ~ False" $ testProxy10 `throws` testProxy10Errors