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,80 @@
+{-# LANGUAGE CPP, DataKinds, EmptyCase, FlexibleContexts, GADTs, LambdaCase #-}
+{-# LANGUAGE PolyKinds, ScopedTypeVariables, TypeFamilies, TypeInType       #-}
+{-# LANGUAGE TypeOperators, UndecidableInstances                            #-}
+{-# OPTIONS_GHC -dcore-lint #-}
+{-# OPTIONS_GHC -fplugin GHC.TypeLits.Presburger #-}
+
+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 806
+{-# LANGUAGE NoStarIsType #-}
+#endif
+
+module Main where
+import Data.Proxy
+import Data.Type.Equality
+import GHC.TypeLits
+import Proof.Propositional (Empty (..), withEmpty)
+import Proof.Propositional (IsTrue (Witness))
+
+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 {}
+
+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ > 802
+hoge :: proxy n -> IsTrue (n + 1 <=? n) -> a
+hoge _ Witness = absurdTrueFalse Refl
+#endif
+
+bar :: ((2 * (n + 1)) ~ ((2 * n) + 2)) => proxy n -> ()
+bar _ = ()
+
+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
+
+predSucc :: forall proxy n. Empty (n <=! 0) => proxy n -> IsTrue (n + 1 <=? 2 * n)
+predSucc _ = 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
+
+main :: IO ()
+main = putStrLn "finished"
diff --git a/examples/simple-arith.hs b/examples/simple-arith.hs
deleted file mode 100644
--- a/examples/simple-arith.hs
+++ /dev/null
@@ -1,77 +0,0 @@
-{-# LANGUAGE DataKinds, TypeOperators, GADTs, TypeFamilies, ExplicitForAll, FlexibleContexts #-}
-{-# LANGUAGE ScopedTypeVariables, CPP #-}
-#if !MIN_VERSION_singletons(2,4,1)
-{-# LANGUAGE KindSignatures #-}
-#endif
-{-# OPTIONS_GHC -fplugin GHC.TypeLits.Presburger #-}
-module Main where
-import Data.Type.Equality
-import GHC.TypeLits       (Nat, type (<=?), CmpNat)
-import Proof.Propositional (Empty(..))
-import Proof.Propositional (IsTrue(Witness))
-import Data.Singletons.Prelude
-import Data.Singletons.Prelude.List
-
-#if !MIN_VERSION_singletons(2,4,1)
-import qualified Data.Singletons.Prelude as Sing
-type n <= m = (n :: Nat) Sing.:<= (m :: Nat)
-infix 4 <=
-type n - m = (n :: Nat) Sing.:- (m :: Nat)
-infixl 6 -
-type n + m = (n :: Nat) Sing.:+ (m :: Nat)
-infixl 6 +
-type n * m = (n :: Nat) Sing.:* (m :: Nat)
-infixl 7 *
-#endif
-
-type n <=! m = IsTrue (n <=? m)
-infix 4 <=!
-
-natLen :: (Length xs <= Length ys) ~ 'True
-       => proxy xs -> proxy ys -> Length ys - Length xs + Length xs :~: Length ys
-natLen _ _ = Refl
-
-natLeqZero' :: ((n <= 0) ~ 'True) => proxy n -> n :~: 0
-natLeqZero' _ = Refl
-
-plusLeq :: (n <= m) ~ 'True => proxy (n :: Nat) -> proxy m -> ((m - n) + n :~: m)
-plusLeq _ _ = Refl
-
-(%:<=?) :: Sing n -> Sing m -> Sing (n <=? m)
-n %:<=? m = case sCompare n m of
-  SLT -> STrue
-  SEQ -> STrue
-  SGT -> SFalse
-
-hoge :: ((n + 1 <=? n) ~ 'False) => proxy n -> ()
-hoge _ = ()
-
-hoge' :: (((n + 1) <= n) ~ 'False) => proxy n -> ()
-hoge' _ = ()
-
-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,61 +1,80 @@
-name:                ghc-typelits-presburger
-version:             0.2.0.5
-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
-                  
-homepage:            https://github.com/konn/ghc-typelits-presburger#readme
-license:             BSD3
-license-file:        LICENSE
-author:              Hiromi ISHII
-maintainer:          konn.jinro _at_ gmail.com
-copyright:           2015 (c) Hiromi ISHII
-category:            Math, Type System
-build-type:          Simple
--- extra-source-files:
-cabal-version:       >=1.10
-tested-with:         GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.3
-
-flag examples
-    Default: False
+cabal-version: 1.12
 
-library
-  ghc-options:         -Wall -Wno-dodgy-imports
-  hs-source-dirs:      src
-                     , presburger/src
-  exposed-modules:     GHC.TypeLits.Presburger
-  other-modules:       GHC.Compat
-                       Data.Integer.SAT
-  build-depends:       base                 >= 4.7  && < 5
-                     , ghc                  >= 7.10 && < 8.5
-                     , ghc-tcplugins-extra  >= 0.2  && < 0.4
-                     , equational-reasoning >= 0.4.0.0
-                     , singletons
-                     , transformers
-                     , mtl
-                     , containers
-                     , pretty
-                     , syb
-                     , reflection
-  default-language:    Haskell2010
+-- This file has been generated from package.yaml by hpack version 0.31.2.
+--
+-- see: https://github.com/sol/hpack
+--
+-- hash: 213617ccefa67bad574a0687988e14cef38a75e07ac2e08140bcda55feeee3f6
 
-executable simple-arith
-  if flag(examples)
-    buildable:         True
-  else
-    buildable:         False
-  hs-source-dirs:      examples
-  Main-is:             simple-arith.hs
-  build-depends:       base
-                     , ghc-typelits-presburger
-                     , equational-reasoning
-                     , singletons
-  default-language:    Haskell2010
-  ghc-options:         -Wall -Wno-dodgy-imports -Wno-unused-imports
+name:           ghc-typelits-presburger
+version:        0.3.0.0
+synopsis:       Presburger Arithmetic Solver for GHC Type-level natural numbers.
+description:    @ghc-typelits-presburger@ augments GHC type-system with Presburger
+                Arithmetic Solver for Type-level natural numbers.
+                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
+maintainer:     konn.jinro _at_ gmail.com
+copyright:      2015 (c) Hiromi ISHII
+license:        BSD3
+license-file:   LICENSE
+tested-with:    GHC==8.4.3 GHC==8.6.3 GHC==8.8.2
+build-type:     Simple
 
 source-repository head
-  type:     git
+  type: git
   location: https://github.com/konn/ghc-typelits-presburger
+
+flag examples
+  description: Builds example
+  manual: False
+  default: False
+
+library
+  exposed-modules:
+      GHC.TypeLits.Presburger.Types
+      GHC.TypeLits.Presburger
+      GHC.TypeLits.Presburger.Compat
+  other-modules:
+      Data.Integer.SAT
+      Paths_ghc_typelits_presburger
+  hs-source-dirs:
+      src
+  ghc-options: -Wall -Wno-dodgy-imports
+  build-depends:
+      base >=4.7 && <5
+    , containers
+    , ghc >=7.10 && <8.11
+    , ghc-tcplugins-extra >=0.2 && <0.4
+    , mtl
+    , pretty
+    , reflection
+    , syb
+    , transformers
+  default-language: Haskell2010
+
+executable simple-arith-core
+  main-is: simple-arith-core.hs
+  other-modules:
+      Paths_ghc_typelits_presburger
+  hs-source-dirs:
+      examples
+  ghc-options: -Wall -Wno-dodgy-imports -Wno-unused-imports
+  build-depends:
+      base
+    , equational-reasoning
+    , ghc-typelits-presburger
+  if !(flag(examples))
+    buildable: False
+  default-language: Haskell2010
diff --git a/presburger/src/Data/Integer/SAT.hs b/presburger/src/Data/Integer/SAT.hs
deleted file mode 100644
--- a/presburger/src/Data/Integer/SAT.hs
+++ /dev/null
@@ -1,981 +0,0 @@
-{-# LANGUAGE BangPatterns, PatternGuards, Trustworthy #-}
-{-|
-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 Debug.Trace
-
-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           Prelude             hiding ((<>))
-import           Text.PrettyPrint
-
-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)
-
--- | The type of integer expressions.
--- Variable names must be non-negative.
-data Expr = Expr :+ Expr          -- ^ Addition
-          | Expr :- Expr          -- ^ Subtraction
-          | Integer :* Expr       -- ^ Multiplication by a constant
-          | Negate Expr           -- ^ Negation
-          | Var Name              -- ^ Variable
-          | K Integer             -- ^ Constant
-          | If Prop Expr Expr     -- ^ A conditional expression
-          | Div Expr Integer      -- ^ Division, rounds down
-          | Mod Expr Integer      -- ^ Non-negative remainder
-            deriving (Read,Show)
-
-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 (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      = Bound Integer Term  -- ^ The integer is strictly positive
-                  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
-               -- -XC*x + S < 0
-               -- S < XC*x
-               then 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 ]
-               -- XC*x + S < 0
-               -- XC*x < -S
-               else 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
-  return a           = One a
-  fail _             = None
-  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  = return
-  (<*>) = ap
-
-
-newtype S a = S (RW -> Answer (a,RW))
-
-instance Monad S where
-  return a      = S $ \s -> return (a,s)
-  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  = return
-  (<*>) = 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.foldWithKey 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/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,980 @@
+{-# LANGUAGE BangPatterns, CPP, PatternGuards, 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           Prelude             hiding ((<>))
+import           Text.PrettyPrint
+
+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 = Expr :+ Expr          -- ^ Addition
+          | Expr :- Expr          -- ^ Subtraction
+          | Integer :* Expr       -- ^ Multiplication by a constant
+          | Negate Expr           -- ^ Negation
+          | Var Name              -- ^ Variable
+          | K Integer             -- ^ Constant
+          | If Prop Expr Expr     -- ^ A conditional expression
+          | Div Expr Integer      -- ^ Division, rounds down
+          | Mod Expr Integer      -- ^ Non-negative remainder
+            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 (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      = Bound Integer Term  -- ^ The integer is strictly positive
+                  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
+               -- -XC*x + S < 0
+               -- S < XC*x
+               then 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 ]
+               -- XC*x + S < 0
+               -- XC*x < -S
+               else 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
+  return a           = One a
+#if !MIN_VERSION_ghc(8,8,1)
+  fail _             = None
+#endif
+  None >>= _         = None
+  One a >>= k        = k a
+  Choice m1 m2 >>= k = mplus (m1 >>= k) (m2 >>= k)
+
+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  = return
+  (<*>) = ap
+
+
+newtype S a = S (RW -> Answer (a,RW))
+
+instance Monad S where
+  return a      = S $ \s -> return (a,s)
+  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  = return
+  (<*>) = 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,121 +0,0 @@
-{-# LANGUAGE CPP, FlexibleInstances, PatternGuards, PatternSynonyms #-}
-{-# LANGUAGE TypeSynonymInstances, ViewPatterns                     #-}
-{-# OPTIONS_GHC -Wno-orphans #-}
-module GHC.Compat (module GHC.Compat) where
-import Data.Function       (on)
-import FamInst             as GHC.Compat
-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 (typeNatKind)
-import Module              as GHC.Compat (ModuleName, mkModuleName)
-import OccName             as GHC.Compat (emptyOccSet, mkInstTyTcOcc)
-import Plugins             as GHC.Compat (Plugin (..), defaultPlugin)
-import TcEvidence          as GHC.Compat (EvTerm)
-import TcHsType            as GHC.Compat (tcInferApps)
-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 TcType              as GHC.Compat (tcTyFamInsts)
-import TcTypeNats          as GHC.Compat
-import TyCon               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           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 Data.Generics.Twins
-import TcPluginM           (lookupOrig)
-import TyCoRep             ()
-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]
-
-newtype TypeEq = TypeEq { runTypeEq :: Type }
-
-instance Eq TypeEq where
-  (==) = geq `on` runTypeEq
-
-instance Ord TypeEq where
-  compare = gcompare `on` runTypeEq
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,389 +1,10 @@
-{-# LANGUAGE CPP, DataKinds, FlexibleContexts, FlexibleInstances      #-}
-{-# LANGUAGE LambdaCase, MultiWayIf, OverloadedStrings, PatternGuards #-}
-{-# LANGUAGE RankNTypes, RecordWildCards, TypeOperators               #-}
-{-# LANGUAGE TypeSynonymInstances                                     #-}
-{-# OPTIONS_GHC -Wno-unused-imports #-}
+-- | Provides a plain Presburger solver plugin for @'GHC.TypeNats.Nat'@.
+--
+--   For an interface for extension, see
+--   "GHC.TypeLits.Presburger.Types".
 module GHC.TypeLits.Presburger (plugin) where
-import GHC.Compat
-
-import           Class                     (Class, classTyCon)
-import           Control.Applicative       ((<|>))
-import           Control.Monad             (forM_, mzero)
-import           Control.Monad.State.Class
-import           Control.Monad.Trans.Class
-import           Control.Monad.Trans.Maybe (MaybeT (..))
-import           Control.Monad.Trans.State (StateT, runStateT)
-import           Data.Foldable             (asum)
-import           Data.Integer.SAT          (Expr (..), Prop (..), PropSet,
-                                            assert)
-import           Data.Integer.SAT          (checkSat, noProps, toName)
-import qualified Data.Integer.SAT          as SAT
-import           Data.List                 (nub)
-import qualified Data.Map.Strict           as M
-import qualified Data.Map.Strict           as M
-import           Data.Maybe                (catMaybes, fromJust)
-import           Data.Maybe                (fromMaybe, isNothing, mapMaybe)
-import           Data.Reflection           (Given, give, given)
-import           GHC.TypeLits              (Nat)
-import           Outputable                (showSDocUnsafe)
-import           TcPluginM                 (getFamInstEnvs, lookupOrig,
-                                            matchFam, newFlexiTyVar, newWanted,
-                                            tcLookupClass, unsafeTcPluginTcM)
-import           TcRnTypes
-import           TyCoRep                   (Coercion (..), KindCoercion (..))
-import           Type                      (mkPrimEqPredRole, mkTyVarTy,
-                                            splitTyConApp)
-import           TysWiredIn                (promotedEQDataCon,
-                                            promotedGTDataCon,
-                                            promotedLTDataCon)
-import           Var
-
-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 (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.Types
+import GhcPlugins
 
 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
-                    , typeLeqBoolTyCon_   :: TyCon
-                    , singCompareCon_     :: TyCon
-                    , caseNameForSingLeq_ :: TyCon
-                    , caseNameForSingGeq_ :: TyCon
-                    , caseNameForSingLt_  :: TyCon
-                    , caseNameForSingGt_  :: TyCon
-                    }
-caseNameForSingLeq :: Given MyEnv => TyCon
-caseNameForSingLeq = caseNameForSingLeq_ given
-caseNameForSingGeq :: Given MyEnv => TyCon
-caseNameForSingGeq = caseNameForSingGeq_ given
-caseNameForSingLt  :: Given MyEnv => TyCon
-caseNameForSingLt = caseNameForSingLt_ given
-caseNameForSingGt  :: Given MyEnv => TyCon
-caseNameForSingGt = caseNameForSingGt_ given
-
-eqTyCon :: Given MyEnv => TyCon
-eqTyCon = eqTyCon_ given
-
-eqWitnessTyCon :: Given MyEnv => TyCon
-eqWitnessTyCon = eqWitCon_ given
-
-isTrueTyCon :: Given MyEnv => TyCon
-isTrueTyCon = isTrueCon_ given
-
-typeLeqBoolTyCon :: Given MyEnv => TyCon
-typeLeqBoolTyCon = typeLeqBoolTyCon_ given
-
-singCompareCon :: Given MyEnv => TyCon
-singCompareCon = singCompareCon_ 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
-    ngs <- mapM (\a -> runMachine $ (,) a <$> toPresburgerPred subst (deconsPred a)) gs
-    let givens = catMaybes ngs
-        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 . genSubst) emptyTvSubst (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
-  (prems, wants) <- do
-    wants <- catMaybes <$>
-             mapM
-             (\ct -> runMachine $ (,) ct <$> toPresburgerPred subst (substTy subst $ deconsPred ct))
-             (filter (isWanted . ctEvidence) ws)
-    resls <- mapM (runMachine . toPresburgerPred subst . substTy subst . deconsPred)
-                     (gs ++ ds)
-    let prems = foldr assert' noProps $ catMaybes resls
-    return (prems, wants)
-  let 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 ((:&&) . snd) PTrue 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")
-  emptyClsTyCon <- classTyCon <$> (tcLookupClass =<< lookupOrig emd (mkTcOcc "Empty"))
-  eqTyCon_ <- getEqTyCon
-  eqWitCon_ <- getEqWitnessTyCon
-  pmd <- lookupModule (mkModuleName "Proof.Propositional") (fsLit "equational-reasoning")
-  isTrueCon_ <- tcLookupTyCon =<< lookupOrig pmd (mkTcOcc "IsTrue")
-  vmd <- lookupModule (mkModuleName "Data.Void") (fsLit "base")
-  voidTyCon <- tcLookupTyCon =<< lookupOrig vmd (mkTcOcc "Void")
-  singletons <- lookupModule (mkModuleName "Data.Singletons.Prelude.Ord") (fsLit "singletons")
-#if MIN_VERSION_singletons(2,4,1)
-  typeLeqBoolTyCon_ <- tcLookupTyCon =<< lookupOrig singletons (mkTcOcc "<=")
-  typeLtBoolTyCon_ <- tcLookupTyCon =<< lookupOrig singletons (mkTcOcc "<")
-  typeGeqBoolTyCon_ <- tcLookupTyCon =<< lookupOrig singletons (mkTcOcc ">=")
-  typeGtBoolTyCon_ <- tcLookupTyCon =<< lookupOrig singletons (mkTcOcc ">")
-#else
-  typeLeqBoolTyCon_ <- tcLookupTyCon =<< lookupOrig singletons (mkTcOcc ":<=")
-  typeLtBoolTyCon_ <- tcLookupTyCon =<< lookupOrig singletons (mkTcOcc ":<")
-  typeGeqBoolTyCon_ <- tcLookupTyCon =<< lookupOrig singletons (mkTcOcc ":>=")
-  typeGtBoolTyCon_ <- tcLookupTyCon =<< lookupOrig singletons (mkTcOcc ":>")
-#endif
-  caseNameForSingLeq_ <- getCaseNameForSingletonOp typeLeqBoolTyCon_
-  caseNameForSingLt_ <- getCaseNameForSingletonOp typeLtBoolTyCon_
-  caseNameForSingGeq_ <- getCaseNameForSingletonOp typeGeqBoolTyCon_
-  caseNameForSingGt_ <- getCaseNameForSingletonOp typeGtBoolTyCon_
-  singCompareCon_ <- tcLookupTyCon =<< lookupOrig singletons (mkTcOcc "Compare")
-  give MyEnv{..} act
-
-getCaseNameForSingletonOp :: TyCon -> TcPluginM TyCon
-getCaseNameForSingletonOp con = do
-  let vars = [typeNatKind, LitTy (NumTyLit 0), LitTy (NumTyLit 0)]
-  Just (appTy0, [n,b,bdy,r]) <- fmap (splitTyConApp . snd) <$> matchFam  con vars
-  let (appTy, args) = splitTyConApp bdy
-  Just innermost <- fmap snd <$> matchFam appTy args
-  Just (_, dat) <- matchFam appTy0 [n,b,innermost,r]
-  Just dat' <- fmap snd <$> uncurry matchFam (splitTyConApp dat)
-  return $ fst $ splitTyConApp dat'
-
-(<=>) :: 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 -> Machine 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 = mzero
-
-boolLeqs :: Given MyEnv => [TyCon]
-boolLeqs = [typeNatLeqTyCon, typeLeqBoolTyCon]
-
-toPresburgerPredTree :: Given MyEnv => TvSubst -> PredTree -> Machine 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 `elem` boolLeqs = (:<=) <$> toPresburgerExp subst t1  <*> toPresburgerExp subst t2
-  | Just promotedTrueDataCon  == tyConAppTyCon_maybe (substTy subst b) -- Singleton's <=...
-  , Just (con, [_,_,_,_,cmpTy]) <- splitTyConApp_maybe p
-  , con == caseNameForSingLeq
-  , Just (cmp, [l, r]) <- splitTyConApp_maybe cmpTy
-  , cmp `elem` [singCompareCon, typeNatCmpTyCon] =
-    (:<=) <$> toPresburgerExp subst l <*> toPresburgerExp subst r
-  | Just promotedTrueDataCon  == tyConAppTyCon_maybe (substTy subst b) -- Singleton's <...
-  , Just (con, [_,_,_,_,cmpTy]) <- splitTyConApp_maybe p
-  , con == caseNameForSingLt
-  , Just (cmp, [l, r]) <- splitTyConApp_maybe cmpTy
-  , cmp `elem` [singCompareCon, typeNatCmpTyCon] =
-    (:<) <$> toPresburgerExp subst l <*> toPresburgerExp subst r
-  | Just promotedTrueDataCon  == tyConAppTyCon_maybe (substTy subst b) -- Singleton's >=...
-  , Just (con, [_,_,_,_,cmpTy]) <- splitTyConApp_maybe p
-  , con == caseNameForSingGeq
-  , Just (cmp, [l, r]) <- splitTyConApp_maybe cmpTy
-  , cmp `elem` [singCompareCon, typeNatCmpTyCon] =
-    (:>=) <$> toPresburgerExp subst l <*> toPresburgerExp subst r
-  | Just promotedTrueDataCon  == tyConAppTyCon_maybe (substTy subst b) -- Singleton's >=...
-  , Just (con, [_,_,_,_,cmpTy]) <- splitTyConApp_maybe p
-  , con == caseNameForSingGt
-  , Just (cmp, [l, r]) <- splitTyConApp_maybe cmpTy
-  , cmp `elem` [singCompareCon, typeNatCmpTyCon] =
-    (:>) <$> toPresburgerExp subst l <*> toPresburgerExp subst r
-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 `elem` [singCompareCon, typeNatCmpTyCon], con' `elem` [typeNatCmpTyCon, singCompareCon]
-  = (<=>) <$> ((:<) <$> 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 `elem` [typeNatCmpTyCon, singCompareCon]
-  , Just cmp <- tyConAppTyCon_maybe (substTy subst t2) =
-    let dic = [(promotedLTDataCon, (:<))
-              ,(promotedEQDataCon, (:==))
-              ,(promotedGTDataCon, (:>))
-              ]
-    in MaybeT (return $ 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 `elem` [singCompareCon, typeNatCmpTyCon]
-  , Just cmp <- tyConAppTyCon_maybe (substTy subst t1) =
-    let dic = [(promotedLTDataCon, (:<))
-              ,(promotedEQDataCon, (:==))
-              ,(promotedGTDataCon, (:>))
-              ]
-    in MaybeT (return $ 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 _ _ = mzero
-
-toPresburgerExp :: TvSubst -> Type -> Machine Expr
-toPresburgerExp dic ty = case substTy dic ty of
-  TyVarTy t          -> return $ Var $ toName $ getKey $ getUnique t
-  t@(TyConApp tc ts) -> body tc ts <|> Var . toName . getKey . getUnique <$> toVar t
-  LitTy (NumTyLit n) -> return (K n)
-  LitTy _            -> mzero
-  t                  -> Var . toName . getKey .getUnique <$> toVar t
-  where
-    body tc ts =
-      let step con op
-            | tc == con, [tl, tr] <- ts =
-              op <$> toPresburgerExp dic tl <*> toPresburgerExp dic tr
-            | otherwise = mzero
-      in case ts of
-        [tl, tr] | tc == typeNatMulTyCon ->
-          case (simpleExp tl, simpleExp tr) of
-            (LitTy (NumTyLit n), LitTy (NumTyLit m)) -> return $ K $ n * m
-            (LitTy (NumTyLit n), x) -> (:*) <$> pure n <*> toPresburgerExp dic x
-            (x, LitTy (NumTyLit n)) -> (:*) <$> pure n <*> toPresburgerExp dic x
-            _ -> mzero
-        _ ->  asum [ step con op
-                   | (con, op) <- [(typeNatAddTyCon, (:+)), (typeNatSubTyCon, (:-))]]
-
--- 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
-
-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) ->
-    newWanted undefined $ 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
+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,194 @@
+{-# LANGUAGE CPP, FlexibleInstances, PatternGuards, PatternSynonyms #-}
+{-# LANGUAGE TypeSynonymInstances, ViewPatterns                     #-}
+{-# OPTIONS_GHC -Wno-orphans #-}
+module GHC.TypeLits.Presburger.Compat (module GHC.TypeLits.Presburger.Compat) where
+import Data.Function       (on)
+import FamInst             as GHC.TypeLits.Presburger.Compat
+import FastString          as GHC.TypeLits.Presburger.Compat (fsLit)
+import GHC.TcPluginM.Extra as GHC.TypeLits.Presburger.Compat (evByFiat, lookupModule, lookupName,
+                                          tracePlugin)
+import GhcPlugins          as GHC.TypeLits.Presburger.Compat (EqRel (..), PredTree (..))
+import GhcPlugins          as GHC.TypeLits.Presburger.Compat (classifyPredType, isEqPred,
+                                          lookupTyCon, mkTyConTy)
+import GhcPlugins          as GHC.TypeLits.Presburger.Compat (mkTcOcc, ppr, promotedFalseDataCon)
+import GhcPlugins          as GHC.TypeLits.Presburger.Compat (promotedTrueDataCon, text)
+import GhcPlugins          as GHC.TypeLits.Presburger.Compat (tyConAppTyCon_maybe, typeKind)
+import GhcPlugins          as GHC.TypeLits.Presburger.Compat (typeNatKind)
+import Module              as GHC.TypeLits.Presburger.Compat (ModuleName, mkModuleName)
+import OccName             as GHC.TypeLits.Presburger.Compat (emptyOccSet, mkInstTyTcOcc)
+import Plugins             as GHC.TypeLits.Presburger.Compat (Plugin (..), defaultPlugin)
+import TcEvidence          as GHC.TypeLits.Presburger.Compat (EvTerm)
+import TcHsType            as GHC.TypeLits.Presburger.Compat (tcInferApps)
+import TcPluginM           as GHC.TypeLits.Presburger.Compat (TcPluginM, tcLookupTyCon,
+                                          tcPluginTrace)
+import TcRnMonad           as GHC.TypeLits.Presburger.Compat (Ct, TcPluginResult (..), isWanted)
+import TcRnTypes           as GHC.TypeLits.Presburger.Compat (TcPlugin (..), ctEvPred, ctEvidence)
+import TcType              as GHC.TypeLits.Presburger.Compat (tcTyFamInsts)
+import TcTypeNats          as GHC.TypeLits.Presburger.Compat
+import TyCon               as GHC.TypeLits.Presburger.Compat
+#if MIN_VERSION_ghc(8,4,1)
+import TcType (TcTyVar, TcType)
+#else
+import TcRnTypes (cc_ev, ctev_pred)
+import Data.Maybe
+import TcPluginM (zonkCt)
+#endif
+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 800
+import           GhcPlugins (InScopeSet, Outputable, emptyUFM)
+import qualified PrelNames  as Old
+import           TyCoRep    as GHC.TypeLits.Presburger.Compat (TyLit (NumTyLit), Type (..))
+import           Type       as GHC.TypeLits.Presburger.Compat (TCvSubst (..), TvSubstEnv,
+                                           emptyTCvSubst)
+import           Type       as GHC.TypeLits.Presburger.Compat (eqType, unionTCvSubst)
+import qualified Type       as Old
+import           TysWiredIn as GHC.TypeLits.Presburger.Compat (boolTyCon)
+import           Unify      as Old (tcUnifyTy)
+#else
+import Type       as GHC.TypeLits.Presburger.Compat (TvSubst, emptyTvSubst)
+import Type       as GHC.TypeLits.Presburger.Compat (substTy, unionTvSubst)
+import TypeRep    as GHC.TypeLits.Presburger.Compat (TyLit (NumTyLit), Type (..))
+import TysWiredIn as Old (eqTyCon)
+import TysWiredIn as GHC.TypeLits.Presburger.Compat (promotedBoolTyCon)
+import Unify      as GHC.TypeLits.Presburger.Compat (tcUnifyTy)
+#endif
+import Data.Generics.Twins
+import TcPluginM           (lookupOrig)
+import TyCoRep             ()
+import Type                as GHC.TypeLits.Presburger.Compat (splitTyConApp_maybe)
+import Unique              as GHC.TypeLits.Presburger.Compat (getKey, getUnique)
+#if MIN_VERSION_ghc(8,4,1)
+import qualified GHC.TcPluginM.Extra as Extra
+#endif
+#if MIN_VERSION_ghc(8,8,1)
+import qualified TysWiredIn
+#endif
+
+#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 =
+#if MIN_VERSION_ghc(8,8,1)
+  return TysWiredIn.eqTyCon
+#else
+  tcLookupTyCon Old.eqTyConName
+#endif
+
+#else
+eqType :: Type -> Type -> Bool
+eqType = (==)
+
+getEqTyCon :: TcPluginM TyCon
+getEqTyCon = return Old.eqTyCon
+
+#endif
+
+
+getEqWitnessTyCon :: TcPluginM TyCon
+getEqWitnessTyCon = do
+  md <- lookupModule (mkModuleName "Data.Type.Equality") (fsLit "base")
+  tcLookupTyCon =<< lookupOrig md (mkTcOcc ":~:")
+
+decompFunTy :: Type -> [Type]
+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 =
+#if MIN_VERSION_ghc(8,4,1)
+  fmap (return . filter (not . isTrivial . ctEvPred . ctEvidence)) 
+  . (++) <$> id <*> Extra.flattenGivens
+#else
+  mapM zonkCt 
+#endif
+
+#if MIN_VERSION_ghc(8,4,1)
+type Substitution = [(TcTyVar, TcType)]
+#else
+type Substitution = TvSubst
+#endif
+
+subsCt :: Substitution -> Ct -> Ct
+subsCt =
+#if MIN_VERSION_ghc(8,4,1)
+  Extra.substCt
+#else
+  \subst ct ->
+  ct { cc_ev = (cc_ev ct) {ctev_pred = substTy subst (ctev_pred (cc_ev ct))}
+     }
+#endif
+
+subsType :: Substitution -> Type -> Type
+subsType =
+#if MIN_VERSION_ghc(8,4,1)
+  Extra.substType
+#else
+  substTy
+#endif
+
+mkSubstitution :: [Ct] -> Substitution
+mkSubstitution =
+#if MIN_VERSION_ghc(8,4,1)
+  fst . unzip . Extra.mkSubst'
+#else
+  foldr (unionTvSubst . genSubst) emptyTvSubst
+#endif
+
+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 804
+genSubst :: Ct -> TvSubst
+genSubst ct = case classifyPredType (ctEvPred . ctEvidence $ ct) of
+  EqPred NomEq t u -> fromMaybe emptyTvSubst $ GHC.TypeLits.Presburger.Compat.tcUnifyTy t u
+  _                -> emptyTvSubst
+#endif
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,501 @@
+{-# LANGUAGE BangPatterns, CPP, DataKinds, FlexibleContexts               #-}
+{-# LANGUAGE FlexibleInstances, LambdaCase, MultiWayIf, OverloadedStrings #-}
+{-# LANGUAGE PatternGuards, RankNTypes, TypeOperators, ViewPatterns       #-}
+-- | Since 0.3.0.0
+module GHC.TypeLits.Presburger.Types
+  ( pluginWith
+  , defaultTranslation
+  , Translation(..), ParseEnv, Machine
+  , module Data.Integer.SAT
+  ) where
+import           Class                          (classTyCon)
+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.Foldable                  (asum)
+import           Data.Integer.SAT               (Expr (..), Prop (..), PropSet,
+                                                 assert)
+import           Data.Integer.SAT               (checkSat, noProps, toName)
+import qualified Data.Integer.SAT               as SAT
+import           Data.List                      (nub)
+import qualified Data.Map.Strict                as M
+import           Data.Maybe                     (catMaybes, fromMaybe,
+                                                 isNothing)
+import           Data.Reflection                (Given, give, given)
+import qualified Data.Set                       as Set
+import           GHC.TypeLits.Presburger.Compat
+import           PrelNames
+import           TcPluginM                      (lookupOrig, newFlexiTyVar,
+                                                 newWanted, tcLookupClass)
+import           Type                           (mkPrimEqPredRole, mkTyVarTy)
+import           TysWiredIn                     (promotedEQDataCon,
+                                                 promotedGTDataCon,
+                                                 promotedLTDataCon)
+import           Var
+#if MIN_VERSION_ghc(8,6,0)
+import Plugins (purePlugin)
+#endif
+
+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 (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
+#if MIN_VERSION_ghc(8,6,0)
+    , pluginRecompile = purePlugin
+#endif
+    }
+  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 ()
+           , tcPluginSolve = decidePresburger mode trans
+           , tcPluginStop  = const $ return ()
+           }
+
+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 e@(K _) = return e
+
+data Translation =
+  Translation
+    { isEmpty     :: [TyCon]
+    , isTrue      :: [TyCon]
+    , trueData    :: [TyCon]
+    , falseData   :: [TyCon]
+    , voids       :: [TyCon]
+    , tyEq        :: [TyCon]
+    , tyEqBool    :: [TyCon]
+    , tyEqWitness :: [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]
+    , orderingLT  :: [TyCon]
+    , orderingGT  :: [TyCon]
+    , orderingEQ  :: [TyCon]
+    , natCompare  :: [TyCon]
+    , parsePred   :: (Type -> Machine Expr) -> Type -> Machine Prop
+    , parseExpr   :: Type -> Machine Expr
+    }
+
+instance Semigroup Translation where
+  l <> r =
+    Translation
+      { isEmpty = isEmpty l <> isEmpty r
+      , isTrue = isTrue l <> isTrue r
+      , voids = voids l <> voids r
+      , tyEq = tyEq l <> tyEq 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 = (<|>) <$> parseExpr l <*> parseExpr r
+      }
+
+instance Monoid Translation where
+  mempty = Translation
+    { isEmpty = mempty
+    , isTrue = mempty
+    , tyEq  = mempty
+    , tyEqBool = mempty
+    , tyEqWitness = mempty
+    , tyNeqBool = 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 mzero
+    }
+
+decidePresburger :: PluginMode -> TcPluginM Translation -> () -> [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginResult
+decidePresburger _ genTrans _ gs [] [] = do
+  tcPluginTrace "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
+        (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 mode genTrans _ gs ds ws = do
+  trans <- genTrans
+  give trans $ do
+    gs' <- normaliseGivens gs
+    let subst = mkSubstitution (gs' ++ ds)
+    tcPluginTrace "Current subst" (ppr subst)
+    tcPluginTrace "wanteds" $ ppr $ map deconsPred ws
+    tcPluginTrace "givens" $ ppr $ map (subsType subst . deconsPred) gs
+    tcPluginTrace "deriveds" $ ppr $ map deconsPred ds
+    (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 ++ ds)
+      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 = [(evByFiat "ghc-typelits-presburger" t1 t2, ct)
+                  | ct <- solved
+                  , EqPred NomEq t1 t2 <- return (classifyPredType $ deconsPred ct)
+                  ]
+    tcPluginTrace "final premises" (text $ show prems0)
+    tcPluginTrace "final goals" (text $ show $ map snd wants)
+    case testIf prems (foldr ((:&&) . snd) PTrue wants) of
+      Proved -> do
+        tcPluginTrace "Proved" (text $ show $ map snd wants)
+        tcPluginTrace "... with coercions" (ppr coerced)
+        return $ TcPluginOk coerced []
+      Disproved wit -> do
+        tcPluginTrace "Failed! " (text $ show wit)
+        return $ TcPluginContradiction $ map fst wants
+
+defaultTranslation :: TcPluginM Translation
+defaultTranslation = do
+  emd <- lookupModule (mkModuleName "Proof.Propositional.Empty") (fsLit "equational-reasoning")
+  emptyClsTyCon <- classTyCon <$> (tcLookupClass =<< lookupOrig emd (mkTcOcc "Empty"))
+  eqTyCon_ <- getEqTyCon
+  eqWitCon_ <- getEqWitnessTyCon
+  pmd <- lookupModule (mkModuleName "Proof.Propositional") (fsLit "equational-reasoning")
+  isTrueCon_ <- tcLookupTyCon =<< lookupOrig pmd (mkTcOcc "IsTrue")
+  vmd <- lookupModule (mkModuleName "Data.Void") (fsLit "base")
+  voidTyCon <- tcLookupTyCon =<< lookupOrig vmd (mkTcOcc "Void")
+  nLeq <- tcLookupTyCon =<< lookupOrig gHC_TYPENATS (mkTcOcc "<=")
+  return
+    mempty
+    { isEmpty = [emptyClsTyCon]
+    , tyEq = [eqTyCon_]
+    , tyEqWitness = [eqWitCon_]
+    , isTrue = [isTrueCon_]
+    , voids = [voidTyCon]
+    , natMinus = [typeNatSubTyCon]
+    , natPlus = [typeNatAddTyCon]
+    , natTimes = [typeNatMulTyCon]
+    , natExp = [typeNatExpTyCon]
+    , falseData = [promotedFalseDataCon]
+    , trueData = [promotedTrueDataCon]
+    , natLeqBool = [typeNatLeqTyCon]
+    , natLeq = [nLeq]
+    , natCompare = [typeNatCmpTyCon]
+    , orderingEQ = [promotedEQDataCon]
+    , orderingLT = [promotedLTDataCon]
+    , orderingGT = [promotedGTDataCon]
+    }
+
+(<=>) :: Prop -> Prop -> Prop
+p <=> q =  (p :&& q) :|| (Not p :&& Not q)
+
+withEv :: Ct -> (EvTerm, Ct)
+withEv ct
+  | EqPred _ t1 t2 <- classifyPredType (deconsPred ct) =
+      (evByFiat "ghc-typelits-presburger" t1 t2, ct)
+  | otherwise = undefined
+
+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 [t1, t2])
+  | con `elem` (natLeq given ++ natLeqBool given)
+  = (:<=) <$> toPresburgerExp t1 <*> toPresburgerExp t2
+toPresburgerPred ty
+  | Just (con, []) <- splitTyConApp_maybe ty
+  , con `elem` trueData given = return PTrue
+  | Just (con, []) <- splitTyConApp_maybe ty
+  , con `elem` falseData given = return PFalse
+  | isEqPred ty = toPresburgerPredTree $ classifyPredType ty
+  | Just (con, [l, r]) <- splitTyConApp_maybe 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
+  | 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)
+
+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 <$> toPresburgerPredTree (EqPred NomEq p (mkTyConTy promotedTrueDataCon))
+toPresburgerPredTree (EqPred NomEq p b)  -- (n :<=? m) ~ 'True
+  | maybe False (`elem` trueData given) $ tyConAppTyCon_maybe b
+  , Just (con, [t1, t2]) <- splitTyConAppLastBin p
+  , con `elem` natLeqBool given = (:<=) <$> toPresburgerExp t1  <*> toPresburgerExp t2
+toPresburgerPredTree (EqPred NomEq p q)  -- (p :: Bool) ~ (q :: Bool)
+    | typeKind p `eqType` mkTyConTy promotedBoolTyCon = do
+      lift $ lift $ tcPluginTrace "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 (ClassPred con ts)
+  -- (n :: Nat) (<=| < | > | >= | == | /=) (m :: Nat)
+  | let n = length ts, n >= 2
+  , [t1, t2] <- drop (n - 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 ]
+
+toPresburgerExp :: Given Translation => Type -> Machine Expr
+toPresburgerExp ty = case ty of
+  TyVarTy t          -> return $ Var $ toName $ getKey $ getUnique t
+  t@(TyConApp tc ts) -> body tc ts <|> Var . toName . getKey . getUnique <$> toVar t
+  LitTy (NumTyLit n) -> return (K n)
+  LitTy _            -> mzero
+  t                  ->
+        parseExpr given 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) -> (:*) <$> pure n <*> toPresburgerExp x
+            (x, LitTy (NumTyLit n)) -> (:*) <$> pure n <*> toPresburgerExp x
+            _ -> mzero
+        _ ->  asum
+           $  [ step con (:+)
+              | con <- natPlus given
+              ] ++
+              [ step con (:-)
+              | con <- natMinus given
+              ]
+
+
+-- simplTypeCmp :: Type -> Type
+
+lastTwo :: [a] -> [a]
+lastTwo = drop <$> subtract 2 . length <*> id
+
+simpleExp :: Given Translation => 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 (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) ->
+    newWanted undefined $ 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