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.3.1 *August 26th 2019*
+* Reduce `a <=? Max a b` to `True`
+* Reduce `n ~ (Max a b) => a <=? n` to `True`
+* Prove `Max (1 + n) 1 ~ (n+1)`
+
 # 0.3 *September 14th 2018*
 * Move `KnownNat2` instances for GHC 8.4's `Div` and `Mod` from `ghc-typelits-extra` to `ghc-typelits-knownnat`
 
diff --git a/ghc-typelits-extra.cabal b/ghc-typelits-extra.cabal
--- a/ghc-typelits-extra.cabal
+++ b/ghc-typelits-extra.cabal
@@ -1,5 +1,5 @@
 name:                ghc-typelits-extra
-version:             0.3
+version:             0.3.1
 synopsis:            Additional type-level operations on GHC.TypeLits.Nat
 description:
   Additional type-level operations on @GHC.TypeLits.Nat@:
@@ -47,8 +47,7 @@
 extra-source-files:  README.md
                      CHANGELOG.md
 cabal-version:       >=1.10
-tested-with:         GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.1, GHC == 8.4.2,
-                     GHC == 8.6
+tested-with:         GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.4, GHC == 8.6.4
 
 source-repository head
   type: git
@@ -66,11 +65,12 @@
   other-modules:       GHC.TypeLits.Extra.Solver.Unify
                        GHC.TypeLits.Extra.Solver.Operations
   build-depends:       base                      >= 4.8     && <5,
-                       ghc                       >= 7.10    && <8.8,
+                       containers                >= 0.5.7.1 && <0.7,
+                       ghc                       >= 7.10    && <8.9,
                        ghc-prim                  >= 0.5     && <1.0,
                        ghc-tcplugins-extra       >= 0.2,
-                       ghc-typelits-knownnat     >= 0.6     && <0.7,
-                       ghc-typelits-natnormalise >= 0.6     && <0.7,
+                       ghc-typelits-knownnat     >= 0.6     && <0.8,
+                       ghc-typelits-natnormalise >= 0.6     && <0.8,
                        integer-gmp               >= 1.0     && <1.1,
                        transformers              >= 0.4.2.0 && <0.6
   hs-source-dirs:      src
@@ -101,12 +101,10 @@
                        ghc-typelits-knownnat     >= 0.6,
                        ghc-typelits-natnormalise >= 0.4.1,
                        tasty                     >= 0.10,
-                       tasty-hunit               >= 0.9,
-                       template-haskell          >= 2.11.0.0
+                       tasty-hunit               >= 0.9
   hs-source-dirs:      tests
   default-language:    Haskell2010
   other-extensions:    DataKinds
-                       TemplateHaskell
                        TypeOperators
   if flag(deverror)
     ghc-options:       -O0 -dcore-lint
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
@@ -23,8 +23,8 @@
 where
 
 -- external
-import Control.Monad             ((<=<))
 import Control.Monad.Trans.Maybe (MaybeT (..))
+import Data.Either               (lefts)
 import Data.Maybe                (catMaybes)
 import GHC.TcPluginM.Extra       (evByFiat, lookupModule, lookupName,
                                   tracePlugin)
@@ -39,9 +39,9 @@
 import Plugins    (purePlugin)
 #endif
 import TcEvidence (EvTerm)
-import TcPluginM  (TcPluginM, tcLookupTyCon, tcPluginTrace, zonkCt)
+import TcPluginM  (TcPluginM, tcLookupTyCon, tcPluginTrace)
 import TcRnTypes  (Ct, TcPlugin(..), TcPluginResult (..), ctEvidence, ctEvPred,
-                   isWanted)
+                   isWantedCt)
 import TcType      (typeKind)
 import Type       (EqRel (NomEq), Kind, PredTree (EqPred), classifyPredType,
                    eqType)
@@ -49,7 +49,11 @@
 import TysWiredIn (typeNatKind, promotedTrueDataCon, promotedFalseDataCon)
 import TcTypeNats (typeNatLeqTyCon)
 #if MIN_VERSION_ghc(8,4,0)
+import GHC.TcPluginM.Extra (flattenGivens)
 import TcTypeNats (typeNatTyCons)
+#else
+import TcPluginM  (zonkCt)
+import Control.Monad ((<=<))
 #endif
 
 -- internal
@@ -102,16 +106,20 @@
 decideEqualSOP _    _givens _deriveds []      = return (TcPluginOk [] [])
 decideEqualSOP defs givens  _deriveds wanteds = do
   -- GHC 7.10.1 puts deriveds with the wanteds, so filter them out
-  let wanteds' = filter (isWanted . ctEvidence) wanteds
+  let wanteds' = filter isWantedCt wanteds
   unit_wanteds <- catMaybes <$> mapM (runMaybeT . toNatEquality defs) wanteds'
   case unit_wanteds of
     [] -> return (TcPluginOk [] [])
     _  -> do
+#if MIN_VERSION_ghc(8,4,0)
+      unit_givens <- catMaybes <$> mapM (runMaybeT . toNatEquality defs) (givens ++ flattenGivens givens)
+#else
       unit_givens <- catMaybes <$> mapM ((runMaybeT . toNatEquality defs) <=< zonkCt) givens
+#endif
       sr <- simplifyExtra (unit_givens ++ unit_wanteds)
       tcPluginTrace "normalised" (ppr sr)
       case sr of
-        Simplified evs -> return (TcPluginOk (filter (isWanted . ctEvidence . snd) evs) [])
+        Simplified evs -> return (TcPluginOk (filter (isWantedCt . snd) evs) [])
         Impossible eq  -> return (TcPluginContradiction [fromNatEquality eq])
 
 type NatEquality   = (Ct,ExtraOp,ExtraOp)
@@ -145,7 +153,30 @@
         (I i,I j)
           | (i <= j) == b -> simples (((,) <$> evMagic ct <*> pure ct):evs) eqs'
           | otherwise     -> return  (Impossible eq)
+        (p, Max x y)
+          | b && (p == x || p == y) -> simples (((,) <$> evMagic ct <*> pure ct):evs) eqs'
+
+        -- transform:  q ~ Max x y => (p <=? q ~ True)
+        -- to:         (p <=? Max x y) ~ True
+        -- and try to solve that along with the rest of the eqs'
+        (p, q@(V _))
+          | b -> case findMax q eqs of
+                   Just m  -> simples evs ((Right (ct,p,m,b)):eqs')
+                   Nothing -> simples evs eqs'
         _ -> simples evs eqs'
+
+    -- look for given constraint with the form: c ~ Max x y
+    findMax :: ExtraOp -> [Either NatEquality NatInEquality] -> Maybe ExtraOp
+    findMax c = go . lefts
+      where
+        go [] = Nothing
+        go ((ct, a,b@(Max _ _)) :_)
+          | c == a && not (isWantedCt ct)
+            = Just b
+        go ((ct, a@(Max _ _),b) :_)
+          | c == b && not (isWantedCt ct)
+            = Just a
+        go (_:rest) = go rest
 
 
 -- Extract the Nat equality constraints
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
@@ -5,6 +5,7 @@
 Maintainer :  Christiaan Baaij <christiaan.baaij@gmail.com>
 -}
 
+{-# LANGUAGE CPP       #-}
 {-# LANGUAGE MagicHash #-}
 
 module GHC.TypeLits.Extra.Solver.Operations
@@ -26,6 +27,9 @@
 
 -- external
 import Control.Monad.Trans.Writer.Strict
+#if MIN_VERSION_ghc_typelits_natnormalise(0,7,0)
+import Data.Set                     as Set
+#endif
 
 import GHC.Base                     (isTrue#,(==#),(+#))
 import GHC.Integer                  (smallInteger)
@@ -111,9 +115,15 @@
   let x' = reifyEOP defs x
       y' = reifyEOP defs y
       z  = fst (runWriter (normaliseNat (mkTyConApp typeNatSubTyCon [y',x'])))
+#if MIN_VERSION_ghc_typelits_natnormalise(0,7,0)
+  in  case runWriterT (isNatural z) of
+        Just (True , cs) | Set.null cs -> y
+        Just (False, cs) | Set.null cs -> x
+#else
   in  case isNatural z of
         Just True  -> y
         Just False -> x
+#endif
         _ -> Max x y
 
 mergeMin :: ExtraDefs -> ExtraOp -> ExtraOp -> ExtraOp
@@ -121,9 +131,15 @@
   let x' = reifyEOP defs x
       y' = reifyEOP defs y
       z  = fst (runWriter (normaliseNat (mkTyConApp typeNatSubTyCon [y',x'])))
+#if MIN_VERSION_ghc_typelits_natnormalise(0,7,0)
+  in  case runWriterT (isNatural z) of
+        Just (True, cs) | Set.null cs -> x
+        Just (False,cs) | Set.null cs -> y
+#else
   in  case isNatural z of
         Just True  -> x
         Just False -> y
+#endif
         _ -> Min x y
 
 mergeDiv :: ExtraOp -> ExtraOp -> Maybe ExtraOp
diff --git a/src/GHC/TypeLits/Extra/Solver/Unify.hs b/src/GHC/TypeLits/Extra/Solver/Unify.hs
--- a/src/GHC/TypeLits/Extra/Solver/Unify.hs
+++ b/src/GHC/TypeLits/Extra/Solver/Unify.hs
@@ -18,8 +18,10 @@
 -- external
 import Control.Monad.Trans.Class    (lift)
 import Control.Monad.Trans.Maybe    (MaybeT (..))
+import Control.Monad.Trans.Writer.Strict (runWriter)
 import Data.Function                (on)
 import GHC.TypeLits.Normalise.Unify (CType (..))
+import qualified GHC.TypeLits.Normalise.Unify as Normalise
 
 -- GHC API
 import Outputable (Outputable (..), ($$), text)
@@ -69,7 +71,8 @@
   tyM    <- lift (matchFam tc tys')
   case tyM of
     Just (_,ty) -> normaliseNat defs ty
-    _ -> return (C (CType (TyConApp tc tys)))
+    _ -> let q = fst (runWriter (Normalise.normaliseNat (TyConApp tc tys)))
+         in  return (C (CType (Normalise.reifySOP q)))
 
 normaliseNat _ t = return (C (CType t))
 
diff --git a/tests/ErrorTests.hs b/tests/ErrorTests.hs
--- a/tests/ErrorTests.hs
+++ b/tests/ErrorTests.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE CPP, DataKinds, TypeOperators, TypeApplications, TypeFamilies, TemplateHaskell #-}
+{-# LANGUAGE CPP, DataKinds, TypeOperators, TypeApplications, TypeFamilies #-}
 #if __GLASGOW_HASKELL__ >= 805
 {-# LANGUAGE NoStarIsType #-}
 #endif
@@ -13,10 +13,6 @@
 import GHC.TypeLits
 import GHC.TypeLits.Extra
 
-import GHC.IO.Encoding            (getLocaleEncoding, textEncodingName, utf8)
-import Language.Haskell.TH        (litE, stringL)
-import Language.Haskell.TH.Syntax (runIO)
-
 testFail1 :: Proxy (GCD 6 8) -> Proxy 4
 testFail1 = id
 
@@ -89,7 +85,18 @@
 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)
+
 testFail1Errors =
   ["Expected type: Proxy (GCD 6 8) -> Proxy 4"
   ,"Actual type: Proxy 4 -> Proxy 4"
@@ -136,18 +143,10 @@
   ]
 
 testFail10Errors =
-  [$(do localeEncoding <- runIO (getLocaleEncoding)
-        if textEncodingName localeEncoding == textEncodingName utf8
-          then litE $ stringL "Couldn't match type ‘'False’ with ‘'True’"
-          else litE $ stringL "Couldn't match type 'False with 'True"
-    )]
+  ["Couldn't match type ‘'False’ with ‘'True’"]
 
 testFail11Errors =
-  [$(do localeEncoding <- runIO (getLocaleEncoding)
-        if textEncodingName localeEncoding == textEncodingName utf8
-          then litE $ stringL "Couldn't match type ‘CLog 2 4 <=? CLog 4 4’ with ‘'True’"
-          else litE $ stringL "Couldn't match type `CLog 2 4 <=? CLog 4 4' with 'True"
-    )]
+  ["Couldn't match type ‘CLog 2 4 <=? CLog 4 4’ with ‘'True’"]
 
 testFail12Errors =
   ["Expected type: Proxy (Div 4 0) -> Proxy 4"
@@ -185,18 +184,10 @@
   ]
 
 testFail19Errors =
-  [$(do localeEncoding <- runIO (getLocaleEncoding)
-        if textEncodingName localeEncoding == textEncodingName utf8
-          then litE $ stringL "Couldn't match type ‘FLog 3 0’ with ‘CLog 3 0’"
-          else litE $ stringL "Couldn't match type `FLog 3 0' with `CLog 3 0'"
-    )]
+  ["Couldn't match type ‘FLog 3 0’ with ‘CLog 3 0’"]
 
 testFail20Errors =
-  [$(do localeEncoding <- runIO (getLocaleEncoding)
-        if textEncodingName localeEncoding == textEncodingName utf8
-          then litE $ stringL "Couldn't match type ‘FLog 3 10’ with ‘CLog 3 10’"
-          else litE $ stringL "Couldn't match type `FLog 3 10' with `CLog 3 10'"
-    )]
+  ["Couldn't match type ‘FLog 3 10’ with ‘CLog 3 10’"]
 
 testFail21Errors =
   ["Expected type: Proxy (Min a (a * b)) -> Proxy a"
@@ -213,3 +204,14 @@
 #else
   ["Couldn't match type ‘1 <=? Div 18 3’ with ‘'False’"]
 #endif
+
+testFail24Errors =
+  ["Couldn't match type ‘z <=? Max x y’ with ‘'True’"]
+
+testFail25Errors =
+  ["Couldn't match type ‘(x + 1) <=? Max x y’ with ‘'True’"]
+
+testFail26Errors =
+  ["Could not deduce: Max x y ~ n"
+  ,"from the context: (x <=? n) ~ 'True"
+  ]
diff --git a/tests/Main.hs b/tests/Main.hs
--- a/tests/Main.hs
+++ b/tests/Main.hs
@@ -147,6 +147,42 @@
 test43 :: Proxy x -> Proxy y -> Proxy (LCM x y) -> Proxy (LCM y x)
 test43 _ _ = id
 
+test44 :: Proxy x -> Proxy y -> Proxy (x <=? (Max x y)) -> Proxy True
+test44 _ _ = id
+
+test45 :: Proxy x -> Proxy y -> Proxy (y <=? (Max x y)) -> Proxy True
+test45 _ _ = id
+
+test46 :: n ~ (Max x y) => Proxy x -> Proxy y -> Proxy (x <=? n) -> Proxy True
+test46 _ _ = id
+
+test47 :: n ~ (Max x y) => Proxy x -> Proxy y -> Proxy (y <=? n) -> Proxy True
+test47 _ _ = id
+
+test48
+  :: Proxy n
+  -> Proxy (Max (1+n) 1)
+  -> Proxy (n+1)
+test48 _ = id
+
+test49
+  :: Proxy n
+  -> Proxy (Max (n+1) 1)
+  -> Proxy (1+n)
+test49 _ = id
+
+test50
+  :: Proxy n
+  -> Proxy (Max (n+2) 1)
+  -> Proxy (Max (2+n) 2)
+test50 _ = id
+
+test51
+  :: Proxy n
+  -> Proxy (Max (((2 ^ n) + 1) + ((2 ^ n) + 1)) 1)
+  -> Proxy (2+((2^n)*2))
+test51 _ = id
+
 main :: IO ()
 main = defaultMain tests
 
@@ -282,6 +318,30 @@
     , testCase "forall x y . LCM x y ~ LCM y x" $
       show (test43 Proxy Proxy Proxy) @?=
       "Proxy"
+    , testCase "forall x y . x <=? Max x y ~ True" $
+      show (test44 Proxy Proxy Proxy) @?=
+      "Proxy"
+    , testCase "forall x y . y <=? Max x y ~ True" $
+      show (test45 Proxy Proxy Proxy) @?=
+      "Proxy"
+    , testCase "forall x y n . n ~ Max x y => x <=? n ~ True" $
+      show (test46 Proxy Proxy Proxy) @?=
+      "Proxy"
+    , testCase "forall x y n . n ~ Max x y => y <=? n ~ True" $
+      show (test47 Proxy Proxy Proxy) @?=
+      "Proxy"
+    , testCase "forall n . Max (n+1) 1 ~ 1+n" $
+      show (test48 Proxy Proxy) @?=
+      "Proxy"
+    , testCase "forall n . Max (1+n) 1 ~ n+1" $
+      show (test49 Proxy Proxy) @?=
+      "Proxy"
+    , testCase "forall n . Max (n+2) 1 ~ Max (2+n) 2" $
+      show (test50 Proxy Proxy) @?=
+      "Proxy"
+    , testCase "forall n . Max (((2 ^ n) + 1) + ((2 ^ n) + 1)) 1 ~ 2 + ((2 ^ n) * 2)" $
+      show (test51 Proxy Proxy) @?=
+      "Proxy"
     ]
   , testGroup "errors"
     [ testCase "GCD 6 8 /~ 4" $ testFail1 `throws` testFail1Errors
@@ -307,6 +367,9 @@
     , 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
     ]
   ]
 
@@ -319,6 +382,12 @@
   case result of
     Right _ -> assertFailure "No exception!"
     Left (TypeError msg) ->
-      if all (`isInfixOf` msg) xs
+      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 = "‘’`'"