diff --git a/Changelog.md b/Changelog.md
--- a/Changelog.md
+++ b/Changelog.md
@@ -1,5 +1,10 @@
 # Changelog
 
+## 0.7.3.0
+
+* Supports GHC 9.8
+* Drops support for GHC <9
+
 ## 0.7.2.0
 
 * Supports GHC 9.6
diff --git a/examples/simple-arith-core.hs b/examples/simple-arith-core.hs
--- a/examples/simple-arith-core.hs
+++ b/examples/simple-arith-core.hs
@@ -8,19 +8,17 @@
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE DataKinds #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE NoStarIsType #-}
+{-# LANGUAGE NoStarIsType #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE ViewPatterns #-}
 {-# OPTIONS_GHC -dcore-lint #-}
 {-# OPTIONS_GHC -fplugin GHC.TypeLits.Presburger #-}
 {-# OPTIONS_GHC -ddump-tc-trace -ddump-to-file #-}
 
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 806
-{-# LANGUAGE NoStarIsType #-}
-{-# LANGUAGE PatternSynonyms #-}
-{-# LANGUAGE ViewPatterns #-}
-#endif
 
 module Main where
 
@@ -74,10 +72,8 @@
 absurdTrueFalse :: ( 'True :~: 'False) -> a
 absurdTrueFalse = \case {}
 
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ > 802
 hoge :: proxy n -> IsTrue (n + 1 <=? n) -> a
 hoge _ Witness = absurdTrueFalse Refl
-#endif
 
 bar :: (2 * (n + 1)) ~ (2 * n + 2) => proxy n -> ()
 bar _ = ()
diff --git a/ghc-typelits-presburger.cabal b/ghc-typelits-presburger.cabal
--- a/ghc-typelits-presburger.cabal
+++ b/ghc-typelits-presburger.cabal
@@ -1,13 +1,13 @@
 cabal-version: 1.12
 
--- This file has been generated from package.yaml by hpack version 0.35.0.
+-- This file has been generated from package.yaml by hpack version 0.35.2.
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: d47f404951bd3c54bbbabe3cea49f853ffe14cf61c99382f7240c493409fcdda
+-- hash: 979226dcc13643574c669d5607b3d16d2cb873154282a49ef47bfd9c8b52c073
 
 name:          ghc-typelits-presburger
-version:       0.7.2.0
+version:       0.7.3.0
 synopsis:      Presburger Arithmetic Solver for GHC Type-level natural numbers.
 description:   @ghc-typelits-presburger@ augments GHC type-system with Presburger
                Arithmetic Solver for Type-level natural numbers.
@@ -30,7 +30,7 @@
 license:       BSD3
 license-file:  LICENSE
 tested-with:
-    GHC==8.6.5 GHC==8.8.4 GHC==8.10.7 GHC==9.0.2 GHC==9.2.7 GHC==9.4.4 GHC==9.6.1
+    GHC==9.0.2 GHC==9.2.7 GHC==9.4.4 GHC==9.6.3 GHC==9.8.1
 extra-source-files:
     Changelog.md
 build-type:    Simple
@@ -59,7 +59,7 @@
   build-depends:
       base >=4.7 && <5
     , containers
-    , ghc <9.7
+    , ghc <9.9
     , ghc-tcplugins-extra >=0.2 && <0.5
     , mtl
     , pretty
diff --git a/src/Data/Integer/SAT.hs b/src/Data/Integer/SAT.hs
--- a/src/Data/Integer/SAT.hs
+++ b/src/Data/Integer/SAT.hs
@@ -12,39 +12,38 @@
   by
   Sergey Berezin, Vijay Ganesh, and David L. Dill
 -}
-module Data.Integer.SAT
-  ( PropSet,
-    noProps,
-    checkSat,
-    assert,
-    Prop (..),
-    Expr (..),
-    BoundType (..),
-    getExprBound,
-    getExprRange,
-    Name,
-    toName,
-    fromName,
+module Data.Integer.SAT (
+  PropSet,
+  noProps,
+  checkSat,
+  assert,
+  Prop (..),
+  Expr (..),
+  BoundType (..),
+  getExprBound,
+  getExprRange,
+  Name,
+  toName,
+  fromName,
 
-    -- * Iterators
-    allSolutions,
-    slnCurrent,
-    slnNextVal,
-    slnNextVar,
-    slnEnumerate,
+  -- * Iterators
+  allSolutions,
+  slnCurrent,
+  slnNextVal,
+  slnNextVar,
+  slnEnumerate,
 
-    -- * Debug
-    dotPropSet,
-    sizePropSet,
-    allInerts,
-    ppInerts,
+  -- * Debug
+  dotPropSet,
+  sizePropSet,
+  allInerts,
+  ppInerts,
 
-    -- * For QuickCheck
-    iPickBounded,
-    Bound (..),
-    tConst,
-  )
-where
+  -- * For QuickCheck
+  iPickBounded,
+  Bound (..),
+  tConst,
+) where
 
 import Control.Applicative (Alternative (..), Applicative (..), (<$>))
 import Control.Monad (MonadPlus (..), ap, guard, liftM)
@@ -281,13 +280,13 @@
 
 -- | The inert contains the solver state on one possible path.
 data Inerts = Inerts
-  { -- | Known lower and upper bounds for variables.
-    -- Each bound @(c,t)@ in the first list asserts that  @t < c * x@
-    -- Each bound @(c,t)@ in the second list asserts that @c * x < t@
-    bounds :: NameMap ([Bound], [Bound])
-  , -- | Definitions for resolved variables.
-    -- These form an idempotent substitution.
-    solved :: NameMap Term
+  { bounds :: NameMap ([Bound], [Bound])
+  -- ^ Known lower and upper bounds for variables.
+  -- Each bound @(c,t)@ in the first list asserts that  @t < c * x@
+  -- Each bound @(c,t)@ in the second list asserts that @c * x < t@
+  , solved :: NameMap Term
+  -- ^ Definitions for resolved variables.
+  -- These form an idempotent substitution.
   }
   deriving (Show)
 
@@ -295,7 +294,7 @@
 ppInerts is =
   vcat $
     [ppLower x b | (x, (ls, _)) <- bnds, b <- ls]
-    ++ [ppUpper x b | (x, (_, us)) <- bnds, b <- us]
+      ++ [ppUpper x b | (x, (_, us)) <- bnds, b <- us]
       ++ [ppEq e | e <- Map.toList (solved is)]
   where
     bnds = Map.toList (bounds is)
@@ -442,10 +441,10 @@
         Just s2 -> go s2 k
 
     hor s k =
-      s :
-      case slnNextVal s of
-        Nothing -> k
-        Just s1 -> hor s1 k
+      s
+        : case slnNextVal s of
+          Nothing -> k
+          Just s1 -> hor s1 k
 
 slnNextVal :: Solutions -> Maybe Solutions
 slnNextVal Done = Nothing
@@ -500,7 +499,7 @@
     -- <=> x   <= (t-1) `div` c
     normBound Upper (Bound c t) = do
       k <- isConst t
-      return (div (k -1) c)
+      return (div (k - 1) c)
 
 {- | The largest (resp. least) upper (resp. lower) bound on a term
  that will satisfy the model
@@ -542,7 +541,7 @@
       Lower -> fst
 
     scaleBound c b = case bt of
-      Upper -> div (b -1) c
+      Upper -> div (b - 1) c
       Lower -> div b c + 1
 
 iModel :: Inerts -> [(Name, Integer)]
@@ -581,29 +580,30 @@
   | Just a <- isConst t = guard (a == 0)
   -- A + B * x = 0
   | Just (a, b, x) <- tIsOneVar t =
-    case divMod (- a) b of
-      (q, 0) -> addDef x (tConst q)
-      _ -> mzero
+      case divMod (-a) b of
+        (q, 0) -> addDef x (tConst q)
+        _ -> mzero
   --  x + S = 0
   -- -x + S = 0
   | Just (xc, x, s) <- tGetSimpleCoeff t =
-    addDef x (if xc > 0 then tNeg s else s)
+      addDef x (if xc > 0 then tNeg s else s)
   -- A * S = 0
   | Just (_, s) <- tFactor t = solveIs0 s
   -- See Section 3.1 of paper for details.
   -- We obtain an equivalent formulation but with smaller coefficients.
   | Just (ak, xk, s) <- tLeastAbsCoeff t =
-    do
-      let m = abs ak + 1
-      v <- newVar
-      let sgn = signum ak
-          soln =
-            (negate sgn * m) |*| tVar v
-              |+| tMapCoeff (\c -> sgn * modulus c m) s
-      addDef xk soln
+      do
+        let m = abs ak + 1
+        v <- newVar
+        let sgn = signum ak
+            soln =
+              (negate sgn * m)
+                |*| tVar v
+                |+| tMapCoeff (\c -> sgn * modulus c m) s
+        addDef xk soln
 
-      let upd i = div (2 * i + m) (2 * m) + modulus i m
-      solveIs0 (negate (abs ak) |*| tVar v |+| tMapCoeff upd s)
+        let upd i = div (2 * i + m) (2 * m) + modulus i m
+        solveIs0 (negate (abs ak) |*| tVar v |+| tMapCoeff upd s)
   | otherwise = error "solveIs0: unreachable"
 
 modulus :: Integer -> Integer -> Integer
@@ -623,40 +623,40 @@
   | Just (_, s) <- tFactor t = solveIsNeg s
   -- See Section 5.1 of the paper
   | Just (xc, x, s) <- tLeastVar t =
-    do
-      ctrs <-
-        if xc < 0
-          then -- -XC*x + S < 0
-          -- S < XC*x
-          do
-            ubs <- getBounds Upper x
-            let b = negate xc
-                beta = s
-            addBound Lower x (Bound b beta)
-            return [(a, alpha, b, beta) | Bound a alpha <- ubs]
-          else -- XC*x + S < 0
-          -- XC*x < -S
-          do
-            lbs <- getBounds Lower x
-            let a = xc
-                alpha = tNeg s
-            addBound Upper x (Bound a alpha)
-            return [(a, alpha, b, beta) | Bound b beta <- lbs]
-
-      -- See Note [Shadows]
-      mapM_
-        ( \(a, alpha, b, beta) ->
+      do
+        ctrs <-
+          if xc < 0
+            then -- -XC*x + S < 0
+            -- S < XC*x
             do
-              let real = ctLt (a |*| beta) (b |*| alpha)
-                  dark = ctLt (tConst (a * b)) (b |*| alpha |-| a |*| beta)
-                  gray =
-                    [ ctEq (b |*| tVar x) (tConst i |+| beta)
-                    | i <- [1 .. b - 1]
-                    ]
-              solveIsNeg real
-              foldl orElse (solveIsNeg dark) (map solveIs0 gray)
-        )
-        ctrs
+              ubs <- getBounds Upper x
+              let b = negate xc
+                  beta = s
+              addBound Lower x (Bound b beta)
+              return [(a, alpha, b, beta) | Bound a alpha <- ubs]
+            else -- XC*x + S < 0
+            -- XC*x < -S
+            do
+              lbs <- getBounds Lower x
+              let a = xc
+                  alpha = tNeg s
+              addBound Upper x (Bound a alpha)
+              return [(a, alpha, b, beta) | Bound b beta <- lbs]
+
+        -- See Note [Shadows]
+        mapM_
+          ( \(a, alpha, b, beta) ->
+              do
+                let real = ctLt (a |*| beta) (b |*| alpha)
+                    dark = ctLt (tConst (a * b)) (b |*| alpha |-| a |*| beta)
+                    gray =
+                      [ ctEq (b |*| tVar x) (tConst i |+| beta)
+                      | i <- [1 .. b - 1]
+                      ]
+                solveIsNeg real
+                foldl orElse (solveIsNeg dark) (map solveIs0 gray)
+          )
+          ctrs
   | otherwise = error "solveIsNeg: unreachable"
 
 orElse :: S () -> S () -> S ()
@@ -712,7 +712,8 @@
 dotAnswer pp g0 = vcat [text "digraph {", nest 2 (fst $ go 0 g0), text "}"]
   where
     node x d =
-      integer x <+> brackets (text "label=" <> text (show d))
+      integer x
+        <+> brackets (text "label=" <> text (show d))
         <> semi
     edge x y = integer x <+> text "->" <+> integer y
 
@@ -746,9 +747,6 @@
     go None xs = xs
 
 instance Monad Answer where
-#if !MIN_VERSION_ghc(8,8,1)
-  fail _             = None
-#endif
   None >>= _ = None
   One a >>= k = k a
   Choice m1 m2 >>= k = mplus (m1 >>= k) (m2 >>= k)
diff --git a/src/GHC/TypeLits/Presburger/Compat.hs b/src/GHC/TypeLits/Presburger/Compat.hs
--- a/src/GHC/TypeLits/Presburger/Compat.hs
+++ b/src/GHC/TypeLits/Presburger/Compat.hs
@@ -1,18 +1,27 @@
-{-# LANGUAGE CPP, FlexibleInstances, PatternGuards, PatternSynonyms #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE OverloadedStrings #-}
-{-# LANGUAGE TypeSynonymInstances, ViewPatterns                     #-}
+{-# LANGUAGE PatternGuards #-}
 {-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE TypeSynonymInstances #-}
+{-# LANGUAGE ViewPatterns #-}
 {-# OPTIONS_GHC -Wno-orphans #-}
+
 module GHC.TypeLits.Presburger.Compat (module GHC.TypeLits.Presburger.Compat) where
-import Data.Function       (on)
-import GHC.TcPluginM.Extra as GHC.TypeLits.Presburger.Compat (evByFiat, lookupModule, lookupName,
-                                          tracePlugin)
-import Data.Generics.Twins
-import Data.Coerce (coerce)
 
-#if MIN_VERSION_ghc(9,0,0)
+import Data.Coerce (coerce)
+import Data.Function (on)
 import Data.Functor ((<&>))
+import Data.Generics.Twins
 import GHC.Builtin.Names as GHC.TypeLits.Presburger.Compat (gHC_TYPENATS)
+import GHC.Tc.Types.Constraint as GHC.TypeLits.Presburger.Compat (CtLoc (..), initialSubGoalDepth)
+import GHC.Tc.Types.Origin as GHC.TypeLits.Presburger.Compat (CtOrigin (..))
+import GHC.TcPluginM.Extra as GHC.TypeLits.Presburger.Compat (
+  evByFiat,
+  lookupModule,
+  lookupName,
+  tracePlugin,
+ )
 #if MIN_VERSION_ghc(9,4,1)
 import GHC.Tc.Types as GHC.TypeLits.Presburger.Compat (TcPlugin (..), TcPluginSolveResult (..))
 import GHC.Builtin.Types as GHC.TypeLits.Presburger.Compat (cTupleTyCon, cTupleDataCon)
@@ -30,16 +39,13 @@
 import GHC.Builtin.Names as GHC.TypeLits.Presburger.Compat (dATA_TYPE_EQUALITY)
 import qualified GHC.Builtin.Names as Old
 #endif
-import GHC.Hs as GHC.TypeLits.Presburger.Compat (HsModule(..), NoExtField(..))
-import GHC.Hs.ImpExp as GHC.TypeLits.Presburger.Compat (ImportDecl(..), ImportDeclQualifiedStyle(..))
-import GHC.Hs.Extension as GHC.TypeLits.Presburger.Compat (GhcPs)
-import GHC.Builtin.Types as GHC.TypeLits.Presburger.Compat
-  ( boolTyCon,
-    eqTyConName,
-    promotedEQDataCon,
-    promotedGTDataCon,
-    promotedLTDataCon,
-  )
+import GHC.Builtin.Types as GHC.TypeLits.Presburger.Compat (
+  boolTyCon,
+  eqTyConName,
+  promotedEQDataCon,
+  promotedGTDataCon,
+  promotedLTDataCon,
+ )
 import qualified GHC.Builtin.Types as TysWiredIn
 import GHC.Builtin.Types.Literals as GHC.TypeLits.Presburger.Compat
 import GHC.Core.Class as GHC.TypeLits.Presburger.Compat (className, classTyCon)
@@ -50,16 +56,19 @@
 import GHC.Core.TyCon as GHC.TypeLits.Presburger.Compat
 import qualified GHC.Core.Type as Old
 import GHC.Core.Unify as Old (tcUnifyTy)
+import GHC.Data.FastString as GHC.TypeLits.Presburger.Compat (FastString, fsLit, unpackFS)
+import GHC.Hs as GHC.TypeLits.Presburger.Compat (HsModule (..), NoExtField (..))
+import GHC.Hs.Extension as GHC.TypeLits.Presburger.Compat (GhcPs)
+import GHC.Hs.ImpExp as GHC.TypeLits.Presburger.Compat (ImportDecl (..), ImportDeclQualifiedStyle (..))
 import GHC.Unit.Types (Module, UnitId, toUnitId)
 import GHC.Unit.Types as GHC.TypeLits.Presburger.Compat (mkModule)
-import GHC.Data.FastString as GHC.TypeLits.Presburger.Compat (FastString, fsLit, unpackFS)
 #if MIN_VERSION_ghc(9,2,0)
 import GHC.Driver.Env.Types as GHC.TypeLits.Presburger.Compat (HscEnv (hsc_dflags))
 #else
 import GHC.Driver.Types as GHC.TypeLits.Presburger.Compat (HscEnv (hsc_dflags))
 import GHC.Driver.Session (unitState, unitDatabases)
 #endif
-import GHC.Plugins (InScopeSet, Outputable, emptyUFM, moduleUnit, Unit, Name)
+import GHC.Plugins (InScopeSet, Name, Outputable, Unit, emptyUFM, moduleUnit)
 #if MIN_VERSION_ghc(9,2,0)
 import GHC.Hs as GHC.TypeLits.Presburger.Compat (HsParsedModule(..))
 import GHC.Types.TyThing as GHC.TypeLits.Presburger.Compat (lookupTyCon)
@@ -89,33 +98,36 @@
   )
 #endif
 
-import GHC.Plugins as GHC.TypeLits.Presburger.Compat
-  ( PackageName (..),isStrLitTy, isNumLitTy,
-    nilDataCon, consDataCon,
-    Hsc,
-    Plugin (..),
-    TvSubstEnv,
-    TyVar,
-    defaultPlugin,
-    mkTcOcc,
-    UnitDatabase(..),
-    GenericUnitInfo(..),
-    elementOfUniqSet,
-    mkUniqSet,
-    mkTyConTy,
-    mkTyVarTy,
-    ppr,
-    promotedFalseDataCon,
-    promotedTrueDataCon,
-    purePlugin,
-    splitTyConApp,
-    splitTyConApp_maybe,
-    text,
-    tyConAppTyCon_maybe,
-    typeKind,
-  )
-import GHC.Tc.Plugin (lookupOrig)
 import GHC.Core.InstEnv as GHC.TypeLits.Presburger.Compat (classInstances)
+import GHC.Plugins as GHC.TypeLits.Presburger.Compat (
+  GenericUnitInfo (..),
+  Hsc,
+  PackageName (..),
+  Plugin (..),
+  TvSubstEnv,
+  TyVar,
+  UnitDatabase (..),
+  consDataCon,
+  defaultPlugin,
+  elementOfUniqSet,
+  isNumLitTy,
+  isStrLitTy,
+  mkTcOcc,
+  mkTyConTy,
+  mkTyVarTy,
+  mkUniqSet,
+  nilDataCon,
+  ppr,
+  promotedFalseDataCon,
+  promotedTrueDataCon,
+  purePlugin,
+  splitTyConApp,
+  splitTyConApp_maybe,
+  text,
+  tyConAppTyCon_maybe,
+  typeKind,
+ )
+import GHC.Tc.Plugin (lookupOrig)
 #if MIN_VERSION_ghc(9,2,0)
 import GHC.Tc.Plugin (unsafeTcPluginTcM)
 import GHC.Utils.Logger (getLogger)
@@ -124,127 +136,40 @@
 import GHC.Driver.Types as GHC.TypeLits.Presburger.Compat (IsBootInterface(..))
 #endif
 
-import GHC.Tc.Plugin as GHC.TypeLits.Presburger.Compat
-  ( TcPluginM,
-    getInstEnvs,
-    newFlexiTyVar,
-    getTopEnv,
-    lookupOrig,
-    newFlexiTyVar,
-    newWanted,
-    matchFam,
-    tcLookupClass,
-    tcLookupTyCon,
-    tcPluginIO,
-    tcPluginTrace,
-  )
+import GHC.Tc.Plugin as GHC.TypeLits.Presburger.Compat (
+  TcPluginM,
+  getInstEnvs,
+  getTopEnv,
+  lookupOrig,
+  matchFam,
+  newFlexiTyVar,
+  newWanted,
+  tcLookupClass,
+  tcLookupTyCon,
+  tcPluginIO,
+  tcPluginTrace,
+ )
 import GHC.Tc.Types as GHC.TypeLits.Presburger.Compat (TcPlugin (..))
-import GHC.Tc.Types.Constraint as GHC.TypeLits.Presburger.Compat
-  ( Ct,
-    CtEvidence,
-    ctEvPred,
-    ctEvidence,
-    isWanted,
-  )
+import GHC.Tc.Types.Constraint as GHC.TypeLits.Presburger.Compat (
+  Ct,
+  CtEvidence,
+  ctEvPred,
+  ctEvidence,
+  isWanted,
+ )
 import GHC.Tc.Types.Evidence as GHC.TypeLits.Presburger.Compat (EvTerm)
+import GHC.Tc.Utils.Monad as GHC.TypeLits.Presburger.Compat (getCtLocM, unsafeTcPluginTcM)
 import GHC.Tc.Utils.TcType (TcTyVar, TcType)
 import GHC.Tc.Utils.TcType as GHC.TypeLits.Presburger.Compat (tcTyFamInsts)
 import qualified GHC.TcPluginM.Extra as Extra
 import GHC.Types.Name.Occurrence as GHC.TypeLits.Presburger.Compat (emptyOccSet, mkInstTyTcOcc)
 import GHC.Types.Unique as GHC.TypeLits.Presburger.Compat (getKey, getUnique)
 import GHC.Unit.Module as GHC.TypeLits.Presburger.Compat (ModuleName, mkModuleName)
+import GHC.Unit.State (UnitState (preloadUnits), initUnits)
 import GHC.Unit.State as GHC.TypeLits.Presburger.Compat (lookupPackageName)
-import GHC.Unit.State (initUnits, UnitState (preloadUnits))
-import GHC.Unit.Types (UnitId(..), fsToUnit, toUnitId)
+import GHC.Unit.Types (UnitId (..), fsToUnit, toUnitId)
 import GHC.Utils.Outputable as GHC.TypeLits.Presburger.Compat (showSDocUnsafe)
--- GHC 9 Ends HERE
-#else
-import UniqSet
-import PackageConfig
-import Class as GHC.TypeLits.Presburger.Compat (classTyCon, className)
-import FastString as GHC.TypeLits.Presburger.Compat (FastString, fsLit, unpackFS)
-import GhcPlugins (InScopeSet, Outputable, emptyUFM, InstalledUnitId(..), initPackages, Name, listPackageConfigMap)
-import GhcPlugins as GHC.TypeLits.Presburger.Compat (PackageName (..), fsToUnitId, lookupPackageName, lookupTyCon, mkTcOcc, mkTyConTy, ppr, promotedFalseDataCon, promotedTrueDataCon, text, tyConAppTyCon_maybe, typeKind, typeNatKind)
-import HscTypes as GHC.TypeLits.Presburger.Compat (HscEnv (hsc_dflags))
-import Module as GHC.TypeLits.Presburger.Compat (ModuleName, mkModuleName, mkModule)
-import Module (Module, UnitId)
-import OccName as GHC.TypeLits.Presburger.Compat (emptyOccSet, mkInstTyTcOcc)
-import Outputable as GHC.TypeLits.Presburger.Compat (showSDocUnsafe)
-import Plugins as GHC.TypeLits.Presburger.Compat (Plugin (..), defaultPlugin)
-import PrelNames as GHC.TypeLits.Presburger.Compat (gHC_TYPENATS, dATA_TYPE_EQUALITY)
-import qualified PrelNames as Old
-import TcEvidence as GHC.TypeLits.Presburger.Compat (EvTerm)
-import TcHsType as GHC.TypeLits.Presburger.Compat (tcInferApps)
-import TcPluginM as GHC.TypeLits.Presburger.Compat
-  ( TcPluginM,
-    getTopEnv,
-    lookupOrig,
-    matchFam,
-    newFlexiTyVar,
-    newWanted,
-    tcLookupClass,
-    tcLookupTyCon,
-    tcPluginIO,
-    tcPluginTrace,
-  )
-import TcRnMonad as GHC.TypeLits.Presburger.Compat (TcPluginResult (..))
-import TcRnTypes as GHC.TypeLits.Presburger.Compat (TcPlugin (..))
-import TcType as GHC.TypeLits.Presburger.Compat (tcTyFamInsts)
-import TcTypeNats as GHC.TypeLits.Presburger.Compat
-import TyCoRep ()
-import TyCoRep as GHC.TypeLits.Presburger.Compat (TyLit (NumTyLit), Type (..))
-import TyCon as GHC.TypeLits.Presburger.Compat
-import Type as GHC.TypeLits.Presburger.Compat (TCvSubst (..), TvSubstEnv, emptyTCvSubst, eqType, mkTyVarTy, splitTyConApp, splitTyConApp_maybe, unionTCvSubst)
-import qualified Type as Old
-import TysWiredIn as GHC.TypeLits.Presburger.Compat
-  ( boolTyCon,
-    promotedEQDataCon,
-    promotedGTDataCon,
-    promotedLTDataCon,
-  )
-import Unify as Old (tcUnifyTy)
-import Unique as GHC.TypeLits.Presburger.Compat (getKey, getUnique)
-import Var as GHC.TypeLits.Presburger.Compat (TyVar)
--- Conditional imports for GHC <9
-#if MIN_VERSION_ghc(8,4,1)
-import TcType (TcTyVar, TcType)
-import qualified GHC.TcPluginM.Extra as Extra
-import qualified GHC
-#else
-import Data.Maybe
-import TcPluginM (zonkCt)
-import TcRnTypes (cc_ev, ctev_pred)
-#endif
-#if MIN_VERSION_ghc(8,6,0)
-import Plugins as GHC.TypeLits.Presburger.Compat (purePlugin)
-#endif
-#if MIN_VERSION_ghc(8,8,1)
-import Name
-import TysWiredIn as GHC.TypeLits.Presburger.Compat (eqTyConName) 
-import qualified TysWiredIn
-#else
-import PrelNames as GHC.TypeLits.Presburger.Compat (eqTyConName) 
-#endif
 
-#if MIN_VERSION_ghc(8,10,1)
-import Predicate as GHC.TypeLits.Presburger.Compat (EqRel (..), Pred(..))
-import Predicate as GHC.TypeLits.Presburger.Compat (isEqPred)
-import GHC (NoExtField(..))
-import qualified Predicate as Old (classifyPredType)
-import Predicate as GHC.TypeLits.Presburger.Compat  (mkPrimEqPredRole)
-import Constraint as GHC.TypeLits.Presburger.Compat 
-    (Ct, ctEvidence, CtEvidence, ctEvPred, isWanted)
-#else
-import GHC (NoExt(..))
-import GhcPlugins as GHC.TypeLits.Presburger.Compat (EqRel (..), PredTree (..))
-import GhcPlugins as GHC.TypeLits.Presburger.Compat (isEqPred)
-import qualified GhcPlugins as Old (classifyPredType)
-import TcRnMonad as GHC.TypeLits.Presburger.Compat (Ct, isWanted)
-import Type      as GHC.TypeLits.Presburger.Compat (mkPrimEqPredRole)
-import TcRnTypes as GHC.TypeLits.Presburger.Compat (ctEvPred, ctEvidence)
-#endif
-#endif
-
 #if !MIN_VERSION_ghc(9,4,1)
 type TcPluginSolveResult = TcPluginResult
 #endif
@@ -254,12 +179,8 @@
 dATA_TYPE_EQUALITY = mkBaseModule "Data.Type.Equality"
 #endif
 
-#if MIN_VERSION_ghc(8,10,1)
 type PredTree = Pred
-#endif
 
-
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 800
 data TvSubst = TvSubst InScopeSet TvSubstEnv
 
 #if MIN_VERSION_ghc(9,6,1)
@@ -271,8 +192,7 @@
 emptyTCvSubst = emptySubst
 #endif
 
-
-instance Outputable  TvSubst where
+instance Outputable TvSubst where
   ppr = ppr . toTCv
 
 emptyTvSubst :: TvSubst
@@ -284,7 +204,6 @@
   TCvSubst set tvsenv _ -> TvSubst set tvsenv
 #endif
 
-
 toTCv :: TvSubst -> TCvSubst
 #if MIN_VERSION_ghc(9,6,1)
 toTCv (TvSubst set tvenv) = Subst set emptyUFM tvenv emptyUFM
@@ -292,7 +211,6 @@
 toTCv (TvSubst set tvenv) = TCvSubst set tvenv emptyUFM
 #endif
 
-
 substTy :: TvSubst -> Type -> Type
 substTy tvs = Old.substTy (toTCv tvs)
 
@@ -307,7 +225,6 @@
 fromTCv (TCvSubst set tvsenv _) = TvSubst set tvsenv
 #endif
 
-
 promotedBoolTyCon :: TyCon
 promotedBoolTyCon = boolTyCon
 
@@ -316,52 +233,23 @@
   | Old.isFunTy t = Just (t1, t2)
 viewFunTy _ = Nothing
 
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 802
-#else
-pattern FunTy :: Type -> Type -> Type
-pattern FunTy t1 t2 <- (viewFunTy -> Just (t1, t2)) where
-  FunTy t1 t2 = Old.mkFunTy t1 t2
-#endif
-
 tcUnifyTy :: Type -> Type -> Maybe TvSubst
 tcUnifyTy t1 t2 = fromTCv <$> Old.tcUnifyTy t1 t2
 
 getEqTyCon :: TcPluginM TyCon
 getEqTyCon =
-#if MIN_VERSION_ghc(8,8,1)
   return TysWiredIn.eqTyCon
-#else
-  tcLookupTyCon Old.eqTyConName
-#endif
 
-#else
-eqType :: Type -> Type -> Bool
-eqType = (==)
-
-getEqTyCon :: TcPluginM TyCon
-getEqTyCon = return Old.eqTyCon
-
-#endif
-
-
 getEqWitnessTyCon :: TcPluginM TyCon
 getEqWitnessTyCon = do
   md <- lookupModule (mkModuleName "Data.Type.Equality") (fsLit "base")
   tcLookupTyCon =<< lookupOrig md (mkTcOcc ":~:")
 
 decompFunTy :: Type -> [Type]
-#if MIN_VERSION_ghc(9,0,0)
 decompFunTy (FunTy _ _ t1 t2) = t1 : decompFunTy t2
-#else
-#if MIN_VERSION_ghc(8,10,1)
-decompFunTy (FunTy _ t1 t2) = t1 : decompFunTy t2
-#else
-decompFunTy (FunTy t1 t2) = t1 : decompFunTy t2
-#endif
-#endif
-decompFunTy t             = [t]
+decompFunTy t = [t]
 
-newtype TypeEq = TypeEq { runTypeEq :: Type }
+newtype TypeEq = TypeEq {runTypeEq :: Type}
 
 instance Eq TypeEq where
   (==) = geq `on` runTypeEq
@@ -375,15 +263,13 @@
     EqPred _ l r -> l `eqType` r
     _ -> False
 
-normaliseGivens
-  :: [Ct] -> TcPluginM [Ct]
+normaliseGivens ::
+  [Ct] -> TcPluginM [Ct]
 normaliseGivens =
-#if MIN_VERSION_ghc(8,4,1)
-  fmap (return . filter (not . isTrivial . ctEvPred . ctEvidence)) 
-  . (++) <$> id <*> Extra.flattenGivens
-#else
-  mapM zonkCt 
-#endif
+  fmap (return . filter (not . isTrivial . ctEvPred . ctEvidence))
+    . (++)
+    <$> id
+    <*> Extra.flattenGivens
 
 #if MIN_VERSION_ghc(8,4,1)
 type Substitution = [(TcTyVar, TcType)]
@@ -392,53 +278,25 @@
 #endif
 
 subsCt :: Substitution -> Ct -> Ct
-subsCt =
-#if MIN_VERSION_ghc(8,4,1)
-  Extra.substCt
-#else
-  \subst ct ->
-  ct { cc_ev = (cc_ev ct) {ctev_pred = substTy subst (ctev_pred (cc_ev ct))}
-     }
-#endif
+subsCt = Extra.substCt
 
 subsType :: Substitution -> Type -> Type
-subsType =
-#if MIN_VERSION_ghc(8,4,1)
-  Extra.substType
-#else
-  substTy
-#endif
+subsType = Extra.substType
 
 mkSubstitution :: [Ct] -> Substitution
-mkSubstitution =
-#if MIN_VERSION_ghc(8,4,1)
-  map fst . Extra.mkSubst'
-#else
-  foldr (unionTvSubst . genSubst) emptyTvSubst
-#endif
-
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 804
-genSubst :: Ct -> TvSubst
-genSubst ct = case classifyPredType (ctEvPred . ctEvidence $ ct) of
-  EqPred NomEq t u -> fromMaybe emptyTvSubst $ GHC.TypeLits.Presburger.Compat.tcUnifyTy t u
-  _                -> emptyTvSubst
-#endif
-
+mkSubstitution = map fst . Extra.mkSubst'
 
 classifyPredType :: Type -> PredTree
 classifyPredType ty = case Old.classifyPredType ty of
-  e@EqPred{} -> e
-  ClassPred cls [_,t1,t2]
-    | className cls == eqTyConName
-    -> EqPred NomEq t1 t2
+  e@EqPred {} -> e
+  ClassPred cls [_, t1, t2]
+    | className cls == eqTyConName ->
+        EqPred NomEq t1 t2
   e -> e
 
-#if MIN_VERSION_ghc(9,0,0)
 fsToUnitId :: FastString -> UnitId
 fsToUnitId = toUnitId . fsToUnit
-#endif
 
-#if MIN_VERSION_ghc(9,0,0)
 loadedPackageNames ::
   [UnitDatabase UnitId] ->
   UnitState ->
@@ -447,11 +305,10 @@
   let preloads = mkUniqSet $ map (\(UnitId p) -> p) $ preloadUnits us
       ents = filter ((`elementOfUniqSet` preloads) . unitIdFS . unitId) $ concatMap unitDatabaseUnits unitDb
    in map (coerce . unitPackageName) ents
-#endif
 
-
 type RawPackageName = FastString
-preloadedUnitsM :: TcPluginM [RawPackageName] 
+
+preloadedUnitsM :: TcPluginM [RawPackageName]
 #if MIN_VERSION_ghc(9,4,0)
 preloadedUnitsM = do
   logger <- unsafeTcPluginTcM getLogger
@@ -489,45 +346,16 @@
   pure packNames
 #endif
 
-
-#if MIN_VERSION_ghc(9,0,0)
 type ModuleUnit = Unit
+
 moduleUnit' :: Module -> ModuleUnit
 moduleUnit' = moduleUnit
-#else
-type ModuleUnit = UnitId
-moduleUnit' :: Module -> ModuleUnit
-moduleUnit' = GHC.moduleUnitId
-#endif
 
-#if !MIN_VERSION_ghc(8,10,1)
-type NoExtField = NoExt
-#endif
-
 noExtField :: NoExtField
-#if MIN_VERSION_ghc(8,10,1)
 noExtField = NoExtField
-#else
-noExtField = NoExt
-#endif
 
-#if MIN_VERSION_ghc(9,0,1)
 type HsModule' = HsModule
-#else
-type HsModule' = GHC.HsModule GHC.GhcPs
-#endif
 
-#if !MIN_VERSION_ghc(9,0,1)
-type IsBootInterface = Bool
-pattern NotBoot :: IsBootInterface
-pattern NotBoot = False
-
-pattern IsBoot :: IsBootInterface
-pattern IsBoot = True
-
-{-# COMPLETE NotBoot, IsBoot #-}
-
-#endif
 #if MIN_VERSION_ghc(9,2,0)
 typeNatKind :: TcType
 typeNatKind = naturalTy
@@ -568,8 +396,8 @@
 lookupAssertTyCon = pure Nothing
 #endif
 
-
 lookupTyNatPredLt :: TcPluginM (Maybe TyCon)
+
 -- Note:  base library shipepd with 9.2.1 has a wrong implementation;
 -- hence we MUST NOT desugar it with <= 9.2.1
 #if MIN_VERSION_ghc(9,2,2)
@@ -643,7 +471,6 @@
 lookupTyGenericCompare = pure Nothing
 #endif
 
-
 lookupBool47 :: String -> TcPluginM (Maybe TyCon)
 #if MIN_VERSION_base(4,17,0)
 lookupBool47 nam = Just <$> do
@@ -658,8 +485,7 @@
 lookupTyAnd = lookupBool47 "&&"
 lookupTyOr = lookupBool47 "||"
 
-
-matchFam' :: TyCon -> [Type] -> TcPluginM (Maybe  Type)
+matchFam' :: TyCon -> [Type] -> TcPluginM (Maybe Type)
 #if MIN_VERSION_ghc(9,4,1)
 matchFam' con args = fmap reductionReducedType <$> matchFam con args
 #else
diff --git a/src/GHC/TypeLits/Presburger/Types.hs b/src/GHC/TypeLits/Presburger/Types.hs
--- a/src/GHC/TypeLits/Presburger/Types.hs
+++ b/src/GHC/TypeLits/Presburger/Types.hs
@@ -18,6 +18,7 @@
 {-# LANGUAGE NamedFieldPuns #-}
 {-# LANGUAGE PartialTypeSignatures #-}
 {-# OPTIONS_GHC -Wno-partial-type-signatures #-}
+
 -- | Since 0.3.0.0
 module GHC.TypeLits.Presburger.Types
   ( pluginWith,
@@ -106,9 +107,7 @@
 pluginWith trans =
   defaultPlugin
     { tcPlugin = Just . presburgerPlugin trans . procOpts
-#if MIN_VERSION_ghc(8,6,0)
     , pluginRecompile = purePlugin
-#endif
     }
   where
     procOpts opts
@@ -733,15 +732,7 @@
 
 simpleExp :: Given Translation => Type -> Type
 simpleExp (AppTy t1 t2) = AppTy (simpleExp t1) (simpleExp t2)
-#if MIN_VERSION_ghc(9,0,0)
 simpleExp (FunTy f m t1 t2) = FunTy f m (simpleExp t1) (simpleExp t2)
-#else
-#if MIN_VERSION_ghc(8,10,1)
-simpleExp (FunTy f t1 t2) = FunTy f (simpleExp t1) (simpleExp t2)
-#else
-simpleExp (FunTy t1 t2) = FunTy (simpleExp t1) (simpleExp t2)
-#endif
-#endif 
 simpleExp (ForAllTy t1 t2) = ForAllTy t1 (simpleExp t2)
 simpleExp (TyConApp tc (lastTwo -> ts)) =
   fromMaybe (TyConApp tc (map simpleExp ts)) $
@@ -767,11 +758,13 @@
 
 type Machine = MaybeT (StateT ParseEnv TcPluginM)
 
+
 runMachine :: Machine a -> TcPluginM (Maybe a)
 runMachine act = do
   (ma, dic) <- runStateT (runMaybeT act) M.empty
-  forM_ (M.toList dic) $ \(TypeEq ty, var) ->
-    newWanted undefined $ mkPrimEqPredRole Nominal (mkTyVarTy var) ty
+  forM_ (M.toList dic) $ \(TypeEq ty, var) -> do
+    loc <- unsafeTcPluginTcM $ getCtLocM (Shouldn'tHappenOrigin "runMachine dummy wanted") Nothing
+    newWanted loc $ mkPrimEqPredRole Nominal (mkTyVarTy var) ty
   return ma
 
 toVar :: Type -> Machine TyVar