diff --git a/examples/simple-arith.hs b/examples/simple-arith.hs
--- a/examples/simple-arith.hs
+++ b/examples/simple-arith.hs
@@ -6,6 +6,9 @@
 #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 806
 {-# LANGUAGE NoStarIsType #-}
 #endif
+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 810
+{-# LANGUAGE StandaloneKindSignatures #-}
+#endif
 
 module Main where
 import Data.Singletons.Decide
diff --git a/singletons-presburger.cabal b/singletons-presburger.cabal
--- a/singletons-presburger.cabal
+++ b/singletons-presburger.cabal
@@ -1,13 +1,13 @@
 cabal-version: 1.12
 
--- This file has been generated from package.yaml by hpack version 0.31.2.
+-- This file has been generated from package.yaml by hpack version 0.33.0.
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: 1398143e2ff5a7650c68eda0c0513d0db5b5ed760488ce49e28425fa4f97830c
+-- hash: b271b824f909f5d2533590977ec2a9e9d107034176402483ca143b699d7d46cd
 
 name:           singletons-presburger
-version:        0.3.0.0
+version:        0.3.0.1
 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.2
+tested-with:    GHC==8.4.3 GHC==8.6.3 GHC==8.8.3 GHC==8.10.1
 build-type:     Simple
 
 source-repository head
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
@@ -9,6 +9,7 @@
 
 import Control.Monad
 import Data.Reflection (Given, give, given)
+import GHC             (mkModule, moduleUnitId)
 import TcPluginM       (lookupOrig, matchFam)
 import Type            (splitTyConApp)
 
@@ -26,6 +27,8 @@
       , singNatMinus       :: TyCon
       , singNatTimes       :: TyCon
       , singNatCompare     :: TyCon
+      , singTrueSym0       :: TyCon
+      , singFalseSym0      :: TyCon
       , caseNameForSingLeq :: TyCon
       , caseNameForSingGeq :: TyCon
       , caseNameForSingLt  :: TyCon
@@ -50,14 +53,17 @@
     , natMinus = [singNatMinus]
     , natTimes = [singNatTimes]
     , parsePred = parseSingPred
+    , trueData = [singTrueSym0]
+    , falseData = [singFalseSym0]
     }
 
 genSingletonCons :: TcPluginM SingletonCons
 genSingletonCons = do
   singletonOrd <- lookupModule (mkModuleName "Data.Singletons.Prelude.Ord") (fsLit "singletons")
   singletonsNum <- lookupModule (mkModuleName "Data.Singletons.Prelude.Num") (fsLit "singletons")
-  -- prel <- lookupModule (mkModuleName "Data.Singletons.Prelude") (fsLit "singletons")
-  -- singTrueSym0 <- tcLookupTyCon =<< lookupOrig prel (mkTcOcc "TrueSym0")
+  let prel = mkModule (moduleUnitId singletonsNum) (mkModuleName "Data.Singletons.Prelude.Instances")
+  singTrueSym0 <- tcLookupTyCon =<< lookupOrig prel (mkTcOcc "TrueSym0")
+  singFalseSym0 <- tcLookupTyCon =<< lookupOrig prel (mkTcOcc "FalseSym0")
 #if MIN_VERSION_singletons(2,4,1)
   singNatLeq <- tcLookupTyCon =<< lookupOrig singletonOrd (mkTcOcc "<=")
   singNatLt <- tcLookupTyCon =<< lookupOrig singletonOrd (mkTcOcc "<")