diff --git a/liquid-base.cabal b/liquid-base.cabal
--- a/liquid-base.cabal
+++ b/liquid-base.cabal
@@ -1,8 +1,8 @@
 cabal-version:      1.24
 name:               liquid-base
-version:            4.14.1.0
-synopsis:           Drop-in base replacement for LiquidHaskell
-description:        Drop-in base replacement for LiquidHaskell.
+version:            4.14.3.0
+synopsis:           Drop-in base replacement for LH
+description:        Superseded by liquidhaskell >= 9.2
 license:            BSD3
 license-file:       LICENSE
 copyright:          2010-19 Ranjit Jhala & Niki Vazou & Eric L. Seidel, University of California, San Diego.
@@ -23,7 +23,7 @@
                     src/Control/*.spec
 
 custom-setup
-  setup-depends: Cabal, base, liquidhaskell
+  setup-depends: Cabal<4, base<5, liquidhaskell
 
 library
   exposed-modules:  Control.Applicative
@@ -244,9 +244,11 @@
                     Liquid.Prelude.Totality
 
   hs-source-dirs:     src
-  build-depends:      base                 == 4.14.1.0
+  build-depends:      base                 == 4.14.3.0
                     , liquid-ghc-prim
-                    , liquidhaskell        >= 0.8.10.1
+                    , liquidhaskell        >= 0.8.10.7.1 && < 0.9
+  if impl(ghc < 9)
+    build-depends:    integer-gmp < 1.0.4.0
   default-language:   Haskell2010
   default-extensions: PackageImports
                       NoImplicitPrelude
diff --git a/src/Control/Exception.spec b/src/Control/Exception.spec
--- a/src/Control/Exception.spec
+++ b/src/Control/Exception.spec
@@ -1,5 +1,5 @@
 module spec Control.Exception where
 
-// Useless as compiled into GHC primitive, which is ignored
+//  Useless as compiled into GHC primitive, which is ignored
 assume assert :: {v:Bool | v } -> a -> a
 
diff --git a/src/Data/Bits.hs b/src/Data/Bits.hs
--- a/src/Data/Bits.hs
+++ b/src/Data/Bits.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE Trustworthy #-}
 module Data.Bits ( module Exports ) where
 
 import "base" Data.Bits as Exports
diff --git a/src/Data/Bits.spec b/src/Data/Bits.spec
--- a/src/Data/Bits.spec
+++ b/src/Data/Bits.spec
@@ -1,6 +1,6 @@
 module spec Data.Bits where
 
-// TODO: cannot use this because `Bits` is not a `Num`
-// Data.Bits.shiftR :: (Data.Bits.Bits a) => x:a -> d:Nat 
-//                  -> {v:a | ((d=1) => (x <= 2*v + 1 && 2*v <= x)) }
+//  TODO: cannot use this because `Bits` is not a `Num`
+//  Data.Bits.shiftR :: (Data.Bits.Bits a) => x:a -> d:Nat 
+//                   -> {v:a | ((d=1) => (x <= 2*v + 1 && 2*v <= x)) }
 
diff --git a/src/Data/Foldable.spec b/src/Data/Foldable.spec
--- a/src/Data/Foldable.spec
+++ b/src/Data/Foldable.spec
@@ -3,3 +3,4 @@
 import GHC.Base
 
 length :: Data.Foldable.Foldable f => forall a. xs:f a -> {v:Nat | v = len xs}
+null   :: Data.Foldable.Foldable f => v:(f a) -> {b:Bool | (b <=> len v = 0) && (not b <=> len v > 0)}
diff --git a/src/Data/Int.spec b/src/Data/Int.spec
--- a/src/Data/Int.spec
+++ b/src/Data/Int.spec
@@ -5,4 +5,4 @@
 embed Data.Int.Int32 as int
 embed Data.Int.Int64 as int
 
-// type Nat64 = {v:Data.Int.Int64 | v >= 0}
+//  type Nat64 = {v:Data.Int.Int64 | v >= 0}
diff --git a/src/Data/Maybe.spec b/src/Data/Maybe.spec
new file mode 100644
--- /dev/null
+++ b/src/Data/Maybe.spec
@@ -0,0 +1,7 @@
+module spec Data.Maybe where
+
+maybe :: v:b -> (a -> b) -> u:(Maybe a) -> {w:b | not (isJust u) => w == v}
+isJust :: v:(Maybe a) -> {b:Bool | b == isJust v}
+isNothing :: v:(Maybe a) -> {b:Bool | not (isJust v) == b}
+fromJust :: {v:(Maybe a) | isJust v} -> a
+fromMaybe :: v:a -> u:(Maybe a) -> {x:a | not (isJust u) => x == v}
diff --git a/src/Data/Typeable.hs b/src/Data/Typeable.hs
--- a/src/Data/Typeable.hs
+++ b/src/Data/Typeable.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE Trustworthy #-}
 module Data.Typeable (module Exports) where
 
 import "base" Data.Typeable as Exports
diff --git a/src/Data/Word.hs b/src/Data/Word.hs
--- a/src/Data/Word.hs
+++ b/src/Data/Word.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE Trustworthy #-}
 module Data.Word ( module Exports) where
 
 import "base" Data.Word as Exports
diff --git a/src/Foreign/C/String.spec b/src/Foreign/C/String.spec
--- a/src/Foreign/C/String.spec
+++ b/src/Foreign/C/String.spec
@@ -5,8 +5,8 @@
 type CStringLen    = ((GHC.Ptr.Ptr Foreign.C.Types.CChar), Nat)<{\p v -> (v <= (plen p))}>
 type CStringLenN N = ((GHC.Ptr.Ptr Foreign.C.Types.CChar), {v:Nat | v = N})<{\p v -> (v <= (plen p))}>
 
-//measure cStringLen :: Foreign.C.String.CStringLen -> GHC.Types.Int
+// measure cStringLen :: Foreign.C.String.CStringLen -> GHC.Types.Int
 measure cStringLen :: ((GHC.Ptr.Ptr Foreign.C.Types.CChar), GHC.Types.Int) -> GHC.Types.Int
 
-//measure cStringLen :: ((GHC.Ptr.Ptr Foreign.C.Types.CChar), GHC.Types.Int) -> GHC.Types.Int 
-//cStringLen (c, n) = n
+// measure cStringLen :: ((GHC.Ptr.Ptr Foreign.C.Types.CChar), GHC.Types.Int) -> GHC.Types.Int 
+// cStringLen (c, n) = n
diff --git a/src/Foreign/ForeignPtr.spec b/src/Foreign/ForeignPtr.spec
--- a/src/Foreign/ForeignPtr.spec
+++ b/src/Foreign/ForeignPtr.spec
@@ -12,5 +12,5 @@
 Foreign.ForeignPtr.newForeignPtr ::  _ -> p:(PtrV a) -> (GHC.Types.IO (ForeignPtrN a (plen p)))
 
 
-// this uses `sizeOf (undefined :: a)`, so the ForeignPtr does not necessarily have length `n`
-// Foreign.ForeignPtr.Imp.mallocForeignPtrArray :: (Foreign.Storable.Storable a) => n:Nat -> IO (ForeignPtrN a n)
+//  this uses `sizeOf (undefined :: a)`, so the ForeignPtr does not necessarily have length `n`
+//  Foreign.ForeignPtr.Imp.mallocForeignPtrArray :: (Foreign.Storable.Storable a) => n:Nat -> IO (ForeignPtrN a n)
diff --git a/src/GHC/IO/Handle.hs b/src/GHC/IO/Handle.hs
--- a/src/GHC/IO/Handle.hs
+++ b/src/GHC/IO/Handle.hs
@@ -1,4 +1,5 @@
 module GHC.IO.Handle ( module Exports ) where
 
 import GHC.Types
+import GHC.Integer
 import "base" GHC.IO.Handle as Exports
diff --git a/src/GHC/IO/Handle.spec b/src/GHC/IO/Handle.spec
--- a/src/GHC/IO/Handle.spec
+++ b/src/GHC/IO/Handle.spec
@@ -7,4 +7,4 @@
                    -> (GHC.Types.IO {v:Nat | v <= n})
 
 hFileSize :: GHC.IO.Handle.Handle
-          -> (GHC.Types.IO {v:GHC.Integer.Type.Integer | v >= 0})
+          -> (GHC.Types.IO {v:Integer | v >= 0})
diff --git a/src/GHC/List.spec b/src/GHC/List.spec
--- a/src/GHC/List.spec
+++ b/src/GHC/List.spec
@@ -46,7 +46,7 @@
 
 reverse      :: xs:[a] -> {v: [a] | len(v) = len(xs)}
 
-// Copy-pasted from len.hquals
+//  Copy-pasted from len.hquals
 qualif LenSum(v:[a], xs:[b], ys:[c]): len([v]) = (len([xs]) + len([ys]))
 qualif LenSum(v:[a], xs:[b], ys:[c]): len([v]) = (len([xs]) - len([ys]))
 
diff --git a/src/GHC/Num.spec b/src/GHC/Num.spec
--- a/src/GHC/Num.spec
+++ b/src/GHC/Num.spec
@@ -1,8 +1,9 @@
 module spec GHC.Num where
 
-embed GHC.Integer.Type.Integer as int 
+embed GHC.Integer.Type.Integer as int
+embed GHC.Num.Integer as int
 
-GHC.Num.fromInteger :: (GHC.Num.Num a) => x:GHC.Integer.Type.Integer -> {v:a | v = x }
+GHC.Num.fromInteger :: (GHC.Num.Num a) => x:Integer -> {v:a | v = x }
 
 GHC.Num.negate :: (GHC.Num.Num a)
                => x:a
diff --git a/src/GHC/Real.hs b/src/GHC/Real.hs
--- a/src/GHC/Real.hs
+++ b/src/GHC/Real.hs
@@ -3,5 +3,4 @@
 import GHC.Types
 import GHC.Num
 import "base" GHC.Enum
-
 import "base" GHC.Real as Exports
diff --git a/src/GHC/Real.spec b/src/GHC/Real.spec
--- a/src/GHC/Real.spec
+++ b/src/GHC/Real.spec
@@ -33,7 +33,7 @@
                                                          ((x >= 0 && y >= 1) => v <= x) }
                                                 , {v:a | v = x mod y && ((0 <= x && 0 < y) => (0 <= v && v < y))}
                                                 )
-  GHC.Real.toInteger :: x:a -> {v:GHC.Integer.Type.Integer | v = x}
+  GHC.Real.toInteger :: x:a -> {v:Integer | v = x}
 
-// fixpoint can't handle (x mod y), only (x mod c) so we need to be more clever here
-// mod :: x:a -> y:a -> {v:a | v = (x mod y) }
+//  fixpoint can't handle (x mod y), only (x mod c) so we need to be more clever here
+//  mod :: x:a -> y:a -> {v:a | v = (x mod y) }
diff --git a/src/Liquid/Prelude/Totality.hs b/src/Liquid/Prelude/Totality.hs
--- a/src/Liquid/Prelude/Totality.hs
+++ b/src/Liquid/Prelude/Totality.hs
@@ -1,3 +1,8 @@
-module Liquid.Prelude.Totality where
+module Liquid.Prelude.Totality (module Exports) where
 
-import "base" Control.Exception.Base
+import GHC.Types
+import "base" Control.Exception.Base as Exports
+
+
+totalityError :: a -> Bool
+totalityError _ = False
diff --git a/src/Liquid/Prelude/Totality.spec b/src/Liquid/Prelude/Totality.spec
--- a/src/Liquid/Prelude/Totality.spec
+++ b/src/Liquid/Prelude/Totality.spec
@@ -1,6 +1,15 @@
 module spec Liquid.Prelude.Totality where
 
-assume Control.Exception.Base.patError :: {v:GHC.Prim.Addr# | 5 <4 } -> a
-assume Control.Exception.Base.recSelError :: {v:GHC.Prim.Addr# | 5 < 4 } -> a
-assume Control.Exception.Base.nonExhaustiveGuardsError :: {v:GHC.Prim.Addr# | 5 < 4 } -> a
-assume Control.Exception.Base.noMethodBindingError :: {v:GHC.Prim.Addr# | 5 < 4 } -> a
+
+measure totalityError :: a -> Bool
+
+
+assume Control.Exception.Base.patError :: {v:GHC.Prim.Addr# | totalityError "Pattern match(es) are non-exhaustive"} -> a
+
+assume Control.Exception.Base.recSelError :: {v:GHC.Prim.Addr# | totalityError "Use of partial record field selector"} -> a
+
+assume Control.Exception.Base.nonExhaustiveGuardsError :: {v:GHC.Prim.Addr# | totalityError "Guards are non-exhaustive"} -> a
+
+assume Control.Exception.Base.noMethodBindingError :: {v:GHC.Prim.Addr# | totalityError "Missing method(s) on instance declaration"} -> a
+
+assume Control.Exception.Base.recConError :: {v:GHC.Prim.Addr# | totalityError "Missing field in record construction"} -> a
diff --git a/src/Prelude.hs b/src/Prelude.hs
--- a/src/Prelude.hs
+++ b/src/Prelude.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE Trustworthy #-}
 module Prelude (module Exports) where
 
 import Data.Foldable
diff --git a/src/Prelude.spec b/src/Prelude.spec
--- a/src/Prelude.spec
+++ b/src/Prelude.spec
@@ -14,11 +14,11 @@
 import GHC.Err 
 
 
-// GHC.Types.D# :: x:_ -> {v:_ | v = x}
+//  GHC.Types.D# :: x:_ -> {v:_ | v = x}
 
 GHC.Err.error :: {v:_ | false} -> a 
 
-//assume GHC.Integer.smallInteger :: x:GHC.Prim.Int# -> { v:GHC.Integer.Type | v = (x :: int) }
+// assume GHC.Integer.smallInteger :: x:GHC.Prim.Int# -> { v:GHC.Integer.Type | v = (x :: int) }
 
 embed Integer           as int
 
@@ -27,7 +27,7 @@
 
 type IncrListD a  = [a]<{\x y -> (x+D) <= y}>
 
-//BOT: Do not delete EVER!
+// BOT: Do not delete EVER!
 
 qualif Bot(v:@(0))    : (0 = 1)
 qualif Bot(v:obj)     : (0 = 1)
@@ -53,16 +53,16 @@
 qualif True1(v:GHC.Types.Bool)   : (v)
 qualif False1(v:GHC.Types.Bool)  : (~ v)
 
-// REBARE constant papp1 : func(1, [Pred @(0); @(0); bool])
+//  REBARE constant papp1 : func(1, [Pred @(0); @(0); bool])
 qualif Papp(v:a, p:Pred a) : (papp1 p v)
 
-// REBARE constant papp2 : func(4, [Pred @(0) @(1); @(2); @(3); bool])
+//  REBARE constant papp2 : func(4, [Pred @(0) @(1); @(2); @(3); bool])
 qualif Papp2(v:a, x:b, p:Pred a b) : (papp2 p v x)
 
-// REBARE constant papp3 : func(6, [Pred @(0) @(1) @(2); @(3); @(4); @(5); bool])
+//  REBARE constant papp3 : func(6, [Pred @(0) @(1) @(2); @(3); @(4); @(5); bool])
 qualif Papp3(v:a, x:b, y:c, p:Pred a b c) : (papp3 p v x y)
 
-// qualif Papp4(v:a,x:b, y:c, z:d, p:Pred a b c d) : papp4(p, v, x, y, z)
-// REBARE constant papp4 : func(8, [Pred @(0) @(1) @(2) @(6); @(3); @(4); @(5); @(7); bool])
+//  qualif Papp4(v:a,x:b, y:c, z:d, p:Pred a b c d) : papp4(p, v, x, y, z)
+//  REBARE constant papp4 : func(8, [Pred @(0) @(1) @(2) @(6); @(3); @(4); @(5); @(7); bool])
 
-// REBARE constant runFun : func(2, [Arrow @(0) @(1); @(0); @(1)])
+//  REBARE constant runFun : func(2, [Arrow @(0) @(1); @(0); @(1)])