diff --git a/examples/simple-arith.hs b/examples/simple-arith.hs
--- a/examples/simple-arith.hs
+++ b/examples/simple-arith.hs
@@ -68,7 +68,7 @@
 leqSucc :: proxy n -> proxy m -> IsTrue ((n + 1) <= m) -> CmpNat n m :~: 'LT
 leqSucc _ _ Witness = Refl
 
-leqEquiv :: (n <= m) ~ 'True => Sing n -> Sing m -> IsTrue (n <=? m)
+leqEquiv :: (n <= m) ~ 'True => Sing (n :: Nat) -> Sing m -> IsTrue (n <=? m)
 leqEquiv _ _ = Witness
 
 data NatView (n :: Nat) where
@@ -87,7 +87,7 @@
 minusLeq :: (n <= m) ~ 'True => proxy (n :: Nat) -> proxy m -> IsTrue ((m - n) + n <= m)
 minusLeq _ _ = Witness
 
-(%:<=?) :: Sing n -> Sing m -> Sing (n <=? m)
+(%:<=?) :: Sing (n :: Nat) -> Sing m -> Sing (n <=? m)
 n %:<=? m = case sCompare n m of
   SLT -> STrue
   SEQ -> STrue
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.33.0.
+-- This file has been generated from package.yaml by hpack version 0.34.4.
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: 067f024523630b434307a5ddecb854a92115694a3e9c16f2391e96bf77395e8a
+-- hash: 086ee70967f896732e0ffccb7b264fa3ec9795f18714c281193aeb7259f86cb5
 
 name:           singletons-presburger
-version:        0.6.0.0
+version:        0.6.1.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,8 @@
 copyright:      2015 (c) Hiromi ISHII
 license:        BSD3
 license-file:   LICENSE
-tested-with:    GHC==8.6.5 GHC==8.8.4 GHC==8.10.4 GHC==9.0.1
+tested-with:
+    GHC==8.6.5 GHC==8.8.4 GHC==8.10.7 GHC==9.0.1 GHC==9.2.1
 build-type:     Simple
 
 source-repository head