diff --git a/grisette.cabal b/grisette.cabal
index 4c528115..877c59dd 100644
--- a/grisette.cabal
+++ b/grisette.cabal
@@ -126,7 +126,7 @@ library
       Paths_grisette
   hs-source-dirs:
       src
-  ghc-options: -Wextra -Werror -Wcompat -Widentities -Wincomplete-record-updates -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields
+  ghc-options: -Wextra -Werror -Wcompat -Widentities -Wincomplete-record-updates -Wmissing-export-lists -Wmissing-home-modules -Wmissing-import-lists -Wpartial-fields
   build-depends:
       QuickCheck >=2.13.2 && <2.15
     , array >=0.5.4 && <0.6
@@ -161,7 +161,7 @@ test-suite doctest
       Paths_grisette
   hs-source-dirs:
       doctest
-  ghc-options: -Wextra -Werror -Wcompat -Widentities -Wincomplete-record-updates -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields
+  ghc-options: -Wextra -Werror -Wcompat -Widentities -Wincomplete-record-updates -Wmissing-export-lists -Wmissing-home-modules -Wmissing-import-lists -Wpartial-fields
   build-depends:
       Glob
     , QuickCheck >=2.13.2 && <2.15
@@ -215,7 +215,7 @@ test-suite spec
       Paths_grisette
   hs-source-dirs:
       test
-  ghc-options: -Wextra -Werror -Wcompat -Widentities -Wincomplete-record-updates -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields
+  ghc-options: -Wextra -Werror -Wcompat -Widentities -Wincomplete-record-updates -Wmissing-export-lists -Wmissing-home-modules -Wmissing-import-lists -Wpartial-fields
   build-depends:
       QuickCheck >=2.13.2 && <2.15
     , array >=0.5.4 && <0.6
diff --git a/package.yaml b/package.yaml
index 35fc7842..9ac4ba8d 100644
--- a/package.yaml
+++ b/package.yaml
@@ -18,44 +18,46 @@ license-file: LICENSE
 github: lsrcz/grisette
 copyright: "2021-2023 Sirui Lu"
 extra-source-files:
-- CHANGELOG.md
-- README.md
+  - CHANGELOG.md
+  - README.md
 tested-with:
-- GHC == 8.10.7
-- GHC == 9.0.2
-- GHC == 9.2.8
-- GHC == 9.4.5
-- GHC == 9.6.2
+  - GHC == 8.10.7
+  - GHC == 9.0.2
+  - GHC == 9.2.8
+  - GHC == 9.4.5
+  - GHC == 9.6.2
 
 dependencies:
-- base >= 4.14 && < 5
-- intern >= 0.9.2 && < 0.10
-- hashable >= 1.2.3 && < 1.5
-- mtl >= 2.2.2 && < 2.4
-- transformers >= 0.5.6 && < 0.7
-- generic-deriving >= 1.14.1 && < 1.15
-- bytestring >= 0.10.12 && < 0.12
-- unordered-containers >= 0.2.11 && < 0.3
-- template-haskell >= 2.16 && < 2.21
-- deepseq >= 1.4.4 && < 1.5
-- hashtables >= 1.2.3.4 && < 1.4
-- loch-th >= 0.2.2 && < 0.3
-- th-compat >= 0.1.2 && < 0.2
-- call-stack >= 0.1 && < 0.5
-- array >= 0.5.4 && < 0.6
-- sbv >= 8.11 && < 10.3
-- parallel >= 3.2.2.0 && < 3.3
-- text >= 1.2.4.1 && < 2.1
-- QuickCheck >= 2.13.2 && < 2.15
-- prettyprinter >= 1.5.0 && < 1.8
+  - base >= 4.14 && < 5
+  - intern >= 0.9.2 && < 0.10
+  - hashable >= 1.2.3 && < 1.5
+  - mtl >= 2.2.2 && < 2.4
+  - transformers >= 0.5.6 && < 0.7
+  - generic-deriving >= 1.14.1 && < 1.15
+  - bytestring >= 0.10.12 && < 0.12
+  - unordered-containers >= 0.2.11 && < 0.3
+  - template-haskell >= 2.16 && < 2.21
+  - deepseq >= 1.4.4 && < 1.5
+  - hashtables >= 1.2.3.4 && < 1.4
+  - loch-th >= 0.2.2 && < 0.3
+  - th-compat >= 0.1.2 && < 0.2
+  - call-stack >= 0.1 && < 0.5
+  - array >= 0.5.4 && < 0.6
+  - sbv >= 8.11 && < 10.3
+  - parallel >= 3.2.2.0 && < 3.3
+  - text >= 1.2.4.1 && < 2.1
+  - QuickCheck >= 2.13.2 && < 2.15
+  - prettyprinter >= 1.5.0 && < 1.8
 
-flags: {
-  fast: {
-    description: "Compile with O2 optimization",
-    manual: False,
-    default: True,
+flags:
+  {
+    fast:
+      {
+        description: "Compile with O2 optimization",
+        manual: False,
+        default: True,
+      },
   }
-}
 
 when:
   - condition: flag(fast)
@@ -72,6 +74,7 @@ ghc-options:
   - -Wincomplete-record-updates
   - -Wmissing-export-lists
   - -Wmissing-home-modules
+  - -Wmissing-import-lists
   - -Wpartial-fields
 
 library:
@@ -94,4 +97,3 @@ tests:
       - grisette
       - doctest >= 0.18.2 && < 0.22
       - Glob
-
diff --git a/src/Grisette.hs b/src/Grisette.hs
index b6ba471a..e1db79dc 100644
--- 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
index 80202de9..e1aedf44 100644
--- 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 @@ where
 
 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
index ad6dcb3f..d07a6fd9 100644
--- a/src/Grisette/Backend/SBV/Data/SMT/Lowering.hs
+++ b/src/Grisette/Backend/SBV/Data/SMT/Lowering.hs
@@ -32,32 +32,123 @@ module Grisette.Backend.SBV.Data.SMT.Lowering
   )
 where
 
-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.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
 
 translateTypeError :: (HasCallStack) => R.TypeRep a -> b
diff --git a/src/Grisette/Backend/SBV/Data/SMT/Solving.hs b/src/Grisette/Backend/SBV/Data/SMT/Solving.hs
index e9eea627..a39aad60 100644
--- a/src/Grisette/Backend/SBV/Data/SMT/Solving.hs
+++ b/src/Grisette/Backend/SBV/Data/SMT/Solving.hs
@@ -37,33 +37,59 @@ module Grisette.Backend.SBV.Data.SMT.Solving
   )
 where
 
-import Control.DeepSeq
-import Control.Exception
+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
+  ( 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
diff --git a/src/Grisette/Backend/SBV/Data/SMT/Solving.hs-boot b/src/Grisette/Backend/SBV/Data/SMT/Solving.hs-boot
index fedbed29..a3c32706 100644
--- a/src/Grisette/Backend/SBV/Data/SMT/Solving.hs-boot
+++ b/src/Grisette/Backend/SBV/Data/SMT/Solving.hs-boot
@@ -13,12 +13,14 @@ module Grisette.Backend.SBV.Data.SMT.Solving
   )
 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
diff --git a/src/Grisette/Backend/SBV/Data/SMT/SymBiMap.hs b/src/Grisette/Backend/SBV/Data/SMT/SymBiMap.hs
index 3e105283..9112709b 100644
--- a/src/Grisette/Backend/SBV/Data/SMT/SymBiMap.hs
+++ b/src/Grisette/Backend/SBV/Data/SMT/SymBiMap.hs
@@ -19,11 +19,15 @@ module Grisette.Backend.SBV.Data.SMT.SymBiMap
   )
 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
index 0d3d309b..74d2bc5c 100644
--- 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 @@ where
 
 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
index 2412cc22..28c6b530 100644
--- a/src/Grisette/Core/BuiltinUnionWrappers.hs
+++ b/src/Grisette/Core/BuiltinUnionWrappers.hs
@@ -30,10 +30,10 @@ module Grisette.Core.BuiltinUnionWrappers
   )
 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
index ae7562ea..78436ea5 100644
--- a/src/Grisette/Core/Control/Exception.hs
+++ b/src/Grisette/Core/Control/Exception.hs
@@ -24,23 +24,33 @@ module Grisette.Core.Control.Exception
   )
 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
index 45cf6aad..f311ec4c 100644
--- 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 @@ module Grisette.Core.Control.Monad.CBMCExcept
   )
 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
index 12e063c1..cdd49f1e 100644
--- a/src/Grisette/Core/Control/Monad/Class/MonadParallelUnion.hs
+++ b/src/Grisette/Core/Control/Monad/Class/MonadParallelUnion.hs
@@ -13,19 +13,22 @@ module Grisette.Core.Control.Monad.Class.MonadParallelUnion
   )
 where
 
-import Control.DeepSeq
-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
+  ( UnionLike,
+    merge,
+  )
 
 -- | Parallel union monad.
 --
diff --git a/src/Grisette/Core/Control/Monad/Union.hs b/src/Grisette/Core/Control/Monad/Union.hs
index 6c10d37c..6ddce73f 100644
--- a/src/Grisette/Core/Control/Monad/Union.hs
+++ b/src/Grisette/Core/Control/Monad/Union.hs
@@ -19,7 +19,7 @@ module Grisette.Core.Control.Monad.Union
   )
 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
index b7cb0581..231f8f51 100644
--- 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,35 +39,90 @@ module Grisette.Core.Control.Monad.UnionM
   )
 where
 
-import Control.DeepSeq
-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.String
-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.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)
 
 -- $setup
diff --git a/src/Grisette/Core/Control/Monad/UnionM.hs-boot b/src/Grisette/Core/Control/Monad/UnionM.hs-boot
index 40a409b6..880a195a 100644
--- a/src/Grisette/Core/Control/Monad/UnionM.hs-boot
+++ b/src/Grisette/Core/Control/Monad/UnionM.hs-boot
@@ -4,9 +4,9 @@
 
 module Grisette.Core.Control.Monad.UnionM (UnionM (..)) where
 
-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
index 6458172d..b61da16d 100644
--- a/src/Grisette/Core/Data/BV.hs
+++ b/src/Grisette/Core/Data/BV.hs
@@ -44,28 +44,93 @@ module Grisette.Core.Data.BV
   )
 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.CallStack (HasCallStack)
+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 (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
diff --git a/src/Grisette/Core/Data/Class/BitVector.hs b/src/Grisette/Core/Data/Class/BitVector.hs
index c0f7380f..b3670473 100644
--- a/src/Grisette/Core/Data/Class/BitVector.hs
+++ b/src/Grisette/Core/Data/Class/BitVector.hs
@@ -28,9 +28,17 @@ module Grisette.Core.Data.Class.BitVector
   )
 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
index ff8f6c8a..d2aa6ee6 100644
--- a/src/Grisette/Core/Data/Class/Bool.hs
+++ b/src/Grisette/Core/Data/Class/Bool.hs
@@ -30,27 +30,59 @@ module Grisette.Core.Data.Class.Bool
   )
 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
index 08418827..c7893392 100644
--- 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 (..), 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
index 5cd91c14..7a281a81 100644
--- a/src/Grisette/Core/Data/Class/CEGISSolver.hs
+++ b/src/Grisette/Core/Data/Class/CEGISSolver.hs
@@ -39,17 +39,25 @@ module Grisette.Core.Data.Class.CEGISSolver
   )
 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.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
index 1ba2d91b..42bc54f8 100644
--- a/src/Grisette/Core/Data/Class/Error.hs
+++ b/src/Grisette/Core/Data/Class/Error.hs
@@ -21,16 +21,17 @@ module Grisette.Core.Data.Class.Error
   )
 where
 
-import Control.Monad.Except
-import Grisette.Core.Control.Monad.Union
-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
index 453191a1..dba45c93 100644
--- a/src/Grisette/Core/Data/Class/Evaluate.hs
+++ b/src/Grisette/Core/Data/Class/Evaluate.hs
@@ -25,23 +25,34 @@ module Grisette.Core.Data.Class.Evaluate
   )
 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.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
index c46ef2c7..262a35c0 100644
--- a/src/Grisette/Core/Data/Class/ExtractSymbolics.hs
+++ b/src/Grisette/Core/Data/Class/ExtractSymbolics.hs
@@ -24,20 +24,33 @@ module Grisette.Core.Data.Class.ExtractSymbolics
   )
 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
index c5e8b817..f3c58224 100644
--- a/src/Grisette/Core/Data/Class/GPretty.hs
+++ b/src/Grisette/Core/Data/Class/GPretty.hs
@@ -18,26 +18,68 @@ module Grisette.Core.Data.Class.GPretty
   )
 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.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
diff --git a/src/Grisette/Core/Data/Class/GenSym.hs b/src/Grisette/Core/Data/Class/GenSym.hs
index f51713ca..09a4604c 100644
--- a/src/Grisette/Core/Data/Class/GenSym.hs
+++ b/src/Grisette/Core/Data/Class/GenSym.hs
@@ -66,38 +66,97 @@ module Grisette.Core.Data.Class.GenSym
   )
 where
 
-import Control.DeepSeq
+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.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.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 {-# SOURCE #-} Grisette.Core.Control.Monad.UnionM
-import Grisette.Core.Data.BV
+  ( 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
diff --git a/src/Grisette/Core/Data/Class/Mergeable.hs b/src/Grisette/Core/Data/Class/Mergeable.hs
index 2f7ba7e0..0ea1635e 100644
--- a/src/Grisette/Core/Data/Class/Mergeable.hs
+++ b/src/Grisette/Core/Data/Class/Mergeable.hs
@@ -51,35 +51,90 @@ module Grisette.Core.Data.Class.Mergeable
 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 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.
diff --git a/src/Grisette/Core/Data/Class/Mergeable.hs-boot b/src/Grisette/Core/Data/Class/Mergeable.hs-boot
index bbf942f9..7a3ba88c 100644
--- a/src/Grisette/Core/Data/Class/Mergeable.hs-boot
+++ b/src/Grisette/Core/Data/Class/Mergeable.hs-boot
@@ -9,8 +9,8 @@ module Grisette.Core.Data.Class.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
index 3550f5d7..d3881f0a 100644
--- a/src/Grisette/Core/Data/Class/ModelOps.hs
+++ b/src/Grisette/Core/Data/Class/ModelOps.hs
@@ -21,7 +21,7 @@ module Grisette.Core.Data.Class.ModelOps
   )
 where
 
-import Data.Kind
+import Data.Kind (Type)
 
 -- $setup
 -- >>> import Grisette.Core
diff --git a/src/Grisette/Core/Data/Class/SOrd.hs b/src/Grisette/Core/Data/Class/SOrd.hs
index 25170369..3c61d470 100644
--- a/src/Grisette/Core/Data/Class/SOrd.hs
+++ b/src/Grisette/Core/Data/Class/SOrd.hs
@@ -26,24 +26,43 @@ module Grisette.Core.Data.Class.SOrd
   )
 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
index 20bf9f13..ee7ff102 100644
--- a/src/Grisette/Core/Data/Class/SafeArith.hs
+++ b/src/Grisette/Core/Data/Class/SafeArith.hs
@@ -30,23 +30,39 @@ module Grisette.Core.Data.Class.SafeArith
   )
 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.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
diff --git a/src/Grisette/Core/Data/Class/SimpleMergeable.hs b/src/Grisette/Core/Data/Class/SimpleMergeable.hs
index 9b251656..befa5f4a 100644
--- a/src/Grisette/Core/Data/Class/SimpleMergeable.hs
+++ b/src/Grisette/Core/Data/Class/SimpleMergeable.hs
@@ -46,26 +46,53 @@ module Grisette.Core.Data.Class.SimpleMergeable
   )
 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
diff --git a/src/Grisette/Core/Data/Class/SimpleMergeable.hs-boot b/src/Grisette/Core/Data/Class/SimpleMergeable.hs-boot
index 0e15a9bf..4e976aa0 100644
--- 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
index 60eeea80..deb2ef6d 100644
--- a/src/Grisette/Core/Data/Class/Solvable.hs
+++ b/src/Grisette/Core/Data/Class/Solvable.hs
@@ -18,11 +18,11 @@ module Grisette.Core.Data.Class.Solvable
   )
 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
index c8a2e345..e9630c0b 100644
--- a/src/Grisette/Core/Data/Class/Solver.hs
+++ b/src/Grisette/Core/Data/Class/Solver.hs
@@ -39,16 +39,20 @@ module Grisette.Core.Data.Class.Solver
   )
 where
 
-import Control.DeepSeq
-import Control.Monad.Except
-import Data.Hashable
-import Generics.Deriving
+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.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
index 7d465adb..2b3ecb0b 100644
--- a/src/Grisette/Core/Data/Class/Substitute.hs
+++ b/src/Grisette/Core/Data/Class/Substitute.hs
@@ -25,21 +25,35 @@ module Grisette.Core.Data.Class.Substitute
   )
 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
+  ( LinkedRep,
+    TypedSymbol,
+  )
 
 -- $setup
 -- >>> import Grisette.Core
diff --git a/src/Grisette/Core/Data/Class/ToCon.hs b/src/Grisette/Core/Data/Class/ToCon.hs
index abcd1eeb..badfd85d 100644
--- a/src/Grisette/Core/Data/Class/ToCon.hs
+++ b/src/Grisette/Core/Data/Class/ToCon.hs
@@ -24,21 +24,31 @@ module Grisette.Core.Data.Class.ToCon
   )
 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
index 4f8e68ac..71f2b313 100644
--- a/src/Grisette/Core/Data/Class/ToSym.hs
+++ b/src/Grisette/Core/Data/Class/ToSym.hs
@@ -25,21 +25,32 @@ module Grisette.Core.Data.Class.ToSym
 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
index 35490243..677c6813 100644
--- 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 @@ module Grisette.Core.Data.FileLocation
   )
 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
index d2a3fac9..b42f7252 100644
--- a/src/Grisette/Core/Data/MemoUtils.hs
+++ b/src/Grisette/Core/Data/MemoUtils.hs
@@ -22,9 +22,9 @@ module Grisette.Core.Data.MemoUtils
 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
index e6824be9..ad7fd0b9 100644
--- 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 @@ module Grisette.Core.Data.Union
   )
 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
index ac5abe16..a2e40d70 100644
--- a/src/Grisette/Core/TH.hs
+++ b/src/Grisette/Core/TH.hs
@@ -17,10 +17,25 @@ module Grisette.Core.TH
   )
 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
index d9ed7048..da35d9af 100644
--- 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,17 +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
+  ( Pred,
+    Q,
+    Specificity,
+    TyVarBndr,
+    Type
+      ( AppT,
+        ArrowT,
+        MulArrowT
+      ),
+  )
+#else
 import Language.Haskell.TH.Syntax
-import Grisette.Core.Data.Class.Mergeable
-import Grisette.Core.Control.Monad.UnionM
+  ( 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
index 39d509f2..5e5c3f16 100644
--- 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 @@ module Grisette.Experimental
 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
index aa7fc572..45c8bef3 100644
--- a/src/Grisette/Experimental/GenSymConstrained.hs
+++ b/src/Grisette/Experimental/GenSymConstrained.hs
@@ -28,16 +28,40 @@ module Grisette.Experimental.GenSymConstrained
   )
 where
 
-import Control.Monad.Except
-import Control.Monad.Trans.Maybe
-import Debug.Trace
+import Control.Monad.Except (ExceptT (ExceptT), MonadError (throwError))
+import Control.Monad.Trans.Maybe (MaybeT (MaybeT))
 import GHC.Generics
+  ( Generic (Rep, from, to),
+    K1 (K1),
+    M1 (M1),
+    U1 (U1),
+    type (:*:) ((:*:)),
+    type (:+:) (L1, R1),
+  )
 import Grisette.Core.Control.Monad.UnionM
-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
@@ -672,7 +696,7 @@ instance
   ) =>
   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
 
diff --git a/src/Grisette/IR/SymPrim.hs b/src/Grisette/IR/SymPrim.hs
index 10a3d4c3..cc6ad615 100644
--- 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 @@ module Grisette.IR.SymPrim
 
     -- ** Symbolic types
     SupportedPrim,
-    SymRep (..),
-    ConRep (..),
+    SymRep (SymType),
+    ConRep (ConType),
     LinkedRep,
     SymBool (..),
     SymInteger (..),
@@ -48,7 +50,38 @@ module Grisette.IR.SymPrim
 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
index 49412ba5..f9be4224 100644
--- a/src/Grisette/IR/SymPrim/Data/IntBitwidth.hs
+++ b/src/Grisette/IR/SymPrim/Data/IntBitwidth.hs
@@ -9,7 +9,7 @@
 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
index f21cadc1..10ea3387 100644
--- a/src/Grisette/IR/SymPrim/Data/Prim/Helpers.hs
+++ b/src/Grisette/IR/SymPrim/Data/Prim/Helpers.hs
@@ -24,10 +24,14 @@ module Grisette.IR.SymPrim.Data.Prim.Helpers
   )
 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
index 8878da9e..6de8095c 100644
--- 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
index a7d9510a..6320ce6e 100644
--- a/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/InternedCtors.hs
+++ b/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/InternedCtors.hs
@@ -65,21 +65,79 @@ module Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors
   )
 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
index cc62b95a..b9290028 100644
--- 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 @@ module Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors
   )
 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
index 9c0d8966..1532d4cd 100644
--- 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
index 8b4f2a32..97eeedbb 100644
--- a/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/Term.hs
+++ b/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/Term.hs
@@ -51,34 +51,115 @@ module Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
   )
 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
@@ -1099,3 +1180,10 @@ instance NFData (a --> b) where
 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
index c0b31d35..decaf2f7 100644
--- a/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/Term.hs-boot
+++ b/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/Term.hs-boot
@@ -28,17 +28,25 @@ module Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
   )
 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
+  ( 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
diff --git a/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/TermSubstitution.hs b/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/TermSubstitution.hs
index d8735d64..bfcad7a4 100644
--- 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
index 0a5e3b43..f8feee69 100644
--- 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
index 992620f9..ef0d883f 100644
--- a/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/TermUtils.hs
+++ b/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/TermUtils.hs
@@ -27,13 +27,74 @@ module Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermUtils
 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
index feaea07c..3f6f1281 100644
--- 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 @@ module Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermUtils
   )
 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
index 050f0526..b1c67080 100644
--- 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 @@ where
 
 import qualified Data.HashMap.Strict as M
 import qualified Data.HashSet as S
-import Data.Hashable
+import Data.Hashable (Hashable)
 import Data.List (sort, sortOn)
-import Data.Proxy
-import GHC.Generics
+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
index 869bd8a7..098f7ff5 100644
--- a/src/Grisette/IR/SymPrim/Data/Prim/Model.hs-boot
+++ b/src/Grisette/IR/SymPrim/Data/Prim/Model.hs-boot
@@ -5,6 +5,8 @@ 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
index 4c45925a..a74c9540 100644
--- 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 @@ module Grisette.IR.SymPrim.Data.Prim.ModelValue
   )
 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
index 7bfffe3a..bc55a036 100644
--- a/src/Grisette/IR/SymPrim/Data/Prim/PartialEval/BV.hs
+++ b/src/Grisette/IR/SymPrim/Data/Prim/PartialEval/BV.hs
@@ -29,13 +29,31 @@ module Grisette.IR.SymPrim.Data.Prim.PartialEval.BV
   )
 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
index 8d87e18a..e18c10af 100644
--- a/src/Grisette/IR/SymPrim/Data/Prim/PartialEval/Bits.hs
+++ b/src/Grisette/IR/SymPrim/Data/Prim/PartialEval/Bits.hs
@@ -26,10 +26,35 @@ module Grisette.IR.SymPrim.Data.Prim.PartialEval.Bits
 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
index b0f24322..85e683b1 100644
--- 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 @@ module Grisette.IR.SymPrim.Data.Prim.PartialEval.Bool
   )
 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
index 4cee2ea9..e2efc815 100644
--- a/src/Grisette/IR/SymPrim/Data/Prim/PartialEval/GeneralFun.hs
+++ b/src/Grisette/IR/SymPrim/Data/Prim/PartialEval/GeneralFun.hs
@@ -11,13 +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.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
index d19b53e8..3543e741 100644
--- a/src/Grisette/IR/SymPrim/Data/Prim/PartialEval/Integral.hs
+++ b/src/Grisette/IR/SymPrim/Data/Prim/PartialEval/Integral.hs
@@ -21,8 +21,21 @@ module Grisette.IR.SymPrim.Data.Prim.PartialEval.Integral
 where
 
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors
+  ( conTerm,
+    divBoundedIntegralTerm,
+    divIntegralTerm,
+    modIntegralTerm,
+    quotBoundedIntegralTerm,
+    quotIntegralTerm,
+    remIntegralTerm,
+  )
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
+  ( SupportedPrim,
+    Term (ConTerm),
+  )
 import Grisette.IR.SymPrim.Data.Prim.PartialEval.Unfold
+  ( 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
index 520e27a7..097199e9 100644
--- 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 @@ module Grisette.IR.SymPrim.Data.Prim.PartialEval.Num
   )
 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
index f204e498..c85b7820 100644
--- a/src/Grisette/IR/SymPrim/Data/Prim/PartialEval/PartialEval.hs
+++ b/src/Grisette/IR/SymPrim/Data/Prim/PartialEval/PartialEval.hs
@@ -31,8 +31,8 @@ module Grisette.IR.SymPrim.Data.Prim.PartialEval.PartialEval
   )
 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
index 8c71d8ec..d3805259 100644
--- a/src/Grisette/IR/SymPrim/Data/Prim/PartialEval/TabularFun.hs
+++ b/src/Grisette/IR/SymPrim/Data/Prim/PartialEval/TabularFun.hs
@@ -16,12 +16,25 @@ module Grisette.IR.SymPrim.Data.Prim.PartialEval.TabularFun
   )
 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
index c4cf4d37..613d7807 100644
--- a/src/Grisette/IR/SymPrim/Data/Prim/PartialEval/Unfold.hs
+++ b/src/Grisette/IR/SymPrim/Data/Prim/PartialEval/Unfold.hs
@@ -16,11 +16,23 @@ module Grisette.IR.SymPrim.Data.Prim.PartialEval.Unfold
   )
 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
index dd72001a..69980f57 100644
--- 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 @@ where
 
 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
index 239d84d8..31a67a23 100644
--- 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,59 +57,227 @@ module Grisette.IR.SymPrim.Data.SymPrim
   )
 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.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
+  ( 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
diff --git a/src/Grisette/IR/SymPrim/Data/SymPrim.hs-boot b/src/Grisette/IR/SymPrim/Data/SymPrim.hs-boot
index a0a302fd..1812de64 100644
--- a/src/Grisette/IR/SymPrim/Data/SymPrim.hs-boot
+++ b/src/Grisette/IR/SymPrim/Data/SymPrim.hs-boot
@@ -31,17 +31,24 @@ module Grisette.IR.SymPrim.Data.SymPrim
   )
 where
 
-import Control.DeepSeq
-import Data.Hashable
-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
index e30db3b2..47fb6f84 100644
--- 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 @@ module Grisette.IR.SymPrim.Data.TabularFun
   )
 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
@@ -46,13 +44,6 @@ data (=->) a b = TabularFun {funcTable :: [(a, b)], defaultFuncValue :: b}
 
 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
   type Ret (a =-> b) = b
diff --git a/src/Grisette/IR/SymPrim/Data/TabularFun.hs-boot b/src/Grisette/IR/SymPrim/Data/TabularFun.hs-boot
index 417aaf26..85adf7ea 100644
--- a/src/Grisette/IR/SymPrim/Data/TabularFun.hs-boot
+++ b/src/Grisette/IR/SymPrim/Data/TabularFun.hs-boot
@@ -5,4 +5,18 @@ module Grisette.IR.SymPrim.Data.TabularFun
   )
 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
index f617571e..2d21b567 100644
--- a/src/Grisette/Internal/Backend/SBV.hs
+++ b/src/Grisette/Internal/Backend/SBV.hs
@@ -14,4 +14,7 @@ module Grisette.Internal.Backend.SBV
 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
index c2f9f8ab..46a1e095 100644
--- 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 @@ module Grisette.Internal.Core
 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
index dd5b6c67..f2e216d3 100644
--- 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,15 +93,103 @@ module Grisette.Internal.IR.SymPrim
 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
+  ( binaryUnfoldOnce,
+    unaryUnfoldOnce,
+  )
diff --git a/src/Grisette/Lib/Base.hs b/src/Grisette/Lib/Base.hs
index 95909e97..ae0186d8 100644
--- a/src/Grisette/Lib/Base.hs
+++ b/src/Grisette/Lib/Base.hs
@@ -49,6 +49,37 @@ module Grisette.Lib.Base
 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
index 0c1b4046..59cf9262 100644
--- a/src/Grisette/Lib/Control/Monad.hs
+++ b/src/Grisette/Lib/Control/Monad.hs
@@ -25,11 +25,17 @@ module Grisette.Lib.Control.Monad
   )
 where
 
-import Control.Monad
-import Grisette.Core.Control.Monad.Union
+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
index 695ca409..5841cd63 100644
--- a/src/Grisette/Lib/Control/Monad.hs-boot
+++ b/src/Grisette/Lib/Control/Monad.hs-boot
@@ -14,9 +14,12 @@ module Grisette.Lib.Control.Monad
   )
 where
 
-import Control.Monad
-import Grisette.Core.Control.Monad.Union
+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
index 3e1634f7..be819ba1 100644
--- a/src/Grisette/Lib/Control/Monad/Except.hs
+++ b/src/Grisette/Lib/Control/Monad/Except.hs
@@ -15,10 +15,10 @@ module Grisette.Lib.Control.Monad.Except
   )
 where
 
-import Control.Monad.Except
-import Grisette.Core.Control.Monad.Union
-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
index d7080a69..df57d69a 100644
--- a/src/Grisette/Lib/Control/Monad/Trans.hs
+++ b/src/Grisette/Lib/Control/Monad/Trans.hs
@@ -16,10 +16,10 @@ module Grisette.Lib.Control.Monad.Trans
   )
 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
index 371d8fa6..6c32effc 100644
--- a/src/Grisette/Lib/Control/Monad/Trans/Cont.hs
+++ b/src/Grisette/Lib/Control/Monad/Trans/Cont.hs
@@ -16,11 +16,14 @@ module Grisette.Lib.Control.Monad.Trans.Cont
   )
 where
 
-import Control.Monad.Cont (ContT (..))
+import Control.Monad.Cont (ContT (runContT))
 import Control.Monad.Trans.Class (lift)
-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,
+  )
+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
index 9b4e9888..27a521fb 100644
--- a/src/Grisette/Lib/Data/Foldable.hs
+++ b/src/Grisette/Lib/Data/Foldable.hs
@@ -22,11 +22,15 @@ module Grisette.Lib.Data.Foldable
   )
 where
 
-import Control.Monad
-import Grisette.Core.Control.Monad.Union
-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
index 7b5c869d..97dd1060 100644
--- a/src/Grisette/Lib/Data/List.hs
+++ b/src/Grisette/Lib/Data/List.hs
@@ -17,16 +17,16 @@ module Grisette.Lib.Data.List
   )
 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.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
index d71a01ab..3aa6b43c 100644
--- a/src/Grisette/Lib/Data/Traversable.hs
+++ b/src/Grisette/Lib/Data/Traversable.hs
@@ -21,9 +21,16 @@ module Grisette.Lib.Data.Traversable
   )
 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
index 8af7d42d..fb4bb001 100644
--- a/src/Grisette/Lib/Mtl.hs
+++ b/src/Grisette/Lib/Mtl.hs
@@ -26,5 +26,12 @@ module Grisette.Lib.Mtl
 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
index 7a914830..dd77a835 100644
--- a/src/Grisette/Qualified/ParallelUnionDo.hs
+++ b/src/Grisette/Qualified/ParallelUnionDo.hs
@@ -8,9 +8,11 @@
 -- Portability :   GHC only
 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
diff --git a/src/Grisette/Utils.hs b/src/Grisette/Utils.hs
index 8f09287d..d4bc3494 100644
--- 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 @@ module Grisette.Utils
 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
index 7e6ecbd4..4b0066ce 100644
--- a/src/Grisette/Utils/Parameterized.hs
+++ b/src/Grisette/Utils/Parameterized.hs
@@ -88,10 +88,20 @@ module Grisette.Utils.Parameterized
   )
 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!
diff --git a/test/Grisette/Backend/SBV/Data/SMT/CEGISTests.hs b/test/Grisette/Backend/SBV/Data/SMT/CEGISTests.hs
index becece41..10480d24 100644
--- a/test/Grisette/Backend/SBV/Data/SMT/CEGISTests.hs
+++ b/test/Grisette/Backend/SBV/Data/SMT/CEGISTests.hs
@@ -7,26 +7,55 @@
 
 module Grisette.Backend.SBV.Data.SMT.CEGISTests (cegisTests) where
 
-import Control.Monad.Except
-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 Data.String (IsString (fromString))
+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.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
+  ( 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
+  ( SymBool,
+    SymIntN,
+    SymInteger,
+    type (-~>),
+    type (=~>),
+  )
+import Test.Tasty (TestTree, testGroup)
 import Test.Tasty.HUnit
+  ( Assertion,
+    HasCallStack,
+    assertFailure,
+    testCase,
+    (@=?),
+  )
 
 testCegis :: (HasCallStack, ExtractSymbolics a, EvaluateSym a, Show a) => GrisetteSMTConfig i -> Bool -> a -> [SymBool] -> Assertion
 testCegis config shouldSuccess a bs = do
diff --git a/test/Grisette/Backend/SBV/Data/SMT/LoweringTests.hs b/test/Grisette/Backend/SBV/Data/SMT/LoweringTests.hs
index 8ff21d5a..3291856e 100644
--- a/test/Grisette/Backend/SBV/Data/SMT/LoweringTests.hs
+++ b/test/Grisette/Backend/SBV/Data/SMT/LoweringTests.hs
@@ -9,22 +9,75 @@
 
 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 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
+  ( SupportedPrim,
+    Term,
+  )
+import Test.Tasty (TestTree, testGroup)
 import Test.Tasty.HUnit
+  ( Assertion,
+    HasCallStack,
+    assertFailure,
+    testCase,
+  )
 
 testUnaryOpLowering ::
   forall a b as n.
diff --git a/test/Grisette/Backend/SBV/Data/SMT/TermRewritingGen.hs b/test/Grisette/Backend/SBV/Data/SMT/TermRewritingGen.hs
index 246511d9..b6427200 100644
--- a/test/Grisette/Backend/SBV/Data/SMT/TermRewritingGen.hs
+++ b/test/Grisette/Backend/SBV/Data/SMT/TermRewritingGen.hs
@@ -42,20 +42,103 @@ module Grisette.Backend.SBV.Data.SMT.TermRewritingGen
   )
 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
+  ( pevalAbsNumTerm,
+    pevalAddNumTerm,
+    pevalLeNumTerm,
+    pevalLtNumTerm,
+    pevalSignumNumTerm,
+    pevalTimesNumTerm,
+    pevalUMinusNumTerm,
+  )
 import Test.Tasty.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
index 996d155d..049ee70b 100644
--- a/test/Grisette/Backend/SBV/Data/SMT/TermRewritingTests.hs
+++ b/test/Grisette/Backend/SBV/Data/SMT/TermRewritingTests.hs
@@ -9,18 +9,56 @@ module Grisette.Backend.SBV.Data.SMT.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.Tasty (TestName, TestTree, testGroup)
+import Test.Tasty.HUnit (Assertion, assertFailure, testCase)
+import Test.Tasty.QuickCheck (ioProperty, mapSize, testProperty)
 
 validateSpec :: (TermRewritingSpec a av, Show a, SupportedPrim av) => GrisetteSMTConfig n -> a -> Assertion
 validateSpec config a = do
diff --git a/test/Grisette/Core/Control/Monad/UnionMTests.hs b/test/Grisette/Core/Control/Monad/UnionMTests.hs
index 0ce78830..f7ab3df2 100644
--- a/test/Grisette/Core/Control/Monad/UnionMTests.hs
+++ b/test/Grisette/Core/Control/Monad/UnionMTests.hs
@@ -2,12 +2,15 @@
 
 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.Tasty (TestTree, testGroup)
+import Test.Tasty.HUnit (testCase, (@=?))
 
 unionMTests :: TestTree
 unionMTests =
diff --git a/test/Grisette/Core/Data/BVTests.hs b/test/Grisette/Core/Data/BVTests.hs
index 9e8790a3..a0d0bf85 100644
--- a/test/Grisette/Core/Data/BVTests.hs
+++ b/test/Grisette/Core/Data/BVTests.hs
@@ -6,20 +6,67 @@
 
 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 Grisette.Core.Data.BV (IntN (IntN), WordN (unWordN))
 import Grisette.Core.Data.Class.BitVector
-import Test.Tasty
+  ( SizedBV
+      ( sizedBVConcat,
+        sizedBVExt,
+        sizedBVSelect,
+        sizedBVSext,
+        sizedBVZext
+      ),
+  )
+import Test.Tasty (TestName, TestTree, testGroup)
 import Test.Tasty.HUnit
-import Test.Tasty.QuickCheck hiding ((.&.))
+  ( Assertion,
+    HasCallStack,
+    assertFailure,
+    testCase,
+    (@=?),
+  )
+import Test.Tasty.QuickCheck
+  ( Arbitrary,
+    Property,
+    ioProperty,
+    testProperty,
+  )
 
 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))
diff --git a/test/Grisette/Core/Data/Class/GPrettyTests.hs b/test/Grisette/Core/Data/Class/GPrettyTests.hs
index 92fca158..f906ee39 100644
--- a/test/Grisette/Core/Data/Class/GPrettyTests.hs
+++ b/test/Grisette/Core/Data/Class/GPrettyTests.hs
@@ -7,26 +7,45 @@
 
 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.Tasty (TestTree, testGroup)
+import Test.Tasty.HUnit (testCase, (@=?))
+import Test.Tasty.QuickCheck
+  ( Arbitrary (arbitrary),
+    Gen,
+    forAll,
+    oneof,
+    testProperty,
+  )
 
 #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
diff --git a/test/Grisette/IR/SymPrim/Data/Prim/BVTests.hs b/test/Grisette/IR/SymPrim/Data/Prim/BVTests.hs
index c90737de..6e331df2 100644
--- a/test/Grisette/IR/SymPrim/Data/Prim/BVTests.hs
+++ b/test/Grisette/IR/SymPrim/Data/Prim/BVTests.hs
@@ -5,13 +5,23 @@
 
 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.Tasty (TestTree, testGroup)
+import Test.Tasty.HUnit (testCase, (@=?))
 
 bvTests :: TestTree
 bvTests =
diff --git a/test/Grisette/IR/SymPrim/Data/Prim/BitsTests.hs b/test/Grisette/IR/SymPrim/Data/Prim/BitsTests.hs
index 8bb87df9..63b9a048 100644
--- a/test/Grisette/IR/SymPrim/Data/Prim/BitsTests.hs
+++ b/test/Grisette/IR/SymPrim/Data/Prim/BitsTests.hs
@@ -3,12 +3,28 @@
 
 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.Tasty (TestTree, testGroup)
+import Test.Tasty.HUnit (testCase, (@=?))
 
 bitsTests :: TestTree
 bitsTests =
diff --git a/test/Grisette/IR/SymPrim/Data/Prim/BoolTests.hs b/test/Grisette/IR/SymPrim/Data/Prim/BoolTests.hs
index bece5ce9..f23ce217 100644
--- a/test/Grisette/IR/SymPrim/Data/Prim/BoolTests.hs
+++ b/test/Grisette/IR/SymPrim/Data/Prim/BoolTests.hs
@@ -4,13 +4,31 @@
 
 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.Tasty (TestTree, testGroup)
+import Test.Tasty.HUnit (testCase, (@=?))
 
 boolTests :: TestTree
 boolTests =
diff --git a/test/Grisette/IR/SymPrim/Data/Prim/IntegralTests.hs b/test/Grisette/IR/SymPrim/Data/Prim/IntegralTests.hs
index f8c7ac9f..cb15ab20 100644
--- a/test/Grisette/IR/SymPrim/Data/Prim/IntegralTests.hs
+++ b/test/Grisette/IR/SymPrim/Data/Prim/IntegralTests.hs
@@ -5,16 +5,39 @@
 
 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
+  ( pevalDivBoundedIntegralTerm,
+    pevalDivIntegralTerm,
+    pevalModIntegralTerm,
+    pevalQuotBoundedIntegralTerm,
+    pevalQuotIntegralTerm,
+    pevalRemIntegralTerm,
+  )
+import Test.Tasty (TestName, TestTree, testGroup)
+import Test.Tasty.HUnit (testCase, (@=?))
 import Test.Tasty.QuickCheck
+  ( Arbitrary,
+    ioProperty,
+    testProperty,
+  )
 
 newtype AEWrapper = AEWrapper ArithException deriving (Eq)
 
diff --git a/test/Grisette/IR/SymPrim/Data/Prim/ModelTests.hs b/test/Grisette/IR/SymPrim/Data/Prim/ModelTests.hs
index 63d27857..ab20b879 100644
--- a/test/Grisette/IR/SymPrim/Data/Prim/ModelTests.hs
+++ b/test/Grisette/IR/SymPrim/Data/Prim/ModelTests.hs
@@ -3,18 +3,48 @@
 
 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
+  ( pevalAddNumTerm,
+    pevalUMinusNumTerm,
+  )
+import Test.Tasty (TestTree, testGroup)
+import Test.Tasty.HUnit (testCase, (@=?))
 
 modelTests :: TestTree
 modelTests =
diff --git a/test/Grisette/IR/SymPrim/Data/Prim/NumTests.hs b/test/Grisette/IR/SymPrim/Data/Prim/NumTests.hs
index 5e37c839..93f90740 100644
--- a/test/Grisette/IR/SymPrim/Data/Prim/NumTests.hs
+++ b/test/Grisette/IR/SymPrim/Data/Prim/NumTests.hs
@@ -3,13 +3,36 @@
 
 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.Tasty (TestTree, testGroup)
+import Test.Tasty.HUnit (testCase, (@=?))
 
 numTests :: TestTree
 numTests =
diff --git a/test/Grisette/IR/SymPrim/Data/Prim/TabularFunTests.hs b/test/Grisette/IR/SymPrim/Data/Prim/TabularFunTests.hs
index bcf80e42..ba9202e9 100644
--- a/test/Grisette/IR/SymPrim/Data/Prim/TabularFunTests.hs
+++ b/test/Grisette/IR/SymPrim/Data/Prim/TabularFunTests.hs
@@ -4,12 +4,23 @@
 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.Tasty (TestTree, testGroup)
+import Test.Tasty.HUnit (testCase, (@=?))
 
 tabularFunTests :: TestTree
 tabularFunTests =
diff --git a/test/Grisette/IR/SymPrim/Data/SymPrimTests.hs b/test/Grisette/IR/SymPrim/Data/SymPrimTests.hs
index 4738dd25..c6ac487a 100644
--- a/test/Grisette/IR/SymPrim/Data/SymPrimTests.hs
+++ b/test/Grisette/IR/SymPrim/Data/SymPrimTests.hs
@@ -2,6 +2,7 @@
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE NegativeLiterals #-}
 {-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeOperators #-}
@@ -9,46 +10,197 @@
 
 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
+  ( ModelSymPair ((:=)),
+    SymBool (SymBool),
+    SymIntN (SymIntN),
+    SymInteger (SymInteger),
+    SymWordN (SymWordN),
+    symSize,
+    symsSize,
+    (-->),
+    type (-~>),
+    type (=~>),
+  )
+import Grisette.IR.SymPrim.Data.TabularFun (type (=->))
+import Test.Tasty (TestName, TestTree, testGroup)
 import Test.Tasty.HUnit
-import Test.Tasty.QuickCheck hiding ((.&.))
+  ( Assertion,
+    assertFailure,
+    testCase,
+    (@=?),
+  )
+import Test.Tasty.QuickCheck
+  ( Arbitrary,
+    ioProperty,
+    testProperty,
+  )
 
 newtype AEWrapper = AEWrapper ArithException deriving (Eq)
 
diff --git a/test/Grisette/IR/SymPrim/Data/TabularFunTests.hs b/test/Grisette/IR/SymPrim/Data/TabularFunTests.hs
index c71cf299..c28510e1 100644
--- a/test/Grisette/IR/SymPrim/Data/TabularFunTests.hs
+++ b/test/Grisette/IR/SymPrim/Data/TabularFunTests.hs
@@ -3,10 +3,12 @@
 
 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.Tasty (TestTree, testGroup)
+import Test.Tasty.HUnit (testCase, (@=?))
 
 tabularFunTests :: TestTree
 tabularFunTests =
diff --git a/test/Main.hs b/test/Main.hs
index 875c1f7c..fa12b054 100644
--- a/test/Main.hs
+++ b/test/Main.hs
@@ -22,28 +22,42 @@ import Grisette.Lib.Data.FoldableTests
 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
+  ( TestTree,
+    defaultMainWithIngredients,
+    testGroup,
+  )
+import Test.Tasty.Ingredients (composeReporters)
 import qualified Test.Tasty.Ingredients.ConsoleReporter as ConsoleReporter
 import qualified Test.Tasty.Runners.Reporter as Reporter
 
 main :: IO ()
-main = defaultMainWithIngredients [composeReporters Reporter.ingredient ConsoleReporter.consoleTestReporter] tests
+main =
+  defaultMainWithIngredients
+    [ composeReporters Reporter.ingredient ConsoleReporter.consoleTestReporter
+    ]
+    tests
 
 tests :: TestTree
 tests =