diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,8 @@
 # Changelog for the [`ghc-typelits-knownnat`](http://hackage.haskell.org/package/ghc-typelits-knownnat) package
 
+## 0.5 *May 9th 2018*
+* Fix Inferred constraint is too strong [#19](https://github.com/clash-lang/ghc-typelits-knownnat/issues/19)
+
 ## 0.4.2 *April 15th 2018*
 * Add support for GHC 8.5.20180306
 
diff --git a/ghc-typelits-knownnat.cabal b/ghc-typelits-knownnat.cabal
--- a/ghc-typelits-knownnat.cabal
+++ b/ghc-typelits-knownnat.cabal
@@ -1,5 +1,5 @@
 name:                ghc-typelits-knownnat
-version:             0.4.2
+version:             0.5
 synopsis:            Derive KnownNat constraints from other KnownNat constraints
 description:
   A type checker plugin for GHC that can derive \"complex\" @KnownNat@
@@ -87,8 +87,8 @@
                        ViewPatterns
   build-depends:       base                      >= 4.9      && <5,
                        ghc                       >= 8.0.1    && <8.6,
-                       ghc-tcplugins-extra       >= 0.2.5,
-                       ghc-typelits-natnormalise >= 0.5.10   && <0.6,
+                       ghc-tcplugins-extra       >= 0.3,
+                       ghc-typelits-natnormalise >= 0.6      && <0.7,
                        transformers              >= 0.5.2.0  && <0.6,
                        template-haskell          >= 2.11.0.0 && <2.14
   hs-source-dirs:      src
@@ -104,7 +104,7 @@
   Other-Modules:       TestFunctions
   build-depends:       base                      >= 4.8   && <5,
                        ghc-typelits-knownnat,
-                       ghc-typelits-natnormalise >= 0.5.10 && <0.6,
+                       ghc-typelits-natnormalise >= 0.6   && <0.7,
                        tasty                     >= 0.10,
                        tasty-hunit               >= 0.9,
                        tasty-quickcheck          >= 0.8
diff --git a/src/GHC/TypeLits/KnownNat.hs b/src/GHC/TypeLits/KnownNat.hs
--- a/src/GHC/TypeLits/KnownNat.hs
+++ b/src/GHC/TypeLits/KnownNat.hs
@@ -115,12 +115,12 @@
 import Data.Proxy             (Proxy (..))
 #if MIN_VERSION_ghc(8,2,0)
 import GHC.TypeNats
-  (KnownNat, Nat, type (+), type (*), type (^), type (-), type (<=), natVal)
+  (KnownNat, Nat, type (+), type (*), type (^), type (-), natVal, type (<=))
 import GHC.TypeLits           (Symbol)
 import Numeric.Natural        (Natural)
 #else
 import GHC.TypeLits           (KnownNat, Nat, Symbol, type (+), type (*),
-                               type (^), type (-), type (<=), natVal)
+                               type (^), type (-), natVal, type (<=))
 #endif
 
 import GHC.TypeLits.KnownNat.TH
diff --git a/src/GHC/TypeLits/KnownNat/Solver.hs b/src/GHC/TypeLits/KnownNat/Solver.hs
--- a/src/GHC/TypeLits/KnownNat/Solver.hs
+++ b/src/GHC/TypeLits/KnownNat/Solver.hs
@@ -98,6 +98,7 @@
 -- external
 import Control.Arrow                ((&&&), first)
 import Control.Monad.Trans.Maybe    (MaybeT (..))
+import Control.Monad.Trans.Writer.Strict
 import Data.Maybe                   (catMaybes,mapMaybe)
 import GHC.TcPluginM.Extra          (lookupModule, lookupName, newWanted,
                                      tracePlugin)
@@ -257,7 +258,8 @@
   -- GHC 7.10 puts deriveds with the wanteds, so filter them out
   let wanteds'   = filter (isWanted . ctEvidence) wanteds
 #if MIN_VERSION_ghc(8,4,0)
-      subst      = mkSubst' givens
+      subst      = map fst
+                 $ mkSubst' givens
       kn_wanteds = map (\(x,y,z) -> (x,y,substType subst z))
                  $ mapMaybe toKnConstraint wanteds'
 #else
@@ -268,7 +270,7 @@
     _  -> do
       -- Make a lookup table for all the [G]iven constraints
 #if MIN_VERSION_ghc(8,4,0)
-      let given_map = map toGivenEntry (givens ++ flattenGivens givens)
+      let given_map = map toGivenEntry (flattenGivens givens)
 #else
       given_map <- mapM (fmap toGivenEntry . zonkCt) givens
 #endif
@@ -304,11 +306,6 @@
 #endif
                   in  (CType c_ty,ev)
 
--- | Normalise a type to Sum-of-Product type form as defined in the
--- `ghc-typelits-natnormalise` package.
-normaliseSOP :: Type -> Type
-normaliseSOP = reifySOP . normaliseNat
-
 -- | Find the \"magic\" classes and instances in "GHC.TypeLits.KnownNat"
 lookupKnownNatDefs :: TcPluginM KnownNatDefs
 lookupKnownNatDefs = do
@@ -346,17 +343,15 @@
   -> TcPluginM (Maybe ((EvTerm,Ct),[Ct]))
 #endif
 constraintToEvTerm defs givens (ct,cls,op) = do
-    -- 1. Normalise to SOP normal form
-    let ty = normaliseSOP op
-    -- 2. Determine if we are an offset apart from a [G]iven constraint
-    offsetM <- offset ty
+    -- 1. Determine if we are an offset apart from a [G]iven constraint
+    offsetM <- offset op
     evM     <- case offsetM of
                  -- 3.a If so, we are done
                  found@Just {} -> return found
                  -- 3.b If not, we check if the outer type-level operation
                  -- has a corresponding KnownNat<N> instance.
-                 _ -> go ty
-    return (first (,ct) <$> evM)
+                 _ -> go op
+    return ((first (,ct)) <$> evM)
   where
     -- Determine whether the outer type-level operation has a corresponding
     -- KnownNat<N> instance, where /N/ corresponds to the arity of the
@@ -411,20 +406,8 @@
     go_arg ty = case lookup (CType ty) givens of
       Just ev -> return (ev,[])
       _ -> do
-        -- Create a new wanted constraint
-        wantedCtEv <- newWanted (ctLoc ct) ty
-#if MIN_VERSION_ghc(8,5,0)
-        let ev      = ctEvExpr wantedCtEv
-#else
-        let ev      = ctEvTerm wantedCtEv
-#endif
-            wanted  = mkNonCanonical wantedCtEv
-        -- Set the source-location of the new wanted constraint to the source
-        -- location of the [W]anted constraint we are currently trying to solve
-        let ct_ls   = ctLocSpan (ctLoc ct)
-            ctl     = ctEvLoc  wantedCtEv
-            wanted' = setCtLoc wanted (setCtLocSpan ctl ct_ls)
-        return (ev,[wanted'])
+        (ev,wanted) <- makeWantedEv ct ty
+        return (ev,[wanted])
 
     -- Fall through case: look up the normalised [W]anted constraint in the list
     -- of [G]iven constraints.
@@ -471,7 +454,8 @@
           -- pair up the sum-of-products KnownNat constraints
           -- with the original Nat operation
           subWant  = mkTyConApp typeNatSubTyCon . (:[want])
-          exploded = map (normaliseNat . subWant &&& id) (knowns ++ knownsR)
+          exploded = map (fst . runWriter . normaliseNat . subWant &&& id)
+                         (knowns ++ knownsR)
           -- interesting cases for us are those where
           -- wanted and given only differ by a constant
           examineDiff (S [P [I n]]) entire = Just (entire,I n)
@@ -486,6 +470,30 @@
                     | otherwise -> mkTyConApp typeNatSubTyCon [h,mkNumLitTy i]
                 _ -> mkTyConApp typeNatSubTyCon [h,reifySOP (S [P [corr]])]
       MaybeT (go x)
+
+makeWantedEv
+  :: Ct
+  -> Type
+#if MIN_VERSION_ghc(8,5,0)
+  -> TcPluginM (EvExpr,Ct)
+#else
+  -> TcPluginM (EvTerm,Ct)
+#endif
+makeWantedEv ct ty = do
+  -- Create a new wanted constraint
+  wantedCtEv <- newWanted (ctLoc ct) ty
+#if MIN_VERSION_ghc(8,5,0)
+  let ev      = ctEvExpr wantedCtEv
+#else
+  let ev      = ctEvTerm wantedCtEv
+#endif
+      wanted  = mkNonCanonical wantedCtEv
+      -- Set the source-location of the new wanted constraint to the source
+      -- location of the [W]anted constraint we are currently trying to solve
+      ct_ls   = ctLocSpan (ctLoc ct)
+      ctl     = ctEvLoc  wantedCtEv
+      wanted' = setCtLoc wanted (setCtLocSpan ctl ct_ls)
+  return (ev,wanted')
 
 {- |
 Given:
diff --git a/tests/Main.hs b/tests/Main.hs
--- a/tests/Main.hs
+++ b/tests/Main.hs
@@ -159,7 +159,7 @@
 test22 :: forall x y . (KnownNat x, KnownNat y) => Proxy x -> Proxy y -> Number
 test22 _ _ = natVal (Proxy :: Proxy (y*x*y))
 
-test23 :: SNat addrSize -> SNat ((addrSize + 1) - (addrSize - 1))
+test23 :: (1 <= addrSize) => SNat addrSize -> SNat ((addrSize + 1) - (addrSize - 1))
 test23 SNat = SNat
 
 test24 :: (KnownNat n, n ~ (m+1)) => proxy m -> Number