diff --git a/ghc-typelits-presburger.cabal b/ghc-typelits-presburger.cabal
--- a/ghc-typelits-presburger.cabal
+++ b/ghc-typelits-presburger.cabal
@@ -4,10 +4,10 @@
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: f4ea69ea55a2f6e349e91e0e359ba111afa36236c8c094e799d1e95ac82ce411
+-- hash: f5d043e0588502295fbbf222a24c404b5415e14c21786d9e5e7bacc06e2088af
 
 name:           ghc-typelits-presburger
-version:        0.5.2.0
+version:        0.6.0.0
 synopsis:       Presburger Arithmetic Solver for GHC Type-level natural numbers.
 description:    @ghc-typelits-presburger@ augments GHC type-system with Presburger
                 Arithmetic Solver for Type-level natural numbers.
@@ -29,7 +29,7 @@
 copyright:      2015 (c) Hiromi ISHII
 license:        BSD3
 license-file:   LICENSE
-tested-with:    GHC==8.4.3 GHC==8.6.3 GHC==8.8.3 GHC==8.10.3 GHC==9.0.1
+tested-with:    GHC==8.6.5 GHC==8.8.4 GHC==8.10.4 GHC==9.0.1
 build-type:     Simple
 
 source-repository head
diff --git a/src/GHC/TypeLits/Presburger/Compat.hs b/src/GHC/TypeLits/Presburger/Compat.hs
--- a/src/GHC/TypeLits/Presburger/Compat.hs
+++ b/src/GHC/TypeLits/Presburger/Compat.hs
@@ -1,5 +1,6 @@
 {-# LANGUAGE CPP, FlexibleInstances, PatternGuards, PatternSynonyms #-}
 {-# LANGUAGE TypeSynonymInstances, ViewPatterns                     #-}
+{-# LANGUAGE PatternSynonyms #-}
 {-# OPTIONS_GHC -Wno-orphans #-}
 module GHC.TypeLits.Presburger.Compat (module GHC.TypeLits.Presburger.Compat) where
 import Data.Function       (on)
@@ -10,6 +11,9 @@
 #if MIN_VERSION_ghc(9,0,0)
 import GHC.Builtin.Names as GHC.TypeLits.Presburger.Compat (gHC_TYPENATS, dATA_TYPE_EQUALITY)
 import qualified GHC.Builtin.Names as Old
+import GHC.Hs as GHC.TypeLits.Presburger.Compat (HsModule(..), NoExtField(..))
+import GHC.Hs.ImpExp as GHC.TypeLits.Presburger.Compat (ImportDecl(..), ImportDeclQualifiedStyle(..))
+import GHC.Hs.Extension as GHC.TypeLits.Presburger.Compat (GhcPs)
 import GHC.Builtin.Types as GHC.TypeLits.Presburger.Compat
   ( boolTyCon,
     eqTyConName,
@@ -34,7 +38,9 @@
 import GHC.Driver.Session (unitState)
 import GHC.Plugins (InScopeSet, Outputable, emptyUFM, moduleUnit, Unit)
 import GHC.Plugins as GHC.TypeLits.Presburger.Compat
-  ( PackageName (..),
+  ( PackageName (..),isStrLitTy, isNumLitTy,
+    nilDataCon, consDataCon,
+    Hsc, HsParsedModule(..),
     Plugin (..),
     TCvSubst (..),
     TvSubstEnv,
@@ -59,8 +65,12 @@
     unionTCvSubst,
   )
 import GHC.Tc.Plugin (lookupOrig)
+import GHC.Core.InstEnv as GHC.TypeLits.Presburger.Compat (classInstances)
+import GHC.Driver.Types as GHC.TypeLits.Presburger.Compat (IsBootInterface(..))
 import GHC.Tc.Plugin as GHC.TypeLits.Presburger.Compat
   ( TcPluginM,
+    getInstEnvs,
+    newFlexiTyVar,
     getTopEnv,
     lookupOrig,
     newFlexiTyVar,
@@ -159,12 +169,13 @@
 #if MIN_VERSION_ghc(8,10,1)
 import Predicate as GHC.TypeLits.Presburger.Compat (EqRel (..), Pred(..))
 import Predicate as GHC.TypeLits.Presburger.Compat (isEqPred)
-
+import GHC (NoExtField(..))
 import qualified Predicate as Old (classifyPredType)
 import Predicate as GHC.TypeLits.Presburger.Compat  (mkPrimEqPredRole)
 import Constraint as GHC.TypeLits.Presburger.Compat 
     (Ct, ctEvidence, ctEvPred, isWanted)
 #else
+import GHC (NoExt(..))
 import GhcPlugins as GHC.TypeLits.Presburger.Compat (EqRel (..), PredTree (..))
 import GhcPlugins as GHC.TypeLits.Presburger.Compat (isEqPred)
 import qualified GhcPlugins as Old (classifyPredType)
@@ -359,3 +370,32 @@
 moduleUnit' :: Module -> ModuleUnit
 moduleUnit' = GHC.moduleUnitId
 #endif
+
+#if !MIN_VERSION_ghc(8,10,1)
+type NoExtField = NoExt
+#endif
+
+noExtField :: NoExtField
+#if MIN_VERSION_ghc(8,10,1)
+noExtField = NoExtField
+#else
+noExtField = NoExt
+#endif
+
+#if MIN_VERSION_ghc(9,0,1)
+type HsModule' = HsModule
+#else
+type HsModule' = GHC.HsModule GHC.GhcPs
+#endif
+
+#if !MIN_VERSION_ghc(9,0,1)
+type IsBootInterface = Bool
+pattern NotBoot :: IsBootInterface
+pattern NotBoot = False
+
+pattern IsBoot :: IsBootInterface
+pattern IsBoot = True
+
+{-# COMPLETE NotBoot, IsBoot #-}
+#endif
+
diff --git a/src/GHC/TypeLits/Presburger/Types.hs b/src/GHC/TypeLits/Presburger/Types.hs
--- a/src/GHC/TypeLits/Presburger/Types.hs
+++ b/src/GHC/TypeLits/Presburger/Types.hs
@@ -267,16 +267,9 @@
     let givens = catMaybes ngs
         prems0 = map snd givens
         prems = foldr assert' noProps prems0
-        (solved, _) = foldr go ([], noProps) givens
     if isNothing (checkSat prems)
       then return $ TcPluginContradiction gs
-      else do
-        tcPluginTrace "Redundant solveds" $ ppr solved
-        return $ TcPluginOk (map withEv solved) []
-  where
-    go (ct, p) (ss, prem)
-      | Proved <- testIf prem p = (ct : ss, prem)
-      | otherwise = (ss, assert' p prem)
+      else return $ TcPluginOk [] []
 decidePresburger mode genTrans _ gs _ds ws = do
   trans <- genTrans
   give trans $ do