diff --git a/src/Data/Type/Natural/Core.hs b/src/Data/Type/Natural/Core.hs
--- a/src/Data/Type/Natural/Core.hs
+++ b/src/Data/Type/Natural/Core.hs
@@ -48,6 +48,7 @@
     sZero,
     sOne,
     Equality (..),
+    equalAbsurdFromBool,
     type (===),
     (%~),
     sFlipOrdering,
@@ -122,12 +123,17 @@
       then Just trustMe
       else Nothing
 
+-- | Since 1.1.0.0 (Type changed)
 data Equality n m where
   Equal :: ((n == n) ~ 'True) => Equality n n
   NonEqual ::
-    ((n === m) ~ 'False, (n == m) ~ 'False, Empty (n :~: m)) =>
+    ((n === m) ~ 'False, (n == m) ~ 'False) =>
     Equality n m
 
+equalAbsurdFromBool ::
+  (x === y) ~ 'False => x :~: y -> a
+equalAbsurdFromBool = \case
+
 type family a === b where
   a === a = 'True
   _ === _ = 'False
@@ -185,9 +191,9 @@
 
 viewNat :: forall n. SNat n -> ZeroOrSucc n
 viewNat n =
-  case n `testEquality` sNat @0 of
-    Just Refl -> IsZero
-    Nothing -> gcastWith (trustMe @(1 <=? n) @ 'True) $ IsSucc (sPred n)
+  case n %~ sNat @0 of
+    Equal -> IsZero
+    NonEqual -> IsSucc (sPred n)
 
 type family FlipOrdering ord where
   FlipOrdering 'LT = 'GT
diff --git a/src/Data/Type/Natural/Lemma/Order.hs b/src/Data/Type/Natural/Lemma/Order.hs
--- a/src/Data/Type/Natural/Lemma/Order.hs
+++ b/src/Data/Type/Natural/Lemma/Order.hs
@@ -502,16 +502,17 @@
           === SLT `because` ih
 
 cmpSuccStepR ::
+  forall n m.
   SNat n ->
   SNat m ->
   CmpNat n m :~: 'LT ->
   CmpNat n (Succ m) :~: 'LT
-cmpSuccStepR = proofCmpSuccStepR . induction base step
+cmpSuccStepR = \sn -> proofCmpSuccStepR (induction base step sn) @m
   where
     base :: CmpSuccStepR 0
     base = CmpSuccStepR $ \m _ -> cmpZero m
 
-    step :: SNat n -> CmpSuccStepR n -> CmpSuccStepR (Succ n)
+    step :: SNat x -> CmpSuccStepR x -> CmpSuccStepR (Succ x)
     step n (CmpSuccStepR ih) = CmpSuccStepR $ \m snltm ->
       case zeroOrSucc m of
         IsZero -> absurd $ zeroNoLT (sSucc n) snltm
@@ -579,26 +580,26 @@
           n'LTm' = cmpSucc n' m' `trans` compareCongR n (sym sm'EQm) `trans` nLTm
        in gcastWith (sym sm'EQm) $ LeqSucc n' m' $ ltToLeq n' m' n'LTm'
 
-leqWitness :: SNat n -> SNat m -> IsTrue (n <=? m) -> DiffNat n m
-leqWitness = leqWitPf . induction base step
+leqWitness :: forall n m. SNat n -> SNat m -> IsTrue (n <=? m) -> DiffNat n m
+leqWitness = \sn -> leqWitPf (induction base step sn) @m
   where
     base :: LeqWitPf 0
     base = LeqWitPf $ \sm _ -> gcastWith (plusZeroL sm) $ DiffNat sZero sm
 
-    step :: SNat n -> LeqWitPf n -> LeqWitPf (Succ n)
-    step (n :: SNat n) (LeqWitPf ih) = LeqWitPf $ \m snLEQm ->
+    step :: SNat x -> LeqWitPf x -> LeqWitPf (Succ x)
+    step (n :: SNat x) (LeqWitPf ih) = LeqWitPf $ \m snLEQm ->
       case viewLeq (sSucc n) m snLEQm of
         LeqZero _ -> absurd $ succNonCyclic n Refl
         LeqSucc (_ :: SNat n') pm nLEQpm ->
-          succDiffNat n pm $ ih pm $ coerceLeqL (succInj Refl :: n' :~: n) pm nLEQpm
+          succDiffNat n pm $ ih pm $ coerceLeqL (succInj Refl :: n' :~: x) pm nLEQpm
 
-leqStep :: SNat n -> SNat m -> SNat l -> n + l :~: m -> IsTrue (n <=? m)
-leqStep = leqStepPf . induction base step
+leqStep :: forall n m l. SNat n -> SNat m -> SNat l -> n + l :~: m -> IsTrue (n <=? m)
+leqStep sn = leqStepPf (induction base step sn) @m @l
   where
     base :: LeqStepPf 0
     base = LeqStepPf $ \k _ _ -> leqZero k
 
-    step :: SNat n -> LeqStepPf n -> LeqStepPf (Succ n)
+    step :: forall k. SNat k -> LeqStepPf k -> LeqStepPf (Succ k)
     step n (LeqStepPf ih) =
       LeqStepPf $ \k l snPlEqk ->
         let kEQspk =
diff --git a/src/Data/Type/Natural/Presburger/MinMaxSolver.hs b/src/Data/Type/Natural/Presburger/MinMaxSolver.hs
--- a/src/Data/Type/Natural/Presburger/MinMaxSolver.hs
+++ b/src/Data/Type/Natural/Presburger/MinMaxSolver.hs
@@ -1,3 +1,5 @@
+{-# LANGUAGE CPP #-}
+
 {- | This module provides a variant of `ghc-typelits-presburger`,
  which can be also solve symbols added in this package, such as
  @Min@, @Max@, @<@, @>@, and @>=@.
@@ -5,8 +7,19 @@
 module Data.Type.Natural.Presburger.MinMaxSolver (plugin) where
 
 import Control.Monad (mzero)
-import GHC.TypeLits.Presburger.Compat (lookupModule)
+import GHC.TypeLits.Presburger.Compat
 import GHC.TypeLits.Presburger.Types
+
+#if MIN_VERSION_ghc(9,0,0)
+import GHC.Plugins
+  ( Plugin,
+    fsLit,
+    mkModuleName,
+    mkTcOcc,
+    splitTyConApp_maybe,
+  )
+import GHC.Tc.Plugin
+#else
 import GhcPlugins
   ( Plugin,
     fsLit,
@@ -15,6 +28,7 @@
     splitTyConApp_maybe,
   )
 import TcPluginM
+#endif
 
 plugin :: Plugin
 plugin =
diff --git a/tests/Data/Type/Natural/Presburger/Cases.hs b/tests/Data/Type/Natural/Presburger/Cases.hs
--- a/tests/Data/Type/Natural/Presburger/Cases.hs
+++ b/tests/Data/Type/Natural/Presburger/Cases.hs
@@ -24,4 +24,4 @@
 maxComm _ _ = Refl
 
 falsity :: n <= m => p n -> q m -> Min n m :~: m
-falsity = Refl
+falsity _ _  = Refl
diff --git a/type-natural.cabal b/type-natural.cabal
--- a/type-natural.cabal
+++ b/type-natural.cabal
@@ -1,6 +1,6 @@
 cabal-version: >=1.10
 name:          type-natural
-version:       1.0.0.0
+version:       1.1.0.0
 license:       BSD3
 license-file:  LICENSE
 copyright:     (C) Hiromi ISHII 2013-2014
@@ -55,7 +55,7 @@
         template-haskell >=2.8,
         constraints >=0.3,
         ghc-typelits-natnormalise >=0.4,
-        ghc-typelits-presburger >=0.5,
+        ghc-typelits-presburger >=0.5.1,
         ghc-typelits-knownnat -any,
         integer-logarithms -any
 
@@ -88,7 +88,6 @@
         tasty-hunit -any,
         tasty-discover -any,
         template-haskell -any,
-        tasty-expected-failure -any,
         base -any,
         type-natural -any,
         equational-reasoning -any