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.34.4.
+-- This file has been generated from package.yaml by hpack version 0.35.0.
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: 086ee70967f896732e0ffccb7b264fa3ec9795f18714c281193aeb7259f86cb5
+-- hash: e0545f55ff7ac60cb7924fcbf3f6a5af8bec6777c00c2f3893027c2a7eb54690
 
 name:           singletons-presburger
-version:        0.6.1.0
+version:        0.7.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.
@@ -25,7 +25,7 @@
 license:        BSD3
 license-file:   LICENSE
 tested-with:
-    GHC==8.6.5 GHC==8.8.4 GHC==8.10.7 GHC==9.0.1 GHC==9.2.1
+    GHC==8.6.5 GHC==8.8.4 GHC==8.10.7 GHC==9.0.2 GHC==9.2.4 GHC==9.4.3
 build-type:     Simple
 
 source-repository head
@@ -47,9 +47,11 @@
   ghc-options: -Wall -Wno-dodgy-imports
   build-depends:
       base >=4.7 && <5
+    , ghc
     , ghc-typelits-presburger >=0.4
     , mtl
     , reflection
+  default-language: Haskell2010
   if impl(ghc >= 9)
     cpp-options: -DSINGLETONS_BASE
     build-depends:
@@ -58,7 +60,6 @@
   else
     build-depends:
         singletons
-  default-language: Haskell2010
 
 executable simple-arith
   main-is: simple-arith.hs
@@ -71,6 +72,7 @@
       base
     , equational-reasoning
     , singletons-presburger
+  default-language: Haskell2010
   if impl(ghc >= 9)
     cpp-options: -DSINGLETONS_BASE
     build-depends:
@@ -89,4 +91,3 @@
         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
@@ -133,11 +133,11 @@
 getCaseNameForSingletonBinOp con = do
   let vars = [typeNatKind, LitTy (NumTyLit 0), LitTy (NumTyLit 0)]
   tcPluginTrace "matching... for " (ppr con)
-  Just (appTy0, [n, b, bdy, r]) <- fmap (splitTyConApp . snd) <$> matchFam con vars
+  Just (appTy0, [n, b, bdy, r]) <- fmap splitTyConApp <$> matchFam' con vars
   let (appTy, args) = splitTyConApp bdy
-  Just innermost <- fmap snd <$> matchFam appTy args
-  Just (_, dat) <- matchFam appTy0 [n, b, innermost, r]
-  Just dat' <- fmap snd <$> uncurry matchFam (splitTyConApp dat)
+  Just innermost <- matchFam' appTy args
+  Just dat <- matchFam' appTy0 [n, b, innermost, r]
+  Just dat' <- uncurry matchFam' (splitTyConApp dat)
   let Just (con', _) = splitTyConApp_maybe dat'
   return con'
 
@@ -145,11 +145,11 @@
 getCaseNameForSingletonBinRel con = do
   let vars = [typeNatKind, LitTy (NumTyLit 0), LitTy (NumTyLit 0)]
   tcPluginTrace "matching... for " (ppr con)
-  Just (appTy0, [n, b, bdy, r]) <- fmap (splitTyConApp . snd) <$> matchFam con vars
+  Just (appTy0, [n, b, bdy, r]) <- fmap splitTyConApp <$> matchFam' con vars
   let (appTy, args) = splitTyConApp bdy
-  Just innermost <- fmap snd <$> matchFam appTy args
-  Just (_, dat) <- matchFam appTy0 [n, b, innermost, r]
-  Just dat' <- fmap snd <$> uncurry matchFam (splitTyConApp dat)
+  Just innermost <- matchFam' appTy args
+  Just dat <- matchFam' appTy0 [n, b, innermost, r]
+  Just dat' <- uncurry matchFam' (splitTyConApp dat)
   tcPluginTrace "matched. (orig, inner) = " (ppr (con, fst $ splitTyConApp dat'))
   return $ fst $ splitTyConApp dat'