diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,7 +1,12 @@
 # Changelog for the [`ghc-typelits-natnormalise`](http://hackage.haskell.org/package/ghc-typelits-natnormalise) package
 
+## 0.2 *April 22nd 2015*
+* Finds more unifications:
+  * `(2 + a) ~ 5  ==>  [a := 3]`
+  * `(3 * a) ~ 0  ==>  [a := 0]`
+
 ## 0.1.2 *April 21st 2015*
-* Don't simply expressions with negative exponents
+* Don't simplify expressions with negative exponents
 
 ## 0.1.1 *April 17th 2015*
 * Add workaround for https://ghc.haskell.org/trac/ghc/ticket/10301
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.1.2
+version:             0.2
 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.hs b/src/GHC/TypeLits/Normalise.hs
--- a/src/GHC/TypeLits/Normalise.hs
+++ b/src/GHC/TypeLits/Normalise.hs
@@ -1,5 +1,6 @@
-{-# LANGUAGE TupleSections #-}
-{-# LANGUAGE CPP           #-}
+{-# LANGUAGE CPP             #-}
+{-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE TupleSections   #-}
 
 {-# OPTIONS_HADDOCK show-extensions #-}
 
@@ -52,7 +53,7 @@
 -- GHC API
 import Coercion   (Role (Nominal), mkUnivCo)
 import FastString (fsLit)
-import Outputable (Outputable (..), (<+>), ($$), text)
+import Outputable (Outputable (..), (<+>), ($$), empty, text)
 import Plugins    (Plugin (..), defaultPlugin)
 import TcEvidence (EvTerm (EvCoercion), TcCoercion (..))
 import TcPluginM  (TcPluginM, tcPluginTrace, unsafeTcPluginTcM, zonkCt)
@@ -90,7 +91,7 @@
 plugin = defaultPlugin { tcPlugin = const $ Just normalisePlugin }
 
 normalisePlugin :: TcPlugin
-normalisePlugin =
+normalisePlugin = tracePlugin "ghc-typelits-natnormalise"
   TcPlugin { tcPluginInit  = return ()
            , tcPluginSolve = decideEqualSOP
            , tcPluginStop  = const (return ())
@@ -99,9 +100,9 @@
 decideEqualSOP :: () -> [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginResult
 decideEqualSOP _ _givens _deriveds []      = return (TcPluginOk [] [])
 decideEqualSOP _ givens  _deriveds wanteds = do
-    -- workaround for https://ghc.haskell.org/trac/ghc/ticket/10301
-    initializeStaticFlags
-    let unit_wanteds = mapMaybe toNatEquality wanteds
+    -- 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'
     case unit_wanteds of
       [] -> return (TcPluginOk [] [])
       _  -> do
@@ -189,6 +190,35 @@
 evByFiat :: String -> (Type, Type) -> EvTerm
 evByFiat name (t1,t2) = EvCoercion $ TcCoercion
                       $ mkUnivCo (fsLit name) Nominal t1 t2
+
+tracePlugin :: String -> TcPlugin -> TcPlugin
+tracePlugin s TcPlugin{..} = TcPlugin { tcPluginInit  = traceInit
+                                      , tcPluginSolve = traceSolve
+                                      , tcPluginStop  = traceStop
+                                      }
+  where
+    traceInit    = do -- workaround for https://ghc.haskell.org/trac/ghc/ticket/10301
+                      initializeStaticFlags
+                      tcPluginTrace ("tcPluginInit " ++ s) empty >> tcPluginInit
+    traceStop  z = do -- workaround for https://ghc.haskell.org/trac/ghc/ticket/10301
+                      initializeStaticFlags
+                      tcPluginTrace ("tcPluginStop " ++ s) empty >> tcPluginStop z
+
+    traceSolve z given derived wanted = do
+        -- workaround for https://ghc.haskell.org/trac/ghc/ticket/10301
+        initializeStaticFlags
+        tcPluginTrace ("tcPluginSolve start " ++ s)
+                          (text "given   =" <+> ppr given
+                        $$ text "derived =" <+> ppr derived
+                        $$ text "wanted  =" <+> ppr wanted)
+        r <- tcPluginSolve z given derived wanted
+        case r of
+          TcPluginOk solved new     -> tcPluginTrace ("tcPluginSolve ok " ++ s)
+                                           (text "solved =" <+> ppr solved
+                                         $$ text "new    =" <+> ppr new)
+          TcPluginContradiction bad -> tcPluginTrace ("tcPluginSolve contradiction " ++ s)
+                                           (text "bad =" <+> ppr bad)
+        return r
 
 -- workaround for https://ghc.haskell.org/trac/ghc/ticket/10301
 initializeStaticFlags :: TcPluginM ()
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
@@ -174,6 +174,8 @@
 -- a + b ~ t          ==>  [t := a + b]
 -- (a + c) ~ (b + c)  ==>  \[a := b\]
 -- (2*a) ~ (2*b)      ==>  [a := b]
+-- (2 + a) ~ 5        ==>  [a := 3]
+-- (3 * a) ~ 0        ==>  [a := 0]
 -- @
 --
 -- However, given a wanted:
@@ -182,7 +184,7 @@
 -- [W] t ~ a + b
 -- @
 --
--- this function returns @[]@, or otherwise we \"solve\" the contstraint by
+-- this function returns @[]@, or otherwise we \"solve\" the constraint by
 -- finding a unifier equal to the constraint.
 --
 -- However, given a wanted:
@@ -208,11 +210,25 @@
 unifiers' :: Ct -> CoreSOP -> CoreSOP -> CoreSubst
 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 (S [P [V x]]) s             = [SubstItem x s     ct]
 unifiers' ct s             (S [P [V x]]) = [SubstItem x s     ct]
+
+-- (3 * a) ~ 0 ==> [a := 0]
+unifiers' ct (S [P ((I _):ps)]) (S [P [I 0]]) = unifiers' ct (S [P ps]) (S [P [I 0]])
+unifiers' ct (S [P [I 0]]) (S [P ((I _):ps)]) = unifiers' ct (S [P ps]) (S [P [I 0]])
+
+-- (2*a) ~ (2*b) ==> [a := b]
 unifiers' ct (S [P (p:ps1)]) (S [P (p':ps2)])
-    | p == p'    = unifiers' ct (S [P ps1]) (S [P ps2])
+    | p == p'   = unifiers' ct (S [P ps1]) (S [P ps2])
     | otherwise = []
+
+-- (2 + a) ~ 5 ==> [a := 3]
+unifiers' ct (S ((P [I i]):ps1)) (S ((P [I j]):ps2))
+    | i < j     = unifiers' ct (S ps1) (S ((P [I (j-i)]):ps2))
+    | i > j     = unifiers' ct (S ((P [I (i-j)]):ps1)) (S ps2)
+
+-- (a + c) ~ (b + c) ==> [a := b]
 unifiers' ct (S ps1)       (S ps2)
     | null psx  = []
     | otherwise = unifiers' ct (S (ps1 \\ psx)) (S (ps2 \\ psx))
