diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,15 @@
 # Changelog for the [`ghc-typelits-natnormalise`](http://hackage.haskell.org/package/ghc-typelits-natnormalise) package
 
+## 0.4 *January 19th 2016*
+* Stop using 'provenance' hack to create conditional evidence (GHC 8.0+ only)
+* Find more unifications:
+  * `F x + 2 - 1 - 1 ~ F x` ==> [F x := F x], where `F` can be any type function with result `Nat`.
+
+## 0.3.2
+* Find more unifications:
+  * `(z ^ a) ~ (z ^ b) ==> [a := b]`
+  * `(i ^ a) ~ j ==> [a := round (logBase i j)]`, when `i` and `j` are integers, and `ceiling (logBase i j) == floor (logBase i j)`.
+
 ## 0.3.1 *October 19th 2015*
 * Find more unifications:
   * `(i * a) ~ j ==> [a := div j i]`, when `i` and `j` are integers, and `mod j i == 0`.
diff --git a/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -1,4 +1,4 @@
-Copyright (c) 2015, University of Twente
+Copyright (c) 2015-2016, University of Twente
 All rights reserved.
 
 Redistribution and use in source and binary forms, with or without
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.3.1
+version:             0.4
 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
@@ -41,7 +41,7 @@
 license-file:        LICENSE
 author:              Christiaan Baaij
 maintainer:          christiaan.baaij@gmail.com
-copyright:           Copyright © 2015 University of Twente
+copyright:           Copyright © 2015-2016 University of Twente
 category:            Type System
 build-type:          Simple
 extra-source-files:  README.md
@@ -64,10 +64,14 @@
                        GHC.TypeLits.Normalise.Unify
   Other-Modules:       GHC.Extra.Instances
   build-depends:       base >=4.8  && <5,
-                       ghc  >=7.10 && <7.12,
-                       ghc-tcplugins-extra >= 0.1
+                       ghc  >=7.10 && <8.2,
+                       ghc-tcplugins-extra >= 0.2
   hs-source-dirs:      src
   default-language:    Haskell2010
+  other-extensions:    CPP
+                       LambdaCase
+                       RecordWildCards
+                       TupleSections
   if flag(deverror)
     ghc-options:         -Wall -Werror
   else
@@ -77,11 +81,18 @@
   type:                exitcode-stdio-1.0
   main-is:             Tests.hs
   Other-Modules:       ErrorTests
-  build-depends:       base >=4.8 && <4.9,
-                       ghc-typelits-natnormalise >= 0.1,
+  build-depends:       base >=4.8 && <5,
+                       ghc-typelits-natnormalise >= 0.4,
                        tasty >= 0.10,
                        tasty-hunit >= 0.9
   hs-source-dirs:      tests
   default-language:    Haskell2010
+  other-extensions:    DataKinds
+                       GADTs
+                       KindSignatures
+                       NoImplicitPrelude
+                       TypeFamilies
+                       TypeOperators
+                       ScopedTypeVariables
   if flag(deverror)
     ghc-options:       -O0 -dcore-lint
diff --git a/src/GHC/Extra/Instances.hs b/src/GHC/Extra/Instances.hs
--- a/src/GHC/Extra/Instances.hs
+++ b/src/GHC/Extra/Instances.hs
@@ -1,6 +1,5 @@
-{-# OPTIONS_GHC -fno-warn-orphans #-}
 {-|
-Copyright  :  (C) 2015, University of Twente
+Copyright  :  (C) 2015-2016, University of Twente
 License    :  BSD2 (see the file LICENSE)
 Maintainer :  Christiaan Baaij <christiaan.baaij@gmail.com>
 
@@ -8,9 +7,21 @@
 
 * 'Ord' instance for 'Type' and 'Ct'
 -}
+
+{-# LANGUAGE CPP #-}
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+
 module GHC.Extra.Instances where
 
-import Type          (Type,cmpType)
+import Type (Type,cmpType)
+#if __GLASGOW_HASKELL__ >= 711
+import Type (eqType)
+#endif
+
+#if __GLASGOW_HASKELL__ >= 711
+instance Eq Type where
+  (==) = eqType
+#endif
 
 instance Ord Type where
   compare = cmpType
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
@@ -1,12 +1,5 @@
-{-# LANGUAGE CPP             #-}
-{-# LANGUAGE LambdaCase      #-}
-{-# LANGUAGE RecordWildCards #-}
-{-# LANGUAGE TupleSections   #-}
-
-{-# OPTIONS_HADDOCK show-extensions #-}
-
 {-|
-Copyright  :  (C) 2015, University of Twente
+Copyright  :  (C) 2015-2016, University of Twente
 License    :  BSD2 (see the file LICENSE)
 Maintainer :  Christiaan Baaij <christiaan.baaij@gmail.com>
 
@@ -44,6 +37,18 @@
 
 To the header of your file.
 -}
+
+{-# LANGUAGE CPP             #-}
+{-# LANGUAGE LambdaCase      #-}
+{-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE TupleSections   #-}
+
+{-# OPTIONS_HADDOCK show-extensions #-}
+
+#if __GLASGOW_HASKELL__ < 711
+{-# OPTIONS_GHC -fno-warn-deprecations #-}
+#endif
+
 module GHC.TypeLits.Normalise
   ( plugin )
 where
@@ -51,21 +56,33 @@
 -- external
 import Data.IORef          (IORef, newIORef,readIORef, modifyIORef)
 import Data.Maybe          (catMaybes, mapMaybe)
-import GHC.TcPluginM.Extra (evByFiat, failWithProvenace, newGiven,
-                            newWantedWithProvenance, tracePlugin)
+import GHC.TcPluginM.Extra (evByFiat, newGiven, tracePlugin)
 
 -- GHC API
 import Outputable (Outputable (..), (<+>), ($$), text)
 import Plugins    (Plugin (..), defaultPlugin)
-import TcEvidence (EvTerm)
+import TcEvidence (EvTerm (..))
 import TcPluginM  (TcPluginM, tcPluginIO, tcPluginTrace, zonkCt)
 import TcRnTypes  (Ct, TcPlugin (..), TcPluginResult(..), ctEvidence, ctEvPred,
                    ctPred, ctLoc, isGiven, isWanted, mkNonCanonical)
-import TcType     (mkEqPred, typeKind)
-import Type       (EqRel (NomEq), Kind, PredTree (EqPred), Type, TyVar,
-                   classifyPredType, mkTyVarTy)
+import Type       (EqRel (NomEq), Kind, PredTree (EqPred), PredType, Type, TyVar,
+                   classifyPredType, getEqPredTys, mkTyVarTy)
 import TysWiredIn (typeNatKind)
 
+#if __GLASGOW_HASKELL__ >= 711
+import Coercion   (CoercionHole, Role (..), mkForAllCos, mkHoleCo, mkInstCo,
+                   mkNomReflCo, mkUnivCo)
+import TcPluginM  (newCoercionHole, newFlexiTyVar)
+import TcRnTypes  (CtEvidence (..), TcEvDest (..))
+import TyCoRep    (UnivCoProvenance (..))
+import Type       (mkPrimEqPred)
+import TcType     (typeKind)
+#else
+import TcType              (mkEqPred, typeKind)
+import GHC.TcPluginM.Extra (newWantedWithProvenance, failWithProvenace)
+#endif
+
+
 -- internal
 import GHC.Extra.Instances () -- Ord instance for Ct
 import GHC.TypeLits.Normalise.Unify
@@ -104,7 +121,11 @@
           Simplified subst evs -> do
             let solved     = filter (isWanted . ctEvidence . snd) evs
             -- Create new wanted constraints
+#if __GLASGOW_HASKELL__ >= 711
+            let newWanteds = filter (isWanted . ctEvidence . snd . siNote) subst
+#else
             let newWanteds = filter (isWanted . ctEvidence . siNote) subst
+#endif
             discharedWanteds <- tcPluginIO (readIORef discharged)
             let existingWanteds = wanteds' ++ discharedWanteds
             newWantedConstraints <- catMaybes <$>
@@ -114,10 +135,14 @@
             tcPluginIO (modifyIORef discharged (++ newWantedConstraints))
             -- return
             return (TcPluginOk solved newWantedConstraints)
-          Impossible eq -> failWithProvenace $ fromNatEquality eq
+#if __GLASGOW_HASKELL__ >= 711
+          Impossible eq -> return (TcPluginContradiction [fromNatEquality eq])
+#else
+          Impossible eq -> failWithProvenace (fromNatEquality eq)
+#endif
 
 substItemToCt :: [Ct] -- ^ Existing wanteds wanted
-              -> UnifyItem TyVar Type Ct
+              -> UnifyItem TyVar Type CoreNote
               -> TcPluginM (Maybe Ct)
 substItemToCt existingWanteds si
   | isGiven (ctEvidence ct)
@@ -126,32 +151,57 @@
   -- Only create new wanteds
   | predicate  `notElem` wantedPreds
   , predicateS `notElem` wantedPreds
+#if __GLASGOW_HASKELL__ >= 711
+  = return (Just (mkNonCanonical (CtWanted predicate (HoleDest ev) loc)))
+#else
   = Just <$> mkNonCanonical <$> newWantedWithProvenance (ctEvidence ct) predicate
+#endif
 
   | otherwise
   = return Nothing
   where
-    predicate   = mkEqPred ty1 ty2
+    predicate   = unifyItemToPredType si
+    (ty1,ty2)   = getEqPredTys predicate
+#if __GLASGOW_HASKELL__ >= 711
+    predicateS    = mkPrimEqPred ty2 ty1
+    ((ev,_,_),ct) = siNote si
+#else
     predicateS  = mkEqPred ty2 ty1
+    ct          = siNote si
+#endif
     wantedPreds = map ctPred existingWanteds
 
-    ty1       = case si of
-                  (SubstItem {..}) -> mkTyVarTy siVar
-                  (UnifyItem {..}) -> reifySOP siLHS
-    ty2       = case si of
-                  (SubstItem {..}) -> reifySOP siSOP
-                  (UnifyItem {..}) -> reifySOP siRHS
-    ct        = siNote si
     loc       = ctLoc ct
     evTm      = evByFiat "ghc-typelits-natnormalise" ty1 ty2
 
+unifyItemToPredType :: UnifyItem TyVar Type a -> PredType
+unifyItemToPredType ui =
+#if __GLASGOW_HASKELL__ >= 711
+    mkPrimEqPred ty1 ty2
+#else
+    mkEqPred ty1 ty2
+#endif
+  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)
 
 fromNatEquality :: NatEquality -> Ct
 fromNatEquality (ct, _, _) = ct
 
+#if __GLASGOW_HASKELL__ >= 711
+type CoreNote = ((CoercionHole,TyVar,PredType), Ct)
+#else
+type CoreNote = Ct
+#endif
+
 data SimplifyResult
-  = Simplified CoreUnify [(EvTerm,Ct)]
+  = Simplified (CoreUnify CoreNote) [(EvTerm,Ct)]
   | Impossible NatEquality
 
 instance Outputable SimplifyResult where
@@ -163,20 +213,38 @@
 simplifyNats eqs =
     tcPluginTrace "simplifyNats" (ppr eqs) >> simples [] [] [] eqs
   where
-    simples :: CoreUnify -> [Maybe (EvTerm, Ct)] -> [NatEquality]
+    simples :: CoreUnify CoreNote -> [Maybe (EvTerm, Ct)] -> [NatEquality]
             -> [NatEquality] -> TcPluginM SimplifyResult
     simples subst evs _xs [] = return (Simplified subst (catMaybes evs))
     simples subst evs xs (eq@(ct,u,v):eqs') = do
       ur <- unifyNats ct (substsSOP subst u) (substsSOP subst v)
       tcPluginTrace "unifyNats result" (ppr ur)
       case ur of
+#if __GLASGOW_HASKELL__ >= 711
+        Win         -> simples subst (((,) <$> evMagic ct [] <*> pure ct):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):evs)
+            [] (xs ++ eqs')
+#else
         Win         -> simples subst (((,) <$> evMagic ct <*> pure ct):evs) []
                                (xs ++ eqs')
         Lose        -> return (Impossible eq)
         Draw []     -> simples subst evs (eq:xs) eqs'
-        Draw subst' -> simples (substsSubst subst' subst ++ subst')
-                               (((,) <$> evMagic ct <*> pure ct):evs)
-                               [] (xs ++ eqs')
+        Draw subst' -> do
+          simples (substsSubst subst' subst ++ subst')
+                  (((,) <$> evMagic ct <*> pure ct):evs)
+                  [] (xs ++ eqs')
+#endif
 
 -- Extract the Nat equality constraints
 toNatEquality :: Ct -> Maybe NatEquality
@@ -189,7 +257,22 @@
     isNatKind :: Kind -> Bool
     isNatKind = (== typeNatKind)
 
+#if __GLASGOW_HASKELL__ >= 711
+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
+        natReflCo = mkNomReflCo typeNatKind
+        forallEv = mkForAllCos (map (,natReflCo) tvs) ctEv
+        finalEv = foldl mkInstCo forallEv holeEvs
+    in  Just (EvCoercion finalEv)
+  _ -> Nothing
+#else
 evMagic :: Ct -> Maybe EvTerm
 evMagic ct = case classifyPredType $ ctEvPred $ ctEvidence ct of
   EqPred NomEq t1 t2 -> Just (evByFiat "ghc-typelits-natnormalise" t1 t2)
   _                  -> Nothing
+#endif
diff --git a/src/GHC/TypeLits/Normalise/SOP.hs b/src/GHC/TypeLits/Normalise/SOP.hs
--- a/src/GHC/TypeLits/Normalise/SOP.hs
+++ b/src/GHC/TypeLits/Normalise/SOP.hs
@@ -1,5 +1,5 @@
 {-|
-Copyright  :  (C) 2015, University of Twente
+Copyright  :  (C) 2015-2016, University of Twente
 License    :  BSD2 (see the file LICENSE)
 Maintainer :  Christiaan Baaij <christiaan.baaij@gmail.com>
 
@@ -284,10 +284,12 @@
   . mergeWith mergeP
   . map (P . sort . map reduceExp . mergeWith mergeS . unP)
   . unS
+{-# INLINEABLE simplifySOP #-}
 
 -- | Merge two SOP terms by additions
 mergeSOPAdd :: (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c
 mergeSOPAdd (S sop1) (S sop2) = simplifySOP $ S (sop1 ++ sop2)
+{-# INLINEABLE mergeSOPAdd #-}
 
 -- | Merge two SOP terms by multiplication
 mergeSOPMul :: (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c
@@ -295,3 +297,4 @@
   = simplifySOP
   . S
   $ concatMap (zipWith (\p1 p2 -> P (unP p1 ++ unP p2)) sop1 . repeat) sop2
+{-# INLINEABLE mergeSOPMul #-}
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
@@ -1,11 +1,13 @@
-{-# LANGUAGE RecordWildCards #-}
-{-# OPTIONS_GHC -fno-warn-unused-imports #-}
-
 {-|
-Copyright  :  (C) 2015, University of Twente
+Copyright  :  (C) 2015-2016, University of Twente
 License    :  BSD2 (see the file LICENSE)
 Maintainer :  Christiaan Baaij <christiaan.baaij@gmail.com>
 -}
+
+{-# LANGUAGE CPP             #-}
+{-# LANGUAGE RecordWildCards #-}
+{-# OPTIONS_GHC -fno-warn-unused-imports #-}
+
 module GHC.TypeLits.Normalise.Unify
   ( -- * 'Nat' expressions \<-\> 'SOP' terms
     CoreSOP
@@ -34,10 +36,16 @@
 import Outputable    (Outputable (..), (<+>), ($$), text)
 import TcPluginM     (TcPluginM, tcPluginTrace)
 import TcRnMonad     (Ct, ctEvidence, isGiven)
+import TcRnTypes     (ctEvPred)
 import TcTypeNats    (typeNatAddTyCon, typeNatExpTyCon, typeNatMulTyCon,
                       typeNatSubTyCon)
-import Type          (TyVar, mkNumLitTy, mkTyConApp, mkTyVarTy, tcView)
+import Type          (EqRel (NomEq), PredTree (EqPred), TyVar, classifyPredType,
+                      coreView, mkNumLitTy, mkTyConApp, mkTyVarTy)
+#if __GLASGOW_HASKELL__ >= 711
+import TyCoRep       (Type (..), TyLit (..))
+#else
 import TypeRep       (Type (..), TyLit (..))
+#endif
 import UniqSet       (UniqSet, unionManyUniqSets, emptyUniqSet, unionUniqSets,
                       unitUniqSet)
 
@@ -60,7 +68,7 @@
 -- * type variables
 -- * Applications of the arithmetic operators @(+,-,*,^)@
 normaliseNat :: Type -> CoreSOP
-normaliseNat ty | Just ty1 <- tcView ty = normaliseNat ty1
+normaliseNat ty | Just ty1 <- coreView ty = normaliseNat ty1
 normaliseNat (TyVarTy v)          = S [P [V v]]
 normaliseNat (LitTy (NumTyLit i)) = S [P [I i]]
 normaliseNat (TyConApp tc [x,y])
@@ -105,7 +113,8 @@
 -- | 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     = TyUnify TyVar Type Ct
+type CoreUnify a = TyUnify TyVar Type a
+
 type TyUnify v c n = [UnifyItem v c n]
 
 data UnifyItem v c n = SubstItem { siVar  :: v
@@ -147,13 +156,14 @@
   where
     subt si@(SubstItem {..}) = si {siSOP = substsSOP s siSOP}
     subt si@(UnifyItem {..}) = si {siLHS = substsSOP s siLHS, siRHS = substsSOP s siRHS}
+{-# INLINEABLE substsSubst #-}
 
 -- | 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 -- ^ Two terms are only equal if the given substitution holds
+  | Draw (CoreUnify Ct) -- ^ Two terms are only equal if the given substitution holds
 
 instance Outputable UnifyResult where
   ppr Win          = text "Win"
@@ -172,12 +182,15 @@
 
 unifyNats' :: Ct -> CoreSOP -> CoreSOP -> UnifyResult
 unifyNats' ct u v
-  | eqFV u v
-  , not (containsConstants u)
-  , not (containsConstants v)
-  = if u == v then Win else Lose
-  | otherwise
-  = Draw (unifiers ct u v)
+  = if eqFV u v
+       then if containsConstants u || containsConstants v
+               then if u == v
+                       then Win
+                       else Draw (unifiers ct u v)
+               else if u == v
+                       then Win
+                       else Lose
+       else Draw (unifiers ct u v)
 
 -- | Find unifiers for two SOP terms
 --
@@ -212,18 +225,30 @@
 -- @
 -- [a := b]
 -- @
-unifiers :: Ct -> CoreSOP -> CoreSOP -> CoreUnify
-unifiers ct (S [P [V x]]) s
-  | isGiven (ctEvidence ct) = [SubstItem x s ct]
-  | otherwise               = []
-unifiers ct s (S [P [V x]])
-  | isGiven (ctEvidence ct) = [SubstItem x s ct]
-  | otherwise               = []
-unifiers _ (S [P [C _]]) _  = []
-unifiers _ _ (S [P [C _]])  = []
+unifiers :: Ct -> CoreSOP -> CoreSOP -> CoreUnify Ct
+unifiers ct u@(S [P [V x]]) v
+  = case classifyPredType $ ctEvPred $ ctEvidence ct of
+      EqPred NomEq t1 _
+        | reifySOP u /= t1 || isGiven (ctEvidence ct) -> [SubstItem x v ct]
+      _ -> []
+unifiers ct u v@(S [P [V x]])
+  = case classifyPredType $ ctEvPred $ ctEvidence ct of
+      EqPred NomEq _ t2
+        | reifySOP v /= t2 || isGiven (ctEvidence ct) -> [SubstItem x u ct]
+      _ -> []
+unifiers ct u@(S [P [C _]]) v
+  = case classifyPredType $ ctEvPred $ ctEvidence ct of
+      EqPred NomEq t1 t2
+        | reifySOP u /= t1 || reifySOP v /= t2 -> [UnifyItem u v ct]
+      _ -> []
+unifiers ct u v@(S [P [C _]])
+  = case classifyPredType $ ctEvPred $ ctEvidence ct of
+      EqPred NomEq t1 t2
+        | reifySOP u /= t1 || reifySOP v /= t2 -> [UnifyItem u v ct]
+      _ -> []
 unifiers ct u v             = unifiers' ct u v
 
-unifiers' :: Ct -> CoreSOP -> CoreSOP -> CoreUnify
+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]
 
@@ -232,6 +257,31 @@
 
 unifiers' ct s1@(S [P [C _]]) s2               = [UnifyItem s1 s2 ct]
 unifiers' ct s1               s2@(S [P [C _]]) = [UnifyItem s1 s2 ct]
+
+
+-- (z ^ a) ~ (z ^ b) ==> [a := b]
+unifiers' ct (S [P [E s1 p1]]) (S [P [E s2 p2]])
+  | s1 == s2 = unifiers' ct (S [p1]) (S [p2])
+
+-- (i ^ a) ~ j ==> [a := round (logBase i j)], when `i` and `j` are integers,
+-- and `ceiling (logBase i j) == floor (logBase i j)`
+unifiers' ct (S [P [E (S [P [I i]]) p]]) (S [P [I j]])
+    = if kC == kF
+         then unifiers' ct (S [p]) (S [P [I kC]])
+         else []
+  where
+    k  = logBase (fromInteger i :: Double) (fromInteger j)
+    kC = ceiling k :: Integer
+    kF = floor k :: Integer
+
+unifiers' ct (S [P [I j]]) (S [P [E (S [P [I i]]) p]])
+    = if kC == kF
+         then unifiers' ct (S [p]) (S [P [I kC]])
+         else []
+  where
+    k  = logBase (fromInteger i :: Double) (fromInteger j)
+    kC = ceiling k :: Integer
+    kF = floor k :: Integer
 
 -- (i * a) ~ j ==> [a := div j i]
 -- Where 'a' is a variable, 'i' and 'j' are integer literals, and j `mod` i == 0
diff --git a/tests/ErrorTests.hs b/tests/ErrorTests.hs
--- a/tests/ErrorTests.hs
+++ b/tests/ErrorTests.hs
@@ -56,3 +56,25 @@
   ["Expected type: Proxy 7 -> ()"
   ,"Actual type: Proxy ((2 * y1) + 4) -> ()"
   ]
+
+proxyFun6 :: Proxy (2^k) -> Proxy (2^k)
+proxyFun6 = const Proxy
+
+testProxy6 :: Proxy 7
+testProxy6 = proxyFun6 (Proxy :: Proxy 7)
+
+testProxy6Errors =
+  ["Expected type: Proxy (2 ^ k0)"
+  ,"Actual type: Proxy 7"
+  ]
+
+proxyFun7 :: Proxy (2^k) -> Proxy k
+proxyFun7 = const Proxy
+
+testProxy8 :: Proxy x -> Proxy (y + x)
+testProxy8 = id
+
+testProxy8Errors =
+  ["Expected type: Proxy x -> Proxy (y + x)"
+  ,"Actual type: Proxy x -> Proxy x"
+  ]
diff --git a/tests/Tests.hs b/tests/Tests.hs
--- a/tests/Tests.hs
+++ b/tests/Tests.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE CPP                 #-}
 {-# LANGUAGE DataKinds           #-}
 {-# LANGUAGE GADTs               #-}
 {-# LANGUAGE KindSignatures      #-}
@@ -7,13 +8,13 @@
 
 {-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}
 
-import Data.Proxy
 import GHC.TypeLits
 import Unsafe.Coerce
 import Prelude hiding (head,tail,init,(++),splitAt,concat,drop)
 import qualified Prelude as P
 
 import Data.List (isInfixOf)
+import Data.Proxy
 import Control.Exception
 import Test.Tasty
 import Test.Tasty.HUnit
@@ -27,7 +28,7 @@
 instance Show a => Show (Vec n a) where
   show vs = "<" P.++ punc vs P.++ ">"
     where
-      punc :: Show a => Vec m a -> String
+      punc :: Vec m a -> String
       punc Nil        = ""
       punc (x :> Nil) = show x
       punc (x :> xs)  = show x P.++ "," P.++ punc xs
@@ -266,6 +267,9 @@
     , testCase "show (proxyFun4 (Proxy :: Proxy 8))" $
       show (proxyFun4 (Proxy :: Proxy 8)) @?=
       "()"
+    , testCase "show (proxyFun7 (Proxy :: Proxy 8) :: Proxy 3)" $
+      show (proxyFun7 (Proxy :: Proxy 8) :: Proxy 3) @?=
+      "Proxy"
     ]
   , testGroup "errors"
     [ testCase "x + 2 ~ 3 + x" $ testProxy1 `throws` testProxy1Errors
@@ -273,6 +277,8 @@
     , 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
     ]
   ]
 
@@ -280,6 +286,15 @@
 -- an exception whose string representation contains the given
 -- substrings.
 throws :: a -> [String] -> Assertion
-throws v xs =
-  (evaluate v >> assertFailure "No exception!")
-  `catch` \ (e :: SomeException) -> if all (`isInfixOf` show e) xs then return () else throw e
+throws v xs = do
+  result <- try (evaluate v)
+  case result of
+    Right _ -> assertFailure "No exception!"
+#if MIN_VERSION_base(4,9,0)
+    Left (TypeError msg) ->
+#else
+    Left (ErrorCall msg) ->
+#endif
+      if all (`isInfixOf` msg) xs
+         then return ()
+         else assertFailure msg