diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,9 @@
 # Changelog for the [`ghc-typelits-knownnat`](http://hackage.haskell.org/package/ghc-typelits-knownnat) package
 
+## 0.7.1 *October 8th 2019*
+* Fix [#29](https://github.com/clash-lang/ghc-typelits-knownnat/issues/29)
+* Fix [#30](https://github.com/clash-lang/ghc-typelits-knownnat/issues/30)
+
 ## 0.7 *August 26th 2018*
 * Solve "known" type-level Booleans, also inside `If` (GHC 8.6+)
 
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.7
+version:             0.7.1
 synopsis:            Derive KnownNat constraints from other KnownNat constraints
 description:
   A type checker plugin for GHC that can derive \"complex\" @KnownNat@
@@ -91,7 +91,7 @@
                        ghc-tcplugins-extra       >= 0.3,
                        ghc-typelits-natnormalise >= 0.6      && <0.8,
                        transformers              >= 0.5.2.0  && <0.6,
-                       template-haskell          >= 2.11.0.0 && <2.15
+                       template-haskell          >= 2.11.0.0 && <2.16
   hs-source-dirs:      src
   default-language:    Haskell2010
   if flag(deverror)
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
@@ -150,6 +150,9 @@
 #endif
                    mkNonCanonical, setCtLoc, setCtLocSpan)
 import TcTypeNats (typeNatAddTyCon, typeNatSubTyCon)
+#if MIN_VERSION_ghc(8,4,0)
+import TcTypeNats (typeNatDivTyCon)
+#endif
 import Type
   (EqRel (NomEq), PredTree (ClassPred,EqPred), PredType, classifyPredType,
    dropForAlls, eqType, funResultTy, mkNumLitTy, mkStrLitTy, mkTyConApp,
@@ -491,11 +494,12 @@
           knowns   = mapMaybe (unKn . unCType . fst) givens
           -- Get all the rewritten KNs
           knownsR  = catMaybes $ concatMap (\t -> map (rewriteTy t) rewrites) knowns
+          knownsX  = knowns ++ knownsR
           -- pair up the sum-of-products KnownNat constraints
           -- with the original Nat operation
           subWant  = mkTyConApp typeNatSubTyCon . (:[want])
           exploded = map (fst . runWriter . normaliseNat . subWant &&& id)
-                         (knowns ++ knownsR)
+                         knownsX
           -- 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)
@@ -504,11 +508,27 @@
           interesting = mapMaybe (uncurry examineDiff) exploded
       -- convert the first suitable evidence
       ((h,corr):_) <- pure interesting
-      let x = case corr of
-                I 0 -> h
-                I i | i < 0     -> mkTyConApp typeNatAddTyCon [h,mkNumLitTy (negate i)]
-                    | otherwise -> mkTyConApp typeNatSubTyCon [h,mkNumLitTy i]
-                _ -> mkTyConApp typeNatSubTyCon [h,reifySOP (S [P [corr]])]
+      x <- case corr of
+                I 0 -> pure h
+                I i | i < 0
+                    -> pure (mkTyConApp typeNatAddTyCon [h,mkNumLitTy (negate i)])
+                    | otherwise
+                    -> pure (mkTyConApp typeNatSubTyCon [h,mkNumLitTy i])
+                -- If the offset between a given and a wanted is again the wanted
+                -- then the given is twice the wanted; so we can just divide
+                -- the given by two. Only possible in GHC 8.4+; for 8.2 we simply
+                -- fail because we don't know how to divide.
+                c   | CType (reifySOP (S [P [c]])) == CType want ->
+#if MIN_VERSION_ghc(8,4,0)
+                     pure (mkTyConApp typeNatDivTyCon [h,reifySOP (S [P [I 2]])])
+#else
+                     MaybeT (pure Nothing)
+#endif
+                -- Only solve with a variable offset if we have [G]iven knownnat for it
+                -- Failing to do this check results in #30
+                V v | all (not . eqType (TyVarTy v)) knownsX
+                    -> MaybeT (pure Nothing)
+                _ -> pure (mkTyConApp typeNatSubTyCon [h,reifySOP (S [P [corr]])])
       MaybeT (go x)
 
 makeWantedEv
diff --git a/tests/Main.hs b/tests/Main.hs
--- a/tests/Main.hs
+++ b/tests/Main.hs
@@ -183,6 +183,11 @@
 test27 _ _ = natVal (Proxy :: Proxy (If (n <=? m) n m))
 #endif
 
+#if __GLASGOW_HASKELL__ >= 804
+test28 :: forall m n . (KnownNat m, (2*n) ~ m) => Proxy m -> Natural
+test28 _ = natVal @n Proxy
+#endif
+
 tests :: TestTree
 tests = testGroup "ghc-typelits-natnormalise"
   [ testGroup "Basic functionality"
@@ -219,6 +224,11 @@
     , testCase "KnownNat (y*x*y), x=3 y=4 ~ 48" $
       show (test22 (Proxy @3) (Proxy @4))@?=
       "48"
+#if __GLASGOW_HASKELL__ >= 804
+    , testCase "KnownNat m, 2 * n ~ m, m = 10 ~ 5" $
+      show (test28 (Proxy @10)) @?=
+      "5"
+#endif
     ],
     testGroup "Implications"
     [ testCase "KnownNat m => KnownNat (m*m); @ 5" $