diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -5,6 +5,12 @@
 The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),
 and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html).
 
+## [Unreleased]
+
+## [0.3.1.1] -- 2023-09-29
+
+No user-facing changes.
+
 ## [0.3.1.0] -- 2023-07-19
 
 ### Added
@@ -64,9 +70,8 @@
 - Initial release for Grisette.
 
 [Unreleased]: https://github.com/lsrcz/grisette/compare/v0.3.1.0...HEAD
+[0.3.1.1]: https://github.com/lsrcz/grisette/compare/v0.3.1.0...v0.3.1.1
 [0.3.1.0]: https://github.com/lsrcz/grisette/compare/v0.3.0.0...v0.3.1.0
-[0.3.0.0]: https://github.com/lsrcz/grisette/compare/v0.2.0.0...v0.3.0.0
-[Unreleased]: https://github.com/lsrcz/grisette/compare/v0.3.0.0...HEAD
 [0.3.0.0]: https://github.com/lsrcz/grisette/compare/v0.2.0.0...v0.3.0.0
 [0.2.0.0]: https://github.com/lsrcz/grisette/compare/v0.1.0.0...v0.2.0.0
 [0.1.0.0]: https://github.com/lsrcz/grisette/tree/v0.1.0.0
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -47,7 +47,7 @@
 ```cabal
 library
   ...
-  build-depends: grisette >= 0.2 < 0.3
+  build-depends: grisette >= 0.3 < 0.4
 ```
 
 #### Quick start template with `stack new`
diff --git a/doctest/Main.hs b/doctest/Main.hs
--- a/doctest/Main.hs
+++ b/doctest/Main.hs
@@ -1,4 +1,4 @@
-module Main where
+module Main (main) where
 
 import System.FilePath.Glob (glob)
 import Test.DocTest (doctest)
diff --git a/grisette.cabal b/grisette.cabal
--- a/grisette.cabal
+++ b/grisette.cabal
@@ -5,7 +5,7 @@
 -- see: https://github.com/sol/hpack
 
 name:           grisette
-version:        0.3.1.0
+version:        0.3.1.1
 synopsis:       Symbolic evaluation as a library
 description:    Grisette is a reusable symbolic evaluation library for Haskell. By
                 translating programs into constraints, Grisette can help the development of
@@ -28,7 +28,7 @@
     GHC == 8.10.7
   , GHC == 9.0.2
   , GHC == 9.2.8
-  , GHC == 9.4.5
+  , GHC == 9.4.6
   , GHC == 9.6.2
 extra-source-files:
     CHANGELOG.md
@@ -126,13 +126,13 @@
       Paths_grisette
   hs-source-dirs:
       src
+  ghc-options: -Wextra -Wcompat -Widentities -Wincomplete-record-updates -Wmissing-export-lists -Wmissing-home-modules -Wmissing-import-lists -Wpartial-fields -Wunused-type-patterns
   build-depends:
       QuickCheck >=2.13.2 && <2.15
     , array >=0.5.4 && <0.6
     , base >=4.14 && <5
-    , bytestring >=0.10.12 && <0.12
-    , call-stack >=0.1 && <0.5
-    , deepseq >=1.4.4 && <1.5
+    , bytestring >=0.10.12 && <0.13
+    , deepseq >=1.4.4 && <1.6
     , generic-deriving >=1.14.1 && <1.15
     , hashable >=1.2.3 && <1.5
     , hashtables >=1.2.3.4 && <1.4
@@ -143,11 +143,10 @@
     , prettyprinter >=1.5.0 && <1.8
     , sbv >=8.11 && <10.3
     , template-haskell >=2.16 && <2.21
-    , text >=1.2.4.1 && <2.1
+    , text >=1.2.4.1 && <2.2
     , th-compat >=0.1.2 && <0.2
     , transformers >=0.5.6 && <0.7
     , unordered-containers >=0.2.11 && <0.3
-    , vector >=0.12.1 && <0.14
   default-language: Haskell2010
   if flag(fast)
     ghc-options: -O2
@@ -161,15 +160,15 @@
       Paths_grisette
   hs-source-dirs:
       doctest
+  ghc-options: -Wextra -Wcompat -Widentities -Wincomplete-record-updates -Wmissing-export-lists -Wmissing-home-modules -Wmissing-import-lists -Wpartial-fields -Wunused-type-patterns -threaded -rtsopts -with-rtsopts=-N
   build-depends:
       Glob
     , QuickCheck >=2.13.2 && <2.15
     , array >=0.5.4 && <0.6
     , base >=4.14 && <5
-    , bytestring >=0.10.12 && <0.12
-    , call-stack >=0.1 && <0.5
-    , deepseq >=1.4.4 && <1.5
-    , doctest >=0.18.2 && <0.22
+    , bytestring >=0.10.12 && <0.13
+    , deepseq >=1.4.4 && <1.6
+    , doctest >=0.18.2 && <0.23
     , generic-deriving >=1.14.1 && <1.15
     , grisette
     , hashable >=1.2.3 && <1.5
@@ -181,11 +180,10 @@
     , prettyprinter >=1.5.0 && <1.8
     , sbv >=8.11 && <10.3
     , template-haskell >=2.16 && <2.21
-    , text >=1.2.4.1 && <2.1
+    , text >=1.2.4.1 && <2.2
     , th-compat >=0.1.2 && <0.2
     , transformers >=0.5.6 && <0.7
     , unordered-containers >=0.2.11 && <0.3
-    , vector >=0.12.1 && <0.14
   default-language: Haskell2010
   if flag(fast)
     ghc-options: -O2
@@ -215,13 +213,14 @@
       Paths_grisette
   hs-source-dirs:
       test
+  ghc-options: -Wextra -Wcompat -Widentities -Wincomplete-record-updates -Wmissing-export-lists -Wmissing-home-modules -Wmissing-import-lists -Wpartial-fields -Wunused-type-patterns -threaded -rtsopts -with-rtsopts=-N
   build-depends:
-      QuickCheck >=2.13.2 && <2.15
+      HUnit ==1.6.*
+    , QuickCheck >=2.13.2 && <2.15
     , array >=0.5.4 && <0.6
     , base >=4.14 && <5
-    , bytestring >=0.10.12 && <0.12
-    , call-stack >=0.1 && <0.5
-    , deepseq >=1.4.4 && <1.5
+    , bytestring >=0.10.12 && <0.13
+    , deepseq >=1.4.4 && <1.6
     , generic-deriving >=1.14.1 && <1.15
     , grisette
     , hashable >=1.2.3 && <1.5
@@ -232,16 +231,14 @@
     , parallel >=3.2.2.0 && <3.3
     , prettyprinter >=1.5.0 && <1.8
     , sbv >=8.11 && <10.3
-    , tasty >=1.1.0.3 && <1.5
-    , tasty-hunit ==0.10.*
-    , tasty-quickcheck >=0.10.1 && <0.11
-    , tasty-test-reporter >=0.1.1.2 && <0.2
     , template-haskell >=2.16 && <2.21
-    , text >=1.2.4.1 && <2.1
+    , test-framework >=0.8.2 && <0.9
+    , test-framework-hunit >=0.3.0.2 && <0.4
+    , test-framework-quickcheck2 >=0.3.0.5 && <0.4
+    , text >=1.2.4.1 && <2.2
     , th-compat >=0.1.2 && <0.2
     , transformers >=0.5.6 && <0.7
     , unordered-containers >=0.2.11 && <0.3
-    , vector >=0.12.1 && <0.14
   default-language: Haskell2010
   if flag(fast)
     ghc-options: -O2
diff --git a/src/Grisette.hs b/src/Grisette.hs
--- a/src/Grisette.hs
+++ b/src/Grisette.hs
@@ -1,5 +1,8 @@
+-- Disable this warning because we are re-exporting things.
+{-# OPTIONS_GHC -Wno-missing-import-lists #-}
+
 -- |
--- Module      :   Grisette.Core
+-- Module      :   Grisette
 -- Copyright   :   (c) Sirui Lu 2021-2023
 -- License     :   BSD-3-Clause (see the LICENSE file)
 --
diff --git a/src/Grisette/Backend/SBV.hs b/src/Grisette/Backend/SBV.hs
--- a/src/Grisette/Backend/SBV.hs
+++ b/src/Grisette/Backend/SBV.hs
@@ -1,3 +1,6 @@
+-- Disable this warning because we are re-exporting things.
+{-# OPTIONS_GHC -Wno-missing-import-lists #-}
+
 -- |
 -- Module      :   Grisette.Backend.SBV
 -- Copyright   :   (c) Sirui Lu 2021-2023
@@ -34,3 +37,14 @@
 
 import qualified Data.SBV as SBV
 import Grisette.Backend.SBV.Data.SMT.Solving
+  ( ApproximationConfig (..),
+    ExtraConfig (..),
+    GrisetteSMTConfig (..),
+    SolvingFailure (..),
+    approx,
+    clearApprox,
+    clearTimeout,
+    precise,
+    withApprox,
+    withTimeout,
+  )
diff --git a/src/Grisette/Backend/SBV/Data/SMT/Lowering.hs b/src/Grisette/Backend/SBV/Data/SMT/Lowering.hs
--- a/src/Grisette/Backend/SBV/Data/SMT/Lowering.hs
+++ b/src/Grisette/Backend/SBV/Data/SMT/Lowering.hs
@@ -32,54 +32,125 @@
   )
 where
 
-import Control.Monad.State.Strict
-import Data.Bifunctor
+import Data.Bifunctor (Bifunctor (bimap, first, second))
 import Data.Bits
-import Data.Dynamic
-import Data.Foldable
-import Data.Kind
-import Data.Maybe
+  ( Bits (complement, rotate, shift, xor, (.&.), (.|.)),
+  )
+import Data.Dynamic (Typeable, fromDyn, toDyn)
+import Data.Foldable (Foldable (foldl'), asum)
+import Data.Kind (Type)
+import Data.Maybe (fromMaybe)
 import qualified Data.SBV as SBV
 import qualified Data.SBV.Control as SBVC
 import qualified Data.SBV.Internals as SBVI
 import Data.Type.Equality (type (~~))
-import Data.Typeable
+import Data.Typeable (Proxy (Proxy), type (:~:) (Refl))
 import GHC.Exts (sortWith)
-import GHC.Natural
-import GHC.Stack
+import GHC.Stack (HasCallStack)
 import GHC.TypeNats
+  ( KnownNat,
+    Nat,
+    natVal,
+    type (+),
+    type (-),
+    type (<=),
+  )
 import {-# SOURCE #-} Grisette.Backend.SBV.Data.SMT.Solving
+  ( ApproximationConfig (Approx, NoApprox),
+    ExtraConfig (integerApprox),
+    GrisetteSMTConfig (GrisetteSMTConfig),
+    TermTy,
+  )
 import Grisette.Backend.SBV.Data.SMT.SymBiMap
-import Grisette.Core.Data.BV
+  ( SymBiMap,
+    addBiMap,
+    addBiMapIntermediate,
+    emptySymBiMap,
+    findStringToSymbol,
+    lookupTerm,
+    sizeBiMap,
+  )
+import Grisette.Core.Data.BV (IntN (IntN, unIntN), WordN (WordN))
 import Grisette.Core.Data.Class.ModelOps
+  ( ModelOps (emptyModel, insertValue),
+  )
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors
+  ( conTerm,
+    symTerm,
+  )
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.SomeTerm
+  ( SomeTerm (SomeTerm),
+  )
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
+  ( SomeTypedSymbol (SomeTypedSymbol),
+    SupportedPrim (withPrim),
+    Term
+      ( AbsNumTerm,
+        AddNumTerm,
+        AndBitsTerm,
+        AndTerm,
+        BVConcatTerm,
+        BVExtendTerm,
+        BVSelectTerm,
+        BVToSignedTerm,
+        BVToUnsignedTerm,
+        BinaryTerm,
+        ComplementBitsTerm,
+        ConTerm,
+        DivBoundedIntegralTerm,
+        DivIntegralTerm,
+        EqvTerm,
+        GeneralFunApplyTerm,
+        ITETerm,
+        LENumTerm,
+        LTNumTerm,
+        ModBoundedIntegralTerm,
+        ModIntegralTerm,
+        NotTerm,
+        OrBitsTerm,
+        OrTerm,
+        QuotBoundedIntegralTerm,
+        QuotIntegralTerm,
+        RemBoundedIntegralTerm,
+        RemIntegralTerm,
+        RotateBitsTerm,
+        ShiftBitsTerm,
+        SignumNumTerm,
+        SymTerm,
+        TabularFunApplyTerm,
+        TernaryTerm,
+        TimesNumTerm,
+        UMinusNumTerm,
+        UnaryTerm,
+        XorBitsTerm
+      ),
+    TypedSymbol (IndexedSymbol),
+    buildGeneralFun,
+    someTypedSymbol,
+    withSymbolSupported,
+    type (-->),
+  )
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermUtils
-import Grisette.IR.SymPrim.Data.Prim.Model as PM
+  ( introSupportedPrimConstraint,
+  )
+import Grisette.IR.SymPrim.Data.Prim.Model as PM (Model)
 import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bool
+  ( pevalEqvTerm,
+    pevalITETerm,
+  )
 import Grisette.IR.SymPrim.Data.TabularFun
+  ( type (=->) (TabularFun),
+  )
 import Grisette.Utils.Parameterized
+  ( KnownProof (KnownProof),
+    LeqProof (LeqProof),
+    unsafeAxiom,
+    unsafeKnownProof,
+    unsafeLeqProof,
+    withKnownProof,
+  )
 import qualified Type.Reflection as R
-import Unsafe.Coerce
 
-cachedResult ::
-  forall integerBitWidth a.
-  (SupportedPrim a, Typeable (TermTy integerBitWidth a)) =>
-  Term a ->
-  State SymBiMap (Maybe (TermTy integerBitWidth a))
-cachedResult t = gets $ \m -> do
-  d <- lookupTerm (SomeTerm t) m
-  Just $ fromDyn d undefined
-
-addResult ::
-  forall integerBitWidth a.
-  (SupportedPrim a, Typeable (TermTy integerBitWidth a)) =>
-  Term a ->
-  TermTy integerBitWidth a ->
-  State SymBiMap ()
-addResult tm sbvtm = modify $ addBiMapIntermediate (SomeTerm tm) (toDyn sbvtm)
-
 translateTypeError :: (HasCallStack) => R.TypeRep a -> b
 translateTypeError ta =
   error $
@@ -144,7 +215,7 @@
           lowerTFunCon config v
         _ -> translateTypeError (R.typeRep @a)
     _ -> translateTypeError (R.typeRep @a)
-lowerValue config v = translateTypeError (R.typeRep @a)
+lowerValue _ _ = translateTypeError (R.typeRep @a)
 
 lowerTFunCon ::
   forall integerBitWidth a b.
@@ -154,9 +225,9 @@
   (TermTy integerBitWidth a -> TermTy integerBitWidth b)
 lowerTFunCon config@ResolvedConfig {} (TabularFun l d) = go l d
   where
-    go [] d v = lowerValue config d
+    go [] d _ = lowerValue config d
     go ((x, r) : xs) d v = SBV.ite (lowerValue config x SBV..== v) (lowerValue config r) (go xs d v)
-lowerTFunCon _ (TabularFun l d) = translateTypeError (R.typeRep @a)
+lowerTFunCon _ TabularFun {} = translateTypeError (R.typeRep @a)
 
 buildUTFun11 ::
   forall integerBitWidth s1 s2 a.
diff --git a/src/Grisette/Backend/SBV/Data/SMT/Solving.hs b/src/Grisette/Backend/SBV/Data/SMT/Solving.hs
--- a/src/Grisette/Backend/SBV/Data/SMT/Solving.hs
+++ b/src/Grisette/Backend/SBV/Data/SMT/Solving.hs
@@ -37,35 +37,59 @@
   )
 where
 
-import Control.DeepSeq
-import Control.Exception
-import Control.Monad.Except
-import Control.Monad.IO.Class
+import Control.DeepSeq (NFData)
+import Control.Exception (handle)
+import Control.Monad.IO.Class (liftIO)
 import qualified Data.HashSet as S
-import Data.Hashable
-import Data.Kind
+import Data.Hashable (Hashable)
+import Data.Kind (Type)
 import Data.List (partition)
-import Data.Maybe
+import Data.Maybe (fromJust)
 import qualified Data.SBV as SBV
 import Data.SBV.Control (Query)
 import qualified Data.SBV.Control as SBVC
-import GHC.TypeNats
+import GHC.TypeNats (KnownNat, Nat)
 import Grisette.Backend.SBV.Data.SMT.Lowering
-import Grisette.Core.Data.BV
-import Grisette.Core.Data.Class.Bool
+  ( SymBiMap,
+    lowerSinglePrim,
+    lowerSinglePrimCached,
+    parseModel,
+  )
+import Grisette.Core.Data.BV (IntN, WordN)
+import Grisette.Core.Data.Class.Bool (LogicalOp (nots, (&&~)))
 import Grisette.Core.Data.Class.CEGISSolver
-import Grisette.Core.Data.Class.Evaluate
+  ( CEGISCondition (CEGISCondition),
+    CEGISSolver (cegisMultiInputs),
+  )
+import Grisette.Core.Data.Class.Evaluate (EvaluateSym (evaluateSym))
 import Grisette.Core.Data.Class.ExtractSymbolics
-import Grisette.Core.Data.Class.GenSym
+  ( ExtractSymbolics (extractSymbolics),
+  )
 import Grisette.Core.Data.Class.ModelOps
-import Grisette.Core.Data.Class.Solvable
-import Grisette.Core.Data.Class.Solver
+  ( ModelOps (exact, exceptFor),
+    SymbolSetOps (isEmptySet),
+  )
+import Grisette.Core.Data.Class.Solvable (Solvable (con))
+import Grisette.Core.Data.Class.Solver (Solver (solve, solveAll, solveMulti))
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors
+  ( conTerm,
+  )
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
+  ( SomeTypedSymbol (SomeTypedSymbol),
+    Term,
+    type (-->),
+  )
 import Grisette.IR.SymPrim.Data.Prim.Model as PM
+  ( Model,
+    SymbolSet (unSymbolSet),
+    equation,
+  )
 import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bool
-import Grisette.IR.SymPrim.Data.SymPrim
-import Grisette.IR.SymPrim.Data.TabularFun
+  ( pevalNotTerm,
+    pevalOrTerm,
+  )
+import Grisette.IR.SymPrim.Data.SymPrim (SymBool (SymBool))
+import Grisette.IR.SymPrim.Data.TabularFun (type (=->))
 import Language.Haskell.TH.Syntax (Lift)
 
 -- $setup
@@ -76,7 +100,7 @@
 
 type Aux :: Bool -> Nat -> Type
 type family Aux o n where
-  Aux 'True n = SBV.SInteger
+  Aux 'True _ = SBV.SInteger
   Aux 'False n = SBV.SInt n
 
 type IsZero :: Nat -> Bool
@@ -88,8 +112,8 @@
 type family TermTy bitWidth b where
   TermTy _ Bool = SBV.SBool
   TermTy n Integer = Aux (IsZero n) n
-  TermTy n (IntN x) = SBV.SBV (SBV.IntN x)
-  TermTy n (WordN x) = SBV.SBV (SBV.WordN x)
+  TermTy _ (IntN x) = SBV.SBV (SBV.IntN x)
+  TermTy _ (WordN x) = SBV.SBV (SBV.WordN x)
   TermTy n (a =-> b) = TermTy n a -> TermTy n b
   TermTy n (a --> b) = TermTy n a -> TermTy n b
   TermTy _ v = v
@@ -325,7 +349,7 @@
 
 instance CEGISSolver (GrisetteSMTConfig n) SolvingFailure where
   cegisMultiInputs ::
-    forall inputs spec.
+    forall inputs.
     (ExtractSymbolics inputs, EvaluateSym inputs) =>
     GrisetteSMTConfig n ->
     [inputs] ->
diff --git a/src/Grisette/Backend/SBV/Data/SMT/Solving.hs-boot b/src/Grisette/Backend/SBV/Data/SMT/Solving.hs-boot
--- a/src/Grisette/Backend/SBV/Data/SMT/Solving.hs-boot
+++ b/src/Grisette/Backend/SBV/Data/SMT/Solving.hs-boot
@@ -13,16 +13,18 @@
   )
 where
 
-import Data.Kind
+import Data.Kind (Type)
 import qualified Data.SBV as SBV
-import GHC.TypeNats
-import Grisette.Core.Data.BV
+import GHC.TypeNats (KnownNat, Nat)
+import Grisette.Core.Data.BV (IntN, WordN)
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
-import Grisette.IR.SymPrim.Data.TabularFun
+  ( type (-->),
+  )
+import Grisette.IR.SymPrim.Data.TabularFun (type (=->))
 
 type Aux :: Bool -> Nat -> Type
 type family Aux o n where
-  Aux 'True n = SBV.SInteger
+  Aux 'True _ = SBV.SInteger
   Aux 'False n = SBV.SInt n
 
 type IsZero :: Nat -> Bool
@@ -34,8 +36,8 @@
 type family TermTy bitWidth b where
   TermTy _ Bool = SBV.SBool
   TermTy n Integer = Aux (IsZero n) n
-  TermTy n (IntN x) = SBV.SBV (SBV.IntN x)
-  TermTy n (WordN x) = SBV.SBV (SBV.WordN x)
+  TermTy _ (IntN x) = SBV.SBV (SBV.IntN x)
+  TermTy _ (WordN x) = SBV.SBV (SBV.WordN x)
   TermTy n (a =-> b) = TermTy n a -> TermTy n b
   TermTy n (a --> b) = TermTy n a -> TermTy n b
   TermTy _ v = v
diff --git a/src/Grisette/Backend/SBV/Data/SMT/SymBiMap.hs b/src/Grisette/Backend/SBV/Data/SMT/SymBiMap.hs
--- a/src/Grisette/Backend/SBV/Data/SMT/SymBiMap.hs
+++ b/src/Grisette/Backend/SBV/Data/SMT/SymBiMap.hs
@@ -19,11 +19,15 @@
   )
 where
 
-import Data.Dynamic
+import Data.Dynamic (Dynamic)
 import qualified Data.HashMap.Strict as M
-import GHC.Stack
+import GHC.Stack (HasCallStack)
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.SomeTerm
+  ( SomeTerm,
+  )
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
+  ( SomeTypedSymbol,
+  )
 
 data SymBiMap = SymBiMap
   { biMapToSBV :: M.HashMap SomeTerm Dynamic,
diff --git a/src/Grisette/Core.hs b/src/Grisette/Core.hs
--- a/src/Grisette/Core.hs
+++ b/src/Grisette/Core.hs
@@ -1,5 +1,7 @@
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE Trustworthy #-}
+-- Disable this warning because we are re-exporting things.
+{-# OPTIONS_GHC -Wno-missing-import-lists #-}
 
 -- |
 -- Module      :   Grisette.Core
@@ -1011,33 +1013,188 @@
 
 import Generics.Deriving (Default (..), Default1 (..))
 import Grisette.Core.BuiltinUnionWrappers
+  ( mrgAssertionViolation,
+    mrgAssumptionViolation,
+    mrgFalse,
+    mrgInL,
+    mrgInR,
+    mrgJust,
+    mrgLeft,
+    mrgNothing,
+    mrgRight,
+    mrgTrue,
+    mrgTuple2,
+    mrgTuple3,
+    mrgUnit,
+  )
 import Grisette.Core.Control.Exception
+  ( AssertionError (..),
+    VerificationConditions (..),
+    symAssert,
+    symAssume,
+  )
 import Grisette.Core.Control.Monad.CBMCExcept
+  ( CBMCEither (..),
+    CBMCExceptT (..),
+    cbmcExcept,
+    mapCBMCExceptT,
+    withCBMCExceptT,
+  )
 import Grisette.Core.Control.Monad.Class.MonadParallelUnion
-import Grisette.Core.Control.Monad.Union
+  ( MonadParallelUnion (..),
+  )
+import Grisette.Core.Control.Monad.Union (MonadUnion)
 import Grisette.Core.Control.Monad.UnionM
+  ( IsConcrete,
+    UnionM,
+    liftToMonadUnion,
+    unionSize,
+    (#~),
+  )
 import Grisette.Core.Data.Class.BitVector
+  ( BV (..),
+    SizedBV (..),
+    bvExtract,
+    sizedBVExtract,
+  )
 import Grisette.Core.Data.Class.Bool
+  ( ITEOp (..),
+    LogicalOp (..),
+    SEq (..),
+    SymBoolOp,
+  )
 import Grisette.Core.Data.Class.CEGISSolver
+  ( CEGISCondition (..),
+    CEGISSolver (..),
+    cegis,
+    cegisExcept,
+    cegisExceptMultiInputs,
+    cegisExceptStdVC,
+    cegisExceptStdVCMultiInputs,
+    cegisExceptVC,
+    cegisExceptVCMultiInputs,
+    cegisPostCond,
+    cegisPrePost,
+  )
 import Grisette.Core.Data.Class.Error
+  ( TransformError (..),
+    symAssertTransformableError,
+    symAssertWith,
+    symThrowTransformableError,
+  )
 import Grisette.Core.Data.Class.Evaluate
+  ( EvaluateSym (..),
+    evaluateSymToCon,
+  )
 import Grisette.Core.Data.Class.ExtractSymbolics
-import Grisette.Core.Data.Class.Function
-import Grisette.Core.Data.Class.GPretty
+  ( ExtractSymbolics (..),
+  )
+import Grisette.Core.Data.Class.Function (Function (..))
+import Grisette.Core.Data.Class.GPretty (GPretty (..))
 import Grisette.Core.Data.Class.GenSym
+  ( EnumGenBound (..),
+    EnumGenUpperBound (..),
+    Fresh,
+    FreshIdent (..),
+    FreshIndex (..),
+    FreshT,
+    GenSym (..),
+    GenSymSimple (..),
+    ListSpec (..),
+    MonadFresh (..),
+    SimpleListSpec (..),
+    choose,
+    chooseFresh,
+    chooseSimple,
+    chooseSimpleFresh,
+    chooseUnion,
+    chooseUnionFresh,
+    derivedNoSpecFresh,
+    derivedNoSpecSimpleFresh,
+    derivedSameShapeSimpleFresh,
+    genSym,
+    genSymSimple,
+    name,
+    nameWithInfo,
+    runFresh,
+    runFreshT,
+  )
 import Grisette.Core.Data.Class.Mergeable
+  ( DynamicSortedIdx (..),
+    Mergeable (..),
+    Mergeable1 (..),
+    Mergeable2 (..),
+    Mergeable3 (..),
+    MergingStrategy (..),
+    StrategyList (..),
+    buildStrategyList,
+    derivedRootStrategy,
+    product2Strategy,
+    resolveStrategy,
+    resolveStrategy',
+    rootStrategy1,
+    rootStrategy2,
+    rootStrategy3,
+    wrapStrategy,
+  )
 import Grisette.Core.Data.Class.ModelOps
-import Grisette.Core.Data.Class.SOrd
+  ( ModelOps (..),
+    ModelRep (..),
+    SymbolSetOps (..),
+    SymbolSetRep (..),
+  )
+import Grisette.Core.Data.Class.SOrd (SOrd (..))
 import Grisette.Core.Data.Class.SafeArith
+  ( SafeDivision (..),
+    SafeLinearArith (..),
+    SymIntegerOp,
+  )
 import Grisette.Core.Data.Class.SimpleMergeable
-import Grisette.Core.Data.Class.Solvable
+  ( SimpleMergeable (..),
+    SimpleMergeable1 (..),
+    SimpleMergeable2 (..),
+    UnionLike (..),
+    UnionPrjOp (..),
+    merge,
+    mrgIf,
+    mrgIte1,
+    mrgIte2,
+    mrgSingle,
+    onUnion,
+    onUnion2,
+    onUnion3,
+    onUnion4,
+    simpleMerge,
+    pattern IfU,
+    pattern SingleU,
+  )
+import Grisette.Core.Data.Class.Solvable (Solvable (..), pattern Con)
 import Grisette.Core.Data.Class.Solver
+  ( Solver (..),
+    UnionWithExcept (..),
+    solveExcept,
+    solveMultiExcept,
+  )
 import Grisette.Core.Data.Class.Substitute
-import Grisette.Core.Data.Class.ToCon
-import Grisette.Core.Data.Class.ToSym
+  ( SubstituteSym (..),
+    SubstituteSym' (..),
+  )
+import Grisette.Core.Data.Class.ToCon (ToCon (..))
+import Grisette.Core.Data.Class.ToSym (ToSym (..))
 import Grisette.Core.Data.FileLocation
+  ( FileLocation (..),
+    ilocsym,
+    nameWithLoc,
+    slocsym,
+  )
 import Grisette.Core.Data.MemoUtils
-import Grisette.Core.TH
+  ( htmemo,
+    htmemo2,
+    htmemo3,
+    htmemoFix,
+    htmup,
+  )
+import Grisette.Core.TH (makeUnionWrapper, makeUnionWrapper')
 
 -- $setup
 -- >>> import Grisette.Core
diff --git a/src/Grisette/Core/BuiltinUnionWrappers.hs b/src/Grisette/Core/BuiltinUnionWrappers.hs
--- a/src/Grisette/Core/BuiltinUnionWrappers.hs
+++ b/src/Grisette/Core/BuiltinUnionWrappers.hs
@@ -30,10 +30,10 @@
   )
 where
 
-import Data.Functor.Sum
-import Grisette.Core.Control.Exception
-import Grisette.Core.Data.Class.SimpleMergeable
-import Grisette.Core.TH
+import Data.Functor.Sum (Sum)
+import Grisette.Core.Control.Exception (VerificationConditions)
+import Grisette.Core.Data.Class.SimpleMergeable (mrgSingle)
+import Grisette.Core.TH (makeUnionWrapper, makeUnionWrapper')
 
 $(makeUnionWrapper "mrg" ''Bool)
 $(makeUnionWrapper' ["mrgUnit"] ''())
diff --git a/src/Grisette/Core/Control/Exception.hs b/src/Grisette/Core/Control/Exception.hs
--- a/src/Grisette/Core/Control/Exception.hs
+++ b/src/Grisette/Core/Control/Exception.hs
@@ -24,23 +24,33 @@
   )
 where
 
-import Control.DeepSeq
-import Control.Exception
-import Control.Monad.Except
-import GHC.Generics
-import Generics.Deriving
-import Grisette.Core.Control.Monad.Union
-import Grisette.Core.Data.Class.Bool
+import Control.DeepSeq (NFData)
+import Control.Exception (ArithException, ArrayException)
+import Control.Monad.Except (MonadError)
+import GHC.Generics (Generic)
+import Generics.Deriving (Default (Default))
+import Grisette.Core.Control.Monad.Union (MonadUnion)
+import Grisette.Core.Data.Class.Bool (SEq)
 import Grisette.Core.Data.Class.Error
-import Grisette.Core.Data.Class.Evaluate
+  ( TransformError (transformError),
+    symAssertTransformableError,
+  )
+import Grisette.Core.Data.Class.Evaluate (EvaluateSym)
 import Grisette.Core.Data.Class.ExtractSymbolics
-import Grisette.Core.Data.Class.Mergeable
+  ( ExtractSymbolics,
+  )
+import Grisette.Core.Data.Class.Mergeable (Mergeable)
 import Grisette.Core.Data.Class.SOrd
+  ( SOrd (symCompare, (<=~), (<~), (>=~), (>~)),
+  )
 import Grisette.Core.Data.Class.SimpleMergeable
-import Grisette.Core.Data.Class.Solvable
-import Grisette.Core.Data.Class.ToCon
-import Grisette.Core.Data.Class.ToSym
-import {-# SOURCE #-} Grisette.IR.SymPrim.Data.SymPrim
+  ( SimpleMergeable,
+    mrgSingle,
+  )
+import Grisette.Core.Data.Class.Solvable (Solvable (con))
+import Grisette.Core.Data.Class.ToCon (ToCon)
+import Grisette.Core.Data.Class.ToSym (ToSym)
+import {-# SOURCE #-} Grisette.IR.SymPrim.Data.SymPrim (SymBool)
 
 -- $setup
 -- >>> import Grisette.Core
diff --git a/src/Grisette/Core/Control/Monad/CBMCExcept.hs b/src/Grisette/Core/Control/Monad/CBMCExcept.hs
--- a/src/Grisette/Core/Control/Monad/CBMCExcept.hs
+++ b/src/Grisette/Core/Control/Monad/CBMCExcept.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE CPP #-}
 {-# LANGUAGE DeriveGeneric #-}
 {-# LANGUAGE DeriveLift #-}
 {-# LANGUAGE DerivingStrategies #-}
@@ -30,30 +31,70 @@
   )
 where
 
+#if MIN_VERSION_base(4,18,0)
 import Control.Applicative
-import Control.DeepSeq
-import Control.Monad
+  ( Alternative (empty, (<|>)),
+  )
+#else
+import Control.Applicative
+  ( Alternative (empty, (<|>)),
+    Applicative (liftA2),
+  )
+#endif
+import Control.DeepSeq (NFData)
+import Control.Monad (MonadPlus (mplus, mzero))
 import qualified Control.Monad.Except as OrigExcept
 import qualified Control.Monad.Fail as Fail
-import Control.Monad.Fix
-import Control.Monad.Trans
-import Control.Monad.Zip
+import Control.Monad.Fix (MonadFix (mfix))
+import Control.Monad.Trans (MonadIO (liftIO), MonadTrans (lift))
+import Control.Monad.Zip (MonadZip (mzipWith))
 import Data.Functor.Classes
-import Data.Functor.Contravariant
-import Data.Hashable
-import GHC.Generics
-import Grisette.Core.Data.Class.Bool
-import Grisette.Core.Data.Class.Evaluate
+  ( Eq1 (liftEq),
+    Ord1 (liftCompare),
+    Read1 (liftReadList, liftReadsPrec),
+    Show1 (liftShowList, liftShowsPrec),
+    compare1,
+    eq1,
+    readsData,
+    readsPrec1,
+    readsUnaryWith,
+    showsPrec1,
+    showsUnaryWith,
+  )
+import Data.Functor.Contravariant (Contravariant (contramap))
+import Data.Hashable (Hashable)
+import GHC.Generics (Generic, Generic1)
+import Grisette.Core.Data.Class.Bool (SEq ((==~)))
+import Grisette.Core.Data.Class.Evaluate (EvaluateSym (evaluateSym))
 import Grisette.Core.Data.Class.ExtractSymbolics
+  ( ExtractSymbolics (extractSymbolics),
+  )
 import Grisette.Core.Data.Class.GenSym
+  ( GenSym (fresh),
+    GenSymSimple (simpleFresh),
+    derivedNoSpecFresh,
+    derivedSameShapeSimpleFresh,
+  )
 import Grisette.Core.Data.Class.Mergeable
-import Grisette.Core.Data.Class.SOrd
+  ( Mergeable (rootStrategy),
+    Mergeable1 (liftRootStrategy),
+    MergingStrategy (NoStrategy, SimpleStrategy, SortedStrategy),
+    rootStrategy1,
+    wrapStrategy,
+  )
+import Grisette.Core.Data.Class.SOrd (SOrd (symCompare, (<=~), (<~), (>=~), (>~)))
 import Grisette.Core.Data.Class.SimpleMergeable
-import Grisette.Core.Data.Class.Solver
-import Grisette.Core.Data.Class.ToCon
-import Grisette.Core.Data.Class.ToSym
+  ( SimpleMergeable (mrgIte),
+    SimpleMergeable1 (liftMrgIte),
+    UnionLike (mergeWithStrategy, mrgIfWithStrategy, single, unionIf),
+    merge,
+    mrgIf,
+  )
+import Grisette.Core.Data.Class.Solver (UnionWithExcept (extractUnionExcept))
+import Grisette.Core.Data.Class.ToCon (ToCon (toCon))
+import Grisette.Core.Data.Class.ToSym (ToSym (toSym))
 import Language.Haskell.TH.Syntax (Lift)
-import Unsafe.Coerce
+import Unsafe.Coerce (unsafeCoerce)
 
 -- | A wrapper type for 'Either'. Uses different merging strategies.
 newtype CBMCEither a b = CBMCEither {runCBMCEither :: Either a b}
diff --git a/src/Grisette/Core/Control/Monad/Class/MonadParallelUnion.hs b/src/Grisette/Core/Control/Monad/Class/MonadParallelUnion.hs
--- a/src/Grisette/Core/Control/Monad/Class/MonadParallelUnion.hs
+++ b/src/Grisette/Core/Control/Monad/Class/MonadParallelUnion.hs
@@ -13,21 +13,22 @@
   )
 where
 
-import Control.DeepSeq
-import Control.Monad.Cont
-import Control.Monad.Except
-import Control.Monad.Identity
+import Control.DeepSeq (NFData)
+import Control.Monad.Except (ExceptT (ExceptT), runExceptT)
+import Control.Monad.Identity (IdentityT (IdentityT, runIdentityT))
 import qualified Control.Monad.RWS.Lazy as RWSLazy
 import qualified Control.Monad.RWS.Strict as RWSStrict
-import Control.Monad.Reader
+import Control.Monad.Reader (ReaderT (ReaderT, runReaderT))
 import qualified Control.Monad.State.Lazy as StateLazy
 import qualified Control.Monad.State.Strict as StateStrict
-import Control.Monad.Trans.Maybe
+import Control.Monad.Trans.Maybe (MaybeT (MaybeT, runMaybeT))
 import qualified Control.Monad.Writer.Lazy as WriterLazy
 import qualified Control.Monad.Writer.Strict as WriterStrict
-import Grisette.Core.Data.Class.Mergeable
+import Grisette.Core.Data.Class.Mergeable (Mergeable)
 import Grisette.Core.Data.Class.SimpleMergeable
-import Grisette.Lib.Control.Monad
+  ( UnionLike,
+    merge,
+  )
 
 -- | Parallel union monad.
 --
diff --git a/src/Grisette/Core/Control/Monad/Union.hs b/src/Grisette/Core/Control/Monad/Union.hs
--- a/src/Grisette/Core/Control/Monad/Union.hs
+++ b/src/Grisette/Core/Control/Monad/Union.hs
@@ -19,7 +19,7 @@
   )
 where
 
-import Grisette.Core.Data.Class.SimpleMergeable
+import Grisette.Core.Data.Class.SimpleMergeable (UnionLike)
 
 -- $setup
 -- >>> import Grisette.Core
diff --git a/src/Grisette/Core/Control/Monad/UnionM.hs b/src/Grisette/Core/Control/Monad/UnionM.hs
--- a/src/Grisette/Core/Control/Monad/UnionM.hs
+++ b/src/Grisette/Core/Control/Monad/UnionM.hs
@@ -8,6 +8,7 @@
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TemplateHaskellQuotes #-}
 {-# LANGUAGE Trustworthy #-}
@@ -38,47 +39,92 @@
   )
 where
 
-import Control.DeepSeq
-import Control.Monad.Identity (Identity (..))
-import Control.Parallel.Strategies
+import Control.DeepSeq (NFData (rnf), NFData1 (liftRnf), force, rnf1)
+import Control.Parallel.Strategies (rpar, rseq, runEval)
 import Data.Functor.Classes
+  ( Eq1 (liftEq),
+    Show1 (liftShowsPrec),
+    showsPrec1,
+  )
 import qualified Data.HashMap.Lazy as HML
-import Data.Hashable
-import Data.IORef
-import Data.String
-import GHC.IO hiding (evaluate)
-import GHC.TypeNats
+import Data.Hashable (Hashable (hashWithSalt))
+import Data.String (IsString (fromString))
+import GHC.TypeNats (KnownNat, type (<=))
 import Grisette.Core.Control.Monad.CBMCExcept
+  ( CBMCEither (runCBMCEither),
+  )
 import Grisette.Core.Control.Monad.Class.MonadParallelUnion
-import Grisette.Core.Control.Monad.Union
-import Grisette.Core.Data.BV
+  ( MonadParallelUnion (parBindUnion),
+  )
+import Grisette.Core.Control.Monad.Union (MonadUnion)
+import Grisette.Core.Data.BV (IntN, WordN)
 import Grisette.Core.Data.Class.Bool
-import Grisette.Core.Data.Class.Evaluate
+  ( ITEOp (ites),
+    LogicalOp (implies, nots, xors, (&&~), (||~)),
+    SEq ((==~)),
+  )
+import Grisette.Core.Data.Class.Evaluate (EvaluateSym (evaluateSym))
 import Grisette.Core.Data.Class.ExtractSymbolics
-import Grisette.Core.Data.Class.Function
+  ( ExtractSymbolics (extractSymbolics),
+  )
+import Grisette.Core.Data.Class.Function (Function (Arg, Ret, (#)))
 import Grisette.Core.Data.Class.GPretty
+  ( GPretty (gpretty),
+    groupedEnclose,
+  )
 import Grisette.Core.Data.Class.GenSym
+  ( GenSym (fresh),
+    GenSymSimple (simpleFresh),
+  )
 import Grisette.Core.Data.Class.Mergeable
+  ( Mergeable (rootStrategy),
+    Mergeable1 (liftRootStrategy),
+    MergingStrategy (SimpleStrategy),
+  )
 import Grisette.Core.Data.Class.SOrd
+  ( SOrd (symCompare, (<=~), (<~), (>=~), (>~)),
+  )
 import Grisette.Core.Data.Class.SimpleMergeable
+  ( SimpleMergeable (mrgIte),
+    SimpleMergeable1 (liftMrgIte),
+    UnionLike (mergeWithStrategy, mrgIfWithStrategy, single, unionIf),
+    UnionPrjOp (ifView, leftMost, singleView),
+    merge,
+    mrgIf,
+    mrgSingle,
+    simpleMerge,
+    (#~),
+  )
 import Grisette.Core.Data.Class.Solvable
-import Grisette.Core.Data.Class.Solver
-import Grisette.Core.Data.Class.Substitute
-import Grisette.Core.Data.Class.ToCon
-import Grisette.Core.Data.Class.ToSym
+  ( Solvable (con, conView, iinfosym, isym, sinfosym, ssym),
+    pattern Con,
+  )
+import Grisette.Core.Data.Class.Solver (UnionWithExcept (extractUnionExcept))
+import Grisette.Core.Data.Class.ToCon (ToCon (toCon))
+import Grisette.Core.Data.Class.ToSym (ToSym (toSym))
 import Grisette.Core.Data.Union
+  ( Union (If, Single),
+    fullReconstruct,
+    ifWithStrategy,
+  )
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
+  ( LinkedRep,
+    SupportedPrim,
+    type (-->),
+  )
 import Grisette.IR.SymPrim.Data.SymPrim
-import Grisette.IR.SymPrim.Data.TabularFun
-import Language.Haskell.TH.Syntax
+  ( AllSyms (allSymsS),
+    SymBool,
+    SymIntN,
+    SymInteger,
+    SymWordN,
+    type (-~>),
+    type (=~>),
+  )
+import Grisette.IR.SymPrim.Data.TabularFun (type (=->))
+import Language.Haskell.TH.Syntax (Lift (lift, liftTyped))
 import Language.Haskell.TH.Syntax.Compat (unTypeSplice)
 
-#if MIN_VERSION_prettyprinter(1,7,0)
-import Prettyprinter
-#else
-import Data.Text.Prettyprint.Doc
-#endif
-
 -- $setup
 -- >>> import Grisette.Core
 -- >>> import Grisette.IR.SymPrim
@@ -238,11 +284,11 @@
 wrapBracket l r p = showChar l . p . showChar r
 
 instance Show1 UnionM where
-  liftShowsPrec sp sl i (UAny a) =
+  liftShowsPrec sp sl _ (UAny a) =
     wrapBracket '<' '>'
       . liftShowsPrecUnion sp sl 0
       $ a
-  liftShowsPrec sp sl i (UMrg _ a) =
+  liftShowsPrec sp sl _ (UMrg _ a) =
     wrapBracket '{' '}'
       . liftShowsPrecUnion sp sl 0
       $ a
diff --git a/src/Grisette/Core/Control/Monad/UnionM.hs-boot b/src/Grisette/Core/Control/Monad/UnionM.hs-boot
--- a/src/Grisette/Core/Control/Monad/UnionM.hs-boot
+++ b/src/Grisette/Core/Control/Monad/UnionM.hs-boot
@@ -4,11 +4,9 @@
 
 module Grisette.Core.Control.Monad.UnionM (UnionM (..)) where
 
-import Data.IORef
-import Grisette.Core.Data.Class.Bool
-import Grisette.Core.Data.Class.Mergeable
-import Grisette.Core.Data.Class.SimpleMergeable
-import Grisette.Core.Data.Union
+import Grisette.Core.Data.Class.Mergeable (MergingStrategy)
+import Grisette.Core.Data.Class.SimpleMergeable (UnionLike)
+import Grisette.Core.Data.Union (Union)
 
 data UnionM a where
   -- | 'UnionM' with no 'Mergeable' knowledge.
diff --git a/src/Grisette/Core/Data/BV.hs b/src/Grisette/Core/Data/BV.hs
--- a/src/Grisette/Core/Data/BV.hs
+++ b/src/Grisette/Core/Data/BV.hs
@@ -44,28 +44,92 @@
   )
 where
 
-import Control.Applicative
-import Control.DeepSeq
+import Control.Applicative (Alternative ((<|>)))
+import Control.DeepSeq (NFData (rnf))
 import Control.Exception
+  ( ArithException (Overflow),
+    Exception (displayException),
+    throw,
+  )
 import Data.Bits
-import Data.CallStack
-import Data.Hashable
-import Data.Maybe
-import Data.Proxy
-import Data.Typeable
+  ( Bits
+      ( bit,
+        bitSize,
+        bitSizeMaybe,
+        clearBit,
+        complement,
+        complementBit,
+        isSigned,
+        popCount,
+        rotate,
+        rotateL,
+        rotateR,
+        setBit,
+        shift,
+        shiftL,
+        shiftR,
+        testBit,
+        unsafeShiftL,
+        unsafeShiftR,
+        xor,
+        zeroBits,
+        (.&.),
+        (.|.)
+      ),
+    FiniteBits (countLeadingZeros, countTrailingZeros, finiteBitSize),
+  )
+import Data.Hashable (Hashable (hashWithSalt))
+import Data.Maybe (fromMaybe, isJust)
+import Data.Proxy (Proxy (Proxy))
+import Data.Typeable (type (:~:) (Refl))
 import GHC.Enum
-import GHC.Generics
+  ( boundedEnumFrom,
+    boundedEnumFromThen,
+    predError,
+    succError,
+    toEnumError,
+  )
+import GHC.Generics (Generic)
 import GHC.Read
-import GHC.Real
+  ( Read (readListPrec, readPrec),
+    parens,
+    readListDefault,
+    readListPrecDefault,
+    readNumber,
+  )
+import GHC.Real ((%))
 import GHC.TypeNats
+  ( KnownNat,
+    Nat,
+    natVal,
+    sameNat,
+    type (+),
+    type (<=),
+  )
 import Grisette.Core.Data.Class.BitVector
+  ( BV (bvConcat, bvExt, bvSelect, bvSext, bvZext),
+    BVSignConversion (toSigned, toUnsigned),
+    SizedBV (sizedBVConcat, sizedBVExt, sizedBVSelect, sizedBVSext, sizedBVZext),
+  )
 import Grisette.Utils.Parameterized
-import Language.Haskell.TH.Syntax
-import Numeric
+  ( KnownProof (KnownProof),
+    LeqProof (LeqProof),
+    knownAdd,
+    leqAddPos,
+    unsafeKnownProof,
+    unsafeLeqProof,
+  )
+import Language.Haskell.TH.Syntax (Lift (liftTyped))
+import Numeric (showHex, showIntAtBase)
 import qualified Test.QuickCheck as QC
-import Text.ParserCombinators.ReadP (skipSpaces, string)
+import Text.ParserCombinators.ReadP (string)
 import Text.ParserCombinators.ReadPrec
-import Text.Read
+  ( ReadPrec,
+    get,
+    look,
+    pfail,
+  )
+import Text.Read (lift)
 import qualified Text.Read.Lex as L
 
 data BitwidthMismatch = BitwidthMismatch
@@ -84,29 +148,29 @@
 data SomeWordN where
   SomeWordN :: (KnownNat n, 1 <= n) => WordN n -> SomeWordN
 
-unarySomeWordN :: (HasCallStack) => (forall n. (KnownNat n, 1 <= n) => WordN n -> r) -> SomeWordN -> r
+unarySomeWordN :: (forall n. (KnownNat n, 1 <= n) => WordN n -> r) -> SomeWordN -> r
 unarySomeWordN op (SomeWordN (w :: WordN w)) = op w
 {-# INLINE unarySomeWordN #-}
 
-unarySomeWordNR1 :: (HasCallStack) => (forall n. (KnownNat n, 1 <= n) => WordN n -> WordN n) -> SomeWordN -> SomeWordN
+unarySomeWordNR1 :: (forall n. (KnownNat n, 1 <= n) => WordN n -> WordN n) -> SomeWordN -> SomeWordN
 unarySomeWordNR1 op (SomeWordN (w :: WordN w)) = SomeWordN $ op w
 {-# INLINE unarySomeWordNR1 #-}
 
-binSomeWordN :: (HasCallStack) => (forall n. (KnownNat n, 1 <= n) => WordN n -> WordN n -> r) -> SomeWordN -> SomeWordN -> r
+binSomeWordN :: (forall n. (KnownNat n, 1 <= n) => WordN n -> WordN n -> r) -> SomeWordN -> SomeWordN -> r
 binSomeWordN op (SomeWordN (l :: WordN l)) (SomeWordN (r :: WordN r)) =
   case sameNat (Proxy @l) (Proxy @r) of
     Just Refl -> op l r
     Nothing -> throw BitwidthMismatch
 {-# INLINE binSomeWordN #-}
 
-binSomeWordNR1 :: (HasCallStack) => (forall n. (KnownNat n, 1 <= n) => WordN n -> WordN n -> WordN n) -> SomeWordN -> SomeWordN -> SomeWordN
+binSomeWordNR1 :: (forall n. (KnownNat n, 1 <= n) => WordN n -> WordN n -> WordN n) -> SomeWordN -> SomeWordN -> SomeWordN
 binSomeWordNR1 op (SomeWordN (l :: WordN l)) (SomeWordN (r :: WordN r)) =
   case sameNat (Proxy @l) (Proxy @r) of
     Just Refl -> SomeWordN $ op l r
     Nothing -> throw BitwidthMismatch
 {-# INLINE binSomeWordNR1 #-}
 
-binSomeWordNR2 :: (HasCallStack) => (forall n. (KnownNat n, 1 <= n) => WordN n -> WordN n -> (WordN n, WordN n)) -> SomeWordN -> SomeWordN -> (SomeWordN, SomeWordN)
+binSomeWordNR2 :: (forall n. (KnownNat n, 1 <= n) => WordN n -> WordN n -> (WordN n, WordN n)) -> SomeWordN -> SomeWordN -> (SomeWordN, SomeWordN)
 binSomeWordNR2 op (SomeWordN (l :: WordN l)) (SomeWordN (r :: WordN r)) =
   case sameNat (Proxy @l) (Proxy @r) of
     Just Refl ->
@@ -699,7 +763,7 @@
     where
       n = fromIntegral $ natVal (Proxy @n)
       res :: forall (w :: Nat) (ix :: Nat). Proxy w -> Proxy ix -> SomeWordN
-      res p1 p2 =
+      res _ _ =
         case ( unsafeKnownProof @ix (fromIntegral ix),
                unsafeKnownProof @w (fromIntegral w),
                unsafeLeqProof @1 @w,
@@ -709,7 +773,7 @@
             SomeWordN $ sizedBVSelect (Proxy @ix) (Proxy @w) a
 
 instance BV SomeIntN where
-  bvConcat l r = toSigned $ bvConcat (toUnsigned l) (toUnsigned l)
+  bvConcat l r = toSigned $ bvConcat (toUnsigned l) (toUnsigned r)
   {-# INLINE bvConcat #-}
   bvZext l = toSigned . bvZext l . toUnsigned
   {-# INLINE bvZext #-}
diff --git a/src/Grisette/Core/Data/Class/BitVector.hs b/src/Grisette/Core/Data/Class/BitVector.hs
--- a/src/Grisette/Core/Data/Class/BitVector.hs
+++ b/src/Grisette/Core/Data/Class/BitVector.hs
@@ -28,9 +28,17 @@
   )
 where
 
-import Data.Proxy
-import GHC.TypeNats
+import Data.Proxy (Proxy (Proxy))
+import GHC.TypeNats (KnownNat, type (+), type (-), type (<=))
 import Grisette.Utils.Parameterized
+  ( KnownProof (KnownProof),
+    LeqProof (LeqProof),
+    addNat,
+    hasRepr,
+    natRepr,
+    subNat,
+    unsafeLeqProof,
+  )
 
 -- $setup
 -- >>> import Grisette.Core
diff --git a/src/Grisette/Core/Data/Class/Bool.hs b/src/Grisette/Core/Data/Class/Bool.hs
--- a/src/Grisette/Core/Data/Class/Bool.hs
+++ b/src/Grisette/Core/Data/Class/Bool.hs
@@ -30,27 +30,59 @@
   )
 where
 
-import Control.Monad.Except
+import Control.Monad.Except (ExceptT (ExceptT))
 import Control.Monad.Identity
   ( Identity (Identity),
     IdentityT (IdentityT),
   )
-import Control.Monad.Trans.Maybe
+import Control.Monad.Trans.Maybe (MaybeT (MaybeT))
 import qualified Control.Monad.Writer.Lazy as WriterLazy
 import qualified Control.Monad.Writer.Strict as WriterStrict
 import qualified Data.ByteString as B
-import Data.Functor.Sum
-import Data.Int
+import Data.Functor.Sum (Sum)
+import Data.Int (Int16, Int32, Int64, Int8)
 import qualified Data.Text as T
-import Data.Word
-import GHC.TypeNats
+import Data.Word (Word16, Word32, Word64, Word8)
+import GHC.TypeNats (KnownNat, type (<=))
 import Generics.Deriving
-import Grisette.Core.Data.BV
+  ( Default (Default),
+    Generic (Rep, from),
+    K1 (K1),
+    M1 (M1),
+    U1,
+    V1,
+    type (:*:) ((:*:)),
+    type (:+:) (L1, R1),
+  )
+import Grisette.Core.Data.BV (IntN, SomeIntN, SomeWordN, WordN)
 import {-# SOURCE #-} Grisette.Core.Data.Class.SimpleMergeable
-import Grisette.Core.Data.Class.Solvable
+  ( SimpleMergeable,
+  )
+import Grisette.Core.Data.Class.Solvable (Solvable (con))
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
+  ( LinkedRep,
+    SupportedPrim,
+  )
 import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bool
+  ( pevalAndTerm,
+    pevalITETerm,
+    pevalImplyTerm,
+    pevalNotTerm,
+    pevalOrTerm,
+    pevalXorTerm,
+  )
 import {-# SOURCE #-} Grisette.IR.SymPrim.Data.SymPrim
+  ( SomeSymIntN,
+    SomeSymWordN,
+    SymBool (SymBool),
+    SymIntN (SymIntN),
+    SymInteger (SymInteger),
+    SymWordN (SymWordN),
+    binSomeSymIntNR1,
+    binSomeSymWordNR1,
+    type (-~>) (SymGeneralFun),
+    type (=~>) (SymTabularFun),
+  )
 
 -- $setup
 -- >>> import Grisette.Core
diff --git a/src/Grisette/Core/Data/Class/Bool.hs-boot b/src/Grisette/Core/Data/Class/Bool.hs-boot
--- a/src/Grisette/Core/Data/Class/Bool.hs-boot
+++ b/src/Grisette/Core/Data/Class/Bool.hs-boot
@@ -1,6 +1,6 @@
-module Grisette.Core.Data.Class.Bool (LogicalOp (..)) where
+module Grisette.Core.Data.Class.Bool (LogicalOp (..), ITEOp (..)) where
 
-import {-# SOURCE #-} Grisette.IR.SymPrim.Data.SymPrim
+import {-# SOURCE #-} Grisette.IR.SymPrim.Data.SymPrim (SymBool)
 
 class LogicalOp b where
   -- | Symbolic disjunction
diff --git a/src/Grisette/Core/Data/Class/CEGISSolver.hs b/src/Grisette/Core/Data/Class/CEGISSolver.hs
--- a/src/Grisette/Core/Data/Class/CEGISSolver.hs
+++ b/src/Grisette/Core/Data/Class/CEGISSolver.hs
@@ -39,18 +39,25 @@
   )
 where
 
-import GHC.Generics
-import Generics.Deriving
+import GHC.Generics (Generic)
+import Generics.Deriving (Default (Default))
 import Grisette.Core.Control.Exception
-import Grisette.Core.Data.Class.Bool
-import Grisette.Core.Data.Class.Evaluate
+  ( VerificationConditions (AssertionViolation, AssumptionViolation),
+  )
+import Grisette.Core.Data.Class.Evaluate (EvaluateSym)
 import Grisette.Core.Data.Class.ExtractSymbolics
-import Grisette.Core.Data.Class.Mergeable
+  ( ExtractSymbolics,
+  )
+import Grisette.Core.Data.Class.Mergeable (Mergeable)
 import Grisette.Core.Data.Class.SimpleMergeable
-import Grisette.Core.Data.Class.Solvable
-import Grisette.Core.Data.Class.Solver
-import Grisette.IR.SymPrim.Data.Prim.Model
-import Grisette.IR.SymPrim.Data.SymPrim
+  ( SimpleMergeable,
+    UnionPrjOp,
+    simpleMerge,
+  )
+import Grisette.Core.Data.Class.Solvable (Solvable (con))
+import Grisette.Core.Data.Class.Solver (UnionWithExcept (extractUnionExcept))
+import Grisette.IR.SymPrim.Data.Prim.Model (Model)
+import Grisette.IR.SymPrim.Data.SymPrim (SymBool)
 
 -- $setup
 -- >>> import Grisette.Core
diff --git a/src/Grisette/Core/Data/Class/Error.hs b/src/Grisette/Core/Data/Class/Error.hs
--- a/src/Grisette/Core/Data/Class/Error.hs
+++ b/src/Grisette/Core/Data/Class/Error.hs
@@ -21,17 +21,17 @@
   )
 where
 
-import Control.Monad.Except
-import Grisette.Core.Control.Monad.Union
-import Grisette.Core.Data.Class.Bool
-import Grisette.Core.Data.Class.Mergeable
-import Grisette.Core.Data.Class.SimpleMergeable
-import {-# SOURCE #-} Grisette.IR.SymPrim.Data.SymPrim
+import Control.Monad.Except (MonadError (throwError))
+import Grisette.Core.Control.Monad.Union (MonadUnion)
+import Grisette.Core.Data.Class.Mergeable (Mergeable)
+import Grisette.Core.Data.Class.SimpleMergeable (merge, mrgIf)
+import {-# SOURCE #-} Grisette.IR.SymPrim.Data.SymPrim (SymBool)
 
 -- $setup
 -- >>> import Control.Exception
 -- >>> import Grisette.Core
 -- >>> import Grisette.IR.SymPrim
+-- >>> import Control.Monad.Except
 -- >>> :set -XOverloadedStrings
 -- >>> :set -XFlexibleContexts
 
diff --git a/src/Grisette/Core/Data/Class/Evaluate.hs b/src/Grisette/Core/Data/Class/Evaluate.hs
--- a/src/Grisette/Core/Data/Class/Evaluate.hs
+++ b/src/Grisette/Core/Data/Class/Evaluate.hs
@@ -25,24 +25,34 @@
   )
 where
 
-import Control.Monad.Except
+import Control.Monad.Except (ExceptT (ExceptT))
 import Control.Monad.Identity
-import Control.Monad.Trans.Maybe
+  ( Identity (Identity),
+    IdentityT (IdentityT),
+  )
+import Control.Monad.Trans.Maybe (MaybeT (MaybeT))
 import qualified Control.Monad.Writer.Lazy as WriterLazy
 import qualified Control.Monad.Writer.Strict as WriterStrict
 import qualified Data.ByteString as B
-import Data.Functor.Sum
-import Data.Int
-import Data.Maybe
+import Data.Functor.Sum (Sum)
+import Data.Int (Int16, Int32, Int64, Int8)
+import Data.Maybe (fromJust)
 import qualified Data.Text as T
-import Data.Word
-import GHC.TypeNats
+import Data.Word (Word16, Word32, Word64, Word8)
+import GHC.TypeNats (KnownNat, type (<=))
 import Generics.Deriving
+  ( Default (Default, unDefault),
+    Generic (Rep, from, to),
+    K1 (K1),
+    M1 (M1),
+    U1,
+    type (:*:) ((:*:)),
+    type (:+:) (L1, R1),
+  )
 import Generics.Deriving.Instances ()
-import Grisette.Core.Data.BV
-import Grisette.Core.Data.Class.ModelOps
-import Grisette.Core.Data.Class.ToCon
-import Grisette.IR.SymPrim.Data.Prim.Model
+import Grisette.Core.Data.BV (IntN, SomeIntN, SomeWordN, WordN)
+import Grisette.Core.Data.Class.ToCon (ToCon (toCon))
+import Grisette.IR.SymPrim.Data.Prim.Model (Model)
 
 -- $setup
 -- >>> import Grisette.Core
diff --git a/src/Grisette/Core/Data/Class/ExtractSymbolics.hs b/src/Grisette/Core/Data/Class/ExtractSymbolics.hs
--- a/src/Grisette/Core/Data/Class/ExtractSymbolics.hs
+++ b/src/Grisette/Core/Data/Class/ExtractSymbolics.hs
@@ -24,20 +24,33 @@
   )
 where
 
-import Control.Monad.Except
+import Control.Monad.Except (ExceptT (ExceptT))
 import Control.Monad.Identity
-import Control.Monad.Trans.Maybe
+  ( Identity (Identity),
+    IdentityT (IdentityT),
+  )
+import Control.Monad.Trans.Maybe (MaybeT (MaybeT))
 import qualified Control.Monad.Writer.Lazy as WriterLazy
 import qualified Control.Monad.Writer.Strict as WriterStrict
 import qualified Data.ByteString as B
-import Data.Functor.Sum
-import Data.Int
+import Data.Functor.Sum (Sum)
+import Data.Int (Int16, Int32, Int64, Int8)
 import qualified Data.Text as T
-import Data.Word
-import GHC.TypeNats
+import Data.Word (Word16, Word32, Word64, Word8)
+import GHC.TypeNats (KnownNat, type (<=))
 import Generics.Deriving
-import Grisette.Core.Data.BV
+  ( Default (Default, unDefault),
+    Generic (Rep, from),
+    K1 (unK1),
+    M1 (unM1),
+    U1,
+    type (:*:) ((:*:)),
+    type (:+:) (L1, R1),
+  )
+import Grisette.Core.Data.BV (IntN, SomeIntN, SomeWordN, WordN)
 import {-# SOURCE #-} Grisette.IR.SymPrim.Data.Prim.Model
+  ( SymbolSet,
+  )
 
 -- $setup
 -- >>> import Grisette.Core
diff --git a/src/Grisette/Core/Data/Class/GPretty.hs b/src/Grisette/Core/Data/Class/GPretty.hs
--- a/src/Grisette/Core/Data/Class/GPretty.hs
+++ b/src/Grisette/Core/Data/Class/GPretty.hs
@@ -18,27 +18,68 @@
   )
 where
 
-import Control.Monad.Except
+import Control.Monad.Except (ExceptT (ExceptT))
 import Control.Monad.Identity
-import Control.Monad.Trans.Maybe
+  ( Identity (Identity),
+    IdentityT (IdentityT),
+  )
+import Control.Monad.Trans.Maybe (MaybeT (MaybeT))
 import qualified Control.Monad.Writer.Lazy as WriterLazy
 import qualified Control.Monad.Writer.Strict as WriterStrict
 import qualified Data.ByteString as B
-import Data.Functor.Sum
-import Data.Int
-import Data.Proxy
-import Data.String
+import Data.Functor.Sum (Sum)
+import Data.Int (Int16, Int32, Int64, Int8)
+import Data.String (IsString (fromString))
 import qualified Data.Text as T
-import Data.Word
+import Data.Word (Word16, Word32, Word64, Word8)
 import GHC.Generics
-import GHC.TypeLits
-import Generics.Deriving hiding (isNullary)
-import Grisette.Core.Data.BV
+  ( C,
+    C1,
+    Constructor (conFixity, conIsRecord, conName),
+    D,
+    Fixity (Infix, Prefix),
+    Generic (Rep, from),
+    K1 (K1),
+    M1 (M1),
+    S,
+    Selector (selName),
+    U1 (U1),
+    V1,
+    type (:*:) ((:*:)),
+    type (:+:) (L1, R1),
+  )
+import GHC.TypeLits (KnownNat, type (<=))
+import Generics.Deriving (Default (Default, unDefault))
+import Grisette.Core.Data.BV (IntN, SomeIntN, SomeWordN, WordN)
 
 #if MIN_VERSION_prettyprinter(1,7,0)
 import Prettyprinter
+  ( (<+>),
+    align,
+    encloseSep,
+    flatAlt,
+    group,
+    nest,
+    vcat,
+    viaShow,
+    vsep,
+    Doc,
+    Pretty(pretty),
+  )
 #else
 import Data.Text.Prettyprint.Doc
+  ( (<+>),
+    align,
+    encloseSep,
+    flatAlt,
+    group,
+    nest,
+    vcat,
+    viaShow,
+    vsep,
+    Doc,
+    Pretty(pretty),
+  )
 #endif
 
 glist :: [Doc ann] -> Doc ann
@@ -153,7 +194,7 @@
           [ gprettyPrec' t n a,
             pretty s <+> gprettyPrec' t n b
           ]
-  gprettyPrec' t@Tup n (a :*: b) =
+  gprettyPrec' t@Tup _ (a :*: b) =
     vcat
       [ gprettyPrec' t 0 a,
         "," <> flatAlt " " "" <> gprettyPrec' t 0 b
@@ -309,7 +350,7 @@
   (GPretty (m (Maybe a))) =>
   GPretty (MaybeT m a)
   where
-  gprettyPrec i (MaybeT a) =
+  gprettyPrec _ (MaybeT a) =
     group $
       nest 2 $
         vsep
@@ -322,7 +363,7 @@
   (GPretty (m (Either e a))) =>
   GPretty (ExceptT e m a)
   where
-  gprettyPrec i (ExceptT a) =
+  gprettyPrec _ (ExceptT a) =
     group $
       nest 2 $
         vsep
@@ -335,7 +376,7 @@
   (GPretty (m (a, w))) =>
   GPretty (WriterLazy.WriterT w m a)
   where
-  gprettyPrec i (WriterLazy.WriterT a) =
+  gprettyPrec _ (WriterLazy.WriterT a) =
     group $
       nest 2 $
         vsep
@@ -347,7 +388,7 @@
   (GPretty (m (a, w))) =>
   GPretty (WriterStrict.WriterT w m a)
   where
-  gprettyPrec i (WriterStrict.WriterT a) =
+  gprettyPrec _ (WriterStrict.WriterT a) =
     group $
       nest 2 $
         vsep
@@ -357,7 +398,7 @@
 
 -- Identity
 instance (GPretty a) => GPretty (Identity a) where
-  gprettyPrec i (Identity a) =
+  gprettyPrec _ (Identity a) =
     group $
       nest 2 $
         vsep
@@ -367,7 +408,7 @@
 
 -- IdentityT
 instance (GPretty (m a)) => GPretty (IdentityT m a) where
-  gprettyPrec i (IdentityT a) =
+  gprettyPrec _ (IdentityT a) =
     group $
       nest 2 $
         vsep
diff --git a/src/Grisette/Core/Data/Class/GenSym.hs b/src/Grisette/Core/Data/Class/GenSym.hs
--- a/src/Grisette/Core/Data/Class/GenSym.hs
+++ b/src/Grisette/Core/Data/Class/GenSym.hs
@@ -66,43 +66,97 @@
   )
 where
 
-import Control.DeepSeq
-import Control.Monad.Cont
+import Control.DeepSeq (NFData (rnf))
 import Control.Monad.Except
-import Control.Monad.Identity
+  ( ExceptT (ExceptT),
+    MonadError (catchError, throwError),
+  )
+import Control.Monad.Identity (Identity (runIdentity))
 import Control.Monad.RWS.Class
+  ( MonadRWS,
+    MonadReader (ask, local),
+    MonadState (get, put),
+    MonadWriter (listen, pass, writer),
+    asks,
+    gets,
+  )
 import qualified Control.Monad.RWS.Lazy as RWSLazy
 import qualified Control.Monad.RWS.Strict as RWSStrict
-import Control.Monad.Reader
-import Control.Monad.Signatures
-import Control.Monad.State
+import Control.Monad.Reader (ReaderT (ReaderT))
+import Control.Monad.Signatures (Catch)
 import qualified Control.Monad.State.Lazy as StateLazy
 import qualified Control.Monad.State.Strict as StateStrict
-import Control.Monad.Trans.Maybe
-import Control.Monad.Writer
+import Control.Monad.Trans.Class
+  ( MonadTrans (lift),
+  )
+import Control.Monad.Trans.Maybe (MaybeT (MaybeT))
 import qualified Control.Monad.Writer.Lazy as WriterLazy
 import qualified Control.Monad.Writer.Strict as WriterStrict
-import Data.Bifunctor
+import Data.Bifunctor (Bifunctor (first))
 import qualified Data.ByteString as B
-import Data.Hashable
-import Data.Int
-import Data.String
+import Data.Hashable (Hashable (hashWithSalt))
+import Data.Int (Int16, Int32, Int64, Int8)
+import Data.String (IsString (fromString))
 import qualified Data.Text as T
 import Data.Typeable
-import Data.Word
-import GHC.TypeNats
-import Generics.Deriving hiding (index)
-import Grisette.Core.Control.Monad.Union
-import {-# SOURCE #-} Grisette.Core.Control.Monad.UnionM
-import Grisette.Core.Data.BV
-import Grisette.Core.Data.Class.Bool
+  ( Proxy (Proxy),
+    Typeable,
+    eqT,
+    typeRep,
+    type (:~:) (Refl),
+  )
+import Data.Word (Word16, Word32, Word64, Word8)
+import GHC.TypeNats (KnownNat, Nat, type (<=))
+import Generics.Deriving
+  ( Generic (Rep, from, to),
+    K1 (K1),
+    M1 (M1),
+    U1 (U1),
+    type (:*:) ((:*:)),
+    type (:+:) (L1, R1),
+  )
+import {-# SOURCE #-} Grisette.Core.Control.Monad.UnionM (UnionM)
+import Grisette.Core.Data.BV (IntN, SomeIntN, SomeWordN, WordN)
 import Grisette.Core.Data.Class.Mergeable
+  ( Mergeable (rootStrategy),
+    Mergeable1 (liftRootStrategy),
+    Mergeable2 (liftRootStrategy2),
+    MergingStrategy (SimpleStrategy),
+    rootStrategy1,
+    wrapStrategy,
+  )
 import Grisette.Core.Data.Class.SimpleMergeable
+  ( SimpleMergeable (mrgIte),
+    SimpleMergeable1 (liftMrgIte),
+    UnionLike (mergeWithStrategy, mrgIfWithStrategy, single, unionIf),
+    merge,
+    mrgIf,
+    mrgSingle,
+  )
 import Grisette.Core.Data.Class.Solvable
+  ( Solvable (iinfosym, isym),
+  )
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
+  ( LinkedRep,
+    SupportedPrim,
+  )
 import {-# SOURCE #-} Grisette.IR.SymPrim.Data.SymPrim
-import Grisette.Utils
-import Language.Haskell.TH.Syntax hiding (lift)
+  ( SomeSymIntN (SomeSymIntN),
+    SomeSymWordN (SomeSymWordN),
+    SymBool,
+    SymIntN,
+    SymInteger,
+    SymWordN,
+    type (-~>),
+    type (=~>),
+  )
+import Grisette.Utils.Parameterized
+  ( KnownProof (KnownProof),
+    LeqProof (LeqProof),
+    unsafeKnownProof,
+    unsafeLeqProof,
+  )
+import Language.Haskell.TH.Syntax (Lift (liftTyped))
 
 -- $setup
 -- >>> import Grisette.Core
@@ -305,17 +359,17 @@
   catchError = liftFreshTCache catchError
 
 instance (MonadWriter w m) => MonadWriter w (FreshT m) where
-  writer p = FreshT $ \ident index -> (,index) <$> writer p
+  writer p = FreshT $ \_ index -> (,index) <$> writer p
   listen (FreshT r) = FreshT $ \ident index -> (\((a, b), c) -> ((a, c), b)) <$> listen (r ident index)
   pass (FreshT r) = FreshT $ \ident index -> pass $ (\((a, b), c) -> ((a, c), b)) <$> r ident index
 
 instance (MonadState s m) => MonadState s (FreshT m) where
-  get = FreshT $ \ident index -> gets (,index)
-  put s = FreshT $ \ident index -> (,index) <$> put s
+  get = FreshT $ \_ index -> gets (,index)
+  put s = FreshT $ \_ index -> (,index) <$> put s
 
 instance (MonadReader r m) => MonadReader r (FreshT m) where
   local t (FreshT r) = FreshT $ \ident index -> local t (r ident index)
-  ask = FreshT $ \ident index -> asks (,index)
+  ask = FreshT $ \_ index -> asks (,index)
 
 instance (MonadRWS r w s m) => MonadRWS r w s (FreshT m)
 
@@ -344,12 +398,12 @@
   getFreshIdent = ReaderT $ const getFreshIdent
 
 instance (MonadFresh m, Monoid w) => MonadFresh (RWSLazy.RWST r w s m) where
-  nextFreshIndex = RWSLazy.RWST $ \r s -> (,s,mempty) <$> nextFreshIndex
-  getFreshIdent = RWSLazy.RWST $ \r s -> (,s,mempty) <$> getFreshIdent
+  nextFreshIndex = RWSLazy.RWST $ \_ s -> (,s,mempty) <$> nextFreshIndex
+  getFreshIdent = RWSLazy.RWST $ \_ s -> (,s,mempty) <$> getFreshIdent
 
 instance (MonadFresh m, Monoid w) => MonadFresh (RWSStrict.RWST r w s m) where
-  nextFreshIndex = RWSStrict.RWST $ \r s -> (,s,mempty) <$> nextFreshIndex
-  getFreshIdent = RWSStrict.RWST $ \r s -> (,s,mempty) <$> getFreshIdent
+  nextFreshIndex = RWSStrict.RWST $ \_ s -> (,s,mempty) <$> nextFreshIndex
+  getFreshIdent = RWSStrict.RWST $ \_ s -> (,s,mempty) <$> getFreshIdent
 
 -- | 'FreshT' specialized with Identity.
 type Fresh = FreshT Identity
@@ -482,7 +536,7 @@
   GenSymNoSpec (a :+: b)
   where
   freshNoSpec ::
-    forall m u c.
+    forall m c.
     ( MonadFresh m
     ) =>
     m (UnionM ((a :+: b) c))
@@ -497,7 +551,7 @@
   GenSymNoSpec (a :*: b)
   where
   freshNoSpec ::
-    forall m u c.
+    forall m c.
     ( MonadFresh m
     ) =>
     m (UnionM ((a :*: b) c))
@@ -518,7 +572,7 @@
 --
 -- __Note:__ __Never__ use on recursive types.
 derivedNoSpecFresh ::
-  forall bool a m u.
+  forall a m.
   ( Generic a,
     GenSymNoSpec (Rep a),
     Mergeable a,
@@ -633,7 +687,7 @@
 -- >>> runFresh (chooseFresh [1,2,3]) "a" :: UnionM Integer
 -- {If a@0 1 (If a@1 2 3)}
 chooseFresh ::
-  forall bool a m u.
+  forall a m.
   ( Mergeable a,
     MonadFresh m
   ) =>
@@ -650,7 +704,7 @@
 -- A globally unique identifier should be supplied to ensure the uniqueness of
 -- symbolic constants in the generated symbolic values.
 choose ::
-  forall bool a u.
+  forall a.
   ( Mergeable a
   ) =>
   [a] ->
@@ -707,7 +761,7 @@
 -- >>> runFresh (chooseUnionFresh [a, b]) "c" :: UnionM Integer
 -- {If (&& c@0 a@0) 1 (If (|| c@0 b@0) 2 3)}
 chooseUnionFresh ::
-  forall bool a m u.
+  forall a m.
   ( Mergeable a,
     MonadFresh m
   ) =>
@@ -724,7 +778,7 @@
 -- A globally unique identifier should be supplied to ensure the uniqueness of
 -- symbolic constants in the generated symbolic values.
 chooseUnion ::
-  forall a u.
+  forall a.
   ( Mergeable a
   ) =>
   [UnionM a] ->
@@ -829,6 +883,7 @@
   GenSymSimple (Either aspec bspec) (Either a b)
   where
   simpleFresh (Left a) = Left <$> simpleFresh a
+  simpleFresh (Right b) = Right <$> simpleFresh b
 
 instance
   (GenSym () a, Mergeable a, GenSym () b, Mergeable b) =>
@@ -1631,7 +1686,7 @@
     error "Can only generate bit vectors with positive bit size" \
     where \
       f :: forall p (n :: Nat) m. (MonadFresh m) => p n -> m symtype; \
-      f p = case (unsafeKnownProof @n (fromIntegral i), unsafeLeqProof @1 @n) of \
+      f _ = case (unsafeKnownProof @n (fromIntegral i), unsafeLeqProof @1 @n) of \
         (KnownProof, LeqProof) -> do \
         v :: origtype n <- simpleFresh (); \
         return $ symtype v; \
diff --git a/src/Grisette/Core/Data/Class/Mergeable.hs b/src/Grisette/Core/Data/Class/Mergeable.hs
--- a/src/Grisette/Core/Data/Class/Mergeable.hs
+++ b/src/Grisette/Core/Data/Class/Mergeable.hs
@@ -51,36 +51,90 @@
 where
 
 import Control.Exception
-import Control.Monad.Cont
-import Control.Monad.Except
+  ( ArithException
+      ( Denormal,
+        DivideByZero,
+        LossOfPrecision,
+        Overflow,
+        RatioZeroDenominator,
+        Underflow
+      ),
+  )
+import Control.Monad.Cont (ContT (ContT))
+import Control.Monad.Except (ExceptT (ExceptT), runExceptT)
 import Control.Monad.Identity
+  ( Identity (Identity, runIdentity),
+    IdentityT (IdentityT, runIdentityT),
+  )
 import qualified Control.Monad.RWS.Lazy as RWSLazy
 import qualified Control.Monad.RWS.Strict as RWSStrict
-import Control.Monad.Reader
+import Control.Monad.Reader (ReaderT (ReaderT, runReaderT))
 import qualified Control.Monad.State.Lazy as StateLazy
 import qualified Control.Monad.State.Strict as StateStrict
-import Control.Monad.Trans.Maybe
+import Control.Monad.Trans.Maybe (MaybeT (MaybeT, runMaybeT))
 import qualified Control.Monad.Writer.Lazy as WriterLazy
 import qualified Control.Monad.Writer.Strict as WriterStrict
 import qualified Data.ByteString as B
 import Data.Functor.Classes
-import Data.Functor.Sum
-import Data.Int
-import Data.Kind
+  ( Eq1,
+    Ord1,
+    Show1,
+    compare1,
+    eq1,
+    showsPrec1,
+  )
+import Data.Functor.Sum (Sum (InL, InR))
+import Data.Int (Int16, Int32, Int64, Int8)
+import Data.Kind (Type)
 import qualified Data.Monoid as Monoid
 import qualified Data.Text as T
 import Data.Typeable
-import Data.Word
-import GHC.Natural
-import qualified GHC.TypeLits
-import GHC.TypeNats
+  ( Proxy (Proxy),
+    Typeable,
+    eqT,
+    type (:~:) (Refl),
+  )
+import Data.Word (Word16, Word32, Word64, Word8)
+import GHC.Natural (Natural)
+import GHC.TypeNats (KnownNat, natVal, type (<=))
 import Generics.Deriving
+  ( Default (Default),
+    Default1 (Default1),
+    Generic (Rep, from, to),
+    Generic1 (Rep1, from1, to1),
+    K1 (K1, unK1),
+    M1 (M1, unM1),
+    Par1 (Par1, unPar1),
+    Rec1 (Rec1, unRec1),
+    U1,
+    V1,
+    type (:*:) ((:*:)),
+    type (:+:) (L1, R1),
+  )
 import Grisette.Core.Data.BV
-import Grisette.Core.Data.Class.Bool
+  ( BitwidthMismatch,
+    IntN (IntN),
+    SomeIntN (SomeIntN),
+    SomeWordN (SomeWordN),
+    WordN (WordN),
+  )
+import Grisette.Core.Data.Class.Bool (ITEOp (ites))
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
+  ( LinkedRep,
+    SupportedPrim,
+  )
 import {-# SOURCE #-} Grisette.IR.SymPrim.Data.SymPrim
-import Grisette.Utils
-import Unsafe.Coerce
+  ( SomeSymIntN (SomeSymIntN),
+    SomeSymWordN (SomeSymWordN),
+    SymBool,
+    SymIntN,
+    SymInteger,
+    SymWordN,
+    type (-~>),
+    type (=~>),
+  )
+import Grisette.Utils.Parameterized (unsafeAxiom)
+import Unsafe.Coerce (unsafeCoerce)
 
 -- | Helper type for combining arbitrary number of indices into one.
 -- Useful when trying to write efficient merge strategy for lists/vectors.
@@ -467,20 +521,20 @@
 instance Mergeable SomeIntN where
   rootStrategy =
     SortedStrategy @Natural
-      (\(SomeIntN (v :: IntN n)) -> natVal (Proxy @n))
-      ( \n ->
+      (\(SomeIntN (_ :: IntN n)) -> natVal (Proxy @n))
+      ( \_ ->
           SortedStrategy @Integer
-            (\(SomeIntN (IntN i)) -> toInteger i)
+            (\(SomeIntN (IntN i)) -> i)
             (const $ SimpleStrategy $ \_ l _ -> l)
       )
 
 instance Mergeable SomeWordN where
   rootStrategy =
     SortedStrategy @Natural
-      (\(SomeWordN (v :: WordN n)) -> natVal (Proxy @n))
-      ( \n ->
+      (\(SomeWordN (_ :: WordN n)) -> natVal (Proxy @n))
+      ( \_ ->
           SortedStrategy @Integer
-            (\(SomeWordN (WordN i)) -> toInteger i)
+            (\(SomeWordN (WordN i)) -> i)
             (const $ SimpleStrategy $ \_ l _ -> l)
       )
 
@@ -513,14 +567,14 @@
 -- | Helper type for building efficient merge strategy for list-like containers.
 data StrategyList container where
   StrategyList ::
-    forall bool a container.
+    forall a container.
     container [DynamicSortedIdx] ->
     container (MergingStrategy a) ->
     StrategyList container
 
 -- | Helper function for building efficient merge strategy for list-like containers.
 buildStrategyList ::
-  forall bool a container.
+  forall a container.
   (Functor container) =>
   MergingStrategy a ->
   container a ->
@@ -994,8 +1048,8 @@
 instance Mergeable SomeSymIntN where
   rootStrategy =
     SortedStrategy @Natural
-      (\(SomeSymIntN (v :: SymIntN n)) -> natVal (Proxy @n))
-      ( \n ->
+      (\(SomeSymIntN (_ :: SymIntN n)) -> natVal (Proxy @n))
+      ( \_ ->
           SimpleStrategy
             ( \c (SomeSymIntN (l :: SymIntN l)) (SomeSymIntN (r :: SymIntN r)) ->
                 case unsafeAxiom @l @r of
@@ -1006,8 +1060,8 @@
 instance Mergeable SomeSymWordN where
   rootStrategy =
     SortedStrategy @Natural
-      (\(SomeSymWordN (v :: SymWordN n)) -> natVal (Proxy @n))
-      ( \n ->
+      (\(SomeSymWordN (_ :: SymWordN n)) -> natVal (Proxy @n))
+      ( \_ ->
           SimpleStrategy
             ( \c (SomeSymWordN (l :: SymWordN l)) (SomeSymWordN (r :: SymWordN r)) ->
                 case unsafeAxiom @l @r of
@@ -1027,6 +1081,6 @@
           Denormal -> 4 :: Int
           RatioZeroDenominator -> 5 :: Int
       )
-      (const $ SimpleStrategy $ \_ l r -> l)
+      (const $ SimpleStrategy $ \_ l _ -> l)
 
 deriving via (Default BitwidthMismatch) instance (Mergeable BitwidthMismatch)
diff --git a/src/Grisette/Core/Data/Class/Mergeable.hs-boot b/src/Grisette/Core/Data/Class/Mergeable.hs-boot
--- a/src/Grisette/Core/Data/Class/Mergeable.hs-boot
+++ b/src/Grisette/Core/Data/Class/Mergeable.hs-boot
@@ -2,10 +2,15 @@
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE Trustworthy #-}
 
-module Grisette.Core.Data.Class.Mergeable where
+module Grisette.Core.Data.Class.Mergeable
+  ( MergingStrategy (..),
+    Mergeable' (..),
+    Mergeable (..),
+  )
+where
 
-import Data.Typeable
-import {-# SOURCE #-} Grisette.IR.SymPrim.Data.SymPrim
+import Data.Typeable (Typeable)
+import {-# SOURCE #-} Grisette.IR.SymPrim.Data.SymPrim (SymBool)
 
 data MergingStrategy a where
   SimpleStrategy :: (SymBool -> a -> a -> a) -> MergingStrategy a
diff --git a/src/Grisette/Core/Data/Class/ModelOps.hs b/src/Grisette/Core/Data/Class/ModelOps.hs
--- a/src/Grisette/Core/Data/Class/ModelOps.hs
+++ b/src/Grisette/Core/Data/Class/ModelOps.hs
@@ -21,9 +21,7 @@
   )
 where
 
-import Data.Hashable
-import Data.Kind
-import Data.Typeable
+import Data.Kind (Type)
 
 -- $setup
 -- >>> import Grisette.Core
@@ -88,7 +86,7 @@
 -- SymbolSet {a :: Bool, b :: Bool}
 class
   (SymbolSetOps symbolSet typedSymbol) =>
-  SymbolSetRep rep symbolSet (typedSymbol :: * -> *)
+  SymbolSetRep rep symbolSet (typedSymbol :: Type -> Type)
   where
   -- | Build a symbolic constant set
   buildSymbolSet :: rep -> symbolSet
diff --git a/src/Grisette/Core/Data/Class/SOrd.hs b/src/Grisette/Core/Data/Class/SOrd.hs
--- a/src/Grisette/Core/Data/Class/SOrd.hs
+++ b/src/Grisette/Core/Data/Class/SOrd.hs
@@ -26,24 +26,43 @@
   )
 where
 
-import Control.Monad.Except
+import Control.Monad.Except (ExceptT (ExceptT))
 import Control.Monad.Identity
-import Control.Monad.Trans.Maybe
+  ( Identity (Identity),
+    IdentityT (IdentityT),
+  )
+import Control.Monad.Trans.Maybe (MaybeT (MaybeT))
 import qualified Control.Monad.Writer.Lazy as WriterLazy
 import qualified Control.Monad.Writer.Strict as WriterStrict
 import qualified Data.ByteString as B
-import Data.Functor.Sum
-import Data.Int
+import Data.Functor.Sum (Sum)
+import Data.Int (Int16, Int32, Int64, Int8)
 import qualified Data.Text as T
-import Data.Word
-import GHC.TypeLits
+import Data.Word (Word16, Word32, Word64, Word8)
+import GHC.TypeLits (KnownNat, type (<=))
 import Generics.Deriving
-import {-# SOURCE #-} Grisette.Core.Control.Monad.UnionM
-import Grisette.Core.Data.BV
+  ( Default (Default),
+    Generic (Rep, from),
+    K1 (K1),
+    M1 (M1),
+    U1,
+    V1,
+    type (:*:) ((:*:)),
+    type (:+:) (L1, R1),
+  )
+import {-# SOURCE #-} Grisette.Core.Control.Monad.UnionM (UnionM)
+import Grisette.Core.Data.BV (IntN, SomeIntN, SomeWordN, WordN)
 import Grisette.Core.Data.Class.Bool
+  ( LogicalOp ((&&~), (||~)),
+    SEq ((/=~), (==~)),
+    SEq' ((==~~)),
+  )
 import Grisette.Core.Data.Class.SimpleMergeable
-import Grisette.Core.Data.Class.Solvable
-import {-# SOURCE #-} Grisette.IR.SymPrim.Data.SymPrim
+  ( mrgIf,
+    mrgSingle,
+  )
+import Grisette.Core.Data.Class.Solvable (Solvable (con))
+import {-# SOURCE #-} Grisette.IR.SymPrim.Data.SymPrim (SymBool)
 
 -- $setup
 -- >>> import Grisette.Core
diff --git a/src/Grisette/Core/Data/Class/SafeArith.hs b/src/Grisette/Core/Data/Class/SafeArith.hs
--- a/src/Grisette/Core/Data/Class/SafeArith.hs
+++ b/src/Grisette/Core/Data/Class/SafeArith.hs
@@ -30,24 +30,39 @@
   )
 where
 
-import Control.Exception
-import Control.Monad.Except
-import Data.Int
-import Data.Typeable
-import Data.Word
-import GHC.TypeNats
-import Grisette.Core.Control.Monad.Union
+import Control.Exception (ArithException (DivideByZero, Overflow, Underflow))
+import Control.Monad.Except (MonadError (throwError))
+import Data.Int (Int16, Int32, Int64, Int8)
+import Data.Typeable (Proxy (Proxy), type (:~:) (Refl))
+import Data.Word (Word16, Word32, Word64, Word8)
+import GHC.TypeNats (KnownNat, sameNat, type (<=))
+import Grisette.Core.Control.Monad.Union (MonadUnion)
 import Grisette.Core.Data.BV
+  ( BitwidthMismatch (BitwidthMismatch),
+    IntN,
+    SomeIntN (SomeIntN),
+    SomeWordN (SomeWordN),
+    WordN,
+  )
 import Grisette.Core.Data.Class.Bool
-import Grisette.Core.Data.Class.Error
-import Grisette.Core.Data.Class.Mergeable
+  ( LogicalOp ((&&~), (||~)),
+    SEq ((==~)),
+  )
+import Grisette.Core.Data.Class.Mergeable (Mergeable)
 import Grisette.Core.Data.Class.SOrd
+  ( SOrd ((<=~), (<~), (>=~), (>~)),
+  )
 import Grisette.Core.Data.Class.SimpleMergeable
-import Grisette.Core.Data.Class.Solvable
+  ( merge,
+    mrgIf,
+    mrgSingle,
+  )
+import Grisette.Core.Data.Class.Solvable (Solvable (con))
 
 -- $setup
 -- >>> import Grisette.Core
 -- >>> import Grisette.IR.SymPrim
+-- >>> import Control.Monad.Except
 
 -- | Safe division with monadic error handling in multi-path
 -- execution. These procedures throw an exception when the
@@ -94,7 +109,7 @@
   -- | Safe signed 'rem' with monadic error handling in multi-path execution.
   safeRem :: (MonadError e uf, MonadUnion uf) => a -> a -> uf a
   safeRem l r = do
-    (d, m) <- safeDivMod l r
+    (_, m) <- safeDivMod l r
     mrgIf
       ((l >=~ 0 &&~ r >~ 0) ||~ (l <=~ 0 &&~ r <~ 0) ||~ m ==~ 0)
       (mrgSingle m)
@@ -154,7 +169,7 @@
   -- The error is transformed.
   safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> a -> uf a
   safeRem' t l r = do
-    (d, m) <- safeDivMod' t l r
+    (_, m) <- safeDivMod' t l r
     mrgIf
       ((l >=~ 0 &&~ r >~ 0) ||~ (l <=~ 0 &&~ r <~ 0) ||~ m ==~ 0)
       (mrgSingle m)
@@ -177,12 +192,13 @@
 #define QRIGHT(a) QID(a)'
 
 #define QRIGHTT(a) QID(a)' t'
+#define QRIGHTU(a) QID(a)' _'
 
 #define SAFE_DIVISION_FUNC(name, op) \
 name _ r | r == 0 = merge $ throwError DivideByZero; \
 name l r = mrgSingle $ l `op` r; \
-QRIGHTT(name) _ r | r == 0 = let t1 = t' in merge $ throwError (t' DivideByZero); \
-QRIGHTT(name) l r = mrgSingle $ l `op` r
+QRIGHTT(name) _ r | r == 0 = let _ = t' in merge $ throwError (t' DivideByZero); \
+QRIGHTU(name) l r = mrgSingle $ l `op` r
 
 #define SAFE_DIVISION_CONCRETE(type) \
 instance SafeDivision ArithException type where \
@@ -395,7 +411,7 @@
   safeAdd' t (type (l :: ctype l)) (type (r :: ctype r)) = merge (\
     case sameNat (Proxy @l) (Proxy @r) of \
       Just Refl -> type <$> safeAdd' (t . Right) l r; \
-      _ -> let t' = t; t''' = t in throwError $ t' $ Left BitwidthMismatch); \
+      _ -> let t' = t; _ = t' in throwError $ t' $ Left BitwidthMismatch); \
   safeMinus (type (l :: ctype l)) (type (r :: ctype r)) = merge (\
     case sameNat (Proxy @l) (Proxy @r) of \
       Just Refl -> type <$> safeMinus' Right l r; \
@@ -403,7 +419,7 @@
   safeMinus' t (type (l :: ctype l)) (type (r :: ctype r)) = merge (\
     case sameNat (Proxy @l) (Proxy @r) of \
       Just Refl -> type <$> safeMinus' (t . Right) l r; \
-      _ -> let t' = t; t''' = t in throwError $ t' $ Left BitwidthMismatch); \
+      _ -> let t' = t; _ = t' in throwError $ t' $ Left BitwidthMismatch); \
   safeNeg (type l) = merge $ type <$> safeNeg' Right l; \
   safeNeg' t (type l) = merge $ type <$> safeNeg' (t . Right) l
 
diff --git a/src/Grisette/Core/Data/Class/SimpleMergeable.hs b/src/Grisette/Core/Data/Class/SimpleMergeable.hs
--- a/src/Grisette/Core/Data/Class/SimpleMergeable.hs
+++ b/src/Grisette/Core/Data/Class/SimpleMergeable.hs
@@ -46,26 +46,53 @@
   )
 where
 
-import Control.Monad.Except
+import Control.Monad.Except (ExceptT (ExceptT))
 import Control.Monad.Identity
+  ( Identity (Identity),
+    IdentityT (IdentityT),
+  )
 import qualified Control.Monad.RWS.Lazy as RWSLazy
 import qualified Control.Monad.RWS.Strict as RWSStrict
-import Control.Monad.Reader
+import Control.Monad.Reader (ReaderT (ReaderT))
 import qualified Control.Monad.State.Lazy as StateLazy
 import qualified Control.Monad.State.Strict as StateStrict
-import Control.Monad.Trans.Cont
-import Control.Monad.Trans.Maybe
+import Control.Monad.Trans.Cont (ContT (ContT))
+import Control.Monad.Trans.Maybe (MaybeT (MaybeT))
 import qualified Control.Monad.Writer.Lazy as WriterLazy
 import qualified Control.Monad.Writer.Strict as WriterStrict
-import Data.Kind
+import Data.Kind (Type)
 import GHC.Generics
-import GHC.TypeNats
-import Generics.Deriving
-import Grisette.Core.Data.Class.Bool
-import Grisette.Core.Data.Class.Function
+  ( Generic (Rep, from, to),
+    K1 (K1),
+    M1 (M1),
+    U1,
+    V1,
+    type (:*:) ((:*:)),
+  )
+import GHC.TypeNats (KnownNat, type (<=))
+import Generics.Deriving (Default (Default))
+import Grisette.Core.Data.Class.Bool (ITEOp (ites))
+import Grisette.Core.Data.Class.Function (Function (Arg, Ret, (#)))
 import Grisette.Core.Data.Class.Mergeable
+  ( Mergeable (rootStrategy),
+    Mergeable',
+    Mergeable1 (liftRootStrategy),
+    Mergeable2 (liftRootStrategy2),
+    Mergeable3 (liftRootStrategy3),
+    MergingStrategy (SimpleStrategy),
+  )
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
+  ( LinkedRep,
+    SupportedPrim,
+  )
 import {-# SOURCE #-} Grisette.IR.SymPrim.Data.SymPrim
+  ( SymBool,
+    SymIntN,
+    SymInteger,
+    SymWordN,
+    type (-~>),
+    type (=~>),
+  )
 
 -- $setup
 -- >>> import Grisette.Core
@@ -718,7 +745,7 @@
 -- <If a b c>
 -- >>> simpleMerge $ (unionIf (ssym "a") (return $ ssym "b") (return $ ssym "c") :: UnionM SymBool)
 -- (ite a b c)
-simpleMerge :: forall bool u a. (SimpleMergeable a, UnionLike u, UnionPrjOp u) => u a -> a
+simpleMerge :: forall u a. (SimpleMergeable a, UnionLike u, UnionPrjOp u) => u a -> a
 simpleMerge u = case merge u of
   SingleU x -> x
   _ -> error "Should not happen"
@@ -730,7 +757,7 @@
 -- >>> sumU (unionIf "cond" (return ["a"]) (return ["b","c"]) :: UnionM [SymInteger])
 -- (ite cond a (+ b c))
 onUnion ::
-  forall bool u a r.
+  forall u a r.
   (SimpleMergeable r, UnionLike u, UnionPrjOp u, Monad u) =>
   (a -> r) ->
   (u a -> r)
@@ -738,7 +765,7 @@
 
 -- | Lift a function to work on union values.
 onUnion2 ::
-  forall bool u a b r.
+  forall u a b r.
   (SimpleMergeable r, UnionLike u, UnionPrjOp u, Monad u) =>
   (a -> b -> r) ->
   (u a -> u b -> r)
@@ -746,7 +773,7 @@
 
 -- | Lift a function to work on union values.
 onUnion3 ::
-  forall bool u a b c r.
+  forall u a b c r.
   (SimpleMergeable r, UnionLike u, UnionPrjOp u, Monad u) =>
   (a -> b -> c -> r) ->
   (u a -> u b -> u c -> r)
@@ -754,7 +781,7 @@
 
 -- | Lift a function to work on union values.
 onUnion4 ::
-  forall bool u a b c d r.
+  forall u a b c d r.
   (SimpleMergeable r, UnionLike u, UnionPrjOp u, Monad u) =>
   (a -> b -> c -> d -> r) ->
   (u a -> u b -> u c -> u d -> r)
diff --git a/src/Grisette/Core/Data/Class/SimpleMergeable.hs-boot b/src/Grisette/Core/Data/Class/SimpleMergeable.hs-boot
--- a/src/Grisette/Core/Data/Class/SimpleMergeable.hs-boot
+++ b/src/Grisette/Core/Data/Class/SimpleMergeable.hs-boot
@@ -4,7 +4,9 @@
 module Grisette.Core.Data.Class.SimpleMergeable (SimpleMergeable (..)) where
 
 import {-# SOURCE #-} Grisette.Core.Data.Class.Mergeable
-import {-# SOURCE #-} Grisette.IR.SymPrim.Data.SymPrim
+  ( Mergeable,
+  )
+import {-# SOURCE #-} Grisette.IR.SymPrim.Data.SymPrim (SymBool)
 
 class (Mergeable a) => SimpleMergeable a where
   mrgIte :: SymBool -> a -> a -> a
diff --git a/src/Grisette/Core/Data/Class/Solvable.hs b/src/Grisette/Core/Data/Class/Solvable.hs
--- a/src/Grisette/Core/Data/Class/Solvable.hs
+++ b/src/Grisette/Core/Data/Class/Solvable.hs
@@ -18,11 +18,11 @@
   )
 where
 
-import Control.DeepSeq
-import Data.Hashable
-import Data.String
-import Data.Typeable
-import Language.Haskell.TH.Syntax
+import Control.DeepSeq (NFData)
+import Data.Hashable (Hashable)
+import Data.String (IsString)
+import Data.Typeable (Typeable)
+import Language.Haskell.TH.Syntax (Lift)
 
 -- $setup
 -- >>> import Grisette.Core
diff --git a/src/Grisette/Core/Data/Class/Solver.hs b/src/Grisette/Core/Data/Class/Solver.hs
--- a/src/Grisette/Core/Data/Class/Solver.hs
+++ b/src/Grisette/Core/Data/Class/Solver.hs
@@ -39,21 +39,20 @@
   )
 where
 
-import Control.DeepSeq
-import Control.Monad.Except
-import Data.Hashable
-import Generics.Deriving
-import Grisette.Core.Control.Exception
-import Grisette.Core.Data.Class.Bool
-import Grisette.Core.Data.Class.Evaluate
-import Grisette.Core.Data.Class.ExtractSymbolics
+import Control.DeepSeq (NFData)
+import Control.Monad.Except (ExceptT, runExceptT)
+import Data.Hashable (Hashable)
+import GHC.Generics (Generic)
 import Grisette.Core.Data.Class.SimpleMergeable
-import Grisette.Core.Data.Class.Solvable
-import Grisette.IR.SymPrim.Data.Prim.Model
-import {-# SOURCE #-} Grisette.IR.SymPrim.Data.SymPrim
-import Language.Haskell.TH.Syntax
+  ( UnionPrjOp,
+    simpleMerge,
+  )
+import Grisette.IR.SymPrim.Data.Prim.Model (Model)
+import {-# SOURCE #-} Grisette.IR.SymPrim.Data.SymPrim (SymBool)
+import Language.Haskell.TH.Syntax (Lift)
 
-data SolveInternal = SolveInternal deriving (Eq, Show, Ord, Generic, Hashable, Lift, NFData)
+data SolveInternal = SolveInternal
+  deriving (Eq, Show, Ord, Generic, Hashable, Lift, NFData)
 
 -- $setup
 -- >>> import Grisette.Core
diff --git a/src/Grisette/Core/Data/Class/Substitute.hs b/src/Grisette/Core/Data/Class/Substitute.hs
--- a/src/Grisette/Core/Data/Class/Substitute.hs
+++ b/src/Grisette/Core/Data/Class/Substitute.hs
@@ -25,24 +25,35 @@
   )
 where
 
-import Control.Monad.Except
+import Control.Monad.Except (ExceptT (ExceptT))
 import Control.Monad.Identity
-import Control.Monad.Trans.Maybe
+  ( Identity (Identity),
+    IdentityT (IdentityT),
+  )
+import Control.Monad.Trans.Maybe (MaybeT (MaybeT))
 import qualified Control.Monad.Writer.Lazy as WriterLazy
 import qualified Control.Monad.Writer.Strict as WriterStrict
 import qualified Data.ByteString as B
-import Data.Functor.Sum
-import Data.Int
+import Data.Functor.Sum (Sum)
+import Data.Int (Int16, Int32, Int64, Int8)
 import qualified Data.Text as T
-import Data.Word
-import GHC.TypeNats
+import Data.Word (Word16, Word32, Word64, Word8)
+import GHC.TypeNats (KnownNat, type (<=))
 import Generics.Deriving
+  ( Default (Default, unDefault),
+    Generic (Rep, from, to),
+    K1 (K1),
+    M1 (M1),
+    U1,
+    type (:*:) ((:*:)),
+    type (:+:) (L1, R1),
+  )
 import Generics.Deriving.Instances ()
-import Grisette.Core.Data.BV
+import Grisette.Core.Data.BV (IntN, SomeIntN, SomeWordN, WordN)
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
-import Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermSubstitution
-import Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermUtils
-import {-# SOURCE #-} Grisette.IR.SymPrim.Data.SymPrim
+  ( LinkedRep,
+    TypedSymbol,
+  )
 
 -- $setup
 -- >>> import Grisette.Core
diff --git a/src/Grisette/Core/Data/Class/ToCon.hs b/src/Grisette/Core/Data/Class/ToCon.hs
--- a/src/Grisette/Core/Data/Class/ToCon.hs
+++ b/src/Grisette/Core/Data/Class/ToCon.hs
@@ -24,21 +24,31 @@
   )
 where
 
-import Control.Monad.Except
+import Control.Monad.Except (ExceptT (ExceptT))
 import Control.Monad.Identity
-import Control.Monad.Trans.Maybe
+  ( Identity (Identity, runIdentity),
+    IdentityT (IdentityT),
+  )
+import Control.Monad.Trans.Maybe (MaybeT (MaybeT))
 import qualified Control.Monad.Writer.Lazy as WriterLazy
 import qualified Control.Monad.Writer.Strict as WriterStrict
 import qualified Data.ByteString as B
-import Data.Functor.Sum
-import Data.Int
+import Data.Functor.Sum (Sum)
+import Data.Int (Int16, Int32, Int64, Int8)
 import qualified Data.Text as T
-import Data.Word
+import Data.Word (Word16, Word32, Word64, Word8)
 import GHC.Generics
-import GHC.TypeNats
-import Generics.Deriving
+  ( Generic (Rep, from, to),
+    K1 (K1),
+    M1 (M1),
+    U1,
+    type (:*:) ((:*:)),
+    type (:+:) (L1, R1),
+  )
+import GHC.TypeNats (KnownNat, type (<=))
+import Generics.Deriving (Default (Default))
 import Generics.Deriving.Instances ()
-import Grisette.Core.Data.BV
+import Grisette.Core.Data.BV (IntN, SomeIntN, SomeWordN, WordN)
 
 -- $setup
 -- >>> import Grisette.Core
diff --git a/src/Grisette/Core/Data/Class/ToSym.hs b/src/Grisette/Core/Data/Class/ToSym.hs
--- a/src/Grisette/Core/Data/Class/ToSym.hs
+++ b/src/Grisette/Core/Data/Class/ToSym.hs
@@ -25,21 +25,32 @@
 where
 
 import Control.Monad.Identity
-import Control.Monad.Reader
+  ( Identity (Identity),
+    IdentityT (IdentityT),
+  )
+import Control.Monad.Reader (ReaderT (ReaderT))
 import qualified Control.Monad.State.Lazy as StateLazy
 import qualified Control.Monad.State.Strict as StateStrict
-import Control.Monad.Trans.Except
-import Control.Monad.Trans.Maybe
+import Control.Monad.Trans.Except (ExceptT (ExceptT))
+import Control.Monad.Trans.Maybe (MaybeT (MaybeT))
 import qualified Control.Monad.Writer.Lazy as WriterLazy
 import qualified Control.Monad.Writer.Strict as WriterStrict
 import qualified Data.ByteString as B
-import Data.Functor.Sum
-import Data.Int
+import Data.Functor.Sum (Sum)
+import Data.Int (Int16, Int32, Int64, Int8)
 import qualified Data.Text as T
-import Data.Word
-import GHC.TypeNats
+import Data.Word (Word16, Word32, Word64, Word8)
+import GHC.TypeNats (KnownNat, type (<=))
 import Generics.Deriving
-import Grisette.Core.Data.BV
+  ( Default (Default),
+    Generic (Rep, from, to),
+    K1 (K1),
+    M1 (M1),
+    U1,
+    type (:*:) ((:*:)),
+    type (:+:) (L1, R1),
+  )
+import Grisette.Core.Data.BV (IntN, SomeIntN, SomeWordN, WordN)
 
 -- $setup
 -- >>> import Grisette.IR.SymPrim
diff --git a/src/Grisette/Core/Data/FileLocation.hs b/src/Grisette/Core/Data/FileLocation.hs
--- a/src/Grisette/Core/Data/FileLocation.hs
+++ b/src/Grisette/Core/Data/FileLocation.hs
@@ -4,6 +4,8 @@
 {-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE Trustworthy #-}
 
+{- HLINT ignore "Unused LANGUAGE pragma" -}
+
 -- |
 -- Module      :   Grisette.Core.Data.FileLocation
 -- Copyright   :   (c) Sirui Lu 2021-2023
@@ -21,14 +23,16 @@
   )
 where
 
-import Control.DeepSeq
-import Data.Hashable
+import Control.DeepSeq (NFData)
+import Data.Hashable (Hashable)
 import Debug.Trace.LocationTH (__LOCATION__)
-import GHC.Generics
-import Grisette.Core.Data.Class.GenSym
+import GHC.Generics (Generic)
+import Grisette.Core.Data.Class.GenSym (FreshIdent, nameWithInfo)
 import Grisette.Core.Data.Class.Solvable
-import Language.Haskell.TH.Syntax
-import Language.Haskell.TH.Syntax.Compat
+  ( Solvable (iinfosym, sinfosym),
+  )
+import Language.Haskell.TH.Syntax (Lift, unsafeTExpCoerce)
+import Language.Haskell.TH.Syntax.Compat (SpliceQ, liftSplice)
 
 -- $setup
 -- >>> import Grisette.Core
diff --git a/src/Grisette/Core/Data/MemoUtils.hs b/src/Grisette/Core/Data/MemoUtils.hs
--- a/src/Grisette/Core/Data/MemoUtils.hs
+++ b/src/Grisette/Core/Data/MemoUtils.hs
@@ -22,9 +22,9 @@
 where
 
 import Data.Function (fix)
-import Data.HashTable.IO as H
-import Data.Hashable
-import System.IO.Unsafe
+import qualified Data.HashTable.IO as H
+import Data.Hashable (Hashable)
+import System.IO.Unsafe (unsafePerformIO)
 
 type HashTable k v = H.BasicHashTable k v
 
diff --git a/src/Grisette/Core/Data/Union.hs b/src/Grisette/Core/Data/Union.hs
--- a/src/Grisette/Core/Data/Union.hs
+++ b/src/Grisette/Core/Data/Union.hs
@@ -4,6 +4,7 @@
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE Trustworthy #-}
 {-# LANGUAGE TypeFamilies #-}
 
@@ -26,22 +27,47 @@
   )
 where
 
-import Control.DeepSeq
+import Control.DeepSeq (NFData (rnf), NFData1 (liftRnf), rnf1)
 import Data.Functor.Classes
-import Data.Hashable
-import GHC.Generics
+  ( Eq1 (liftEq),
+    Show1 (liftShowsPrec),
+    showsPrec1,
+    showsUnaryWith,
+  )
+import Data.Hashable (Hashable (hashWithSalt))
+import GHC.Generics (Generic, Generic1)
 import Grisette.Core.Data.Class.Bool
+  ( ITEOp (ites),
+    LogicalOp (nots, (&&~), (||~)),
+  )
 import Grisette.Core.Data.Class.GPretty
+  ( GPretty (gprettyPrec),
+    condEnclose,
+  )
 import Grisette.Core.Data.Class.Mergeable
+  ( Mergeable (rootStrategy),
+    Mergeable1 (liftRootStrategy),
+    MergingStrategy (NoStrategy, SimpleStrategy, SortedStrategy),
+  )
 import Grisette.Core.Data.Class.SimpleMergeable
-import Grisette.Core.Data.Class.Solvable
+  ( SimpleMergeable (mrgIte),
+    SimpleMergeable1 (liftMrgIte),
+    UnionLike (mergeWithStrategy, mrgIfWithStrategy, mrgSingleWithStrategy, single, unionIf),
+    UnionPrjOp (ifView, leftMost, singleView),
+    mrgIf,
+  )
+import Grisette.Core.Data.Class.Solvable (pattern Con)
 import {-# SOURCE #-} Grisette.IR.SymPrim.Data.SymPrim
-import Language.Haskell.TH.Syntax
+  ( AllSyms (allSymsS),
+    SomeSym (SomeSym),
+    SymBool,
+  )
+import Language.Haskell.TH.Syntax (Lift)
 
 #if MIN_VERSION_prettyprinter(1,7,0)
-import Prettyprinter
+import Prettyprinter (align, group, nest, vsep)
 #else
-import Data.Text.Prettyprint.Doc
+import Data.Text.Prettyprint.Doc (align, group, nest, vsep)
 #endif
 
 -- | The default union implementation.
diff --git a/src/Grisette/Core/TH.hs b/src/Grisette/Core/TH.hs
--- a/src/Grisette/Core/TH.hs
+++ b/src/Grisette/Core/TH.hs
@@ -17,10 +17,25 @@
   )
 where
 
-import Control.Monad
-import Grisette.Core.THCompat
+import Control.Monad (join, replicateM, when, zipWithM)
+import Grisette.Core.THCompat (augmentFinalType)
 import Language.Haskell.TH
-import Language.Haskell.TH.Syntax
+  ( Body (NormalB),
+    Clause (Clause),
+    Con (ForallC, GadtC, InfixC, NormalC, RecC, RecGadtC),
+    Dec (DataD, FunD, NewtypeD, SigD),
+    Exp (AppE, ConE, LamE, VarE),
+    Info (DataConI, TyConI),
+    Name,
+    Pat (VarP),
+    Q,
+    Type (ForallT),
+    mkName,
+    newName,
+    pprint,
+    reify,
+  )
+import Language.Haskell.TH.Syntax (Name (Name), OccName (OccName))
 
 -- | Generate constructor wrappers that wraps the result in a union-like monad with provided names.
 --
diff --git a/src/Grisette/Core/THCompat.hs b/src/Grisette/Core/THCompat.hs
--- a/src/Grisette/Core/THCompat.hs
+++ b/src/Grisette/Core/THCompat.hs
@@ -1,7 +1,6 @@
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE TemplateHaskellQuotes #-}
 {-# LANGUAGE Trustworthy #-}
-{- ORMOLU_DISABLE -}
 
 -- |
 -- Module      :   Grisette.Core.THCompat
@@ -11,20 +10,38 @@
 -- Maintainer  :   siruilu@cs.washington.edu
 -- Stability   :   Experimental
 -- Portability :   GHC only
-
 module Grisette.Core.THCompat (augmentFinalType) where
 
-import Data.Bifunctor
+import Data.Bifunctor (Bifunctor (second))
+import Grisette.Core.Control.Monad.UnionM (UnionM)
+import Grisette.Core.Data.Class.Mergeable (Mergeable)
+#if MIN_VERSION_template_haskell(2,17,0)
 import Language.Haskell.TH.Syntax
-import Grisette.Core.Control.Monad.Union
-import Grisette.Core.Data.Class.Bool
-import Grisette.Core.Data.Class.Mergeable
-import Grisette.Core.Control.Monad.UnionM
-import Grisette.IR.SymPrim.Data.SymPrim
+  ( Pred,
+    Q,
+    Specificity,
+    TyVarBndr,
+    Type
+      ( AppT,
+        ArrowT,
+        MulArrowT
+      ),
+  )
+#else
+import Language.Haskell.TH.Syntax
+  ( Pred,
+    Q,
+    TyVarBndr,
+    Type
+      ( AppT,
+        ArrowT
+      ),
+  )
+#endif
 
 #if MIN_VERSION_template_haskell(2,17,0)
 augmentFinalType :: Type -> Q (([TyVarBndr Specificity], [Pred]), Type)
-#elif MIN_VERSION_template_haskell(2,16,0)
+#else
 augmentFinalType :: Type -> Q (([TyVarBndr], [Pred]), Type)
 #endif
 augmentFinalType (AppT a@(AppT ArrowT _) t) = do
diff --git a/src/Grisette/Experimental.hs b/src/Grisette/Experimental.hs
--- a/src/Grisette/Experimental.hs
+++ b/src/Grisette/Experimental.hs
@@ -1,3 +1,6 @@
+-- Disable this warning because we are re-exporting things.
+{-# OPTIONS_GHC -Wno-missing-import-lists #-}
+
 module Grisette.Experimental
   ( -- * Experimental features
 
@@ -23,3 +26,14 @@
 where
 
 import Grisette.Experimental.GenSymConstrained
+  ( GenSymConstrained (..),
+    GenSymSimpleConstrained (..),
+    SOrdBound (..),
+    SOrdLowerBound (..),
+    SOrdUpperBound (..),
+    derivedFreshConstrainedNoSpec,
+    derivedSimpleFreshConstrainedNoSpec,
+    derivedSimpleFreshConstrainedSameShape,
+    genSymConstrained,
+    genSymSimpleConstrained,
+  )
diff --git a/src/Grisette/Experimental/GenSymConstrained.hs b/src/Grisette/Experimental/GenSymConstrained.hs
--- a/src/Grisette/Experimental/GenSymConstrained.hs
+++ b/src/Grisette/Experimental/GenSymConstrained.hs
@@ -28,20 +28,40 @@
   )
 where
 
-import Control.Monad.Except
-import Control.Monad.Trans.Maybe
-import Data.Int
-import Data.Word
-import Debug.Trace
+import Control.Monad.Except (ExceptT (ExceptT), MonadError (throwError))
+import Control.Monad.Trans.Maybe (MaybeT (MaybeT))
 import GHC.Generics
-import GHC.TypeLits
+  ( Generic (Rep, from, to),
+    K1 (K1),
+    M1 (M1),
+    U1 (U1),
+    type (:*:) ((:*:)),
+    type (:+:) (L1, R1),
+  )
 import Grisette.Core.Control.Monad.UnionM
-import Grisette.Core.Data.BV
-import Grisette.Core.Data.Class.Bool
+  ( UnionM,
+    liftToMonadUnion,
+  )
+import Grisette.Core.Data.Class.Bool (LogicalOp ((||~)))
 import Grisette.Core.Data.Class.GenSym
-import Grisette.Core.Data.Class.Mergeable
-import Grisette.Core.Data.Class.SOrd
+  ( FreshIdent,
+    GenSym (fresh),
+    GenSymSimple (simpleFresh),
+    ListSpec (ListSpec),
+    MonadFresh,
+    SimpleListSpec (SimpleListSpec),
+    chooseFresh,
+    chooseUnionFresh,
+    runFreshT,
+  )
+import Grisette.Core.Data.Class.Mergeable (Mergeable, Mergeable1)
+import Grisette.Core.Data.Class.SOrd (SOrd ((<~), (>=~)))
 import Grisette.Core.Data.Class.SimpleMergeable
+  ( UnionLike,
+    merge,
+    mrgIf,
+    mrgSingle,
+  )
 
 -- $setup
 -- >>> import Grisette.Core
@@ -160,7 +180,7 @@
     mrgSingle s
 
 instance GenSymConstrained (SOrdBound Integer ()) Integer where
-  freshConstrained e (SOrdBound l r _) = chooseFresh [l .. r - 1]
+  freshConstrained _ (SOrdBound l r _) = chooseFresh [l .. r - 1]
 
 -- Either
 instance
@@ -676,7 +696,7 @@
   ) =>
   GenSymConstrained spec (ExceptT a m b)
   where
-  freshConstrained e v = trace "x" $ do
+  freshConstrained e v = do
     x <- freshConstrained e v
     mrgSingle $ merge . fmap ExceptT $ x
 
@@ -740,7 +760,7 @@
   GenSymConstrainedNoSpec (a :+: b)
   where
   freshConstrainedNoSpec ::
-    forall m u c e.
+    forall m c e.
     ( MonadFresh m,
       MonadError e m,
       UnionLike m
@@ -758,7 +778,7 @@
   GenSymConstrainedNoSpec (a :*: b)
   where
   freshConstrainedNoSpec ::
-    forall m u c e.
+    forall m c e.
     ( MonadFresh m,
       MonadError e m,
       UnionLike m
@@ -782,7 +802,7 @@
 --
 -- __Note:__ __Never__ use on recursive types.
 derivedFreshConstrainedNoSpec ::
-  forall bool a m u e.
+  forall a m e.
   ( Generic a,
     GenSymConstrainedNoSpec (Rep a),
     Mergeable a,
diff --git a/src/Grisette/IR/SymPrim.hs b/src/Grisette/IR/SymPrim.hs
--- a/src/Grisette/IR/SymPrim.hs
+++ b/src/Grisette/IR/SymPrim.hs
@@ -1,4 +1,6 @@
 {-# LANGUAGE ExplicitNamespaces #-}
+-- Disable this warning because we are re-exporting things.
+{-# OPTIONS_GHC -Wno-missing-import-lists #-}
 
 -- |
 -- Module      :   Grisette.IR.SymPrim
@@ -22,8 +24,8 @@
 
     -- ** Symbolic types
     SupportedPrim,
-    SymRep (..),
-    ConRep (..),
+    SymRep (SymType),
+    ConRep (ConType),
     LinkedRep,
     SymBool (..),
     SymInteger (..),
@@ -48,7 +50,38 @@
 where
 
 import Grisette.Core.Data.BV
+  ( IntN,
+    SomeIntN (..),
+    SomeWordN (..),
+    WordN,
+  )
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
+  ( ConRep (..),
+    LinkedRep,
+    SupportedPrim,
+    SymRep (..),
+    TypedSymbol (..),
+    type (-->),
+  )
 import Grisette.IR.SymPrim.Data.Prim.Model
+  ( Model (..),
+    ModelValuePair (..),
+    SymbolSet (..),
+  )
 import Grisette.IR.SymPrim.Data.SymPrim
-import Grisette.IR.SymPrim.Data.TabularFun
+  ( AllSyms (..),
+    ModelSymPair (..),
+    SomeSymIntN (..),
+    SomeSymWordN (..),
+    SymBool (..),
+    SymIntN (..),
+    SymInteger (..),
+    SymWordN (..),
+    allSymsSize,
+    symSize,
+    symsSize,
+    (-->),
+    type (-~>) (..),
+    type (=~>) (..),
+  )
+import Grisette.IR.SymPrim.Data.TabularFun (type (=->) (..))
diff --git a/src/Grisette/IR/SymPrim/Data/IntBitwidth.hs b/src/Grisette/IR/SymPrim/Data/IntBitwidth.hs
--- a/src/Grisette/IR/SymPrim/Data/IntBitwidth.hs
+++ b/src/Grisette/IR/SymPrim/Data/IntBitwidth.hs
@@ -6,10 +6,10 @@
 -- Maintainer  :   siruilu@cs.washington.edu
 -- Stability   :   Experimental
 -- Portability :   GHC only
-module Grisette.IR.SymPrim.Data.IntBitwidth where
+module Grisette.IR.SymPrim.Data.IntBitwidth (intBitwidthQ) where
 
 import Data.Bits (FiniteBits (finiteBitSize))
-import Language.Haskell.TH
+import Language.Haskell.TH (TyLit (NumTyLit), Type (LitT), TypeQ)
 
 intBitwidthQ :: TypeQ
 intBitwidthQ = return $ LitT (NumTyLit $ toInteger $ finiteBitSize (undefined :: Int))
diff --git a/src/Grisette/IR/SymPrim/Data/Prim/Helpers.hs b/src/Grisette/IR/SymPrim/Data/Prim/Helpers.hs
--- a/src/Grisette/IR/SymPrim/Data/Prim/Helpers.hs
+++ b/src/Grisette/IR/SymPrim/Data/Prim/Helpers.hs
@@ -24,10 +24,14 @@
   )
 where
 
-import Data.Typeable
+import Data.Typeable (Typeable, cast)
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
+  ( Term (BinaryTerm, TernaryTerm, UnaryTerm),
+  )
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermUtils
-import Unsafe.Coerce
+  ( castTerm,
+  )
+import Unsafe.Coerce (unsafeCoerce)
 
 unsafeUnaryTermView :: forall a b tag. (Typeable tag) => Term a -> Maybe (tag, Term b)
 unsafeUnaryTermView (UnaryTerm _ (tag :: tagt) t1) =
diff --git a/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/Caches.hs b/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/Caches.hs
--- a/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/Caches.hs
+++ b/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/Caches.hs
@@ -16,13 +16,20 @@
 module Grisette.IR.SymPrim.Data.Prim.InternedTerm.Caches (typeMemoizedCache) where
 
 import Control.Concurrent
-import Data.Data
+  ( forkIO,
+    newEmptyMVar,
+    putMVar,
+    readMVar,
+    takeMVar,
+    tryPutMVar,
+  )
+import Data.Data (Proxy (Proxy), TypeRep, Typeable, typeRep)
 import qualified Data.HashMap.Strict as M
-import Data.IORef
-import Data.Interned
+import Data.IORef (IORef, atomicModifyIORef', newIORef)
+import Data.Interned (Cache, Interned, mkCache)
 import GHC.Base (Any)
-import GHC.IO
-import Unsafe.Coerce
+import GHC.IO (unsafeDupablePerformIO, unsafePerformIO)
+import Unsafe.Coerce (unsafeCoerce)
 
 mkOnceIO :: IO a -> IO (IO a)
 mkOnceIO io = do
diff --git a/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/InternedCtors.hs b/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/InternedCtors.hs
--- a/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/InternedCtors.hs
+++ b/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/InternedCtors.hs
@@ -65,21 +65,79 @@
   )
 where
 
-import Control.DeepSeq
-import Data.Array
-import Data.Bits
+import Control.DeepSeq (NFData)
+import Data.Array ((!))
+import Data.Bits (Bits)
 import qualified Data.HashMap.Strict as M
-import Data.Hashable
+import Data.Hashable (Hashable (hash))
 import Data.IORef (atomicModifyIORef')
 import Data.Interned
+  ( Interned (Uninterned, cache, cacheWidth, describe, identify),
+  )
 import Data.Interned.Internal
+  ( Cache (getCache),
+    CacheState (CacheState),
+  )
 import GHC.IO (unsafeDupablePerformIO)
-import GHC.TypeNats
+import GHC.TypeNats (KnownNat, type (+), type (<=))
 import Grisette.Core.Data.Class.BitVector
+  ( BVSignConversion,
+    SizedBV,
+  )
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
-import {-# SOURCE #-} Grisette.IR.SymPrim.Data.TabularFun
-import Language.Haskell.TH.Syntax
-import Type.Reflection
+  ( BinaryOp,
+    SupportedPrim,
+    Term,
+    TernaryOp,
+    TypedSymbol (IndexedSymbol, SimpleSymbol, WithInfo),
+    UTerm
+      ( UAbsNumTerm,
+        UAddNumTerm,
+        UAndBitsTerm,
+        UAndTerm,
+        UBVConcatTerm,
+        UBVExtendTerm,
+        UBVSelectTerm,
+        UBVToSignedTerm,
+        UBVToUnsignedTerm,
+        UBinaryTerm,
+        UComplementBitsTerm,
+        UConTerm,
+        UDivBoundedIntegralTerm,
+        UDivIntegralTerm,
+        UEqvTerm,
+        UGeneralFunApplyTerm,
+        UITETerm,
+        ULENumTerm,
+        ULTNumTerm,
+        UModBoundedIntegralTerm,
+        UModIntegralTerm,
+        UNotTerm,
+        UOrBitsTerm,
+        UOrTerm,
+        UQuotBoundedIntegralTerm,
+        UQuotIntegralTerm,
+        URemBoundedIntegralTerm,
+        URemIntegralTerm,
+        URotateBitsTerm,
+        UShiftBitsTerm,
+        USignumNumTerm,
+        USymTerm,
+        UTabularFunApplyTerm,
+        UTernaryTerm,
+        UTimesNumTerm,
+        UUMinusNumTerm,
+        UUnaryTerm,
+        UXorBitsTerm
+      ),
+    UnaryOp,
+    type (-->),
+  )
+import Grisette.IR.SymPrim.Data.TabularFun
+  ( type (=->),
+  )
+import Language.Haskell.TH.Syntax (Lift)
+import Type.Reflection (Typeable, typeRep)
 
 internTerm :: forall t. (SupportedPrim t) => Uninterned (Term t) -> Term t
 internTerm !bt = unsafeDupablePerformIO $ atomicModifyIORef' slot go
diff --git a/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/InternedCtors.hs-boot b/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/InternedCtors.hs-boot
--- a/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/InternedCtors.hs-boot
+++ b/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/InternedCtors.hs-boot
@@ -54,15 +54,28 @@
   )
 where
 
-import Control.DeepSeq
-import Data.Bits
-import Data.Hashable
-import Data.Typeable
-import GHC.TypeNats
+import Control.DeepSeq (NFData)
+import Data.Bits (Bits)
+import Data.Hashable (Hashable)
+import Data.Typeable (Typeable)
+import GHC.TypeNats (KnownNat, type (+), type (<=))
 import Grisette.Core.Data.Class.BitVector
+  ( BVSignConversion,
+    SizedBV,
+  )
 import {-# SOURCE #-} Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
+  ( BinaryOp,
+    SupportedPrim,
+    Term,
+    TernaryOp,
+    TypedSymbol,
+    UnaryOp,
+    type (-->),
+  )
 import {-# SOURCE #-} Grisette.IR.SymPrim.Data.TabularFun
-import Language.Haskell.TH.Syntax
+  ( type (=->),
+  )
+import Language.Haskell.TH.Syntax (Lift)
 
 constructUnary ::
   forall tag arg t.
diff --git a/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/SomeTerm.hs b/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/SomeTerm.hs
--- a/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/SomeTerm.hs
+++ b/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/SomeTerm.hs
@@ -13,10 +13,15 @@
 -- Portability :   GHC only
 module Grisette.IR.SymPrim.Data.Prim.InternedTerm.SomeTerm (SomeTerm (..)) where
 
-import Data.Hashable
-import Data.Typeable
+import Data.Hashable (Hashable (hashWithSalt))
+import Data.Typeable (Proxy (Proxy), typeRep)
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
+  ( SupportedPrim,
+    Term,
+  )
 import {-# SOURCE #-} Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermUtils
+  ( identityWithTypeRep,
+  )
 
 data SomeTerm where
   SomeTerm :: forall a. (SupportedPrim a) => Term a -> SomeTerm
diff --git a/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/Term.hs b/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/Term.hs
--- a/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/Term.hs
+++ b/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/Term.hs
@@ -51,34 +51,115 @@
   )
 where
 
-import Control.DeepSeq
-import Data.Bits
+import Control.DeepSeq (NFData (rnf))
+import Data.Bits (Bits)
 import Data.Function (on)
-import Data.Hashable
+import Data.Hashable (Hashable (hashWithSalt))
 import Data.Interned
-import Data.Kind
-import Data.String
-import Data.Typeable (Proxy (..), cast)
-import GHC.Generics
-import GHC.TypeNats
-import Grisette.Core.Data.BV
+  ( Cache,
+    Id,
+    Interned (Description, Uninterned, cache, describe, identify),
+  )
+import Data.Kind (Constraint)
+import Data.String (IsString (fromString))
+import Data.Typeable (Proxy (Proxy), cast)
+import GHC.Generics (Generic)
+import GHC.TypeNats (KnownNat, Nat, type (+), type (<=))
+import Grisette.Core.Data.BV (IntN, WordN)
 import Grisette.Core.Data.Class.BitVector
-import Grisette.Core.Data.Class.Function
+  ( BVSignConversion,
+    SizedBV,
+  )
+import Grisette.Core.Data.Class.Function (Function (Arg, Ret, (#)))
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Caches
+  ( typeMemoizedCache,
+  )
 import {-# SOURCE #-} Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors
+  ( absNumTerm,
+    addNumTerm,
+    andBitsTerm,
+    andTerm,
+    bvToSignedTerm,
+    bvToUnsignedTerm,
+    bvconcatTerm,
+    bvextendTerm,
+    bvselectTerm,
+    complementBitsTerm,
+    conTerm,
+    constructBinary,
+    constructTernary,
+    constructUnary,
+    divBoundedIntegralTerm,
+    divIntegralTerm,
+    eqvTerm,
+    generalFunApplyTerm,
+    iteTerm,
+    leNumTerm,
+    ltNumTerm,
+    modBoundedIntegralTerm,
+    modIntegralTerm,
+    notTerm,
+    orBitsTerm,
+    orTerm,
+    quotBoundedIntegralTerm,
+    quotIntegralTerm,
+    remBoundedIntegralTerm,
+    remIntegralTerm,
+    rotateBitsTerm,
+    shiftBitsTerm,
+    signumNumTerm,
+    symTerm,
+    tabularFunApplyTerm,
+    timesNumTerm,
+    uminusNumTerm,
+    xorBitsTerm,
+  )
 import {-# SOURCE #-} Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermSubstitution
+  ( substTerm,
+  )
 import {-# SOURCE #-} Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermUtils
+  ( identity,
+    introSupportedPrimConstraint,
+    pformat,
+  )
 import Grisette.IR.SymPrim.Data.Prim.ModelValue
+  ( ModelValue,
+    toModelValue,
+  )
 import Grisette.IR.SymPrim.Data.Prim.Utils
-import {-# SOURCE #-} Grisette.IR.SymPrim.Data.TabularFun
-import Language.Haskell.TH.Syntax
-import Language.Haskell.TH.Syntax.Compat
+  ( eqHeteroRep,
+    eqTypeRepBool,
+  )
+import Grisette.IR.SymPrim.Data.TabularFun
+  ( type (=->) (TabularFun),
+  )
+import Language.Haskell.TH.Syntax (Lift (lift, liftTyped))
+import Language.Haskell.TH.Syntax.Compat (unTypeSplice)
 import Type.Reflection
+  ( SomeTypeRep (SomeTypeRep),
+    TypeRep,
+    Typeable,
+    eqTypeRep,
+    typeRep,
+    type (:~~:) (HRefl),
+  )
 
 #if MIN_VERSION_prettyprinter(1,7,0)
 import Prettyprinter
+  ( column,
+    pageWidth,
+    Doc,
+    PageWidth(Unbounded, AvailablePerLine),
+    Pretty(pretty),
+  )
 #else
 import Data.Text.Prettyprint.Doc
+  ( column,
+    pageWidth,
+    Doc,
+    PageWidth(Unbounded, AvailablePerLine),
+    Pretty(pretty),
+  )
 #endif
 
 -- $setup
@@ -89,7 +170,7 @@
 -- term.
 class (Lift t, Typeable t, Hashable t, Eq t, Show t, NFData t) => SupportedPrim t where
   type PrimConstraint t :: Constraint
-  type PrimConstraint t = ()
+  type PrimConstraint _ = ()
   default withPrim :: (PrimConstraint t) => proxy t -> ((PrimConstraint t) => a) -> a
   withPrim :: proxy t -> ((PrimConstraint t) => a) -> a
   withPrim _ i = i
@@ -1099,3 +1180,10 @@
 instance (SupportedPrim a, SupportedPrim b) => SupportedPrim (a --> b) where
   type PrimConstraint (a --> b) = (SupportedPrim a, SupportedPrim b)
   defaultValue = buildGeneralFun (SimpleSymbol "a") (conTerm defaultValue)
+
+instance
+  (SupportedPrim a, SupportedPrim b) =>
+  SupportedPrim (a =-> b)
+  where
+  type PrimConstraint (a =-> b) = (SupportedPrim a, SupportedPrim b)
+  defaultValue = TabularFun [] (defaultValue @b)
diff --git a/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/Term.hs-boot b/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/Term.hs-boot
--- a/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/Term.hs-boot
+++ b/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/Term.hs-boot
@@ -28,22 +28,29 @@
   )
 where
 
-import Control.DeepSeq
-import Data.Bits
-import Data.Hashable
-import Data.Interned
-import Data.Kind
-import GHC.TypeNats
+import Control.DeepSeq (NFData)
+import Data.Bits (Bits)
+import Data.Hashable (Hashable)
+import Data.Interned (Cache, Id)
+import Data.Kind (Constraint)
+import GHC.TypeNats (KnownNat, type (+), type (<=))
 import Grisette.Core.Data.Class.BitVector
-import Grisette.Core.Data.Class.Function
+  ( BVSignConversion,
+    SizedBV,
+  )
 import Grisette.IR.SymPrim.Data.Prim.ModelValue
+  ( ModelValue,
+    toModelValue,
+  )
 import {-# SOURCE #-} Grisette.IR.SymPrim.Data.TabularFun
-import Language.Haskell.TH.Syntax
-import Type.Reflection
+  ( type (=->),
+  )
+import Language.Haskell.TH.Syntax (Lift)
+import Type.Reflection (TypeRep, Typeable)
 
 class (Lift t, Typeable t, Hashable t, Eq t, Show t, NFData t) => SupportedPrim t where
   type PrimConstraint t :: Constraint
-  type PrimConstraint t = ()
+  type PrimConstraint _ = ()
   default withPrim :: (PrimConstraint t) => proxy t -> ((PrimConstraint t) => a) -> a
   withPrim :: proxy t -> ((PrimConstraint t) => a) -> a
   withPrim _ i = i
diff --git a/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/TermSubstitution.hs b/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/TermSubstitution.hs
--- a/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/TermSubstitution.hs
+++ b/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/TermSubstitution.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE GADTs #-}
+{-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
@@ -12,21 +13,122 @@
 -- Maintainer  :   siruilu@cs.washington.edu
 -- Stability   :   Experimental
 -- Portability :   GHC only
-module Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermSubstitution (substTerm) where
+module Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermSubstitution
+  ( substTerm,
+  )
+where
 
-import Grisette.Core.Data.MemoUtils
+import Grisette.Core.Data.MemoUtils (htmemo)
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors
+  ( conTerm,
+  )
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.SomeTerm
+  ( SomeTerm (SomeTerm),
+  )
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
+  ( BinaryOp (partialEvalBinary),
+    SupportedPrim,
+    Term
+      ( AbsNumTerm,
+        AddNumTerm,
+        AndBitsTerm,
+        AndTerm,
+        BVConcatTerm,
+        BVExtendTerm,
+        BVSelectTerm,
+        BVToSignedTerm,
+        BVToUnsignedTerm,
+        BinaryTerm,
+        ComplementBitsTerm,
+        ConTerm,
+        DivBoundedIntegralTerm,
+        DivIntegralTerm,
+        EqvTerm,
+        GeneralFunApplyTerm,
+        ITETerm,
+        LENumTerm,
+        LTNumTerm,
+        ModBoundedIntegralTerm,
+        ModIntegralTerm,
+        NotTerm,
+        OrBitsTerm,
+        OrTerm,
+        QuotBoundedIntegralTerm,
+        QuotIntegralTerm,
+        RemBoundedIntegralTerm,
+        RemIntegralTerm,
+        RotateBitsTerm,
+        ShiftBitsTerm,
+        SignumNumTerm,
+        SymTerm,
+        TabularFunApplyTerm,
+        TernaryTerm,
+        TimesNumTerm,
+        UMinusNumTerm,
+        UnaryTerm,
+        XorBitsTerm
+      ),
+    TernaryOp (partialEvalTernary),
+    TypedSymbol,
+    UnaryOp (partialEvalUnary),
+    someTypedSymbol,
+    type (-->) (GeneralFun),
+  )
 import Grisette.IR.SymPrim.Data.Prim.PartialEval.BV
+  ( pevalBVConcatTerm,
+    pevalBVExtendTerm,
+    pevalBVSelectTerm,
+    pevalBVToSignedTerm,
+    pevalBVToUnsignedTerm,
+  )
 import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bits
+  ( pevalAndBitsTerm,
+    pevalComplementBitsTerm,
+    pevalOrBitsTerm,
+    pevalRotateBitsTerm,
+    pevalShiftBitsTerm,
+    pevalXorBitsTerm,
+  )
 import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bool
+  ( pevalAndTerm,
+    pevalEqvTerm,
+    pevalITETerm,
+    pevalNotTerm,
+    pevalOrTerm,
+  )
 import Grisette.IR.SymPrim.Data.Prim.PartialEval.GeneralFun
+  ( pevalGeneralFunApplyTerm,
+  )
 import Grisette.IR.SymPrim.Data.Prim.PartialEval.Integral
+  ( pevalDivBoundedIntegralTerm,
+    pevalDivIntegralTerm,
+    pevalModBoundedIntegralTerm,
+    pevalModIntegralTerm,
+    pevalQuotBoundedIntegralTerm,
+    pevalQuotIntegralTerm,
+    pevalRemBoundedIntegralTerm,
+    pevalRemIntegralTerm,
+  )
 import Grisette.IR.SymPrim.Data.Prim.PartialEval.Num
+  ( pevalAbsNumTerm,
+    pevalAddNumTerm,
+    pevalLeNumTerm,
+    pevalLtNumTerm,
+    pevalSignumNumTerm,
+    pevalTimesNumTerm,
+    pevalUMinusNumTerm,
+  )
 import Grisette.IR.SymPrim.Data.Prim.PartialEval.TabularFun
+  ( pevalTabularFunApplyTerm,
+  )
 import Type.Reflection
-import Unsafe.Coerce
+  ( TypeRep,
+    eqTypeRep,
+    typeRep,
+    pattern App,
+    type (:~~:) (HRefl),
+  )
+import Unsafe.Coerce (unsafeCoerce)
 
 substTerm :: forall a b. (SupportedPrim a, SupportedPrim b) => TypedSymbol a -> Term a -> Term b -> Term b
 substTerm sym term = gov
diff --git a/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/TermSubstitution.hs-boot b/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/TermSubstitution.hs-boot
--- a/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/TermSubstitution.hs-boot
+++ b/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/TermSubstitution.hs-boot
@@ -1,7 +1,20 @@
 {-# LANGUAGE RankNTypes #-}
 
-module Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermSubstitution (substTerm) where
+module Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermSubstitution
+  ( substTerm,
+  )
+where
 
 import {-# SOURCE #-} Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
+  ( SupportedPrim,
+    Term,
+    TypedSymbol,
+  )
 
-substTerm :: forall a b. (SupportedPrim a, SupportedPrim b) => TypedSymbol a -> Term a -> Term b -> Term b
+substTerm ::
+  forall a b.
+  (SupportedPrim a, SupportedPrim b) =>
+  TypedSymbol a ->
+  Term a ->
+  Term b ->
+  Term b
diff --git a/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/TermUtils.hs b/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/TermUtils.hs
--- a/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/TermUtils.hs
+++ b/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/TermUtils.hs
@@ -27,13 +27,74 @@
 where
 
 import Control.Monad.State
-import Data.HashMap.Strict as M
-import Data.HashSet as S
-import Data.Interned
+  ( MonadState (get, put),
+    State,
+    evalState,
+    execState,
+    gets,
+    modify',
+  )
+import qualified Data.HashMap.Strict as M
+import qualified Data.HashSet as S
+import Data.Interned (Id)
 import Data.Typeable
+  ( Proxy (Proxy),
+    TypeRep,
+    Typeable,
+    cast,
+    typeRep,
+  )
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.SomeTerm
+  ( SomeTerm (SomeTerm),
+  )
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
-import Grisette.IR.SymPrim.Data.TabularFun ()
+  ( BinaryOp (pformatBinary),
+    SomeTypedSymbol (SomeTypedSymbol),
+    SupportedPrim (pformatCon, pformatSym),
+    Term
+      ( AbsNumTerm,
+        AddNumTerm,
+        AndBitsTerm,
+        AndTerm,
+        BVConcatTerm,
+        BVExtendTerm,
+        BVSelectTerm,
+        BVToSignedTerm,
+        BVToUnsignedTerm,
+        BinaryTerm,
+        ComplementBitsTerm,
+        ConTerm,
+        DivBoundedIntegralTerm,
+        DivIntegralTerm,
+        EqvTerm,
+        GeneralFunApplyTerm,
+        ITETerm,
+        LENumTerm,
+        LTNumTerm,
+        ModBoundedIntegralTerm,
+        ModIntegralTerm,
+        NotTerm,
+        OrBitsTerm,
+        OrTerm,
+        QuotBoundedIntegralTerm,
+        QuotIntegralTerm,
+        RemBoundedIntegralTerm,
+        RemIntegralTerm,
+        RotateBitsTerm,
+        ShiftBitsTerm,
+        SignumNumTerm,
+        SymTerm,
+        TabularFunApplyTerm,
+        TernaryTerm,
+        TimesNumTerm,
+        UMinusNumTerm,
+        UnaryTerm,
+        XorBitsTerm
+      ),
+    TernaryOp (pformatTernary),
+    TypedSymbol,
+    UnaryOp (pformatUnary),
+  )
 import qualified Type.Reflection as R
 
 identity :: Term t -> Id
diff --git a/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/TermUtils.hs-boot b/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/TermUtils.hs-boot
--- a/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/TermUtils.hs-boot
+++ b/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/TermUtils.hs-boot
@@ -12,10 +12,14 @@
   )
 where
 
-import Data.HashSet as S
-import Data.Interned
-import Data.Typeable
+import qualified Data.HashSet as S
+import Data.Interned (Id)
+import Data.Typeable (TypeRep, Typeable)
 import {-# SOURCE #-} Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
+  ( SomeTypedSymbol,
+    SupportedPrim,
+    Term,
+  )
 
 identity :: Term t -> Id
 identityWithTypeRep :: forall t. Term t -> (TypeRep, Id)
diff --git a/src/Grisette/IR/SymPrim/Data/Prim/Model.hs b/src/Grisette/IR/SymPrim/Data/Prim/Model.hs
--- a/src/Grisette/IR/SymPrim/Data/Prim/Model.hs
+++ b/src/Grisette/IR/SymPrim/Data/Prim/Model.hs
@@ -5,6 +5,7 @@
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE InstanceSigs #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
@@ -29,26 +30,157 @@
 
 import qualified Data.HashMap.Strict as M
 import qualified Data.HashSet as S
-import Data.Hashable
-import Data.List
-import Data.Proxy
-import GHC.Generics
+import Data.Hashable (Hashable)
+import Data.List (sort, sortOn)
+import Data.Proxy (Proxy (Proxy))
+import GHC.Generics (Generic)
 import Grisette.Core.Data.Class.ExtractSymbolics
+  ( ExtractSymbolics (extractSymbolics),
+  )
 import Grisette.Core.Data.Class.ModelOps
-import Grisette.Core.Data.MemoUtils
+  ( ModelOps
+      ( emptyModel,
+        exceptFor,
+        exceptFor',
+        extendTo,
+        insertValue,
+        isEmptyModel,
+        modelContains,
+        restrictTo,
+        valueOf
+      ),
+    ModelRep (buildModel),
+    SymbolSetOps
+      ( containsSymbol,
+        differenceSet,
+        emptySet,
+        insertSymbol,
+        intersectionSet,
+        isEmptySet,
+        unionSet
+      ),
+    SymbolSetRep (buildSymbolSet),
+  )
+import Grisette.Core.Data.MemoUtils (htmemo)
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors
+  ( conTerm,
+    symTerm,
+  )
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.SomeTerm
+  ( SomeTerm (SomeTerm),
+  )
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
+  ( BinaryOp (partialEvalBinary),
+    SomeTypedSymbol (SomeTypedSymbol),
+    SupportedPrim (defaultValue, defaultValueDynamic),
+    Term
+      ( AbsNumTerm,
+        AddNumTerm,
+        AndBitsTerm,
+        AndTerm,
+        BVConcatTerm,
+        BVExtendTerm,
+        BVSelectTerm,
+        BVToSignedTerm,
+        BVToUnsignedTerm,
+        BinaryTerm,
+        ComplementBitsTerm,
+        ConTerm,
+        DivBoundedIntegralTerm,
+        DivIntegralTerm,
+        EqvTerm,
+        GeneralFunApplyTerm,
+        ITETerm,
+        LENumTerm,
+        LTNumTerm,
+        ModBoundedIntegralTerm,
+        ModIntegralTerm,
+        NotTerm,
+        OrBitsTerm,
+        OrTerm,
+        QuotBoundedIntegralTerm,
+        QuotIntegralTerm,
+        RemBoundedIntegralTerm,
+        RemIntegralTerm,
+        RotateBitsTerm,
+        ShiftBitsTerm,
+        SignumNumTerm,
+        SymTerm,
+        TabularFunApplyTerm,
+        TernaryTerm,
+        TimesNumTerm,
+        UMinusNumTerm,
+        UnaryTerm,
+        XorBitsTerm
+      ),
+    TernaryOp (partialEvalTernary),
+    TypedSymbol,
+    UnaryOp (partialEvalUnary),
+    showUntyped,
+    someTypedSymbol,
+    withSymbolSupported,
+    type (-->) (GeneralFun),
+  )
 import Grisette.IR.SymPrim.Data.Prim.ModelValue
+  ( ModelValue,
+    toModelValue,
+    unsafeFromModelValue,
+  )
 import Grisette.IR.SymPrim.Data.Prim.PartialEval.BV
+  ( pevalBVConcatTerm,
+    pevalBVExtendTerm,
+    pevalBVSelectTerm,
+    pevalBVToSignedTerm,
+    pevalBVToUnsignedTerm,
+  )
 import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bits
+  ( pevalAndBitsTerm,
+    pevalComplementBitsTerm,
+    pevalOrBitsTerm,
+    pevalRotateBitsTerm,
+    pevalShiftBitsTerm,
+    pevalXorBitsTerm,
+  )
 import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bool
+  ( pevalAndTerm,
+    pevalEqvTerm,
+    pevalITETerm,
+    pevalNotTerm,
+    pevalOrTerm,
+  )
 import Grisette.IR.SymPrim.Data.Prim.PartialEval.GeneralFun
+  ( pevalGeneralFunApplyTerm,
+  )
 import Grisette.IR.SymPrim.Data.Prim.PartialEval.Integral
+  ( pevalDivBoundedIntegralTerm,
+    pevalDivIntegralTerm,
+    pevalModBoundedIntegralTerm,
+    pevalModIntegralTerm,
+    pevalQuotBoundedIntegralTerm,
+    pevalQuotIntegralTerm,
+    pevalRemBoundedIntegralTerm,
+    pevalRemIntegralTerm,
+  )
 import Grisette.IR.SymPrim.Data.Prim.PartialEval.Num
+  ( pevalAbsNumTerm,
+    pevalAddNumTerm,
+    pevalLeNumTerm,
+    pevalLtNumTerm,
+    pevalSignumNumTerm,
+    pevalTimesNumTerm,
+    pevalUMinusNumTerm,
+  )
 import Grisette.IR.SymPrim.Data.Prim.PartialEval.TabularFun
+  ( pevalTabularFunApplyTerm,
+  )
 import Type.Reflection
-import Unsafe.Coerce
+  ( TypeRep,
+    eqTypeRep,
+    typeRep,
+    pattern App,
+    type (:~~:) (HRefl),
+  )
+import Unsafe.Coerce (unsafeCoerce)
 
 -- $setup
 -- >>> import Grisette.Core
diff --git a/src/Grisette/IR/SymPrim/Data/Prim/Model.hs-boot b/src/Grisette/IR/SymPrim/Data/Prim/Model.hs-boot
--- a/src/Grisette/IR/SymPrim/Data/Prim/Model.hs-boot
+++ b/src/Grisette/IR/SymPrim/Data/Prim/Model.hs-boot
@@ -1,7 +1,12 @@
-module Grisette.IR.SymPrim.Data.Prim.Model where
+module Grisette.IR.SymPrim.Data.Prim.Model
+  ( SymbolSet (..),
+  )
+where
 
 import qualified Data.HashSet as S
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
+  ( SomeTypedSymbol,
+  )
 
 newtype SymbolSet = SymbolSet {unSymbolSet :: S.HashSet SomeTypedSymbol}
 
diff --git a/src/Grisette/IR/SymPrim/Data/Prim/ModelValue.hs b/src/Grisette/IR/SymPrim/Data/Prim/ModelValue.hs
--- a/src/Grisette/IR/SymPrim/Data/Prim/ModelValue.hs
+++ b/src/Grisette/IR/SymPrim/Data/Prim/ModelValue.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE ExplicitNamespaces #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
@@ -18,8 +19,14 @@
   )
 where
 
-import Data.Hashable
+import Data.Hashable (Hashable (hashWithSalt))
 import Type.Reflection
+  ( TypeRep,
+    Typeable,
+    eqTypeRep,
+    typeRep,
+    type (:~~:) (HRefl),
+  )
 
 data ModelValue where
   ModelValue :: forall v. (Show v, Eq v, Hashable v) => TypeRep v -> v -> ModelValue
diff --git a/src/Grisette/IR/SymPrim/Data/Prim/PartialEval/BV.hs b/src/Grisette/IR/SymPrim/Data/Prim/PartialEval/BV.hs
--- a/src/Grisette/IR/SymPrim/Data/Prim/PartialEval/BV.hs
+++ b/src/Grisette/IR/SymPrim/Data/Prim/PartialEval/BV.hs
@@ -29,13 +29,31 @@
   )
 where
 
-import Data.Typeable
-import GHC.TypeNats
+import Data.Typeable (Typeable)
+import GHC.TypeNats (KnownNat, type (+), type (<=))
 import Grisette.Core.Data.Class.BitVector
+  ( BVSignConversion (toSigned, toUnsigned),
+    SizedBV (sizedBVConcat, sizedBVSelect, sizedBVSext, sizedBVZext),
+  )
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors
+  ( bvToSignedTerm,
+    bvToUnsignedTerm,
+    bvconcatTerm,
+    bvextendTerm,
+    bvselectTerm,
+    conTerm,
+  )
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
+  ( SupportedPrim,
+    Term (BVToSignedTerm, BVToUnsignedTerm, ConTerm),
+  )
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermUtils
+  ( castTerm,
+  )
 import Grisette.IR.SymPrim.Data.Prim.PartialEval.Unfold
+  ( binaryUnfoldOnce,
+    unaryUnfoldOnce,
+  )
 
 -- ToSigned
 pevalBVToSignedTerm ::
diff --git a/src/Grisette/IR/SymPrim/Data/Prim/PartialEval/Bits.hs b/src/Grisette/IR/SymPrim/Data/Prim/PartialEval/Bits.hs
--- a/src/Grisette/IR/SymPrim/Data/Prim/PartialEval/Bits.hs
+++ b/src/Grisette/IR/SymPrim/Data/Prim/PartialEval/Bits.hs
@@ -26,10 +26,35 @@
 where
 
 import Data.Bits
-import Data.Typeable
+  ( Bits
+      ( bitSizeMaybe,
+        complement,
+        rotate,
+        shift,
+        xor,
+        zeroBits,
+        (.&.),
+        (.|.)
+      ),
+  )
+import Data.Typeable (Typeable, cast)
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors
+  ( andBitsTerm,
+    complementBitsTerm,
+    conTerm,
+    orBitsTerm,
+    rotateBitsTerm,
+    shiftBitsTerm,
+    xorBitsTerm,
+  )
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
+  ( SupportedPrim,
+    Term (ComplementBitsTerm, ConTerm, RotateBitsTerm, ShiftBitsTerm),
+  )
 import Grisette.IR.SymPrim.Data.Prim.PartialEval.Unfold
+  ( binaryUnfoldOnce,
+    unaryUnfoldOnce,
+  )
 
 bitsConTermView :: (Bits b, Typeable b) => Term a -> Maybe b
 bitsConTermView (ConTerm _ b) = cast b
diff --git a/src/Grisette/IR/SymPrim/Data/Prim/PartialEval/Bool.hs b/src/Grisette/IR/SymPrim/Data/Prim/PartialEval/Bool.hs
--- a/src/Grisette/IR/SymPrim/Data/Prim/PartialEval/Bool.hs
+++ b/src/Grisette/IR/SymPrim/Data/Prim/PartialEval/Bool.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE ExplicitNamespaces #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
@@ -35,14 +36,34 @@
   )
 where
 
-import Control.Monad
-import Data.Maybe
-import Data.Typeable
+import Control.Monad (msum)
+import Data.Maybe (fromMaybe)
+import Data.Typeable (cast, eqT, type (:~:) (Refl))
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors
+  ( andTerm,
+    conTerm,
+    eqvTerm,
+    iteTerm,
+    notTerm,
+    orTerm,
+  )
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
+  ( SupportedPrim,
+    Term
+      ( AddNumTerm,
+        AndTerm,
+        ConTerm,
+        EqvTerm,
+        ITETerm,
+        NotTerm,
+        OrTerm
+      ),
+  )
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermUtils
-import Grisette.IR.SymPrim.Data.Prim.Utils
-import Unsafe.Coerce
+  ( castTerm,
+  )
+import Grisette.IR.SymPrim.Data.Prim.Utils (pattern Dyn)
+import Unsafe.Coerce (unsafeCoerce)
 
 trueTerm :: Term Bool
 trueTerm = conTerm True
diff --git a/src/Grisette/IR/SymPrim/Data/Prim/PartialEval/GeneralFun.hs b/src/Grisette/IR/SymPrim/Data/Prim/PartialEval/GeneralFun.hs
--- a/src/Grisette/IR/SymPrim/Data/Prim/PartialEval/GeneralFun.hs
+++ b/src/Grisette/IR/SymPrim/Data/Prim/PartialEval/GeneralFun.hs
@@ -11,14 +11,26 @@
 -- Maintainer  :   siruilu@cs.washington.edu
 -- Stability   :   Experimental
 -- Portability :   GHC only
-module Grisette.IR.SymPrim.Data.Prim.PartialEval.GeneralFun (pevalGeneralFunApplyTerm) where
+module Grisette.IR.SymPrim.Data.Prim.PartialEval.GeneralFun
+  ( pevalGeneralFunApplyTerm,
+  )
+where
 
-import Grisette.Core.Data.Class.Function
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors
+  ( generalFunApplyTerm,
+  )
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
+  ( SupportedPrim,
+    Term (ConTerm, ITETerm),
+    type (-->) (GeneralFun),
+  )
 import {-# SOURCE #-} Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermSubstitution
+  ( substTerm,
+  )
 import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bool (pevalITETerm)
 import Grisette.IR.SymPrim.Data.Prim.PartialEval.PartialEval
+  ( totalize2,
+  )
 
 pevalGeneralFunApplyTerm :: (SupportedPrim a, SupportedPrim b) => Term (a --> b) -> Term a -> Term b
 pevalGeneralFunApplyTerm = totalize2 doPevalGeneralFunApplyTerm generalFunApplyTerm
diff --git a/src/Grisette/IR/SymPrim/Data/Prim/PartialEval/Integral.hs b/src/Grisette/IR/SymPrim/Data/Prim/PartialEval/Integral.hs
--- a/src/Grisette/IR/SymPrim/Data/Prim/PartialEval/Integral.hs
+++ b/src/Grisette/IR/SymPrim/Data/Prim/PartialEval/Integral.hs
@@ -20,12 +20,22 @@
   )
 where
 
-import Grisette.Core.Data.BV
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors
+  ( conTerm,
+    divBoundedIntegralTerm,
+    divIntegralTerm,
+    modIntegralTerm,
+    quotBoundedIntegralTerm,
+    quotIntegralTerm,
+    remIntegralTerm,
+  )
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
-import Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermUtils
+  ( SupportedPrim,
+    Term (ConTerm),
+  )
 import Grisette.IR.SymPrim.Data.Prim.PartialEval.Unfold
-import Grisette.IR.SymPrim.Data.Prim.Utils
+  ( binaryUnfoldOnce,
+  )
 
 -- div
 pevalDivIntegralTerm :: (SupportedPrim a, Integral a) => Term a -> Term a -> Term a
diff --git a/src/Grisette/IR/SymPrim/Data/Prim/PartialEval/Num.hs b/src/Grisette/IR/SymPrim/Data/Prim/PartialEval/Num.hs
--- a/src/Grisette/IR/SymPrim/Data/Prim/PartialEval/Num.hs
+++ b/src/Grisette/IR/SymPrim/Data/Prim/PartialEval/Num.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE ExplicitNamespaces #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
@@ -31,12 +32,33 @@
   )
 where
 
-import Data.Typeable
+import Data.Typeable (Typeable, cast, eqT, type (:~:) (Refl))
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors
+  ( absNumTerm,
+    addNumTerm,
+    conTerm,
+    leNumTerm,
+    ltNumTerm,
+    signumNumTerm,
+    timesNumTerm,
+    uminusNumTerm,
+  )
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
+  ( SupportedPrim,
+    Term
+      ( AbsNumTerm,
+        AddNumTerm,
+        ConTerm,
+        TimesNumTerm,
+        UMinusNumTerm
+      ),
+  )
 import Grisette.IR.SymPrim.Data.Prim.PartialEval.Unfold
-import Grisette.IR.SymPrim.Data.Prim.Utils
-import Unsafe.Coerce
+  ( binaryUnfoldOnce,
+    unaryUnfoldOnce,
+  )
+import Grisette.IR.SymPrim.Data.Prim.Utils (pattern Dyn)
+import Unsafe.Coerce (unsafeCoerce)
 
 numConTermView :: (Num b, Typeable b) => Term a -> Maybe b
 numConTermView (ConTerm _ b) = cast b
diff --git a/src/Grisette/IR/SymPrim/Data/Prim/PartialEval/PartialEval.hs b/src/Grisette/IR/SymPrim/Data/Prim/PartialEval/PartialEval.hs
--- a/src/Grisette/IR/SymPrim/Data/Prim/PartialEval/PartialEval.hs
+++ b/src/Grisette/IR/SymPrim/Data/Prim/PartialEval/PartialEval.hs
@@ -31,8 +31,8 @@
   )
 where
 
-import Control.Monad.Except
-import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
+import Control.Monad.Except (MonadError (catchError))
+import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term (Term)
 
 type PartialFun a b = a -> Maybe b
 
diff --git a/src/Grisette/IR/SymPrim/Data/Prim/PartialEval/TabularFun.hs b/src/Grisette/IR/SymPrim/Data/Prim/PartialEval/TabularFun.hs
--- a/src/Grisette/IR/SymPrim/Data/Prim/PartialEval/TabularFun.hs
+++ b/src/Grisette/IR/SymPrim/Data/Prim/PartialEval/TabularFun.hs
@@ -16,12 +16,25 @@
   )
 where
 
-import Grisette.Core.Data.Class.Function
+import Grisette.Core.Data.Class.Function (Function ((#)))
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors
+  ( conTerm,
+    tabularFunApplyTerm,
+  )
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
+  ( SupportedPrim,
+    Term (ConTerm),
+  )
 import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bool
+  ( pevalEqvTerm,
+    pevalITETerm,
+  )
 import Grisette.IR.SymPrim.Data.Prim.PartialEval.PartialEval
+  ( totalize2,
+  )
 import Grisette.IR.SymPrim.Data.TabularFun
+  ( type (=->) (TabularFun),
+  )
 
 pevalTabularFunApplyTerm :: (SupportedPrim a, SupportedPrim b) => Term (a =-> b) -> Term a -> Term b
 pevalTabularFunApplyTerm = totalize2 doPevalTabularFunApplyTerm tabularFunApplyTerm
diff --git a/src/Grisette/IR/SymPrim/Data/Prim/PartialEval/Unfold.hs b/src/Grisette/IR/SymPrim/Data/Prim/PartialEval/Unfold.hs
--- a/src/Grisette/IR/SymPrim/Data/Prim/PartialEval/Unfold.hs
+++ b/src/Grisette/IR/SymPrim/Data/Prim/PartialEval/Unfold.hs
@@ -16,11 +16,23 @@
   )
 where
 
-import Control.Monad.Except
-import Data.Typeable
+import Control.Monad.Except (MonadError (catchError))
+import Data.Typeable (Typeable)
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
+  ( SupportedPrim,
+    Term (ITETerm),
+  )
 import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bool
+  ( pevalITETerm,
+  )
 import Grisette.IR.SymPrim.Data.Prim.PartialEval.PartialEval
+  ( PartialRuleBinary,
+    PartialRuleUnary,
+    TotalRuleBinary,
+    TotalRuleUnary,
+    totalize,
+    totalize2,
+  )
 
 unaryPartialUnfoldOnce ::
   forall a b.
diff --git a/src/Grisette/IR/SymPrim/Data/Prim/Utils.hs b/src/Grisette/IR/SymPrim/Data/Prim/Utils.hs
--- a/src/Grisette/IR/SymPrim/Data/Prim/Utils.hs
+++ b/src/Grisette/IR/SymPrim/Data/Prim/Utils.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE ExplicitNamespaces #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE PolyKinds #-}
@@ -26,6 +27,12 @@
 
 import Data.Typeable (cast)
 import Type.Reflection
+  ( TypeRep,
+    Typeable,
+    eqTypeRep,
+    typeRep,
+    type (:~~:) (HRefl),
+  )
 
 pattern Dyn :: (Typeable a, Typeable b) => a -> b
 pattern Dyn x <- (cast -> Just x)
diff --git a/src/Grisette/IR/SymPrim/Data/SymPrim.hs b/src/Grisette/IR/SymPrim/Data/SymPrim.hs
--- a/src/Grisette/IR/SymPrim/Data/SymPrim.hs
+++ b/src/Grisette/IR/SymPrim/Data/SymPrim.hs
@@ -10,6 +10,7 @@
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE InstanceSigs #-}
+{-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE StandaloneDeriving #-}
@@ -56,62 +57,227 @@
   )
 where
 
-import Control.DeepSeq
-import Control.Monad.Except
+import Control.DeepSeq (NFData (rnf))
+import Control.Monad.Except (ExceptT (ExceptT), MonadError (throwError))
 import Control.Monad.Identity
-import Control.Monad.Trans.Maybe
+  ( Identity (Identity),
+    IdentityT (IdentityT),
+  )
+import Control.Monad.Trans.Maybe (MaybeT (MaybeT))
 import qualified Control.Monad.Writer.Lazy as WriterLazy
 import qualified Control.Monad.Writer.Strict as WriterStrict
 import Data.Bits
+  ( Bits
+      ( bit,
+        bitSize,
+        bitSizeMaybe,
+        clearBit,
+        complement,
+        complementBit,
+        isSigned,
+        popCount,
+        rotate,
+        rotateL,
+        rotateR,
+        setBit,
+        shift,
+        shiftL,
+        shiftR,
+        testBit,
+        unsafeShiftL,
+        unsafeShiftR,
+        xor,
+        zeroBits,
+        (.&.),
+        (.|.)
+      ),
+    FiniteBits (finiteBitSize),
+  )
 import qualified Data.ByteString as B
-import Data.Functor.Sum
-import Data.Hashable
-import Data.Int
-import Data.Proxy
-import Data.String
+import Data.Functor.Sum (Sum)
+import Data.Hashable (Hashable (hashWithSalt))
+import Data.Int (Int16, Int32, Int64, Int8)
+import Data.Proxy (Proxy (Proxy))
+import Data.String (IsString (fromString))
 import qualified Data.Text as T
-import Data.Typeable
-import Data.Word
+import Data.Typeable (typeRep, type (:~:) (Refl))
+import Data.Word (Word16, Word32, Word64, Word8)
 import GHC.Generics
+  ( Generic (Rep, from),
+    K1 (K1),
+    M1 (M1),
+    U1,
+    type (:*:) ((:*:)),
+    type (:+:) (L1, R1),
+  )
 import GHC.TypeNats
-import Generics.Deriving
+  ( KnownNat,
+    Nat,
+    natVal,
+    sameNat,
+    type (+),
+    type (<=),
+  )
+import Generics.Deriving (Default (Default, unDefault))
 import Grisette.Core.Control.Exception
+  ( AssertionError,
+    VerificationConditions,
+  )
 import Grisette.Core.Data.BV
+  ( IntN (IntN),
+    SomeIntN (SomeIntN),
+    SomeWordN (SomeWordN),
+    WordN (WordN),
+  )
 import Grisette.Core.Data.Class.BitVector
+  ( BV (bvConcat, bvExt, bvSelect, bvSext, bvZext),
+    BVSignConversion (toSigned, toUnsigned),
+    SizedBV (sizedBVConcat, sizedBVExt, sizedBVSelect, sizedBVSext, sizedBVZext),
+  )
 import Grisette.Core.Data.Class.Bool
-import Grisette.Core.Data.Class.Error
-import Grisette.Core.Data.Class.Evaluate
+  ( LogicalOp (nots, (&&~), (||~)),
+    SEq ((/=~), (==~)),
+  )
+import Grisette.Core.Data.Class.Evaluate (EvaluateSym (evaluateSym))
 import Grisette.Core.Data.Class.ExtractSymbolics
-import Grisette.Core.Data.Class.Function
-import Grisette.Core.Data.Class.GPretty
-import Grisette.Core.Data.Class.GenSym
-import Grisette.Core.Data.Class.Mergeable
+  ( ExtractSymbolics (extractSymbolics),
+  )
+import Grisette.Core.Data.Class.Function (Function (Arg, Ret, (#)))
+import Grisette.Core.Data.Class.GPretty (GPretty (gpretty))
 import Grisette.Core.Data.Class.ModelOps
-import Grisette.Core.Data.Class.SOrd
+  ( ModelOps (emptyModel, insertValue),
+    ModelRep (buildModel),
+  )
+import Grisette.Core.Data.Class.SOrd (SOrd (symCompare, (<=~), (<~), (>=~), (>~)))
 import Grisette.Core.Data.Class.SafeArith
-import Grisette.Core.Data.Class.SimpleMergeable
+  ( ArithException (DivideByZero, Overflow, Underflow),
+    SafeDivision
+      ( safeDiv,
+        safeDiv',
+        safeDivMod,
+        safeDivMod',
+        safeMod,
+        safeMod',
+        safeQuot,
+        safeQuot',
+        safeQuotRem,
+        safeQuotRem',
+        safeRem,
+        safeRem'
+      ),
+    SafeLinearArith
+      ( safeAdd,
+        safeAdd',
+        safeMinus,
+        safeMinus',
+        safeNeg,
+        safeNeg'
+      ),
+    SymIntegerOp,
+  )
+import Grisette.Core.Data.Class.SimpleMergeable (mrgIf)
 import Grisette.Core.Data.Class.Solvable
-import Grisette.Core.Data.Class.Substitute
-import Grisette.Core.Data.Class.ToCon
-import Grisette.Core.Data.Class.ToSym
-import Grisette.IR.SymPrim.Data.IntBitwidth
+  ( Solvable (con, conView, iinfosym, isym, sinfosym, ssym),
+    pattern Con,
+  )
+import Grisette.Core.Data.Class.Substitute (SubstituteSym (substituteSym))
+import Grisette.Core.Data.Class.ToCon (ToCon (toCon))
+import Grisette.Core.Data.Class.ToSym (ToSym (toSym))
+import Grisette.IR.SymPrim.Data.IntBitwidth (intBitwidthQ)
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors
+  ( conTerm,
+    iinfosymTerm,
+    isymTerm,
+    sinfosymTerm,
+    ssymTerm,
+    symTerm,
+  )
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.SomeTerm
+  ( SomeTerm (SomeTerm),
+  )
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
+  ( ConRep (ConType),
+    LinkedRep (underlyingTerm, wrapTerm),
+    SupportedPrim,
+    SymRep (SymType),
+    Term (ConTerm, SymTerm),
+    TypedSymbol (WithInfo),
+    prettyPrintTerm,
+    type (-->) (GeneralFun),
+  )
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermSubstitution
+  ( substTerm,
+  )
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermUtils
+  ( extractSymbolicsTerm,
+    pformat,
+    someTermsSize,
+    termSize,
+    termsSize,
+  )
 import Grisette.IR.SymPrim.Data.Prim.Model
+  ( Model,
+    SymbolSet (SymbolSet),
+    evaluateTerm,
+  )
 import Grisette.IR.SymPrim.Data.Prim.PartialEval.BV
+  ( pevalBVConcatTerm,
+    pevalBVExtendTerm,
+    pevalBVSelectTerm,
+    pevalBVToSignedTerm,
+    pevalBVToUnsignedTerm,
+  )
 import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bits
+  ( pevalAndBitsTerm,
+    pevalComplementBitsTerm,
+    pevalOrBitsTerm,
+    pevalRotateBitsTerm,
+    pevalShiftBitsTerm,
+    pevalXorBitsTerm,
+  )
 import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bool
+  ( pevalEqvTerm,
+  )
 import Grisette.IR.SymPrim.Data.Prim.PartialEval.GeneralFun
+  ( pevalGeneralFunApplyTerm,
+  )
 import Grisette.IR.SymPrim.Data.Prim.PartialEval.Integral
+  ( pevalDivBoundedIntegralTerm,
+    pevalDivIntegralTerm,
+    pevalModBoundedIntegralTerm,
+    pevalModIntegralTerm,
+    pevalQuotBoundedIntegralTerm,
+    pevalQuotIntegralTerm,
+    pevalRemBoundedIntegralTerm,
+    pevalRemIntegralTerm,
+  )
 import Grisette.IR.SymPrim.Data.Prim.PartialEval.Num
+  ( pevalAbsNumTerm,
+    pevalAddNumTerm,
+    pevalGeNumTerm,
+    pevalGtNumTerm,
+    pevalLeNumTerm,
+    pevalLtNumTerm,
+    pevalMinusNumTerm,
+    pevalSignumNumTerm,
+    pevalTimesNumTerm,
+    pevalUMinusNumTerm,
+  )
 import Grisette.IR.SymPrim.Data.Prim.PartialEval.TabularFun
-import Grisette.IR.SymPrim.Data.TabularFun
-import Grisette.Lib.Control.Monad
+  ( pevalTabularFunApplyTerm,
+  )
+import Grisette.IR.SymPrim.Data.TabularFun (type (=->))
+import Grisette.Lib.Control.Monad (mrgReturn)
 import Grisette.Utils.Parameterized
-import Language.Haskell.TH.Syntax
+  ( KnownProof (KnownProof),
+    LeqProof (LeqProof),
+    knownAdd,
+    leqAddPos,
+    leqTrans,
+    unsafeKnownProof,
+    unsafeLeqProof,
+  )
+import Language.Haskell.TH.Syntax (Lift)
 
 -- $setup
 -- >>> import Grisette.Core
@@ -186,7 +352,7 @@
   safeNeg v = mrgReturn $ -v
   safeNeg' _ v = mrgReturn $ -v
   safeMinus ls rs = mrgReturn $ ls - rs
-  safeMinus' e ls rs = mrgReturn $ ls - rs
+  safeMinus' _ ls rs = mrgReturn $ ls - rs
 
 instance SymIntegerOp SymInteger
 
@@ -320,11 +486,11 @@
   SomeSymIntN :: (KnownNat n, 1 <= n) => SymIntN n -> SomeSymIntN
 
 unarySomeSymIntN :: (forall n. (KnownNat n, 1 <= n) => SymIntN n -> r) -> String -> SomeSymIntN -> r
-unarySomeSymIntN op str (SomeSymIntN (w :: SymIntN w)) = op w
+unarySomeSymIntN op _ (SomeSymIntN (w :: SymIntN w)) = op w
 {-# INLINE unarySomeSymIntN #-}
 
 unarySomeSymIntNR1 :: (forall n. (KnownNat n, 1 <= n) => SymIntN n -> SymIntN n) -> String -> SomeSymIntN -> SomeSymIntN
-unarySomeSymIntNR1 op str (SomeSymIntN (w :: SymIntN w)) = SomeSymIntN $ op w
+unarySomeSymIntNR1 op _ (SomeSymIntN (w :: SymIntN w)) = SomeSymIntN $ op w
 {-# INLINE unarySomeSymIntNR1 #-}
 
 binSomeSymIntN :: (forall n. (KnownNat n, 1 <= n) => SymIntN n -> SymIntN n -> r) -> String -> SomeSymIntN -> SomeSymIntN -> r
@@ -432,11 +598,11 @@
   SomeSymWordN :: (KnownNat n, 1 <= n) => SymWordN n -> SomeSymWordN
 
 unarySomeSymWordN :: (forall n. (KnownNat n, 1 <= n) => SymWordN n -> r) -> String -> SomeSymWordN -> r
-unarySomeSymWordN op str (SomeSymWordN (w :: SymWordN w)) = op w
+unarySomeSymWordN op _ (SomeSymWordN (w :: SymWordN w)) = op w
 {-# INLINE unarySomeSymWordN #-}
 
 unarySomeSymWordNR1 :: (forall n. (KnownNat n, 1 <= n) => SymWordN n -> SymWordN n) -> String -> SomeSymWordN -> SomeSymWordN
-unarySomeSymWordNR1 op str (SomeSymWordN (w :: SymWordN w)) = SomeSymWordN $ op w
+unarySomeSymWordNR1 op _ (SomeSymWordN (w :: SymWordN w)) = SomeSymWordN $ op w
 {-# INLINE unarySomeSymWordNR1 #-}
 
 binSomeSymWordN :: (forall n. (KnownNat n, 1 <= n) => SymWordN n -> SymWordN n -> r) -> String -> SomeSymWordN -> SomeSymWordN -> r
@@ -1356,7 +1522,7 @@
     where \
       n = fromIntegral $ natVal (Proxy @n); \
       res :: forall (w :: Nat) (ix :: Nat). Proxy w -> Proxy ix -> somety; \
-      res p1 p2 = \
+      res _ _ = \
         case ( unsafeKnownProof @ix (fromIntegral ix), \
                unsafeKnownProof @w (fromIntegral w), \
                unsafeLeqProof @1 @w, \
@@ -1447,10 +1613,6 @@
 
 someUnderlyingTerm :: SomeSym -> SomeTerm
 someUnderlyingTerm (SomeSym s) = SomeTerm $ underlyingTerm s
-
-someSymSize :: [SomeSym] -> Int
-someSymSize = someTermsSize . fmap someUnderlyingTerm
-{-# INLINE someSymSize #-}
 
 someSymsSize :: [SomeSym] -> Int
 someSymsSize = someTermsSize . fmap someUnderlyingTerm
diff --git a/src/Grisette/IR/SymPrim/Data/SymPrim.hs-boot b/src/Grisette/IR/SymPrim/Data/SymPrim.hs-boot
--- a/src/Grisette/IR/SymPrim/Data/SymPrim.hs-boot
+++ b/src/Grisette/IR/SymPrim/Data/SymPrim.hs-boot
@@ -31,18 +31,24 @@
   )
 where
 
-import Control.DeepSeq
-import Data.Hashable
-import GHC.Generics
-import GHC.TypeNats
-import Grisette.Core.Data.BV
-import Grisette.Core.Data.Class.Evaluate
+import Control.DeepSeq (NFData)
+import Data.Hashable (Hashable)
+import GHC.TypeNats (KnownNat, Nat, type (<=))
+import Grisette.Core.Data.BV (IntN, WordN)
+import Grisette.Core.Data.Class.Evaluate (EvaluateSym)
 import Grisette.Core.Data.Class.ExtractSymbolics
-import Grisette.Core.Data.Class.GPretty
-import Grisette.Core.Data.Class.Solvable
+  ( ExtractSymbolics,
+  )
+import Grisette.Core.Data.Class.GPretty (GPretty)
+import Grisette.Core.Data.Class.Solvable (Solvable)
 import {-# SOURCE #-} Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
-import Grisette.IR.SymPrim.Data.TabularFun
-import Language.Haskell.TH.Syntax
+  ( LinkedRep,
+    SupportedPrim,
+    Term,
+    type (-->),
+  )
+import Grisette.IR.SymPrim.Data.TabularFun (type (=->))
+import Language.Haskell.TH.Syntax (Lift)
 
 newtype SymBool = SymBool {underlyingBoolTerm :: Term Bool}
 
diff --git a/src/Grisette/IR/SymPrim/Data/TabularFun.hs b/src/Grisette/IR/SymPrim/Data/TabularFun.hs
--- a/src/Grisette/IR/SymPrim/Data/TabularFun.hs
+++ b/src/Grisette/IR/SymPrim/Data/TabularFun.hs
@@ -2,7 +2,6 @@
 {-# LANGUAGE DeriveGeneric #-}
 {-# LANGUAGE DeriveLift #-}
 {-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
 
@@ -19,12 +18,11 @@
   )
 where
 
-import Control.DeepSeq
-import Data.Hashable
-import GHC.Generics
-import Grisette.Core.Data.Class.Function
-import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
-import Language.Haskell.TH.Syntax
+import Control.DeepSeq (NFData, NFData1)
+import Data.Hashable (Hashable)
+import GHC.Generics (Generic, Generic1)
+import Grisette.Core.Data.Class.Function (Function (Arg, Ret, (#)))
+import Language.Haskell.TH.Syntax (Lift)
 
 -- $setup
 -- >>> import Grisette.Core
@@ -45,13 +43,6 @@
   deriving (Show, Eq, Generic, Generic1, Lift, NFData, NFData1)
 
 infixr 0 =->
-
-instance
-  (SupportedPrim a, SupportedPrim b) =>
-  SupportedPrim (a =-> b)
-  where
-  type PrimConstraint (a =-> b) = (SupportedPrim a, SupportedPrim b)
-  defaultValue = TabularFun [] (defaultValue @b)
 
 instance (Eq a) => Function (a =-> b) where
   type Arg (a =-> b) = a
diff --git a/src/Grisette/IR/SymPrim/Data/TabularFun.hs-boot b/src/Grisette/IR/SymPrim/Data/TabularFun.hs-boot
--- a/src/Grisette/IR/SymPrim/Data/TabularFun.hs-boot
+++ b/src/Grisette/IR/SymPrim/Data/TabularFun.hs-boot
@@ -5,4 +5,18 @@
   )
 where
 
+import Control.DeepSeq (NFData)
+import Data.Hashable (Hashable)
+import Language.Haskell.TH.Syntax (Lift)
+
 data (=->) a b = TabularFun {funcTable :: [(a, b)], defaultFuncValue :: b}
+
+instance (Eq a, Eq b) => Eq (a =-> b)
+
+instance (Show a, Show b) => Show (a =-> b)
+
+instance (Hashable a, Hashable b) => Hashable (a =-> b)
+
+instance (Lift a, Lift b) => Lift (a =-> b)
+
+instance (NFData a, NFData b) => NFData (a =-> b)
diff --git a/src/Grisette/Internal/Backend/SBV.hs b/src/Grisette/Internal/Backend/SBV.hs
--- a/src/Grisette/Internal/Backend/SBV.hs
+++ b/src/Grisette/Internal/Backend/SBV.hs
@@ -14,4 +14,7 @@
 where
 
 import Grisette.Backend.SBV.Data.SMT.Lowering
-import Grisette.Backend.SBV.Data.SMT.Solving
+  ( lowerSinglePrim,
+    parseModel,
+  )
+import Grisette.Backend.SBV.Data.SMT.Solving (TermTy)
diff --git a/src/Grisette/Internal/Core.hs b/src/Grisette/Internal/Core.hs
--- a/src/Grisette/Internal/Core.hs
+++ b/src/Grisette/Internal/Core.hs
@@ -1,4 +1,6 @@
 {-# LANGUAGE Trustworthy #-}
+-- Disable this warning because we are re-exporting things.
+{-# OPTIONS_GHC -Wno-missing-import-lists #-}
 
 -- |
 -- Module      :   Grisette.Internal.Core
@@ -23,4 +25,13 @@
 where
 
 import Grisette.Core.Control.Monad.UnionM
+  ( UnionM (..),
+    isMerged,
+    underlyingUnion,
+  )
 import Grisette.Core.Data.Union
+  ( Union (..),
+    fullReconstruct,
+    ifWithLeftMost,
+    ifWithStrategy,
+  )
diff --git a/src/Grisette/Internal/IR/SymPrim.hs b/src/Grisette/Internal/IR/SymPrim.hs
--- a/src/Grisette/Internal/IR/SymPrim.hs
+++ b/src/Grisette/Internal/IR/SymPrim.hs
@@ -1,4 +1,6 @@
 {-# LANGUAGE PatternSynonyms #-}
+-- Disable this warning because we are re-exporting things.
+{-# OPTIONS_GHC -Wno-missing-import-lists #-}
 
 -- |
 -- Module      :   Grisette.Internal.IR.SymPrim
@@ -91,16 +93,103 @@
 where
 
 import Grisette.IR.SymPrim.Data.Prim.Helpers
+  ( pattern BinaryTermPatt,
+    pattern TernaryTermPatt,
+    pattern UnaryTermPatt,
+  )
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors
+  ( conTerm,
+    constructBinary,
+    constructTernary,
+    constructUnary,
+    iinfosymTerm,
+    isymTerm,
+    sinfosymTerm,
+    ssymTerm,
+    symTerm,
+  )
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.SomeTerm
+  ( SomeTerm (..),
+  )
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
+  ( BinaryOp (..),
+    SomeTypedSymbol (..),
+    SupportedPrim (..),
+    Term (..),
+    TernaryOp (..),
+    UnaryOp (..),
+    showUntyped,
+    someTypedSymbol,
+    withSymbolSupported,
+  )
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermUtils
-import Grisette.IR.SymPrim.Data.Prim.Model
+  ( castTerm,
+    extractSymbolicsTerm,
+    identity,
+    identityWithTypeRep,
+    introSupportedPrimConstraint,
+    pformat,
+    termSize,
+    termsSize,
+  )
+import Grisette.IR.SymPrim.Data.Prim.Model (evaluateTerm)
 import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bool
+  ( falseTerm,
+    pevalAndTerm,
+    pevalEqvTerm,
+    pevalITETerm,
+    pevalImplyTerm,
+    pevalNotEqvTerm,
+    pevalNotTerm,
+    pevalOrTerm,
+    pevalXorTerm,
+    trueTerm,
+    pattern BoolConTerm,
+    pattern BoolTerm,
+    pattern FalseTerm,
+    pattern TrueTerm,
+  )
 import Grisette.IR.SymPrim.Data.Prim.PartialEval.GeneralFun
+  ( pevalGeneralFunApplyTerm,
+  )
 import Grisette.IR.SymPrim.Data.Prim.PartialEval.Integral
+  ( pevalDivIntegralTerm,
+    pevalModIntegralTerm,
+    pevalQuotIntegralTerm,
+    pevalRemIntegralTerm,
+  )
 import Grisette.IR.SymPrim.Data.Prim.PartialEval.Num
+  ( pevalAbsNumTerm,
+    pevalAddNumTerm,
+    pevalGeNumTerm,
+    pevalGtNumTerm,
+    pevalLeNumTerm,
+    pevalLtNumTerm,
+    pevalMinusNumTerm,
+    pevalSignumNumTerm,
+    pevalTimesNumTerm,
+    pevalUMinusNumTerm,
+    pattern NumConTerm,
+    pattern NumOrdConTerm,
+  )
 import Grisette.IR.SymPrim.Data.Prim.PartialEval.PartialEval
+  ( BinaryCommPartialStrategy (..),
+    BinaryPartialStrategy (..),
+    PartialFun,
+    PartialRuleBinary,
+    PartialRuleUnary,
+    TotalRuleBinary,
+    TotalRuleUnary,
+    UnaryPartialStrategy (..),
+    binaryPartial,
+    totalize,
+    totalize2,
+    unaryPartial,
+  )
 import Grisette.IR.SymPrim.Data.Prim.PartialEval.TabularFun
+  ( pevalTabularFunApplyTerm,
+  )
 import Grisette.IR.SymPrim.Data.Prim.PartialEval.Unfold
-import Grisette.IR.SymPrim.Data.SymPrim
+  ( binaryUnfoldOnce,
+    unaryUnfoldOnce,
+  )
diff --git a/src/Grisette/Lib/Base.hs b/src/Grisette/Lib/Base.hs
--- a/src/Grisette/Lib/Base.hs
+++ b/src/Grisette/Lib/Base.hs
@@ -49,6 +49,37 @@
 where
 
 import Grisette.Lib.Control.Monad
+  ( mrgBindWithStrategy,
+    mrgFmap,
+    mrgFoldM,
+    mrgMplus,
+    mrgMzero,
+    mrgReturn,
+    mrgReturnWithStrategy,
+    (>>=~),
+    (>>~),
+  )
 import Grisette.Lib.Data.Foldable
+  ( mrgFoldlM,
+    mrgFoldrM,
+    mrgForM_,
+    mrgFor_,
+    mrgMapM_,
+    mrgMsum,
+    mrgSequence_,
+    mrgTraverse_,
+  )
 import Grisette.Lib.Data.List
+  ( symDrop,
+    symFilter,
+    symTake,
+    (!!~),
+  )
 import Grisette.Lib.Data.Traversable
+  ( mrgFor,
+    mrgForM,
+    mrgMapM,
+    mrgSequence,
+    mrgSequenceA,
+    mrgTraverse,
+  )
diff --git a/src/Grisette/Lib/Control/Monad.hs b/src/Grisette/Lib/Control/Monad.hs
--- a/src/Grisette/Lib/Control/Monad.hs
+++ b/src/Grisette/Lib/Control/Monad.hs
@@ -25,12 +25,17 @@
   )
 where
 
-import Control.Monad
-import Grisette.Core.Control.Monad.Union
-import Grisette.Core.Data.Class.Bool
+import Control.Monad (MonadPlus (mplus, mzero))
+import Grisette.Core.Control.Monad.Union (MonadUnion)
 import Grisette.Core.Data.Class.Mergeable
+  ( Mergeable,
+    MergingStrategy,
+  )
 import Grisette.Core.Data.Class.SimpleMergeable
-import Grisette.Lib.Data.Foldable
+  ( UnionLike (mergeWithStrategy),
+    merge,
+  )
+import Grisette.Lib.Data.Foldable (mrgFoldlM)
 
 -- | 'return' with 'MergingStrategy' knowledge propagation.
 mrgReturnWithStrategy :: (MonadUnion u) => MergingStrategy a -> a -> u a
diff --git a/src/Grisette/Lib/Control/Monad.hs-boot b/src/Grisette/Lib/Control/Monad.hs-boot
--- a/src/Grisette/Lib/Control/Monad.hs-boot
+++ b/src/Grisette/Lib/Control/Monad.hs-boot
@@ -1,12 +1,25 @@
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE Trustworthy #-}
 
-module Grisette.Lib.Control.Monad where
+module Grisette.Lib.Control.Monad
+  ( mrgReturnWithStrategy,
+    mrgBindWithStrategy,
+    mrgReturn,
+    (>>=~),
+    mrgFoldM,
+    (>>~),
+    mrgMzero,
+    mrgMplus,
+    mrgFmap,
+  )
+where
 
-import Control.Monad
-import Grisette.Core.Control.Monad.Union
-import Grisette.Core.Data.Class.Bool
+import Control.Monad (MonadPlus)
+import Grisette.Core.Control.Monad.Union (MonadUnion)
 import Grisette.Core.Data.Class.Mergeable
+  ( Mergeable,
+    MergingStrategy,
+  )
 
 mrgReturnWithStrategy :: (MonadUnion u) => MergingStrategy a -> a -> u a
 mrgBindWithStrategy :: (MonadUnion u) => MergingStrategy b -> u a -> (a -> u b) -> u b
diff --git a/src/Grisette/Lib/Control/Monad/Except.hs b/src/Grisette/Lib/Control/Monad/Except.hs
--- a/src/Grisette/Lib/Control/Monad/Except.hs
+++ b/src/Grisette/Lib/Control/Monad/Except.hs
@@ -15,11 +15,10 @@
   )
 where
 
-import Control.Monad.Except
-import Grisette.Core.Control.Monad.Union
-import Grisette.Core.Data.Class.Bool
-import Grisette.Core.Data.Class.Mergeable
-import Grisette.Core.Data.Class.SimpleMergeable
+import Control.Monad.Except (MonadError (catchError, throwError))
+import Grisette.Core.Control.Monad.Union (MonadUnion)
+import Grisette.Core.Data.Class.Mergeable (Mergeable)
+import Grisette.Core.Data.Class.SimpleMergeable (merge)
 
 -- | 'throwError' with 'MergingStrategy' knowledge propagation.
 mrgThrowError :: (MonadError e m, MonadUnion m, Mergeable a) => e -> m a
diff --git a/src/Grisette/Lib/Control/Monad/Trans.hs b/src/Grisette/Lib/Control/Monad/Trans.hs
--- a/src/Grisette/Lib/Control/Monad/Trans.hs
+++ b/src/Grisette/Lib/Control/Monad/Trans.hs
@@ -16,10 +16,10 @@
   )
 where
 
-import Control.Monad.Trans
-import Grisette.Core.Control.Monad.Union
-import Grisette.Core.Data.Class.Mergeable
-import Grisette.Core.Data.Class.SimpleMergeable
+import Control.Monad.Trans (MonadTrans (lift))
+import Grisette.Core.Control.Monad.Union (MonadUnion)
+import Grisette.Core.Data.Class.Mergeable (Mergeable)
+import Grisette.Core.Data.Class.SimpleMergeable (merge)
 
 -- | 'lift' with 'MergingStrategy' knowledge propagation.
 mrgLift ::
diff --git a/src/Grisette/Lib/Control/Monad/Trans/Cont.hs b/src/Grisette/Lib/Control/Monad/Trans/Cont.hs
--- a/src/Grisette/Lib/Control/Monad/Trans/Cont.hs
+++ b/src/Grisette/Lib/Control/Monad/Trans/Cont.hs
@@ -16,12 +16,14 @@
   )
 where
 
-import Control.Monad.Cont
-import Control.Monad.Trans.Class
-import Grisette.Core.Data.Class.Bool
-import Grisette.Core.Data.Class.Mergeable
+import Control.Monad.Cont (ContT (runContT))
+import Control.Monad.Trans.Class (lift)
+import Grisette.Core.Data.Class.Mergeable (Mergeable)
 import Grisette.Core.Data.Class.SimpleMergeable
-import Grisette.Lib.Control.Monad
+  ( UnionLike,
+    merge,
+  )
+import Grisette.Lib.Control.Monad (mrgReturn)
 
 -- | 'Control.Monad.Cont.runContT' with 'MergingStrategy' knowledge propagation
 mrgRunContT :: (UnionLike m, Mergeable r) => ContT r m a -> (a -> m r) -> m r
diff --git a/src/Grisette/Lib/Data/Foldable.hs b/src/Grisette/Lib/Data/Foldable.hs
--- a/src/Grisette/Lib/Data/Foldable.hs
+++ b/src/Grisette/Lib/Data/Foldable.hs
@@ -22,12 +22,15 @@
   )
 where
 
-import Control.Monad
-import Grisette.Core.Control.Monad.Union
-import Grisette.Core.Data.Class.Bool
-import Grisette.Core.Data.Class.Mergeable
-import Grisette.Core.Data.Class.SimpleMergeable
+import Control.Monad (MonadPlus)
+import Grisette.Core.Control.Monad.Union (MonadUnion)
+import Grisette.Core.Data.Class.Mergeable (Mergeable)
+import Grisette.Core.Data.Class.SimpleMergeable (merge)
 import {-# SOURCE #-} Grisette.Lib.Control.Monad
+  ( mrgMplus,
+    mrgMzero,
+    mrgReturn,
+  )
 
 -- | 'Data.Foldable.foldlM' with 'MergingStrategy' knowledge propagation.
 mrgFoldlM :: (MonadUnion m, Mergeable b, Foldable t) => (b -> a -> m b) -> b -> t a -> m b
diff --git a/src/Grisette/Lib/Data/List.hs b/src/Grisette/Lib/Data/List.hs
--- a/src/Grisette/Lib/Data/List.hs
+++ b/src/Grisette/Lib/Data/List.hs
@@ -17,17 +17,16 @@
   )
 where
 
-import Control.Exception
-import Control.Monad.Except
-import Grisette.Core.Control.Monad.Union
-import Grisette.Core.Data.Class.Bool
-import Grisette.Core.Data.Class.Error
-import Grisette.Core.Data.Class.Mergeable
-import Grisette.Core.Data.Class.SOrd
-import Grisette.Core.Data.Class.SafeArith
-import Grisette.Core.Data.Class.SimpleMergeable
-import Grisette.IR.SymPrim.Data.SymPrim
-import Grisette.Lib.Control.Monad
+import Control.Exception (ArrayException (IndexOutOfBounds))
+import Control.Monad.Except (MonadError (throwError))
+import Grisette.Core.Control.Monad.Union (MonadUnion)
+import Grisette.Core.Data.Class.Bool (SEq ((==~)))
+import Grisette.Core.Data.Class.Error (TransformError (transformError))
+import Grisette.Core.Data.Class.Mergeable (Mergeable)
+import Grisette.Core.Data.Class.SOrd (SOrd ((<=~)))
+import Grisette.Core.Data.Class.SimpleMergeable (mrgIf)
+import Grisette.IR.SymPrim.Data.SymPrim (SymBool, SymInteger)
+import Grisette.Lib.Control.Monad (mrgFmap, mrgReturn)
 
 -- | Symbolic version of 'Data.List.!!', the result would be merged and
 -- propagate the mergeable knowledge.
diff --git a/src/Grisette/Lib/Data/Traversable.hs b/src/Grisette/Lib/Data/Traversable.hs
--- a/src/Grisette/Lib/Data/Traversable.hs
+++ b/src/Grisette/Lib/Data/Traversable.hs
@@ -21,9 +21,16 @@
   )
 where
 
-import Grisette.Core.Control.Monad.Union
+import Grisette.Core.Control.Monad.Union (MonadUnion)
 import Grisette.Core.Data.Class.Mergeable
+  ( Mergeable,
+    Mergeable1,
+    rootStrategy1,
+  )
 import Grisette.Core.Data.Class.SimpleMergeable
+  ( UnionLike (mergeWithStrategy),
+    merge,
+  )
 
 -- | 'Data.Traversable.traverse' with 'MergingStrategy' knowledge propagation.
 mrgTraverse ::
diff --git a/src/Grisette/Lib/Mtl.hs b/src/Grisette/Lib/Mtl.hs
--- a/src/Grisette/Lib/Mtl.hs
+++ b/src/Grisette/Lib/Mtl.hs
@@ -26,5 +26,12 @@
 where
 
 import Grisette.Lib.Control.Monad.Except
-import Grisette.Lib.Control.Monad.Trans
+  ( mrgCatchError,
+    mrgThrowError,
+  )
+import Grisette.Lib.Control.Monad.Trans (mrgLift)
 import Grisette.Lib.Control.Monad.Trans.Cont
+  ( mrgEvalContT,
+    mrgResetT,
+    mrgRunContT,
+  )
diff --git a/src/Grisette/Qualified/ParallelUnionDo.hs b/src/Grisette/Qualified/ParallelUnionDo.hs
--- a/src/Grisette/Qualified/ParallelUnionDo.hs
+++ b/src/Grisette/Qualified/ParallelUnionDo.hs
@@ -6,11 +6,14 @@
 -- Maintainer  :   siruilu@cs.washington.edu
 -- Stability   :   Experimental
 -- Portability :   GHC only
-module Grisette.Qualified.ParallelUnionDo where
+module Grisette.Qualified.ParallelUnionDo ((>>=), (>>)) where
 
-import Control.Parallel.Strategies
+import Control.Parallel.Strategies (NFData)
 import Grisette.Core.Control.Monad.Class.MonadParallelUnion
-import Grisette.Core.Data.Class.Mergeable
+  ( MonadParallelUnion (parBindUnion),
+  )
+import Grisette.Core.Data.Class.Mergeable (Mergeable)
+import Prelude (const, ($))
 
 (>>=) :: (MonadParallelUnion m, Mergeable b, NFData b) => m a -> (a -> m b) -> m b
 (>>=) = parBindUnion
diff --git a/src/Grisette/Utils.hs b/src/Grisette/Utils.hs
--- a/src/Grisette/Utils.hs
+++ b/src/Grisette/Utils.hs
@@ -1,3 +1,6 @@
+-- Disable this warning because we are re-exporting things.
+{-# OPTIONS_GHC -Wno-missing-import-lists #-}
+
 -- |
 -- Module      :   Grisette.Utils
 -- Copyright   :   (c) Sirui Lu 2021-2023
@@ -48,3 +51,32 @@
 where
 
 import Grisette.Utils.Parameterized
+  ( KnownProof (..),
+    LeqProof (..),
+    NatRepr,
+    addNat,
+    decNat,
+    divNat,
+    halfNat,
+    hasRepr,
+    incNat,
+    knownAdd,
+    leqAdd,
+    leqAdd2,
+    leqAddPos,
+    leqRefl,
+    leqSucc,
+    leqTrans,
+    leqZero,
+    natRepr,
+    natValue,
+    predNat,
+    subNat,
+    testLeq,
+    unsafeAxiom,
+    unsafeKnownProof,
+    unsafeLeqProof,
+    unsafeMkNatRepr,
+    withKnownProof,
+    withLeqProof,
+  )
diff --git a/src/Grisette/Utils/Parameterized.hs b/src/Grisette/Utils/Parameterized.hs
--- a/src/Grisette/Utils/Parameterized.hs
+++ b/src/Grisette/Utils/Parameterized.hs
@@ -88,10 +88,20 @@
   )
 where
 
-import Data.Typeable
-import GHC.Natural
+import Data.Typeable (Proxy (Proxy), type (:~:) (Refl))
+import GHC.Natural (Natural)
 import GHC.TypeNats
-import Unsafe.Coerce
+  ( Div,
+    KnownNat,
+    Nat,
+    SomeNat (SomeNat),
+    natVal,
+    someNatVal,
+    type (+),
+    type (-),
+    type (<=),
+  )
+import Unsafe.Coerce (unsafeCoerce)
 
 -- | Assert a proof of equality between two types.
 -- This is unsafe if used improperly, so use this with caution!
@@ -176,7 +186,7 @@
 
 -- | Adding two type-level natural numbers with known runtime values gives a
 -- type-level natural number with a known runtime value.
-knownAdd :: forall m n r. KnownProof m -> KnownProof n -> KnownProof (m + n)
+knownAdd :: forall m n. KnownProof m -> KnownProof n -> KnownProof (m + n)
 knownAdd KnownProof KnownProof = hasRepr @(m + n) (NatRepr (natVal (Proxy @m) + natVal (Proxy @n)))
 
 -- | @'LeqProof m n'@ is a type whose values are only inhabited when @m <= n@.
diff --git a/test/Grisette/Backend/SBV/Data/SMT/CEGISTests.hs b/test/Grisette/Backend/SBV/Data/SMT/CEGISTests.hs
--- a/test/Grisette/Backend/SBV/Data/SMT/CEGISTests.hs
+++ b/test/Grisette/Backend/SBV/Data/SMT/CEGISTests.hs
@@ -5,33 +5,53 @@
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeOperators #-}
 
-module Grisette.Backend.SBV.Data.SMT.CEGISTests where
+module Grisette.Backend.SBV.Data.SMT.CEGISTests (cegisTests) where
 
-import Control.Monad.Except
-import qualified Data.HashSet as S
-import Data.Proxy
+import Control.Monad.Except (ExceptT, runExceptT)
+import Data.Proxy (Proxy (Proxy))
 import qualified Data.SBV as SBV
-import Data.String
-import Grisette.Backend.SBV
-import Grisette.Backend.SBV.Data.SMT.Solving
+import Data.String (IsString (fromString))
+import GHC.Stack (HasCallStack)
+import Grisette.Backend.SBV (GrisetteSMTConfig, precise, z3)
 import Grisette.Core.Control.Exception
-import Grisette.Core.Control.Monad.UnionM
+  ( VerificationConditions,
+    symAssert,
+    symAssume,
+  )
+import Grisette.Core.Control.Monad.UnionM (UnionM)
 import Grisette.Core.Data.Class.BitVector
+  ( SizedBV (sizedBVConcat, sizedBVSelect, sizedBVSext, sizedBVZext),
+  )
 import Grisette.Core.Data.Class.Bool
+  ( ITEOp (ites),
+    LogicalOp (nots, xors, (&&~), (||~)),
+    SEq ((==~)),
+  )
 import Grisette.Core.Data.Class.CEGISSolver
-import Grisette.Core.Data.Class.Error
-import Grisette.Core.Data.Class.Evaluate
+  ( CEGISSolver (cegisMultiInputs),
+    cegis,
+    cegisExceptVC,
+    cegisPostCond,
+  )
+import Grisette.Core.Data.Class.Evaluate (EvaluateSym (evaluateSym))
 import Grisette.Core.Data.Class.ExtractSymbolics
-import Grisette.Core.Data.Class.Function
-import Grisette.Core.Data.Class.SOrd
-import Grisette.Core.Data.Class.SimpleMergeable
-import Grisette.Core.Data.Class.Solvable
-import Grisette.Core.Data.Class.Solver
-import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
-import Grisette.IR.SymPrim.Data.Prim.Model
+  ( ExtractSymbolics,
+  )
+import Grisette.Core.Data.Class.Function (Function ((#)))
+import Grisette.Core.Data.Class.SOrd (SOrd ((<~), (>=~)))
+import Grisette.Core.Data.Class.SimpleMergeable (mrgIf)
+import Grisette.Core.Data.Class.Solvable (Solvable (con, ssym))
+import Grisette.Core.Data.Class.Solver (Solver (solve))
 import Grisette.IR.SymPrim.Data.SymPrim
-import Test.Tasty
-import Test.Tasty.HUnit
+  ( SymBool,
+    SymIntN,
+    SymInteger,
+    type (-~>),
+    type (=~>),
+  )
+import Test.Framework (Test, testGroup)
+import Test.Framework.Providers.HUnit (testCase)
+import Test.HUnit (Assertion, assertFailure, (@=?))
 
 testCegis :: (HasCallStack, ExtractSymbolics a, EvaluateSym a, Show a) => GrisetteSMTConfig i -> Bool -> a -> [SymBool] -> Assertion
 testCegis config shouldSuccess a bs = do
@@ -63,7 +83,7 @@
             (symAssert x)
             (go xs (i + 1))
 
-cegisTests :: TestTree
+cegisTests :: Test
 cegisTests =
   let unboundedConfig = precise SBV.z3 -- {SBV.verbose=True}
    in testGroup
diff --git a/test/Grisette/Backend/SBV/Data/SMT/LoweringTests.hs b/test/Grisette/Backend/SBV/Data/SMT/LoweringTests.hs
--- a/test/Grisette/Backend/SBV/Data/SMT/LoweringTests.hs
+++ b/test/Grisette/Backend/SBV/Data/SMT/LoweringTests.hs
@@ -7,24 +7,74 @@
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeOperators #-}
 
-module Grisette.Backend.SBV.Data.SMT.LoweringTests where
+module Grisette.Backend.SBV.Data.SMT.LoweringTests (loweringTests) where
 
-import Control.Monad.Trans
+import Control.Monad.Trans (MonadTrans (lift))
 import Data.Bits
-import Data.Dynamic
+  ( Bits (complement, rotate, shift, xor, (.&.), (.|.)),
+  )
+import Data.Dynamic (Typeable, fromDynamic)
 import qualified Data.HashMap.Strict as M
-import Data.Proxy
+import Data.Proxy (Proxy (Proxy))
 import qualified Data.SBV as SBV
 import qualified Data.SBV.Control as SBV
-import Grisette.Backend.SBV.Data.SMT.Lowering
+import GHC.Stack (HasCallStack)
+import Grisette.Backend.SBV.Data.SMT.Lowering (lowerSinglePrim)
 import Grisette.Backend.SBV.Data.SMT.Solving
+  ( GrisetteSMTConfig (sbvConfig),
+    TermTy,
+    approx,
+    precise,
+  )
 import Grisette.Backend.SBV.Data.SMT.SymBiMap
-import Grisette.Core.Data.BV
+  ( SymBiMap (biMapToSBV),
+  )
+import Grisette.Core.Data.BV (IntN, WordN)
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors
+  ( absNumTerm,
+    addNumTerm,
+    andBitsTerm,
+    andTerm,
+    bvToSignedTerm,
+    bvToUnsignedTerm,
+    bvconcatTerm,
+    bvselectTerm,
+    bvsignExtendTerm,
+    bvzeroExtendTerm,
+    complementBitsTerm,
+    divBoundedIntegralTerm,
+    divIntegralTerm,
+    eqvTerm,
+    iteTerm,
+    leNumTerm,
+    ltNumTerm,
+    modBoundedIntegralTerm,
+    modIntegralTerm,
+    notTerm,
+    orBitsTerm,
+    orTerm,
+    quotBoundedIntegralTerm,
+    quotIntegralTerm,
+    remBoundedIntegralTerm,
+    remIntegralTerm,
+    rotateBitsTerm,
+    shiftBitsTerm,
+    signumNumTerm,
+    ssymTerm,
+    timesNumTerm,
+    uminusNumTerm,
+    xorBitsTerm,
+  )
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.SomeTerm
+  ( SomeTerm (SomeTerm),
+  )
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
-import Test.Tasty
-import Test.Tasty.HUnit
+  ( SupportedPrim,
+    Term,
+  )
+import Test.Framework (Test, testGroup)
+import Test.Framework.Providers.HUnit (testCase)
+import Test.HUnit (Assertion, assertFailure)
 
 testUnaryOpLowering ::
   forall a b as n.
@@ -70,21 +120,21 @@
           SBV.Unsat -> return ()
           _ -> lift $ assertFailure $ "Lowering for " ++ name ++ " generated unknown formula"
 
-testUnaryOpLowering' ::
-  forall a b as n tag.
-  ( HasCallStack,
-    UnaryOp tag a b,
-    SBV.EqSymbolic (TermTy n b),
-    Typeable (TermTy n a),
-    SBV.SymVal as,
-    TermTy n a ~ SBV.SBV as,
-    Show as
-  ) =>
-  GrisetteSMTConfig n ->
-  tag ->
-  (TermTy n a -> TermTy n b) ->
-  Assertion
-testUnaryOpLowering' config t = testUnaryOpLowering @a @b @as config (constructUnary t) (show t)
+-- testUnaryOpLowering' ::
+--   forall a b as n tag.
+--   ( HasCallStack,
+--     UnaryOp tag a b,
+--     SBV.EqSymbolic (TermTy n b),
+--     Typeable (TermTy n a),
+--     SBV.SymVal as,
+--     TermTy n a ~ SBV.SBV as,
+--     Show as
+--   ) =>
+--   GrisetteSMTConfig n ->
+--   tag ->
+--   (TermTy n a -> TermTy n b) ->
+--   Assertion
+-- testUnaryOpLowering' config t = testUnaryOpLowering @a @b @as config (constructUnary t) (show t)
 
 testBinaryOpLowering ::
   forall a b c as bs n.
@@ -139,25 +189,25 @@
           _ -> lift $ assertFailure $ "Lowering for " ++ name ++ " generated unknown formula"
       _ -> lift $ assertFailure "Failed to extract the term"
 
-testBinaryOpLowering' ::
-  forall a b c as bs n tag.
-  ( HasCallStack,
-    BinaryOp tag a b c,
-    SBV.EqSymbolic (TermTy n c),
-    Typeable (TermTy n a),
-    Typeable (TermTy n b),
-    SBV.SymVal as,
-    SBV.SymVal bs,
-    Show as,
-    Show bs,
-    TermTy n a ~ SBV.SBV as,
-    TermTy n b ~ SBV.SBV bs
-  ) =>
-  GrisetteSMTConfig n ->
-  tag ->
-  (TermTy n a -> TermTy n b -> TermTy n c) ->
-  Assertion
-testBinaryOpLowering' config t = testBinaryOpLowering @a @b @c @as @bs config (constructBinary t) (show t)
+-- testBinaryOpLowering' ::
+--   forall a b c as bs n tag.
+--   ( HasCallStack,
+--     BinaryOp tag a b c,
+--     SBV.EqSymbolic (TermTy n c),
+--     Typeable (TermTy n a),
+--     Typeable (TermTy n b),
+--     SBV.SymVal as,
+--     SBV.SymVal bs,
+--     Show as,
+--     Show bs,
+--     TermTy n a ~ SBV.SBV as,
+--     TermTy n b ~ SBV.SBV bs
+--   ) =>
+--   GrisetteSMTConfig n ->
+--   tag ->
+--   (TermTy n a -> TermTy n b -> TermTy n c) ->
+--   Assertion
+-- testBinaryOpLowering' config t = testBinaryOpLowering @a @b @c @as @bs config (constructBinary t) (show t)
 
 testTernaryOpLowering ::
   forall a b c d as bs cs n.
@@ -224,31 +274,31 @@
           _ -> lift $ assertFailure $ "Lowering for " ++ name ++ " generated unknown formula"
       _ -> lift $ assertFailure "Failed to extract the term"
 
-testTernaryOpLowering' ::
-  forall a b c d as bs cs n tag.
-  ( HasCallStack,
-    TernaryOp tag a b c d,
-    SBV.EqSymbolic (TermTy n d),
-    Typeable (TermTy n a),
-    Typeable (TermTy n b),
-    Typeable (TermTy n c),
-    SBV.SymVal as,
-    SBV.SymVal bs,
-    SBV.SymVal cs,
-    Show as,
-    Show bs,
-    Show cs,
-    TermTy n a ~ SBV.SBV as,
-    TermTy n b ~ SBV.SBV bs,
-    TermTy n c ~ SBV.SBV cs
-  ) =>
-  GrisetteSMTConfig n ->
-  tag ->
-  (TermTy n a -> TermTy n b -> TermTy n c -> TermTy n d) ->
-  Assertion
-testTernaryOpLowering' config t = testTernaryOpLowering @a @b @c @d @as @bs @cs config (constructTernary t) (show t)
+-- testTernaryOpLowering' ::
+--   forall a b c d as bs cs n tag.
+--   ( HasCallStack,
+--     TernaryOp tag a b c d,
+--     SBV.EqSymbolic (TermTy n d),
+--     Typeable (TermTy n a),
+--     Typeable (TermTy n b),
+--     Typeable (TermTy n c),
+--     SBV.SymVal as,
+--     SBV.SymVal bs,
+--     SBV.SymVal cs,
+--     Show as,
+--     Show bs,
+--     Show cs,
+--     TermTy n a ~ SBV.SBV as,
+--     TermTy n b ~ SBV.SBV bs,
+--     TermTy n c ~ SBV.SBV cs
+--   ) =>
+--   GrisetteSMTConfig n ->
+--   tag ->
+--   (TermTy n a -> TermTy n b -> TermTy n c -> TermTy n d) ->
+--   Assertion
+-- testTernaryOpLowering' config t = testTernaryOpLowering @a @b @c @d @as @bs @cs config (constructTernary t) (show t)
 
-loweringTests :: TestTree
+loweringTests :: Test
 loweringTests =
   let unboundedConfig = precise SBV.z3
       boundedConfig = approx (Proxy @5) SBV.z3
diff --git a/test/Grisette/Backend/SBV/Data/SMT/TermRewritingGen.hs b/test/Grisette/Backend/SBV/Data/SMT/TermRewritingGen.hs
--- a/test/Grisette/Backend/SBV/Data/SMT/TermRewritingGen.hs
+++ b/test/Grisette/Backend/SBV/Data/SMT/TermRewritingGen.hs
@@ -12,22 +12,127 @@
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE UndecidableInstances #-}
 
-module Grisette.Backend.SBV.Data.SMT.TermRewritingGen where
+module Grisette.Backend.SBV.Data.SMT.TermRewritingGen
+  ( TermRewritingSpec (..),
+    GeneralSpec (..),
+    DifferentSizeBVSpec (..),
+    FixedSizedBVWithBoolSpec (..),
+    BoolWithLIASpec (..),
+    LIAWithBoolSpec (..),
+    BoolOnlySpec (..),
+    constructUnarySpec',
+    constructBinarySpec',
+    constructTernarySpec',
+    divIntegralSpec,
+    modIntegralSpec,
+    quotIntegralSpec,
+    remIntegralSpec,
+    divBoundedIntegralSpec,
+    modBoundedIntegralSpec,
+    quotBoundedIntegralSpec,
+    remBoundedIntegralSpec,
+    uminusNumSpec,
+    timesNumSpec,
+    addNumSpec,
+    iteSpec,
+    eqvSpec,
+    notSpec,
+    andSpec,
+    orSpec,
+  )
+where
 
-import Data.Bits
-import Data.Data
-import Data.Kind
-import GHC.TypeLits
-import Grisette.Core.Data.Class.BitVector
+import Data.Bits (Bits)
+import Data.Data (Proxy (Proxy), Typeable)
+import Data.Kind (Type)
+import GHC.TypeLits (KnownNat, Nat, type (+), type (<=))
+import Grisette.Core.Data.Class.BitVector (SizedBV)
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors
+  ( absNumTerm,
+    addNumTerm,
+    andBitsTerm,
+    andTerm,
+    bvconcatTerm,
+    bvextendTerm,
+    bvselectTerm,
+    complementBitsTerm,
+    conTerm,
+    constructBinary,
+    constructTernary,
+    constructUnary,
+    divBoundedIntegralTerm,
+    divIntegralTerm,
+    eqvTerm,
+    iteTerm,
+    leNumTerm,
+    ltNumTerm,
+    modBoundedIntegralTerm,
+    modIntegralTerm,
+    notTerm,
+    orBitsTerm,
+    orTerm,
+    quotBoundedIntegralTerm,
+    quotIntegralTerm,
+    remBoundedIntegralTerm,
+    remIntegralTerm,
+    rotateBitsTerm,
+    shiftBitsTerm,
+    signumNumTerm,
+    ssymTerm,
+    timesNumTerm,
+    uminusNumTerm,
+    xorBitsTerm,
+  )
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
+  ( BinaryOp (partialEvalBinary),
+    SupportedPrim,
+    Term,
+    TernaryOp (partialEvalTernary),
+    UnaryOp (partialEvalUnary),
+  )
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermUtils
+  ( pformat,
+  )
 import Grisette.IR.SymPrim.Data.Prim.PartialEval.BV
+  ( pevalBVConcatTerm,
+    pevalBVExtendTerm,
+    pevalBVSelectTerm,
+  )
 import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bits
+  ( pevalAndBitsTerm,
+    pevalComplementBitsTerm,
+    pevalOrBitsTerm,
+    pevalRotateBitsTerm,
+    pevalShiftBitsTerm,
+    pevalXorBitsTerm,
+  )
 import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bool
+  ( pevalAndTerm,
+    pevalEqvTerm,
+    pevalITETerm,
+    pevalNotTerm,
+    pevalOrTerm,
+  )
 import Grisette.IR.SymPrim.Data.Prim.PartialEval.Integral
+  ( pevalDivBoundedIntegralTerm,
+    pevalDivIntegralTerm,
+    pevalModBoundedIntegralTerm,
+    pevalModIntegralTerm,
+    pevalQuotBoundedIntegralTerm,
+    pevalQuotIntegralTerm,
+    pevalRemBoundedIntegralTerm,
+    pevalRemIntegralTerm,
+  )
 import Grisette.IR.SymPrim.Data.Prim.PartialEval.Num
-import Test.Tasty.QuickCheck
+  ( pevalAbsNumTerm,
+    pevalAddNumTerm,
+    pevalLeNumTerm,
+    pevalLtNumTerm,
+    pevalSignumNumTerm,
+    pevalTimesNumTerm,
+    pevalUMinusNumTerm,
+  )
+import Test.QuickCheck (Arbitrary (arbitrary), Gen, frequency, oneof, sized)
 
 class (SupportedPrim b) => TermRewritingSpec a b | a -> b where
   norewriteVer :: a -> Term b
diff --git a/test/Grisette/Backend/SBV/Data/SMT/TermRewritingTests.hs b/test/Grisette/Backend/SBV/Data/SMT/TermRewritingTests.hs
--- a/test/Grisette/Backend/SBV/Data/SMT/TermRewritingTests.hs
+++ b/test/Grisette/Backend/SBV/Data/SMT/TermRewritingTests.hs
@@ -4,20 +4,63 @@
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE UndecidableInstances #-}
 
-module Grisette.Backend.SBV.Data.SMT.TermRewritingTests where
+module Grisette.Backend.SBV.Data.SMT.TermRewritingTests
+  ( termRewritingTests,
+  )
+where
 
-import Data.Foldable
+import Data.Foldable (traverse_)
 import qualified Data.SBV as SBV
 import Grisette.Backend.SBV.Data.SMT.Solving
+  ( GrisetteSMTConfig,
+    precise,
+  )
 import Grisette.Backend.SBV.Data.SMT.TermRewritingGen
-import Grisette.Core.Data.BV
-import Grisette.Core.Data.Class.Solver
+  ( BoolOnlySpec,
+    BoolWithLIASpec,
+    DifferentSizeBVSpec,
+    FixedSizedBVWithBoolSpec,
+    GeneralSpec,
+    LIAWithBoolSpec,
+    TermRewritingSpec
+      ( conSpec,
+        counterExample,
+        norewriteVer,
+        rewriteVer,
+        same,
+        symSpec
+      ),
+    addNumSpec,
+    andSpec,
+    divBoundedIntegralSpec,
+    divIntegralSpec,
+    eqvSpec,
+    iteSpec,
+    modBoundedIntegralSpec,
+    modIntegralSpec,
+    notSpec,
+    orSpec,
+    quotBoundedIntegralSpec,
+    quotIntegralSpec,
+    remBoundedIntegralSpec,
+    remIntegralSpec,
+    timesNumSpec,
+    uminusNumSpec,
+  )
+import Grisette.Core.Data.BV (IntN, WordN)
+import Grisette.Core.Data.Class.Solver (Solver (solve))
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
+  ( SupportedPrim,
+  )
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermUtils
-import Grisette.IR.SymPrim.Data.SymPrim
-import Test.Tasty
-import Test.Tasty.HUnit
-import Test.Tasty.QuickCheck
+  ( pformat,
+  )
+import Grisette.IR.SymPrim.Data.SymPrim (SymBool (SymBool))
+import Test.Framework (Test, TestName, testGroup)
+import Test.Framework.Providers.HUnit (testCase)
+import Test.Framework.Providers.QuickCheck2 (testProperty)
+import Test.HUnit (Assertion, assertFailure)
+import Test.QuickCheck (ioProperty, mapSize)
 
 validateSpec :: (TermRewritingSpec a av, Show a, SupportedPrim av) => GrisetteSMTConfig n -> a -> Assertion
 validateSpec config a = do
@@ -38,7 +81,7 @@
   (TermRewritingSpec a b, Show a, Enum b, Num b, SupportedPrim b) =>
   TestName ->
   (a -> a -> a) ->
-  TestTree
+  Test
 divisionTest name f =
   testGroup
     name
@@ -57,7 +100,7 @@
           [-3 .. 3]
     ]
 
-termRewritingTests :: TestTree
+termRewritingTests :: Test
 termRewritingTests =
   testGroup
     "TermRewritingTests"
diff --git a/test/Grisette/Core/Control/Monad/UnionMTests.hs b/test/Grisette/Core/Control/Monad/UnionMTests.hs
--- a/test/Grisette/Core/Control/Monad/UnionMTests.hs
+++ b/test/Grisette/Core/Control/Monad/UnionMTests.hs
@@ -1,15 +1,19 @@
 {-# LANGUAGE OverloadedStrings #-}
 
-module Grisette.Core.Control.Monad.UnionMTests where
+module Grisette.Core.Control.Monad.UnionMTests (unionMTests) where
 
-import Grisette.Core.Control.Monad.UnionM
-import Grisette.Core.Data.Class.GenSym
+import Grisette.Core.Control.Monad.UnionM (UnionM, unionSize)
+import Grisette.Core.Data.Class.GenSym (choose)
 import Grisette.Core.Data.Class.SimpleMergeable
-import Grisette.Core.Data.Class.Solvable
-import Test.Tasty
-import Test.Tasty.HUnit
+  ( UnionLike (single),
+    mrgIf,
+  )
+import Grisette.Core.Data.Class.Solvable (Solvable (ssym))
+import Test.Framework (Test, testGroup)
+import Test.Framework.Providers.HUnit (testCase)
+import Test.HUnit ((@=?))
 
-unionMTests :: TestTree
+unionMTests :: Test
 unionMTests =
   testGroup
     "UnionMTests"
diff --git a/test/Grisette/Core/Data/BVTests.hs b/test/Grisette/Core/Data/BVTests.hs
--- a/test/Grisette/Core/Data/BVTests.hs
+++ b/test/Grisette/Core/Data/BVTests.hs
@@ -4,22 +4,61 @@
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
 
-module Grisette.Core.Data.BVTests where
+module Grisette.Core.Data.BVTests (bvTests) where
 
-import Control.DeepSeq
+import Control.DeepSeq (NFData (rnf), deepseq, force)
 import Control.Exception
-import Control.Monad
-import Data.Bifunctor
+  ( ArithException,
+    SomeException,
+    catch,
+    evaluate,
+  )
+import Control.Monad (when)
+import Data.Bifunctor (Bifunctor (bimap))
 import Data.Bits
-import Data.Int
-import Data.Proxy
-import Data.Typeable
-import Data.Word
-import Grisette.Core.Data.BV
+  ( Bits
+      ( bit,
+        bitSizeMaybe,
+        clearBit,
+        complement,
+        complementBit,
+        isSigned,
+        popCount,
+        rotate,
+        rotateL,
+        rotateR,
+        setBit,
+        shift,
+        shiftL,
+        shiftR,
+        testBit,
+        xor,
+        zeroBits,
+        (.&.),
+        (.|.)
+      ),
+    FiniteBits (countLeadingZeros, countTrailingZeros, finiteBitSize),
+  )
+import Data.Int (Int8)
+import Data.Proxy (Proxy (Proxy))
+import Data.Typeable (Typeable, typeRep)
+import Data.Word (Word8)
+import GHC.Stack (HasCallStack)
+import Grisette.Core.Data.BV (IntN (IntN), WordN (unWordN))
 import Grisette.Core.Data.Class.BitVector
-import Test.Tasty
-import Test.Tasty.HUnit
-import Test.Tasty.QuickCheck hiding ((.&.))
+  ( SizedBV
+      ( sizedBVConcat,
+        sizedBVExt,
+        sizedBVSelect,
+        sizedBVSext,
+        sizedBVZext
+      ),
+  )
+import Test.Framework (Test, TestName, testGroup)
+import Test.Framework.Providers.HUnit (testCase)
+import Test.Framework.Providers.QuickCheck2 (testProperty)
+import Test.HUnit (Assertion, assertFailure, (@=?))
+import Test.QuickCheck (Arbitrary, Property, ioProperty)
 
 unaryConform :: forall a b c d. (Show c, Eq c, HasCallStack) => (a -> b) -> (d -> c) -> (a -> c) -> (b -> d) -> a -> Property
 unaryConform a2b d2c f g x = ioProperty $ f x @=? d2c (g (a2b x))
@@ -80,7 +119,7 @@
   Proxy ref ->
   Proxy typ ->
   Int ->
-  TestTree
+  Test
 finiteBitsConformTest pref ptyp numBits =
   testGroup
     (show (typeRep ptyp) ++ " conform to " ++ show (typeRep pref) ++ " for FiniteBits instances")
@@ -94,7 +133,7 @@
   (Typeable ref, Typeable typ, Bounded typ, Bounded ref, Integral ref, Num typ, Eq typ, Show typ) =>
   Proxy ref ->
   Proxy typ ->
-  TestTree
+  Test
 boundedConformTest pref ptyp =
   testGroup
     (show (typeRep ptyp) ++ " conform to " ++ show (typeRep pref) ++ " for Bounded instances")
@@ -117,7 +156,7 @@
   (b -> b) ->
   a ->
   b ->
-  TestTree
+  Test
 succPredLikeTest name boundName a2b fa fb bounda boundb =
   testGroup
     name
@@ -144,7 +183,7 @@
   ) =>
   Proxy ref ->
   Proxy typ ->
-  TestTree
+  Test
 enumConformTest pref ptyp =
   testGroup
     (show (typeRep ptyp) ++ " conform to " ++ show (typeRep pref) ++ " for Enum instances")
@@ -203,10 +242,10 @@
   (a -> b) ->
   (a -> a -> a) ->
   (b -> b -> b) ->
-  TestTree
+  Test
 divLikeTest name a2b fa fb =
   testGroup
-    "name"
+    name
     [ testCase "divided by zero" $ do
         sameDiv 1 0 a2b fa fb
         sameDiv 0 0 a2b fa fb
@@ -225,10 +264,10 @@
   (a -> b) ->
   (a -> a -> (a, a)) ->
   (b -> b -> (b, b)) ->
-  TestTree
+  Test
 divModLikeTest name a2b fa fb =
   testGroup
-    "name"
+    name
     [ testCase "divided by zero" $ do
         sameDivMod 1 0 a2b fa fb
         sameDivMod 0 0 a2b fa fb
@@ -245,7 +284,7 @@
   (Typeable ref, Typeable typ, Integral ref, Num typ, Arbitrary ref, Real typ, Show ref) =>
   proxy ref ->
   proxy typ ->
-  TestTree
+  Test
 realConformTest pref ptyp =
   testGroup
     (show (typeRep ptyp) ++ " conform to " ++ show (typeRep pref) ++ " for Real instances")
@@ -274,7 +313,7 @@
   ) =>
   Proxy ref ->
   Proxy typ ->
-  TestTree
+  Test
 integralConformTest pref ptyp =
   testGroup
     (show (typeRep ptyp) ++ " conform to " ++ show (typeRep pref) ++ " for Integral instances")
@@ -287,7 +326,7 @@
       testProperty "toInteger" $ unaryConform @ref @typ fromIntegral id toInteger toInteger
     ]
 
-bvTests :: TestTree
+bvTests :: Test
 bvTests =
   testGroup
     "BVTests"
diff --git a/test/Grisette/Core/Data/Class/GPrettyTests.hs b/test/Grisette/Core/Data/Class/GPrettyTests.hs
--- a/test/Grisette/Core/Data/Class/GPrettyTests.hs
+++ b/test/Grisette/Core/Data/Class/GPrettyTests.hs
@@ -5,31 +5,46 @@
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 
-module Grisette.Core.Data.Class.GPrettyTests where
+module Grisette.Core.Data.Class.GPrettyTests (gprettyTests) where
 
-import Data.Int
-import Data.Text as T
-import Data.Word
-import GHC.Generics
-import GHC.Stack
-import Generics.Deriving
+import Data.Int (Int16, Int32, Int64, Int8)
+import Data.Text as T (Text, pack, unpack)
+import Data.Word (Word16, Word32, Word64, Word8)
+import GHC.Generics (Generic)
+import GHC.Stack (HasCallStack)
+import Generics.Deriving (Default (Default))
 import Grisette.Core.Data.BV
-import Grisette.Core.Data.Class.Bool
-import Grisette.Core.Data.Class.GPretty
-import Grisette.IR.SymPrim.Data.SymPrim
-import Test.Tasty
-import Test.Tasty.HUnit
-import Test.Tasty.QuickCheck hiding ((.&.))
+  ( IntN,
+    SomeIntN (SomeIntN),
+    SomeWordN (SomeWordN),
+    WordN,
+  )
+import Grisette.Core.Data.Class.Bool (LogicalOp ((&&~)))
+import Grisette.Core.Data.Class.GPretty (GPretty (gpretty))
+import Grisette.IR.SymPrim.Data.SymPrim (SymBool)
+import Test.Framework (Test, testGroup)
+import Test.Framework.Providers.HUnit (testCase)
+import Test.Framework.Providers.QuickCheck2 (testProperty)
+import Test.HUnit ((@=?))
+import Test.QuickCheck (Arbitrary (arbitrary), Gen, forAll, oneof)
 
 #if MIN_VERSION_prettyprinter(1,7,0)
 import Prettyprinter
-import Prettyprinter.Render.Text
+  ( PageWidth(AvailablePerLine, Unbounded),
+    layoutPretty,
+    LayoutOptions(LayoutOptions),
+  )
+import Prettyprinter.Render.Text (renderStrict)
 #else
 import Data.Text.Prettyprint.Doc
-import Data.Text.Prettyprint.Doc.Render.Text
+  ( PageWidth(AvailablePerLine, Unbounded),
+    layoutPretty,
+    LayoutOptions(LayoutOptions),
+  )
+import Data.Text.Prettyprint.Doc.Render.Text (renderStrict)
 #endif
 
-testGPretty :: (HasCallStack, GPretty a) => String -> Int -> a -> T.Text -> TestTree
+testGPretty :: (HasCallStack, GPretty a) => String -> Int -> a -> T.Text -> Test
 testGPretty n i a s =
   testCase n $
     renderStrict
@@ -40,21 +55,21 @@
       @=? s
 
 propertyGPrettyShow ::
-  forall proxy a.
+  forall a.
   (HasCallStack, GPretty a, Show a) =>
   String ->
   Gen a ->
-  TestTree
+  Test
 propertyGPrettyShow n g =
   testProperty n $ forAll g $ \(a :: a) -> do
     renderStrict (layoutPretty (LayoutOptions Unbounded) (gpretty a)) == T.pack (show a)
 
 propertyGPrettyRead ::
-  forall proxy a.
+  forall a.
   (HasCallStack, GPretty a, Read a, Show a, Eq a) =>
   String ->
   Gen a ->
-  TestTree
+  Test
 propertyGPrettyRead n g =
   testProperty n $ \i -> forAll g $ \(a :: a) -> do
     read
@@ -69,11 +84,11 @@
       == a
 
 propertyGPretty ::
-  forall proxy a.
+  forall a.
   (HasCallStack, GPretty a, Read a, Show a, Eq a) =>
   String ->
   Gen a ->
-  TestTree
+  Test
 propertyGPretty n g =
   testGroup
     n
@@ -123,7 +138,7 @@
     a <- arbitrary
     Record a <$> arbitrary
 
-gprettyTests :: TestTree
+gprettyTests :: Test
 gprettyTests =
   testGroup
     "GPrettyTests"
diff --git a/test/Grisette/IR/SymPrim/Data/Prim/BVTests.hs b/test/Grisette/IR/SymPrim/Data/Prim/BVTests.hs
--- a/test/Grisette/IR/SymPrim/Data/Prim/BVTests.hs
+++ b/test/Grisette/IR/SymPrim/Data/Prim/BVTests.hs
@@ -3,17 +3,28 @@
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
 
-module Grisette.IR.SymPrim.Data.Prim.BVTests where
+module Grisette.IR.SymPrim.Data.Prim.BVTests (bvTests) where
 
-import Data.Proxy
-import Grisette.Core.Data.BV
+import Data.Proxy (Proxy (Proxy))
+import Grisette.Core.Data.BV (IntN, WordN)
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors
-import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
+  ( bvconcatTerm,
+    bvextendTerm,
+    bvselectTerm,
+    conTerm,
+    ssymTerm,
+  )
+import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term (Term)
 import Grisette.IR.SymPrim.Data.Prim.PartialEval.BV
-import Test.Tasty
-import Test.Tasty.HUnit
+  ( pevalBVConcatTerm,
+    pevalBVExtendTerm,
+    pevalBVSelectTerm,
+  )
+import Test.Framework (Test, testGroup)
+import Test.Framework.Providers.HUnit (testCase)
+import Test.HUnit ((@=?))
 
-bvTests :: TestTree
+bvTests :: Test
 bvTests =
   testGroup
     "BVTests"
diff --git a/test/Grisette/IR/SymPrim/Data/Prim/BitsTests.hs b/test/Grisette/IR/SymPrim/Data/Prim/BitsTests.hs
--- a/test/Grisette/IR/SymPrim/Data/Prim/BitsTests.hs
+++ b/test/Grisette/IR/SymPrim/Data/Prim/BitsTests.hs
@@ -1,16 +1,33 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 
-module Grisette.IR.SymPrim.Data.Prim.BitsTests where
+module Grisette.IR.SymPrim.Data.Prim.BitsTests (bitsTests) where
 
-import Grisette.Core.Data.BV
+import Grisette.Core.Data.BV (IntN, WordN)
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors
-import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
+  ( andBitsTerm,
+    complementBitsTerm,
+    conTerm,
+    orBitsTerm,
+    rotateBitsTerm,
+    shiftBitsTerm,
+    ssymTerm,
+    xorBitsTerm,
+  )
+import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term (Term)
 import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bits
-import Test.Tasty
-import Test.Tasty.HUnit
+  ( pevalAndBitsTerm,
+    pevalComplementBitsTerm,
+    pevalOrBitsTerm,
+    pevalRotateBitsTerm,
+    pevalShiftBitsTerm,
+    pevalXorBitsTerm,
+  )
+import Test.Framework (Test, testGroup)
+import Test.Framework.Providers.HUnit (testCase)
+import Test.HUnit ((@=?))
 
-bitsTests :: TestTree
+bitsTests :: Test
 bitsTests =
   testGroup
     "BitsTests"
diff --git a/test/Grisette/IR/SymPrim/Data/Prim/BoolTests.hs b/test/Grisette/IR/SymPrim/Data/Prim/BoolTests.hs
--- a/test/Grisette/IR/SymPrim/Data/Prim/BoolTests.hs
+++ b/test/Grisette/IR/SymPrim/Data/Prim/BoolTests.hs
@@ -2,17 +2,36 @@
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 
-module Grisette.IR.SymPrim.Data.Prim.BoolTests where
+module Grisette.IR.SymPrim.Data.Prim.BoolTests (boolTests) where
 
-import Grisette.Core.Data.BV
+import Grisette.Core.Data.BV (IntN, WordN)
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors
-import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
+  ( andTerm,
+    conTerm,
+    eqvTerm,
+    notTerm,
+    orTerm,
+    ssymTerm,
+  )
+import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term (Term)
 import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bool
+  ( pevalAndTerm,
+    pevalEqvTerm,
+    pevalITETerm,
+    pevalImplyTerm,
+    pevalNotEqvTerm,
+    pevalNotTerm,
+    pevalOrTerm,
+    pevalXorTerm,
+  )
 import Grisette.IR.SymPrim.Data.Prim.PartialEval.Num
-import Test.Tasty
-import Test.Tasty.HUnit
+  ( pevalAddNumTerm,
+  )
+import Test.Framework (Test, testGroup)
+import Test.Framework.Providers.HUnit (testCase)
+import Test.HUnit ((@=?))
 
-boolTests :: TestTree
+boolTests :: Test
 boolTests =
   testGroup
     "BoolTests"
diff --git a/test/Grisette/IR/SymPrim/Data/Prim/IntegralTests.hs b/test/Grisette/IR/SymPrim/Data/Prim/IntegralTests.hs
--- a/test/Grisette/IR/SymPrim/Data/Prim/IntegralTests.hs
+++ b/test/Grisette/IR/SymPrim/Data/Prim/IntegralTests.hs
@@ -3,18 +3,39 @@
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
 
-module Grisette.IR.SymPrim.Data.Prim.IntegralTests where
+module Grisette.IR.SymPrim.Data.Prim.IntegralTests (integralTests) where
 
-import Control.DeepSeq
-import Control.Exception
-import Data.Proxy
-import Grisette.Core.Data.BV
+import Control.DeepSeq (NFData (rnf), force)
+import Control.Exception (ArithException, catch, evaluate)
+import Data.Proxy (Proxy (Proxy))
+import Grisette.Core.Data.BV (IntN (IntN), WordN (WordN))
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors
+  ( conTerm,
+    divBoundedIntegralTerm,
+    divIntegralTerm,
+    modIntegralTerm,
+    quotBoundedIntegralTerm,
+    quotIntegralTerm,
+    remIntegralTerm,
+    ssymTerm,
+  )
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
+  ( SupportedPrim,
+    Term,
+  )
 import Grisette.IR.SymPrim.Data.Prim.PartialEval.Integral
-import Test.Tasty
-import Test.Tasty.HUnit
-import Test.Tasty.QuickCheck
+  ( pevalDivBoundedIntegralTerm,
+    pevalDivIntegralTerm,
+    pevalModIntegralTerm,
+    pevalQuotBoundedIntegralTerm,
+    pevalQuotIntegralTerm,
+    pevalRemIntegralTerm,
+  )
+import Test.Framework (Test, TestName, testGroup)
+import Test.Framework.Providers.HUnit (testCase)
+import Test.Framework.Providers.QuickCheck2 (testProperty)
+import Test.HUnit ((@=?))
+import Test.QuickCheck (Arbitrary, ioProperty)
 
 newtype AEWrapper = AEWrapper ArithException deriving (Eq)
 
@@ -34,22 +55,21 @@
   (Term t -> Term t -> Term t) ->
   IO ()
 sameDivPeval i j pf cf consf = do
-  cx <- evaluate (force $ Right $ cf i j) `catch` \(e :: ArithException) -> return $ Left AEWrapper
+  cx <- evaluate (force $ Right $ cf i j) `catch` \(_ :: ArithException) -> return $ Left AEWrapper
   case cx of
-    Left f -> pf (conTerm i) (conTerm j) @=? consf (conTerm i) (conTerm j)
+    Left _ -> pf (conTerm i) (conTerm j) @=? consf (conTerm i) (conTerm j)
     Right t -> pf (conTerm i) (conTerm j) @=? conTerm t
 
 divisionPevalBoundedTests ::
-  forall p t0 t.
-  (Num t, Eq t, Arbitrary t0, Show t0, Bounded t, SupportedPrim t, Integral t) =>
+  forall p t.
+  (Num t, Eq t, Bounded t, SupportedPrim t, Integral t) =>
   p t ->
   TestName ->
-  (t0 -> t) ->
   (Term t -> Term t -> Term t) ->
   (t -> t -> t) ->
   (Term t -> Term t -> Term t) ->
-  TestTree
-divisionPevalBoundedTests _ name transform pf cf consf =
+  Test
+divisionPevalBoundedTests _ name pf cf consf =
   testGroup
     name
     [ testCase "On concrete min divide by -1" $
@@ -65,8 +85,8 @@
   (Term t -> Term t -> Term t) ->
   (t -> t -> t) ->
   (Term t -> Term t -> Term t) ->
-  TestTree
-divisionPevalTests p name transform pf cf consf =
+  Test
+divisionPevalTests _ name transform pf cf consf =
   testGroup
     name
     [ testProperty "On concrete prop" $
@@ -90,12 +110,12 @@
   (forall t. (SupportedPrim t, Bounded t, Integral t) => Term t -> Term t -> Term t) ->
   (forall t. (Bounded t, Integral t) => t -> t -> t) ->
   (forall t. (SupportedPrim t, Bounded t, Integral t) => Term t -> Term t -> Term t) ->
-  TestTree
+  Test
 divisionPevalBoundedTestGroup name pf cf consf =
   testGroup
     name
     [ divisionPevalTests (Proxy @(IntN 4)) "IntN" IntN pf cf consf,
-      divisionPevalBoundedTests (Proxy @(IntN 4)) "IntN Bounded" IntN pf cf consf
+      divisionPevalBoundedTests (Proxy @(IntN 4)) "IntN Bounded" pf cf consf
     ]
 
 divisionPevalUnboundedTestGroup ::
@@ -103,13 +123,13 @@
   (forall t. (SupportedPrim t, Integral t) => Term t -> Term t -> Term t) ->
   (forall t. (Integral t) => t -> t -> t) ->
   (forall t. (SupportedPrim t, Integral t) => Term t -> Term t -> Term t) ->
-  TestTree
+  Test
 divisionPevalUnboundedTestGroup name pf cf consf =
   testGroup
     name
     [ divisionPevalTests (Proxy @Integer) "Integer" id pf cf consf,
       divisionPevalTests (Proxy @(WordN 4)) "WordN" WordN pf cf consf,
-      divisionPevalBoundedTests (Proxy @(WordN 4)) "WordN Bounded" WordN pf cf consf
+      divisionPevalBoundedTests (Proxy @(WordN 4)) "WordN Bounded" pf cf consf
     ]
 
 moduloPevalTests ::
@@ -121,8 +141,8 @@
   (Term t -> Term t -> Term t) ->
   (t -> t -> t) ->
   (Term t -> Term t -> Term t) ->
-  TestTree
-moduloPevalTests p name transform pf cf consf =
+  Test
+moduloPevalTests _ name transform pf cf consf =
   testGroup
     name
     [ testProperty "On concrete" $
@@ -148,7 +168,7 @@
   (forall t. (SupportedPrim t, Integral t) => Term t -> Term t -> Term t) ->
   (forall t. (Integral t) => t -> t -> t) ->
   (forall t. (SupportedPrim t, Integral t) => Term t -> Term t -> Term t) ->
-  TestTree
+  Test
 moduloPevalTestGroup name pf cf consf =
   testGroup
     name
@@ -157,7 +177,7 @@
       moduloPevalTests (Proxy @(WordN 4)) "WordN" WordN pf cf consf
     ]
 
-integralTests :: TestTree
+integralTests :: Test
 integralTests =
   testGroup
     "IntegralTests"
diff --git a/test/Grisette/IR/SymPrim/Data/Prim/ModelTests.hs b/test/Grisette/IR/SymPrim/Data/Prim/ModelTests.hs
--- a/test/Grisette/IR/SymPrim/Data/Prim/ModelTests.hs
+++ b/test/Grisette/IR/SymPrim/Data/Prim/ModelTests.hs
@@ -1,23 +1,53 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 
-module Grisette.IR.SymPrim.Data.Prim.ModelTests where
+module Grisette.IR.SymPrim.Data.Prim.ModelTests (modelTests) where
 
-import Data.HashMap.Strict as M
+import qualified Data.HashMap.Strict as M
 import qualified Data.HashSet as S
-import Grisette.Core.Data.BV
+import Grisette.Core.Data.BV (IntN, WordN)
 import Grisette.Core.Data.Class.ModelOps
+  ( ModelOps
+      ( emptyModel,
+        exact,
+        exceptFor,
+        extendTo,
+        insertValue,
+        restrictTo,
+        valueOf
+      ),
+    ModelRep (buildModel),
+  )
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors
+  ( conTerm,
+    ssymTerm,
+  )
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
-import Grisette.IR.SymPrim.Data.Prim.Model as Model
-import Grisette.IR.SymPrim.Data.Prim.ModelValue
+  ( Term,
+    TypedSymbol (SimpleSymbol),
+    someTypedSymbol,
+  )
+import Grisette.IR.SymPrim.Data.Prim.Model
+  ( Model (Model),
+    ModelValuePair ((::=)),
+    SymbolSet (SymbolSet),
+    equation,
+    evaluateTerm,
+  )
+import Grisette.IR.SymPrim.Data.Prim.ModelValue (toModelValue)
 import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bool
+  ( pevalEqvTerm,
+    pevalITETerm,
+  )
 import Grisette.IR.SymPrim.Data.Prim.PartialEval.Num
-import Test.Tasty
-import Test.Tasty.HUnit
-import Type.Reflection
+  ( pevalAddNumTerm,
+    pevalUMinusNumTerm,
+  )
+import Test.Framework (Test, testGroup)
+import Test.Framework.Providers.HUnit (testCase)
+import Test.HUnit ((@=?))
 
-modelTests :: TestTree
+modelTests :: Test
 modelTests =
   let asymbol :: TypedSymbol Integer = SimpleSymbol "a"
       bsymbol :: TypedSymbol Bool = SimpleSymbol "b"
diff --git a/test/Grisette/IR/SymPrim/Data/Prim/NumTests.hs b/test/Grisette/IR/SymPrim/Data/Prim/NumTests.hs
--- a/test/Grisette/IR/SymPrim/Data/Prim/NumTests.hs
+++ b/test/Grisette/IR/SymPrim/Data/Prim/NumTests.hs
@@ -1,17 +1,41 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 
-module Grisette.IR.SymPrim.Data.Prim.NumTests where
+module Grisette.IR.SymPrim.Data.Prim.NumTests (numTests) where
 
-import Grisette.Core.Data.BV
+import Grisette.Core.Data.BV (IntN, WordN)
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors
-import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
+  ( absNumTerm,
+    addNumTerm,
+    conTerm,
+    leNumTerm,
+    ltNumTerm,
+    signumNumTerm,
+    ssymTerm,
+    timesNumTerm,
+    uminusNumTerm,
+  )
+import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term (Term)
 import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bool
+  ( pevalITETerm,
+  )
 import Grisette.IR.SymPrim.Data.Prim.PartialEval.Num
-import Test.Tasty
-import Test.Tasty.HUnit
+  ( pevalAbsNumTerm,
+    pevalAddNumTerm,
+    pevalGeNumTerm,
+    pevalGtNumTerm,
+    pevalLeNumTerm,
+    pevalLtNumTerm,
+    pevalMinusNumTerm,
+    pevalSignumNumTerm,
+    pevalTimesNumTerm,
+    pevalUMinusNumTerm,
+  )
+import Test.Framework (Test, testGroup)
+import Test.Framework.Providers.HUnit (testCase)
+import Test.HUnit ((@=?))
 
-numTests :: TestTree
+numTests :: Test
 numTests =
   testGroup
     "NumTests"
diff --git a/test/Grisette/IR/SymPrim/Data/Prim/TabularFunTests.hs b/test/Grisette/IR/SymPrim/Data/Prim/TabularFunTests.hs
--- a/test/Grisette/IR/SymPrim/Data/Prim/TabularFunTests.hs
+++ b/test/Grisette/IR/SymPrim/Data/Prim/TabularFunTests.hs
@@ -1,17 +1,29 @@
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeOperators #-}
 
-module Grisette.IR.SymPrim.Data.Prim.TabularFunTests where
+module Grisette.IR.SymPrim.Data.Prim.TabularFunTests (tabularFunTests) where
 
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors
-import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
+  ( conTerm,
+    ssymTerm,
+    tabularFunApplyTerm,
+  )
+import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term (Term)
 import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bool
+  ( pevalEqvTerm,
+    pevalITETerm,
+  )
 import Grisette.IR.SymPrim.Data.Prim.PartialEval.TabularFun
+  ( pevalTabularFunApplyTerm,
+  )
 import Grisette.IR.SymPrim.Data.TabularFun
-import Test.Tasty
-import Test.Tasty.HUnit
+  ( type (=->) (TabularFun),
+  )
+import Test.Framework (Test, testGroup)
+import Test.Framework.Providers.HUnit (testCase)
+import Test.HUnit ((@=?))
 
-tabularFunTests :: TestTree
+tabularFunTests :: Test
 tabularFunTests =
   testGroup
     "TabularFunTests"
diff --git a/test/Grisette/IR/SymPrim/Data/SymPrimTests.hs b/test/Grisette/IR/SymPrim/Data/SymPrimTests.hs
--- a/test/Grisette/IR/SymPrim/Data/SymPrimTests.hs
+++ b/test/Grisette/IR/SymPrim/Data/SymPrimTests.hs
@@ -2,54 +2,198 @@
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE NegativeLiterals #-}
 {-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeOperators #-}
 {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
 
-module Grisette.IR.SymPrim.Data.SymPrimTests where
+module Grisette.IR.SymPrim.Data.SymPrimTests (symPrimTests) where
 
-import Control.DeepSeq
+import Control.DeepSeq (NFData (rnf), force)
 import Control.Exception
-import Control.Monad.Except
+  ( ArithException (DivideByZero, Overflow, Underflow),
+    catch,
+    evaluate,
+  )
+import Control.Monad.Except (ExceptT, MonadError (throwError))
 import Data.Bits
+  ( Bits
+      ( bit,
+        bitSizeMaybe,
+        complement,
+        isSigned,
+        popCount,
+        rotate,
+        shift,
+        testBit,
+        xor,
+        (.&.),
+        (.|.)
+      ),
+  )
 import qualified Data.HashMap.Strict as M
 import qualified Data.HashSet as S
-import Data.Int
-import Data.Proxy
-import Data.Word
-import Grisette.Core.Control.Monad.UnionM
-import Grisette.Core.Data.BV
+import Data.Int (Int8)
+import Data.Proxy (Proxy (Proxy))
+import Data.Word (Word8)
+import Grisette.Core.Control.Monad.UnionM (UnionM)
+import Grisette.Core.Data.BV (IntN (IntN), WordN (WordN))
 import Grisette.Core.Data.Class.BitVector
+  ( SizedBV
+      ( sizedBVConcat,
+        sizedBVExt,
+        sizedBVSelect,
+        sizedBVSext,
+        sizedBVZext
+      ),
+  )
 import Grisette.Core.Data.Class.Bool
+  ( ITEOp (ites),
+    LogicalOp (implies, nots, xors, (&&~), (||~)),
+    SEq ((/=~), (==~)),
+  )
 import Grisette.Core.Data.Class.Evaluate
+  ( EvaluateSym (evaluateSym),
+  )
 import Grisette.Core.Data.Class.ExtractSymbolics
-import Grisette.Core.Data.Class.Function
+  ( ExtractSymbolics (extractSymbolics),
+  )
+import Grisette.Core.Data.Class.Function (Function ((#)))
 import Grisette.Core.Data.Class.GenSym
+  ( genSym,
+    genSymSimple,
+    nameWithInfo,
+  )
 import Grisette.Core.Data.Class.Mergeable
+  ( Mergeable (rootStrategy),
+    MergingStrategy (SimpleStrategy),
+  )
 import Grisette.Core.Data.Class.ModelOps
+  ( ModelOps (emptyModel, insertValue),
+    ModelRep (buildModel),
+  )
 import Grisette.Core.Data.Class.SOrd
+  ( SOrd (symCompare, (<=~), (<~), (>=~), (>~)),
+  )
 import Grisette.Core.Data.Class.SafeArith
+  ( SafeDivision
+      ( safeDiv,
+        safeDiv',
+        safeDivMod,
+        safeDivMod',
+        safeMod,
+        safeMod',
+        safeQuot,
+        safeQuot',
+        safeQuotRem,
+        safeQuotRem',
+        safeRem,
+        safeRem'
+      ),
+    SafeLinearArith
+      ( safeAdd,
+        safeAdd',
+        safeMinus,
+        safeMinus',
+        safeNeg,
+        safeNeg'
+      ),
+  )
 import Grisette.Core.Data.Class.SimpleMergeable
+  ( SimpleMergeable (mrgIte),
+    merge,
+    mrgIf,
+    mrgSingle,
+  )
 import Grisette.Core.Data.Class.Solvable
-import Grisette.Core.Data.Class.ToCon
-import Grisette.Core.Data.Class.ToSym
+  ( Solvable (con, conView, iinfosym, isym, ssym),
+    pattern Con,
+  )
+import Grisette.Core.Data.Class.ToCon (ToCon (toCon))
+import Grisette.Core.Data.Class.ToSym (ToSym (toSym))
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors
+  ( conTerm,
+    isymTerm,
+    ssymTerm,
+  )
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
+  ( LinkedRep (wrapTerm),
+    Term,
+    TypedSymbol (SimpleSymbol),
+    someTypedSymbol,
+    type (-->),
+  )
 import Grisette.IR.SymPrim.Data.Prim.Model
-import Grisette.IR.SymPrim.Data.Prim.ModelValue
+  ( Model (Model),
+    SymbolSet (SymbolSet),
+  )
+import Grisette.IR.SymPrim.Data.Prim.ModelValue (toModelValue)
 import Grisette.IR.SymPrim.Data.Prim.PartialEval.BV
+  ( pevalBVConcatTerm,
+    pevalBVExtendTerm,
+    pevalBVSelectTerm,
+  )
 import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bits
+  ( pevalAndBitsTerm,
+    pevalComplementBitsTerm,
+    pevalOrBitsTerm,
+    pevalRotateBitsTerm,
+    pevalShiftBitsTerm,
+    pevalXorBitsTerm,
+  )
 import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bool
+  ( pevalAndTerm,
+    pevalEqvTerm,
+    pevalITETerm,
+    pevalImplyTerm,
+    pevalNotTerm,
+    pevalOrTerm,
+    pevalXorTerm,
+  )
 import Grisette.IR.SymPrim.Data.Prim.PartialEval.Integral
+  ( pevalDivBoundedIntegralTerm,
+    pevalDivIntegralTerm,
+    pevalModBoundedIntegralTerm,
+    pevalModIntegralTerm,
+    pevalQuotBoundedIntegralTerm,
+    pevalQuotIntegralTerm,
+    pevalRemBoundedIntegralTerm,
+    pevalRemIntegralTerm,
+  )
 import Grisette.IR.SymPrim.Data.Prim.PartialEval.Num
+  ( pevalAbsNumTerm,
+    pevalAddNumTerm,
+    pevalGeNumTerm,
+    pevalGtNumTerm,
+    pevalLeNumTerm,
+    pevalLtNumTerm,
+    pevalMinusNumTerm,
+    pevalSignumNumTerm,
+    pevalTimesNumTerm,
+    pevalUMinusNumTerm,
+  )
 import Grisette.IR.SymPrim.Data.Prim.PartialEval.TabularFun
+  ( pevalTabularFunApplyTerm,
+  )
 import Grisette.IR.SymPrim.Data.SymPrim
-import Grisette.IR.SymPrim.Data.TabularFun
-import Test.Tasty
-import Test.Tasty.HUnit
-import Test.Tasty.QuickCheck hiding ((.&.))
-import Type.Reflection hiding (Con)
+  ( ModelSymPair ((:=)),
+    SymBool (SymBool),
+    SymIntN (SymIntN),
+    SymInteger (SymInteger),
+    SymWordN (SymWordN),
+    symSize,
+    symsSize,
+    (-->),
+    type (-~>),
+    type (=~>),
+  )
+import Grisette.IR.SymPrim.Data.TabularFun (type (=->))
+import Test.Framework (Test, TestName, testGroup)
+import Test.Framework.Providers.HUnit (testCase)
+import Test.Framework.Providers.QuickCheck2 (testProperty)
+import Test.HUnit (Assertion, assertFailure, (@=?))
+import Test.QuickCheck (Arbitrary, ioProperty)
 
 newtype AEWrapper = AEWrapper ArithException deriving (Eq)
 
@@ -96,7 +240,7 @@
   (c -> c -> c) ->
   Assertion
 sameSafeDiv' i j f cf = do
-  xc <- evaluate (force $ Right $ cf i j) `catch` \(e :: ArithException) -> return $ Left ()
+  xc <- evaluate (force $ Right $ cf i j) `catch` \(_ :: ArithException) -> return $ Left ()
   case xc of
     Left () -> f (const ()) (con i :: s) (con j) @=? merge (throwError ())
     Right c -> f (const ()) (con i :: s) (con j) @=? mrgSingle (con c)
@@ -138,7 +282,7 @@
   (c -> c -> (c, c)) ->
   Assertion
 sameSafeDivMod' i j f cf = do
-  xc <- evaluate (force $ Right $ cf i j) `catch` \(e :: ArithException) -> return $ Left ()
+  xc <- evaluate (force $ Right $ cf i j) `catch` \(_ :: ArithException) -> return $ Left ()
   case xc of
     Left () -> f (const ()) (con i :: s) (con j) @=? merge (throwError ())
     Right (c1, c2) -> f (const ()) (con i :: s) (con j) @=? mrgSingle (con c1, con c2)
@@ -150,7 +294,7 @@
   ((ArithException -> ()) -> s -> s -> ExceptT () UnionM s) ->
   (c -> c -> c) ->
   (Term c -> Term c -> Term c) ->
-  [TestTree]
+  [Test]
 safeDivisionBoundedOnlyTests f f' cf pf =
   [ testCase "on concrete min divided by minus one" $ do
       sameSafeDiv minBound (-1) f cf
@@ -185,10 +329,9 @@
   (LinkedRep c s, Solvable c s, Eq s, Num c, Show s, Mergeable s, SEq s) =>
   (s -> s -> ExceptT ArithException UnionM s) ->
   ((ArithException -> ()) -> s -> s -> ExceptT () UnionM s) ->
-  (c -> c -> c) ->
   (Term c -> Term c -> Term c) ->
-  [TestTree]
-safeDivisionUnboundedOnlyTests f f' cf pf =
+  [Test]
+safeDivisionUnboundedOnlyTests f f' pf =
   [ testCase "on symbolic" $ do
       f (ssym "a" :: s) (ssym "b")
         @=? ( mrgIf
@@ -213,9 +356,8 @@
   (s -> s -> ExceptT ArithException UnionM s) ->
   ((ArithException -> ()) -> s -> s -> ExceptT () UnionM s) ->
   (c -> c -> c) ->
-  (Term c -> Term c -> Term c) ->
-  [TestTree]
-safeDivisionGeneralTests transform f f' cf pf =
+  [Test]
+safeDivisionGeneralTests transform f f' cf =
   [ testProperty "on concrete prop" $ \(i0 :: c0, j0 :: c0) ->
       ioProperty $ do
         let i = transform i0
@@ -243,10 +385,10 @@
   ((ArithException -> ()) -> s -> s -> ExceptT () UnionM s) ->
   (c -> c -> c) ->
   (Term c -> Term c -> Term c) ->
-  TestTree
+  Test
 safeDivisionBoundedTests name transform f f' cf pf =
   testGroup name $
-    safeDivisionGeneralTests transform f f' cf pf
+    safeDivisionGeneralTests transform f f' cf
       ++ safeDivisionBoundedOnlyTests f f' cf pf
 
 safeDivisionUnboundedTests ::
@@ -258,11 +400,11 @@
   ((ArithException -> ()) -> s -> s -> ExceptT () UnionM s) ->
   (c -> c -> c) ->
   (Term c -> Term c -> Term c) ->
-  TestTree
+  Test
 safeDivisionUnboundedTests name transform f f' cf pf =
   testGroup name $
-    safeDivisionGeneralTests transform f f' cf pf
-      ++ safeDivisionUnboundedOnlyTests f f' cf pf
+    safeDivisionGeneralTests transform f f' cf
+      ++ safeDivisionUnboundedOnlyTests f f' pf
 
 safeDivModBoundedOnlyTests ::
   forall c s.
@@ -279,7 +421,7 @@
   (c -> c -> (c, c)) ->
   (Term c -> Term c -> Term c) ->
   (Term c -> Term c -> Term c) ->
-  [TestTree]
+  [Test]
 safeDivModBoundedOnlyTests f f' cf pf1 pf2 =
   [ testCase "on concrete min divided by minus one" $ do
       sameSafeDivMod minBound (-1) f cf
@@ -329,11 +471,10 @@
     s ->
     ExceptT () UnionM (s, s)
   ) ->
-  (c -> c -> (c, c)) ->
   (Term c -> Term c -> Term c) ->
   (Term c -> Term c -> Term c) ->
-  [TestTree]
-safeDivModUnboundedOnlyTests f f' cf pf1 pf2 =
+  [Test]
+safeDivModUnboundedOnlyTests f f' pf1 pf2 =
   [ testCase "on symbolic" $ do
       f (ssym "a" :: s) (ssym "b")
         @=? ( mrgIf
@@ -373,10 +514,8 @@
     ExceptT () UnionM (s, s)
   ) ->
   (c -> c -> (c, c)) ->
-  (Term c -> Term c -> Term c) ->
-  (Term c -> Term c -> Term c) ->
-  [TestTree]
-safeDivModGeneralTests transform f f' cf pf1 pf2 =
+  [Test]
+safeDivModGeneralTests transform f f' cf =
   [ testProperty "on concrete" $ \(i0 :: c0, j0 :: c0) ->
       ioProperty $ do
         let i = transform i0
@@ -412,10 +551,10 @@
   (c -> c -> (c, c)) ->
   (Term c -> Term c -> Term c) ->
   (Term c -> Term c -> Term c) ->
-  TestTree
+  Test
 safeDivModBoundedTests name transform f f' cf pf1 pf2 =
   testGroup name $
-    safeDivModGeneralTests transform f f' cf pf1 pf2
+    safeDivModGeneralTests transform f f' cf
       ++ safeDivModBoundedOnlyTests f f' cf pf1 pf2
 
 safeDivModUnboundedTests ::
@@ -435,13 +574,13 @@
   (c -> c -> (c, c)) ->
   (Term c -> Term c -> Term c) ->
   (Term c -> Term c -> Term c) ->
-  TestTree
+  Test
 safeDivModUnboundedTests name transform f f' cf pf1 pf2 =
   testGroup name $
-    safeDivModGeneralTests transform f f' cf pf1 pf2
-      ++ safeDivModUnboundedOnlyTests f f' cf pf1 pf2
+    safeDivModGeneralTests transform f f' cf
+      ++ safeDivModUnboundedOnlyTests f f' pf1 pf2
 
-symPrimTests :: TestTree
+symPrimTests :: Test
 symPrimTests =
   testGroup
     "SymPrimTests"
@@ -919,14 +1058,6 @@
           fsymbol :: TypedSymbol (IntN 4) = "f"
           gsymbol :: TypedSymbol (WordN 16) = "g"
           hsymbol :: TypedSymbol (IntN 16) = "h"
-          a :: SymInteger = ssym "a"
-          b :: SymBool = "b"
-          c :: SymInteger = "c"
-          d :: SymBool = "d"
-          e :: SymWordN 4 = "e"
-          f :: SymIntN 4 = "f"
-          g :: SymWordN 16 = "g"
-          h :: SymIntN 16 = "h"
           va :: Integer = 1
           vc :: Integer = 2
           ve :: WordN 4 = 3
diff --git a/test/Grisette/IR/SymPrim/Data/TabularFunTests.hs b/test/Grisette/IR/SymPrim/Data/TabularFunTests.hs
--- a/test/Grisette/IR/SymPrim/Data/TabularFunTests.hs
+++ b/test/Grisette/IR/SymPrim/Data/TabularFunTests.hs
@@ -1,14 +1,17 @@
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeOperators #-}
 
-module Grisette.IR.SymPrim.Data.TabularFunTests where
+module Grisette.IR.SymPrim.Data.TabularFunTests (tabularFunTests) where
 
-import Grisette.Core.Data.Class.Function
+import Grisette.Core.Data.Class.Function (Function ((#)))
 import Grisette.IR.SymPrim.Data.TabularFun
-import Test.Tasty
-import Test.Tasty.HUnit
+  ( type (=->) (TabularFun),
+  )
+import Test.Framework (Test, testGroup)
+import Test.Framework.Providers.HUnit (testCase)
+import Test.HUnit ((@=?))
 
-tabularFunTests :: TestTree
+tabularFunTests :: Test
 tabularFunTests =
   testGroup
     "TabularFunTests"
diff --git a/test/Main.hs b/test/Main.hs
--- a/test/Main.hs
+++ b/test/Main.hs
@@ -1,4 +1,4 @@
-module Main where
+module Main (main) where
 
 {-
 import Grisette.Core.Control.ExceptionTests
@@ -22,39 +22,38 @@
 import Grisette.Lib.Data.TraversableTests
 -}
 
-import Grisette.Backend.SBV.Data.SMT.CEGISTests
+import Grisette.Backend.SBV.Data.SMT.CEGISTests (cegisTests)
 import Grisette.Backend.SBV.Data.SMT.LoweringTests
+  ( loweringTests,
+  )
 import Grisette.Backend.SBV.Data.SMT.TermRewritingTests
-import Grisette.Core.Control.Monad.UnionMTests
+  ( termRewritingTests,
+  )
+import Grisette.Core.Control.Monad.UnionMTests (unionMTests)
 import qualified Grisette.Core.Data.BVTests
-import Grisette.Core.Data.Class.GPrettyTests
+import Grisette.Core.Data.Class.GPrettyTests (gprettyTests)
 import qualified Grisette.IR.SymPrim.Data.Prim.BVTests
-import Grisette.IR.SymPrim.Data.Prim.BitsTests
-import Grisette.IR.SymPrim.Data.Prim.BoolTests
+import Grisette.IR.SymPrim.Data.Prim.BitsTests (bitsTests)
+import Grisette.IR.SymPrim.Data.Prim.BoolTests (boolTests)
 import Grisette.IR.SymPrim.Data.Prim.IntegralTests
-import Grisette.IR.SymPrim.Data.Prim.ModelTests
-import Grisette.IR.SymPrim.Data.Prim.NumTests
+  ( integralTests,
+  )
+import Grisette.IR.SymPrim.Data.Prim.ModelTests (modelTests)
+import Grisette.IR.SymPrim.Data.Prim.NumTests (numTests)
 import qualified Grisette.IR.SymPrim.Data.Prim.TabularFunTests
-import Grisette.IR.SymPrim.Data.SymPrimTests
+import Grisette.IR.SymPrim.Data.SymPrimTests (symPrimTests)
 import qualified Grisette.IR.SymPrim.Data.TabularFunTests
-import Test.Tasty
-import Test.Tasty.Ingredients
-import qualified Test.Tasty.Ingredients.ConsoleReporter as ConsoleReporter
-import qualified Test.Tasty.Runners.Reporter as Reporter
+import Test.Framework (Test, defaultMain, testGroup)
 
 main :: IO ()
-main = defaultMainWithIngredients [composeReporters Reporter.ingredient ConsoleReporter.consoleTestReporter] tests
-
-tests :: TestTree
-tests =
-  testGroup
-    "grisette"
+main =
+  defaultMain
     [ coreTests,
       irTests,
       sbvTests
     ]
 
-coreTests :: TestTree
+coreTests :: Test
 coreTests =
   testGroup
     "core"
@@ -71,7 +70,7 @@
     ]
 
 {-
-coreTests :: TestTree
+coreTests :: Test
 coreTests =
   testGroup
     "grisette-core"
@@ -127,7 +126,7 @@
     ]
 -}
 
-irTests :: TestTree
+irTests :: Test
 irTests =
   testGroup
     "grisette-symir"
@@ -148,7 +147,7 @@
         ]
     ]
 
-sbvTests :: TestTree
+sbvTests :: Test
 sbvTests =
   testGroup
     "Grisette.Backend.SBV.Data.SMT"