diff --git a/CHANGES.md b/CHANGES.md
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,6 +1,10 @@
 * Hackage: <http://hackage.haskell.org/package/sbv>
 * GitHub:  <http://github.com/LeventErkok/sbv>
 
+### Version 13.1, 2025-10-31
+
+  * Tweaks to make sure SBV compiles with GHC 9.8.4. No other changes on top of 13.0 below.
+
 ### Version 13.0, 2025-10-31
 
   * SBV now supports algebraic data-types. A new function 'mkSymbolic' is introduced, which take a list of types
diff --git a/Data/SBV/TP/List.hs b/Data/SBV/TP/List.hs
--- a/Data/SBV/TP/List.hs
+++ b/Data/SBV/TP/List.hs
@@ -16,6 +16,7 @@
 {-# LANGUAGE OverloadedLists     #-}
 {-# LANGUAGE QuasiQuotes         #-}
 {-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeAbstractions    #-}
 {-# LANGUAGE TypeApplications    #-}
 
 {-# OPTIONS_GHC -Wall -Werror #-}
diff --git a/Data/SBV/TP/Utils.hs b/Data/SBV/TP/Utils.hs
--- a/Data/SBV/TP/Utils.hs
+++ b/Data/SBV/TP/Utils.hs
@@ -17,6 +17,7 @@
 {-# LANGUAGE NamedFieldPuns             #-}
 {-# LANGUAGE ScopedTypeVariables        #-}
 {-# LANGUAGE TupleSections              #-}
+{-# LANGUAGE TypeAbstractions           #-}
 {-# LANGUAGE TypeApplications           #-}
 
 {-# OPTIONS_GHC -Wall -Werror #-}
diff --git a/Documentation/SBV/Examples/TP/Basics.hs b/Documentation/SBV/Examples/TP/Basics.hs
--- a/Documentation/SBV/Examples/TP/Basics.hs
+++ b/Documentation/SBV/Examples/TP/Basics.hs
@@ -11,8 +11,9 @@
 
 {-# LANGUAGE CPP                 #-}
 {-# LANGUAGE DataKinds           #-}
-{-# LANGUAGE TypeApplications    #-}
 {-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeAbstractions    #-}
+{-# LANGUAGE TypeApplications    #-}
 
 {-# OPTIONS_GHC -Wall -Werror #-}
 
diff --git a/Documentation/SBV/Examples/TP/InsertionSort.hs b/Documentation/SBV/Examples/TP/InsertionSort.hs
--- a/Documentation/SBV/Examples/TP/InsertionSort.hs
+++ b/Documentation/SBV/Examples/TP/InsertionSort.hs
@@ -14,6 +14,7 @@
 {-# LANGUAGE FlexibleContexts    #-}
 {-# LANGUAGE OverloadedLists     #-}
 {-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeAbstractions    #-}
 {-# LANGUAGE TypeApplications    #-}
 
 {-# OPTIONS_GHC -Wall -Werror #-}
diff --git a/Documentation/SBV/Examples/TP/QuickSort.hs b/Documentation/SBV/Examples/TP/QuickSort.hs
--- a/Documentation/SBV/Examples/TP/QuickSort.hs
+++ b/Documentation/SBV/Examples/TP/QuickSort.hs
@@ -17,6 +17,7 @@
 {-# LANGUAGE FlexibleContexts    #-}
 {-# LANGUAGE OverloadedLists     #-}
 {-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeAbstractions    #-}
 {-# LANGUAGE TypeApplications    #-}
 
 {-# OPTIONS_GHC -Wall -Werror #-}
diff --git a/Documentation/SBV/Examples/TP/VM.hs b/Documentation/SBV/Examples/TP/VM.hs
--- a/Documentation/SBV/Examples/TP/VM.hs
+++ b/Documentation/SBV/Examples/TP/VM.hs
@@ -17,6 +17,7 @@
 {-# LANGUAGE QuasiQuotes         #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TemplateHaskell     #-}
+{-# LANGUAGE TypeAbstractions    #-}
 {-# LANGUAGE TypeApplications    #-}
 
 {-# OPTIONS_GHC -Wall -Werror #-}
diff --git a/sbv.cabal b/sbv.cabal
--- a/sbv.cabal
+++ b/sbv.cabal
@@ -1,7 +1,7 @@
 Cabal-Version: 2.2
 
 Name        : sbv
-Version     : 13.0
+Version     : 13.1
 Category    : Formal Methods, Theorem Provers, Bit vectors, Symbolic Computation, Math, SMT
 Synopsis    : SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.
 Description : Express properties about Haskell programs and automatically prove them using SMT