diff --git a/examples/simple-arith.hs b/examples/simple-arith.hs
--- a/examples/simple-arith.hs
+++ b/examples/simple-arith.hs
@@ -9,6 +9,7 @@
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeInType #-}
 {-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
 #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 806
 {-# LANGUAGE NoStarIsType #-}
 #endif
@@ -20,12 +21,20 @@
 
 module Main where
 
+#if defined(SINGLETONS_BASE)
+import Prelude.Singletons
+import Data.Singletons.Base.Enum
+import Data.Singletons.TH
+import GHC.TypeLits.Singletons
+#else
 import Data.Singletons.Decide
 import Data.Singletons.Prelude
 import Data.Singletons.Prelude.Enum
 import Data.Singletons.Prelude.List
 import Data.Singletons.TH
 import Data.Singletons.TypeLits
+#endif
+
 import Data.Type.Equality
 import GHC.TypeLits (CmpNat, Nat, type (<=?))
 import Proof.Propositional (Empty (..), IsTrue (Witness), withEmpty)
diff --git a/singletons-presburger.cabal b/singletons-presburger.cabal
--- a/singletons-presburger.cabal
+++ b/singletons-presburger.cabal
@@ -4,10 +4,10 @@
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: 70dbe672ac6a08a171c823e902bc91918e2e99e85f85577e9d450133c8d5f202
+-- hash: 067f024523630b434307a5ddecb854a92115694a3e9c16f2391e96bf77395e8a
 
 name:           singletons-presburger
-version:        0.5.0.0
+version:        0.6.0.0
 synopsis:       Presburger Arithmetic Solver for GHC Type-level natural numbers with Singletons package.
 description:    The @singletons-presburger@ plugin augments GHC type-system with Presburger
                 Arithmetic Solver for Type-level natural numbers, with integration with <https://hackage.haskell.org/package/singletons singletons> package.
@@ -24,7 +24,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.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
@@ -46,11 +46,17 @@
   ghc-options: -Wall -Wno-dodgy-imports
   build-depends:
       base >=4.7 && <5
-    , ghc >=7.10 && <8.11
     , ghc-typelits-presburger >=0.4
     , mtl
     , reflection
-    , singletons
+  if impl(ghc >= 9)
+    cpp-options: -DSINGLETONS_BASE
+    build-depends:
+        singletons
+      , singletons-base >=3.0
+  else
+    build-depends:
+        singletons
   default-language: Haskell2010
 
 executable simple-arith
@@ -63,8 +69,23 @@
   build-depends:
       base
     , equational-reasoning
-    , singletons
     , singletons-presburger
+  if impl(ghc >= 9)
+    cpp-options: -DSINGLETONS_BASE
+    build-depends:
+        singletons
+      , singletons-base >=3.0
+  else
+    build-depends:
+        singletons
+  if impl(ghc >= 9)
+    cpp-options: -DSINGLETONS_BASE
+    build-depends:
+        singletons-base >=3.0
+      , singletons-th
+  else
+    build-depends:
+        singletons
   if !(flag(examples))
     buildable: False
   default-language: Haskell2010
diff --git a/src/Data/Singletons/TypeNats/Presburger.hs b/src/Data/Singletons/TypeNats/Presburger.hs
--- a/src/Data/Singletons/TypeNats/Presburger.hs
+++ b/src/Data/Singletons/TypeNats/Presburger.hs
@@ -19,11 +19,8 @@
 import Control.Monad
 import Control.Monad.Trans (MonadTrans (lift))
 import Data.Reflection (Given, give, given)
-import GHC (mkModule, moduleUnitId)
 import GHC.TypeLits.Presburger.Compat
 import GHC.TypeLits.Presburger.Types
-import TcPluginM (lookupOrig, matchFam)
-import Type (splitTyConApp)
 
 plugin :: Plugin
 plugin =
@@ -76,11 +73,30 @@
       , falseData = [singFalseSym0]
       }
 
+singPackage :: FastString
+#if defined(MIN_VERISION_singletons_base)
+singPackage = "singletons-base"
+#else
+singPackage = "singletons"
+#endif
+
+ordModName, numModName, prelInstName :: ModuleName
+#if defined(SINGLETONS_BASE)
+ordModName = mkModuleName "Data.Ord.Singletons"
+numModName = mkModuleName "GHC.Num.Singletons"
+prelInstName = mkModuleName "Data.Singletons.Base.Instances"
+#else
+ordModName = mkModuleName "Data.Singletons.Prelude.Ord"
+numModName = mkModuleName "Data.Singletons.Prelude.Num"
+prelInstName = mkModuleName "Data.Singletons.Prelude.Instances"
+#endif
+
 genSingletonCons :: TcPluginM SingletonCons
 genSingletonCons = do
-  singletonOrd <- lookupModule (mkModuleName "Data.Singletons.Prelude.Ord") (fsLit "singletons")
-  singletonsNum <- lookupModule (mkModuleName "Data.Singletons.Prelude.Num") (fsLit "singletons")
-  let prel = mkModule (moduleUnitId singletonsNum) (mkModuleName "Data.Singletons.Prelude.Instances")
+  singletonOrd <- lookupModule ordModName singPackage
+  let singUnit = moduleUnit' singletonOrd
+      prel = mkModule singUnit prelInstName
+      singletonsNum = mkModule singUnit numModName
   singTrueSym0 <- tcLookupTyCon =<< lookupOrig prel (mkTcOcc "TrueSym0")
   singFalseSym0 <- tcLookupTyCon =<< lookupOrig prel (mkTcOcc "FalseSym0")
 #if MIN_VERSION_singletons(2,4,1)