diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,10 @@
 # Changelog for the [`ghc-typelits-natnormalise`](http://hackage.haskell.org/package/ghc-typelits-natnormalise) package
 
+## 0.4.6 *July 21th 2016*
+* Reduce "x^(-y) * x^y" to 1
+* Fixes bugs:
+  * Subtraction in exponent induces infinite loop
+
 ## 0.4.5 *July 20th 2016*
 * Fixes bugs:
   * Reifying negative exponent causes GHC panic
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.4.5
+version:             0.4.6
 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
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
@@ -205,6 +205,20 @@
       (S [P [e]]) -> Left  e
       _           -> Right l
 
+-- x^y * x^(-y) ==> 1
+mergeS (E s1 (P p1)) (E s2 (P (I i:p2)))
+  | i == (-1)
+  , s1 == s2
+  , p1 == p2
+  = Left (I 1)
+
+-- x^(-y) * x^y ==> 1
+mergeS (E s1 (P (I i:p1))) (E s2 (P p2))
+  | i == (-1)
+  , s1 == s2
+  , p1 == p2
+  = Left (I 1)
+
 mergeS l _ = Right l
 
 -- | Merge two products of a SOP term
@@ -259,7 +273,9 @@
   foldr1 mergeSOPMul (replicate (fromInteger i) b)
 
 -- (x + 2)^(2x) ==> (x^2 + 4xy + 4)^x
-normaliseExp b (S [P (e@(I _):es)]) =
+normaliseExp b (S [P (e@(I i):es)]) | i >= 0 =
+  -- Without the "| i >= 0" guard, normaliseExp can loop with itself
+  -- for exponentials such as: 2^(n-k)
   normaliseExp (normaliseExp b (S [P [e]])) (S [P es])
 
 -- (x + 2)^(xy) ==> (x+2)^(xy)
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
@@ -91,21 +91,40 @@
 reifySOP = combineP . map negateP . unS
   where
     negateP :: CoreProduct -> Either CoreProduct CoreProduct
-    negateP (P ((I i):ps)) | i < 0 = Left  (P ((I (abs i)):ps))
-    negateP ps                     = Right ps
+    negateP (P ((I i):ps@(_:_))) | i == (-1) = Left  (P ps)
+    negateP (P ((I i):ps)) | i < 0           = Left  (P ((I (abs i)):ps))
+    negateP ps                               = Right ps
 
     combineP :: [Either CoreProduct CoreProduct] -> Type
     combineP []     = mkNumLitTy 0
     combineP [p]    = either (\p' -> mkTyConApp typeNatSubTyCon
                                                 [mkNumLitTy 0, reifyProduct p'])
                              reifyProduct p
-    combineP (p:ps) = let es = combineP ps
-                      in  either (\x -> mkTyConApp typeNatSubTyCon
-                                                   [es, reifyProduct x])
-                                 (\x -> mkTyConApp typeNatAddTyCon
-                                                  [reifyProduct x, es])
-                                 p
+    combineP [p1,p2] = either
+      (\x -> either
+               -- x neg, y neg
+               (\y -> let r = mkTyConApp typeNatSubTyCon [reifyProduct x
+                                                         ,reifyProduct y]
+                      in  mkTyConApp typeNatSubTyCon [mkNumLitTy 0, r])
+               -- x neg, y pos
+               (\y -> mkTyConApp typeNatSubTyCon [reifyProduct y, reifyProduct x])
+               p2)
+      (\x -> either
+               -- x pos, y neg
+               (\y -> mkTyConApp typeNatSubTyCon [reifyProduct x, reifyProduct y])
+               -- x pos, y pos
+               (\y -> mkTyConApp typeNatAddTyCon [reifyProduct x, reifyProduct y])
+               p2)
+      p1
 
+
+    combineP (p:ps)  = let es = combineP ps
+                       in  either (\x -> mkTyConApp typeNatSubTyCon
+                                                    [es, reifyProduct x])
+                                  (\x -> mkTyConApp typeNatAddTyCon
+                                                   [reifyProduct x, es])
+                                  p
+
 reifyProduct :: CoreProduct -> Type
 reifyProduct (P ps) =
     let ps' = map reifySymbol (foldr mergeExp [] ps)
@@ -113,30 +132,25 @@
   where
     -- "2 ^ -1 * 2 ^ a" must be merged into "2 ^ (a-1)", otherwise GHC barfs
     -- at the "2 ^ -1" because of the negative exponent.
-    mergeExp :: CoreSymbol -> [Either CoreSymbol (CoreSOP,CoreProduct,Integer)]
-                           -> [Either CoreSymbol (CoreSOP,CoreProduct,Integer)]
-    mergeExp (E s1 (P [I i])) (y:ys)
-      | i < 0
-      , Left (E s2 p2) <- y
-      , s1 == s2
-      = Right (s1,p2,negate i) : ys
-      | i < 0
-      , Right (s2,p2,j) <- y
+    mergeExp :: CoreSymbol -> [Either CoreSymbol (CoreSOP,[CoreProduct])]
+                           -> [Either CoreSymbol (CoreSOP,[CoreProduct])]
+    mergeExp (E s p)   []     = [Right (s,[p])]
+    mergeExp (E s1 p1) (y:ys)
+      | Right (s2,p2) <- y
       , s1 == s2
-      = Right (s1,p2,j+negate i) : ys
-    mergeExp x ys = Left x:ys
+      = Right (s1,(p1:p2)) : ys
+      | otherwise
+      = Right (s1,[p1]) : ys
+    mergeExp x ys = Left x : ys
 
-reifySymbol :: Either CoreSymbol (CoreSOP,CoreProduct,Integer) -> Type
+reifySymbol :: Either CoreSymbol (CoreSOP,[CoreProduct]) -> Type
 reifySymbol (Left (I i)  )  = mkNumLitTy i
 reifySymbol (Left (C c)  )  = c
 reifySymbol (Left (V v)  )  = mkTyVarTy v
 reifySymbol (Left (E s p))  = mkTyConApp typeNatExpTyCon [reifySOP s,reifyProduct p]
-reifySymbol (Right (s,p,i)) = mkTyConApp typeNatExpTyCon
-                                         [reifySOP s
-                                         ,mkTyConApp typeNatSubTyCon
-                                                     [reifyProduct p
-                                                     ,mkNumLitTy i
-                                                     ]
+reifySymbol (Right (s1,s2)) = mkTyConApp typeNatExpTyCon
+                                         [reifySOP s1
+                                         ,reifySOP (S s2)
                                          ]
 
 -- | A substitution is essentially a list of (variable, 'SOP') pairs,