diff --git a/patches/sbv-10.1.patch b/patches/sbv-10.1.patch
index bdacf417ce38f4a943abc095f40c4589277c0b9b..ad1a929e13ea9f789302cdad5a91b8431bc621a9 100644
--- a/patches/sbv-10.1.patch
+++ b/patches/sbv-10.1.patch
@@ -252,6 +252,24 @@ index 416f8e2..c4b719b 100644
  
  module Documentation.SBV.Examples.Existentials.Diophantine where
  
+diff --git a/Documentation/SBV/Examples/Misc/FirstOrderLogic.hs b/Documentation/SBV/Examples/Misc/FirstOrderLogic.hs
+index 29576d4..7bc4e97 100644
+--- a/Documentation/SBV/Examples/Misc/FirstOrderLogic.hs
++++ b/Documentation/SBV/Examples/Misc/FirstOrderLogic.hs
+@@ -17,6 +17,13 @@
+ {-# LANGUAGE StandaloneDeriving  #-}
+ {-# LANGUAGE TemplateHaskell     #-}
+ {-# LANGUAGE TypeApplications    #-}
++{-# LANGUAGE CPP #-}
++
++-- Type applications in patterns require the TypeAbstractions
++-- extension starting in GHC 9.8.
++#if __GLASGOW_HASKELL__ >= 907
++{-# LANGUAGE TypeAbstractions #-}
++#endif
+ 
+ {-# OPTIONS_GHC -Wall -Werror #-}
+ 
 diff --git a/Documentation/SBV/Examples/Puzzles/Coins.hs b/Documentation/SBV/Examples/Puzzles/Coins.hs
 index 1c1eaee..594d1ab 100644
 --- a/Documentation/SBV/Examples/Puzzles/Coins.hs
diff --git a/patches/singletons-3.0.2.patch b/patches/singletons-3.0.2.patch
index 8abaf8023e17b69ff928ef1c3fc2856147cea19f..3a1f892b9fbf6d55637edf6ed8b8eb2d81de4aef 100644
--- a/patches/singletons-3.0.2.patch
+++ b/patches/singletons-3.0.2.patch
@@ -1,8 +1,24 @@
 diff --git a/src/Data/Singletons.hs b/src/Data/Singletons.hs
-index 67e0a63..6154010 100644
+index 67e0a63..b95bfe5 100644
 --- a/src/Data/Singletons.hs
 +++ b/src/Data/Singletons.hs
-@@ -149,7 +149,11 @@ type SameKind (a :: k) (b :: k) = (() :: Constraint)
+@@ -27,6 +27,15 @@
+ {-# LANGUAGE StandaloneKindSignatures #-}
+ #endif
+ 
++-- Invisible type binders in type declarations, such as
++--
++--   type family Sing @k
++--
++-- require the TypeAbstractions extension.
++#if GLASGOW_HASKELL >= 909
++{-# LANGUAGE TypeAbstractions #-}
++#endif
++
+ -----------------------------------------------------------------------------
+ -- |
+ -- Module      :  Data.Singletons
+@@ -149,7 +158,11 @@ type SameKind (a :: k) (b :: k) = (() :: Constraint)
  #if __GLASGOW_HASKELL__ >= 810
  type Sing :: k -> Type
  #endif
@@ -14,7 +30,7 @@ index 67e0a63..6154010 100644
  
  {-
  Note [The kind of Sing]
-@@ -512,7 +516,11 @@ data family TyCon :: (k1 -> k2) -> unmatchable_fun
+@@ -512,7 +525,11 @@ data family TyCon :: (k1 -> k2) -> unmatchable_fun
  #if __GLASGOW_HASKELL__ >= 810
  type ApplyTyCon :: (k1 -> k2) -> (k1 ~> unmatchable_fun)
  #endif
@@ -26,7 +42,7 @@ index 67e0a63..6154010 100644
  #if __GLASGOW_HASKELL__ >= 808
    ApplyTyCon @k1 @(k2 -> k3) @unmatchable_fun = ApplyTyConAux2
    ApplyTyCon @k1 @k2         @k2              = ApplyTyConAux1
-@@ -589,6 +597,29 @@ type TyCon8          :: (k1 -> k2 -> k3 -> k4 -> k5 -> k6 -> k7 -> k8 -> k9)
+@@ -589,6 +606,29 @@ type TyCon8          :: (k1 -> k2 -> k3 -> k4 -> k5 -> k6 -> k7 -> k8 -> k9)
  -- We can write:
  --
  -- > Map (TyCon1 Succ) [Zero, Succ Zero]
@@ -56,7 +72,7 @@ index 67e0a63..6154010 100644
  type TyCon1 = (TyCon :: (k1 -> k2) -> (k1 ~> k2))
  
  -- | Similar to 'TyCon1', but for two-parameter type constructors.
-@@ -603,6 +634,7 @@ type TyCon7 = (TyCon :: (k1 -> k2 -> k3 -> k4 -> k5 -> k6 -> k7 -> k8)
+@@ -603,6 +643,7 @@ type TyCon7 = (TyCon :: (k1 -> k2 -> k3 -> k4 -> k5 -> k6 -> k7 -> k8)
                       -> (k1 ~> k2 ~> k3 ~> k4 ~> k5 ~> k6 ~> k7 ~> k8))
  type TyCon8 = (TyCon :: (k1 -> k2 -> k3 -> k4 -> k5 -> k6 -> k7 -> k8 -> k9)
                       -> (k1 ~> k2 ~> k3 ~> k4 ~> k5 ~> k6 ~> k7 ~> k8 ~> k9))