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.6.2 *July 10th 2018*
+* Add support for GHC 8.6.1-alpha1
+* Solve larger inequalities from smaller inequalities, e.g.
+  * `a <= n` implies `a <= n + 1`
+
 ## 0.6.1 *May 9th 2018*
 * Stop solving `x + y ~ a + b` by asking GHC to solve `x ~ a` and `y ~ b` as
   this leads to a situation where we find a solution that is not the most
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.6.1
+version:             0.6.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
@@ -49,7 +49,7 @@
                      CHANGELOG.md
 cabal-version:       >=1.10
 tested-with:         GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.1, GHC == 8.4.2,
-                     GHC == 8.5.0
+                     GHC == 8.6
 
 source-repository head
   type: git
@@ -66,7 +66,7 @@
                        GHC.TypeLits.Normalise.SOP,
                        GHC.TypeLits.Normalise.Unify
   build-depends:       base                >=4.9   && <5,
-                       ghc                 >=8.0.1 && <8.6,
+                       ghc                 >=8.0.1 && <8.8,
                        ghc-tcplugins-extra >=0.3,
                        integer-gmp         >=1.0   && <1.1,
                        transformers        >=0.5.2.0 && < 0.6
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
@@ -156,7 +156,9 @@
 
 -- external
 import Control.Arrow       (second)
+#if !MIN_VERSION_ghc(8,4,1)
 import Control.Monad       (replicateM)
+#endif
 import Control.Monad.Trans.Writer.Strict
 import Data.Either         (rights)
 import Data.List           (intersect)
@@ -172,6 +174,9 @@
 #endif
 import Outputable (Outputable (..), (<+>), ($$), text)
 import Plugins    (Plugin (..), defaultPlugin)
+#if MIN_VERSION_ghc(8,6,0)
+import Plugins    (purePlugin)
+#endif
 import TcEvidence (EvTerm (..))
 #if !MIN_VERSION_ghc(8,4,0)
 import TcPluginM  (zonkCt)
@@ -211,7 +216,13 @@
 --
 -- To the header of your file.
 plugin :: Plugin
-plugin = defaultPlugin { tcPlugin = go }
+plugin
+  = defaultPlugin
+  { tcPlugin = go
+#if MIN_VERSION_ghc(8,6,0)
+  , pluginRecompile = purePlugin
+#endif
+  }
  where
   go ["allow-negated-numbers"] = Just (normalisePlugin True)
   go _ = Just (normalisePlugin False)
@@ -386,9 +397,9 @@
     isNatKind :: Kind -> Bool
     isNatKind = (`eqType` typeNatKind)
 
-unifyItemToPredType :: CoreUnify -> PredType
+unifyItemToPredType :: CoreUnify -> (PredType,Kind)
 unifyItemToPredType ui =
-    mkPrimEqPred ty1 ty2
+    (mkPrimEqPred ty1 ty2,typeNatKind)
   where
     ty1 = case ui of
             SubstItem {..} -> mkTyVarTy siVar
@@ -397,24 +408,24 @@
             SubstItem {..} -> reifySOP siSOP
             UnifyItem {..} -> reifySOP siRHS
 
-evMagic :: Ct -> [PredType] -> TcPluginM (Maybe ((EvTerm, Ct), [Ct]))
+evMagic :: Ct -> [(PredType,Kind)] -> TcPluginM (Maybe ((EvTerm, Ct), [Ct]))
 evMagic ct preds = case classifyPredType $ ctEvPred $ ctEvidence ct of
   EqPred NomEq t1 t2 -> do
+    let predTypes = map fst preds
+        predKinds = map snd preds
 #if MIN_VERSION_ghc(8,4,1)
-    holes <- mapM (newCoercionHole . uncurry mkPrimEqPred . getEqPredTys) preds
+    holes <- mapM (newCoercionHole . uncurry mkPrimEqPred . getEqPredTys) predTypes
 #else
     holes <- replicateM (length preds) newCoercionHole
 #endif
-    let newWanted = zipWith (unifyItemToCt (ctLoc ct)) preds holes
+    let newWanted = zipWith (unifyItemToCt (ctLoc ct)) predTypes holes
         ctEv      = mkUnivCo (PluginProv "ghc-typelits-natnormalise") Nominal t1 t2
 #if MIN_VERSION_ghc(8,4,1)
         holeEvs   = map mkHoleCo holes
 #else
-        holeEvs   = zipWith (\h p -> uncurry (mkHoleCo h Nominal) (getEqPredTys p)) holes preds
+        holeEvs   = zipWith (\h p -> uncurry (mkHoleCo h Nominal) (getEqPredTys p)) holes predTypes
 #endif
-        natReflCo = mkNomReflCo typeNatKind
-        natCoBndr = (,natReflCo) <$> (newFlexiTyVar typeNatKind)
-    forallEv <- mkForAllCos <$> (replicateM (length preds) natCoBndr) <*> pure ctEv
+    forallEv <- mkForAllCos <$> (mapM mkCoVar predKinds) <*> pure ctEv
     let finalEv = foldl mkInstCo forallEv holeEvs
 #if MIN_VERSION_ghc(8,5,0)
     return (Just ((EvExpr (Coercion finalEv), ct),newWanted))
@@ -422,6 +433,10 @@
     return (Just ((EvCoercion finalEv, ct),newWanted))
 #endif
   _ -> return Nothing
+  where
+    mkCoVar k = (,natReflCo) <$> (newFlexiTyVar k)
+      where
+        natReflCo = mkNomReflCo k
 
 unifyItemToCt :: CtLoc
               -> PredType
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
@@ -62,8 +62,8 @@
 import Type          (EqRel (NomEq), PredTree (EqPred), TyVar, classifyPredType,
                       coreView, eqType, mkNumLitTy, mkTyConApp, mkTyVarTy,
                       nonDetCmpType, PredType, mkPrimEqPred)
-import TyCoRep       (Type (..), TyLit (..))
-import TysWiredIn    (promotedTrueDataCon)
+import TyCoRep       (Kind, Type (..), TyLit (..))
+import TysWiredIn    (boolTy, promotedTrueDataCon)
 import UniqSet       (UniqSet, unionManyUniqSets, emptyUniqSet, unionUniqSets,
                       unitUniqSet)
 
@@ -222,10 +222,11 @@
 
 subtractionToPred
   :: (Type,Type)
-  -> PredType
+  -> (PredType, Kind)
 subtractionToPred (x,y) =
-  mkPrimEqPred (mkTyConApp typeNatLeqTyCon [y,x])
-               (mkTyConApp promotedTrueDataCon [])
+  (mkPrimEqPred (mkTyConApp typeNatLeqTyCon [y,x])
+                (mkTyConApp promotedTrueDataCon [])
+  ,boolTy)
 
 -- | A substitution is essentially a list of (variable, 'SOP') pairs,
 -- but we keep the original 'Ct' that lead to the substitution being
@@ -607,6 +608,7 @@
   , powMonotone
   , pow2MonotoneSpecial
   , haveSmaller
+  , haveBigger
   ]
 
 -- | Transitivity of inequality
@@ -660,6 +662,21 @@
   | (S [P [I 1]], S [P (I _:p@(_:_))],True) <- have
   = [(want,(S [P [I 1]],S [P p],True))]
 haveSmaller _ _ = []
+
+-- | Make the `b` of a given `a <= b` bigger
+haveBigger :: IneqRule
+haveBigger want have
+  | (_,S vs,True) <- want
+  , (as,S bs,True) <- have
+  , let vs' = vs \\ bs
+  , not (null vs')
+  -- want : a <= x + 1
+  -- have : y <= x
+  --
+  -- new want: want
+  -- new have: y <= x + 1
+  = [(want,(as,mergeSOPAdd (S bs) (S vs'),True))]
+haveBigger _ _ = []
 
 -- | Monotonicity of multiplication
 timesMonotone :: IneqRule
diff --git a/tests/ErrorTests.hs b/tests/ErrorTests.hs
--- a/tests/ErrorTests.hs
+++ b/tests/ErrorTests.hs
@@ -1,5 +1,10 @@
+{-# LANGUAGE CPP #-}
 {-# LANGUAGE DataKinds, GADTs, KindSignatures, ScopedTypeVariables, TemplateHaskell,
              TypeApplications, TypeFamilies, TypeOperators #-}
+
+#if __GLASGOW_HASKELL__ >= 805
+{-# LANGUAGE NoStarIsType #-}
+#endif
 
 {-# OPTIONS_GHC -fdefer-type-errors #-}
 {-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}
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,6 +8,10 @@
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications    #-}
 
+#if __GLASGOW_HASKELL__ >= 805
+{-# LANGUAGE NoStarIsType #-}
+#endif
+
 {-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}
 
 import GHC.TypeLits
@@ -14,6 +19,7 @@
 import Prelude hiding (head,tail,init,(++),splitAt,concat,drop)
 import qualified Prelude as P
 
+import Data.Kind (Type)
 import Data.List (isInfixOf)
 import Data.Proxy
 import Control.Exception
@@ -22,7 +28,7 @@
 
 import ErrorTests
 
-data Vec :: Nat -> * -> * where
+data Vec :: Nat -> Type -> Type where
   Nil  :: Vec 0 a
   (:>) :: a -> Vec n a -> Vec (n + 1) a
 
@@ -55,7 +61,7 @@
 snatToInteger :: SNat n -> Integer
 snatToInteger (SNat p) = natVal p
 
-data UNat :: Nat -> * where
+data UNat :: Nat -> Type where
   UZero :: UNat 0
   USucc :: UNat n -> UNat (n + 1)
 
@@ -270,7 +276,7 @@
   -> r
 leToPlus _ a f = f @ (n-k) a
 
-data BNat :: Nat -> * where
+data BNat :: Nat -> Type where
   BT :: BNat 0
   B0 :: BNat n -> BNat (2*n)
   B1 :: BNat n -> BNat ((2*n) + 1)
@@ -356,6 +362,14 @@
   -> Proxy n
 proxyInEqImplication2 _ _ _ x = x
 
+data AtMost n = forall a. (KnownNat a, a <= n) => AtMost (Proxy a)
+
+instance Show (AtMost n) where
+  show (AtMost (x :: Proxy a)) = "AtMost " P.++ show (natVal x)
+
+succAtMost :: AtMost n -> AtMost (n + 1)
+succAtMost (AtMost (Proxy :: Proxy a)) = AtMost (Proxy :: Proxy a)
+
 main :: IO ()
 main = defaultMain tests
 
@@ -438,6 +452,9 @@
     , testCase "`x + 2 <= y` implies `x <= y` and `2 <= y`" $
       show (proxyInEqImplication2 (Proxy :: Proxy 3) (Proxy :: Proxy 2) (Proxy :: Proxy 2) Proxy) @?=
       "Proxy"
+    , testCase "`a <= n` implies `a <= (n+1)`" $
+      show (succAtMost (AtMost (Proxy :: Proxy 3) :: AtMost 5)) @?=
+      "AtMost 3"
     ]
   , testGroup "errors"
     [ testCase "x + 2 ~ 3 + x" $ testProxy1 `throws` testProxy1Errors