diff --git a/Changelog.md b/Changelog.md
new file mode 100644
--- /dev/null
+++ b/Changelog.md
@@ -0,0 +1,54 @@
+# Changelog
+
+## 0.7.4.0
+
+* Supports GHC 9.10
+* Drops GHC <9.2
+
+## 0.7.3.0
+
+* Supports GHC 9.8
+* Drops support for GHC <9
+
+## 0.7.2.0
+
+* Supports GHC 9.6
+* More robust `equational-reasoning` package detection logic.
+
+## 0.7.1.0
+
+* Proper Support of GHC 9.4 (Now can solve `Assert` properly)
+
+## 0.7.0.0
+
+* Support GHC 9.4
+* The plugin can solve constraints involving type-level `Assert`, `Not`, `(&&)`, `(||)`, and/or `If` from new base.
+
+## 0.6.2.0
+
+* Support GHC 9.2.1
+* Decoding in Min/Max expression in terms of OrdCond
+
+## 0.6.0.0
+
+* Stop discharging redundant constraints
+* Support GHC 9.0.1
+* Drop a support for GHC <8.6
+
+## 0.4.0.0
+
+* Fixes constraint solving (fixes #9); this may change the previous (unsound) behaviour, and hence it is breaking change.
+
+## 0.3.0.1
+
+* Supports GHC >= 8.10.
+
+## 0.3.0.0
+
+* Drops support for GHC < 8.4
+* Entire overhaul.
+* Adds `negated-numbers` option.
+* Allows terms which includes uninterpreted terms (still much incomplete).
+* Separates `singletons` support as `singletons-presburger` package.
+* Provides an interface for extending solver with additional syntax constructs.
+  See `GHC.TypeLits.Presburger.Types` module for more detail.
diff --git a/examples/simple-arith-core.hs b/examples/simple-arith-core.hs
new file mode 100644
--- /dev/null
+++ b/examples/simple-arith-core.hs
@@ -0,0 +1,206 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE EmptyCase #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE NoStarIsType #-}
+{-# OPTIONS_GHC -dcore-lint #-}
+{-# OPTIONS_GHC -ddump-tc-trace -ddump-to-file #-}
+{-# OPTIONS_GHC -fplugin GHC.TypeLits.Presburger #-}
+
+module Main where
+
+import Data.Proxy
+import Data.Type.Equality
+import Data.Void
+import GHC.TypeLits hiding (SNat)
+import Numeric.Natural
+import Proof.Propositional (Empty (..), IsTrue (Witness), withEmpty)
+import Unsafe.Coerce
+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 902
+import qualified Data.Type.Ord as DTO
+#endif
+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 904
+import Data.Type.Bool
+#endif
+
+main :: IO ()
+main = putStrLn "finished"
+
+type n <=! m = IsTrue (n <=? m)
+
+infix 4 <=!
+
+type family Length (as :: [k]) where
+  Length '[] = 0
+  Length (x ': xs) = 1 + Length xs
+
+natLen ::
+  (Length xs <= Length ys) =>
+  proxy xs ->
+  proxy ys ->
+  (Length ys - Length xs) + Length xs :~: Length ys
+natLen _ _ = Refl
+
+natLeqZero' :: (n <= 0) => proxy n -> n :~: 0
+natLeqZero' _ = Refl
+
+leqSucc :: proxy n -> proxy m -> IsTrue ((n + 1) <=? m) -> CmpNat n m :~: 'LT
+leqSucc _ _ Witness = Refl
+
+leqEquiv :: (n <= m) => p n -> p m -> IsTrue (n <=? m)
+leqEquiv _ _ = Witness
+
+plusLeq :: (n <= m) => proxy (n :: Nat) -> proxy m -> ((m - n) + n :~: m)
+plusLeq _ _ = Refl
+
+minusLeq :: (n <= m) => proxy (n :: Nat) -> proxy m -> IsTrue ((m - n) + n <=? m)
+minusLeq _ _ = Witness
+
+absurdTrueFalse :: ('True :~: 'False) -> a
+absurdTrueFalse = \case {}
+
+hoge :: proxy n -> IsTrue (n + 1 <=? n) -> a
+hoge _ Witness = absurdTrueFalse Refl
+
+bar :: ((2 * (n + 1)) ~ (2 * n + 2)) => proxy n -> ()
+bar _ = ()
+
+barResult :: ()
+barResult = bar (Proxy :: Proxy 2)
+
+trans :: proxy n -> proxy m -> n <=! m -> (n + 1) <=! (m + 1)
+trans _ _ Witness = Witness
+
+eqv :: proxy n -> proxy m -> (n <=? m) :~: ((n + 1) <=? (m + 1))
+eqv _ _ = Refl
+
+predSuccBool :: forall proxy n. ((n <=? 0) ~ 'False) => proxy n -> IsTrue (n + 1 <=? 2 * n)
+predSuccBool _ = Witness
+
+predSuccProp :: forall proxy n. (Empty (n <=! 0)) => proxy n -> IsTrue (n + 1 <=? 2 * n)
+predSuccProp _ = Witness
+
+succLEqLTSucc :: pxy m -> CmpNat 0 (m + 1) :~: 'LT
+succLEqLTSucc _ = Refl
+
+succCompare :: pxy n -> pxy m -> CmpNat n m :~: CmpNat (n + 1) (m + 1)
+succCompare _ _ = Refl
+
+eqToRefl :: pxy n -> pxy m -> CmpNat n m :~: 'EQ -> n :~: m
+eqToRefl _n _m Refl = Refl
+
+rangeEql ::
+  ((n == 0) ~ 'False) =>
+  pxy n ->
+  (1 <=? n) :~: 'True
+rangeEql _ = Refl
+
+rangeEqlLeq ::
+  ((n == 3) ~ 'False, n <= 3) =>
+  pxy n ->
+  (n <=? 2) :~: 'True
+rangeEqlLeq _ = Refl
+
+data NProxy (n :: Nat) = NProxy
+
+-- GHC >= 9.2 only Tests
+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 902
+
+ghc92NLeqToGt :: (n DTO.<=? m) ~ 'False 
+  => NProxy n -> NProxy m -> (n DTO.>? m) :~: 'True
+ghc92NLeqToGt _ _ = Refl
+
+ghc92GtToGeq :: (n DTO.> m)
+  => NProxy n -> NProxy m -> (n DTO.>=? m) :~: 'True
+ghc92GtToGeq _ _ = Refl
+
+ghc92GeqEquivNLt :: NProxy n -> NProxy m -> (n DTO.>=? m) :~: ((n DTO.<? m) == 'False)
+ghc92GeqEquivNLt _ _ = Refl
+
+-- N.B. We can't replace with predicate style with GHC 9.2.1
+-- by the bug in base-4.16.0.0
+ghc92NLtToGeq :: (n DTO.<? m) ~ 'True
+  => NProxy n -> NProxy m -> (n DTO.>=? m) :~: 'False
+ghc92NLtToGeq _ _ = Refl
+
+minLeq :: n <= m => NProxy n -> NProxy m -> DTO.Min n m :~: n
+minLeq _ _ = Refl
+
+maxLeq :: n <= m => NProxy n -> NProxy m -> DTO.Max n m :~: m
+maxLeq _ _ = Refl
+
+mkOrd :: forall n m. (n DTO.< m) => NProxy n -> NProxy m
+mkOrd _ = NProxy
+
+maxOrd :: forall n. (0 DTO.< n) => NProxy n
+maxOrd = mkOrd (NProxy @(n - 1))
+#endif
+
+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 904
+leqGeqToEq :: NProxy n -> NProxy m -> IsTrue (n <=? m && m <=? n) -> n :~: m
+leqGeqToEq _ _ Witness = Refl
+
+leqTotal :: NProxy n -> NProxy m -> IsTrue (n <=? m || m <=? n)
+leqTotal _ _ = Witness
+
+zeroMinimal :: NProxy n -> (n DTO.<? 0) :~: 'False
+zeroMinimal _ = Refl
+
+zeroMinimal' :: NProxy n -> IsTrue (Not (n DTO.<? 0))
+zeroMinimal' _ = Witness
+
+caseZero :: NProxy n -> IsTrue (If (n DTO.<=? 0) (n == 0) (n DTO.>? 0))
+caseZero _ = Witness
+
+succGtZero :: NProxy n -> IsTrue (0 DTO.<? If (n == 0) (n + 1) n)
+succGtZero _ = Witness
+#endif
+
+succStepBack :: (Succ n <= Succ m) => NProxy n -> NProxy m -> IsTrue (n <=? m)
+succStepBack _ _ = Witness
+
+type Succ n = n + 1
+
+data Leq n m where
+  ZeroLeq :: SNat m -> Leq 0 m
+  SuccLeqSucc :: Leq n m -> Leq (n + 1) (m + 1)
+
+newtype SNat n = SNat Natural
+
+data ZeroOrSucc n where
+  IsZero :: ZeroOrSucc 0
+  IsSucc ::
+    SNat n ->
+    ZeroOrSucc (n + 1)
+
+viewNat :: forall n. SNat n -> ZeroOrSucc n
+viewNat (SNat n) =
+  if n == 0
+    then unsafeCoerce IsZero
+    else unsafeCoerce (SNat (n - 1))
+
+pattern Zero :: forall n. () => (n ~ 0) => SNat n
+pattern Zero <- (viewNat -> IsZero)
+
+pattern Succ :: forall n. () => forall n1. (n ~ Succ n1) => SNat n1 -> SNat n
+pattern Succ n <- (viewNat -> IsSucc n)
+
+{-# COMPLETE Zero, Succ #-}
+
+succLeqZeroAbsurd :: SNat n -> IsTrue (Succ n <=? 0) -> Void
+succLeqZeroAbsurd = undefined
+
+boolToPropLeq :: (n <= m) => SNat n -> SNat m -> Leq n m
+boolToPropLeq Zero m = ZeroLeq m
+boolToPropLeq (Succ n) (Succ m) = SuccLeqSucc $ boolToPropLeq n m
+boolToPropLeq (Succ n) Zero = absurd $ succLeqZeroAbsurd n Witness
diff --git a/examples/simple-arith.hs b/examples/simple-arith.hs
deleted file mode 100644
--- a/examples/simple-arith.hs
+++ /dev/null
@@ -1,61 +0,0 @@
-{-# LANGUAGE DataKinds, TypeOperators, GADTs, TypeFamilies, ExplicitForAll, FlexibleContexts, EmptyCase #-}
-{-# OPTIONS_GHC -fplugin GHC.TypeLits.Presburger #-}
-{-# OPTIONS_GHC -ddump-tc-trace -ddump-to-file #-}
-module Main where
-import Data.Type.Equality
-import GHC.TypeLits       (Nat, type (<=), type (*), type (+), type (<=?), CmpNat)
-import Proof.Propositional (Empty(..))
-import Proof.Propositional (IsTrue(Witness))
-import Data.Singletons.Prelude
-import Data.Void
-
-type n <=! m = IsTrue (n <=? m)
-infix 4 <=!
-
-natLeqZero :: (n <= 0) => proxy n -> n :~: 0
-natLeqZero _ = Refl
-
--- (%:<=?) :: Sing n -> Sing m -> Sing (n <=? m)
--- n %:<=? m = case sCompare n m of
---   SLT -> STrue
---   SEQ -> STrue
---   SGT -> SFalse
-
--- natLeqZero :: IsTrue (n <=? 0) -> Sing n -> n :~: 0
--- natLeqZero Witness Zero = Refl
-
-
--- hoge :: ((n + 1 <=? n) ~ 'False) => ()
--- hoge = ()
-
--- fuga :: ((n + 1 <=? 0) ~ 'False) => ()
--- fuga = ()
-
--- bar :: ((2 * (n + 1)) ~ ((2 * n) + 2)) => proxy n -> ()
--- bar _ = ()
-
--- trans :: proxy n -> proxy m -> n <=! m -> (n + 1) <=! (m + 1)
--- trans _ _  Witness = Witness
-
--- eqv :: proxy n -> proxy m -> (n <=? m) :~: ((n + 1) <=? (m + 1))
--- eqv _ _ = Refl
-
--- leqSucc :: proxy n -> proxy m -> IsTrue ((n + 1) :<= m) -> CmpNat n m :~: 'LT
--- leqSucc _ _ Witness = Refl
-
-
--- predSucc :: forall proxy n. Empty (n <=! 0) => proxy n -> IsTrue (n + 1 <=? 2 * n)
--- predSucc _ = Witness
-
-main :: IO ()
-main = putStrLn "finished"
-
--- succLEqLTSucc :: Sing m -> Compare 0 (m + 1) :~: 'LT
--- succLEqLTSucc _ = Refl
-
-
--- succCompare :: Sing (n :: Nat) -> Sing m -> CmpNat n m :~: CmpNat (n + 1) (m + 1)
--- succCompare _ _ = Refl
-
-eqToRefl :: Sing (n :: Nat) -> Sing (m :: Nat) -> CmpNat n m :~: 'EQ -> n :~: m
-eqToRefl _n _m Refl = Refl
diff --git a/ghc-typelits-presburger.cabal b/ghc-typelits-presburger.cabal
--- a/ghc-typelits-presburger.cabal
+++ b/ghc-typelits-presburger.cabal
@@ -1,56 +1,118 @@
+cabal-version: 3.4
 name: ghc-typelits-presburger
-version: 0.1.1.1
-cabal-version: >=1.10
-build-type: Simple
-license: BSD3
-license-file: LICENSE
-copyright: 2015 (c) Hiromi ISHII
-maintainer: konn.jinro _at_ gmail.com
-homepage: https://github.com/konn/ghc-typelits-presburger#readme
+version: 0.7.4.2
 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.
-    You can use by adding this package to @build-depends@ and add the following pragma to the head of .hs files:
-    .
-    > OPTIONS_GHC -fplugin GHC.TypeLits.Presburger
+  @ghc-typelits-presburger@ augments GHC type-system with Presburger
+  Arithmetic Solver for Type-level natural numbers.
+  This plugin only work with GHC builtin operations.
+  To work with those of @singletons@ package, use @ghc-typelits-meta@ and/or @ghc-typelits-presburger@ instead.
+  .
+  Since 0.3.0.0, integration with <https://hackage.haskell.org/package/singletons singletons> package moves to <https://hackage.haskell.org/package/singletons-presburger singletons-presburger>.
+  .
+  You can use by adding this package to @build-depends@ and add the following pragma
+  to the head of .hs files:
+  .
+  .
+  > OPTIONS_GHC -fplugin GHC.TypeLits.Presburger
+
 category: Math, Type System
+homepage: https://github.com/konn/ghc-typelits-presburger#readme
+bug-reports: https://github.com/konn/ghc-typelits-presburger/issues
 author: Hiromi ISHII
-tested-with: GHC ==8.0.2 GHC ==8.2.2
+maintainer: konn.jinro _at_ gmail.com
+copyright: 2015-2025 (c) Hiromi ISHII
+license: BSD-3-Clause
+license-file: LICENSE
+build-type: Simple
+tested-with:
+  ghc ==9.6.7
+  ghc ==9.8.4
+  ghc ==9.10.2
+  ghc ==9.12.2
 
+extra-source-files:
+  Changelog.md
+
 source-repository head
-    type: git
-    location: https://github.com/konn/ghc-typelits-presburger
+  type: git
+  location: https://github.com/konn/ghc-typelits-presburger
 
 flag examples
-    default: False
+  description: Builds example
+  manual: False
+  default: False
 
+common defaults
+  autogen-modules: Paths_ghc_typelits_presburger
+  other-modules: Paths_ghc_typelits_presburger
+  default-language: Haskell2010
+  ghc-options:
+    -Wall
+    -Wcompat
+    -Widentities
+    -Wincomplete-record-updates
+    -Wincomplete-uni-patterns
+    -Wmissing-export-lists
+    -Wmissing-home-modules
+    -Wpartial-fields
+    -Wredundant-constraints
+    -Wunused-packages
+
 library
-    exposed-modules:
-        GHC.TypeLits.Presburger
-    build-depends:
-        base >=4.7 && <5,
-        ghc >=7.10 && <8.4,
-        ghc-tcplugins-extra ==0.2.*,
-        presburger ==1.3.*,
-        equational-reasoning >=0.4.0.0 && <0.6,
-        reflection >=2.1.2 && <2.2
-    default-language: Haskell2010
-    hs-source-dirs: src
-    other-modules:
-        GHC.Compat
-    ghc-options: -Wall
+  import: defaults
+  hs-source-dirs: src
+  exposed-modules:
+    GHC.TypeLits.Presburger
+    GHC.TypeLits.Presburger.Compat
+    GHC.TypeLits.Presburger.Types
 
-executable simple-arith
-    
-    if !flag(examples)
-        buildable: False
-    main-is: simple-arith.hs
-    build-depends:
-        base >=4.10.1.0 && <4.11,
-        ghc-typelits-presburger >=0.1.1.1 && <0.2,
-        equational-reasoning >=0.5.0.0 && <0.6,
-        singletons >=2.3.1 && <2.4
-    default-language: Haskell2010
-    hs-source-dirs: examples
-    ghc-options: -Wall
+  other-modules:
+    Data.Integer.SAT
+    GHC.TypeLits.Presburger.Flags
 
+  build-depends:
+    base >=4.7 && <5,
+    containers,
+    ghc <9.13,
+    ghc-tcplugins-extra >=0.2 && <0.6,
+    mtl,
+    pretty,
+    reflection,
+    syb,
+    transformers,
+
+executable simple-arith-core
+  import: defaults
+  main-is: simple-arith-core.hs
+  hs-source-dirs: examples
+  build-depends:
+    base,
+    equational-reasoning,
+    ghc-typelits-presburger,
+
+  if !(flag(examples))
+    buildable: False
+
+test-suite test-typeltis-presburger
+  import: defaults
+  type: exitcode-stdio-1.0
+  main-is: test.hs
+  hs-source-dirs: test
+  -- cabal-gild: discover test --exclude=test/test.hs
+  other-modules:
+    ErrorsNoPlugin
+    ErrorsWithPlugin
+    GHC.TypeLits.PresburgerSpec
+    Shared
+
+  build-tool-depends: tasty-discover:tasty-discover
+  build-depends:
+    base,
+    equational-reasoning,
+    ghc-typelits-presburger,
+    tasty,
+    tasty-discover,
+    tasty-expected-failure,
+    tasty-hunit,
+    text,
diff --git a/src/Data/Integer/SAT.hs b/src/Data/Integer/SAT.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Integer/SAT.hs
@@ -0,0 +1,1021 @@
+{-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE PatternGuards #-}
+{-# LANGUAGE Safe #-}
+
+{- |
+This module implements a decision procedure for quantifier-free linear
+arithmetic.  The algorithm is based on the following paper:
+
+  An Online Proof-Producing Decision Procedure for
+  Mixed-Integer Linear Arithmetic
+  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,
+
+  -- * Iterators
+  allSolutions,
+  slnCurrent,
+  slnNextVal,
+  slnNextVar,
+  slnEnumerate,
+
+  -- * Debug
+  dotPropSet,
+  sizePropSet,
+  allInerts,
+  ppInerts,
+
+  -- * For QuickCheck
+  iPickBounded,
+  Bound (..),
+  tConst,
+) where
+
+import Control.Applicative (Alternative (..), Applicative (..), (<$>))
+import Control.Monad (MonadPlus (..), ap, guard, liftM)
+import Data.List (partition)
+import Data.Map (Map)
+import qualified Data.Map as Map
+import Data.Maybe (fromMaybe, mapMaybe, maybeToList)
+import Text.PrettyPrint
+import Prelude hiding ((<>))
+
+infixr 2 :||
+
+infixr 3 :&&
+
+infix 4 :==, :/=, :<, :<=, :>, :>=
+
+infixl 6 :+, :-
+
+infixl 7 :*
+
+--------------------------------------------------------------------------------
+-- Solver interface
+
+-- | A collection of propositions.
+newtype PropSet = State (Answer RW)
+  deriving (Show)
+
+dotPropSet :: PropSet -> Doc
+dotPropSet (State a) = dotAnswer (ppInerts . inerts) a
+
+sizePropSet :: PropSet -> (Integer, Integer, Integer)
+sizePropSet (State a) = answerSize a
+
+-- | An empty collection of propositions.
+noProps :: PropSet
+noProps = State $ return initRW
+
+-- | Add a new proposition to an existing collection.
+assert :: Prop -> PropSet -> PropSet
+assert p (State rws) = State $ fmap snd $ m =<< rws
+  where
+    S m = prop p
+
+{- | Extract a model from a consistent set of propositions.
+ Returns 'Nothing' if the assertions have no model.
+ If a variable does not appear in the assignment, then it is 0 (?).
+-}
+checkSat :: PropSet -> Maybe [(Int, Integer)]
+checkSat (State m) = go m
+  where
+    go None = mzero
+    go (One rw) = return [(x, v) | (UserName x, v) <- iModel (inerts rw)]
+    go (Choice m1 m2) = mplus (go m1) (go m2)
+
+allInerts :: PropSet -> [Inerts]
+allInerts (State m) = map inerts (toList m)
+
+allSolutions :: PropSet -> [Solutions]
+allSolutions = map startIter . allInerts
+
+{- | Computes bounds on the expression that are compatible with the model.
+ Returns `Nothing` if the bound is not known.
+-}
+getExprBound :: BoundType -> Expr -> PropSet -> Maybe Integer
+getExprBound bt e (State s) =
+  do
+    let S m = expr e
+        check (t, s1) = iTermBound bt t (inerts s1)
+    bs <- mapM check $ toList $ s >>= m
+    case bs of
+      [] -> Nothing
+      _ -> Just (maximum bs)
+
+{- | Compute the range of possible values for an expression.
+ Returns `Nothing` if the bound is not known.
+-}
+getExprRange :: Expr -> PropSet -> Maybe [Integer]
+getExprRange e (State s) =
+  do
+    let S m = expr e
+        check (t, s1) = do
+          l <- iTermBound Lower t (inerts s1)
+          u <- iTermBound Upper t (inerts s1)
+          return (l, u)
+    bs <- mapM check $ toList $ s >>= m
+    case bs of
+      [] -> Nothing
+      _ ->
+        let (ls, us) = unzip bs
+         in Just [x | x <- [minimum ls .. maximum us]]
+
+-- | The type of proposition.
+data Prop
+  = PTrue
+  | PFalse
+  | Prop :|| Prop
+  | Prop :&& Prop
+  | Not Prop
+  | Expr :== Expr
+  | Expr :/= Expr
+  | Expr :< Expr
+  | Expr :> Expr
+  | Expr :<= Expr
+  | Expr :>= Expr
+  deriving (Read, Show, Ord, Eq)
+
+{- | The type of integer expressions.
+ Variable names must be non-negative.
+-}
+data Expr
+  = -- | Addition
+    Expr :+ Expr
+  | -- | Subtraction
+    Expr :- Expr
+  | -- | Multiplication by a constant
+    Integer :* Expr
+  | -- | Negation
+    Negate Expr
+  | -- | Variable
+    Var Name
+  | -- | Constant
+    K Integer
+  | -- | A conditional expression
+    If Prop Expr Expr
+  | -- | Division, rounds down
+    Div Expr Integer
+  | -- | Non-negative remainder
+    Mod Expr Integer
+  | -- | Minimum of two arguments
+    Min Expr Expr
+  | -- | Maximum of two arguments
+    Max Expr Expr
+  deriving (Read, Show, Ord, Eq)
+
+prop :: Prop -> S ()
+prop PTrue = return ()
+prop PFalse = mzero
+prop (p1 :|| p2) = prop p1 `mplus` prop p2
+prop (p1 :&& p2) = prop p1 >> prop p2
+prop (Not p) = prop (neg p)
+  where
+    neg PTrue = PFalse
+    neg PFalse = PTrue
+    neg (p1 :&& p2) = neg p1 :|| neg p2
+    neg (p1 :|| p2) = neg p1 :&& neg p2
+    neg (Not q) = q
+    neg (e1 :== e2) = e1 :/= e2
+    neg (e1 :/= e2) = e1 :== e2
+    neg (e1 :< e2) = e1 :>= e2
+    neg (e1 :<= e2) = e1 :> e2
+    neg (e1 :> e2) = e1 :<= e2
+    neg (e1 :>= e2) = e1 :< e2
+prop (e1 :== e2) = do
+  t1 <- expr e1
+  t2 <- expr e2
+  solveIs0 (t1 |-| t2)
+prop (e1 :/= e2) = do
+  t1 <- expr e1
+  t2 <- expr e2
+  let t = t1 |-| t2
+  solveIsNeg t `orElse` solveIsNeg (tNeg t)
+prop (e1 :< e2) = do
+  t1 <- expr e1
+  t2 <- expr e2
+  solveIsNeg (t1 |-| t2)
+prop (e1 :<= e2) = do
+  t1 <- expr e1
+  t2 <- expr e2
+  let t = t1 |-| t2 |-| tConst 1
+  solveIsNeg t
+prop (e1 :> e2) = prop (e2 :< e1)
+prop (e1 :>= e2) = prop (e2 :<= e1)
+
+expr :: Expr -> S Term
+expr (e1 :+ e2) = (|+|) <$> expr e1 <*> expr e2
+expr (e1 :- e2) = (|-|) <$> expr e1 <*> expr e2
+expr (k :* e2) = (k |*|) <$> expr e2
+expr (Negate e) = tNeg <$> expr e
+expr (Var x) = pure (tVar x)
+expr (K x) = pure (tConst x)
+expr (Min a b) = expr (If (a :<= b) a b)
+expr (Max a b) = expr (If (a :<= b) b a)
+expr (If p e1 e2) = do
+  x <- newVar
+  prop (p :&& Var x :== e1 :|| Not p :&& Var x :== e2)
+  return (tVar x)
+expr (Div e k) = fmap fst $ exprDivMod e k
+expr (Mod e k) = fmap snd $ exprDivMod e k
+
+exprDivMod :: Expr -> Integer -> S (Term, Term)
+exprDivMod e k =
+  do
+    guard (k /= 0) -- Always unsat
+    q <- newVar
+    r <- newVar
+    let er = Var r
+    prop (k :* Var q :+ er :== e :&& er :< K k :&& K 0 :<= er)
+    return (tVar q, tVar r)
+
+--------------------------------------------------------------------------------
+
+data RW = RW
+  { nameSource :: !Int
+  , inerts :: Inerts
+  }
+  deriving (Show)
+
+initRW :: RW
+initRW = RW {nameSource = 0, inerts = iNone}
+
+--------------------------------------------------------------------------------
+-- Constraints and Bound on Variables
+
+ctLt :: Term -> Term -> Term
+ctLt t1 t2 = t1 |-| t2
+
+ctEq :: Term -> Term -> Term
+ctEq t1 t2 = t1 |-| t2
+
+data Bound
+  = -- | The integer is strictly positive
+    Bound Integer Term
+  deriving (Show)
+
+data BoundType = Lower | Upper
+  deriving (Show)
+
+toCt :: BoundType -> Name -> Bound -> Term
+toCt Lower x (Bound c t) = ctLt t (c |*| tVar x)
+toCt Upper x (Bound c t) = ctLt (c |*| tVar x) t
+
+--------------------------------------------------------------------------------
+-- Inert set
+
+-- | The inert contains the solver state on one possible path.
+data Inerts = Inerts
+  { 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)
+
+ppInerts :: Inerts -> Doc
+ppInerts is =
+  vcat $
+    [ppLower x b | (x, (ls, _)) <- bnds, b <- ls]
+      ++ [ppUpper x b | (x, (_, us)) <- bnds, b <- us]
+      ++ [ppEq e | e <- Map.toList (solved is)]
+  where
+    bnds = Map.toList (bounds is)
+
+    ppT c x = ppTerm (c |*| tVar x)
+    ppLower x (Bound c t) = ppTerm t <+> text "<" <+> ppT c x
+    ppUpper x (Bound c t) = ppT c x <+> text "<" <+> ppTerm t
+    ppEq (x, t) = ppName x <+> text "=" <+> ppTerm t
+
+-- | An empty inert set.
+iNone :: Inerts
+iNone =
+  Inerts
+    { bounds = Map.empty
+    , solved = Map.empty
+    }
+
+-- | Rewrite a term using the definitions from an inert set.
+iApSubst :: Inerts -> Term -> Term
+iApSubst i t = foldr apS t $ Map.toList $ solved i
+  where
+    apS (x, t1) t2 = tLet x t1 t2
+
+{- | Add a definition.  Upper and lower bound constraints that mention
+ the variable are "kicked-out" so that they can be reinserted in the
+ context of the new knowledge.
+
+    * Assumes substitution has already been applied.
+
+    * The kicked-out constraints are NOT rewritten, this happens
+      when they get inserted in the work queue.
+-}
+iSolved :: Name -> Term -> Inerts -> ([Term], Inerts)
+iSolved x t i =
+  ( kickedOut
+  , Inerts
+      { bounds = otherBounds
+      , solved = Map.insert x t $ Map.map (tLet x t) $ solved i
+      }
+  )
+  where
+    (kickedOut, otherBounds) =
+      -- First, we eliminate all entries for `x`
+      let (mb, mp1) = Map.updateLookupWithKey (\_ _ -> Nothing) x (bounds i)
+
+          -- Next, we elminate all constraints that mentiond `x` in bounds
+          mp2 = Map.mapWithKey extractBounds mp1
+       in ( [ ct | (lbs, ubs) <- maybeToList mb, ct <- map (toCt Lower x) lbs ++ map (toCt Upper x) ubs
+            ]
+              ++ [ct | (_, cts) <- Map.elems mp2, ct <- cts]
+          , fmap fst mp2
+          )
+
+    extractBounds y (lbs, ubs) =
+      let (lbsStay, lbsKick) = partition stay lbs
+          (ubsStay, ubsKick) = partition stay ubs
+       in ( (lbsStay, ubsStay)
+          , map (toCt Lower y) lbsKick
+              ++ map (toCt Upper y) ubsKick
+          )
+
+    stay (Bound _ bnd) = not (tHasVar x bnd)
+
+{- | Given some lower and upper bounds, find the interval the satisfies them.
+ Note the upper and lower bounds are strict (i.e., < and >)
+-}
+boundInterval :: [Bound] -> [Bound] -> Maybe (Maybe Integer, Maybe Integer)
+boundInterval lbs ubs =
+  do
+    ls <- mapM (normBound Lower) lbs
+    us <- mapM (normBound Upper) ubs
+    let lb = case ls of
+          [] -> Nothing
+          _ -> Just (maximum ls + 1)
+        ub = case us of
+          [] -> Nothing
+          _ -> Just (minimum us - 1)
+    case (lb, ub) of
+      (Just l, Just u) -> guard (l <= u)
+      _ -> return ()
+    return (lb, ub)
+  where
+    normBound Lower (Bound c t) = do
+      k <- isConst t
+      return (div (k + c - 1) c)
+    normBound Upper (Bound c t) = do
+      k <- isConst t
+      return (div k c)
+
+data Solutions
+  = Done
+  | TopVar Name Integer (Maybe Integer) (Maybe Integer) Inerts
+  | FixedVar Name Integer Solutions
+  deriving (Show)
+
+slnCurrent :: Solutions -> [(Int, Integer)]
+slnCurrent s = [(x, v) | (UserName x, v) <- go s]
+  where
+    go Done = []
+    go (TopVar x v _ _ is) = (x, v) : iModel (iLet x v is)
+    go (FixedVar x v i) = (x, v) : go i
+
+{- | Replace occurances of a variable with an integer.
+ WARNING: The integer should be a valid value for the variable.
+-}
+iLet :: Name -> Integer -> Inerts -> Inerts
+iLet x v is =
+  Inerts
+    { bounds = fmap updBs (bounds is)
+    , solved = fmap (tLetNum x v) (solved is)
+    }
+  where
+    updB (Bound c t) = Bound c (tLetNum x v t)
+    updBs (ls, us) = (map updB ls, map updB us)
+
+startIter :: Inerts -> Solutions
+startIter is =
+  case Map.maxViewWithKey (bounds is) of
+    Nothing ->
+      case Map.maxViewWithKey (solved is) of
+        Nothing -> Done
+        Just ((x, t), mp1) ->
+          case [y | y <- tVarList t] of
+            y : _ -> TopVar y 0 Nothing Nothing is
+            [] ->
+              let v = tConstPart t
+               in TopVar x v (Just v) (Just v) $ is {solved = mp1}
+    Just ((x, (lbs, ubs)), mp1) ->
+      case [y | Bound _ t <- lbs ++ ubs, y <- tVarList t] of
+        y : _ -> TopVar y 0 Nothing Nothing is
+        [] -> case boundInterval lbs ubs of
+          Nothing -> error "bug: cannot compute interval?"
+          Just (lb, ub) ->
+            let v = fromMaybe 0 (mplus lb ub)
+             in TopVar x v lb ub $ is {bounds = mp1}
+
+slnEnumerate :: Solutions -> [Solutions]
+slnEnumerate s0 = go s0 []
+  where
+    go s k = case slnNextVar s of
+      Nothing -> hor s k
+      Just s1 -> go s1 $ case slnNextVal s of
+        Nothing -> k
+        Just s2 -> go s2 k
+
+    hor s k =
+      s
+        : case slnNextVal s of
+          Nothing -> k
+          Just s1 -> hor s1 k
+
+slnNextVal :: Solutions -> Maybe Solutions
+slnNextVal Done = Nothing
+slnNextVal (FixedVar x v i) = FixedVar x v `fmap` slnNextVal i
+slnNextVal it@(TopVar _ _ lb _ _) =
+  case lb of
+    Just _ -> slnNextValWith (+ 1) it
+    Nothing -> slnNextValWith (subtract 1) it
+
+slnNextValWith :: (Integer -> Integer) -> Solutions -> Maybe Solutions
+slnNextValWith _ Done = Nothing
+slnNextValWith f (FixedVar x v i) = FixedVar x v `fmap` slnNextValWith f i
+slnNextValWith f (TopVar x v lb ub is) =
+  do
+    let v1 = f v
+    case lb of
+      Just l -> guard (l <= v1)
+      Nothing -> return ()
+    case ub of
+      Just u -> guard (v1 <= u)
+      Nothing -> return ()
+    return $ TopVar x v1 lb ub is
+
+slnNextVar :: Solutions -> Maybe Solutions
+slnNextVar Done = Nothing
+slnNextVar (TopVar x v _ _ is) = Just $ FixedVar x v $ startIter $ iLet x v is
+slnNextVar (FixedVar x v i) = FixedVar x v `fmap` slnNextVar i
+
+-- Given a list of lower (resp. upper) bounds, compute the least (resp. largest)
+-- value that satisfies them all.
+iPickBounded :: BoundType -> [Bound] -> Maybe Integer
+iPickBounded _ [] = Nothing
+iPickBounded bt bs =
+  do
+    xs <- mapM (normBound bt) bs
+    return $ case bt of
+      Lower -> maximum xs
+      Upper -> minimum xs
+  where
+    -- t < c*x
+    -- <=> t+1 <= c*x
+    -- <=> (t+1)/c <= x
+    -- <=> ceil((t+1)/c) <= x
+    -- <=> t `div` c + 1 <= x
+    normBound Lower (Bound c t) = do
+      k <- isConst t
+      return (k `div` c + 1)
+    -- c*x < t
+    -- <=> c*x <= t-1
+    -- <=> x   <= (t-1)/c
+    -- <=> x   <= floor((t-1)/c)
+    -- <=> x   <= (t-1) `div` c
+    normBound Upper (Bound c t) = do
+      k <- isConst t
+      return (div (k - 1) c)
+
+{- | The largest (resp. least) upper (resp. lower) bound on a term
+ that will satisfy the model
+-}
+iTermBound :: BoundType -> Term -> Inerts -> Maybe Integer
+iTermBound bt (T k xs) is = do
+  ks <- mapM summand (Map.toList xs)
+  return $ sum $ k : ks
+  where
+    summand (x, c) = fmap (c *) (iVarBound (newBt c) x is)
+    newBt c =
+      if c > 0
+        then bt
+        else case bt of
+          Lower -> Upper
+          Upper -> Lower
+
+{- | The largest (resp. least) upper (resp. lower) bound on a variable
+ that will satisfy the model.
+-}
+iVarBound :: BoundType -> Name -> Inerts -> Maybe Integer
+iVarBound bt x is
+  | Just t <- Map.lookup x (solved is) = iTermBound bt t is
+iVarBound bt x is =
+  do
+    both <- Map.lookup x (bounds is)
+    case mapMaybe fromBound (chooseBounds both) of
+      [] -> Nothing
+      bs -> return (combineBounds bs)
+  where
+    fromBound (Bound c t) = fmap (scaleBound c) (iTermBound bt t is)
+
+    combineBounds = case bt of
+      Upper -> minimum
+      Lower -> maximum
+
+    chooseBounds = case bt of
+      Upper -> snd
+      Lower -> fst
+
+    scaleBound c b = case bt of
+      Upper -> div (b - 1) c
+      Lower -> div b c + 1
+
+iModel :: Inerts -> [(Name, Integer)]
+iModel i = goBounds [] (bounds i)
+  where
+    goBounds su mp =
+      case Map.maxViewWithKey mp of
+        Nothing -> goEqs su $ Map.toList $ solved i
+        Just ((x, (lbs0, ubs0)), mp1) ->
+          let lbs = [Bound c (tLetNums su t) | Bound c t <- lbs0]
+              ubs = [Bound c (tLetNums su t) | Bound c t <- ubs0]
+              sln =
+                fromMaybe 0 $
+                  mplus (iPickBounded Lower lbs) (iPickBounded Upper ubs)
+           in goBounds ((x, sln) : su) mp1
+
+    goEqs su [] = su
+    goEqs su ((x, t) : more) =
+      let t1 = tLetNums su t
+          vs = tVarList t1
+          su1 = [(v, 0) | v <- vs] ++ (x, tConstPart t1) : su
+       in goEqs su1 more
+
+--------------------------------------------------------------------------------
+-- Solving constraints
+
+solveIs0 :: Term -> S ()
+solveIs0 t = solveIs0' =<< apSubst t
+
+{- | Solve a constraint if the form @t = 0@.
+ Assumes substitution has already been applied.
+-}
+solveIs0' :: Term -> S ()
+solveIs0' t
+  -- A == 0
+  | 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
+  --  x + S = 0
+  -- -x + S = 0
+  | Just (xc, x, s) <- tGetSimpleCoeff t =
+      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
+
+        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
+modulus a m = a - m * div (2 * a + m) (2 * m)
+
+solveIsNeg :: Term -> S ()
+solveIsNeg t = solveIsNeg' =<< apSubst t
+
+{- | Solve a constraint of the form @t < 0@.
+ Assumes that substitution has been applied
+-}
+solveIsNeg' :: Term -> S ()
+solveIsNeg' t
+  -- A < 0
+  | Just a <- isConst t = guard (a < 0)
+  -- A * S < 0
+  | 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
+                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 ()
+orElse x y = mplus x y
+
+{- Note [Shadows]
+
+  P: beta < b * x
+  Q: a * x < alpha
+
+real: a * beta < b * alpha
+
+  beta     < b * x      -- from P
+  a * beta < a * b * x  -- (a *)
+  a * beta < b * alpha  -- comm. and Q
+
+dark: b * alpha - a * beta > a * b
+
+gray: b * x = beta + 1 \/
+      b * x = beta + 2 \/
+      ...
+      b * x = beta + (b-1)
+
+We stop at @b - 1@ because if:
+
+> b * x                >= beta + b
+> a * b * x            >= a * (beta + b)     -- (a *)
+> a * b * x            >= a * beta + a * b   -- distrib.
+> b * alpha            >  a * beta + a * b   -- comm. and Q
+> b * alpha - a * beta > a * b               -- subtract (a * beta)
+
+which is covered by the dark shadow.
+-}
+
+--------------------------------------------------------------------------------
+-- Monads
+
+data Answer a = None | One a | Choice (Answer a) (Answer a)
+  deriving (Show)
+
+answerSize :: Answer a -> (Integer, Integer, Integer)
+answerSize = go 0 0 0
+  where
+    go !n !o !c ans =
+      case ans of
+        None -> (n + 1, o, c)
+        One _ -> (n, o + 1, c)
+        Choice x y ->
+          case go n o (c + 1) x of
+            (n', o', c') -> go n' o' c' y
+
+dotAnswer :: (a -> Doc) -> Answer a -> Doc
+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))
+        <> semi
+    edge x y = integer x <+> text "->" <+> integer y
+
+    go x None =
+      let x' = x + 1
+       in seq x' (node x "", x')
+    go x (One a) =
+      let x' = x + 1
+       in seq x' (node x (show (pp a)), x')
+    go x (Choice c1 c2) =
+      let x' = x + 1
+          (ls1, x1) = go x' c1
+          (ls2, x2) = go x1 c2
+       in seq
+            x'
+            ( vcat
+                [ node x "|"
+                , edge x x'
+                , edge x x1
+                , ls1
+                , ls2
+                ]
+            , x2
+            )
+
+toList :: Answer a -> [a]
+toList a = go a []
+  where
+    go (Choice xs ys) zs = go xs (go ys zs)
+    go (One x) xs = x : xs
+    go None xs = xs
+
+instance Monad Answer where
+  None >>= _ = None
+  One a >>= k = k a
+  Choice m1 m2 >>= k = mplus (m1 >>= k) (m2 >>= k)
+
+instance Alternative Answer where
+  empty = mzero
+  (<|>) = mplus
+
+instance MonadPlus Answer where
+  mzero = None
+  mplus None x = x
+  -- mplus (Choice x y) z = mplus x (mplus y z)
+  mplus x y = Choice x y
+
+instance Functor Answer where
+  fmap _ None = None
+  fmap f (One x) = One (f x)
+  fmap f (Choice x1 x2) = Choice (fmap f x1) (fmap f x2)
+
+instance Applicative Answer where
+  pure = One
+  (<*>) = ap
+
+newtype S a = S (RW -> Answer (a, RW))
+
+instance Monad S where
+  S m >>= k = S $ \s -> do
+    (a, s1) <- m s
+    let S m1 = k a
+    m1 s1
+
+instance Alternative S where
+  empty = mzero
+  (<|>) = mplus
+
+instance MonadPlus S where
+  mzero = S $ \_ -> mzero
+  mplus (S m1) (S m2) = S $ \s -> mplus (m1 s) (m2 s)
+
+instance Functor S where
+  fmap = liftM
+
+instance Applicative S where
+  pure a = S $ \s -> pure (a, s)
+  (<*>) = ap
+
+updS :: (RW -> (a, RW)) -> S a
+updS f = S $ \s -> return (f s)
+
+updS_ :: (RW -> RW) -> S ()
+updS_ f = updS $ \rw -> ((), f rw)
+
+get :: (RW -> a) -> S a
+get f = updS $ \rw -> (f rw, rw)
+
+newVar :: S Name
+newVar = updS $ \rw ->
+  ( SysName (nameSource rw)
+  , rw {nameSource = nameSource rw + 1}
+  )
+
+-- | Get lower ('fst'), or upper ('snd') bounds for a variable.
+getBounds :: BoundType -> Name -> S [Bound]
+getBounds f x = get $ \rw -> case Map.lookup x $ bounds $ inerts rw of
+  Nothing -> []
+  Just bs -> case f of
+    Lower -> fst bs
+    Upper -> snd bs
+
+addBound :: BoundType -> Name -> Bound -> S ()
+addBound bt x b = updS_ $ \rw ->
+  let i = inerts rw
+      entry = case bt of
+        Lower -> ([b], [])
+        Upper -> ([], [b])
+      jn (newL, newU) (oldL, oldU) = (newL ++ oldL, newU ++ oldU)
+   in rw {inerts = i {bounds = Map.insertWith jn x entry (bounds i)}}
+
+{- | Add a new definition.
+ Assumes substitution has already been applied
+-}
+addDef :: Name -> Term -> S ()
+addDef x t =
+  do
+    newWork <- updS $ \rw ->
+      let (newWork, newInerts) = iSolved x t (inerts rw)
+       in (newWork, rw {inerts = newInerts})
+    mapM_ solveIsNeg newWork
+
+apSubst :: Term -> S Term
+apSubst t =
+  do
+    i <- get inerts
+    return (iApSubst i t)
+
+--------------------------------------------------------------------------------
+
+data Name = UserName !Int | SysName !Int
+  deriving (Read, Show, Eq, Ord)
+
+ppName :: Name -> Doc
+ppName (UserName x) = text "u" <> int x
+ppName (SysName x) = text "s" <> int x
+
+toName :: Int -> Name
+toName = UserName
+
+fromName :: Name -> Maybe Int
+fromName (UserName x) = Just x
+fromName (SysName _) = Nothing
+
+type NameMap = Map Name
+
+{- | The type of terms.  The integer is the constant part of the term,
+ and the `Map` maps variables (represented by @Int@ to their coefficients).
+ The term is a sum of its parts.
+ INVARIANT: the `Map` does not map anything to 0.
+-}
+data Term = T !Integer (NameMap Integer)
+  deriving (Eq, Ord)
+
+infixl 6 |+|, |-|
+
+infixr 7 |*|
+
+-- | A constant term.
+tConst :: Integer -> Term
+tConst k = T k Map.empty
+
+-- | Construct a term with a single variable.
+tVar :: Name -> Term
+tVar x = T 0 (Map.singleton x 1)
+
+(|+|) :: Term -> Term -> Term
+T n1 m1 |+| T n2 m2 =
+  T (n1 + n2) $
+    if Map.null m1
+      then m2
+      else
+        if Map.null m2
+          then m1
+          else Map.filter (/= 0) $ Map.unionWith (+) m1 m2
+
+(|*|) :: Integer -> Term -> Term
+0 |*| _ = tConst 0
+1 |*| t = t
+k |*| T n m = T (k * n) (fmap (k *) m)
+
+tNeg :: Term -> Term
+tNeg t = (-1) |*| t
+
+(|-|) :: Term -> Term -> Term
+t1 |-| t2 = t1 |+| tNeg t2
+
+-- | Replace a variable with a term.
+tLet :: Name -> Term -> Term -> Term
+tLet x t1 t2 =
+  let (a, t) = tSplitVar x t2
+   in a |*| t1 |+| t
+
+-- | Replace a variable with a constant.
+tLetNum :: Name -> Integer -> Term -> Term
+tLetNum x k t =
+  let (c, T n m) = tSplitVar x t
+   in T (c * k + n) m
+
+-- | Replace the given variables with constants.
+tLetNums :: [(Name, Integer)] -> Term -> Term
+tLetNums xs t = foldr (\(x, i) t1 -> tLetNum x i t1) t xs
+
+instance Show Term where
+  showsPrec c t = showsPrec c (show (ppTerm t))
+
+ppTerm :: Term -> Doc
+ppTerm (T k m) =
+  case Map.toList m of
+    [] -> integer k
+    xs | k /= 0 -> hsep (integer k : map ppProd xs)
+    x : xs -> hsep (ppFst x : map ppProd xs)
+  where
+    ppFst (x, 1) = ppName x
+    ppFst (x, -1) = text "-" <> ppName x
+    ppFst (x, n) = ppMul n x
+
+    ppProd (x, 1) = text "+" <+> ppName x
+    ppProd (x, -1) = text "-" <+> ppName x
+    ppProd (x, n)
+      | n > 0 = text "+" <+> ppMul n x
+      | otherwise = text "-" <+> ppMul (abs n) x
+
+    ppMul n x = integer n <+> text "*" <+> ppName x
+
+{- | Remove a variable from the term, and return its coefficient.
+ If the variable is not present in the term, the coefficient is 0.
+-}
+tSplitVar :: Name -> Term -> (Integer, Term)
+tSplitVar x t@(T n m) =
+  case Map.updateLookupWithKey (\_ _ -> Nothing) x m of
+    (Nothing, _) -> (0, t)
+    (Just k, m1) -> (k, T n m1)
+
+-- | Does the term contain this varibale?
+tHasVar :: Name -> Term -> Bool
+tHasVar x (T _ m) = Map.member x m
+
+-- | Is this terms just an integer.
+isConst :: Term -> Maybe Integer
+isConst (T n m)
+  | Map.null m = Just n
+  | otherwise = Nothing
+
+tConstPart :: Term -> Integer
+tConstPart (T n _) = n
+
+-- | Returns: @Just (a, b, x)@ if the term is the form: @a + b * x@
+tIsOneVar :: Term -> Maybe (Integer, Integer, Name)
+tIsOneVar (T a m) = case Map.toList m of
+  [(x, b)] -> Just (a, b, x)
+  _ -> Nothing
+
+{- | Spots terms that contain variables with unit coefficients
+ (i.e., of the form @x + t@ or @t - x@).
+ Returns (coeff, var, rest of term)
+-}
+tGetSimpleCoeff :: Term -> Maybe (Integer, Name, Term)
+tGetSimpleCoeff (T a m) =
+  do
+    let (m1, m2) = Map.partition (\x -> x == 1 || x == -1) m
+    ((x, xc), m3) <- Map.minViewWithKey m1
+    return (xc, x, T a (Map.union m3 m2))
+
+tVarList :: Term -> [Name]
+tVarList (T _ m) = Map.keys m
+
+{- | Try to factor-out a common consant (> 1) from a term.
+ For example, @2 + 4x@ becomes @2 * (1 + 2x)@.
+-}
+tFactor :: Term -> Maybe (Integer, Term)
+tFactor (T c m) =
+  do
+    d <- common (c : Map.elems m)
+    return (d, T (div c d) (fmap (`div` d) m))
+  where
+    common :: [Integer] -> Maybe Integer
+    common [] = Nothing
+    common [x] = Just x
+    common (x : y : zs) =
+      case gcd x y of
+        1 -> Nothing
+        n -> common (n : zs)
+
+-- | Extract a variable with a coefficient whose absolute value is minimal.
+tLeastAbsCoeff :: Term -> Maybe (Integer, Name, Term)
+tLeastAbsCoeff (T c m) = do
+  (xc, x, m1) <- Map.foldrWithKey step Nothing m
+  return (xc, x, T c m1)
+  where
+    step x xc Nothing = Just (xc, x, Map.delete x m)
+    step x xc (Just (yc, _, _))
+      | abs xc < abs yc = Just (xc, x, Map.delete x m)
+    step _ _ it = it
+
+-- | Extract the least variable from a term
+tLeastVar :: Term -> Maybe (Integer, Name, Term)
+tLeastVar (T c m) =
+  do
+    ((x, xc), m1) <- Map.minViewWithKey m
+    return (xc, x, T c m1)
+
+-- | Apply a function to all coefficients, including the constnat
+tMapCoeff :: (Integer -> Integer) -> Term -> Term
+tMapCoeff f (T c m) = T (f c) (fmap f m)
diff --git a/src/GHC/Compat.hs b/src/GHC/Compat.hs
deleted file mode 100644
--- a/src/GHC/Compat.hs
+++ /dev/null
@@ -1,104 +0,0 @@
-{-# LANGUAGE CPP, PatternGuards, PatternSynonyms, ViewPatterns #-}
-module GHC.Compat (module GHC.Compat) where
-import FastString          as GHC.Compat (fsLit)
-import GHC.TcPluginM.Extra as GHC.Compat (evByFiat, lookupModule, lookupName,
-                                          tracePlugin)
-import GhcPlugins          as GHC.Compat (EqRel (..), PredTree (..))
-import GhcPlugins          as GHC.Compat (classifyPredType, isEqPred,
-                                          lookupTyCon, mkTyConTy)
-import GhcPlugins          as GHC.Compat (mkTcOcc, ppr, promotedFalseDataCon)
-import GhcPlugins          as GHC.Compat (promotedTrueDataCon, text)
-import GhcPlugins          as GHC.Compat (tyConAppTyCon_maybe, typeKind)
-import GhcPlugins          as GHC.Compat (TyCon, typeNatKind)
-import Module              as GHC.Compat (ModuleName, mkModuleName)
-import Plugins             as GHC.Compat (Plugin (..), defaultPlugin)
-import TcEvidence          as GHC.Compat (EvTerm)
-import TcPluginM           as GHC.Compat (TcPluginM, tcLookupTyCon,
-                                          tcPluginTrace)
-import TcRnMonad           as GHC.Compat (Ct, TcPluginResult (..), isWanted)
-import TcRnTypes           as GHC.Compat (TcPlugin (..), ctEvPred, ctEvidence)
-import TcTypeNats          as GHC.Compat
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 800
-import           GhcPlugins (InScopeSet, Outputable, emptyUFM)
-import qualified PrelNames  as Old
-import           TyCoRep    as GHC.Compat (TyLit (NumTyLit), Type (..))
-import           Type       as GHC.Compat (TCvSubst (..), TvSubstEnv,
-                                           emptyTCvSubst)
-import           Type       as GHC.Compat (eqType, unionTCvSubst)
-import qualified Type       as Old
-import qualified TysPrim    as Old
-import           TysWiredIn as GHC.Compat (boolTyCon)
-import           Unify      as Old (tcUnifyTy)
-#else
-import Type       as GHC.Compat (TvSubst, emptyTvSubst)
-import Type       as GHC.Compat (substTy, unionTvSubst)
-import TypeRep    as GHC.Compat (TyLit (NumTyLit), Type (..))
-import TysWiredIn as Old (eqTyCon)
-import TysWiredIn as GHC.Compat (promotedBoolTyCon)
-import Unify      as GHC.Compat (tcUnifyTy)
-#endif
-import TcPluginM (lookupOrig)
-import Type      as GHC.Compat (splitTyConApp_maybe)
-import Unique    as GHC.Compat (getKey, getUnique)
-
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 800
-data TvSubst = TvSubst InScopeSet TvSubstEnv
-
-instance Outputable  TvSubst where
-  ppr = ppr . toTCv
-
-emptyTvSubst :: TvSubst
-emptyTvSubst = case emptyTCvSubst of
-  TCvSubst set tvsenv _ -> TvSubst set tvsenv
-
-toTCv :: TvSubst -> TCvSubst
-toTCv (TvSubst set tvenv) = TCvSubst set tvenv emptyUFM
-
-substTy :: TvSubst -> Type -> Type
-substTy tvs = Old.substTy (toTCv tvs)
-
-unionTvSubst :: TvSubst -> TvSubst -> TvSubst
-unionTvSubst s1 s2 =
-  fromTCv $ unionTCvSubst (toTCv s1) (toTCv s2)
-fromTCv :: TCvSubst -> TvSubst
-fromTCv (TCvSubst set tvsenv _) = TvSubst set tvsenv
-
-promotedBoolTyCon :: TyCon
-promotedBoolTyCon = boolTyCon
-
-viewFunTy :: Type -> Maybe (Type, Type)
-viewFunTy t@(TyConApp _ [t1, t2])
-  | 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 = tcLookupTyCon Old.eqTyConName
-
-#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]
-decompFunTy (FunTy t1 t2) = t1 : decompFunTy t2
-decompFunTy t             = [t]
diff --git a/src/GHC/TypeLits/Presburger.hs b/src/GHC/TypeLits/Presburger.hs
--- a/src/GHC/TypeLits/Presburger.hs
+++ b/src/GHC/TypeLits/Presburger.hs
@@ -1,270 +1,12 @@
-{-# LANGUAGE FlexibleContexts, MultiWayIf, OverloadedStrings, PatternGuards #-}
-{-# LANGUAGE RankNTypes, TupleSections                                      #-}
-module GHC.TypeLits.Presburger (plugin) where
-import GHC.Compat
-
-import           Class            (classTyCon)
-import           Data.Foldable    (asum)
-import           Data.Integer.SAT (Expr (..), Prop (..), Prop, PropSet)
-import           Data.Integer.SAT (assert, checkSat, noProps, toName)
-import qualified Data.Integer.SAT as SAT
-import           Data.List        (nub)
-import           Data.Maybe       (catMaybes, fromMaybe, isNothing, mapMaybe)
-import           Data.Reflection  (Given)
-import           Data.Reflection  (given)
-import           Data.Reflection  (give)
-import           TcPluginM        (tcLookupClass)
-import           TcPluginM        (lookupOrig)
-import           TysWiredIn       (promotedEQDataCon, promotedGTDataCon,
-                                   promotedLTDataCon)
-
-assert' :: Prop -> PropSet -> PropSet
-assert' p ps = foldr assert ps (p : varPos)
-  where
-    varPos = [K 0 :<= Var i | i <- varsProp p ]
-
-data Proof = Proved | Disproved [(Int, Integer)]
-           deriving (Read, Show, Eq, Ord)
-
-isProved :: Proof -> Bool
-isProved Proved = True
-isProved _      = False
+{- | Provides a plain Presburger solver plugin for @'GHC.TypeNats.Nat'@.
 
-varsProp :: Prop -> [SAT.Name]
-varsProp (p :|| q) = nub $ varsProp p ++ varsProp q
-varsProp (p :&& q) = nub $ varsProp p ++ varsProp q
-varsProp (Not p)   = varsProp p
-varsProp (e :== v) = nub $ varsExpr e ++ varsExpr v
-varsProp (e :/= v) = nub $ varsExpr e ++ varsExpr v
-varsProp (e :< v)  = nub $ varsExpr e ++ varsExpr v
-varsProp (e :> v)  = nub $ varsExpr e ++ varsExpr v
-varsProp (e :<= v) = nub $ varsExpr e ++ varsExpr v
-varsProp (e :>= v) = nub $ varsExpr e ++ varsExpr v
-varsProp _         = []
+   For an interface for extension, see
+   "GHC.TypeLits.Presburger.Types".
+-}
+module GHC.TypeLits.Presburger (plugin) where
 
-varsExpr :: Expr -> [SAT.Name]
-varsExpr (e :+ v)   = nub $ varsExpr e ++ varsExpr v
-varsExpr (e :- v)   = nub $ varsExpr e ++ varsExpr v
-varsExpr (_ :* v)   = varsExpr v
-varsExpr (Negate e) = varsExpr e
-varsExpr (Var i)    = [i]
-varsExpr (K _)      = []
-varsExpr (If p e v) = nub $ varsProp p ++ varsExpr e ++ varsExpr v
-varsExpr (Div e _)  = varsExpr e
-varsExpr (Mod e _)  = varsExpr e
+import GHC.TypeLits.Presburger.Compat
+import GHC.TypeLits.Presburger.Types
 
 plugin :: Plugin
-plugin = defaultPlugin { tcPlugin = const $ Just presburgerPlugin }
-
-presburgerPlugin :: TcPlugin
-presburgerPlugin =
-  tracePlugin "typelits-presburger" $
-  TcPlugin { tcPluginInit  = return () -- tcPluginIO $ newIORef emptyTvSubst
-           , tcPluginSolve = decidePresburger
-           , tcPluginStop  = const $ return ()
-           }
-
-testIf :: PropSet -> Prop -> Proof
-testIf ps q = maybe Proved Disproved $ checkSat (Not q `assert'` ps)
-
-type PresState = ()
-
-data MyEnv  = MyEnv { emptyClsTyCon :: TyCon
-                    , eqTyCon_      :: TyCon
-                    , eqWitCon_     :: TyCon
-                    , isTrueCon_    :: TyCon
-                    , voidTyCon     :: TyCon
-                    }
-
-eqTyCon :: Given MyEnv => TyCon
-eqTyCon = eqTyCon_ given
-
-eqWitnessTyCon :: Given MyEnv => TyCon
-eqWitnessTyCon = eqWitCon_ given
-
-isTrueTyCon :: Given MyEnv => TyCon
-isTrueTyCon = isTrueCon_ given
-
-decidePresburger :: PresState -> [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginResult
-decidePresburger _ref gs [] [] = do
-  tcPluginTrace "Started givens with: " (ppr $ map (ctEvPred . ctEvidence) gs)
-  withTyCons $ do
-    let subst = emptyTvSubst
-                -- foldr unionTvSubst emptyTvSubst $ map genSubst gs
-        givens = mapMaybe (\a -> (,) a <$> toPresburgerPred subst (deconsPred a)) gs
-        prems0 = map snd givens
-        prems  = foldr assert' noProps prems0
-        (solved, _) = foldr go ([], noProps) givens
-    if isNothing (checkSat prems)
-      then return $ TcPluginContradiction gs
-      else return $ TcPluginOk (map withEv solved) []
-    where
-      go (ct, p) (ss, prem)
-        | Proved <- testIf prem p = (ct : ss, prem)
-        | otherwise = (ss, assert' p prem)
-decidePresburger _ref gs ds ws = withTyCons $ do
-  tcPluginTrace "Env" $ ppr (emptyTyCon, eqTyCon, eqWitnessTyCon, isTrueTyCon)
-  let subst = foldr unionTvSubst emptyTvSubst $ map genSubst (gs ++ ds)
-  tcPluginTrace "Current subst" (ppr subst)
-  tcPluginTrace "wanteds" $ ppr $ map (deconsPred) ws
-  tcPluginTrace "givens" $ ppr $ map (substTy subst . deconsPred) gs
-  tcPluginTrace "deriveds" $ ppr $ map deconsPred ds
-  let wants = mapMaybe (\ct -> (,) ct <$> toPresburgerPred subst (substTy subst $ deconsPred ct)) $
-              filter (isWanted . ctEvidence) ws
-      prems = foldr assert' noProps $
-              mapMaybe (toPresburgerPred subst . substTy subst . deconsPred) (gs ++ ds)
-      solved = map fst $ filter (isProved . testIf prems . snd) wants
-      coerced = [(evByFiat "ghc-typelits-presburger" t1 t2, ct)
-                | ct <- solved
-                , EqPred NomEq t1 t2 <- return (classifyPredType $ deconsPred ct)
-                ]
-  tcPluginTrace "prems" (text $ show $ map (toPresburgerPred subst .substTy subst . deconsPred) (gs ++ ds))
-  tcPluginTrace "final goals" (text $ show $ map snd wants)
-  case testIf prems (foldr (:&&) PTrue (map snd wants)) of
-    Proved -> do
-      tcPluginTrace "Proved" (text $ show $ map snd wants)
-      return $ TcPluginOk coerced []
-    Disproved wit -> do
-      tcPluginTrace "Failed! " (text $ show $ wit)
-      return $ TcPluginContradiction $ map fst wants
-
-withTyCons :: (Given MyEnv => TcPluginM a) -> TcPluginM a
-withTyCons act = do
-  emd <- lookupModule (mkModuleName "Proof.Propositional.Empty") (fsLit "equational-reasoning")
-  emptyCon <- classTyCon <$> (tcLookupClass =<< lookupOrig emd (mkTcOcc "Empty"))
-  eqcon <- getEqTyCon
-  witcon <- getEqWitnessTyCon
-  pmd <- lookupModule (mkModuleName "Proof.Propositional") (fsLit "equational-reasoning")
-  trucon <- tcLookupTyCon =<< lookupOrig pmd (mkTcOcc "IsTrue")
-  vmd <- lookupModule (mkModuleName "Data.Void") (fsLit "base")
-  voidTyCon <- tcLookupTyCon =<< lookupOrig vmd (mkTcOcc "Void")
-  give (MyEnv emptyCon eqcon witcon trucon voidTyCon) act
-
-isVoidTy :: Given MyEnv => Type -> Bool
-isVoidTy typ =
-  tyConAppTyCon_maybe typ == Just (voidTyCon given)
-
-(<=>) :: Prop -> Prop -> Prop
-p <=> q =  (p :&& q) :|| (Not p :&& Not q)
-
-genSubst :: Ct -> TvSubst
-genSubst ct = case classifyPredType (deconsPred ct) of
-  EqPred NomEq t u -> fromMaybe emptyTvSubst $ tcUnifyTy t u
-  _                -> emptyTvSubst
-
-withEv :: Ct -> (EvTerm, Ct)
-withEv ct
-  | EqPred _ t1 t2 <- classifyPredType (deconsPred ct) =
-      (evByFiat "ghc-typelits-presburger" t1 t2, ct)
-  | otherwise = undefined
-
-deconsPred :: Ct -> Type
-deconsPred = ctEvPred . ctEvidence
-
-emptyTyCon :: Given MyEnv => TyCon
-emptyTyCon = emptyClsTyCon given
-
-toPresburgerPred :: Given MyEnv => TvSubst -> Type -> Maybe Prop
-toPresburgerPred subst (TyConApp con [t1, t2])
-  | con == typeNatLeqTyCon = (:<=) <$> toPresburgerExp subst t1 <*> toPresburgerExp subst t2
-toPresburgerPred subst ty
-  | isEqPred ty = toPresburgerPredTree subst $ classifyPredType ty
-  | Just (con, [l, r]) <- splitTyConApp_maybe ty -- l ~ r
-  , con == eqTyCon = toPresburgerPredTree subst $ EqPred NomEq l r
-  | Just (con, [_k, l, r]) <- splitTyConApp_maybe ty -- l (:~: {k}) r
-  , con == eqWitnessTyCon = toPresburgerPredTree subst $ EqPred NomEq l r
-  | Just (con, [l]) <- splitTyConApp_maybe ty -- Empty l => ...
-  , con == emptyTyCon = Not <$> toPresburgerPred subst l
-  | Just (con, [l]) <- splitTyConApp_maybe ty -- IsTrue l =>
-  , con == isTrueTyCon = toPresburgerPred subst l
-  | otherwise = Nothing
-
-toPresburgerPredTree :: Given MyEnv => TvSubst -> PredTree -> Maybe Prop
-toPresburgerPredTree subst (EqPred NomEq p false) -- P ~ 'False <=> Not P ~ 'True
-  | Just promotedFalseDataCon  == tyConAppTyCon_maybe (substTy subst false) =
-    Not <$> toPresburgerPredTree subst (EqPred NomEq p (mkTyConTy promotedTrueDataCon))
-toPresburgerPredTree subst (EqPred NomEq p b)  -- (n :<=? m) ~ 'True
-  | Just promotedTrueDataCon  == tyConAppTyCon_maybe (substTy subst b)
-  , Just (con, [t1, t2]) <- splitTyConApp_maybe (substTy subst p)
-  , con == typeNatLeqTyCon = (:<=) <$> toPresburgerExp subst t1  <*> toPresburgerExp subst t2
-toPresburgerPredTree subst (EqPred NomEq p q)  -- (p :: Bool) ~ (q :: Bool)
-  | typeKind p `eqType` mkTyConTy promotedBoolTyCon =
-    (<=>) <$> toPresburgerPred subst p
-          <*> toPresburgerPred subst q
-toPresburgerPredTree subst (EqPred NomEq n m)  -- (n :: Nat) ~ (m :: Nat)
-  | typeKind n `eqType` typeNatKind =
-    (:==) <$> toPresburgerExp subst n
-          <*> toPresburgerExp subst m
-toPresburgerPredTree subst (EqPred _ t1 t2) -- CmpNat a b ~ CmpNat c d
-  | Just (con,  [a, b]) <- splitTyConApp_maybe (substTy subst t1)
-  , Just (con', [c, d]) <- splitTyConApp_maybe (substTy subst t2)
-  , con == typeNatCmpTyCon, con' == typeNatCmpTyCon
-  = (<=>) <$> ((:<) <$> toPresburgerExp subst a <*> toPresburgerExp subst b)
-          <*> ((:<) <$> toPresburgerExp subst c <*> toPresburgerExp subst d)
-toPresburgerPredTree subst (EqPred NomEq t1 t2) -- CmpNat a b ~ x
-  | Just (con, [a, b]) <- splitTyConApp_maybe (substTy subst t1)
-  , con == typeNatCmpTyCon
-  , Just cmp <- tyConAppTyCon_maybe (substTy subst t2) =
-    let dic = [(promotedLTDataCon, (:<))
-              ,(promotedEQDataCon, (:==))
-              ,(promotedGTDataCon, (:>))
-              ]
-    in lookup cmp dic <*> toPresburgerExp subst a
-                      <*> toPresburgerExp subst b
-toPresburgerPredTree subst (EqPred NomEq t1 t2) -- x ~ CmpNat a b
-  | Just (con, [a, b]) <- splitTyConApp_maybe (substTy subst t2)
-  , con == typeNatCmpTyCon
-  , Just cmp <- tyConAppTyCon_maybe (substTy subst t1) =
-    let dic = [(promotedLTDataCon, (:<))
-              ,(promotedEQDataCon, (:==))
-              ,(promotedGTDataCon, (:>))
-              ]
-    in lookup cmp dic <*> toPresburgerExp subst a
-                      <*> toPresburgerExp subst b
-toPresburgerPredTree subst (ClassPred con [t1, t2]) -- (n :: Nat) <= (m :: Nat)
-  | typeNatLeqTyCon == classTyCon con
-  , typeKind t1 `eqType` typeNatKind = (:<=) <$> toPresburgerExp subst t1 <*> toPresburgerExp subst t2
-toPresburgerPredTree _ _ = Nothing
-
-toPresburgerExp :: TvSubst -> Type -> Maybe Expr
-toPresburgerExp dic ty = case substTy dic ty of
-  TyVarTy t -> Just $ Var $ toName $ getKey $ getUnique t
-  TyConApp tc ts  ->
-    let step con op
-          | tc == con, [tl, tr] <- ts =
-            op <$> toPresburgerExp dic tl <*> toPresburgerExp dic tr
-          | otherwise = Nothing
-    in case ts of
-      [tl, tr] | tc == typeNatMulTyCon ->
-        case (simpleExp tl, simpleExp tr) of
-          (LitTy (NumTyLit n), LitTy (NumTyLit m)) -> Just $ K $ n * m
-          (LitTy (NumTyLit n), x) -> (:*) <$> pure n <*> toPresburgerExp dic x
-          (x, LitTy (NumTyLit n)) -> (:*) <$> pure n <*> toPresburgerExp dic x
-          _ -> Nothing
-      _ ->  asum [ step con op
-                 | (con, op) <- [(typeNatAddTyCon, (:+)), (typeNatSubTyCon, (:-))]]
-  LitTy (NumTyLit n) -> Just (K n)
-  _ -> Nothing
-
--- simplTypeCmp :: Type -> Type
-
-simpleExp :: Type -> Type
-simpleExp (AppTy t1 t2) = AppTy (simpleExp t1) (simpleExp t2)
-simpleExp (FunTy t1 t2) = FunTy (simpleExp t1) (simpleExp t2)
-simpleExp (ForAllTy t1 t2) = ForAllTy t1 (simpleExp t2)
-simpleExp (TyConApp tc ts) = fromMaybe (TyConApp tc (map simpleExp ts)) $
-  asum (map simpler [(typeNatAddTyCon, (+))
-                    ,(typeNatSubTyCon, (-))
-                    ,(typeNatMulTyCon, (*))
-                    ,(typeNatExpTyCon, (^))
-                    ])
-  where
-    simpler (con, op)
-      | con == tc, [tl, tr] <- map simpleExp ts =
-        Just $
-        case (tl, tr) of
-          (LitTy (NumTyLit n), LitTy (NumTyLit m)) -> LitTy (NumTyLit (op n m))
-          _ -> TyConApp con [tl, tr]
-      | otherwise = Nothing
-simpleExp t = t
-
+plugin = pluginWith defaultTranslation
diff --git a/src/GHC/TypeLits/Presburger/Compat.hs b/src/GHC/TypeLits/Presburger/Compat.hs
new file mode 100644
--- /dev/null
+++ b/src/GHC/TypeLits/Presburger/Compat.hs
@@ -0,0 +1,549 @@
+{- HLINT ignore "Use camelCase" -}
+{- HLINT ignore "Move filter" -}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# 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.Coerce (coerce)
+import Data.Function (on)
+import Data.Functor ((<&>))
+import Data.Generics.Twins
+import GHC.TypeLits.Presburger.Flags
+import GHC.Types.Unique as GHC.TypeLits.Presburger.Compat (Unique, getUnique)
+import qualified GHC.Types.Unique as Unique (Unique, getKey)
+#if MIN_VERSION_ghc(9,10,1)
+import GHC.Builtin.Names (gHC_INTERNAL_TYPENATS, gHC_INTERNAL_TYPEERROR)
+import GHC.Builtin.Names (mkGhcInternalModule)
+#else
+import GHC.Builtin.Names (gHC_TYPENATS)
+#if MIN_VERSION_ghc(9,4,1)
+import GHC.Builtin.Names (gHC_TYPENATS, gHC_TYPEERROR)
+#endif
+#endif
+import GHC.Tc.Types.Constraint as GHC.TypeLits.Presburger.Compat
+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)
+import GHC.Tc.Types.Evidence as GHC.TypeLits.Presburger.Compat (evCast)
+import GHC.Plugins as GHC.TypeLits.Presburger.Compat (mkUnivCo, Role(..))
+import GHC.Core.TyCo.Rep as GHC.TypeLits.Presburger.Compat (Coercion)
+import GHC.Core.TyCo.Rep as GHC.TypeLits.Presburger.Compat (UnivCoProvenance(..))
+import GHC.Core.DataCon as GHC.TypeLits.Presburger.Compat (dataConWrapId)
+#else
+import GHC.Tc.Types as GHC.TypeLits.Presburger.Compat (TcPlugin (..), TcPluginResult (..))
+#endif
+#if MIN_VERSION_ghc(9,12,1)
+-- mkBaseModule is not available in GHC 9.12.1+
+import GHC.Core.Reduction (reductionReducedType)
+#elif MIN_VERSION_ghc(9,4,1)
+import GHC.Builtin.Names as GHC.TypeLits.Presburger.Compat (mkBaseModule)
+import GHC.Core.Reduction (reductionReducedType)
+#else
+import qualified GHC.Builtin.Names as Old
+#endif
+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)
+import GHC.Core.FamInstEnv as GHC.TypeLits.Presburger.Compat
+import GHC.Core.Predicate as GHC.TypeLits.Presburger.Compat (EqRel (..), Pred (..), isEqPred, mkPrimEqPredRole)
+import qualified GHC.Core.Predicate as Old (classifyPredType)
+import GHC.Core.TyCo.Rep as GHC.TypeLits.Presburger.Compat (TyLit (NumTyLit), Type (..))
+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)
+#if MIN_VERSION_ghc(9,2,0)
+import GHC.Driver.Env.Types as GHC.TypeLits.Presburger.Compat (HscEnv (hsc_dflags))
+#if !MIN_VERSION_ghc(9,12,1)
+import GHC.Builtin.Names (mkBaseModule)
+#endif
+#else
+import GHC.Driver.Types as GHC.TypeLits.Presburger.Compat (HscEnv (hsc_dflags))
+import GHC.Driver.Session (unitState, unitDatabases)
+#endif
+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)
+import GHC.Builtin.Types (naturalTy)
+#else
+import GHC.Plugins as GHC.TypeLits.Presburger.Compat 
+  ( HsParsedModule(..),
+    lookupTyCon,
+    typeNatKind
+  )
+#endif
+
+#if MIN_VERSION_ghc(9,6,1)
+import GHC.Plugins as GHC.TypeLits.Presburger.Compat
+  ( Subst (..),
+    emptySubst,
+    unionSubst,
+  )
+import GHC.Core.TyCo.Compare as GHC.TypeLits.Presburger.Compat
+  (eqType)
+#else
+import GHC.Plugins as GHC.TypeLits.Presburger.Compat
+  ( TCvSubst (..),
+    emptyTCvSubst,
+    eqType,
+    unionTCvSubst,
+  )
+#endif
+
+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)
+import GHC.Unit.Types as GHC.TypeLits.Presburger.Compat (IsBootInterface(..))
+#else
+import GHC.Driver.Types as GHC.TypeLits.Presburger.Compat (IsBootInterface(..))
+#endif
+
+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.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.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.Types (UnitId (..), fsToUnit, toUnitId)
+import GHC.Utils.Outputable as GHC.TypeLits.Presburger.Compat (showSDocUnsafe)
+
+#if !MIN_VERSION_ghc(9,4,1)
+type TcPluginSolveResult = TcPluginResult
+#endif
+
+-- mkUnivCo API compatibility
+#if MIN_VERSION_ghc(9,12,1)
+mkUnivCo' :: UnivCoProvenance -> Role -> Type -> Type -> Coercion  
+mkUnivCo' prov role ty1 ty2 = mkUnivCo prov [] role ty1 ty2
+#else
+mkUnivCo' :: UnivCoProvenance -> Role -> Type -> Type -> Coercion  
+mkUnivCo' = mkUnivCo
+#endif
+
+#if MIN_VERSION_ghc(9,10,1)
+dATA_TYPE_EQUALITY :: Module
+dATA_TYPE_EQUALITY = mkGhcInternalModule "GHC.Internal.Data.Type.Equality"
+#else
+dATA_TYPE_EQUALITY :: Module
+dATA_TYPE_EQUALITY = mkBaseModule "Data.Type.Equality"
+#endif
+
+#if MIN_VERSION_ghc(9,10,1)
+gHC_TYPEERROR :: Module
+gHC_TYPEERROR = gHC_INTERNAL_TYPEERROR
+
+gHC_TYPENATS :: Module
+gHC_TYPENATS =  gHC_INTERNAL_TYPENATS
+#elif !MIN_VERSION_ghc(9,4,1)
+gHC_TYPEERROR :: Module
+gHC_TYPEERROR = mkBaseModule "GHC.TypeLits"
+#endif
+
+type PredTree = Pred
+
+data TvSubst = TvSubst InScopeSet TvSubstEnv
+
+#if MIN_VERSION_ghc(9,6,1)
+type TCvSubst = Subst
+unionTCvSubst :: TCvSubst -> TCvSubst -> TCvSubst
+unionTCvSubst = unionSubst
+
+emptyTCvSubst :: Subst
+emptyTCvSubst = emptySubst
+#endif
+
+instance Outputable TvSubst where
+  ppr = ppr . toTCv
+
+emptyTvSubst :: TvSubst
+#if MIN_VERSION_ghc(9,6,1)
+emptyTvSubst = case emptyTCvSubst of
+  Subst set _ tvsenv _ -> TvSubst set tvsenv
+#else
+emptyTvSubst = case emptyTCvSubst of
+  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
+#else
+toTCv (TvSubst set tvenv) = TCvSubst set tvenv emptyUFM
+#endif
+
+substTy :: TvSubst -> Type -> Type
+substTy tvs = Old.substTy (toTCv tvs)
+
+unionTvSubst :: TvSubst -> TvSubst -> TvSubst
+unionTvSubst s1 s2 =
+  fromTCv $ unionTCvSubst (toTCv s1) (toTCv s2)
+
+fromTCv :: TCvSubst -> TvSubst
+#if MIN_VERSION_ghc(9,6,1)
+fromTCv (Subst set _ tvsenv _) = TvSubst set tvsenv
+#else
+fromTCv (TCvSubst set tvsenv _) = TvSubst set tvsenv
+#endif
+
+promotedBoolTyCon :: TyCon
+promotedBoolTyCon = boolTyCon
+
+viewFunTy :: Type -> Maybe (Type, Type)
+viewFunTy t@(TyConApp _ [t1, t2])
+  | Old.isFunTy t = Just (t1, t2)
+viewFunTy _ = Nothing
+
+tcUnifyTy :: Type -> Type -> Maybe TvSubst
+tcUnifyTy t1 t2 = fromTCv <$> Old.tcUnifyTy t1 t2
+
+getEqTyCon :: TcPluginM TyCon
+getEqTyCon =
+  return TysWiredIn.eqTyCon
+
+getEqWitnessTyCon :: TcPluginM TyCon
+getEqWitnessTyCon = do
+  tcLookupTyCon =<< lookupOrig dATA_TYPE_EQUALITY (mkTcOcc ":~:")
+
+getEqBoolTyCon :: TcPluginM TyCon
+getEqBoolTyCon = do
+  tcLookupTyCon =<< lookupOrig dATA_TYPE_EQUALITY (mkTcOcc "==")
+
+decompFunTy :: Type -> [Type]
+decompFunTy (FunTy _ _ t1 t2) = t1 : decompFunTy t2
+decompFunTy t = [t]
+
+newtype TypeEq = TypeEq {runTypeEq :: Type}
+
+instance Eq TypeEq where
+  (==) = geq `on` runTypeEq
+
+instance Ord TypeEq where
+  compare = gcompare `on` runTypeEq
+
+isTrivial :: Old.PredType -> Bool
+isTrivial ty =
+  case classifyPredType ty of
+    EqPred _ l r -> l `eqType` r
+    _ -> False
+
+normaliseGivens ::
+  [Ct] -> TcPluginM [Ct]
+normaliseGivens =
+  fmap (return . filter (not . isTrivial . ctEvPred . ctEvidence))
+    . (++)
+    <$> id
+    <*> Extra.flattenGivens
+
+#if MIN_VERSION_ghc(8,4,1)
+type Substitution = [(TcTyVar, TcType)]
+#else
+type Substitution = TvSubst
+#endif
+
+subsCt :: Substitution -> Ct -> Ct
+subsCt = Extra.substCt
+
+subsType :: Substitution -> Type -> Type
+subsType = Extra.substType
+
+mkSubstitution :: [Ct] -> Substitution
+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 -> e
+
+fsToUnitId :: FastString -> UnitId
+fsToUnitId = toUnitId . fsToUnit
+
+loadedPackageNames ::
+  [UnitDatabase UnitId] ->
+  UnitState ->
+  [RawPackageName]
+loadedPackageNames unitDb us =
+  let preloads = mkUniqSet $ map (\(UnitId p) -> p) $ preloadUnits us
+      ents = filter ((`elementOfUniqSet` preloads) . unitIdFS . unitId) $ concatMap unitDatabaseUnits unitDb
+   in map (coerce . unitPackageName) ents
+
+type RawPackageName = FastString
+
+preloadedUnitsM :: TcPluginM [RawPackageName]
+#if MIN_VERSION_ghc(9,4,0)
+preloadedUnitsM = do
+  logger <- unsafeTcPluginTcM getLogger
+  dflags <- hsc_dflags <$> getTopEnv
+  packNames <- tcPluginIO $ initUnits logger dflags Nothing mempty <&> 
+    \(unitDb, us, _, _ ) -> loadedPackageNames unitDb us
+  tcPluginTrace "pres: packs" $ ppr packNames
+  pure $ coerce packNames
+#elif MIN_VERSION_ghc(9,2,0)
+preloadedUnitsM = do
+  logger <- unsafeTcPluginTcM getLogger
+  dflags <- hsc_dflags <$> getTopEnv
+  packNames <- tcPluginIO $ initUnits logger dflags Nothing <&> 
+    \(unitDb, us, _, _ ) -> loadedPackageNames unitDb us
+  tcPluginTrace "pres: packs" $ ppr packNames
+  pure packNames
+#elif MIN_VERSION_ghc(9,0,0)
+preloadedUnitsM = do
+  dflags <- hsc_dflags <$> getTopEnv
+  packNames <- tcPluginIO $ initUnits dflags <&> \dfs' ->
+    let st = unitState dfs'
+        db = maybe [] id $ unitDatabases dfs'
+     in loadedPackageNames db st
+  tcPluginTrace "pres: packs" $ ppr packNames
+  pure packNames
+#else
+preloadedUnitsM = do
+  dflags <- hsc_dflags <$> getTopEnv
+  (dfs', packs) <- tcPluginIO $ initPackages dflags
+  let db = listPackageConfigMap dfs'
+      loadeds = mkUniqSet $ map (\(InstalledUnitId p) -> p) packs
+      packNames = map (coerce . packageName) $
+        filter ((`elementOfUniqSet` loadeds) . coerce . unitId) db
+  tcPluginTrace "pres: packs" $ ppr packNames
+  pure packNames
+#endif
+
+type ModuleUnit = Unit
+
+moduleUnit' :: Module -> ModuleUnit
+moduleUnit' = moduleUnit
+
+noExtField :: NoExtField
+noExtField = NoExtField
+
+type HsModule' = HsModule
+
+#if MIN_VERSION_ghc(9,2,0)
+typeNatKind :: TcType
+typeNatKind = naturalTy
+#endif
+
+mtypeNatLeqTyCon :: Maybe TyCon
+#if MIN_VERSION_ghc(9,2,0)
+mtypeNatLeqTyCon = Nothing
+#else
+mtypeNatLeqTyCon = Just typeNatLeqTyCon
+#endif
+
+dATA_TYPE_ORD :: Module
+#if MIN_VERSION_ghc(9,10,0)
+dATA_TYPE_ORD = mkGhcInternalModule "GHC.Internal.Data.Type.Ord"
+#else
+dATA_TYPE_ORD = mkBaseModule "Data.Type.Ord"
+#endif
+
+lookupTyNatPredLeq :: TcPluginM Name
+#if MIN_VERSION_ghc(9,2,0)
+lookupTyNatPredLeq = lookupOrig dATA_TYPE_ORD (mkTcOcc "<=")
+#else
+lookupTyNatPredLeq = 
+  lookupOrig gHC_TYPENATS (mkTcOcc "<=")
+#endif
+
+lookupTyNatBoolLeq :: TcPluginM TyCon
+#if MIN_VERSION_ghc(9,2,0)
+lookupTyNatBoolLeq = tcLookupTyCon =<< lookupOrig dATA_TYPE_ORD (mkTcOcc "<=?")
+#else
+lookupTyNatBoolLeq = 
+  pure typeNatLeqTyCon
+#endif
+
+lookupAssertTyCon :: TcPluginM (Maybe TyCon)
+#if MIN_VERSION_base(4,17,0)
+lookupAssertTyCon = 
+  fmap Just . tcLookupTyCon =<< lookupOrig gHC_TYPEERROR (mkTcOcc "Assert")
+#else
+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)
+lookupTyNatPredLt = Just <$> do
+  tcLookupTyCon =<< lookupOrig dATA_TYPE_ORD (mkTcOcc "<")
+#else
+lookupTyNatPredLt = pure Nothing
+#endif
+
+lookupTyNatBoolLt :: TcPluginM (Maybe TyCon)
+#if MIN_VERSION_ghc(9,2,0)
+lookupTyNatBoolLt = Just <$> do
+  tcLookupTyCon =<< lookupOrig dATA_TYPE_ORD (mkTcOcc "<?")
+#else
+lookupTyNatBoolLt = pure Nothing
+#endif
+
+lookupTyNatPredGt :: TcPluginM (Maybe TyCon)
+#if MIN_VERSION_ghc(9,2,0)
+lookupTyNatPredGt = Just <$> do
+  tcLookupTyCon =<< lookupOrig dATA_TYPE_ORD (mkTcOcc ">")
+#else
+lookupTyNatPredGt = pure Nothing
+#endif
+
+lookupTyNatBoolGt :: TcPluginM (Maybe TyCon)
+#if MIN_VERSION_ghc(9,2,0)
+lookupTyNatBoolGt = Just <$> do
+  tcLookupTyCon =<< lookupOrig dATA_TYPE_ORD (mkTcOcc ">?")
+#else
+lookupTyNatBoolGt = pure Nothing
+#endif
+
+lookupTyNatPredGeq :: TcPluginM (Maybe TyCon)
+#if MIN_VERSION_ghc(9,2,0)
+lookupTyNatPredGeq = Just <$> do
+  tcLookupTyCon =<< lookupOrig dATA_TYPE_ORD (mkTcOcc ">=")
+#else
+lookupTyNatPredGeq = pure Nothing
+#endif
+
+lookupTyNatBoolGeq :: TcPluginM (Maybe TyCon)
+#if MIN_VERSION_ghc(9,2,0)
+lookupTyNatBoolGeq = Just <$> do
+  tcLookupTyCon =<< lookupOrig dATA_TYPE_ORD (mkTcOcc ">=?")
+#else
+lookupTyNatBoolGeq = pure Nothing
+#endif
+
+mOrdCondTyCon :: TcPluginM (Maybe TyCon)
+#if MIN_VERSION_ghc(9,2,0)
+mOrdCondTyCon = Just <$> do
+  tcLookupTyCon =<< lookupOrig dATA_TYPE_ORD (mkTcOcc "OrdCond")
+#else
+mOrdCondTyCon = pure Nothing
+#endif
+
+lookupTyGenericCompare :: TcPluginM (Maybe TyCon)
+#if MIN_VERSION_ghc(9,2,0)
+lookupTyGenericCompare = Just <$> do
+  tcLookupTyCon =<< lookupOrig dATA_TYPE_ORD (mkTcOcc "Compare")
+#else
+lookupTyGenericCompare = pure Nothing
+#endif
+
+lookupBool47 :: String -> TcPluginM (Maybe TyCon)
+#if MIN_VERSION_ghc(9,10,0)
+lookupBool47 nam = Just <$> do
+  tcLookupTyCon =<< lookupOrig (mkGhcInternalModule "GHC.Internal.Data.Type.Bool") (mkTcOcc nam)
+#elif MIN_VERSION_base(4,17,0)
+lookupBool47 nam = Just <$> do
+  tcLookupTyCon =<< lookupOrig (mkBaseModule "Data.Type.Bool") (mkTcOcc nam)
+#else
+lookupBool47 = const $ pure Nothing
+#endif
+
+lookupTyNot, lookupTyIf, lookupTyAnd, lookupTyOr :: TcPluginM (Maybe TyCon)
+lookupTyNot = lookupBool47 "Not"
+lookupTyIf = lookupBool47 "If"
+lookupTyAnd = lookupBool47 "&&"
+lookupTyOr = lookupBool47 "||"
+
+matchFam' :: TyCon -> [Type] -> TcPluginM (Maybe Type)
+#if MIN_VERSION_ghc(9,4,1)
+matchFam' con args = fmap reductionReducedType <$> matchFam con args
+#else
+matchFam' con args = fmap snd <$> matchFam con args 
+#endif
+
+getKey :: Unique.Unique -> Int
+getKey = fromIntegral . Unique.getKey
+
+getVoidTyCon :: TcPluginM TyCon
+getVoidTyCon = tcLookupTyCon =<< lookupOrig aMod (mkTcOcc "Void")
+  where
+#if MIN_VERSION_ghc(9,10,1)
+    aMod = mkGhcInternalModule "GHC.Internal.Base"
+#elif MIN_VERSION_ghc(9,6,1)
+    aMod = mkBaseModule "GHC.Base"
+#else
+    aMod = mkBaseModule "Data.Void"
+#endif
diff --git a/src/GHC/TypeLits/Presburger/Flags.hs b/src/GHC/TypeLits/Presburger/Flags.hs
new file mode 100644
--- /dev/null
+++ b/src/GHC/TypeLits/Presburger/Flags.hs
@@ -0,0 +1,31 @@
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE CPP #-}
+module GHC.TypeLits.Presburger.Flags (GHCVer(..), ghcVer) where
+import GHC.Generics (Generic)
+
+data GHCVer 
+  = GHC806 | GHC808 | GHC810 
+  | GHC900 | GHC902 | GHC904 
+  | GHC906 | GHC908 | GHC910
+  deriving (Show, Eq, Ord, Generic)
+
+ghcVer :: GHCVer
+#if MIN_VERSION_ghc(9,10,1)
+ghcVer = GHC910
+#elif MIN_VERSION_ghc(9,8,1)
+ghcVer = GHC908
+#elif MIN_VERSION_ghc(9,6,1)
+ghcVer = GHC906
+#elif MIN_VERSION_ghc(9,4,1)
+ghcVer = GHC904
+#elif MIN_VERSION_ghc(9,2,1)
+ghcVer = GHC902
+#elif MIN_VERSION_ghc(9,0,1)
+ghcVer = GHC900
+#elif MIN_VERSION_ghc(8,10,1)
+ghcVer = GHC810
+#elif MIN_VERSION_ghc(8,8,1)
+ghcVer = GHC808
+#else
+ghcVer = GHC806
+#endif
diff --git a/src/GHC/TypeLits/Presburger/Types.hs b/src/GHC/TypeLits/Presburger/Types.hs
new file mode 100644
--- /dev/null
+++ b/src/GHC/TypeLits/Presburger/Types.hs
@@ -0,0 +1,773 @@
+{-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE MultiWayIf #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE PatternGuards #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE DerivingVia #-}
+{-# LANGUAGE NamedFieldPuns #-}
+{-# LANGUAGE PartialTypeSignatures #-}
+{-# OPTIONS_GHC -Wno-partial-type-signatures #-}
+
+-- | Since 0.3.0.0
+module GHC.TypeLits.Presburger.Types
+  ( pluginWith,
+    defaultTranslation,
+    Translation (..),
+    ParseEnv,
+    Machine,
+    module Data.Integer.SAT,
+  )
+where
+
+import Control.Applicative ((<|>))
+import Control.Arrow (second)
+import Control.Monad (forM_, guard, mzero, unless)
+import Control.Monad.State.Class
+import Control.Monad.Trans.Class
+import Control.Monad.Trans.Maybe (MaybeT (..))
+import Control.Monad.Trans.RWS.Strict (runRWS, tell)
+import Control.Monad.Trans.State (StateT, runStateT)
+import Data.Char (isDigit)
+import Data.Foldable (asum)
+import Data.Integer.SAT (Expr (..), Prop (..), PropSet, assert, checkSat, noProps, toName)
+import qualified Data.Integer.SAT as SAT
+import Data.List (nub)
+#if MIN_VERSION_ghc(9,4,0)
+import qualified GHC.Core as GHC (Expr(..))
+#endif
+import qualified Data.List as L
+import qualified Data.Map.Strict as M
+import Data.Maybe
+  ( catMaybes,
+    fromMaybe,
+    isNothing,
+    listToMaybe,
+    maybeToList,
+  )
+import Data.Reflection (Given, give, given)
+import qualified Data.Set as Set
+import GHC.TypeLits.Presburger.Compat as Compat
+import qualified Data.Foldable as F
+import GHC.TypeLits.Presburger.Flags
+
+assert' :: Prop -> PropSet -> PropSet
+assert' p ps = foldr assert ps (p : varPos)
+  where
+    varPos = [K 0 :<= Var i | i <- varsProp p]
+
+data Proof = Proved | Disproved [(Int, Integer)]
+  deriving (Read, Show, Eq, Ord)
+
+isProved :: Proof -> Bool
+isProved Proved = True
+isProved _ = False
+
+varsProp :: Prop -> [SAT.Name]
+varsProp (p :|| q) = nub $ varsProp p ++ varsProp q
+varsProp (p :&& q) = nub $ varsProp p ++ varsProp q
+varsProp (Not p) = varsProp p
+varsProp (e :== v) = nub $ varsExpr e ++ varsExpr v
+varsProp (e :/= v) = nub $ varsExpr e ++ varsExpr v
+varsProp (e :< v) = nub $ varsExpr e ++ varsExpr v
+varsProp (e :> v) = nub $ varsExpr e ++ varsExpr v
+varsProp (e :<= v) = nub $ varsExpr e ++ varsExpr v
+varsProp (e :>= v) = nub $ varsExpr e ++ varsExpr v
+varsProp _ = []
+
+varsExpr :: Expr -> [SAT.Name]
+varsExpr (e :+ v) = nub $ varsExpr e ++ varsExpr v
+varsExpr (e :- v) = nub $ varsExpr e ++ varsExpr v
+varsExpr (_ :* v) = varsExpr v
+varsExpr (Negate e) = varsExpr e
+varsExpr (Min l r) = nub $ varsExpr l ++ varsExpr r
+varsExpr (Max l r) = nub $ varsExpr l ++ varsExpr r
+varsExpr (Var i) = [i]
+varsExpr (K _) = []
+varsExpr (If p e v) = nub $ varsProp p ++ varsExpr e ++ varsExpr v
+varsExpr (Div e _) = varsExpr e
+varsExpr (Mod e _) = varsExpr e
+
+data PluginMode
+  = DisallowNegatives
+  | AllowNegatives
+  deriving (Read, Show, Eq, Ord)
+
+pluginWith :: TcPluginM Translation -> Plugin
+pluginWith trans =
+  defaultPlugin
+    { tcPlugin = Just . presburgerPlugin trans . procOpts
+    , pluginRecompile = purePlugin
+    }
+  where
+    procOpts opts
+      | "allow-negated-numbers" `elem` opts = AllowNegatives
+      | otherwise = DisallowNegatives
+
+presburgerPlugin :: TcPluginM Translation -> PluginMode -> TcPlugin
+presburgerPlugin trans mode =
+  tracePlugin
+    "typelits-presburger"
+    TcPlugin
+      { tcPluginInit = return ()
+      , tcPluginStop = const $ return ()
+#if MIN_VERSION_ghc(9,4,1)
+      , tcPluginSolve = const $ \_ gs ws -> decidePresburger mode trans () gs [] ws
+#else
+      , tcPluginSolve = decidePresburger mode trans
+#endif
+
+#if MIN_VERSION_ghc(9,4,1)
+      , tcPluginRewrite = mempty
+#endif
+      }
+
+testIf :: PropSet -> Prop -> Proof
+testIf ps q = maybe Proved Disproved $ checkSat (Not q `assert'` ps)
+
+-- Replaces every subtraction with new constant,
+-- adding order constraint.
+handleSubtraction :: PluginMode -> Prop -> Prop
+handleSubtraction AllowNegatives p = p
+handleSubtraction DisallowNegatives p0 =
+  let (p, _, w) = runRWS (loop p0) () Set.empty
+   in foldr (:&&) p w
+  where
+    loop PTrue = return PTrue
+    loop PFalse = return PFalse
+    loop (q :|| r) = (:||) <$> loop q <*> loop r
+    loop (q :&& r) = (:&&) <$> loop q <*> loop r
+    loop (Not q) = Not <$> loop q
+    loop (l :<= r) = (:<=) <$> loopExp l <*> loopExp r
+    loop (l :< r) = (:<) <$> loopExp l <*> loopExp r
+    loop (l :>= r) = (:>=) <$> loopExp l <*> loopExp r
+    loop (l :> r) = (:>) <$> loopExp l <*> loopExp r
+    loop (l :== r) = (:==) <$> loopExp l <*> loopExp r
+    loop (l :/= r) = (:/=) <$> loopExp l <*> loopExp r
+
+    withPositive pos = do
+      dic <- get
+      unless (Set.member pos dic) $ do
+        modify $ Set.insert pos
+        tell $ Set.fromList [pos :>= K 0]
+      return pos
+
+    loopExp e@(Negate _) = withPositive . Negate =<< loopExp e
+    loopExp (l :- r) = do
+      e <- (:-) <$> loopExp l <*> loopExp r
+      withPositive e
+    loopExp (l :+ r) = (:+) <$> loopExp l <*> loopExp r
+    loopExp v@Var {} = return v
+    loopExp (c :* e)
+      | c > 0 = (c :*) <$> loopExp e
+      | otherwise = (negate c :*) <$> loopExp (Negate e)
+    loopExp (Min l r) = Min <$> loopExp l <*> loopExp r
+    loopExp (Max l r) = Max <$> loopExp l <*> loopExp r
+    loopExp (If p l r) = If <$> loop p <*> loopExp l <*> loopExp r
+    loopExp (Mod l n) = Mod <$> loopExp l <*> pure n
+    loopExp (Div l n) = Div <$> loopExp l <*> pure n
+    loopExp e@(K _) = return e
+
+data Translation = Translation
+  { isEmpty :: [TyCon]
+  , ordCond :: [TyCon]
+  , assertTy :: [TyCon]
+  , isTrue :: [TyCon]
+  , trueData :: [TyCon]
+  , falseData :: [TyCon]
+  , voids :: [TyCon]
+  , tyEq :: [TyCon]
+  , tyEqBool :: [TyCon]
+  , tyEqWitness :: [TyCon]
+  , tyNot :: [TyCon]
+  , tyAnd :: [TyCon]
+  , tyOr :: [TyCon]
+  , tyIf :: [TyCon]
+  , tyNeqBool :: [TyCon]
+  , natPlus :: [TyCon]
+  , natMinus :: [TyCon]
+  , natExp :: [TyCon]
+  , natTimes :: [TyCon]
+  , natLeq :: [TyCon]
+  , natLeqBool :: [TyCon]
+  , natGeq :: [TyCon]
+  , natGeqBool :: [TyCon]
+  , natLt :: [TyCon]
+  , natLtBool :: [TyCon]
+  , natGt :: [TyCon]
+  , natGtBool :: [TyCon]
+  , natMin :: [TyCon]
+  , natMax :: [TyCon]
+  , orderingLT :: [TyCon]
+  , orderingGT :: [TyCon]
+  , orderingEQ :: [TyCon]
+  , natCompare :: [TyCon]
+  , parsePred :: (Type -> Machine Expr) -> Type -> Machine Prop
+  , parseExpr :: (Type -> Machine Expr) -> Type -> Machine Expr
+  }
+
+instance Semigroup Translation where
+  l <> r =
+    Translation
+      { isEmpty = isEmpty l <> isEmpty r
+      , isTrue = isTrue l <> isTrue r
+      , assertTy = assertTy l <> assertTy r
+      , voids = voids l <> voids r
+      , tyEq = tyEq l <> tyEq r
+      , tyNot = tyNot l <> tyNot r
+      , tyAnd = tyAnd l <> tyAnd r
+      , tyOr = tyOr l <> tyOr r
+      , tyIf = tyIf l <> tyIf r
+      , tyEqBool = tyEqBool l <> tyEqBool r
+      , tyEqWitness = tyEqWitness l <> tyEqWitness r
+      , tyNeqBool = tyNeqBool l <> tyNeqBool r
+      , natPlus = natPlus l <> natPlus r
+      , natMinus = natMinus l <> natMinus r
+      , natTimes = natTimes l <> natTimes r
+      , natExp = natExp l <> natExp r
+      , natLeq = natLeq l <> natLeq r
+      , natGeq = natGeq l <> natGeq r
+      , natLt = natLt l <> natLt r
+      , natGt = natGt l <> natGt r
+      , natLeqBool = natLeqBool l <> natLeqBool r
+      , natGeqBool = natGeqBool l <> natGeqBool r
+      , natLtBool = natLtBool l <> natLtBool r
+      , natGtBool = natGtBool l <> natGtBool r
+      , orderingLT = orderingLT l <> orderingLT r
+      , orderingGT = orderingGT l <> orderingGT r
+      , orderingEQ = orderingEQ l <> orderingEQ r
+      , natCompare = natCompare l <> natCompare r
+      , trueData = trueData l <> trueData r
+      , falseData = falseData l <> falseData r
+      , parsePred = \f ty -> parsePred l f ty <|> parsePred r f ty
+      , parseExpr = \toE -> (<|>) <$> parseExpr l toE <*> parseExpr r toE
+      , natMin = natMin l <> natMin r
+      , natMax = natMax l <> natMax r
+      , ordCond = ordCond l <> ordCond r
+      }
+
+instance Monoid Translation where
+  mempty =
+    Translation
+      { isEmpty = mempty
+      , isTrue = mempty
+      , assertTy = mempty
+      , tyEq = mempty
+      , tyEqBool = mempty
+      , tyEqWitness = mempty
+      , tyNeqBool = mempty
+      , tyNot = mempty
+      , tyAnd = mempty
+      , tyOr = mempty
+      , tyIf = mempty
+      , voids = mempty
+      , natPlus = mempty
+      , natMinus = mempty
+      , natTimes = mempty
+      , natExp = mempty
+      , natLeq = mempty
+      , natGeq = mempty
+      , natLt = mempty
+      , natGt = mempty
+      , natLeqBool = mempty
+      , natGeqBool = mempty
+      , natLtBool = mempty
+      , natGtBool = mempty
+      , orderingLT = mempty
+      , orderingGT = mempty
+      , orderingEQ = mempty
+      , natCompare = mempty
+      , trueData = []
+      , falseData = []
+      , parsePred = const $ const mzero
+      , parseExpr = const $ const mzero
+      , natMin = mempty
+      , natMax = mempty
+      , ordCond = mempty
+      }
+
+decidePresburger :: PluginMode -> TcPluginM Translation -> () -> [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginSolveResult
+decidePresburger _ genTrans _ gs [] [] = do
+  tcPluginTrace "pres: Started givens with: " (ppr $ map (ctEvPred . ctEvidence) gs)
+  trans <- genTrans
+  give trans $ do
+    ngs <- mapM (\a -> runMachine $ (,) a <$> toPresburgerPred (deconsPred a)) gs
+    let givens = catMaybes ngs
+        prems0 = map snd givens
+        prems = foldr assert' noProps prems0
+    if isNothing (checkSat prems)
+      then return $ TcPluginContradiction gs
+      else return $ TcPluginOk [] []
+decidePresburger mode genTrans _ gs _ds ws = do
+  trans <- genTrans
+  give trans $ do
+    gs' <- normaliseGivens gs
+    let subst = mkSubstitution gs'
+    tcPluginTrace "pres: Current subst" (ppr subst)
+    tcPluginTrace "pres: wanteds" $ ppr $ map (subsType subst . deconsPred . subsCt subst) ws
+    tcPluginTrace "pres: givens" $ ppr $ map (subsType subst . deconsPred) gs
+    (prems, wants, prems0) <- do
+      wants <-
+        catMaybes
+          <$> mapM
+            ( \ct ->
+                runMachine $
+                  (,) ct
+                    <$> toPresburgerPred
+                      ( subsType subst $
+                          deconsPred $ subsCt subst ct
+                      )
+            )
+            (filter (isWanted . ctEvidence) ws)
+
+      resls <-
+        mapM
+          (runMachine . toPresburgerPred . subsType subst . deconsPred)
+          gs
+      let prems = foldr assert' noProps $ catMaybes resls
+      return (prems, map (second $ handleSubtraction mode) wants, catMaybes resls)
+    let solved = map fst $ filter (isProved . testIf prems . snd) wants
+        coerced =
+          [ (evProof, ct)
+          | ct <- solved
+          , Just evProof <- pure $ extractProof $ classifyPredType $ deconsPred ct
+          ]
+    tcPluginTrace "pres: final premises" (text $ show prems0)
+    tcPluginTrace "pres: final goals" (text $ show $ map snd wants)
+    case testIf prems (foldr ((:&&) . snd) PTrue wants) of
+      Proved -> do
+        tcPluginTrace "pres: Proved" (text $ show $ map snd wants)
+        tcPluginTrace "pres: ... with coercions" (ppr coerced)
+        return $ TcPluginOk coerced []
+      Disproved wit -> do
+        tcPluginTrace "pres: Failed! " (text $ show wit)
+        return $ TcPluginContradiction $ map fst wants
+
+
+extractProof :: Given Translation => PredTree -> Maybe EvTerm
+extractProof (EqPred NomEq t1 t2) = 
+    Just $ evByFiat "ghc-typelits-presburger" t1 t2
+#if MIN_VERSION_base(4,17,0)
+extractProof (IrredPred prd)
+  | Just (con, lastN 2 -> [_, _]) <- splitTyConApp_maybe prd
+  , con `elem` assertTy given = 
+    Just $ GHC.Var (dataConWrapId $ cTupleDataCon 0) `evCast`
+      mkUnivCo'
+      (PluginProv $ "ghc-typelits-presburger: extractProof")
+      Representational
+      (mkTyConTy (cTupleTyCon 0))
+      prd
+#endif
+extractProof _ = Nothing
+
+eqReasoning :: FastString
+eqReasoning = fsLit "equational-reasoning"
+
+defaultTranslation :: TcPluginM Translation
+defaultTranslation = do
+  packs <- preloadedUnitsM
+  let eqThere = elem eqReasoning packs
+  (isEmpties, isTrues) <-
+    if eqThere
+      then do
+        tcPluginTrace "pres: equational-reasoning activated!" $ ppr ()
+        emd <- lookupModule (mkModuleName "Proof.Propositional.Empty") eqReasoning
+        pmd <- lookupModule (mkModuleName "Proof.Propositional") eqReasoning
+
+        emptyClsTyCon <- classTyCon <$> (tcLookupClass =<< lookupOrig emd (mkTcOcc "Empty"))
+        isTrueCon_ <- tcLookupTyCon =<< lookupOrig pmd (mkTcOcc "IsTrue")
+        pure ([emptyClsTyCon], [isTrueCon_])
+      else do
+        tcPluginTrace "pres: No equational-reasoning found." $ ppr ()
+        pure ([], [])
+
+  eqTyCon_ <- getEqTyCon
+  eqBoolTyCon <- getEqBoolTyCon
+  eqWitCon_ <- getEqWitnessTyCon
+  assertTy <- lookupAssertTyCon
+  voidTyCon <- getVoidTyCon
+  nLeq <- tcLookupTyCon =<< lookupTyNatPredLeq
+  tyLeqB <- lookupTyNatBoolLeq
+  mTyLtP <- lookupTyNatPredLt
+  mTyLtB <- lookupTyNatBoolLt
+  mTyGeqP <- lookupTyNatPredGeq
+  mTyGeqB <- lookupTyNatBoolGeq
+  mTyGtP <- lookupTyNatPredGt
+  mTyGtB <- lookupTyNatBoolGt
+  mOrdCond <- mOrdCondTyCon
+  mtyGenericCompare <- lookupTyGenericCompare
+  tyNot <- maybeToList <$> lookupTyNot
+  tyAnd <- maybeToList <$> lookupTyAnd
+  tyOr <- maybeToList <$> lookupTyOr
+  tyIf <- maybeToList <$> lookupTyIf
+  let trans =
+        mempty
+          { isEmpty = isEmpties
+          , assertTy = maybeToList assertTy
+          , tyEq = [eqTyCon_]
+          , tyNot
+          , tyAnd
+          , tyOr
+          , tyIf
+          , ordCond = F.toList mOrdCond
+          , tyEqWitness = [eqWitCon_]
+          , tyEqBool = [eqBoolTyCon]
+          , isTrue = isTrues
+          , voids = [voidTyCon]
+          , natMinus = [typeNatSubTyCon]
+          , natPlus = [typeNatAddTyCon]
+          , natTimes = [typeNatMulTyCon]
+          , natExp = [typeNatExpTyCon]
+          , falseData = [promotedFalseDataCon]
+          , trueData = [promotedTrueDataCon]
+          , natLeqBool = [tyLeqB]
+          , natLeq = [nLeq]
+          , natGeqBool = F.toList mTyGeqB
+          , natGeq = F.toList mTyGeqP
+          , natGtBool = F.toList mTyGtB
+          , natGt = F.toList mTyGtP
+          , natLtBool = F.toList mTyLtB
+          , natLt = F.toList mTyLtP
+          , natCompare = typeNatCmpTyCon : F.toList mtyGenericCompare
+          , orderingEQ = [promotedEQDataCon]
+          , orderingLT = [promotedLTDataCon]
+          , orderingGT = [promotedGTDataCon]
+          }
+  tcPluginTrace "Final translation: " (ppr mTyGeqB)
+  pure trans
+
+(<=>) :: Prop -> Prop -> Prop
+p <=> q = (p :&& q) :|| (Not p :&& Not q)
+
+orderingDic :: Given Translation => [(TyCon, Expr -> Expr -> Prop)]
+orderingDic =
+  [(lt, (:<)) | lt <- orderingLT given]
+  ++ [(eq, (:==)) | eq <- orderingEQ given]
+    ++ [(gt, (:>)) | gt <- orderingGT given]
+
+deconsPred :: Ct -> Type
+deconsPred = ctEvPred . ctEvidence
+
+toPresburgerPred :: Given Translation => Type -> Machine Prop
+toPresburgerPred (TyConApp con (lastN 2 -> [t1, t2]))
+  | con `elem` (natLeq given ++ natLeqBool given) =
+    (:<=) <$> toPresburgerExp t1 <*> toPresburgerExp t2
+toPresburgerPred (TyConApp con [t1, _])
+  | con `elem` assertTy given = toPresburgerPred t1
+toPresburgerPred ty
+  | Just (con, []) <- splitTyConApp_maybe ty
+    , con `elem` trueData given =
+    return PTrue
+  | Just (con, []) <- splitTyConApp_maybe ty
+    , con `elem` falseData given =
+    return PFalse
+  | cls@(EqPred NomEq _ _) <- classifyPredType ty =
+    toPresburgerPredTree cls
+  | isEqPred ty = toPresburgerPredTree $ classifyPredType ty
+  | Just (con, [l, r]) <- splitTyConAppLastBin ty -- l ~ r
+    , con `elem` (tyEq given ++ tyEqBool given) =
+    toPresburgerPredTree $ EqPred NomEq l r
+  | Just (con, [_k, l, r]) <- splitTyConApp_maybe ty -- l (:~: {k}) r
+    , con `elem` tyEqWitness given =
+    toPresburgerPredTree $ EqPred NomEq l r
+  | Just (con, [l]) <- splitTyConApp_maybe ty -- Empty l => ...
+    , con `elem` isEmpty given =
+    Not <$> toPresburgerPred l
+  | Just (con, [l]) <- splitTyConApp_maybe ty -- IsTrue l =>
+    , con `elem` isTrue given =
+    toPresburgerPred l
+  | Just (con, [l]) <- splitTyConApp_maybe ty -- Not p (from Data.Type.Bool)
+    , con `elem` tyNot given =
+    Not <$> toPresburgerPred l
+  | Just (con, [l, r]) <- splitTyConApp_maybe ty -- p && q (from Data.Type.Bool)
+    , con `elem` tyAnd given =
+    (:&&) <$> toPresburgerPred l <*> toPresburgerPred r
+  | Just (con, [l, r]) <- splitTyConApp_maybe ty -- p || q (from Data.Type.Bool)
+    , con `elem` tyOr given =
+    (:||) <$> toPresburgerPred l <*> toPresburgerPred r
+  | Just (con, lastN 3 -> [p, t, f]) <- splitTyConApp_maybe ty -- If p t f (from Data.Type.Bool)
+    , con `elem` tyIf given = do
+    p' <- toPresburgerPred p
+    (:||) 
+      <$> ((p' :&&) <$> toPresburgerPred t) 
+      <*> ((Not p':&&) <$> toPresburgerPred f)
+  | Just (con, [t1, t2]) <- splitTyConAppLastBin ty
+    , typeKind t1 `eqType` typeNatKind
+    , typeKind t2 `eqType` typeNatKind 
+    , Just p <- lookup con binPropDic =
+      p <$> toPresburgerExp t1 <*> toPresburgerExp t2
+  | Just DataCond{..} <- parseOrdCond ty = do -- OrdCond
+      fromCondCases condCases
+          <$> toPresburgerExp lhs
+          <*> toPresburgerExp rhs
+  | otherwise = parsePred given toPresburgerExp ty
+
+splitTyConAppLastBin :: Type -> Maybe (TyCon, [Type])
+splitTyConAppLastBin t = do
+  (con, ts) <- splitTyConApp_maybe t
+  let !n = length ts
+  guard $ n >= 2
+  return (con, drop (n - 2) ts)
+
+data DataCond = DataCond { lhs, rhs :: Type, condCases :: CondCases }
+
+data CondCases = CondCases { ltCase, eqCase, gtCase :: Bool }
+  deriving (Show, Eq, Ord)
+
+fromCondCases :: CondCases -> Expr -> Expr -> Prop
+fromCondCases (CondCases True False False) = (:<)
+fromCondCases (CondCases False True False) = (:==)
+fromCondCases (CondCases False False True) = (:>)
+fromCondCases (CondCases True True False) = (:<=)
+fromCondCases (CondCases True False True) = (:/=)
+fromCondCases (CondCases True True True) = const $ const PTrue
+fromCondCases (CondCases False True True) = (:>=)
+fromCondCases (CondCases False False False) = const $ const PFalse
+
+parseOrdCond :: Given Translation => Type -> Maybe DataCond
+parseOrdCond ty = do
+  (con, lastN 4 -> [cmp, ltTy, eqTy, gtTy]) <- splitTyConApp_maybe ty
+  guard $ con `elem` ordCond given
+  (cmpCon, lastN 2 -> [lhs, rhs]) <- splitTyConApp_maybe  cmp
+  guard $ cmpCon `elem` natCompare given
+  ltCase <- decodeTyBool ltTy
+  eqCase <- decodeTyBool eqTy
+  gtCase <- decodeTyBool gtTy
+  let  condCases = CondCases{..}
+  pure DataCond{..}
+
+decodeTyBool :: Type -> Maybe Bool
+decodeTyBool ty = do
+  con <- tyConAppTyCon_maybe ty
+  (True <$ guard (con == promotedTrueDataCon))
+    <|> (False <$ guard (con == promotedFalseDataCon))
+
+
+toPresburgerPredTree :: Given Translation => PredTree -> Machine Prop
+toPresburgerPredTree (EqPred NomEq p false) -- P ~ 'False <=> Not P ~ 'True
+  | maybe False (`elem` falseData given) $ tyConAppTyCon_maybe false =
+    Not <$> toPresburgerPred p
+toPresburgerPredTree (EqPred NomEq p b) -- (n :<=? m) ~ 'b
+  | Just isTrue <- decodeTyBool b
+    , Just (con, [t1, t2]) <- splitTyConAppLastBin p
+    , con `elem` natLeqBool given =
+    if isTrue 
+      then (:<=) <$> toPresburgerExp t1 <*> toPresburgerExp t2
+       else (:>) <$> toPresburgerExp t1 <*> toPresburgerExp t2
+toPresburgerPredTree (EqPred NomEq p b) -- (n :<? m) ~ b
+  | Just isTrue <- decodeTyBool b
+    , Just (con, [t1, t2]) <- splitTyConAppLastBin p
+    , con `elem` natLtBool given =
+    if isTrue 
+      then (:<) <$> toPresburgerExp t1 <*> toPresburgerExp t2
+       else (:>=) <$> toPresburgerExp t1 <*> toPresburgerExp t2
+toPresburgerPredTree (EqPred NomEq p b) -- (n :>? m) ~ b
+  | Just isTrue <- decodeTyBool b
+    , Just (con, [t1, t2]) <- splitTyConAppLastBin p
+    , con `elem` natGtBool given =
+    if isTrue 
+      then (:>) <$> toPresburgerExp t1 <*> toPresburgerExp t2
+       else (:<=) <$> toPresburgerExp t1 <*> toPresburgerExp t2
+toPresburgerPredTree (EqPred NomEq p b) -- (n :>=? m) ~ b
+  | Just isTrue <- decodeTyBool b
+    , Just (con, [t1, t2]) <- splitTyConAppLastBin p
+    , con `elem` natGeqBool given =
+    if isTrue 
+      then (:>=) <$> toPresburgerExp t1 <*> toPresburgerExp t2
+       else (:<) <$> toPresburgerExp t1 <*> toPresburgerExp t2
+toPresburgerPredTree (EqPred NomEq p b) 
+  | maybe False (`elem` trueData given) $ tyConAppTyCon_maybe b =
+    toPresburgerPred p
+toPresburgerPredTree (EqPred NomEq b p) 
+  | maybe False (`elem` trueData given) $ tyConAppTyCon_maybe b =
+    toPresburgerPred p
+toPresburgerPredTree (EqPred NomEq p q) -- (p :: Bool) ~ (q :: Bool)
+  | typeKind p `eqType` mkTyConTy promotedBoolTyCon = do
+    lift $ lift $ tcPluginTrace "pres: EQBOOL:" $ ppr (p, q)
+    (<=>) <$> toPresburgerPred p
+      <*> toPresburgerPred q
+toPresburgerPredTree (EqPred NomEq n m) -- (n :: Nat) ~ (m :: Nat)
+  | typeKind n `eqType` typeNatKind =
+    (:==) <$> toPresburgerExp n
+      <*> toPresburgerExp m
+toPresburgerPredTree (EqPred _ t1 t2) -- CmpNat a b ~ CmpNat c d
+  | Just (con, lastTwo -> [a, b]) <- splitTyConAppLastBin t1
+    , Just (con', lastTwo -> [c, d]) <- splitTyConAppLastBin t2
+    , con `elem` natCompare given
+    , con' `elem` natCompare given =
+    (<=>) <$> ((:<) <$> toPresburgerExp a <*> toPresburgerExp b)
+      <*> ((:<) <$> toPresburgerExp c <*> toPresburgerExp d)
+toPresburgerPredTree (EqPred NomEq t1 t2) -- CmpNat a b ~ x
+  | Just (con, lastTwo -> [a, b]) <- splitTyConAppLastBin t1
+    , con `elem` natCompare given
+    , Just cmp <- tyConAppTyCon_maybe t2 =
+    MaybeT (return $ lookup cmp orderingDic)
+      <*> toPresburgerExp a
+      <*> toPresburgerExp b
+toPresburgerPredTree (EqPred NomEq t1 t2) -- x ~ CmpNat a b
+  | Just (con, lastTwo -> [a, b]) <- splitTyConAppLastBin t2
+    , con `elem` natCompare given
+    , Just cmp <- tyConAppTyCon_maybe t1 =
+    MaybeT (return $ lookup cmp orderingDic)
+      <*> toPresburgerExp a
+      <*> toPresburgerExp b
+toPresburgerPredTree (EqPred NomEq cond p) 
+  -- OrdCond (CmpNat _ _) lt eq gt ~ ? (for GHC >= 9.2)
+  | Just DataCond{..} <- parseOrdCond cond = do
+    body <- fromCondCases condCases
+          <$> toPresburgerExp lhs
+          <*> toPresburgerExp rhs
+    maybe ((body <=>) <$> toPresburgerPred p) 
+      (\q -> if q then pure body else pure $ Not body)
+      $ decodeTyBool p
+  -- ? ~ OrdCond (CmpNat _ _) lt eq gt  (for GHC >= 9.2)
+  | Just DataCond{..} <- parseOrdCond p = do
+    body <- fromCondCases condCases
+          <$> toPresburgerExp lhs
+          <*> toPresburgerExp rhs
+    maybe ((body <=>) <$> toPresburgerPred cond) 
+      (\q -> if q then pure body else pure $ Not body)
+      $ decodeTyBool cond
+toPresburgerPredTree (ClassPred con ts)
+  -- (n :: Nat) (<=| < | > | >= | == | /=) (m :: Nat)
+  | [t1, t2] <- lastN 2 ts
+    , typeKind t1 `eqType` typeNatKind
+    , typeKind t2 `eqType` typeNatKind =
+    let p = lookup (classTyCon con) binPropDic
+     in MaybeT (return p) <*> toPresburgerExp t1 <*> toPresburgerExp t2
+toPresburgerPredTree _ = mzero
+
+binPropDic :: Given Translation => [(TyCon, Expr -> Expr -> Prop)]
+binPropDic =
+  [(n, (:<)) | n <- natLt given ++ natLtBool given]
+  ++ [(n, (:>)) | n <- natGt given ++ natGtBool given]
+    ++ [(n, (:<=)) | n <- natLeq given ++ natLeqBool given]
+    ++ [(n, (:>=)) | n <- natGeq given ++ natGeqBool given]
+    ++ [(n, (:==)) | n <- tyEq given ++ tyEqBool given]
+    ++ [(n, (:/=)) | n <- tyNeqBool given]
+    ++ [(n, (:==)) | n <- tyEqBool given]
+
+toPresburgerExp :: Given Translation => Type -> Machine Expr
+toPresburgerExp ty = case ty of
+  TyVarTy t -> return $ Var $ toName $ getKey $ getUnique t
+  TyConApp tc (lastN 3 -> [p, t, f])
+    | tc `elem` tyIf given ->
+      If <$> toPresburgerPred p <*> toPresburgerExp t <*> toPresburgerExp f 
+  TyConApp tc (lastN 4 -> [cmpNM, l, e, g])
+    | tc `elem` ordCond given
+    , TyConApp cmp (lastN 2 -> [n, m]) <- cmpNM
+    , cmp `elem` natCompare given
+    , all ((`elem` [TypeEq n, TypeEq m]) . TypeEq) [l,e,g]
+    -> decodeMinMax n m l e g
+  t@(TyConApp tc ts) ->
+    parseExpr given toPresburgerExp ty
+      <|> body tc ts
+      <|> Var . toName . getKey . getUnique <$> toVar t
+  LitTy (NumTyLit n) -> return (K n)
+  LitTy _ -> mzero
+  t ->
+    parseExpr given toPresburgerExp ty
+      <|> Var . toName . getKey . getUnique <$> toVar t
+  where
+    body tc ts =
+      let step con op
+            | tc == con
+              , [tl, tr] <- lastTwo ts =
+              op <$> toPresburgerExp tl <*> toPresburgerExp tr
+            | otherwise = mzero
+       in case ts of
+            [tl, tr] | tc `elem` natTimes given ->
+              case (simpleExp tl, simpleExp tr) of
+                (LitTy (NumTyLit n), LitTy (NumTyLit m)) -> return $ K $ n * m
+                (LitTy (NumTyLit n), x) -> (:*) n <$> toPresburgerExp x
+                (x, LitTy (NumTyLit n)) -> (:*) n <$> toPresburgerExp x
+                _ -> mzero
+            _ ->
+              asum $
+                [ step con (:+)
+                | con <- natPlus given
+                ]
+                  ++ [ step con (:-)
+                     | con <- natMinus given
+                     ]
+                  ++ [ step con Min
+                     | con <- natMin given
+                     ]
+                  ++ [ step con Max
+                     | con <- natMin given
+                     ]
+
+decodeMinMax :: Given Translation => Type -> Type -> Type -> Type -> Type -> Machine Expr
+decodeMinMax n m lt eq gt 
+  | lt `eqType`  n && eq `eqType`  n && gt `eqType` m = 
+    Min <$> toPresburgerExp n <*> toPresburgerExp m
+  | lt `eqType`  n && eq `eqType`  m && gt `eqType` m = 
+    Min <$> toPresburgerExp n <*> toPresburgerExp m
+  | lt `eqType` m && eq `eqType`  m && gt `eqType` n = 
+    Max <$> toPresburgerExp n <*> toPresburgerExp m
+  | lt `eqType` m && eq `eqType`  n && gt `eqType` n = 
+    Max <$> toPresburgerExp n <*> toPresburgerExp m
+  | otherwise = mzero
+
+-- simplTypeCmp :: Type -> Type
+
+lastTwo :: [a] -> [a]
+lastTwo = drop <$> subtract 2 . length <*> id
+lastN :: Int -> [a] -> [a]
+lastN n = drop <$> subtract n . length <*> id
+
+simpleExp :: Given Translation => Type -> Type
+simpleExp (AppTy t1 t2) = AppTy (simpleExp t1) (simpleExp t2)
+simpleExp (FunTy f m t1 t2) = FunTy f m (simpleExp t1) (simpleExp t2)
+simpleExp (ForAllTy t1 t2) = ForAllTy t1 (simpleExp t2)
+simpleExp (TyConApp tc (lastTwo -> ts)) =
+  fromMaybe (TyConApp tc (map simpleExp ts)) $
+    asum
+      ( map simpler $
+          [(c, (+)) | c <- natPlus given]
+          ++ [(c, (-)) | c <- natMinus given]
+            ++ [(c, (*)) | c <- natTimes given]
+            ++ [(c, (^)) | c <- natExp given]
+      )
+  where
+    simpler (con, op)
+      | con == tc
+        , [tl, tr] <- map simpleExp ts =
+        Just $
+          case (tl, tr) of
+            (LitTy (NumTyLit n), LitTy (NumTyLit m)) -> LitTy (NumTyLit (op n m))
+            _ -> TyConApp con [tl, tr]
+      | otherwise = Nothing
+simpleExp t = t
+
+type ParseEnv = M.Map TypeEq TyVar
+
+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) -> do
+    loc <- unsafeTcPluginTcM $ getCtLocM (Shouldn'tHappenOrigin "runMachine dummy wanted") Nothing
+    newWanted loc $ mkPrimEqPredRole Nominal (mkTyVarTy var) ty
+  return ma
+
+toVar :: Type -> Machine TyVar
+toVar ty =
+  gets (M.lookup (TypeEq ty)) >>= \case
+    Just v -> return v
+    Nothing -> do
+      v <- lift $ lift $ newFlexiTyVar $ typeKind ty
+      modify $ M.insert (TypeEq ty) v
+      return v
diff --git a/test/ErrorsNoPlugin.hs b/test/ErrorsNoPlugin.hs
new file mode 100644
--- /dev/null
+++ b/test/ErrorsNoPlugin.hs
@@ -0,0 +1,18 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# OPTIONS_GHC -fdefer-type-errors #-}
+
+module ErrorsNoPlugin where
+
+import Shared
+
+zipMVec :: Vec n a -> Vec n b -> Vec n (a, b)
+zipMVec Nil Nil = Nil
+zipMVec zs@(a :- as) (b :- bs) = (a, b) :- zipMVec zs bs
+
+spin :: Vec n a -> Vec n a -> ()
+spin _ _ = ()
+
+unSpin :: Vec n a -> ()
+unSpin Nil = ()
+unSpin zs@(_ :- ws) = spin zs ws
diff --git a/test/ErrorsWithPlugin.hs b/test/ErrorsWithPlugin.hs
new file mode 100644
--- /dev/null
+++ b/test/ErrorsWithPlugin.hs
@@ -0,0 +1,19 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# OPTIONS_GHC -fdefer-type-errors #-}
+{-# OPTIONS_GHC -fplugin GHC.TypeLits.Presburger #-}
+
+module ErrorsWithPlugin where
+
+import Shared
+
+zipMVec :: Vec n a -> Vec n b -> Vec n (a, b)
+zipMVec Nil Nil = Nil
+zipMVec zs@(a :- as) (b :- bs) = (a, b) :- zipMVec zs bs
+
+spin :: Vec n a -> Vec n a -> ()
+spin _ _ = ()
+
+unSpin :: Vec n a -> ()
+unSpin Nil = ()
+unSpin zs@(_ :- ws) = spin zs ws
diff --git a/test/GHC/TypeLits/PresburgerSpec.hs b/test/GHC/TypeLits/PresburgerSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/GHC/TypeLits/PresburgerSpec.hs
@@ -0,0 +1,70 @@
+{-# LANGUAGE OverloadedStrings #-}
+
+module GHC.TypeLits.PresburgerSpec where
+
+import Control.Exception (evaluate, try)
+import Control.Exception.Base (TypeError (TypeError))
+import Control.Monad (void)
+import qualified Data.Text as T
+import qualified ErrorsNoPlugin as NoPlugin
+import qualified ErrorsWithPlugin as Plugin
+import Shared
+import Test.Tasty (TestTree, testGroup)
+import Test.Tasty.HUnit (assertFailure, testCase)
+
+test_recursiveContradiction :: TestTree
+test_recursiveContradiction =
+  testGroup
+    "n ~ n + 1 in recursive call should be rejected as type error"
+    [ testCase "Without plugin" $ do
+        eith <- try $ void (evaluate $ NoPlugin.zipMVec (True :- Nil) (() :- Nil))
+        case eith of
+          Left (TypeError msg)
+            | any (`T.isInfixOf` T.pack msg)
+              [ "Could not deduce: (n GHC.TypeNats.+ 1) ~ n"
+              , "Could not deduce ((n GHC.TypeNats.+ 1) ~ n)"
+              , "Could not deduce ‘(n GHC.TypeNats.+ 1) ~ n’"
+              , "[GHC-25897]"
+              ]
+              -> pure ()
+          _ -> assertFailure $ "TypeError with mismatch expected, but got: " <> show eith
+    , testCase "With plugin" $ do
+        eith <- try $ void (evaluate $ Plugin.zipMVec (True :- Nil) (() :- Nil))
+        case eith of
+          Left (TypeError msg)
+            | any (`T.isInfixOf` T.pack msg)
+              [ "Could not deduce: (n GHC.TypeNats.+ 1) ~ n"
+              , "Could not deduce ((n GHC.TypeNats.+ 1) ~ n)"
+              , "Could not deduce ‘(n GHC.TypeNats.+ 1) ~ n’"
+              , "[GHC-25897]"
+              ] -> pure ()
+          _ -> assertFailure $ "TypeError with mismatch expected, but got: " <> show eith
+    ]
+
+test_nonrecursiveContradiction :: TestTree
+test_nonrecursiveContradiction =
+  testGroup
+    "n ~ n + 1 in non-recursive call should be rejected as type error"
+    [ testCase "Without plugin" $ do
+        eith <- try $ void (evaluate $ NoPlugin.unSpin (True :- Nil))
+        case eith of
+          Left (TypeError msg)
+            | any (`T.isInfixOf` T.pack msg )
+              [ "Could not deduce: n1 ~ n"
+              , "Could not deduce (n1 ~ n)"
+              , "Could not deduce ‘n1 ~ n’"
+              ]
+              -> pure ()
+          _ -> assertFailure $ "TypeError with mismatch expected, but got: " <> show eith
+    , testCase "With plugin" $ do
+        eith <- try $ void (evaluate $ Plugin.unSpin (True :- Nil))
+        case eith of
+          Left (TypeError msg)
+            | any (`T.isInfixOf` T.pack msg )
+              [ "Could not deduce: n1 ~ n"
+              , "Could not deduce (n1 ~ n)"
+              , "Could not deduce ‘n1 ~ n’"
+              ]
+              -> pure ()
+          _ -> assertFailure $ "TypeError with mismatch expected, but got: " <> show eith
+    ]
diff --git a/test/Shared.hs b/test/Shared.hs
new file mode 100644
--- /dev/null
+++ b/test/Shared.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE TypeOperators #-}
+
+module Shared (Vec (..)) where
+
+import GHC.TypeNats (Nat, type (+))
+
+data Vec (n :: Nat) a where
+  Nil :: Vec 0 a
+  (:-) :: a -> Vec n a -> Vec (n + 1) a
+
+infixr 9 :-
diff --git a/test/test.hs b/test/test.hs
new file mode 100644
--- /dev/null
+++ b/test/test.hs
@@ -0,0 +1,1 @@
+{-# OPTIONS_GHC -F -pgmF tasty-discover #-}