diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,27 +1,57 @@
-# Changes
+# Changelog
 
-## Version 0.2.0.0
+All notable changes to this project will be documented in this file.
 
-### Feature
-- Redesigned symbolic value interface.
-  - `Sym Bool`/`Sym Integer`, etc., are no longer available and are replaced with `SymBool` and `SymInteger`. ([#41](https://github.com/lsrcz/grisette/pull/41))
-  - New symbolic bit vector interface. Added unsized bit vector. ([#41](https://github.com/lsrcz/grisette/pull/41))
+The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),
+and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html).
+
+## [0.3.0.0] -- 2023-07-07
+
+### Added
+- Added the conversion between signed and unsigned bit vectors. ([#69](https://github.com/lsrcz/grisette/pull/69))
+- Added the generation of `SomeSymIntN` and `SomeSymWordN` from a single `Int` for bit width. ([#73](https://github.com/lsrcz/grisette/pull/73))
+- Added the `FiniteBits` instance for `SomeSymIntN` and `SomeSymWordN`. ([#83](https://github.com/lsrcz/grisette/pull/83))
+- Added more flexible instances for symbolic generation for `Either`, `Maybe` and list types. ([#84](https://github.com/lsrcz/grisette/pull/84))
+- Added an experimental `GenSymConstrained` type class. ([#89](https://github.com/lsrcz/grisette/pull/89))
+
+### Changed
+- Changed the operations for `SomeIntN` and `SomeWordN` to accepting dynamic runtime integers rather than compile-time integers. ([#71](https://github.com/lsrcz/grisette/pull/71))
+- Comparing the equality of `SomeIntN`/`SomeWordN`/`SomeSymIntN`/`SomeSymWordN` with different bit widths returns false rather than crash now. ([#74](https://github.com/lsrcz/grisette/pull/74))
+
+### Fixed
+- Fixed the compatibility issue with sbv 10+. ([#66](https://github.com/lsrcz/grisette/pull/66))
+- Fixed build error with newer GHC. ([#70](https://github.com/lsrcz/grisette/pull/70))
+- Fixed the merging for `SomeSymIntN` and `SomeSymWordN`. ([#72](https://github.com/lsrcz/grisette/pull/72))
+
+## [0.2.0.0] - 2023-04-13
+
+### Added
 - Add term size count API. ([#48](https://github.com/lsrcz/grisette/pull/48), [#53](https://github.com/lsrcz/grisette/pull/53))
 - Add timeout to solver interface. ([#49](https://github.com/lsrcz/grisette/pull/49), [#50](https://github.com/lsrcz/grisette/pull/50))
 - Add parallel do-notation for parallel symbolic compilation. ([#51](https://github.com/lsrcz/grisette/pull/51))
-- New safe operator interfaces. ([#56](https://github.com/lsrcz/grisette/pull/56))
+- Added some missing instances for symbolic values and bit vectors. ([#46](https://github.com/lsrcz/grisette/pull/46), [#61](https://github.com/lsrcz/grisette/pull/61))
+- Add missing instances for `MonadFresh` and `FreshT`. ([#59](https://github.com/lsrcz/grisette/pull/59))
 
+### Changed
+- New safe operator interfaces. ([#56](https://github.com/lsrcz/grisette/pull/56))
+- Redesigned symbolic value interface.
+  - `Sym Bool`/`Sym Integer`, etc., are no longer available and are replaced with `SymBool` and `SymInteger`. ([#41](https://github.com/lsrcz/grisette/pull/41))
+  - New symbolic bit vector interface. Added unsized bit vector. ([#41](https://github.com/lsrcz/grisette/pull/41))
 
-### Bugfix
+### Removed
 - Dropped merging cache for `UnionM`. This fixed some segmentation fault errors. ([#43](https://github.com/lsrcz/grisette/pull/43))
-- Added some missing instances for symbolic values and bit vectors. ([#46](https://github.com/lsrcz/grisette/pull/46), [#61](https://github.com/lsrcz/grisette/pull/61))
+
+### Fixed
 - Fix CEGIS when no symbolic input is present. ([#52](https://github.com/lsrcz/grisette/pull/52))
 - Fix overlapping `ToSym` and `ToCon` instances. ([#54](https://github.com/lsrcz/grisette/pull/54))
 - Fix uninterpreted function lowering. ([#57](https://github.com/lsrcz/grisette/pull/57), [#58](https://github.com/lsrcz/grisette/pull/58))
-- Add missing instances for `MonadFresh` and `FreshT`. ([#59](https://github.com/lsrcz/grisette/pull/59))
 - Fix CEGIS crash when subsequent solver calls introduces new symbolic constant. ([#60](https://github.com/lsrcz/grisette/pull/60))
 
+## [0.1.0.0] - 2023-01-20
 
+### Added
+- Initial release for Grisette.
 
-## Version 0.1.0.0
-Initial release.
+[0.3.0.0]: https://github.com/lsrcz/grisette/compare/v0.2.0.0...v0.3.0.0
+[0.2.0.0]: https://github.com/lsrcz/grisette/compare/v0.1.0.0...v0.2.0.0
+[0.1.0.0]: https://github.com/lsrcz/grisette/tree/v0.1.0.0
diff --git a/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -1,4 +1,4 @@
-Copyright (c) 2021-2022, Sirui Lu (siruilu@cs.washington.edu)
+Copyright (c) 2021-2023, Sirui Lu (siruilu@cs.washington.edu)
 
 All rights reserved.
 
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -35,21 +35,47 @@
 ### Install Grisette
 
 Grisette is available via
-[Hackage](https://hackage.haskell.org/package/grisette). You can install it with
-`cabal`:
+[Hackage](https://hackage.haskell.org/package/grisette). You can add it to your
+project with `cabal`, and we also provided a stack template for quickly starting a
+new project with Grisette.
 
-```bash
-$ cabal install grisette
-```
+#### Manually writing cabal file
 
-However, Grisette is a library and is usually used as a dependency of other
+Grisette is a library and is usually used as a dependency of other
 packages. You can add it to your project's `.cabal` file:
 
 ```cabal
 library
   ...
-  build-depends: grisette >= 0.1 < 0.2
+  build-depends: grisette >= 0.2 < 0.3
 ```
+
+#### Quick start template with `stack new`
+
+You can quickly start an stack-based Grisette project with `stack new`:
+
+```bash
+$ stack new <projectname> github:lsrcz/grisette
+```
+
+You can specify the resolver version with the parameters:
+
+```bash
+$ stack new a-new-project github:lsrcz/grisette -p "resolver:lts-19.33"
+```
+
+For more details, please see the
+[template file](https://github.com/lsrcz/stack-templates/blob/main/grisette.hsfiles) and the
+[documentation for stack templates](https://docs.haskellstack.org/en/stable/templates_command/).
+
+You can test your installation by running the following command:
+
+```bash
+$ stack run app
+```
+
+The command assumes a working [Z3](https://github.com/Z3Prover/z3) available
+through `PATH`. You can install it with the instructions below.
 
 ### Install SMT Solvers
 
diff --git a/grisette.cabal b/grisette.cabal
--- a/grisette.cabal
+++ b/grisette.cabal
@@ -1,11 +1,11 @@
 cabal-version: 1.12
 
--- This file has been generated from package.yaml by hpack version 0.35.1.
+-- This file has been generated from package.yaml by hpack version 0.35.2.
 --
 -- see: https://github.com/sol/hpack
 
 name:           grisette
-version:        0.2.0.0
+version:        0.3.0.0
 synopsis:       Symbolic evaluation as a library
 description:    Grisette is a reusable symbolic evaluation library for Haskell. By
                 translating programs into constraints, Grisette can help the development of
@@ -24,6 +24,12 @@
 license:        BSD3
 license-file:   LICENSE
 build-type:     Simple
+tested-with:
+    GHC == 8.10.7
+  , GHC == 9.0.2
+  , GHC == 9.2.8
+  , GHC == 9.4.5
+  , GHC == 9.6.2
 extra-source-files:
     CHANGELOG.md
     README.md
@@ -75,6 +81,8 @@
       Grisette.Core.Data.Union
       Grisette.Core.TH
       Grisette.Core.THCompat
+      Grisette.Experimental
+      Grisette.Experimental.GenSymConstrained
       Grisette.Internal.Backend.SBV
       Grisette.Internal.Core
       Grisette.Internal.IR.SymPrim
@@ -119,7 +127,7 @@
       src
   build-depends:
       array >=0.5.4 && <0.6
-    , base >4.14 && <5
+    , base >=4.14 && <5
     , bytestring >=0.10.12 && <0.12
     , call-stack >=0.1 && <0.5
     , deepseq >=1.4.4 && <1.5
@@ -128,13 +136,12 @@
     , hashtables >=1.2.3.4 && <1.4
     , intern >=0.9.2 && <0.10
     , loch-th >=0.2.2 && <0.3
-    , mtl >=2.2.2 && <2.3
-    , once >=0.2 && <0.5
-    , parallel
-    , sbv >=8.11 && <9.1
-    , template-haskell >=2.16 && <2.20
+    , mtl >=2.2.2 && <2.4
+    , parallel >=3.2.2.0 && <3.3
+    , sbv >=8.11 && <10.3
+    , template-haskell >=2.16 && <2.21
     , th-compat >=0.1.2 && <0.2
-    , transformers >=0.5.6 && <0.6
+    , transformers >=0.5.6 && <0.7
     , unordered-containers >=0.2.11 && <0.3
     , vector >=0.12.1 && <0.14
   default-language: Haskell2010
@@ -153,24 +160,23 @@
   build-depends:
       Glob
     , array >=0.5.4 && <0.6
-    , base >4.14 && <5
+    , base >=4.14 && <5
     , bytestring >=0.10.12 && <0.12
     , call-stack >=0.1 && <0.5
     , deepseq >=1.4.4 && <1.5
-    , doctest >=0.18.2 && <0.21
+    , doctest >=0.18.2 && <0.22
     , generic-deriving >=1.14.1 && <1.15
     , grisette
     , hashable >=1.2.3 && <1.5
     , hashtables >=1.2.3.4 && <1.4
     , intern >=0.9.2 && <0.10
     , loch-th >=0.2.2 && <0.3
-    , mtl >=2.2.2 && <2.3
-    , once >=0.2 && <0.5
-    , parallel
-    , sbv >=8.11 && <9.1
-    , template-haskell >=2.16 && <2.20
+    , mtl >=2.2.2 && <2.4
+    , parallel >=3.2.2.0 && <3.3
+    , sbv >=8.11 && <10.3
+    , template-haskell >=2.16 && <2.21
     , th-compat >=0.1.2 && <0.2
-    , transformers >=0.5.6 && <0.6
+    , transformers >=0.5.6 && <0.7
     , unordered-containers >=0.2.11 && <0.3
     , vector >=0.12.1 && <0.14
   default-language: Haskell2010
@@ -203,7 +209,7 @@
       test
   build-depends:
       array >=0.5.4 && <0.6
-    , base >4.14 && <5
+    , base >=4.14 && <5
     , bytestring >=0.10.12 && <0.12
     , call-stack >=0.1 && <0.5
     , deepseq >=1.4.4 && <1.5
@@ -213,17 +219,16 @@
     , hashtables >=1.2.3.4 && <1.4
     , intern >=0.9.2 && <0.10
     , loch-th >=0.2.2 && <0.3
-    , mtl >=2.2.2 && <2.3
-    , once >=0.2 && <0.5
-    , parallel
-    , sbv >=8.11 && <9.1
+    , mtl >=2.2.2 && <2.4
+    , parallel >=3.2.2.0 && <3.3
+    , sbv >=8.11 && <10.3
     , tasty >=1.1.0.3 && <1.5
     , tasty-hunit ==0.10.*
     , tasty-quickcheck >=0.10.1 && <0.11
     , tasty-test-reporter >=0.1.1.2 && <0.2
-    , template-haskell >=2.16 && <2.20
+    , template-haskell >=2.16 && <2.21
     , th-compat >=0.1.2 && <0.2
-    , transformers >=0.5.6 && <0.6
+    , transformers >=0.5.6 && <0.7
     , unordered-containers >=0.2.11 && <0.3
     , vector >=0.12.1 && <0.14
   default-language: Haskell2010
diff --git a/src/Grisette/Backend/SBV/Data/SMT/Lowering.hs b/src/Grisette/Backend/SBV/Data/SMT/Lowering.hs
--- a/src/Grisette/Backend/SBV/Data/SMT/Lowering.hs
+++ b/src/Grisette/Backend/SBV/Data/SMT/Lowering.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE CPP #-}
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE FlexibleContexts #-}
@@ -79,12 +80,12 @@
   State SymBiMap ()
 addResult tm sbvtm = modify $ addBiMapIntermediate (SomeTerm tm) (toDyn sbvtm)
 
-translateTypeError :: HasCallStack => R.TypeRep a -> b
+translateTypeError :: (HasCallStack) => R.TypeRep a -> b
 translateTypeError ta =
   error $
     "Don't know how to translate the type " ++ show ta ++ " to SMT"
 
-translateUnaryError :: HasCallStack => String -> R.TypeRep a -> R.TypeRep b -> c
+translateUnaryError :: (HasCallStack) => String -> R.TypeRep a -> R.TypeRep b -> c
 translateUnaryError op ta tb =
   error $
     "Don't know how to translate the op "
@@ -95,7 +96,7 @@
       ++ show tb
       ++ " to SMT"
 
-translateBinaryError :: HasCallStack => String -> R.TypeRep a -> R.TypeRep b -> R.TypeRep c -> d
+translateBinaryError :: (HasCallStack) => String -> R.TypeRep a -> R.TypeRep b -> R.TypeRep c -> d
 translateBinaryError op ta tb tc =
   error $
     "Don't know how to translate the op "
@@ -108,7 +109,7 @@
       ++ show tc
       ++ " to SMT"
 
-translateTernaryError :: HasCallStack => String -> R.TypeRep a -> R.TypeRep b -> R.TypeRep c -> R.TypeRep d -> e
+translateTernaryError :: (HasCallStack) => String -> R.TypeRep a -> R.TypeRep b -> R.TypeRep c -> R.TypeRep d -> e
 translateTernaryError op ta tb tc td =
   error $
     "Don't know how to translate the op "
@@ -545,8 +546,8 @@
     _ -> Nothing
 lowerSinglePrimUFun _ _ _ = error "Should not call this function"
 
-class Monad m => SBVFreshMonad m where
-  sbvFresh :: SBV.SymVal a => String -> m (SBV.SBV a)
+class (Monad m) => SBVFreshMonad m where
+  sbvFresh :: (SBV.SymVal a) => String -> m (SBV.SBV a)
 
 instance SBVFreshMonad SBV.Symbolic where
   sbvFresh = SBV.free
@@ -710,6 +711,22 @@
   case (config, R.typeRep @a) of
     ResolvedBitsType -> lowerUnaryTerm config t arg (`rotate` n) m
     _ -> translateBinaryError "rotate" (R.typeRep @a) (R.typeRep @Int) (R.typeRep @a)
+lowerSinglePrimImpl config t@(BVToSignedTerm _ (bv :: Term x)) m =
+  case (R.typeRep @a, R.typeRep @x) of
+    (SignedBVType (_ :: Proxy na), UnsignedBVType (_ :: Proxy nx)) ->
+      case R.eqTypeRep (R.typeRep @na) (R.typeRep @nx) of
+        Just R.HRefl ->
+          lowerUnaryTerm config t bv SBV.sFromIntegral m
+        _ -> translateUnaryError "bvu2s" (R.typeRep @x) (R.typeRep @a)
+    _ -> translateUnaryError "bvu2s" (R.typeRep @x) (R.typeRep @a)
+lowerSinglePrimImpl config t@(BVToUnsignedTerm _ (bv :: Term x)) m =
+  case (R.typeRep @a, R.typeRep @x) of
+    (UnsignedBVType (_ :: Proxy na), SignedBVType (_ :: Proxy nx)) ->
+      case R.eqTypeRep (R.typeRep @na) (R.typeRep @nx) of
+        Just R.HRefl ->
+          lowerUnaryTerm config t bv SBV.sFromIntegral m
+        _ -> translateUnaryError "bvs2u" (R.typeRep @x) (R.typeRep @a)
+    _ -> translateUnaryError "bvs2u" (R.typeRep @x) (R.typeRep @a)
 lowerSinglePrimImpl config t@(BVConcatTerm _ (bv1 :: Term x) (bv2 :: Term y)) m =
   case (R.typeRep @a, R.typeRep @x, R.typeRep @y) of
     (UnsignedBVType (_ :: Proxy na), UnsignedBVType (_ :: Proxy nx), UnsignedBVType (_ :: Proxy ny)) ->
@@ -827,8 +844,27 @@
 bvIsNonZeroFromGEq1 r1 = case unsafeAxiom :: w :~: 1 of
   Refl -> r1
 
+#if MIN_VERSION_sbv(10,0,0)
+preprocessUIFuncs ::
+  [(String, (SBVI.SBVType, Either String ([([SBVI.CV], SBVI.CV)], SBVI.CV)))] ->
+  Maybe [(String, (SBVI.SBVType, ([([SBVI.CV], SBVI.CV)], SBVI.CV)))]
+preprocessUIFuncs =
+  traverse
+    (\case
+      (a, (b, Right c)) -> Just (a, (b, c))
+      _ -> Nothing)
+#else
+preprocessUIFuncs ::
+  [(String, (SBVI.SBVType, ([([SBVI.CV], SBVI.CV)], SBVI.CV)))] ->
+  Maybe [(String, (SBVI.SBVType, ([([SBVI.CV], SBVI.CV)], SBVI.CV)))]
+preprocessUIFuncs = Just
+#endif
+
 parseModel :: forall integerBitWidth. GrisetteSMTConfig integerBitWidth -> SBVI.SMTModel -> SymBiMap -> PM.Model
-parseModel _ (SBVI.SMTModel _ _ assoc uifuncs) mp = foldr gouifuncs (foldr goassoc emptyModel assoc) uifuncs
+parseModel _ (SBVI.SMTModel _ _ assoc orguifuncs) mp =
+  case preprocessUIFuncs orguifuncs of
+    Just uifuncs -> foldr gouifuncs (foldr goassoc emptyModel assoc) uifuncs
+    _ -> error "SBV Failed to parse model"
   where
     goassoc :: (String, SBVI.CV) -> PM.Model -> PM.Model
     goassoc (name, cv) m = case findStringToSymbol name mp of
@@ -939,7 +975,7 @@
     resolveFirst :: R.TypeRep a -> [([SBVI.CV], SBVI.CV)] -> [(a, [([SBVI.CV], SBVI.CV)])]
     resolveFirst tf = fmap (\case (x : xs, v) -> (resolveSingle tf x, [(xs, v)]); _ -> error "impossible")
 
-    partitionWithOrd :: forall a. Ord a => [(a, [([SBVI.CV], SBVI.CV)])] -> [(a, [([SBVI.CV], SBVI.CV)])]
+    partitionWithOrd :: forall a. (Ord a) => [(a, [([SBVI.CV], SBVI.CV)])] -> [(a, [([SBVI.CV], SBVI.CV)])]
     partitionWithOrd v = go sorted
       where
         sorted = sortWith fst v
@@ -1485,7 +1521,7 @@
   forall integerBitWidth.
   () =>
   forall s.
-  ConfigConstraint integerBitWidth s =>
+  (ConfigConstraint integerBitWidth s) =>
   SBV.SMTConfig ->
   GrisetteSMTConfig integerBitWidth
 pattern ResolvedConfig c <- (resolveConfigView -> DictConfig c)
@@ -1522,7 +1558,7 @@
 pattern ResolvedMergeableType ::
   forall integerBitWidth s.
   (SupportedPrim s) =>
-  MergeableTypeConstraint integerBitWidth s =>
+  (MergeableTypeConstraint integerBitWidth s) =>
   (GrisetteSMTConfig integerBitWidth, R.TypeRep s)
 pattern ResolvedMergeableType <- (resolveMergeableTypeView -> Just DictMergeableType)
 
@@ -1561,7 +1597,7 @@
   forall integerBitWidth s.
   (SupportedPrim s) =>
   forall s'.
-  SimpleTypeConstraint integerBitWidth s s' =>
+  (SimpleTypeConstraint integerBitWidth s s') =>
   (GrisetteSMTConfig integerBitWidth, R.TypeRep s)
 pattern ResolvedSimpleType <- (resolveSimpleTypeView -> Just DictSimpleType)
 
@@ -1594,7 +1630,7 @@
   forall integerBitWidth s.
   (SupportedPrim s) =>
   forall s'.
-  DeepTypeConstraint integerBitWidth s s' =>
+  (DeepTypeConstraint integerBitWidth s s') =>
   (GrisetteSMTConfig integerBitWidth, R.TypeRep s)
 pattern ResolvedDeepType <- (resolveDeepTypeView -> Just DictDeepType)
 
@@ -1623,7 +1659,7 @@
   forall integerBitWidth s.
   (SupportedPrim s) =>
   forall s'.
-  NumTypeConstraint integerBitWidth s s' =>
+  (NumTypeConstraint integerBitWidth s s') =>
   (GrisetteSMTConfig integerBitWidth, R.TypeRep s)
 pattern ResolvedNumType <- (resolveNumTypeView -> Just DictNumType)
 
@@ -1651,7 +1687,7 @@
   forall integerBitWidth s.
   (SupportedPrim s) =>
   forall s'.
-  SDivisibleTypeConstraint integerBitWidth s s' =>
+  (SDivisibleTypeConstraint integerBitWidth s s') =>
   (GrisetteSMTConfig integerBitWidth, R.TypeRep s)
 pattern ResolvedSDivisibleType <- (resolveSDivisibleTypeView -> Just DictSDivisibleType)
 
@@ -1680,7 +1716,7 @@
   forall integerBitWidth s.
   (SupportedPrim s) =>
   forall s'.
-  NumOrdTypeConstraint integerBitWidth s s' =>
+  (NumOrdTypeConstraint integerBitWidth s s') =>
   (GrisetteSMTConfig integerBitWidth, R.TypeRep s)
 pattern ResolvedNumOrdType <- (resolveNumOrdTypeView -> Just DictNumOrdType)
 
@@ -1708,6 +1744,6 @@
   forall integerBitWidth s.
   (SupportedPrim s) =>
   forall s'.
-  BitsTypeConstraint integerBitWidth s s' =>
+  (BitsTypeConstraint integerBitWidth s s') =>
   (GrisetteSMTConfig integerBitWidth, R.TypeRep s)
 pattern ResolvedBitsType <- (resolveBitsTypeView -> Just DictBitsType)
diff --git a/src/Grisette/Backend/SBV/Data/SMT/Solving.hs b/src/Grisette/Backend/SBV/Data/SMT/Solving.hs
--- a/src/Grisette/Backend/SBV/Data/SMT/Solving.hs
+++ b/src/Grisette/Backend/SBV/Data/SMT/Solving.hs
@@ -40,6 +40,7 @@
 import Control.DeepSeq
 import Control.Exception
 import Control.Monad.Except
+import Control.Monad.IO.Class
 import qualified Data.HashSet as S
 import Data.Hashable
 import Data.Kind
diff --git a/src/Grisette/Backend/SBV/Data/SMT/SymBiMap.hs b/src/Grisette/Backend/SBV/Data/SMT/SymBiMap.hs
--- a/src/Grisette/Backend/SBV/Data/SMT/SymBiMap.hs
+++ b/src/Grisette/Backend/SBV/Data/SMT/SymBiMap.hs
@@ -37,14 +37,14 @@
 sizeBiMap :: SymBiMap -> Int
 sizeBiMap = M.size . biMapToSBV
 
-addBiMap :: HasCallStack => SomeTerm -> Dynamic -> String -> SomeTypedSymbol -> SymBiMap -> SymBiMap
+addBiMap :: (HasCallStack) => SomeTerm -> Dynamic -> String -> SomeTypedSymbol -> SymBiMap -> SymBiMap
 addBiMap s d n sb (SymBiMap t f) = SymBiMap (M.insert s d t) (M.insert n sb f)
 
-addBiMapIntermediate :: HasCallStack => SomeTerm -> Dynamic -> SymBiMap -> SymBiMap
+addBiMapIntermediate :: (HasCallStack) => SomeTerm -> Dynamic -> SymBiMap -> SymBiMap
 addBiMapIntermediate s d (SymBiMap t f) = SymBiMap (M.insert s d t) f
 
 findStringToSymbol :: String -> SymBiMap -> Maybe SomeTypedSymbol
 findStringToSymbol s (SymBiMap _ f) = M.lookup s f
 
-lookupTerm :: HasCallStack => SomeTerm -> SymBiMap -> Maybe Dynamic
+lookupTerm :: (HasCallStack) => SomeTerm -> SymBiMap -> Maybe Dynamic
 lookupTerm t m = M.lookup t (biMapToSBV m)
diff --git a/src/Grisette/Core.hs b/src/Grisette/Core.hs
--- a/src/Grisette/Core.hs
+++ b/src/Grisette/Core.hs
@@ -181,13 +181,8 @@
     SEq (..),
     SymBoolOp,
     SOrd (..),
-    SomeBV (..),
-    someBVZext',
-    someBVSext',
-    someBVExt',
-    someBVSelect',
-    someBVExtract,
-    someBVExtract',
+    BV (..),
+    bvExtract,
     SizedBV (..),
     sizedBVExtract,
     SafeDivision (..),
diff --git a/src/Grisette/Core/Control/Monad/CBMCExcept.hs b/src/Grisette/Core/Control/Monad/CBMCExcept.hs
--- a/src/Grisette/Core/Control/Monad/CBMCExcept.hs
+++ b/src/Grisette/Core/Control/Monad/CBMCExcept.hs
@@ -161,7 +161,7 @@
 mapCBMCExceptT f m = CBMCExceptT $ (unsafeCoerce . f . unsafeCoerce) (runCBMCExceptT m)
 
 -- | Map the error in a 'CBMCExceptT'
-withCBMCExceptT :: Functor m => (e -> e') -> CBMCExceptT e m a -> CBMCExceptT e' m a
+withCBMCExceptT :: (Functor m) => (e -> e') -> CBMCExceptT e m a -> CBMCExceptT e' m a
 withCBMCExceptT f = mapCBMCExceptT $ fmap $ either (Left . f) Right
 
 -- | Similar to 'ExceptT', but with different error handling mechanism.
@@ -282,7 +282,7 @@
   mzipWith f (CBMCExceptT a) (CBMCExceptT b) = CBMCExceptT $ mzipWith (liftA2 f) a b
   {-# INLINE mzipWith #-}
 
-instance Contravariant m => Contravariant (CBMCExceptT e m) where
+instance (Contravariant m) => Contravariant (CBMCExceptT e m) where
   contramap f = CBMCExceptT . contramap (fmap f) . runCBMCExceptT
   {-# INLINE contramap #-}
 
@@ -302,7 +302,7 @@
     CBMCEither (Right r) -> return (CBMCEither . Right $ r)
 {-# INLINE catchE #-}
 
-instance Monad m => OrigExcept.MonadError e (CBMCExceptT e m) where
+instance (Monad m) => OrigExcept.MonadError e (CBMCExceptT e m) where
   throwError = throwE
   {-# INLINE throwError #-}
   catchError = catchE
@@ -406,13 +406,13 @@
   symCompare (CBMCExceptT l) (CBMCExceptT r) = symCompare l r
 
 instance
-  ToCon (m1 (CBMCEither e1 a)) (m2 (CBMCEither e2 b)) =>
+  (ToCon (m1 (CBMCEither e1 a)) (m2 (CBMCEither e2 b))) =>
   ToCon (CBMCExceptT e1 m1 a) (CBMCExceptT e2 m2 b)
   where
   toCon (CBMCExceptT v) = CBMCExceptT <$> toCon v
 
 instance
-  ToCon (m1 (CBMCEither e1 a)) (Either e2 b) =>
+  (ToCon (m1 (CBMCEither e1 a)) (Either e2 b)) =>
   ToCon (CBMCExceptT e1 m1 a) (Either e2 b)
   where
   toCon (CBMCExceptT v) = toCon v
diff --git a/src/Grisette/Core/Control/Monad/UnionM.hs b/src/Grisette/Core/Control/Monad/UnionM.hs
--- a/src/Grisette/Core/Control/Monad/UnionM.hs
+++ b/src/Grisette/Core/Control/Monad/UnionM.hs
@@ -397,8 +397,6 @@
 TO_SYM_FROM_UNION_CON_BV(WordN, SymWordN)
 TO_SYM_FROM_UNION_CON_FUN((=->), (=~>))
 TO_SYM_FROM_UNION_CON_FUN((-->), (-~>))
-TO_SYM_FROM_UNION_CON_BV_SOME(SomeIntN, SomeSymIntN)
-TO_SYM_FROM_UNION_CON_BV_SOME(SomeWordN, SomeSymWordN)
 #endif
 
 instance {-# INCOHERENT #-} (ToCon a b) => ToCon (UnionM a) b where
@@ -543,7 +541,7 @@
       go (If _ _ _ t f) = mrgIf <$> simpleFresh () <*> go t <*> go f
 
 -- AllSyms
-instance AllSyms a => AllSyms (UnionM a) where
+instance (AllSyms a) => AllSyms (UnionM a) where
   allSymsS = allSymsS . underlyingUnion
 
 -- Concrete Key HashMaps
diff --git a/src/Grisette/Core/Data/BV.hs b/src/Grisette/Core/Data/BV.hs
--- a/src/Grisette/Core/Data/BV.hs
+++ b/src/Grisette/Core/Data/BV.hs
@@ -79,29 +79,29 @@
 data SomeWordN where
   SomeWordN :: (KnownNat n, 1 <= n) => WordN n -> SomeWordN
 
-unarySomeWordN :: HasCallStack => (forall n. (KnownNat n, 1 <= n) => WordN n -> r) -> SomeWordN -> r
+unarySomeWordN :: (HasCallStack) => (forall n. (KnownNat n, 1 <= n) => WordN n -> r) -> SomeWordN -> r
 unarySomeWordN op (SomeWordN (w :: WordN w)) = op w
 {-# INLINE unarySomeWordN #-}
 
-unarySomeWordNR1 :: HasCallStack => (forall n. (KnownNat n, 1 <= n) => WordN n -> WordN n) -> SomeWordN -> SomeWordN
+unarySomeWordNR1 :: (HasCallStack) => (forall n. (KnownNat n, 1 <= n) => WordN n -> WordN n) -> SomeWordN -> SomeWordN
 unarySomeWordNR1 op (SomeWordN (w :: WordN w)) = SomeWordN $ op w
 {-# INLINE unarySomeWordNR1 #-}
 
-binSomeWordN :: HasCallStack => (forall n. (KnownNat n, 1 <= n) => WordN n -> WordN n -> r) -> SomeWordN -> SomeWordN -> r
+binSomeWordN :: (HasCallStack) => (forall n. (KnownNat n, 1 <= n) => WordN n -> WordN n -> r) -> SomeWordN -> SomeWordN -> r
 binSomeWordN op (SomeWordN (l :: WordN l)) (SomeWordN (r :: WordN r)) =
   case sameNat (Proxy @l) (Proxy @r) of
     Just Refl -> op l r
     Nothing -> throw BitwidthMismatch
 {-# INLINE binSomeWordN #-}
 
-binSomeWordNR1 :: HasCallStack => (forall n. (KnownNat n, 1 <= n) => WordN n -> WordN n -> WordN n) -> SomeWordN -> SomeWordN -> SomeWordN
+binSomeWordNR1 :: (HasCallStack) => (forall n. (KnownNat n, 1 <= n) => WordN n -> WordN n -> WordN n) -> SomeWordN -> SomeWordN -> SomeWordN
 binSomeWordNR1 op (SomeWordN (l :: WordN l)) (SomeWordN (r :: WordN r)) =
   case sameNat (Proxy @l) (Proxy @r) of
     Just Refl -> SomeWordN $ op l r
     Nothing -> throw BitwidthMismatch
 {-# INLINE binSomeWordNR1 #-}
 
-binSomeWordNR2 :: HasCallStack => (forall n. (KnownNat n, 1 <= n) => WordN n -> WordN n -> (WordN n, WordN n)) -> SomeWordN -> SomeWordN -> (SomeWordN, SomeWordN)
+binSomeWordNR2 :: (HasCallStack) => (forall n. (KnownNat n, 1 <= n) => WordN n -> WordN n -> (WordN n, WordN n)) -> SomeWordN -> SomeWordN -> (SomeWordN, SomeWordN)
 binSomeWordNR2 op (SomeWordN (l :: WordN l)) (SomeWordN (r :: WordN r)) =
   case sameNat (Proxy @l) (Proxy @r) of
     Just Refl ->
@@ -111,9 +111,15 @@
 {-# INLINE binSomeWordNR2 #-}
 
 instance Eq SomeWordN where
-  (==) = binSomeWordN (==)
+  SomeWordN (l :: WordN l) == SomeWordN (r :: WordN r) =
+    case sameNat (Proxy @l) (Proxy @r) of
+      Just Refl -> l == r
+      Nothing -> False
   {-# INLINE (==) #-}
-  (/=) = binSomeWordN (/=)
+  SomeWordN (l :: WordN l) /= SomeWordN (r :: WordN r) =
+    case sameNat (Proxy @l) (Proxy @r) of
+      Just Refl -> l /= r
+      Nothing -> True
   {-# INLINE (/=) #-}
 
 instance Ord SomeWordN where
@@ -150,7 +156,7 @@
       binRepPre = "0b" ++ replicate (fromIntegral bitwidth - length binRep) '0'
       binRep = showIntAtBase 2 (\x -> if x == 0 then '0' else '1') w ""
 
-convertInt :: Num a => L.Lexeme -> ReadPrec a
+convertInt :: (Num a) => L.Lexeme -> ReadPrec a
 convertInt (L.Number n)
   | Just i <- L.numberToInteger n = return (fromInteger i)
 convertInt _ = pfail
@@ -205,9 +211,15 @@
 {-# INLINE binSomeIntNR2 #-}
 
 instance Eq SomeIntN where
-  (==) = binSomeIntN (==)
+  SomeIntN (l :: IntN l) == SomeIntN (r :: IntN r) =
+    case sameNat (Proxy @l) (Proxy @r) of
+      Just Refl -> l == r
+      Nothing -> False
   {-# INLINE (==) #-}
-  (/=) = binSomeIntN (/=)
+  SomeIntN (l :: IntN l) /= SomeIntN (r :: IntN r) =
+    case sameNat (Proxy @l) (Proxy @r) of
+      Just Refl -> l /= r
+      Nothing -> True
   {-# INLINE (/=) #-}
 
 instance Ord SomeIntN where
@@ -270,8 +282,8 @@
 
   -- complementBit use default implementation
   testBit (WordN a) = testBit a
-  bitSizeMaybe _ = Just $ fromIntegral (natVal (Proxy :: Proxy n))
-  bitSize _ = fromIntegral (natVal (Proxy :: Proxy n))
+  bitSizeMaybe = Just . finiteBitSize
+  bitSize = finiteBitSize
   isSigned _ = False
   shiftL (WordN a) i = WordN (a `shiftL` i) .&. maxBound
 
@@ -312,8 +324,8 @@
   clearBit s i = unarySomeWordNR1 (`clearBit` i) s
   complementBit s i = unarySomeWordNR1 (`complementBit` i) s
   testBit s i = unarySomeWordN (`testBit` i) s
-  bitSizeMaybe (SomeWordN (n :: WordN n)) = Just $ fromIntegral $ natVal n
-  bitSize (SomeWordN (n :: WordN n)) = fromIntegral $ natVal n
+  bitSizeMaybe = Just . finiteBitSize
+  bitSize = finiteBitSize
   isSigned _ = False
   shiftL s i = unarySomeWordNR1 (`shiftL` i) s
   unsafeShiftL s i = unarySomeWordNR1 (`unsafeShiftL` i) s
@@ -405,7 +417,7 @@
   signum = unarySomeWordNR1 signum
   fromInteger = error "fromInteger is not defined for SomeWordN as no bitwidth is known"
 
-minusOneIntN :: forall proxy n. KnownNat n => proxy n -> IntN n
+minusOneIntN :: forall proxy n. (KnownNat n) => proxy n -> IntN n
 minusOneIntN _ = IntN (1 `shiftL` fromIntegral (natVal (Proxy :: Proxy n)) - 1)
 
 instance (KnownNat n, 1 <= n) => Bits (IntN n) where
@@ -424,8 +436,8 @@
 
   -- complementBit use default implementation
   testBit (IntN a) = testBit a
-  bitSizeMaybe _ = Just $ fromIntegral (natVal (Proxy :: Proxy n))
-  bitSize _ = fromIntegral (natVal (Proxy :: Proxy n))
+  bitSizeMaybe = Just . finiteBitSize
+  bitSize = finiteBitSize
   isSigned _ = True
 
   shiftL (IntN a) i = IntN (unWordN $ (WordN a :: WordN n) `shiftL` i)
@@ -459,8 +471,8 @@
   clearBit s i = unarySomeIntNR1 (`clearBit` i) s
   complementBit s i = unarySomeIntNR1 (`complementBit` i) s
   testBit s i = unarySomeIntN (`testBit` i) s
-  bitSizeMaybe (SomeIntN (n :: IntN n)) = Just $ fromIntegral $ natVal n
-  bitSize (SomeIntN (n :: IntN n)) = fromIntegral $ natVal n
+  bitSizeMaybe = Just . finiteBitSize
+  bitSize = finiteBitSize
   isSigned _ = False
   shiftL s i = unarySomeIntNR1 (`shiftL` i) s
   unsafeShiftL s i = unarySomeIntNR1 (`unsafeShiftL` i) s
@@ -596,10 +608,10 @@
       noi = (1 :: Integer) `shiftL` l
   sizedBVExt = sizedBVZext
   sizedBVSelect ::
-    forall n ix w proxy.
+    forall n ix w p q.
     (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, ix + w <= n) =>
-    proxy ix ->
-    proxy w ->
+    p ix ->
+    q w ->
     WordN n ->
     WordN w
   sizedBVSelect pix pw (WordN v) = WordN ((v `shiftR` ix) .&. mask)
@@ -616,76 +628,71 @@
   sizedBVSext pr (IntN v) = IntN $ unWordN $ sizedBVSext pr (WordN v :: WordN l)
   sizedBVExt = sizedBVSext
   sizedBVSelect ::
-    forall n ix w proxy.
+    forall n ix w p q.
     (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, ix + w <= n) =>
-    proxy ix ->
-    proxy w ->
+    p ix ->
+    q w ->
     IntN n ->
     IntN w
   sizedBVSelect pix pw (IntN v) = IntN $ unWordN $ sizedBVSelect pix pw (WordN v :: WordN n)
 
-instance SomeBV SomeWordN where
-  someBVConcat (SomeWordN (a :: WordN l)) (SomeWordN (b :: WordN r)) =
+instance BV SomeWordN where
+  bvConcat (SomeWordN (a :: WordN l)) (SomeWordN (b :: WordN r)) =
     case (leqAddPos (Proxy @l) (Proxy @r), knownAdd @l @r KnownProof KnownProof) of
       (LeqProof, KnownProof) ->
         SomeWordN $ sizedBVConcat a b
-  someBVZext (p :: p l) (SomeWordN (a :: WordN n))
-    | l < n = error "someBVZext: trying to zero extend a value to a smaller size"
-    | otherwise =
-        case (unsafeLeqProof @1 @l, unsafeLeqProof @n @l) of
-          (LeqProof, LeqProof) -> SomeWordN $ sizedBVZext p a
+  {-# INLINE bvConcat #-}
+  bvZext l (SomeWordN (a :: WordN n))
+    | l < n = error "bvZext: trying to zero extend a value to a smaller size"
+    | otherwise = res (Proxy @n)
     where
-      l = natVal p
-      n = natVal (Proxy @n)
-  someBVSext (p :: p l) (SomeWordN (a :: WordN n))
-    | l < n = error "someBVSext: trying to zero extend a value to a smaller size"
-    | otherwise =
-        case (unsafeLeqProof @1 @l, unsafeLeqProof @n @l) of
-          (LeqProof, LeqProof) -> SomeWordN $ sizedBVSext p a
+      n = fromIntegral $ natVal (Proxy @n)
+      res :: forall (l :: Nat). Proxy l -> SomeWordN
+      res p =
+        case (unsafeKnownProof @l (fromIntegral l), unsafeLeqProof @1 @l, unsafeLeqProof @n @l) of
+          (KnownProof, LeqProof, LeqProof) -> SomeWordN $ sizedBVZext p a
+  bvSext l (SomeWordN (a :: WordN n))
+    | l < n = error "bvSext: trying to zero extend a value to a smaller size"
+    | otherwise = res (Proxy @n)
     where
-      l = natVal p
-      n = natVal (Proxy @n)
-  someBVExt = someBVZext
-  someBVSelect (p :: p ix) (q :: q w) (SomeWordN (a :: WordN n))
-    | ix + w > n = error "someBVSelect: trying to select a bitvector outside the bounds of the input"
-    | w == 0 = error "someBVSelect: trying to select a bitvector of size 0"
-    | otherwise =
-        case (unsafeLeqProof @1 @w, unsafeLeqProof @(ix + w) @n) of
-          (LeqProof, LeqProof) -> SomeWordN $ sizedBVSelect (Proxy @ix) (Proxy @w) a
+      n = fromIntegral $ natVal (Proxy @n)
+      res :: forall (l :: Nat). Proxy l -> SomeWordN
+      res p =
+        case (unsafeKnownProof @l (fromIntegral l), unsafeLeqProof @1 @l, unsafeLeqProof @n @l) of
+          (KnownProof, LeqProof, LeqProof) -> SomeWordN $ sizedBVSext p a
+  bvExt = bvZext
+  bvSelect ix w (SomeWordN (a :: WordN n))
+    | ix + w > n = error "bvSelect: trying to select a bitvector outside the bounds of the input"
+    | w == 0 = error "bvSelect: trying to select a bitvector of size 0"
+    | otherwise = res (Proxy @n) (Proxy @n)
     where
-      ix = natVal p
-      w = natVal q
-      n = natVal (Proxy @n)
+      n = fromIntegral $ natVal (Proxy @n)
+      res :: forall (w :: Nat) (ix :: Nat). Proxy w -> Proxy ix -> SomeWordN
+      res p1 p2 =
+        case ( unsafeKnownProof @ix (fromIntegral ix),
+               unsafeKnownProof @w (fromIntegral w),
+               unsafeLeqProof @1 @w,
+               unsafeLeqProof @(ix + w) @n
+             ) of
+          (KnownProof, KnownProof, LeqProof, LeqProof) ->
+            SomeWordN $ sizedBVSelect (Proxy @ix) (Proxy @w) a
 
-instance SomeBV SomeIntN where
-  someBVConcat (SomeIntN (a :: IntN l)) (SomeIntN (b :: IntN r)) =
-    case (leqAddPos (Proxy @l) (Proxy @r), knownAdd (KnownProof @l) (KnownProof @r)) of
-      (LeqProof, KnownProof) ->
-        SomeIntN $ sizedBVConcat a b
-  someBVZext (p :: p l) (SomeIntN (a :: IntN n))
-    | l < n = error "someBVZext: trying to zero extend a value to a smaller size"
-    | otherwise =
-        case (unsafeLeqProof @1 @l, unsafeLeqProof @n @l) of
-          (LeqProof, LeqProof) -> SomeIntN $ sizedBVZext p a
-    where
-      l = natVal p
-      n = natVal (Proxy @n)
-  someBVSext (p :: p l) (SomeIntN (a :: IntN n))
-    | l < n = error "someBVSext: trying to zero extend a value to a smaller size"
-    | otherwise =
-        case (unsafeLeqProof @1 @l, unsafeLeqProof @n @l) of
-          (LeqProof, LeqProof) -> SomeIntN $ sizedBVSext p a
-    where
-      l = natVal p
-      n = natVal (Proxy @n)
-  someBVExt = someBVZext
-  someBVSelect (p :: p ix) (q :: q w) (SomeIntN (a :: IntN n))
-    | ix + w > n = error "someBVSelect: trying to select a bitvector outside the bounds of the input"
-    | w == 0 = error "someBVSelect: trying to select a bitvector of size 0"
-    | otherwise =
-        case (unsafeLeqProof @1 @w, unsafeLeqProof @(ix + w) @n) of
-          (LeqProof, LeqProof) -> SomeIntN $ sizedBVSelect (Proxy @ix) (Proxy @w) a
-    where
-      ix = natVal p
-      w = natVal q
-      n = natVal (Proxy @n)
+instance BV SomeIntN where
+  bvConcat l r = toSigned $ bvConcat (toUnsigned l) (toUnsigned l)
+  {-# INLINE bvConcat #-}
+  bvZext l = toSigned . bvZext l . toUnsigned
+  {-# INLINE bvZext #-}
+  bvSext l = toSigned . bvSext l . toUnsigned
+  {-# INLINE bvSext #-}
+  bvExt l = toSigned . bvExt l . toUnsigned
+  {-# INLINE bvExt #-}
+  bvSelect ix w = toSigned . bvSelect ix w . toUnsigned
+  {-# INLINE bvSelect #-}
+
+instance (KnownNat n, 1 <= n) => BVSignConversion (WordN n) (IntN n) where
+  toSigned (WordN i) = IntN i
+  toUnsigned (IntN i) = WordN i
+
+instance BVSignConversion SomeWordN SomeIntN where
+  toSigned (SomeWordN i) = SomeIntN $ toSigned i
+  toUnsigned (SomeIntN i) = SomeWordN $ toUnsigned i
diff --git a/src/Grisette/Core/Data/Class/BitVector.hs b/src/Grisette/Core/Data/Class/BitVector.hs
--- a/src/Grisette/Core/Data/Class/BitVector.hs
+++ b/src/Grisette/Core/Data/Class/BitVector.hs
@@ -1,6 +1,7 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FunctionalDependencies #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE RankNTypes #-}
@@ -19,15 +20,11 @@
 -- Portability :   GHC only
 module Grisette.Core.Data.Class.BitVector
   ( -- * Bit vector operations
-    SomeBV (..),
-    someBVZext',
-    someBVSext',
-    someBVExt',
-    someBVSelect',
-    someBVExtract,
-    someBVExtract',
+    BV (..),
+    bvExtract,
     SizedBV (..),
     sizedBVExtract,
+    BVSignConversion (..),
   )
 where
 
@@ -45,38 +42,34 @@
 -- >>> :set -XFlexibleInstances
 -- >>> :set -XFunctionalDependencies
 
--- | Bit vector operations. Including concatenation ('someBVConcat'),
--- extension ('someBVZext', 'someBVSext', 'someBVExt'), and selection
--- ('someBVSelect').
-class SomeBV bv where
+-- | Bit vector operations. Including concatenation ('bvConcat'),
+-- extension ('bvZext', 'bvSext', 'bvExt'), and selection
+-- ('bvSelect').
+class BV bv where
   -- | Concatenation of two bit vectors.
   --
-  -- >>> someBVConcat (SomeSymWordN (0b101 :: SymWordN 3)) (SomeSymWordN (0b010 :: SymWordN 3))
+  -- >>> bvConcat (SomeSymWordN (0b101 :: SymWordN 3)) (SomeSymWordN (0b010 :: SymWordN 3))
   -- 0b101010
-  someBVConcat :: bv -> bv -> bv
+  bvConcat :: bv -> bv -> bv
 
   -- | Zero extension of a bit vector.
   --
-  -- >>> someBVZext (Proxy @6) (SomeSymWordN (0b101 :: SymWordN 3))
+  -- >>> bvZext 6 (SomeSymWordN (0b101 :: SymWordN 3))
   -- 0b000101
-  someBVZext ::
-    forall p l.
-    KnownNat l =>
+  bvZext ::
     -- | Desired output length
-    p l ->
+    Int ->
     -- | Bit vector to extend
     bv ->
     bv
 
   -- | Sign extension of a bit vector.
   --
-  -- >>> someBVSext (Proxy @6) (SomeSymWordN (0b101 :: SymWordN 3))
+  -- >>> bvSext 6 (SomeSymWordN (0b101 :: SymWordN 3))
   -- 0b111101
-  someBVSext ::
-    forall p l.
-    KnownNat l =>
+  bvSext ::
     -- | Desired output length
-    p l ->
+    Int ->
     -- | Bit vector to extend
     bv ->
     bv
@@ -84,19 +77,17 @@
   -- | Extension of a bit vector.
   -- Signedness is determined by the input bit vector type.
   --
-  -- >>> someBVExt (Proxy @6) (SomeSymIntN (0b101 :: SymIntN 3))
+  -- >>> bvExt 6 (SomeSymIntN (0b101 :: SymIntN 3))
   -- 0b111101
-  -- >>> someBVExt (Proxy @6) (SomeSymIntN (0b001 :: SymIntN 3))
+  -- >>> bvExt 6 (SomeSymIntN (0b001 :: SymIntN 3))
   -- 0b000001
-  -- >>> someBVExt (Proxy @6) (SomeSymWordN (0b101 :: SymWordN 3))
+  -- >>> bvExt 6 (SomeSymWordN (0b101 :: SymWordN 3))
   -- 0b000101
-  -- >>> someBVExt (Proxy @6) (SomeSymWordN (0b001 :: SymWordN 3))
+  -- >>> bvExt 6 (SomeSymWordN (0b001 :: SymWordN 3))
   -- 0b000001
-  someBVExt ::
-    forall p l.
-    KnownNat l =>
+  bvExt ::
     -- | Desired output length
-    p l ->
+    Int ->
     -- | Bit vector to extend
     bv ->
     bv
@@ -106,136 +97,37 @@
   --
   -- The least significant bit is indexed as 0.
   --
-  -- >>> someBVSelect (Proxy @1) (Proxy @3) (SomeSymIntN (0b001010 :: SymIntN 6))
+  -- >>> bvSelect 1 3 (SomeSymIntN (0b001010 :: SymIntN 6))
   -- 0b101
-  someBVSelect ::
-    forall p ix q w.
-    (KnownNat ix, KnownNat w) =>
+  bvSelect ::
     -- | Index of the least significant bit of the slice
-    p ix ->
+    Int ->
     -- | Desired output width, @ix + w <= n@ must hold where @n@ is
     -- the size of the input bit vector
-    q w ->
+    Int ->
     -- | Bit vector to select from
     bv ->
     bv
 
--- | Zero extension of a bit vector.
---
--- >>> someBVZext' (natRepr @6) (SomeSymWordN (0b101 :: SymWordN 3))
--- 0b000101
-someBVZext' ::
-  forall l bv.
-  SomeBV bv =>
-  -- | Desired output length
-  NatRepr l ->
-  -- | Bit vector to extend
-  bv ->
-  bv
-someBVZext' p@(_ :: NatRepr l) = withKnownProof (hasRepr p) $ someBVZext (Proxy @l)
-{-# INLINE someBVZext' #-}
-
--- | Sign extension of a bit vector.
---
--- >>> someBVSext' (natRepr @6) (SomeSymWordN (0b101 :: SymWordN 3))
--- 0b111101
-someBVSext' ::
-  forall l bv.
-  SomeBV bv =>
-  NatRepr l ->
-  -- | Desired output length
-  bv ->
-  -- | Bit vector to extend
-  bv
-someBVSext' p@(_ :: NatRepr l) = withKnownProof (hasRepr p) $ someBVSext (Proxy @l)
-{-# INLINE someBVSext' #-}
-
--- | Extension of a bit vector.
--- Signedness is determined by the input bit vector type.
---
--- >>> someBVExt' (natRepr @6) (SomeSymIntN (0b101 :: SymIntN 3))
--- 0b111101
--- >>> someBVExt' (natRepr @6) (SomeSymIntN (0b001 :: SymIntN 3))
--- 0b000001
--- >>> someBVExt' (natRepr @6) (SomeSymWordN (0b101 :: SymWordN 3))
--- 0b000101
--- >>> someBVExt' (natRepr @6) (SomeSymWordN (0b001 :: SymWordN 3))
--- 0b000001
-someBVExt' ::
-  forall l bv.
-  SomeBV bv =>
-  -- | Desired output length
-  NatRepr l ->
-  -- | Bit vector to extend
-  bv ->
-  bv
-someBVExt' p@(_ :: NatRepr l) = withKnownProof (hasRepr p) $ someBVExt (Proxy @l)
-{-# INLINE someBVExt' #-}
-
--- | Slicing out a smaller bit vector from a larger one,
--- selecting a slice with width @w@ starting from index @ix@.
---
--- The least significant bit is indexed as 0.
---
--- >>> someBVSelect' (natRepr @1) (natRepr @3) (SomeSymIntN (0b001010 :: SymIntN 6))
--- 0b101
-someBVSelect' ::
-  forall ix w bv.
-  SomeBV bv =>
-  -- | Index of the least significant bit of the slice
-  NatRepr ix ->
-  -- | Desired output width, @ix + w <= n@ must hold where @n@ is
-  -- the size of the input bit vector
-  NatRepr w ->
-  -- | Bit vector to select from
-  bv ->
-  bv
-someBVSelect' p@(_ :: NatRepr l) q@(_ :: NatRepr r) = withKnownProof (hasRepr p) $ withKnownProof (hasRepr q) $ someBVSelect p q
-{-# INLINE someBVSelect' #-}
-
 -- | Slicing out a smaller bit vector from a larger one, extract a slice from
 -- bit @i@ down to @j@.
 --
 -- The least significant bit is indexed as 0.
 --
--- >>> someBVExtract (Proxy @4) (Proxy @2) (SomeSymIntN (0b010100 :: SymIntN 6))
--- 0b101
-someBVExtract ::
-  forall p (i :: Nat) q (j :: Nat) bv.
-  (SomeBV bv, KnownNat i, KnownNat j) =>
-  -- | The start position to extract from, @i < n@ must hold where @n@ is
-  -- the size of the output bit vector
-  p i ->
-  -- | The end position to extract from, @j <= i@ must hold
-  q j ->
-  -- | Bit vector to extract from
-  bv ->
-  bv
-someBVExtract _ _ =
-  withKnownProof (unsafeKnownProof @(i - j + 1) (fromIntegral (natVal (Proxy @i)) - fromIntegral (natVal (Proxy @j)) + 1)) $
-    someBVSelect (Proxy @j) (Proxy @(i - j + 1))
-{-# INLINE someBVExtract #-}
-
--- | Slicing out a smaller bit vector from a larger one, extract a slice from
--- bit @i@ down to @j@.
---
--- The least significant bit is indexed as 0.
---
--- >>> someBVExtract' (natRepr @4) (natRepr @2) (SomeSymIntN (0b010100 :: SymIntN 6))
+-- >>> bvExtract 4 2 (SomeSymIntN (0b010100 :: SymIntN 6))
 -- 0b101
-someBVExtract' ::
-  forall (i :: Nat) (j :: Nat) bv.
-  SomeBV bv =>
+bvExtract ::
+  (BV bv) =>
   -- | The start position to extract from, @i < n@ must hold where @n@ is
   -- the size of the output bit vector
-  NatRepr i ->
+  Int ->
   -- | The end position to extract from, @j <= i@ must hold
-  NatRepr j ->
+  Int ->
   -- | Bit vector to extract from
   bv ->
   bv
-someBVExtract' p@(_ :: NatRepr l) q@(_ :: NatRepr r) = withKnownProof (hasRepr p) $ withKnownProof (hasRepr q) $ someBVExtract p q
-{-# INLINE someBVExtract' #-}
+bvExtract i j = bvSelect j (i - j + 1)
+{-# INLINE bvExtract #-}
 
 -- | Sized bit vector operations. Including concatenation ('sizedBVConcat'),
 -- extension ('sizedBVZext', 'sizedBVSext', 'sizedBVExt'), and selection
@@ -300,10 +192,10 @@
   sizedBVSelect ::
     (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, ix + w <= n) =>
     -- | Index of the least significant bit of the slice
-    proxy ix ->
+    p ix ->
     -- | Desired output width, @ix + w <= n@ must hold where @n@ is
     -- the size of the input bit vector
-    proxy w ->
+    q w ->
     -- | Bit vector to select from
     bv n ->
     bv w
@@ -316,13 +208,13 @@
 -- >>> sizedBVExtract (Proxy @4) (Proxy @2) (con 0b010100 :: SymIntN 6)
 -- 0b101
 sizedBVExtract ::
-  forall proxy i j n bv.
+  forall p i q j n bv.
   (SizedBV bv, KnownNat n, KnownNat i, KnownNat j, 1 <= n, i + 1 <= n, j <= i) =>
   -- | The start position to extract from, @i < n@ must hold where @n@ is
   -- the size of the output bit vector
-  proxy i ->
+  p i ->
   -- | The end position to extract from, @j <= i@ must hold
-  proxy j ->
+  q j ->
   -- | Bit vector to extract from
   bv n ->
   bv (i - j + 1)
@@ -334,3 +226,11 @@
     (KnownProof, LeqProof, LeqProof) ->
       sizedBVSelect (Proxy @j) (Proxy @(i - j + 1))
 {-# INLINE sizedBVExtract #-}
+
+-- | Convert bitvectors from and to signed
+class BVSignConversion ubv sbv | ubv -> sbv, sbv -> ubv where
+  -- | Convert unsigned bitvector to signed
+  toSigned :: ubv -> sbv
+
+  -- | Convert signed bitvector to unsigned
+  toUnsigned :: sbv -> ubv
diff --git a/src/Grisette/Core/Data/Class/Bool.hs b/src/Grisette/Core/Data/Class/Bool.hs
--- a/src/Grisette/Core/Data/Class/Bool.hs
+++ b/src/Grisette/Core/Data/Class/Bool.hs
@@ -75,11 +75,11 @@
   _ ==~~ _ = con True
   {-# INLINE (==~~) #-}
 
-instance SEq c => SEq' (K1 i c) where
+instance (SEq c) => SEq' (K1 i c) where
   (K1 a) ==~~ (K1 b) = a ==~ b
   {-# INLINE (==~~) #-}
 
-instance SEq' a => SEq' (M1 i c a) where
+instance (SEq' a) => SEq' (M1 i c a) where
   (M1 a) ==~~ (M1 b) = a ==~~ b
   {-# INLINE (==~~) #-}
 
diff --git a/src/Grisette/Core/Data/Class/Evaluate.hs b/src/Grisette/Core/Data/Class/Evaluate.hs
--- a/src/Grisette/Core/Data/Class/Evaluate.hs
+++ b/src/Grisette/Core/Data/Class/Evaluate.hs
@@ -78,10 +78,10 @@
 instance EvaluateSym' U1 where
   evaluateSym' _ _ = id
 
-instance EvaluateSym c => EvaluateSym' (K1 i c) where
+instance (EvaluateSym c) => EvaluateSym' (K1 i c) where
   evaluateSym' fillDefault model (K1 v) = K1 $ evaluateSym fillDefault model v
 
-instance EvaluateSym' a => EvaluateSym' (M1 i c a) where
+instance (EvaluateSym' a) => EvaluateSym' (M1 i c a) where
   evaluateSym' fillDefault model (M1 v) = M1 $ evaluateSym' fillDefault model v
 
 instance (EvaluateSym' a, EvaluateSym' b) => EvaluateSym' (a :+: b) where
@@ -214,16 +214,16 @@
     (EvaluateSym (f a), EvaluateSym (g a)) => EvaluateSym (Sum f g a)
 
 -- WriterT
-instance EvaluateSym (m (a, s)) => EvaluateSym (WriterLazy.WriterT s m a) where
+instance (EvaluateSym (m (a, s))) => EvaluateSym (WriterLazy.WriterT s m a) where
   evaluateSym fillDefault model (WriterLazy.WriterT v) = WriterLazy.WriterT $ evaluateSym fillDefault model v
 
-instance EvaluateSym (m (a, s)) => EvaluateSym (WriterStrict.WriterT s m a) where
+instance (EvaluateSym (m (a, s))) => EvaluateSym (WriterStrict.WriterT s m a) where
   evaluateSym fillDefault model (WriterStrict.WriterT v) = WriterStrict.WriterT $ evaluateSym fillDefault model v
 
 -- Identity
-instance EvaluateSym a => EvaluateSym (Identity a) where
+instance (EvaluateSym a) => EvaluateSym (Identity a) where
   evaluateSym fillDefault model (Identity a) = Identity $ evaluateSym fillDefault model a
 
 -- IdentityT
-instance EvaluateSym (m a) => EvaluateSym (IdentityT m a) where
+instance (EvaluateSym (m a)) => EvaluateSym (IdentityT m a) where
   evaluateSym fillDefault model (IdentityT a) = IdentityT $ evaluateSym fillDefault model a
diff --git a/src/Grisette/Core/Data/Class/GenSym.hs b/src/Grisette/Core/Data/Class/GenSym.hs
--- a/src/Grisette/Core/Data/Class/GenSym.hs
+++ b/src/Grisette/Core/Data/Class/GenSym.hs
@@ -6,6 +6,7 @@
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE InstanceSigs #-}
+{-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE QuantifiedConstraints #-}
@@ -99,6 +100,7 @@
 import Grisette.Core.Data.Class.Solvable
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
 import {-# SOURCE #-} Grisette.IR.SymPrim.Data.SymPrim
+import Grisette.Utils
 import Language.Haskell.TH.Syntax hiding (lift)
 
 -- $setup
@@ -219,7 +221,7 @@
 --
 -- The monad should be a reader monad for the 'FreshIdent' and a state monad for
 -- the 'FreshIndex'.
-class Monad m => MonadFresh m where
+class (Monad m) => MonadFresh m where
   -- | Increase the index by one and return the new index.
   nextFreshIndex :: m FreshIndex
 
@@ -355,7 +357,7 @@
 runFresh :: Fresh a -> FreshIdent -> a
 runFresh m ident = runIdentity $ runFreshT m ident
 
-instance Monad m => MonadFresh (FreshT m) where
+instance (Monad m) => MonadFresh (FreshT m) where
   nextFreshIndex = FreshT $ \_ idx -> return (idx, idx + 1)
   getFreshIdent = FreshT $ curry return
 
@@ -388,7 +390,7 @@
   -- is ensured. No specification is needed.
   --
   -- >>> runFresh (fresh ()) "a" :: UnionM (Maybe Bool)
-  -- {If a@0 Nothing (If a@1 (Just False) (Just True))}
+  -- {If a@1 Nothing (If a@0 (Just False) (Just True))}
   --
   -- The following example generates lists of symbolic booleans with length 1 to 2.
   --
@@ -807,20 +809,23 @@
 
 -- Either
 instance
-  ( GenSymSimple a a,
+  ( GenSym aspec a,
     Mergeable a,
-    GenSymSimple b b,
+    GenSym bspec b,
     Mergeable b
   ) =>
-  GenSym (Either a b) (Either a b)
+  GenSym (Either aspec bspec) (Either a b)
+  where
+  fresh (Left aspec) = (merge . fmap Left) <$> fresh aspec
+  fresh (Right bspec) = (merge . fmap Right) <$> fresh bspec
 
 instance
-  ( GenSymSimple a a,
-    GenSymSimple b b
+  ( GenSymSimple aspec a,
+    GenSymSimple bspec b
   ) =>
-  GenSymSimple (Either a b) (Either a b)
+  GenSymSimple (Either aspec bspec) (Either a b)
   where
-  simpleFresh = derivedSameShapeSimpleFresh
+  simpleFresh (Left a) = Left <$> simpleFresh a
 
 instance
   (GenSym () a, Mergeable a, GenSym () b, Mergeable b) =>
@@ -828,35 +833,54 @@
   where
   fresh = derivedNoSpecFresh
 
+instance
+  ( GenSym aspec a,
+    Mergeable a,
+    GenSym bspec b,
+    Mergeable b
+  ) =>
+  GenSym (aspec, bspec) (Either a b)
+  where
+  fresh (aspec, bspec) = do
+    l :: UnionM a <- fresh aspec
+    r :: UnionM b <- fresh bspec
+    chooseUnionFresh [Left <$> l, Right <$> r]
+
 -- Maybe
 instance
-  (GenSymSimple a a, Mergeable a) =>
-  GenSym (Maybe a) (Maybe a)
+  (GenSym aspec a, Mergeable a) =>
+  GenSym (Maybe aspec) (Maybe a)
+  where
+  fresh Nothing = return $ mrgSingle Nothing
+  fresh (Just aspec) = (merge . fmap Just) <$> fresh aspec
 
 instance
-  (GenSymSimple a a) =>
-  GenSymSimple (Maybe a) (Maybe a)
+  (GenSymSimple aspec a) =>
+  GenSymSimple (Maybe aspec) (Maybe a)
   where
-  simpleFresh = derivedSameShapeSimpleFresh
+  simpleFresh Nothing = return Nothing
+  simpleFresh (Just aspec) = Just <$> simpleFresh aspec
 
-instance (GenSym () a, Mergeable a) => GenSym () (Maybe a) where
-  fresh = derivedNoSpecFresh
+instance (GenSym aspec a, Mergeable a) => GenSym aspec (Maybe a) where
+  fresh aspec = do
+    a :: UnionM a <- fresh aspec
+    chooseUnionFresh [return Nothing, Just <$> a]
 
 -- List
 instance
-  (GenSymSimple () a, Mergeable a) =>
+  (GenSym () a, Mergeable a) =>
   GenSym Integer [a]
   where
   fresh v = do
     l <- gl v
     let xs = reverse $ scanr (:) [] l
-    chooseFresh xs
+    chooseUnionFresh $ merge . sequence <$> xs
     where
-      gl :: (MonadFresh m) => Integer -> m [a]
+      gl :: (MonadFresh m) => Integer -> m [UnionM a]
       gl v1
         | v1 <= 0 = return []
         | otherwise = do
-            l <- simpleFresh ()
+            l <- fresh ()
             r <- gl (v1 - 1)
             return $ l : r
 
@@ -878,7 +902,7 @@
   deriving (Show)
 
 instance
-  (GenSymSimple spec a, Mergeable a) =>
+  (GenSym spec a, Mergeable a) =>
   GenSym (ListSpec spec) [a]
   where
   fresh (ListSpec minLen maxLen subSpec) =
@@ -887,19 +911,23 @@
       else do
         l <- gl maxLen
         let xs = drop minLen $ reverse $ scanr (:) [] l
-        chooseFresh xs
+        chooseUnionFresh $ merge . sequence <$> xs
     where
-      gl :: (MonadFresh m) => Int -> m [a]
+      gl :: (MonadFresh m) => Int -> m [UnionM a]
       gl currLen
         | currLen <= 0 = return []
         | otherwise = do
-            l <- simpleFresh subSpec
+            l <- fresh subSpec
             r <- gl (currLen - 1)
             return $ l : r
 
 instance
-  (GenSymSimple a a, Mergeable a) =>
+  (GenSym a a, Mergeable a) =>
   GenSym [a] [a]
+  where
+  fresh l = do
+    r :: [UnionM a] <- traverse fresh l
+    return $ merge $ sequence r
 
 instance
   (GenSymSimple a a) =>
@@ -920,10 +948,22 @@
   deriving (Show)
 
 instance
-  (GenSymSimple spec a, Mergeable a) =>
+  (GenSym spec a, Mergeable a) =>
   GenSym (SimpleListSpec spec) [a]
   where
-  fresh = fmap mrgSingle . simpleFresh
+  fresh (SimpleListSpec len subSpec) =
+    if len < 0
+      then error $ "Bad lengths: " ++ show len
+      else do
+        merge . sequence <$> gl len
+    where
+      gl :: (MonadFresh m) => Int -> m [UnionM a]
+      gl currLen
+        | currLen <= 0 = return []
+        | otherwise = do
+            l <- fresh subSpec
+            r <- gl (currLen - 1)
+            return $ l : r
 
 instance
   (GenSymSimple spec a) =>
@@ -1579,6 +1619,19 @@
   simpleFresh _ = do; \
     i :: origtype n <- simpleFresh (); \
     return $ symtype i
+#define GENSYM_N_INT_BV_SOME(symtype) \
+instance GenSym Int symtype where \
+  fresh p = mrgSingle <$> simpleFresh p
+#define GENSYM_N_INT_SIMPLE_BV_SOME(symtype, origtype) \
+instance GenSymSimple Int symtype where \
+  simpleFresh i = if i > 0 then f (Proxy @0) else \
+    error "Can only generate bit vectors with positive bit size" \
+    where \
+      f :: forall p (n :: Nat) m. (MonadFresh m) => p n -> m symtype; \
+      f p = case (unsafeKnownProof @n (fromIntegral i), unsafeLeqProof @1 @n) of \
+        (KnownProof, LeqProof) -> do \
+        v :: origtype n <- simpleFresh (); \
+        return $ symtype v; \
 
 #define GENSYM_FUN(op) \
 instance (SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => GenSym (sa op sb) (sa op sb)
@@ -1620,10 +1673,14 @@
 GENSYM_SIMPLE_BV_SOME(SomeSymIntN)
 GENSYM_N_BV_SOME(SomeSymIntN)
 GENSYM_N_SIMPLE_BV_SOME(SomeSymIntN, SymIntN)
+GENSYM_N_INT_BV_SOME(SomeSymIntN)
+GENSYM_N_INT_SIMPLE_BV_SOME(SomeSymIntN, SymIntN)
 GENSYM_BV_SOME(SomeSymWordN)
 GENSYM_SIMPLE_BV_SOME(SomeSymWordN)
 GENSYM_N_BV_SOME(SomeSymWordN)
 GENSYM_N_SIMPLE_BV_SOME(SomeSymWordN, SymWordN)
+GENSYM_N_INT_BV_SOME(SomeSymWordN)
+GENSYM_N_INT_SIMPLE_BV_SOME(SomeSymWordN, SymWordN)
 
 GENSYM_FUN(=~>)
 GENSYM_SIMPLE_FUN(=~>)
diff --git a/src/Grisette/Core/Data/Class/Mergeable.hs b/src/Grisette/Core/Data/Class/Mergeable.hs
--- a/src/Grisette/Core/Data/Class/Mergeable.hs
+++ b/src/Grisette/Core/Data/Class/Mergeable.hs
@@ -78,6 +78,7 @@
 import Grisette.Core.Data.Class.Bool
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
 import {-# SOURCE #-} Grisette.IR.SymPrim.Data.SymPrim
+import Grisette.Utils
 import Unsafe.Coerce
 
 -- | Helper type for combining arbitrary number of indices into one.
@@ -322,15 +323,15 @@
   liftRootStrategy' m = wrapStrategy m Par1 unPar1
   {-# INLINE liftRootStrategy' #-}
 
-instance Mergeable1 f => Mergeable1' (Rec1 f) where
+instance (Mergeable1 f) => Mergeable1' (Rec1 f) where
   liftRootStrategy' m = wrapStrategy (liftRootStrategy m) Rec1 unRec1
   {-# INLINE liftRootStrategy' #-}
 
-instance Mergeable c => Mergeable1' (K1 i c) where
+instance (Mergeable c) => Mergeable1' (K1 i c) where
   liftRootStrategy' _ = wrapStrategy rootStrategy K1 unK1
   {-# INLINE liftRootStrategy' #-}
 
-instance Mergeable1' a => Mergeable1' (M1 i c a) where
+instance (Mergeable1' a) => Mergeable1' (M1 i c a) where
   liftRootStrategy' m = wrapStrategy (liftRootStrategy' m) M1 unM1
   {-# INLINE liftRootStrategy' #-}
 
@@ -529,15 +530,15 @@
     strategies = snd <$> r
 {-# INLINE buildStrategyList #-}
 
-instance Eq1 container => Eq (StrategyList container) where
+instance (Eq1 container) => Eq (StrategyList container) where
   (StrategyList idxs1 _) == (StrategyList idxs2 _) = eq1 idxs1 idxs2
   {-# INLINE (==) #-}
 
-instance Ord1 container => Ord (StrategyList container) where
+instance (Ord1 container) => Ord (StrategyList container) where
   compare (StrategyList idxs1 _) (StrategyList idxs2 _) = compare1 idxs1 idxs2
   {-# INLINE compare #-}
 
-instance Show1 container => Show (StrategyList container) where
+instance (Show1 container) => Show (StrategyList container) where
   showsPrec i (StrategyList idxs1 _) = showsPrec1 i idxs1
 
 -- List
@@ -975,10 +976,6 @@
 instance (KnownNat n, 1 <= n) => Mergeable (symtype n) where \
   rootStrategy = SimpleStrategy ites
 
-#define MERGEABLE_BV_SOME(symtype) \
-instance Mergeable symtype where \
-  rootStrategy = SimpleStrategy ites
-
 #define MERGEABLE_FUN(op) \
 instance (SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => Mergeable (sa op sb) where \
   rootStrategy = SimpleStrategy ites
@@ -988,11 +985,33 @@
 MERGEABLE_SIMPLE(SymInteger)
 MERGEABLE_BV(SymIntN)
 MERGEABLE_BV(SymWordN)
-MERGEABLE_BV_SOME(SomeSymIntN)
-MERGEABLE_BV_SOME(SomeSymWordN)
 MERGEABLE_FUN(=~>)
 MERGEABLE_FUN(-~>)
 #endif
+
+instance Mergeable SomeSymIntN where
+  rootStrategy =
+    SortedStrategy @Natural
+      (\(SomeSymIntN (v :: SymIntN n)) -> natVal (Proxy @n))
+      ( \n ->
+          SimpleStrategy
+            ( \c (SomeSymIntN (l :: SymIntN l)) (SomeSymIntN (r :: SymIntN r)) ->
+                case unsafeAxiom @l @r of
+                  Refl -> SomeSymIntN $ ites c l r
+            )
+      )
+
+instance Mergeable SomeSymWordN where
+  rootStrategy =
+    SortedStrategy @Natural
+      (\(SomeSymWordN (v :: SymWordN n)) -> natVal (Proxy @n))
+      ( \n ->
+          SimpleStrategy
+            ( \c (SomeSymWordN (l :: SymWordN l)) (SomeSymWordN (r :: SymWordN r)) ->
+                case unsafeAxiom @l @r of
+                  Refl -> SomeSymWordN $ ites c l r
+            )
+      )
 
 -- Exceptions
 instance Mergeable ArithException where
diff --git a/src/Grisette/Core/Data/Class/ModelOps.hs b/src/Grisette/Core/Data/Class/ModelOps.hs
--- a/src/Grisette/Core/Data/Class/ModelOps.hs
+++ b/src/Grisette/Core/Data/Class/ModelOps.hs
@@ -56,7 +56,7 @@
 -- >>> differenceSet abSet acSet
 -- SymbolSet {b :: Bool}
 class
-  Monoid symbolSet =>
+  (Monoid symbolSet) =>
   SymbolSetOps symbolSet (typedSymbol :: Type -> Type)
     | symbolSet -> typedSymbol
   where
@@ -87,7 +87,7 @@
 -- >>> buildSymbolSet ("a" :: TypedSymbol Bool, "b" :: TypedSymbol Bool) :: SymbolSet
 -- SymbolSet {a :: Bool, b :: Bool}
 class
-  SymbolSetOps symbolSet typedSymbol =>
+  (SymbolSetOps symbolSet typedSymbol) =>
   SymbolSetRep rep symbolSet (typedSymbol :: * -> *)
   where
   -- | Build a symbolic constant set
@@ -120,7 +120,7 @@
 -- >>> exact acSet abModel
 -- Model {a -> True :: Bool, c -> False :: Bool}
 class
-  SymbolSetOps symbolSet typedSymbol =>
+  (SymbolSetOps symbolSet typedSymbol) =>
   ModelOps model symbolSet typedSymbol
     | model -> symbolSet typedSymbol
   where
diff --git a/src/Grisette/Core/Data/Class/SOrd.hs b/src/Grisette/Core/Data/Class/SOrd.hs
--- a/src/Grisette/Core/Data/Class/SOrd.hs
+++ b/src/Grisette/Core/Data/Class/SOrd.hs
@@ -279,7 +279,7 @@
   (>~) = symCompareSingleList False True
   symCompare = symCompareList
 
-deriving via (Default (Maybe a)) instance SOrd a => SOrd (Maybe a)
+deriving via (Default (Maybe a)) instance (SOrd a) => SOrd (Maybe a)
 
 deriving via (Default (Either a b)) instance (SOrd a, SOrd b) => SOrd (Either a b)
 
diff --git a/src/Grisette/Core/Data/Class/SimpleMergeable.hs b/src/Grisette/Core/Data/Class/SimpleMergeable.hs
--- a/src/Grisette/Core/Data/Class/SimpleMergeable.hs
+++ b/src/Grisette/Core/Data/Class/SimpleMergeable.hs
@@ -104,7 +104,7 @@
 -- > data X = ...
 -- >   deriving Generic
 -- >   deriving (Mergeable, SimpleMergeable) via (Default X)
-class Mergeable a => SimpleMergeable a where
+class (Mergeable a) => SimpleMergeable a where
   -- | Performs if-then-else with the simple root merge strategy.
   --
   -- >>> mrgIte "a" "b" "c" :: SymInteger
@@ -359,7 +359,7 @@
     )
   {-# INLINE mrgIte #-}
 
-instance SimpleMergeable b => SimpleMergeable (a -> b) where
+instance (SimpleMergeable b) => SimpleMergeable (a -> b) where
   mrgIte = mrgIte1
   {-# INLINE mrgIte #-}
 
@@ -694,7 +694,7 @@
 --
 -- >>> case (single 1 :: UnionM Integer) of SingleU v -> v
 -- 1
-pattern SingleU :: UnionPrjOp u => a -> u a
+pattern SingleU :: (UnionPrjOp u) => a -> u a
 pattern SingleU x <-
   (singleView -> Just x)
   where
@@ -703,7 +703,7 @@
 -- | Pattern match to extract guard values with 'ifView'
 -- >>> case (unionIf "a" (single 1) (single 2) :: UnionM Integer) of IfU c t f -> (c,t,f)
 -- (a,<1>,<2>)
-pattern IfU :: UnionPrjOp u => SymBool -> u a -> u a -> u a
+pattern IfU :: (UnionPrjOp u) => SymBool -> u a -> u a -> u a
 pattern IfU c t f <-
   (ifView -> Just (c, t, f))
   where
@@ -785,11 +785,6 @@
   mrgIte = ites; \
   {-# INLINE mrgIte #-}
 
-#define SIMPLE_MERGEABLE_SOME_BV(symtype, bf) \
-instance SimpleMergeable symtype where \
-  mrgIte c = bf (ites c) "mrgIte"; \
-  {-# INLINE mrgIte #-}
-
 #define SIMPLE_MERGEABLE_FUN(op) \
 instance (SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => SimpleMergeable (sa op sb) where \
   mrgIte = ites; \
@@ -800,8 +795,6 @@
 SIMPLE_MERGEABLE_SIMPLE(SymInteger)
 SIMPLE_MERGEABLE_BV(SymIntN)
 SIMPLE_MERGEABLE_BV(SymWordN)
-SIMPLE_MERGEABLE_SOME_BV(SomeSymIntN, binSomeSymIntNR1)
-SIMPLE_MERGEABLE_SOME_BV(SomeSymWordN, binSomeSymWordNR1)
 SIMPLE_MERGEABLE_FUN(=~>)
 SIMPLE_MERGEABLE_FUN(-~>)
 #endif
diff --git a/src/Grisette/Core/Data/Class/SimpleMergeable.hs-boot b/src/Grisette/Core/Data/Class/SimpleMergeable.hs-boot
--- a/src/Grisette/Core/Data/Class/SimpleMergeable.hs-boot
+++ b/src/Grisette/Core/Data/Class/SimpleMergeable.hs-boot
@@ -6,5 +6,5 @@
 import {-# SOURCE #-} Grisette.Core.Data.Class.Mergeable
 import {-# SOURCE #-} Grisette.IR.SymPrim.Data.SymPrim
 
-class Mergeable a => SimpleMergeable a where
+class (Mergeable a) => SimpleMergeable a where
   mrgIte :: SymBool -> a -> a -> a
diff --git a/src/Grisette/Core/Data/Class/Solvable.hs b/src/Grisette/Core/Data/Class/Solvable.hs
--- a/src/Grisette/Core/Data/Class/Solvable.hs
+++ b/src/Grisette/Core/Data/Class/Solvable.hs
@@ -30,7 +30,7 @@
 
 -- | The class defines the creation and pattern matching of solvable type
 -- values.
-class IsString t => Solvable c t | t -> c where
+class (IsString t) => Solvable c t | t -> c where
   -- | Wrap a concrete value in a symbolic value.
   --
   -- >>> con True :: SymBool
@@ -95,7 +95,7 @@
 --
 -- >>> case con True :: SymBool of Con v -> v
 -- True
-pattern Con :: Solvable c t => c -> t
+pattern Con :: (Solvable c t) => c -> t
 pattern Con c <-
   (conView -> Just c)
   where
diff --git a/src/Grisette/Core/Data/Class/Substitute.hs b/src/Grisette/Core/Data/Class/Substitute.hs
--- a/src/Grisette/Core/Data/Class/Substitute.hs
+++ b/src/Grisette/Core/Data/Class/Substitute.hs
@@ -63,12 +63,12 @@
   --
   -- >>> substituteSym "a" ("c" &&~ "d" :: Sym Bool) ["a" &&~ "b" :: Sym Bool, "a"]
   -- [(&& (&& c d) b),(&& c d)]
-  substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> a -> a
+  substituteSym :: (LinkedRep cb sb) => TypedSymbol cb -> sb -> a -> a
 
 -- | Auxiliary class for 'SubstituteSym' instance derivation
 class SubstituteSym' a where
   -- | Auxiliary function for 'substituteSym' derivation
-  substituteSym' :: LinkedRep cb sb => TypedSymbol cb -> sb -> a c -> a c
+  substituteSym' :: (LinkedRep cb sb) => TypedSymbol cb -> sb -> a c -> a c
 
 instance
   ( Generic a,
@@ -81,10 +81,10 @@
 instance SubstituteSym' U1 where
   substituteSym' _ _ = id
 
-instance SubstituteSym c => SubstituteSym' (K1 i c) where
+instance (SubstituteSym c) => SubstituteSym' (K1 i c) where
   substituteSym' sym val (K1 v) = K1 $ substituteSym sym val v
 
-instance SubstituteSym' a => SubstituteSym' (M1 i c a) where
+instance (SubstituteSym' a) => SubstituteSym' (M1 i c a) where
   substituteSym' sym val (M1 v) = M1 $ substituteSym' sym val v
 
 instance (SubstituteSym' a, SubstituteSym' b) => SubstituteSym' (a :+: b) where
@@ -258,11 +258,11 @@
   substituteSym sym val (WriterStrict.WriterT v) = WriterStrict.WriterT $ substituteSym sym val v
 
 -- Identity
-instance SubstituteSym a => SubstituteSym (Identity a) where
+instance (SubstituteSym a) => SubstituteSym (Identity a) where
   substituteSym sym val (Identity a) = Identity $ substituteSym sym val a
 
 -- IdentityT
-instance SubstituteSym (m a) => SubstituteSym (IdentityT m a) where
+instance (SubstituteSym (m a)) => SubstituteSym (IdentityT m a) where
   substituteSym sym val (IdentityT a) = IdentityT $ substituteSym sym val a
 
 {-
diff --git a/src/Grisette/Core/Data/Class/ToCon.hs b/src/Grisette/Core/Data/Class/ToCon.hs
--- a/src/Grisette/Core/Data/Class/ToCon.hs
+++ b/src/Grisette/Core/Data/Class/ToCon.hs
@@ -72,10 +72,10 @@
 instance ToCon' U1 U1 where
   toCon' = Just
 
-instance ToCon a b => ToCon' (K1 i a) (K1 i b) where
+instance (ToCon a b) => ToCon' (K1 i a) (K1 i b) where
   toCon' (K1 a) = K1 <$> toCon a
 
-instance ToCon' a b => ToCon' (M1 i c1 a) (M1 i c2 b) where
+instance (ToCon' a b) => ToCon' (M1 i c1 a) (M1 i c2 b) where
   toCon' (M1 a) = M1 <$> toCon' a
 
 instance (ToCon' a1 a2, ToCon' b1 b2) => ToCon' (a1 :+: b1) (a2 :+: b2) where
@@ -172,20 +172,20 @@
 
 -- MaybeT
 instance
-  ToCon (m1 (Maybe a)) (m2 (Maybe b)) =>
+  (ToCon (m1 (Maybe a)) (m2 (Maybe b))) =>
   ToCon (MaybeT m1 a) (MaybeT m2 b)
   where
   toCon (MaybeT v) = MaybeT <$> toCon v
 
 -- ExceptT
 instance
-  ToCon (m1 (Either e1 a)) (m2 (Either e2 b)) =>
+  (ToCon (m1 (Either e1 a)) (m2 (Either e2 b))) =>
   ToCon (ExceptT e1 m1 a) (ExceptT e2 m2 b)
   where
   toCon (ExceptT v) = ExceptT <$> toCon v
 
 instance
-  ToCon (m1 (Either e1 a)) (Either e2 b) =>
+  (ToCon (m1 (Either e1 a)) (Either e2 b)) =>
   ToCon (ExceptT e1 m1 a) (Either e2 b)
   where
   toCon (ExceptT v) = toCon v
@@ -198,19 +198,19 @@
 
 -- WriterT
 instance
-  ToCon (m1 (a, s1)) (m2 (b, s2)) =>
+  (ToCon (m1 (a, s1)) (m2 (b, s2))) =>
   ToCon (WriterLazy.WriterT s1 m1 a) (WriterLazy.WriterT s2 m2 b)
   where
   toCon (WriterLazy.WriterT v) = WriterLazy.WriterT <$> toCon v
 
 instance
-  ToCon (m1 (a, s1)) (m2 (b, s2)) =>
+  (ToCon (m1 (a, s1)) (m2 (b, s2))) =>
   ToCon (WriterStrict.WriterT s1 m1 a) (WriterStrict.WriterT s2 m2 b)
   where
   toCon (WriterStrict.WriterT v) = WriterStrict.WriterT <$> toCon v
 
 -- Identity
-instance ToCon a b => ToCon (Identity a) (Identity b) where
+instance (ToCon a b) => ToCon (Identity a) (Identity b) where
   toCon (Identity a) = Identity <$> toCon a
 
 instance ToCon (Identity v) v where
@@ -220,5 +220,5 @@
   toCon = Just . Identity
 
 -- IdentityT
-instance ToCon (m a) (m1 b) => ToCon (IdentityT m a) (IdentityT m1 b) where
+instance (ToCon (m a) (m1 b)) => ToCon (IdentityT m a) (IdentityT m1 b) where
   toCon (IdentityT a) = IdentityT <$> toCon a
diff --git a/src/Grisette/Core/Data/Class/ToSym.hs b/src/Grisette/Core/Data/Class/ToSym.hs
--- a/src/Grisette/Core/Data/Class/ToSym.hs
+++ b/src/Grisette/Core/Data/Class/ToSym.hs
@@ -113,7 +113,7 @@
 deriving via (Default (Either e2 a2)) instance (ToSym e1 e2, ToSym a1 a2) => ToSym (Either e1 a1) (Either e2 a2)
 
 -- Maybe
-deriving via (Default (Maybe b)) instance ToSym a b => ToSym (Maybe a) (Maybe b)
+deriving via (Default (Maybe b)) instance (ToSym a b) => ToSym (Maybe a) (Maybe b)
 
 -- List
 deriving via (Default [b]) instance (ToSym a b) => ToSym [a] [b]
@@ -201,9 +201,9 @@
     (ToSym (f a) (f1 a1), ToSym (g a) (g1 a1)) => ToSym (Sum f g a) (Sum f1 g1 a1)
 
 -- Identity
-instance ToSym a b => ToSym (Identity a) (Identity b) where
+instance (ToSym a b) => ToSym (Identity a) (Identity b) where
   toSym (Identity a) = Identity $ toSym a
 
 -- IdentityT
-instance ToSym (m a) (m1 b) => ToSym (IdentityT m a) (IdentityT m1 b) where
+instance (ToSym (m a) (m1 b)) => ToSym (IdentityT m a) (IdentityT m1 b) where
   toSym (IdentityT v) = IdentityT $ toSym v
diff --git a/src/Grisette/Core/Data/Union.hs b/src/Grisette/Core/Data/Union.hs
--- a/src/Grisette/Core/Data/Union.hs
+++ b/src/Grisette/Core/Data/Union.hs
@@ -128,7 +128,7 @@
   s `hashWithSalt` (Single a) = s `hashWithSalt` (0 :: Int) `hashWithSalt` a
   s `hashWithSalt` (If _ _ c l r) = s `hashWithSalt` (1 :: Int) `hashWithSalt` c `hashWithSalt` l `hashWithSalt` r
 
-instance AllSyms a => AllSyms (Union a) where
+instance (AllSyms a) => AllSyms (Union a) where
   allSymsS (Single v) = allSymsS v
   allSymsS (If _ _ c t f) = \l -> SomeSym c : (allSymsS t . allSymsS f $ l)
 
diff --git a/src/Grisette/Experimental.hs b/src/Grisette/Experimental.hs
new file mode 100644
--- /dev/null
+++ b/src/Grisette/Experimental.hs
@@ -0,0 +1,25 @@
+module Grisette.Experimental
+  ( -- * Experimental features
+
+    -- | The experimental features are likely to be changed in the future,
+    -- and they do not comply with the semantics versioning policy.
+    --
+    -- Use the APIs with caution.
+
+    -- ** Symbolic Generation with Errors Class
+    GenSymConstrained (..),
+    GenSymSimpleConstrained (..),
+    genSymConstrained,
+    genSymSimpleConstrained,
+    derivedSimpleFreshConstrainedNoSpec,
+    derivedSimpleFreshConstrainedSameShape,
+    derivedFreshConstrainedNoSpec,
+
+    -- ** Some common GenSymConstrained specifications
+    SOrdUpperBound (..),
+    SOrdLowerBound (..),
+    SOrdBound (..),
+  )
+where
+
+import Grisette.Experimental.GenSymConstrained
diff --git a/src/Grisette/Experimental/GenSymConstrained.hs b/src/Grisette/Experimental/GenSymConstrained.hs
new file mode 100644
--- /dev/null
+++ b/src/Grisette/Experimental/GenSymConstrained.hs
@@ -0,0 +1,907 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DefaultSignatures #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE InstanceSigs #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module Grisette.Experimental.GenSymConstrained
+  ( -- * Symbolic value generation with errors
+    GenSymConstrained (..),
+    GenSymSimpleConstrained (..),
+    genSymConstrained,
+    genSymSimpleConstrained,
+    derivedFreshConstrainedNoSpec,
+    derivedSimpleFreshConstrainedNoSpec,
+    derivedSimpleFreshConstrainedSameShape,
+
+    -- * Some common GenSymConstrained specifications
+    SOrdUpperBound (..),
+    SOrdLowerBound (..),
+    SOrdBound (..),
+  )
+where
+
+import Control.Monad.Except
+import Control.Monad.Trans.Maybe
+import qualified Data.ByteString as B
+import Data.Int
+import Data.Word
+import Debug.Trace
+import GHC.Generics
+import GHC.TypeLits
+import Grisette.Core.Control.Monad.UnionM
+import Grisette.Core.Data.BV
+import Grisette.Core.Data.Class.Bool
+import Grisette.Core.Data.Class.GenSym
+import Grisette.Core.Data.Class.Mergeable
+import Grisette.Core.Data.Class.SOrd
+import Grisette.Core.Data.Class.SimpleMergeable
+
+-- $setup
+-- >>> import Grisette.Core
+-- >>> import Grisette.Experimental
+-- >>> import Grisette.IR.SymPrim
+-- >>> :set -XOverloadedStrings
+-- >>> :set -XTypeApplications
+
+-- | Class of types in which symbolic values can be generated with some
+-- specification.
+--
+-- See 'GenSym' for more details. The difference of this class is that it allows
+-- constraints to be generated along with the generation of symbolic values.
+class (Mergeable a) => GenSymConstrained spec a where
+  -- | Generates a symbolic value with the given specification.
+  --
+  -- Constraint violations will throw an error in the monadic environment.
+  --
+  -- >>> runFreshT (freshConstrained () (SOrdUpperBound (1 :: SymInteger) ())) "a" :: ExceptT () UnionM (UnionM SymInteger)
+  -- ExceptT <If (<= 1 a@0) (Left ()) (Right {a@0})>
+  freshConstrained ::
+    (MonadFresh m, MonadError e m, UnionLike m) =>
+    e ->
+    spec ->
+    m (UnionM a)
+  default freshConstrained ::
+    (GenSymSimpleConstrained spec a) =>
+    ( MonadFresh m,
+      MonadError e m,
+      UnionLike m
+    ) =>
+    e ->
+    spec ->
+    m (UnionM a)
+  freshConstrained e spec = mrgSingle <$> simpleFreshConstrained e spec
+
+genSymConstrained :: forall spec a e. (GenSymConstrained spec a, Mergeable e) => e -> spec -> FreshIdent -> ExceptT e UnionM (UnionM a)
+genSymConstrained e spec = merge . runFreshT (freshConstrained e spec)
+
+-- | Class of types in which symbolic values can be generated with some
+-- specification.
+--
+-- See 'GenSymSimple' for more details. The difference of this class is that it allows
+-- constraints to be generated along with the generation of symbolic values.
+class (Mergeable a) => GenSymSimpleConstrained spec a where
+  -- | Generates a symbolic value with the given specification.
+  --
+  -- Constraint violations will throw an error in the monadic environment.
+  --
+  -- >>> runFreshT (simpleFreshConstrained () (SOrdUpperBound (1 :: SymInteger) ())) "a" :: ExceptT () UnionM SymInteger
+  -- ExceptT <If (<= 1 a@0) (Left ()) (Right a@0)>
+  simpleFreshConstrained ::
+    (MonadFresh m, MonadError e m, UnionLike m) =>
+    e ->
+    spec ->
+    m a
+
+genSymSimpleConstrained :: forall spec a e. (GenSymSimpleConstrained spec a, Mergeable e) => e -> spec -> FreshIdent -> ExceptT e UnionM a
+genSymSimpleConstrained e spec = merge . runFreshT (simpleFreshConstrained e spec)
+
+instance {-# OVERLAPPABLE #-} (Mergeable a, GenSym spec a) => GenSymConstrained spec a where
+  freshConstrained _ = fresh
+
+instance {-# OVERLAPPABLE #-} (Mergeable a, GenSymSimple spec a) => GenSymSimpleConstrained spec a where
+  simpleFreshConstrained _ = simpleFresh
+
+-- | Exclusive bound, generates the values with the specification, then filters
+-- out the ones that are greater than or equal to the bound
+data SOrdUpperBound a spec = SOrdUpperBound a spec
+
+instance {-# OVERLAPPABLE #-} (SOrd a, Mergeable a, GenSym spec a) => GenSymConstrained (SOrdUpperBound a spec) a where
+  freshConstrained e (SOrdUpperBound u spec) = do
+    s <- fresh spec
+    v <- liftToMonadUnion s
+    mrgIf (v >=~ u) (throwError e) (return ())
+    mrgSingle $ mrgSingle v
+
+instance {-# OVERLAPPABLE #-} (SOrd a, Mergeable a, GenSymSimple spec a) => GenSymSimpleConstrained (SOrdUpperBound a spec) a where
+  simpleFreshConstrained e (SOrdUpperBound u spec) = do
+    s <- simpleFresh spec
+    mrgIf (s >=~ u) (throwError e) (return ())
+    mrgSingle s
+
+-- | Inclusive bound, generates the values with the specification, then filters
+-- out the ones that are less than the bound
+data SOrdLowerBound a spec = SOrdLowerBound a spec
+
+instance {-# OVERLAPPABLE #-} (SOrd a, Mergeable a, GenSym spec a) => GenSymConstrained (SOrdLowerBound a spec) a where
+  freshConstrained e (SOrdLowerBound l spec) = do
+    s <- fresh spec
+    v <- liftToMonadUnion s
+    mrgIf (v <~ l) (throwError e) (return ())
+    mrgSingle $ mrgSingle v
+
+instance {-# OVERLAPPABLE #-} (SOrd a, Mergeable a, GenSymSimple spec a) => GenSymSimpleConstrained (SOrdLowerBound a spec) a where
+  simpleFreshConstrained e (SOrdLowerBound l spec) = do
+    s <- simpleFresh spec
+    mrgIf (s <~ l) (throwError e) (return ())
+    mrgSingle s
+
+-- | Left-inclusive, right-exclusive bound, generates the values with the
+-- specification, then filters out the ones that are out-of-bound
+data SOrdBound a spec = SOrdBound a a spec
+
+instance {-# OVERLAPPABLE #-} (SOrd a, Mergeable a, GenSym spec a) => GenSymConstrained (SOrdBound a spec) a where
+  freshConstrained e (SOrdBound l u spec) = do
+    s <- fresh spec
+    v <- liftToMonadUnion s
+    mrgIf (v <~ l ||~ v >=~ u) (throwError e) (return ())
+    mrgSingle $ mrgSingle v
+
+instance {-# OVERLAPPABLE #-} (SOrd a, Mergeable a, GenSymSimple spec a) => GenSymSimpleConstrained (SOrdBound a spec) a where
+  simpleFreshConstrained e (SOrdBound l u spec) = do
+    s <- simpleFresh spec
+    mrgIf (s <~ l ||~ s >=~ u) (throwError e) (return ())
+    mrgSingle s
+
+instance GenSymConstrained (SOrdBound Integer ()) Integer where
+  freshConstrained e (SOrdBound l r _) = chooseFresh [l .. r - 1]
+
+-- Either
+instance
+  ( GenSymConstrained aspec a,
+    Mergeable a,
+    GenSymConstrained bspec b,
+    Mergeable b
+  ) =>
+  GenSymConstrained (Either aspec bspec) (Either a b)
+  where
+  freshConstrained e (Left aspec) = merge $ (merge . fmap Left) <$> freshConstrained e aspec
+  freshConstrained e (Right bspec) = merge $ (merge . fmap Right) <$> freshConstrained e bspec
+
+instance
+  ( GenSymSimpleConstrained a a,
+    GenSymSimpleConstrained b b
+  ) =>
+  GenSymSimpleConstrained (Either a b) (Either a b)
+  where
+  simpleFreshConstrained = derivedSimpleFreshConstrainedSameShape
+
+instance
+  (GenSymConstrained () a, Mergeable a, GenSymConstrained () b, Mergeable b) =>
+  GenSymConstrained () (Either a b)
+  where
+  freshConstrained = derivedFreshConstrainedNoSpec
+
+-- Maybe
+instance
+  (GenSymConstrained aspec a, Mergeable a) =>
+  GenSymConstrained (Maybe aspec) (Maybe a)
+  where
+  freshConstrained _ Nothing = mrgSingle $ mrgSingle Nothing
+  freshConstrained e (Just aspec) = merge $ (merge . fmap Just) <$> freshConstrained e aspec
+
+instance
+  (GenSymSimpleConstrained aspec a) =>
+  GenSymSimpleConstrained (Maybe aspec) (Maybe a)
+  where
+  simpleFreshConstrained _ Nothing = mrgSingle Nothing
+  simpleFreshConstrained e (Just aspec) = merge $ Just <$> simpleFreshConstrained e aspec
+
+instance (GenSymConstrained aspec a, Mergeable a) => GenSymConstrained aspec (Maybe a) where
+  freshConstrained e aspec = do
+    a :: UnionM a <- freshConstrained e aspec
+    merge $ chooseUnionFresh [return Nothing, Just <$> a]
+
+-- List
+instance
+  (GenSymConstrained () a, Mergeable a) =>
+  GenSymConstrained Integer [a]
+  where
+  freshConstrained e v = do
+    l <- gl e v
+    let xs = reverse $ scanr (:) [] l
+    merge $ chooseUnionFresh $ merge . sequence <$> xs
+    where
+      gl :: (MonadFresh m, MonadError e m, UnionLike m) => e -> Integer -> m [UnionM a]
+      gl e1 v1
+        | v1 <= 0 = mrgSingle []
+        | otherwise = do
+            l <- freshConstrained e1 ()
+            r <- gl e1 (v1 - 1)
+            mrgSingle $ l : r
+
+instance
+  (GenSymConstrained spec a, Mergeable a) =>
+  GenSymConstrained (ListSpec spec) [a]
+  where
+  freshConstrained e (ListSpec minLen maxLen subSpec) =
+    if minLen < 0 || maxLen < 0 || minLen >= maxLen
+      then error $ "Bad lengths: " ++ show (minLen, maxLen)
+      else do
+        l <- gl e maxLen
+        let xs = drop minLen $ reverse $ scanr (:) [] l
+        merge $ chooseUnionFresh $ merge . sequence <$> xs
+    where
+      gl :: (MonadFresh m, MonadError e m, UnionLike m) => e -> Int -> m [UnionM a]
+      gl e1 currLen
+        | currLen <= 0 = return []
+        | otherwise = do
+            l <- freshConstrained e1 subSpec
+            r <- gl e1 (currLen - 1)
+            return $ l : r
+
+instance
+  (GenSymConstrained a a, Mergeable a) =>
+  GenSymConstrained [a] [a]
+  where
+  freshConstrained e l = do
+    r :: [UnionM a] <- traverse (freshConstrained e) l
+    mrgSingle $ merge $ sequence r
+
+instance
+  (GenSymSimpleConstrained a a) =>
+  GenSymSimpleConstrained [a] [a]
+  where
+  simpleFreshConstrained = derivedSimpleFreshConstrainedSameShape
+
+instance
+  (GenSymConstrained spec a, Mergeable a) =>
+  GenSymConstrained (SimpleListSpec spec) [a]
+  where
+  freshConstrained e (SimpleListSpec len subSpec) =
+    if len < 0
+      then error $ "Bad lengths: " ++ show len
+      else do
+        merge $ merge . sequence <$> gl e len
+    where
+      gl :: (MonadFresh m, MonadError e m, UnionLike m) => e -> Int -> m [UnionM a]
+      gl e1 currLen
+        | currLen <= 0 = mrgSingle []
+        | otherwise = do
+            l <- freshConstrained e1 subSpec
+            r <- gl e1 (currLen - 1)
+            mrgSingle $ l : r
+
+instance
+  (GenSymSimpleConstrained spec a) =>
+  GenSymSimpleConstrained (SimpleListSpec spec) [a]
+  where
+  simpleFreshConstrained e (SimpleListSpec len subSpec) =
+    if len < 0
+      then error $ "Bad lengths: " ++ show len
+      else do
+        gl e len
+    where
+      gl :: (MonadFresh m, MonadError e m, UnionLike m) => e -> Int -> m [a]
+      gl e1 currLen
+        | currLen <= 0 = mrgSingle []
+        | otherwise = do
+            l <- simpleFreshConstrained e1 subSpec
+            r <- gl e1 (currLen - 1)
+            mrgSingle $ l : r
+
+-- (,)
+instance
+  ( GenSymConstrained aspec a,
+    Mergeable a,
+    GenSymConstrained bspec b,
+    Mergeable b
+  ) =>
+  GenSymConstrained (aspec, bspec) (a, b)
+  where
+  freshConstrained err (aspec, bspec) = do
+    a1 <- freshConstrained err aspec
+    b1 <- freshConstrained err bspec
+    mrgSingle $ do
+      ax <- a1
+      bx <- b1
+      mrgSingle (ax, bx)
+
+instance
+  ( GenSymSimpleConstrained aspec a,
+    GenSymSimpleConstrained bspec b
+  ) =>
+  GenSymSimpleConstrained (aspec, bspec) (a, b)
+  where
+  simpleFreshConstrained e (aspec, bspec) = do
+    merge $
+      (,)
+        <$> simpleFreshConstrained e aspec
+        <*> simpleFreshConstrained e bspec
+
+-- (,,)
+instance
+  ( GenSymConstrained aspec a,
+    Mergeable a,
+    GenSymConstrained bspec b,
+    Mergeable b,
+    GenSymConstrained cspec c,
+    Mergeable c
+  ) =>
+  GenSymConstrained (aspec, bspec, cspec) (a, b, c)
+  where
+  freshConstrained err (aspec, bspec, cspec) = do
+    a1 <- freshConstrained err aspec
+    b1 <- freshConstrained err bspec
+    c1 <- freshConstrained err cspec
+    mrgSingle $ do
+      ax <- a1
+      bx <- b1
+      cx <- c1
+      mrgSingle (ax, bx, cx)
+
+instance
+  ( GenSymSimpleConstrained aspec a,
+    GenSymSimpleConstrained bspec b,
+    GenSymSimpleConstrained cspec c
+  ) =>
+  GenSymSimpleConstrained (aspec, bspec, cspec) (a, b, c)
+  where
+  simpleFreshConstrained e (aspec, bspec, cspec) = do
+    merge $
+      (,,)
+        <$> simpleFreshConstrained e aspec
+        <*> simpleFreshConstrained e bspec
+        <*> simpleFreshConstrained e cspec
+
+-- (,,,)
+instance
+  ( GenSymConstrained aspec a,
+    Mergeable a,
+    GenSymConstrained bspec b,
+    Mergeable b,
+    GenSymConstrained cspec c,
+    Mergeable c,
+    GenSymConstrained dspec d,
+    Mergeable d
+  ) =>
+  GenSymConstrained (aspec, bspec, cspec, dspec) (a, b, c, d)
+  where
+  freshConstrained err (aspec, bspec, cspec, dspec) = do
+    a1 <- freshConstrained err aspec
+    b1 <- freshConstrained err bspec
+    c1 <- freshConstrained err cspec
+    d1 <- freshConstrained err dspec
+    mrgSingle $ do
+      ax <- a1
+      bx <- b1
+      cx <- c1
+      dx <- d1
+      mrgSingle (ax, bx, cx, dx)
+
+instance
+  ( GenSymSimpleConstrained aspec a,
+    GenSymSimpleConstrained bspec b,
+    GenSymSimpleConstrained cspec c,
+    GenSymSimpleConstrained dspec d
+  ) =>
+  GenSymSimpleConstrained (aspec, bspec, cspec, dspec) (a, b, c, d)
+  where
+  simpleFreshConstrained e (aspec, bspec, cspec, dspec) = do
+    merge $
+      (,,,)
+        <$> simpleFreshConstrained e aspec
+        <*> simpleFreshConstrained e bspec
+        <*> simpleFreshConstrained e cspec
+        <*> simpleFreshConstrained e dspec
+
+-- (,,,,)
+instance
+  ( GenSymConstrained aspec a,
+    Mergeable a,
+    GenSymConstrained bspec b,
+    Mergeable b,
+    GenSymConstrained cspec c,
+    Mergeable c,
+    GenSymConstrained dspec d,
+    Mergeable d,
+    GenSymConstrained espec e,
+    Mergeable e
+  ) =>
+  GenSymConstrained (aspec, bspec, cspec, dspec, espec) (a, b, c, d, e)
+  where
+  freshConstrained err (aspec, bspec, cspec, dspec, espec) = do
+    a1 <- freshConstrained err aspec
+    b1 <- freshConstrained err bspec
+    c1 <- freshConstrained err cspec
+    d1 <- freshConstrained err dspec
+    e1 <- freshConstrained err espec
+    mrgSingle $ do
+      ax <- a1
+      bx <- b1
+      cx <- c1
+      dx <- d1
+      ex <- e1
+      mrgSingle (ax, bx, cx, dx, ex)
+
+instance
+  ( GenSymSimpleConstrained aspec a,
+    GenSymSimpleConstrained bspec b,
+    GenSymSimpleConstrained cspec c,
+    GenSymSimpleConstrained dspec d,
+    GenSymSimpleConstrained espec e
+  ) =>
+  GenSymSimpleConstrained (aspec, bspec, cspec, dspec, espec) (a, b, c, d, e)
+  where
+  simpleFreshConstrained e (aspec, bspec, cspec, dspec, espec) = do
+    merge $
+      (,,,,)
+        <$> simpleFreshConstrained e aspec
+        <*> simpleFreshConstrained e bspec
+        <*> simpleFreshConstrained e cspec
+        <*> simpleFreshConstrained e dspec
+        <*> simpleFreshConstrained e espec
+
+-- (,,,,,)
+instance
+  ( GenSymConstrained aspec a,
+    Mergeable a,
+    GenSymConstrained bspec b,
+    Mergeable b,
+    GenSymConstrained cspec c,
+    Mergeable c,
+    GenSymConstrained dspec d,
+    Mergeable d,
+    GenSymConstrained espec e,
+    Mergeable e,
+    GenSymConstrained fspec f,
+    Mergeable f
+  ) =>
+  GenSymConstrained (aspec, bspec, cspec, dspec, espec, fspec) (a, b, c, d, e, f)
+  where
+  freshConstrained err (aspec, bspec, cspec, dspec, espec, fspec) = do
+    a1 <- freshConstrained err aspec
+    b1 <- freshConstrained err bspec
+    c1 <- freshConstrained err cspec
+    d1 <- freshConstrained err dspec
+    e1 <- freshConstrained err espec
+    f1 <- freshConstrained err fspec
+    mrgSingle $ do
+      ax <- a1
+      bx <- b1
+      cx <- c1
+      dx <- d1
+      ex <- e1
+      fx <- f1
+      mrgSingle (ax, bx, cx, dx, ex, fx)
+
+instance
+  ( GenSymSimpleConstrained aspec a,
+    GenSymSimpleConstrained bspec b,
+    GenSymSimpleConstrained cspec c,
+    GenSymSimpleConstrained dspec d,
+    GenSymSimpleConstrained espec e,
+    GenSymSimpleConstrained fspec f
+  ) =>
+  GenSymSimpleConstrained (aspec, bspec, cspec, dspec, espec, fspec) (a, b, c, d, e, f)
+  where
+  simpleFreshConstrained e (aspec, bspec, cspec, dspec, espec, fspec) = do
+    merge $
+      (,,,,,)
+        <$> simpleFreshConstrained e aspec
+        <*> simpleFreshConstrained e bspec
+        <*> simpleFreshConstrained e cspec
+        <*> simpleFreshConstrained e dspec
+        <*> simpleFreshConstrained e espec
+        <*> simpleFreshConstrained e fspec
+
+-- (,,,,,,)
+instance
+  ( GenSymConstrained aspec a,
+    Mergeable a,
+    GenSymConstrained bspec b,
+    Mergeable b,
+    GenSymConstrained cspec c,
+    Mergeable c,
+    GenSymConstrained dspec d,
+    Mergeable d,
+    GenSymConstrained espec e,
+    Mergeable e,
+    GenSymConstrained fspec f,
+    Mergeable f,
+    GenSymConstrained gspec g,
+    Mergeable g
+  ) =>
+  GenSymConstrained (aspec, bspec, cspec, dspec, espec, fspec, gspec) (a, b, c, d, e, f, g)
+  where
+  freshConstrained err (aspec, bspec, cspec, dspec, espec, fspec, gspec) = do
+    a1 <- freshConstrained err aspec
+    b1 <- freshConstrained err bspec
+    c1 <- freshConstrained err cspec
+    d1 <- freshConstrained err dspec
+    e1 <- freshConstrained err espec
+    f1 <- freshConstrained err fspec
+    g1 <- freshConstrained err gspec
+    mrgSingle $ do
+      ax <- a1
+      bx <- b1
+      cx <- c1
+      dx <- d1
+      ex <- e1
+      fx <- f1
+      gx <- g1
+      mrgSingle (ax, bx, cx, dx, ex, fx, gx)
+
+instance
+  ( GenSymSimpleConstrained aspec a,
+    GenSymSimpleConstrained bspec b,
+    GenSymSimpleConstrained cspec c,
+    GenSymSimpleConstrained dspec d,
+    GenSymSimpleConstrained espec e,
+    GenSymSimpleConstrained fspec f,
+    GenSymSimpleConstrained gspec g
+  ) =>
+  GenSymSimpleConstrained (aspec, bspec, cspec, dspec, espec, fspec, gspec) (a, b, c, d, e, f, g)
+  where
+  simpleFreshConstrained e (aspec, bspec, cspec, dspec, espec, fspec, gspec) = do
+    merge $
+      (,,,,,,)
+        <$> simpleFreshConstrained e aspec
+        <*> simpleFreshConstrained e bspec
+        <*> simpleFreshConstrained e cspec
+        <*> simpleFreshConstrained e dspec
+        <*> simpleFreshConstrained e espec
+        <*> simpleFreshConstrained e fspec
+        <*> simpleFreshConstrained e gspec
+
+-- (,,,,,,,)
+instance
+  ( GenSymConstrained aspec a,
+    Mergeable a,
+    GenSymConstrained bspec b,
+    Mergeable b,
+    GenSymConstrained cspec c,
+    Mergeable c,
+    GenSymConstrained dspec d,
+    Mergeable d,
+    GenSymConstrained espec e,
+    Mergeable e,
+    GenSymConstrained fspec f,
+    Mergeable f,
+    GenSymConstrained gspec g,
+    Mergeable g,
+    GenSymConstrained hspec h,
+    Mergeable h
+  ) =>
+  GenSymConstrained (aspec, bspec, cspec, dspec, espec, fspec, gspec, hspec) (a, b, c, d, e, f, g, h)
+  where
+  freshConstrained err (aspec, bspec, cspec, dspec, espec, fspec, gspec, hspec) = do
+    a1 <- freshConstrained err aspec
+    b1 <- freshConstrained err bspec
+    c1 <- freshConstrained err cspec
+    d1 <- freshConstrained err dspec
+    e1 <- freshConstrained err espec
+    f1 <- freshConstrained err fspec
+    g1 <- freshConstrained err gspec
+    h1 <- freshConstrained err hspec
+    mrgSingle $ do
+      ax <- a1
+      bx <- b1
+      cx <- c1
+      dx <- d1
+      ex <- e1
+      fx <- f1
+      gx <- g1
+      hx <- h1
+      mrgSingle (ax, bx, cx, dx, ex, fx, gx, hx)
+
+instance
+  ( GenSymSimpleConstrained aspec a,
+    GenSymSimpleConstrained bspec b,
+    GenSymSimpleConstrained cspec c,
+    GenSymSimpleConstrained dspec d,
+    GenSymSimpleConstrained espec e,
+    GenSymSimpleConstrained fspec f,
+    GenSymSimpleConstrained gspec g,
+    GenSymSimpleConstrained hspec h
+  ) =>
+  GenSymSimpleConstrained (aspec, bspec, cspec, dspec, espec, fspec, gspec, hspec) (a, b, c, d, e, f, g, h)
+  where
+  simpleFreshConstrained e (aspec, bspec, cspec, dspec, espec, fspec, gspec, hspec) = do
+    merge $
+      (,,,,,,,)
+        <$> simpleFreshConstrained e aspec
+        <*> simpleFreshConstrained e bspec
+        <*> simpleFreshConstrained e cspec
+        <*> simpleFreshConstrained e dspec
+        <*> simpleFreshConstrained e espec
+        <*> simpleFreshConstrained e fspec
+        <*> simpleFreshConstrained e gspec
+        <*> simpleFreshConstrained e hspec
+
+-- MaybeT
+instance
+  {-# OVERLAPPABLE #-}
+  ( GenSymConstrained spec (m (Maybe a)),
+    Mergeable1 m,
+    Mergeable a
+  ) =>
+  GenSymConstrained spec (MaybeT m a)
+  where
+  freshConstrained e v = do
+    x <- freshConstrained e v
+    mrgSingle $ merge . fmap MaybeT $ x
+
+instance
+  {-# OVERLAPPABLE #-}
+  ( GenSymSimpleConstrained spec (m (Maybe a)),
+    Mergeable1 m,
+    Mergeable a
+  ) =>
+  GenSymSimpleConstrained spec (MaybeT m a)
+  where
+  simpleFreshConstrained e v = merge $ MaybeT <$> simpleFreshConstrained e v
+
+instance
+  {-# OVERLAPPING #-}
+  ( GenSymSimpleConstrained (m (Maybe a)) (m (Maybe a)),
+    Mergeable1 m,
+    Mergeable a
+  ) =>
+  GenSymSimpleConstrained (MaybeT m a) (MaybeT m a)
+  where
+  simpleFreshConstrained e (MaybeT v) = merge $ MaybeT <$> simpleFreshConstrained e v
+
+instance
+  {-# OVERLAPPING #-}
+  ( GenSymSimpleConstrained (m (Maybe a)) (m (Maybe a)),
+    Mergeable1 m,
+    Mergeable a
+  ) =>
+  GenSymConstrained (MaybeT m a) (MaybeT m a)
+
+-- ExceptT
+instance
+  {-# OVERLAPPABLE #-}
+  ( GenSymConstrained spec (m (Either a b)),
+    Mergeable1 m,
+    Mergeable a,
+    Mergeable b
+  ) =>
+  GenSymConstrained spec (ExceptT a m b)
+  where
+  freshConstrained e v = trace "x" $ do
+    x <- freshConstrained e v
+    mrgSingle $ merge . fmap ExceptT $ x
+
+instance
+  {-# OVERLAPPABLE #-}
+  ( GenSymSimpleConstrained spec (m (Either a b)),
+    Mergeable1 m,
+    Mergeable a,
+    Mergeable b
+  ) =>
+  GenSymSimpleConstrained spec (ExceptT a m b)
+  where
+  simpleFreshConstrained e v = merge $ ExceptT <$> simpleFreshConstrained e v
+
+instance
+  {-# OVERLAPPING #-}
+  ( GenSymSimpleConstrained (m (Either e a)) (m (Either e a)),
+    Mergeable1 m,
+    Mergeable e,
+    Mergeable a
+  ) =>
+  GenSymSimpleConstrained (ExceptT e m a) (ExceptT e m a)
+  where
+  simpleFreshConstrained e (ExceptT v) = merge $ ExceptT <$> simpleFreshConstrained e v
+
+instance
+  {-# OVERLAPPING #-}
+  ( GenSymSimpleConstrained (m (Either e a)) (m (Either e a)),
+    Mergeable1 m,
+    Mergeable e,
+    Mergeable a
+  ) =>
+  GenSymConstrained (ExceptT e m a) (ExceptT e m a)
+
+-- Deriving
+
+class GenSymConstrainedNoSpec a where
+  freshConstrainedNoSpec ::
+    ( MonadFresh m,
+      MonadError e m,
+      UnionLike m
+    ) =>
+    e ->
+    m (UnionM (a c))
+
+instance GenSymConstrainedNoSpec U1 where
+  freshConstrainedNoSpec _ = return $ mrgSingle U1
+
+instance (GenSymConstrained () c) => GenSymConstrainedNoSpec (K1 i c) where
+  freshConstrainedNoSpec e = fmap K1 <$> freshConstrained e ()
+
+instance (GenSymConstrainedNoSpec a) => GenSymConstrainedNoSpec (M1 i c a) where
+  freshConstrainedNoSpec e = fmap M1 <$> freshConstrainedNoSpec e
+
+instance
+  ( GenSymConstrainedNoSpec a,
+    GenSymConstrainedNoSpec b,
+    forall x. Mergeable (a x),
+    forall x. Mergeable (b x)
+  ) =>
+  GenSymConstrainedNoSpec (a :+: b)
+  where
+  freshConstrainedNoSpec ::
+    forall m u c e.
+    ( MonadFresh m,
+      MonadError e m,
+      UnionLike m
+    ) =>
+    e ->
+    m (UnionM ((a :+: b) c))
+  freshConstrainedNoSpec e = do
+    cond :: bool <- simpleFresh ()
+    l :: UnionM (a c) <- freshConstrainedNoSpec e
+    r :: UnionM (b c) <- freshConstrainedNoSpec e
+    return $ mrgIf cond (fmap L1 l) (fmap R1 r)
+
+instance
+  (GenSymConstrainedNoSpec a, GenSymConstrainedNoSpec b) =>
+  GenSymConstrainedNoSpec (a :*: b)
+  where
+  freshConstrainedNoSpec ::
+    forall m u c e.
+    ( MonadFresh m,
+      MonadError e m,
+      UnionLike m
+    ) =>
+    e ->
+    m (UnionM ((a :*: b) c))
+  freshConstrainedNoSpec e = do
+    l :: UnionM (a c) <- freshConstrainedNoSpec e
+    r :: UnionM (b c) <- freshConstrainedNoSpec e
+    return $ do
+      l1 <- l
+      r1 <- r
+      return $ l1 :*: r1
+
+-- | We cannot provide DerivingVia style derivation for 'GenSymConstrained', while you can
+-- use this 'freshConstrained' implementation to implement 'GenSymConstrained' for your own types.
+--
+-- This 'freshConstrained' implementation is for the types that does not need any specification.
+-- It will generate product types by generating each fields with @()@ as specification,
+-- and generate all possible values for a sum type.
+--
+-- __Note:__ __Never__ use on recursive types.
+derivedFreshConstrainedNoSpec ::
+  forall bool a m u e.
+  ( Generic a,
+    GenSymConstrainedNoSpec (Rep a),
+    Mergeable a,
+    MonadFresh m,
+    MonadError e m,
+    UnionLike m
+  ) =>
+  e ->
+  () ->
+  m (UnionM a)
+derivedFreshConstrainedNoSpec e _ = merge $ (merge . fmap to) <$> freshConstrainedNoSpec e
+
+class GenSymSimpleConstrainedNoSpec a where
+  simpleFreshConstrainedNoSpec ::
+    ( MonadFresh m,
+      MonadError e m,
+      UnionLike m
+    ) =>
+    e ->
+    m (a c)
+
+instance GenSymSimpleConstrainedNoSpec U1 where
+  simpleFreshConstrainedNoSpec _ = return U1
+
+instance (GenSymSimpleConstrained () c) => GenSymSimpleConstrainedNoSpec (K1 i c) where
+  simpleFreshConstrainedNoSpec e = K1 <$> simpleFreshConstrained e ()
+
+instance (GenSymSimpleConstrainedNoSpec a) => GenSymSimpleConstrainedNoSpec (M1 i c a) where
+  simpleFreshConstrainedNoSpec e = M1 <$> simpleFreshConstrainedNoSpec e
+
+instance
+  (GenSymSimpleConstrainedNoSpec a, GenSymSimpleConstrainedNoSpec b) =>
+  GenSymSimpleConstrainedNoSpec (a :*: b)
+  where
+  simpleFreshConstrainedNoSpec e = do
+    l :: a c <- simpleFreshConstrainedNoSpec e
+    r :: b c <- simpleFreshConstrainedNoSpec e
+    return $ l :*: r
+
+-- | We cannot provide DerivingVia style derivation for 'GenSymSimpleConstrained', while
+-- you can use this 'simpleFreshConstrained' implementation to implement 'GenSymSimpleConstrained' fo
+-- your own types.
+--
+-- This 'simpleFreshConstrained' implementation is for the types that does not need any specification.
+-- It will generate product types by generating each fields with '()' as specification.
+-- It will not work on sum types.
+--
+-- __Note:__ __Never__ use on recursive types.
+derivedSimpleFreshConstrainedNoSpec ::
+  forall a m e.
+  ( Generic a,
+    GenSymSimpleConstrainedNoSpec (Rep a),
+    MonadFresh m,
+    MonadError e m,
+    UnionLike m,
+    Mergeable a
+  ) =>
+  e ->
+  () ->
+  m a
+derivedSimpleFreshConstrainedNoSpec e _ = merge $ (merge . fmap to) $ simpleFreshConstrainedNoSpec e
+
+class GenSymConstrainedSameShape a where
+  simpleFreshConstrainedSameShape ::
+    ( MonadFresh m,
+      MonadError e m,
+      UnionLike m
+    ) =>
+    e ->
+    a c ->
+    m (a c)
+
+instance GenSymConstrainedSameShape U1 where
+  simpleFreshConstrainedSameShape _ _ = return U1
+
+instance (GenSymSimpleConstrained c c) => GenSymConstrainedSameShape (K1 i c) where
+  simpleFreshConstrainedSameShape e (K1 c) = K1 <$> simpleFreshConstrained e c
+
+instance (GenSymConstrainedSameShape a) => GenSymConstrainedSameShape (M1 i c a) where
+  simpleFreshConstrainedSameShape e (M1 a) = M1 <$> simpleFreshConstrainedSameShape e a
+
+instance
+  (GenSymConstrainedSameShape a, GenSymConstrainedSameShape b) =>
+  GenSymConstrainedSameShape (a :+: b)
+  where
+  simpleFreshConstrainedSameShape e (L1 a) = L1 <$> simpleFreshConstrainedSameShape e a
+  simpleFreshConstrainedSameShape e (R1 a) = R1 <$> simpleFreshConstrainedSameShape e a
+
+instance
+  (GenSymConstrainedSameShape a, GenSymConstrainedSameShape b) =>
+  GenSymConstrainedSameShape (a :*: b)
+  where
+  simpleFreshConstrainedSameShape e (a :*: b) = do
+    l :: a c <- simpleFreshConstrainedSameShape e a
+    r :: b c <- simpleFreshConstrainedSameShape e b
+    return $ l :*: r
+
+-- | We cannot provide DerivingVia style derivation for 'GenSymSimpleConstrained', while
+-- you can use this 'simpleFreshConstrained' implementation to implement 'GenSymSimpleConstrained' fo
+-- your own types.
+--
+-- This 'simpleFreshConstrained' implementation is for the types that can be generated with
+-- a reference value of the same type.
+--
+-- For sum types, it will generate the result with the same data constructor.
+-- For product types, it will generate the result by generating each field with
+-- the corresponding reference value.
+--
+-- __Note:__ __Can__ be used on recursive types.
+derivedSimpleFreshConstrainedSameShape ::
+  ( Generic a,
+    GenSymConstrainedSameShape (Rep a),
+    Mergeable a,
+    MonadFresh m,
+    MonadError e m,
+    UnionLike m
+  ) =>
+  e ->
+  a ->
+  m a
+derivedSimpleFreshConstrainedSameShape e a = merge $ (merge . fmap to) $ simpleFreshConstrainedSameShape e (from a)
diff --git a/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/Caches.hs b/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/Caches.hs
--- a/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/Caches.hs
+++ b/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/Caches.hs
@@ -3,6 +3,7 @@
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
+{-# OPTIONS_GHC -fno-cse #-}
 
 -- |
 -- Module      :   Grisette.IR.SymPrim.Data.Prim.InternedTerm.Caches
@@ -14,7 +15,7 @@
 -- Portability :   GHC only
 module Grisette.IR.SymPrim.Data.Prim.InternedTerm.Caches (typeMemoizedCache) where
 
-import Control.Once
+import Control.Concurrent
 import Data.Data
 import qualified Data.HashMap.Strict as M
 import Data.IORef
@@ -23,8 +24,16 @@
 import GHC.IO
 import Unsafe.Coerce
 
+mkOnceIO :: IO a -> IO (IO a)
+mkOnceIO io = do
+  mv <- newEmptyMVar
+  demand <- newEmptyMVar
+  forkIO (takeMVar demand >> io >>= putMVar mv)
+  return (tryPutMVar demand () >> readMVar mv)
+
 termCacheCell :: IO (IORef (M.HashMap TypeRep Any))
-termCacheCell = unsafeDupablePerformIO $ once $ newIORef M.empty
+termCacheCell = unsafePerformIO $ mkOnceIO $ newIORef M.empty
+{-# NOINLINE termCacheCell #-}
 
 typeMemoizedCache :: forall a. (Interned a, Typeable a) => Cache a
 typeMemoizedCache = unsafeDupablePerformIO $ do
diff --git a/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/InternedCtors.hs b/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/InternedCtors.hs
--- a/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/InternedCtors.hs
+++ b/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/InternedCtors.hs
@@ -1,10 +1,13 @@
 {-# LANGUAGE BangPatterns #-}
 {-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE GADTs #-}
+{-# LANGUAGE QuantifiedConstraints #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
 
 -- |
 -- Module      :   Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors
@@ -42,6 +45,8 @@
     complementBitsTerm,
     shiftBitsTerm,
     rotateBitsTerm,
+    bvToSignedTerm,
+    bvToUnsignedTerm,
     bvconcatTerm,
     bvselectTerm,
     bvextendTerm,
@@ -163,11 +168,11 @@
 andTerm l r = internTerm $ UAndTerm l r
 {-# INLINE andTerm #-}
 
-eqvTerm :: SupportedPrim a => Term a -> Term a -> Term Bool
+eqvTerm :: (SupportedPrim a) => Term a -> Term a -> Term Bool
 eqvTerm l r = internTerm $ UEqvTerm l r
 {-# INLINE eqvTerm #-}
 
-iteTerm :: SupportedPrim a => Term Bool -> Term a -> Term a -> Term a
+iteTerm :: (SupportedPrim a) => Term Bool -> Term a -> Term a -> Term a
 iteTerm c l r = internTerm $ UITETerm c l r
 {-# INLINE iteTerm #-}
 
@@ -223,14 +228,41 @@
 rotateBitsTerm t n = internTerm $ URotateBitsTerm t n
 {-# INLINE rotateBitsTerm #-}
 
+bvToSignedTerm ::
+  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (ubv n),
+    forall n. (KnownNat n, 1 <= n) => SupportedPrim (sbv n),
+    Typeable ubv,
+    Typeable sbv,
+    KnownNat n,
+    1 <= n,
+    BVSignConversion (ubv n) (sbv n)
+  ) =>
+  Term (ubv n) ->
+  Term (sbv n)
+bvToSignedTerm = internTerm . UBVToSignedTerm
+
+bvToUnsignedTerm ::
+  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (ubv n),
+    forall n. (KnownNat n, 1 <= n) => SupportedPrim (sbv n),
+    Typeable ubv,
+    Typeable sbv,
+    KnownNat n,
+    1 <= n,
+    BVSignConversion (ubv n) (sbv n)
+  ) =>
+  Term (sbv n) ->
+  Term (ubv n)
+bvToUnsignedTerm = internTerm . UBVToUnsignedTerm
+
 bvconcatTerm ::
-  ( SupportedPrim (bv a),
-    SupportedPrim (bv b),
-    SupportedPrim (bv (a + b)),
+  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
+    Typeable bv,
     KnownNat a,
     KnownNat b,
+    KnownNat (a + b),
     1 <= a,
     1 <= b,
+    1 <= a + b,
     SizedBV bv
   ) =>
   Term (bv a) ->
@@ -240,9 +272,9 @@
 {-# INLINE bvconcatTerm #-}
 
 bvselectTerm ::
-  forall bv n ix w proxy.
-  ( SupportedPrim (bv n),
-    SupportedPrim (bv w),
+  forall bv n ix w p q.
+  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
+    Typeable bv,
     KnownNat n,
     KnownNat ix,
     KnownNat w,
@@ -251,8 +283,8 @@
     ix + w <= n,
     SizedBV bv
   ) =>
-  proxy ix ->
-  proxy w ->
+  p ix ->
+  q w ->
   Term (bv n) ->
   Term (bv w)
 bvselectTerm _ _ v = internTerm $ UBVSelectTerm (typeRep @ix) (typeRep @w) v
@@ -260,11 +292,12 @@
 
 bvextendTerm ::
   forall bv l r proxy.
-  ( SupportedPrim (bv l),
-    SupportedPrim (bv r),
+  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
+    Typeable bv,
     KnownNat l,
     KnownNat r,
     1 <= l,
+    1 <= r,
     l <= r,
     SizedBV bv
   ) =>
@@ -277,11 +310,12 @@
 
 bvsignExtendTerm ::
   forall bv l r proxy.
-  ( SupportedPrim (bv l),
-    SupportedPrim (bv r),
+  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
+    Typeable bv,
     KnownNat l,
     KnownNat r,
     1 <= l,
+    1 <= r,
     l <= r,
     SizedBV bv
   ) =>
@@ -293,11 +327,12 @@
 
 bvzeroExtendTerm ::
   forall bv l r proxy.
-  ( SupportedPrim (bv l),
-    SupportedPrim (bv r),
+  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
+    Typeable bv,
     KnownNat l,
     KnownNat r,
     1 <= l,
+    1 <= r,
     l <= r,
     SizedBV bv
   ) =>
diff --git a/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/InternedCtors.hs-boot b/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/InternedCtors.hs-boot
--- a/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/InternedCtors.hs-boot
+++ b/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/InternedCtors.hs-boot
@@ -1,7 +1,10 @@
 {-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE GADTs #-}
+{-# LANGUAGE QuantifiedConstraints #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
 
 module Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors
   ( constructUnary,
@@ -31,6 +34,8 @@
     complementBitsTerm,
     shiftBitsTerm,
     rotateBitsTerm,
+    bvToSignedTerm,
+    bvToUnsignedTerm,
     bvconcatTerm,
     bvselectTerm,
     bvextendTerm,
@@ -98,8 +103,8 @@
 notTerm :: Term Bool -> Term Bool
 orTerm :: Term Bool -> Term Bool -> Term Bool
 andTerm :: Term Bool -> Term Bool -> Term Bool
-eqvTerm :: SupportedPrim a => Term a -> Term a -> Term Bool
-iteTerm :: SupportedPrim a => Term Bool -> Term a -> Term a -> Term a
+eqvTerm :: (SupportedPrim a) => Term a -> Term a -> Term Bool
+iteTerm :: (SupportedPrim a) => Term Bool -> Term a -> Term a -> Term a
 addNumTerm :: (SupportedPrim a, Num a) => Term a -> Term a -> Term a
 uminusNumTerm :: (SupportedPrim a, Num a) => Term a -> Term a
 timesNumTerm :: (SupportedPrim a, Num a) => Term a -> Term a -> Term a
@@ -113,23 +118,46 @@
 complementBitsTerm :: (SupportedPrim a, Bits a) => Term a -> Term a
 shiftBitsTerm :: (SupportedPrim a, Bits a) => Term a -> Int -> Term a
 rotateBitsTerm :: (SupportedPrim a, Bits a) => Term a -> Int -> Term a
+bvToSignedTerm ::
+  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (ubv n),
+    forall n. (KnownNat n, 1 <= n) => SupportedPrim (sbv n),
+    Typeable ubv,
+    Typeable sbv,
+    KnownNat n,
+    1 <= n,
+    BVSignConversion (ubv n) (sbv n)
+  ) =>
+  Term (ubv n) ->
+  Term (sbv n)
+bvToUnsignedTerm ::
+  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (ubv n),
+    forall n. (KnownNat n, 1 <= n) => SupportedPrim (sbv n),
+    Typeable ubv,
+    Typeable sbv,
+    KnownNat n,
+    1 <= n,
+    BVSignConversion (ubv n) (sbv n)
+  ) =>
+  Term (sbv n) ->
+  Term (ubv n)
 bvconcatTerm ::
-  ( SupportedPrim (bv a),
-    SupportedPrim (bv b),
-    SupportedPrim (bv (a + b)),
+  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
+    Typeable bv,
     KnownNat a,
     KnownNat b,
+    KnownNat (a + b),
     1 <= a,
     1 <= b,
+    1 <= a + b,
     SizedBV bv
   ) =>
   Term (bv a) ->
   Term (bv b) ->
   Term (bv (a + b))
 bvselectTerm ::
-  forall bv n ix w proxy.
-  ( SupportedPrim (bv n),
-    SupportedPrim (bv w),
+  forall bv n ix w p q.
+  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
+    Typeable bv,
     KnownNat n,
     KnownNat ix,
     KnownNat w,
@@ -138,17 +166,18 @@
     ix + w <= n,
     SizedBV bv
   ) =>
-  proxy ix ->
-  proxy w ->
+  p ix ->
+  q w ->
   Term (bv n) ->
   Term (bv w)
 bvextendTerm ::
   forall bv l r proxy.
-  ( SupportedPrim (bv l),
-    SupportedPrim (bv r),
+  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
+    Typeable bv,
     KnownNat l,
     KnownNat r,
     1 <= l,
+    1 <= r,
     l <= r,
     SizedBV bv
   ) =>
@@ -158,11 +187,12 @@
   Term (bv r)
 bvsignExtendTerm ::
   forall bv l r proxy.
-  ( SupportedPrim (bv l),
-    SupportedPrim (bv r),
+  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
+    Typeable bv,
     KnownNat l,
     KnownNat r,
     1 <= l,
+    1 <= r,
     l <= r,
     SizedBV bv
   ) =>
@@ -171,11 +201,12 @@
   Term (bv r)
 bvzeroExtendTerm ::
   forall bv l r proxy.
-  ( SupportedPrim (bv l),
-    SupportedPrim (bv r),
+  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
+    Typeable bv,
     KnownNat l,
     KnownNat r,
     1 <= l,
+    1 <= r,
     l <= r,
     SizedBV bv
   ) =>
diff --git a/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/Term.hs b/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/Term.hs
--- a/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/Term.hs
+++ b/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/Term.hs
@@ -5,10 +5,12 @@
 {-# LANGUAGE DeriveAnyClass #-}
 {-# LANGUAGE DeriveGeneric #-}
 {-# LANGUAGE DeriveLift #-}
+{-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE FunctionalDependencies #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE QuantifiedConstraints #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TemplateHaskellQuotes #-}
@@ -78,8 +80,8 @@
 class (Lift t, Typeable t, Hashable t, Eq t, Show t, NFData t) => SupportedPrim t where
   type PrimConstraint t :: Constraint
   type PrimConstraint t = ()
-  default withPrim :: PrimConstraint t => proxy t -> (PrimConstraint t => a) -> a
-  withPrim :: proxy t -> (PrimConstraint t => a) -> a
+  default withPrim :: (PrimConstraint t) => proxy t -> ((PrimConstraint t) => a) -> a
+  withPrim :: proxy t -> ((PrimConstraint t) => a) -> a
   withPrim _ i = i
   termCache :: Cache (Term t)
   termCache = typeMemoizedCache
@@ -97,7 +99,7 @@
   type ConType sym
 
 -- | Type family to resolve the symbolic type associated with a concrete type.
-class SupportedPrim con => SymRep con where
+class (SupportedPrim con) => SymRep con where
   type SymType con
 
 -- | One-to-one mapping between symbolic types and concrete types.
@@ -163,8 +165,8 @@
 -- >>> "a" :: TypedSymbol Bool
 -- a :: Bool
 data TypedSymbol t where
-  SimpleSymbol :: SupportedPrim t => String -> TypedSymbol t
-  IndexedSymbol :: SupportedPrim t => String -> Int -> TypedSymbol t
+  SimpleSymbol :: (SupportedPrim t) => String -> TypedSymbol t
+  IndexedSymbol :: (SupportedPrim t) => String -> Int -> TypedSymbol t
   WithInfo ::
     forall t a.
     ( SupportedPrim t,
@@ -222,10 +224,10 @@
   rnf (IndexedSymbol str i) = rnf str `seq` rnf i
   rnf (WithInfo s info) = rnf s `seq` rnf info
 
-instance SupportedPrim t => IsString (TypedSymbol t) where
+instance (SupportedPrim t) => IsString (TypedSymbol t) where
   fromString = SimpleSymbol
 
-withSymbolSupported :: TypedSymbol t -> (SupportedPrim t => a) -> a
+withSymbolSupported :: TypedSymbol t -> ((SupportedPrim t) => a) -> a
 withSymbolSupported (SimpleSymbol _) a = a
 withSymbolSupported (IndexedSymbol _ _) a = a
 withSymbolSupported (WithInfo _ _) a = a
@@ -313,8 +315,8 @@
   NotTerm :: {-# UNPACK #-} !Id -> !(Term Bool) -> Term Bool
   OrTerm :: {-# UNPACK #-} !Id -> !(Term Bool) -> !(Term Bool) -> Term Bool
   AndTerm :: {-# UNPACK #-} !Id -> !(Term Bool) -> !(Term Bool) -> Term Bool
-  EqvTerm :: SupportedPrim t => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term Bool
-  ITETerm :: SupportedPrim t => {-# UNPACK #-} !Id -> !(Term Bool) -> !(Term t) -> !(Term t) -> Term t
+  EqvTerm :: (SupportedPrim t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term Bool
+  ITETerm :: (SupportedPrim t) => {-# UNPACK #-} !Id -> !(Term Bool) -> !(Term t) -> !(Term t) -> Term t
   AddNumTerm :: (SupportedPrim t, Num t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term t
   UMinusNumTerm :: (SupportedPrim t, Num t) => {-# UNPACK #-} !Id -> !(Term t) -> Term t
   TimesNumTerm :: (SupportedPrim t, Num t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term t
@@ -328,14 +330,39 @@
   ComplementBitsTerm :: (SupportedPrim t, Bits t) => {-# UNPACK #-} !Id -> !(Term t) -> Term t
   ShiftBitsTerm :: (SupportedPrim t, Bits t) => {-# UNPACK #-} !Id -> !(Term t) -> {-# UNPACK #-} !Int -> Term t
   RotateBitsTerm :: (SupportedPrim t, Bits t) => {-# UNPACK #-} !Id -> !(Term t) -> {-# UNPACK #-} !Int -> Term t
+  BVToSignedTerm ::
+    ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (ubv n),
+      forall n. (KnownNat n, 1 <= n) => SupportedPrim (sbv n),
+      Typeable ubv,
+      Typeable sbv,
+      KnownNat n,
+      1 <= n,
+      BVSignConversion (ubv n) (sbv n)
+    ) =>
+    {-# UNPACK #-} !Id ->
+    !(Term (ubv n)) ->
+    Term (sbv n)
+  BVToUnsignedTerm ::
+    ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (ubv n),
+      forall n. (KnownNat n, 1 <= n) => SupportedPrim (sbv n),
+      Typeable ubv,
+      Typeable sbv,
+      KnownNat n,
+      1 <= n,
+      BVSignConversion (ubv n) (sbv n)
+    ) =>
+    {-# UNPACK #-} !Id ->
+    !(Term (sbv n)) ->
+    Term (ubv n)
   BVConcatTerm ::
-    ( SupportedPrim (bv a),
-      SupportedPrim (bv b),
-      SupportedPrim (bv (a + b)),
+    ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
+      Typeable bv,
       KnownNat a,
       KnownNat b,
+      KnownNat (a + b),
       1 <= a,
       1 <= b,
+      1 <= a + b,
       SizedBV bv
     ) =>
     {-# UNPACK #-} !Id ->
@@ -343,8 +370,8 @@
     !(Term (bv b)) ->
     Term (bv (a + b))
   BVSelectTerm ::
-    ( SupportedPrim (bv n),
-      SupportedPrim (bv w),
+    ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
+      Typeable bv,
       KnownNat n,
       KnownNat ix,
       KnownNat w,
@@ -359,11 +386,12 @@
     !(Term (bv n)) ->
     Term (bv w)
   BVExtendTerm ::
-    ( SupportedPrim (bv l),
-      SupportedPrim (bv r),
+    ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
+      Typeable bv,
       KnownNat l,
       KnownNat r,
       1 <= l,
+      1 <= r,
       l <= r,
       SizedBV bv
     ) =>
@@ -425,6 +453,8 @@
   liftTyped (ComplementBitsTerm _ arg) = [||complementBitsTerm arg||]
   liftTyped (ShiftBitsTerm _ arg n) = [||shiftBitsTerm arg n||]
   liftTyped (RotateBitsTerm _ arg n) = [||rotateBitsTerm arg n||]
+  liftTyped (BVToSignedTerm _ v) = [||bvToSignedTerm v||]
+  liftTyped (BVToUnsignedTerm _ v) = [||bvToUnsignedTerm v||]
   liftTyped (BVConcatTerm _ arg1 arg2) = [||bvconcatTerm arg1 arg2||]
   liftTyped (BVSelectTerm _ (_ :: TypeRep ix) (_ :: TypeRep w) arg) = [||bvselectTerm (Proxy @ix) (Proxy @w) arg||]
   liftTyped (BVExtendTerm _ signed (_ :: TypeRep n) arg) = [||bvextendTerm signed (Proxy @n) arg||]
@@ -499,6 +529,8 @@
   show (ComplementBitsTerm i arg) = "ComplementBits{id=" ++ show i ++ ", arg=" ++ show arg ++ "}"
   show (ShiftBitsTerm i arg n) = "ShiftBits{id=" ++ show i ++ ", arg=" ++ show arg ++ ", n=" ++ show n ++ "}"
   show (RotateBitsTerm i arg n) = "RotateBits{id=" ++ show i ++ ", arg=" ++ show arg ++ ", n=" ++ show n ++ "}"
+  show (BVToSignedTerm i arg) = "BVToSigned{id=" ++ show i ++ ", arg=" ++ show arg ++ "}"
+  show (BVToUnsignedTerm i arg) = "BVToUnsigned{id=" ++ show i ++ ", arg=" ++ show arg ++ "}"
   show (BVConcatTerm i arg1 arg2) = "BVConcat{id=" ++ show i ++ ", arg1=" ++ show arg1 ++ ", arg2=" ++ show arg2 ++ "}"
   show (BVSelectTerm i ix w arg) =
     "BVSelect{id=" ++ show i ++ ", ix=" ++ show ix ++ ", w=" ++ show w ++ ", arg=" ++ show arg ++ "}"
@@ -551,8 +583,8 @@
   UNotTerm :: !(Term Bool) -> UTerm Bool
   UOrTerm :: !(Term Bool) -> !(Term Bool) -> UTerm Bool
   UAndTerm :: !(Term Bool) -> !(Term Bool) -> UTerm Bool
-  UEqvTerm :: SupportedPrim t => !(Term t) -> !(Term t) -> UTerm Bool
-  UITETerm :: SupportedPrim t => !(Term Bool) -> !(Term t) -> !(Term t) -> UTerm t
+  UEqvTerm :: (SupportedPrim t) => !(Term t) -> !(Term t) -> UTerm Bool
+  UITETerm :: (SupportedPrim t) => !(Term Bool) -> !(Term t) -> !(Term t) -> UTerm t
   UAddNumTerm :: (SupportedPrim t, Num t) => !(Term t) -> !(Term t) -> UTerm t
   UUMinusNumTerm :: (SupportedPrim t, Num t) => !(Term t) -> UTerm t
   UTimesNumTerm :: (SupportedPrim t, Num t) => !(Term t) -> !(Term t) -> UTerm t
@@ -566,22 +598,45 @@
   UComplementBitsTerm :: (SupportedPrim t, Bits t) => !(Term t) -> UTerm t
   UShiftBitsTerm :: (SupportedPrim t, Bits t) => !(Term t) -> {-# UNPACK #-} !Int -> UTerm t
   URotateBitsTerm :: (SupportedPrim t, Bits t) => !(Term t) -> {-# UNPACK #-} !Int -> UTerm t
+  UBVToSignedTerm ::
+    ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (ubv n),
+      forall n. (KnownNat n, 1 <= n) => SupportedPrim (sbv n),
+      Typeable ubv,
+      Typeable sbv,
+      KnownNat n,
+      1 <= n,
+      BVSignConversion (ubv n) (sbv n)
+    ) =>
+    !(Term (ubv n)) ->
+    UTerm (sbv n)
+  UBVToUnsignedTerm ::
+    ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (ubv n),
+      forall n. (KnownNat n, 1 <= n) => SupportedPrim (sbv n),
+      Typeable ubv,
+      Typeable sbv,
+      KnownNat n,
+      1 <= n,
+      BVSignConversion (ubv n) (sbv n)
+    ) =>
+    !(Term (sbv n)) ->
+    UTerm (ubv n)
   UBVConcatTerm ::
-    ( SupportedPrim (bv a),
-      SupportedPrim (bv b),
-      SupportedPrim (bv (a + b)),
+    ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
+      Typeable bv,
       KnownNat a,
       KnownNat b,
+      KnownNat (a + b),
       1 <= a,
       1 <= b,
+      1 <= a + b,
       SizedBV bv
     ) =>
     !(Term (bv a)) ->
     !(Term (bv b)) ->
     UTerm (bv (a + b))
   UBVSelectTerm ::
-    ( SupportedPrim (bv n),
-      SupportedPrim (bv w),
+    ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
+      Typeable bv,
       KnownNat n,
       KnownNat ix,
       KnownNat w,
@@ -595,11 +650,12 @@
     !(Term (bv n)) ->
     UTerm (bv w)
   UBVExtendTerm ::
-    ( SupportedPrim (bv l),
-      SupportedPrim (bv r),
+    ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
+      Typeable bv,
       KnownNat l,
       KnownNat r,
       1 <= l,
+      1 <= r,
       l <= r,
       SizedBV bv
     ) =>
@@ -634,7 +690,7 @@
 eqTypedId (a, i1) (b, i2) = i1 == i2 && eqTypeRepBool a b
 {-# INLINE eqTypedId #-}
 
-eqHeteroTag :: Eq a => (TypeRep a, a) -> (TypeRep b, b) -> Bool
+eqHeteroTag :: (Eq a) => (TypeRep a, a) -> (TypeRep b, b) -> Bool
 eqHeteroTag (tpa, taga) (tpb, tagb) = eqHeteroRep tpa tpb taga tagb
 {-# INLINE eqHeteroTag #-}
 
@@ -680,6 +736,14 @@
     DShiftBitsTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Int -> Description (Term t)
     DRotateBitsTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Int -> Description (Term t)
     DBVConcatTerm :: TypeRep bv1 -> TypeRep bv2 -> {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term t)
+    DBVToSignedTerm ::
+      forall ubv sbv (n :: Nat).
+      !(TypeRep (ubv n), Id) ->
+      Description (Term (sbv n))
+    DBVToUnsignedTerm ::
+      forall sbv ubv (n :: Nat).
+      !(TypeRep (sbv n), Id) ->
+      Description (Term (ubv n))
     DBVSelectTerm ::
       forall bv (n :: Nat) (w :: Nat) (ix :: Nat).
       !(TypeRep ix) ->
@@ -738,6 +802,8 @@
   describe (UComplementBitsTerm arg) = DComplementBitsTerm (identity arg)
   describe (UShiftBitsTerm arg n) = DShiftBitsTerm (identity arg) n
   describe (URotateBitsTerm arg n) = DRotateBitsTerm (identity arg) n
+  describe (UBVToSignedTerm (arg :: Term bv)) = DBVToSignedTerm (typeRep :: TypeRep bv, identity arg)
+  describe (UBVToUnsignedTerm (arg :: Term bv)) = DBVToSignedTerm (typeRep :: TypeRep bv, identity arg)
   describe (UBVConcatTerm (arg1 :: bv1) (arg2 :: bv2)) =
     DBVConcatTerm (typeRep :: TypeRep bv1) (typeRep :: TypeRep bv2) (identity arg1) (identity arg2)
   describe (UBVSelectTerm (ix :: TypeRep ix) _ (arg :: Term arg)) =
@@ -782,6 +848,8 @@
       go (UComplementBitsTerm arg) = ComplementBitsTerm i arg
       go (UShiftBitsTerm arg n) = ShiftBitsTerm i arg n
       go (URotateBitsTerm arg n) = RotateBitsTerm i arg n
+      go (UBVToSignedTerm arg) = BVToSignedTerm i arg
+      go (UBVToUnsignedTerm arg) = BVToUnsignedTerm i arg
       go (UBVConcatTerm arg1 arg2) = BVConcatTerm i arg1 arg2
       go (UBVSelectTerm ix w arg) = BVSelectTerm i ix w arg
       go (UBVExtendTerm signed n arg) = BVExtendTerm i signed n arg
@@ -823,6 +891,8 @@
   DComplementBitsTerm li == DComplementBitsTerm ri = li == ri
   DShiftBitsTerm li ln == DShiftBitsTerm ri rn = li == ri && ln == rn
   DRotateBitsTerm li ln == DRotateBitsTerm ri rn = li == ri && ln == rn
+  DBVToSignedTerm li == DBVToSignedTerm ri = eqTypedId li ri
+  DBVToUnsignedTerm li == DBVToUnsignedTerm ri = eqTypedId li ri
   DBVConcatTerm lrep1 lrep2 li1 li2 == DBVConcatTerm rrep1 rrep2 ri1 ri2 =
     eqTypeRepBool lrep1 rrep1 && eqTypeRepBool lrep2 rrep2 && li1 == ri1 && li2 == ri2
   DBVSelectTerm lix li == DBVSelectTerm rix ri =
@@ -881,25 +951,27 @@
   hashWithSalt s (DComplementBitsTerm id1) = s `hashWithSalt` (20 :: Int) `hashWithSalt` id1
   hashWithSalt s (DShiftBitsTerm id1 n) = s `hashWithSalt` (21 :: Int) `hashWithSalt` id1 `hashWithSalt` n
   hashWithSalt s (DRotateBitsTerm id1 n) = s `hashWithSalt` (22 :: Int) `hashWithSalt` id1 `hashWithSalt` n
+  hashWithSalt s (DBVToSignedTerm id) = s `hashWithSalt` (23 :: Int) `hashWithSalt` id
+  hashWithSalt s (DBVToUnsignedTerm id) = s `hashWithSalt` (24 :: Int) `hashWithSalt` id
   hashWithSalt s (DBVConcatTerm rep1 rep2 id1 id2) =
-    s `hashWithSalt` (23 :: Int) `hashWithSalt` rep1 `hashWithSalt` rep2 `hashWithSalt` id1 `hashWithSalt` id2
-  hashWithSalt s (DBVSelectTerm ix id1) = s `hashWithSalt` (24 :: Int) `hashWithSalt` ix `hashWithSalt` id1
+    s `hashWithSalt` (25 :: Int) `hashWithSalt` rep1 `hashWithSalt` rep2 `hashWithSalt` id1 `hashWithSalt` id2
+  hashWithSalt s (DBVSelectTerm ix id1) = s `hashWithSalt` (26 :: Int) `hashWithSalt` ix `hashWithSalt` id1
   hashWithSalt s (DBVExtendTerm signed n id1) =
     s
-      `hashWithSalt` (25 :: Int)
+      `hashWithSalt` (27 :: Int)
       `hashWithSalt` signed
       `hashWithSalt` n
       `hashWithSalt` id1
-  hashWithSalt s (DTabularFunApplyTerm id1 id2) = s `hashWithSalt` (26 :: Int) `hashWithSalt` id1 `hashWithSalt` id2
-  hashWithSalt s (DGeneralFunApplyTerm id1 id2) = s `hashWithSalt` (27 :: Int) `hashWithSalt` id1 `hashWithSalt` id2
-  hashWithSalt s (DDivIntegralTerm id1 id2) = s `hashWithSalt` (28 :: Int) `hashWithSalt` id1 `hashWithSalt` id2
-  hashWithSalt s (DModIntegralTerm id1 id2) = s `hashWithSalt` (29 :: Int) `hashWithSalt` id1 `hashWithSalt` id2
-  hashWithSalt s (DQuotIntegralTerm id1 id2) = s `hashWithSalt` (30 :: Int) `hashWithSalt` id1 `hashWithSalt` id2
-  hashWithSalt s (DRemIntegralTerm id1 id2) = s `hashWithSalt` (31 :: Int) `hashWithSalt` id1 `hashWithSalt` id2
-  hashWithSalt s (DDivBoundedIntegralTerm id1 id2) = s `hashWithSalt` (32 :: Int) `hashWithSalt` id1 `hashWithSalt` id2
-  hashWithSalt s (DModBoundedIntegralTerm id1 id2) = s `hashWithSalt` (33 :: Int) `hashWithSalt` id1 `hashWithSalt` id2
-  hashWithSalt s (DQuotBoundedIntegralTerm id1 id2) = s `hashWithSalt` (34 :: Int) `hashWithSalt` id1 `hashWithSalt` id2
-  hashWithSalt s (DRemBoundedIntegralTerm id1 id2) = s `hashWithSalt` (35 :: Int) `hashWithSalt` id1 `hashWithSalt` id2
+  hashWithSalt s (DTabularFunApplyTerm id1 id2) = s `hashWithSalt` (28 :: Int) `hashWithSalt` id1 `hashWithSalt` id2
+  hashWithSalt s (DGeneralFunApplyTerm id1 id2) = s `hashWithSalt` (29 :: Int) `hashWithSalt` id1 `hashWithSalt` id2
+  hashWithSalt s (DDivIntegralTerm id1 id2) = s `hashWithSalt` (30 :: Int) `hashWithSalt` id1 `hashWithSalt` id2
+  hashWithSalt s (DModIntegralTerm id1 id2) = s `hashWithSalt` (31 :: Int) `hashWithSalt` id1 `hashWithSalt` id2
+  hashWithSalt s (DQuotIntegralTerm id1 id2) = s `hashWithSalt` (32 :: Int) `hashWithSalt` id1 `hashWithSalt` id2
+  hashWithSalt s (DRemIntegralTerm id1 id2) = s `hashWithSalt` (33 :: Int) `hashWithSalt` id1 `hashWithSalt` id2
+  hashWithSalt s (DDivBoundedIntegralTerm id1 id2) = s `hashWithSalt` (34 :: Int) `hashWithSalt` id1 `hashWithSalt` id2
+  hashWithSalt s (DModBoundedIntegralTerm id1 id2) = s `hashWithSalt` (35 :: Int) `hashWithSalt` id1 `hashWithSalt` id2
+  hashWithSalt s (DQuotBoundedIntegralTerm id1 id2) = s `hashWithSalt` (36 :: Int) `hashWithSalt` id1 `hashWithSalt` id2
+  hashWithSalt s (DRemBoundedIntegralTerm id1 id2) = s `hashWithSalt` (37 :: Int) `hashWithSalt` id1 `hashWithSalt` id2
 
 -- Basic Bool
 defaultValueForBool :: Bool
diff --git a/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/Term.hs-boot b/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/Term.hs-boot
--- a/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/Term.hs-boot
+++ b/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/Term.hs-boot
@@ -1,12 +1,15 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE DefaultSignatures #-}
+{-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FunctionalDependencies #-}
 {-# LANGUAGE GADTs #-}
+{-# LANGUAGE QuantifiedConstraints #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
 
 module Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
   ( SupportedPrim (..),
@@ -41,8 +44,8 @@
 class (Lift t, Typeable t, Hashable t, Eq t, Show t, NFData t) => SupportedPrim t where
   type PrimConstraint t :: Constraint
   type PrimConstraint t = ()
-  default withPrim :: PrimConstraint t => proxy t -> (PrimConstraint t => a) -> a
-  withPrim :: proxy t -> (PrimConstraint t => a) -> a
+  default withPrim :: (PrimConstraint t) => proxy t -> ((PrimConstraint t) => a) -> a
+  withPrim :: proxy t -> ((PrimConstraint t) => a) -> a
   withPrim _ i = i
   termCache :: Cache (Term t)
   termCache = typeMemoizedCache
@@ -58,7 +61,7 @@
 class ConRep sym where
   type ConType sym
 
-class SupportedPrim con => SymRep con where
+class (SupportedPrim con) => SymRep con where
   type SymType con
 
 class
@@ -114,8 +117,8 @@
   pformatTernary :: tag -> Term arg1 -> Term arg2 -> Term arg3 -> String
 
 data TypedSymbol t where
-  SimpleSymbol :: SupportedPrim t => String -> TypedSymbol t
-  IndexedSymbol :: SupportedPrim t => String -> Int -> TypedSymbol t
+  SimpleSymbol :: (SupportedPrim t) => String -> TypedSymbol t
+  IndexedSymbol :: (SupportedPrim t) => String -> Int -> TypedSymbol t
   WithInfo ::
     forall t a.
     ( SupportedPrim t,
@@ -160,8 +163,8 @@
   NotTerm :: {-# UNPACK #-} !Id -> !(Term Bool) -> Term Bool
   OrTerm :: {-# UNPACK #-} !Id -> !(Term Bool) -> !(Term Bool) -> Term Bool
   AndTerm :: {-# UNPACK #-} !Id -> !(Term Bool) -> !(Term Bool) -> Term Bool
-  EqvTerm :: SupportedPrim t => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term Bool
-  ITETerm :: SupportedPrim t => {-# UNPACK #-} !Id -> !(Term Bool) -> !(Term t) -> !(Term t) -> Term t
+  EqvTerm :: (SupportedPrim t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term Bool
+  ITETerm :: (SupportedPrim t) => {-# UNPACK #-} !Id -> !(Term Bool) -> !(Term t) -> !(Term t) -> Term t
   AddNumTerm :: (SupportedPrim t, Num t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term t
   UMinusNumTerm :: (SupportedPrim t, Num t) => {-# UNPACK #-} !Id -> !(Term t) -> Term t
   TimesNumTerm :: (SupportedPrim t, Num t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term t
@@ -175,14 +178,39 @@
   ComplementBitsTerm :: (SupportedPrim t, Bits t) => {-# UNPACK #-} !Id -> !(Term t) -> Term t
   ShiftBitsTerm :: (SupportedPrim t, Bits t) => {-# UNPACK #-} !Id -> !(Term t) -> {-# UNPACK #-} !Int -> Term t
   RotateBitsTerm :: (SupportedPrim t, Bits t) => {-# UNPACK #-} !Id -> !(Term t) -> {-# UNPACK #-} !Int -> Term t
+  BVToSignedTerm ::
+    ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (ubv n),
+      forall n. (KnownNat n, 1 <= n) => SupportedPrim (sbv n),
+      Typeable ubv,
+      Typeable sbv,
+      KnownNat n,
+      1 <= n,
+      BVSignConversion (ubv n) (sbv n)
+    ) =>
+    {-# UNPACK #-} !Id ->
+    !(Term (ubv n)) ->
+    Term (sbv n)
+  BVToUnsignedTerm ::
+    ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (ubv n),
+      forall n. (KnownNat n, 1 <= n) => SupportedPrim (sbv n),
+      Typeable ubv,
+      Typeable sbv,
+      KnownNat n,
+      1 <= n,
+      BVSignConversion (ubv n) (sbv n)
+    ) =>
+    {-# UNPACK #-} !Id ->
+    !(Term (sbv n)) ->
+    Term (ubv n)
   BVConcatTerm ::
-    ( SupportedPrim (bv a),
-      SupportedPrim (bv b),
-      SupportedPrim (bv (a + b)),
+    ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
+      Typeable bv,
       KnownNat a,
       KnownNat b,
+      KnownNat (a + b),
       1 <= a,
       1 <= b,
+      1 <= (a + b),
       SizedBV bv
     ) =>
     {-# UNPACK #-} !Id ->
@@ -190,8 +218,8 @@
     !(Term (bv b)) ->
     Term (bv (a + b))
   BVSelectTerm ::
-    ( SupportedPrim (bv n),
-      SupportedPrim (bv w),
+    ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
+      Typeable bv,
       KnownNat n,
       KnownNat ix,
       KnownNat w,
@@ -206,11 +234,12 @@
     !(Term (bv n)) ->
     Term (bv w)
   BVExtendTerm ::
-    ( SupportedPrim (bv l),
-      SupportedPrim (bv r),
+    ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
+      Typeable bv,
       KnownNat l,
       KnownNat r,
       1 <= l,
+      1 <= r,
       l <= r,
       SizedBV bv
     ) =>
@@ -264,8 +293,8 @@
   UNotTerm :: !(Term Bool) -> UTerm Bool
   UOrTerm :: !(Term Bool) -> !(Term Bool) -> UTerm Bool
   UAndTerm :: !(Term Bool) -> !(Term Bool) -> UTerm Bool
-  UEqvTerm :: SupportedPrim t => !(Term t) -> !(Term t) -> UTerm Bool
-  UITETerm :: SupportedPrim t => !(Term Bool) -> !(Term t) -> !(Term t) -> UTerm t
+  UEqvTerm :: (SupportedPrim t) => !(Term t) -> !(Term t) -> UTerm Bool
+  UITETerm :: (SupportedPrim t) => !(Term Bool) -> !(Term t) -> !(Term t) -> UTerm t
   UAddNumTerm :: (SupportedPrim t, Num t) => !(Term t) -> !(Term t) -> UTerm t
   UUMinusNumTerm :: (SupportedPrim t, Num t) => !(Term t) -> UTerm t
   UTimesNumTerm :: (SupportedPrim t, Num t) => !(Term t) -> !(Term t) -> UTerm t
@@ -279,22 +308,45 @@
   UComplementBitsTerm :: (SupportedPrim t, Bits t) => !(Term t) -> UTerm t
   UShiftBitsTerm :: (SupportedPrim t, Bits t) => !(Term t) -> {-# UNPACK #-} !Int -> UTerm t
   URotateBitsTerm :: (SupportedPrim t, Bits t) => !(Term t) -> {-# UNPACK #-} !Int -> UTerm t
+  UBVToSignedTerm ::
+    ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (ubv n),
+      forall n. (KnownNat n, 1 <= n) => SupportedPrim (sbv n),
+      Typeable ubv,
+      Typeable sbv,
+      KnownNat n,
+      1 <= n,
+      BVSignConversion (ubv n) (sbv n)
+    ) =>
+    !(Term (ubv n)) ->
+    UTerm (sbv n)
+  UBVToUnsignedTerm ::
+    ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (ubv n),
+      forall n. (KnownNat n, 1 <= n) => SupportedPrim (sbv n),
+      Typeable ubv,
+      Typeable sbv,
+      KnownNat n,
+      1 <= n,
+      BVSignConversion (ubv n) (sbv n)
+    ) =>
+    !(Term (sbv n)) ->
+    UTerm (ubv n)
   UBVConcatTerm ::
-    ( SupportedPrim (bv a),
-      SupportedPrim (bv b),
-      SupportedPrim (bv (a + b)),
+    ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
+      Typeable bv,
       KnownNat a,
       KnownNat b,
+      KnownNat (a + b),
       1 <= a,
       1 <= b,
+      1 <= a + b,
       SizedBV bv
     ) =>
     !(Term (bv a)) ->
     !(Term (bv b)) ->
     UTerm (bv (a + b))
   UBVSelectTerm ::
-    ( SupportedPrim (bv n),
-      SupportedPrim (bv w),
+    ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
+      Typeable bv,
       KnownNat n,
       KnownNat ix,
       KnownNat w,
@@ -308,11 +360,12 @@
     !(Term (bv n)) ->
     UTerm (bv w)
   UBVExtendTerm ::
-    ( SupportedPrim (bv l),
-      SupportedPrim (bv r),
+    ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
+      Typeable bv,
       KnownNat l,
       KnownNat r,
       1 <= l,
+      1 <= r,
       l <= r,
       SizedBV bv
     ) =>
diff --git a/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/TermSubstitution.hs b/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/TermSubstitution.hs
--- a/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/TermSubstitution.hs
+++ b/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/TermSubstitution.hs
@@ -69,6 +69,8 @@
         ComplementBitsTerm _ op -> SomeTerm $ pevalComplementBitsTerm (gov op)
         ShiftBitsTerm _ op n -> SomeTerm $ pevalShiftBitsTerm (gov op) n
         RotateBitsTerm _ op n -> SomeTerm $ pevalRotateBitsTerm (gov op) n
+        BVToSignedTerm _ op -> SomeTerm $ pevalBVToSignedTerm op
+        BVToUnsignedTerm _ op -> SomeTerm $ pevalBVToUnsignedTerm op
         BVConcatTerm _ op1 op2 -> SomeTerm $ pevalBVConcatTerm (gov op1) (gov op2)
         BVSelectTerm _ ix w op -> SomeTerm $ pevalBVSelectTerm ix w (gov op)
         BVExtendTerm _ n signed op -> SomeTerm $ pevalBVExtendTerm n signed (gov op)
diff --git a/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/TermUtils.hs b/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/TermUtils.hs
--- a/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/TermUtils.hs
+++ b/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/TermUtils.hs
@@ -64,6 +64,8 @@
 identityWithTypeRep (ComplementBitsTerm i _) = (typeRep (Proxy @t), i)
 identityWithTypeRep (ShiftBitsTerm i _ _) = (typeRep (Proxy @t), i)
 identityWithTypeRep (RotateBitsTerm i _ _) = (typeRep (Proxy @t), i)
+identityWithTypeRep (BVToSignedTerm i _) = (typeRep (Proxy @t), i)
+identityWithTypeRep (BVToUnsignedTerm i _) = (typeRep (Proxy @t), i)
 identityWithTypeRep (BVConcatTerm i _ _) = (typeRep (Proxy @t), i)
 identityWithTypeRep (BVSelectTerm i _ _ _) = (typeRep (Proxy @t), i)
 identityWithTypeRep (BVExtendTerm i _ _ _) = (typeRep (Proxy @t), i)
@@ -103,6 +105,8 @@
 introSupportedPrimConstraint ComplementBitsTerm {} x = x
 introSupportedPrimConstraint ShiftBitsTerm {} x = x
 introSupportedPrimConstraint RotateBitsTerm {} x = x
+introSupportedPrimConstraint BVToSignedTerm {} x = x
+introSupportedPrimConstraint BVToUnsignedTerm {} x = x
 introSupportedPrimConstraint BVConcatTerm {} x = x
 introSupportedPrimConstraint BVSelectTerm {} x = x
 introSupportedPrimConstraint BVExtendTerm {} x = x
@@ -155,6 +159,8 @@
     go (SomeTerm (ComplementBitsTerm _ arg)) = goUnary arg
     go (SomeTerm (ShiftBitsTerm _ arg _)) = goUnary arg
     go (SomeTerm (RotateBitsTerm _ arg _)) = goUnary arg
+    go (SomeTerm (BVToSignedTerm _ arg)) = goUnary arg
+    go (SomeTerm (BVToUnsignedTerm _ arg)) = goUnary arg
     go (SomeTerm (BVConcatTerm _ arg1 arg2)) = goBinary arg1 arg2
     go (SomeTerm (BVSelectTerm _ _ _ arg)) = goUnary arg
     go (SomeTerm (BVExtendTerm _ _ _ arg)) = goUnary arg
@@ -208,6 +214,8 @@
 castTerm t@ComplementBitsTerm {} = cast t
 castTerm t@ShiftBitsTerm {} = cast t
 castTerm t@RotateBitsTerm {} = cast t
+castTerm t@BVToSignedTerm {} = cast t
+castTerm t@BVToUnsignedTerm {} = cast t
 castTerm t@BVConcatTerm {} = cast t
 castTerm t@BVSelectTerm {} = cast t
 castTerm t@BVExtendTerm {} = cast t
@@ -247,6 +255,8 @@
 pformat (ComplementBitsTerm _ arg) = "(~ " ++ pformat arg ++ ")"
 pformat (ShiftBitsTerm _ arg n) = "(shift " ++ pformat arg ++ " " ++ show n ++ ")"
 pformat (RotateBitsTerm _ arg n) = "(rotate " ++ pformat arg ++ " " ++ show n ++ ")"
+pformat (BVToSignedTerm _ arg) = "(bvu2s " ++ pformat arg ++ " " ++ ")"
+pformat (BVToUnsignedTerm _ arg) = "(bvs2u " ++ pformat arg ++ " " ++ ")"
 pformat (BVConcatTerm _ arg1 arg2) = "(bvconcat " ++ pformat arg1 ++ " " ++ pformat arg2 ++ ")"
 pformat (BVSelectTerm _ ix w arg) = "(bvselect " ++ show ix ++ " " ++ show w ++ " " ++ pformat arg ++ ")"
 pformat (BVExtendTerm _ signed n arg) =
@@ -294,6 +304,8 @@
     go t@(ComplementBitsTerm _ arg) = goUnary t arg
     go t@(ShiftBitsTerm _ arg _) = goUnary t arg
     go t@(RotateBitsTerm _ arg _) = goUnary t arg
+    go t@(BVToSignedTerm _ arg) = goUnary t arg
+    go t@(BVToUnsignedTerm _ arg) = goUnary t arg
     go t@(BVConcatTerm _ arg1 arg2) = goBinary t arg1 arg2
     go t@(BVSelectTerm _ _ _ arg) = goUnary t arg
     go t@(BVExtendTerm _ _ _ arg) = goUnary t arg
diff --git a/src/Grisette/IR/SymPrim/Data/Prim/Model.hs b/src/Grisette/IR/SymPrim/Data/Prim/Model.hs
--- a/src/Grisette/IR/SymPrim/Data/Prim/Model.hs
+++ b/src/Grisette/IR/SymPrim/Data/Prim/Model.hs
@@ -332,6 +332,10 @@
       goUnary (`pevalShiftBitsTerm` n) arg
     go (SomeTerm (RotateBitsTerm _ arg n)) =
       goUnary (`pevalRotateBitsTerm` n) arg
+    go (SomeTerm (BVToSignedTerm _ arg)) =
+      goUnary pevalBVToSignedTerm arg
+    go (SomeTerm (BVToUnsignedTerm _ arg)) =
+      goUnary pevalBVToUnsignedTerm arg
     go (SomeTerm (BVConcatTerm _ arg1 arg2)) =
       goBinary pevalBVConcatTerm arg1 arg2
     go (SomeTerm (BVSelectTerm _ ix w arg)) =
diff --git a/src/Grisette/IR/SymPrim/Data/Prim/PartialEval/BV.hs b/src/Grisette/IR/SymPrim/Data/Prim/PartialEval/BV.hs
--- a/src/Grisette/IR/SymPrim/Data/Prim/PartialEval/BV.hs
+++ b/src/Grisette/IR/SymPrim/Data/Prim/PartialEval/BV.hs
@@ -4,6 +4,7 @@
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE QuantifiedConstraints #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeOperators #-}
@@ -18,7 +19,9 @@
 -- Stability   :   Experimental
 -- Portability :   GHC only
 module Grisette.IR.SymPrim.Data.Prim.PartialEval.BV
-  ( pevalBVConcatTerm,
+  ( pevalBVToSignedTerm,
+    pevalBVToUnsignedTerm,
+    pevalBVConcatTerm,
     pevalBVSelectTerm,
     pevalBVExtendTerm,
     pevalBVZeroExtendTerm,
@@ -26,17 +29,91 @@
   )
 where
 
+import Data.Typeable
 import GHC.TypeNats
 import Grisette.Core.Data.Class.BitVector
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors
 import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
+import Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermUtils
 import Grisette.IR.SymPrim.Data.Prim.PartialEval.Unfold
 
+-- ToSigned
+pevalBVToSignedTerm ::
+  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (ubv n),
+    forall n. (KnownNat n, 1 <= n) => SupportedPrim (sbv n),
+    Typeable ubv,
+    Typeable sbv,
+    KnownNat n,
+    1 <= n,
+    BVSignConversion (ubv n) (sbv n)
+  ) =>
+  Term (ubv n) ->
+  Term (sbv n)
+pevalBVToSignedTerm = unaryUnfoldOnce doPevalBVToSignedTerm bvToSignedTerm
+
+doPevalBVToSignedTerm ::
+  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (ubv n),
+    forall n. (KnownNat n, 1 <= n) => SupportedPrim (sbv n),
+    Typeable ubv,
+    Typeable sbv,
+    KnownNat n,
+    1 <= n,
+    BVSignConversion (ubv n) (sbv n)
+  ) =>
+  Term (ubv n) ->
+  Maybe (Term (sbv n))
+doPevalBVToSignedTerm (ConTerm _ b) = Just $ conTerm $ toSigned b
+doPevalBVToSignedTerm (BVToUnsignedTerm _ b) = Just b >>= castTerm
+doPevalBVToSignedTerm _ = Nothing
+
+-- ToUnsigned
+{-
+bvToUnsignedTerm ::
+  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (sbv n),
+    forall n. (KnownNat n, 1 <= n) => SupportedPrim (ubv n),
+    Typeable sbv,
+    Typeable ubv,
+    KnownNat n,
+    1 <= n,
+    BVToUnsigned (sbv n) (ubv n)
+  ) =>
+  Term (sbv n) ->
+  Term (ubv n)
+bvToUnsignedTerm = internTerm . UBVToUnsignedTerm
+-}
+pevalBVToUnsignedTerm ::
+  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (ubv n),
+    forall n. (KnownNat n, 1 <= n) => SupportedPrim (sbv n),
+    Typeable ubv,
+    Typeable sbv,
+    KnownNat n,
+    1 <= n,
+    BVSignConversion (ubv n) (sbv n)
+  ) =>
+  Term (sbv n) ->
+  Term (ubv n)
+pevalBVToUnsignedTerm = unaryUnfoldOnce doPevalBVToUnsignedTerm bvToUnsignedTerm
+
+doPevalBVToUnsignedTerm ::
+  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (ubv n),
+    forall n. (KnownNat n, 1 <= n) => SupportedPrim (sbv n),
+    Typeable ubv,
+    Typeable sbv,
+    KnownNat n,
+    1 <= n,
+    BVSignConversion (ubv n) (sbv n)
+  ) =>
+  Term (sbv n) ->
+  Maybe (Term (ubv n))
+doPevalBVToUnsignedTerm (ConTerm _ b) = Just $ conTerm $ toUnsigned b
+doPevalBVToUnsignedTerm (BVToSignedTerm _ b) = Just b >>= castTerm
+doPevalBVToUnsignedTerm _ = Nothing
+
 -- select
 pevalBVSelectTerm ::
-  forall bv n ix w proxy.
-  ( SupportedPrim (bv n),
-    SupportedPrim (bv w),
+  forall bv n ix w p q.
+  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
+    Typeable bv,
     KnownNat n,
     KnownNat ix,
     KnownNat w,
@@ -45,16 +122,16 @@
     ix + w <= n,
     SizedBV bv
   ) =>
-  proxy ix ->
-  proxy w ->
+  p ix ->
+  q w ->
   Term (bv n) ->
   Term (bv w)
 pevalBVSelectTerm ix w = unaryUnfoldOnce (doPevalBVSelectTerm ix w) (bvselectTerm ix w)
 
 doPevalBVSelectTerm ::
-  forall bv n ix w proxy.
-  ( SupportedPrim (bv n),
-    SupportedPrim (bv w),
+  forall bv n ix w p q.
+  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
+    Typeable bv,
     KnownNat n,
     KnownNat ix,
     KnownNat w,
@@ -63,8 +140,8 @@
     ix + w <= n,
     SizedBV bv
   ) =>
-  proxy ix ->
-  proxy w ->
+  p ix ->
+  q w ->
   Term (bv n) ->
   Maybe (Term (bv w))
 doPevalBVSelectTerm ix w (ConTerm _ b) = Just $ conTerm $ sizedBVSelect ix w b
@@ -73,12 +150,13 @@
 -- ext
 pevalBVZeroExtendTerm ::
   forall proxy l r bv.
-  ( KnownNat l,
+  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
+    Typeable bv,
+    KnownNat l,
     KnownNat r,
     1 <= l,
+    1 <= r,
     l <= r,
-    SupportedPrim (bv l),
-    SupportedPrim (bv r),
     SizedBV bv
   ) =>
   proxy r ->
@@ -88,12 +166,13 @@
 
 pevalBVSignExtendTerm ::
   forall proxy l r bv.
-  ( KnownNat l,
+  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
+    Typeable bv,
+    KnownNat l,
     KnownNat r,
     1 <= l,
+    1 <= r,
     l <= r,
-    SupportedPrim (bv l),
-    SupportedPrim (bv r),
     SizedBV bv
   ) =>
   proxy r ->
@@ -103,12 +182,13 @@
 
 pevalBVExtendTerm ::
   forall proxy l r bv.
-  ( KnownNat l,
+  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
+    Typeable bv,
+    KnownNat l,
     KnownNat r,
     1 <= l,
+    1 <= r,
     l <= r,
-    SupportedPrim (bv l),
-    SupportedPrim (bv r),
     SizedBV bv
   ) =>
   Bool ->
@@ -119,12 +199,13 @@
 
 doPevalBVExtendTerm ::
   forall proxy l r bv.
-  ( KnownNat l,
+  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
+    Typeable bv,
+    KnownNat l,
     KnownNat r,
     1 <= l,
+    1 <= r,
     l <= r,
-    SupportedPrim (bv l),
-    SupportedPrim (bv r),
     SizedBV bv
   ) =>
   Bool ->
@@ -135,13 +216,14 @@
 doPevalBVExtendTerm _ _ _ = Nothing
 
 pevalBVConcatTerm ::
-  ( SupportedPrim (bv a),
-    SupportedPrim (bv b),
-    SupportedPrim (bv (a + b)),
+  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
+    Typeable bv,
     KnownNat a,
     KnownNat b,
+    KnownNat (a + b),
     1 <= a,
     1 <= b,
+    1 <= a + b,
     SizedBV bv
   ) =>
   Term (bv a) ->
@@ -150,13 +232,14 @@
 pevalBVConcatTerm = binaryUnfoldOnce doPevalBVConcatTerm bvconcatTerm
 
 doPevalBVConcatTerm ::
-  ( SupportedPrim (bv a),
-    SupportedPrim (bv b),
-    SupportedPrim (bv (a + b)),
+  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
+    Typeable bv,
     KnownNat a,
     KnownNat b,
+    KnownNat (a + b),
     1 <= a,
     1 <= b,
+    1 <= (a + b),
     SizedBV bv
   ) =>
   Term (bv a) ->
diff --git a/src/Grisette/IR/SymPrim/Data/Prim/Utils.hs b/src/Grisette/IR/SymPrim/Data/Prim/Utils.hs
--- a/src/Grisette/IR/SymPrim/Data/Prim/Utils.hs
+++ b/src/Grisette/IR/SymPrim/Data/Prim/Utils.hs
@@ -44,7 +44,7 @@
 eqHetero = cmpHetero (==)
 {-# INLINE eqHetero #-}
 
-eqHeteroRep :: forall a b. Eq a => TypeRep a -> TypeRep b -> a -> b -> Bool
+eqHeteroRep :: forall a b. (Eq a) => TypeRep a -> TypeRep b -> a -> b -> Bool
 eqHeteroRep ta tb = cmpHeteroRep ta tb (==)
 {-# INLINE eqHeteroRep #-}
 
diff --git a/src/Grisette/IR/SymPrim/Data/SymPrim.hs b/src/Grisette/IR/SymPrim/Data/SymPrim.hs
--- a/src/Grisette/IR/SymPrim/Data/SymPrim.hs
+++ b/src/Grisette/IR/SymPrim/Data/SymPrim.hs
@@ -309,7 +309,7 @@
 -- >>> :set -XOverloadedStrings -XDataKinds -XBinaryLiterals
 -- >>> (SomeSymIntN ("a" :: SymIntN 5)) + (SomeSymIntN (5 :: SymIntN 5))
 -- (+ 0b00101 a)
--- >>> someBVConcat (SomeSymIntN (con 0b101 :: SymIntN 3)) (SomeSymIntN (con 0b110 :: SymIntN 3))
+-- >>> bvConcat (SomeSymIntN (con 0b101 :: SymIntN 3)) (SomeSymIntN (con 0b110 :: SymIntN 3))
 -- 0b101110
 --
 -- More symbolic operations are available. Please refer to the documentation
@@ -421,7 +421,7 @@
 -- >>> :set -XOverloadedStrings -XDataKinds -XBinaryLiterals
 -- >>> (SomeSymWordN ("a" :: SymWordN 5)) + (SomeSymWordN (5 :: SymWordN 5))
 -- (+ 0b00101 a)
--- >>> someBVConcat (SomeSymWordN (con 0b101 :: SymWordN 3)) (SomeSymWordN (con 0b110 :: SymWordN 3))
+-- >>> bvConcat (SomeSymWordN (con 0b101 :: SymWordN 3)) (SomeSymWordN (con 0b110 :: SymWordN 3))
 -- 0b101110
 --
 -- More symbolic operations are available. Please refer to the documentation
@@ -656,19 +656,31 @@
 #define BITS_BV(symtype, signed) \
 instance (KnownNat n, 1 <= n) => Bits (symtype n) where \
   symtype l .&. symtype r = symtype $ pevalAndBitsTerm l r; \
+  {-# INLINE (.&.) #-}; \
   symtype l .|. symtype r = symtype $ pevalOrBitsTerm l r; \
+  {-# INLINE (.|.) #-}; \
   symtype l `xor` symtype r = symtype $ pevalXorBitsTerm l r; \
+  {-# INLINE xor #-}; \
   complement (symtype n) = symtype $ pevalComplementBitsTerm n; \
+  {-# INLINE complement #-}; \
   shift (symtype n) i = symtype $ pevalShiftBitsTerm n i; \
+  {-# INLINE shift #-}; \
   rotate (symtype n) i = symtype $ pevalRotateBitsTerm n i; \
-  bitSize _ = fromIntegral $ natVal (Proxy @n); \
-  bitSizeMaybe _ = Just $ fromIntegral $ natVal (Proxy @n); \
+  {-# INLINE rotate #-}; \
+  bitSize = finiteBitSize; \
+  {-# INLINE bitSize #-}; \
+  bitSizeMaybe = Just . finiteBitSize; \
+  {-# INLINE bitSizeMaybe #-}; \
   isSigned _ = signed; \
+  {-# INLINE isSigned #-}; \
   testBit (Con n) =  testBit n; \
   testBit _ = error "You cannot call testBit on symbolic variables"; \
+  {-# INLINE testBit #-}; \
   bit = con . bit; \
+  {-# INLINE bit #-}; \
   popCount (Con n) = popCount n; \
-  popCount _ = error "You cannot call popCount on symbolic variables"
+  popCount _ = error "You cannot call popCount on symbolic variables"; \
+  {-# INLINE popCount #-}
 
 #define BITS_BV_SOME(somety, origty, br1, uf, ur1) \
 instance Bits somety where \
@@ -696,9 +708,9 @@
   {-# INLINE complementBit #-}; \
   testBit s i = uf (`testBit` i) "testBit" s; \
   {-# INLINE testBit #-}; \
-  bitSizeMaybe (somety (n :: origty n)) = Just $ fromIntegral $ natVal n; \
+  bitSizeMaybe = Just . finiteBitSize; \
   {-# INLINE bitSizeMaybe #-}; \
-  bitSize (somety (n :: origty n)) = fromIntegral $ natVal n; \
+  bitSize = finiteBitSize; \
   {-# INLINE bitSize #-}; \
   isSigned _ = False; \
   {-# INLINE isSigned #-}; \
@@ -724,6 +736,25 @@
 BITS_BV_SOME(SomeSymWordN, SymWordN, binSomeSymWordNR1, unarySomeSymWordN, unarySomeSymWordNR1)
 #endif
 
+-- FiniteBits
+
+#define FINITE_BITS_BV(symtype) \
+instance (KnownNat n, 1 <= n) => FiniteBits (symtype n) where \
+  finiteBitSize _ = fromIntegral $ natVal (Proxy @n); \
+  {-# INLINE finiteBitSize #-}; \
+
+#define FINITE_BITS_BV_SOME(somety, origty) \
+instance FiniteBits somety where \
+  finiteBitSize (somety (n :: origty n)) = fromIntegral $ natVal n; \
+  {-# INLINE finiteBitSize #-}
+
+#if 1
+FINITE_BITS_BV(SymIntN)
+FINITE_BITS_BV(SymWordN)
+FINITE_BITS_BV_SOME(SomeSymIntN, SymIntN)
+FINITE_BITS_BV_SOME(SomeSymWordN, SymWordN)
+#endif
+
 -- Show
 
 #define SHOW_SIMPLE(symtype) \
@@ -1105,11 +1136,17 @@
 instance (KnownNat n, 1 <= n) => SEq (symtype n) where \
   (symtype l) ==~ (symtype r) = SymBool $ pevalEqvTerm l r
 
-#define SEQ_BV_SOME(somety, bf) \
+#define SEQ_BV_SOME(somety, origty) \
 instance SEq somety where \
-  (==~) = bf (==~) "==~"; \
+  somety (l :: origty l) ==~ somety (r :: origty r) = \
+    (case sameNat (Proxy @l) (Proxy @r) of \
+      Just Refl -> l ==~ r; \
+      Nothing -> con False); \
   {-# INLINE (==~) #-}; \
-  (/=~) = bf (/=~) "/=~"; \
+  somety (l :: origty l) /=~ somety (r :: origty r) = \
+    (case sameNat (Proxy @l) (Proxy @r) of \
+      Just Refl -> l /=~ r; \
+      Nothing -> con True); \
   {-# INLINE (/=~) #-}
 
 #if 1
@@ -1117,8 +1154,8 @@
 SEQ_SIMPLE(SymInteger)
 SEQ_BV(SymIntN)
 SEQ_BV(SymWordN)
-SEQ_BV_SOME(SomeSymIntN, binSomeSymIntN)
-SEQ_BV_SOME(SomeSymWordN, binSomeSymWordN)
+SEQ_BV_SOME(SomeSymIntN, SymIntN)
+SEQ_BV_SOME(SomeSymWordN, SymWordN)
 #endif
 
 -- SOrd
@@ -1231,8 +1268,8 @@
     LeqProof -> symtype $ pevalBVExtendTerm True (Proxy @r) v
 
 #define BVSELECT_SIZED(symtype) \
-sizedBVSelect :: forall n ix w proxy. (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, ix + w <= n) => \
-  proxy ix -> proxy w -> symtype n -> symtype w; \
+sizedBVSelect :: forall n ix w p q. (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, ix + w <= n) => \
+  p ix -> q w -> symtype n -> symtype w; \
 sizedBVSelect pix pw (symtype v) = symtype $ pevalBVSelectTerm pix pw v
 
 #if 1
@@ -1254,49 +1291,86 @@
 -- BV
 
 #define BVCONCAT(somety, origty) \
-someBVConcat (somety (a :: origty l)) (somety (b :: origty r)) = \
+bvConcat (somety (a :: origty l)) (somety (b :: origty r)) = \
   case (leqAddPos (Proxy @l) (Proxy @r), knownAdd @l @r KnownProof KnownProof) of \
     (LeqProof, KnownProof) -> \
       somety $ sizedBVConcat a b
 
 #define BVZEXT(somety, origty) \
-someBVZext (p :: p l) (somety (a :: origty n)) \
-  | natVal p < natVal (Proxy @n) = error "zextBV: trying to zero extend a value to a smaller size" \
-  | otherwise = \
-    case (unsafeLeqProof @1 @l, unsafeLeqProof @n @l) of \
-      (LeqProof, LeqProof) -> somety $ sizedBVZext p a
+bvZext l (somety (a :: origty n)) \
+  | l < n = error "bvZext: trying to zero extend a value to a smaller size" \
+  | otherwise = res (Proxy @n) \
+  where \
+    n = fromIntegral $ natVal (Proxy @n); \
+    res :: forall (l :: Nat). Proxy l -> somety; \
+    res p = \
+      case (unsafeKnownProof @l (fromIntegral l), unsafeLeqProof @1 @l, unsafeLeqProof @n @l) of \
+        (KnownProof, LeqProof, LeqProof) -> somety $ sizedBVZext p a
 
 #define BVSEXT(somety, origty) \
-someBVSext (p :: p l) (somety (a :: origty n)) \
-  | natVal p < natVal (Proxy @n) = error "zextBV: trying to zero extend a value to a smaller size" \
-  | otherwise = \
-    case (unsafeLeqProof @1 @l, unsafeLeqProof @n @l) of \
-      (LeqProof, LeqProof) -> somety $ sizedBVSext p a
+bvSext l (somety (a :: origty n)) \
+  | l < n = error "bvZext: trying to zero extend a value to a smaller size" \
+  | otherwise = res (Proxy @n) \
+  where \
+    n = fromIntegral $ natVal (Proxy @n); \
+    res :: forall (l :: Nat). Proxy l -> somety; \
+    res p = \
+      case (unsafeKnownProof @l (fromIntegral l), unsafeLeqProof @1 @l, unsafeLeqProof @n @l) of \
+        (KnownProof, LeqProof, LeqProof) -> somety $ sizedBVSext p a
 
 #define BVSELECT(somety, origty) \
-someBVSelect (p :: p ix) (q :: q w) (somety (a :: origty n)) \
-  | natVal p + natVal q > natVal (Proxy @n) = error "selectBV: trying to select a bitvector outside the bounds of the input" \
-  | natVal q == 0 = error "selectBV: trying to select a bitvector of size 0" \
-  | otherwise = \
-    case (unsafeLeqProof @1 @w, unsafeLeqProof @(ix + w) @n) of \
-      (LeqProof, LeqProof) -> somety $ sizedBVSelect (Proxy @ix) (Proxy @w) a
+bvSelect ix w (somety (a :: origty n)) \
+    | ix + w > n = error "bvSelect: trying to select a bitvector outside the bounds of the input" \
+    | w == 0 = error "bvSelect: trying to select a bitvector of size 0" \
+    | otherwise = res (Proxy @n) (Proxy @n) \
+    where \
+      n = fromIntegral $ natVal (Proxy @n); \
+      res :: forall (w :: Nat) (ix :: Nat). Proxy w -> Proxy ix -> somety; \
+      res p1 p2 = \
+        case ( unsafeKnownProof @ix (fromIntegral ix), \
+               unsafeKnownProof @w (fromIntegral w), \
+               unsafeLeqProof @1 @w, \
+               unsafeLeqProof @(ix + w) @n \
+             ) of \
+          (KnownProof, KnownProof, LeqProof, LeqProof) -> \
+            somety $ sizedBVSelect (Proxy @ix) (Proxy @w) a
 
 #if 1
-instance SomeBV SomeSymIntN where
+instance BV SomeSymIntN where
   BVCONCAT(SomeSymIntN, SymIntN)
+  {-# INLINE bvConcat #-}
   BVZEXT(SomeSymIntN, SymIntN)
+  {-# INLINE bvZext #-}
   BVSEXT(SomeSymIntN, SymIntN)
-  someBVExt = someBVSext
+  {-# INLINE bvSext #-}
+  bvExt = bvSext
+  {-# INLINE bvExt #-}
   BVSELECT(SomeSymIntN, SymIntN)
+  {-# INLINE bvSelect #-}
 
-instance SomeBV SomeSymWordN where
+instance BV SomeSymWordN where
   BVCONCAT(SomeSymWordN, SymWordN)
+  {-# INLINE bvConcat #-}
   BVZEXT(SomeSymWordN, SymWordN)
+  {-# INLINE bvZext #-}
   BVSEXT(SomeSymWordN, SymWordN)
-  someBVExt = someBVZext
+  {-# INLINE bvSext #-}
+  bvExt = bvZext
+  {-# INLINE bvExt #-}
   BVSELECT(SomeSymWordN, SymWordN)
+  {-# INLINE bvSelect #-}
 #endif
 
+-- BVSignConversion
+
+instance (KnownNat n, 1 <= n) => BVSignConversion (SymWordN n) (SymIntN n) where
+  toSigned (SymWordN n) = SymIntN $ pevalBVToSignedTerm n
+  toUnsigned (SymIntN n) = SymWordN $ pevalBVToUnsignedTerm n
+
+instance BVSignConversion SomeSymWordN SomeSymIntN where
+  toSigned (SomeSymWordN n) = SomeSymIntN $ toSigned n
+  toUnsigned (SomeSymIntN n) = SomeSymWordN $ toUnsigned n
+
 -- ModelRep
 
 -- | A pair of a symbolic constant and its value.
@@ -1305,7 +1379,7 @@
 -- >>> buildModel ("a" := (1 :: Integer), "b" := True) :: Model
 -- Model {a -> 1 :: Integer, b -> True :: Bool}
 data ModelSymPair ct st where
-  (:=) :: LinkedRep ct st => st -> ct -> ModelSymPair ct st
+  (:=) :: (LinkedRep ct st) => st -> ct -> ModelSymPair ct st
 
 instance ModelRep (ModelSymPair ct st) Model where
   buildModel (sym := val) =
@@ -1318,7 +1392,7 @@
 --
 -- >>> symsSize [1, "a" :: SymInteger, "a" + 1 :: SymInteger]
 -- 3
-symsSize :: forall con sym. LinkedRep con sym => [sym] -> Int
+symsSize :: forall con sym. (LinkedRep con sym) => [sym] -> Int
 symsSize = termsSize . fmap (underlyingTerm @con)
 {-# INLINE symsSize #-}
 
@@ -1333,7 +1407,7 @@
 -- 3
 -- >>> symSize (("a" + 1) * ("a" + 1) :: SymInteger)
 -- 4
-symSize :: forall con sym. LinkedRep con sym => sym -> Int
+symSize :: forall con sym. (LinkedRep con sym) => sym -> Int
 symSize = termSize . underlyingTerm @con
 {-# INLINE symSize #-}
 
@@ -1375,7 +1449,7 @@
 --
 -- >>> allSymsSize ("a" :: SymInteger, "a" + "b" :: SymInteger, ("a" + "b") * "c" :: SymInteger)
 -- 5
-allSymsSize :: AllSyms a => a -> Int
+allSymsSize :: (AllSyms a) => a -> Int
 allSymsSize = someSymsSize . allSyms
 
 class AllSyms' a where
@@ -1387,10 +1461,10 @@
 instance AllSyms' U1 where
   allSymsS' _ = id
 
-instance AllSyms c => AllSyms' (K1 i c) where
+instance (AllSyms c) => AllSyms' (K1 i c) where
   allSymsS' (K1 v) = allSymsS v
 
-instance AllSyms' a => AllSyms' (M1 i c a) where
+instance (AllSyms' a) => AllSyms' (M1 i c a) where
   allSymsS' (M1 v) = allSymsS' v
 
 instance (AllSyms' a, AllSyms' b) => AllSyms' (a :+: b) where
@@ -1580,11 +1654,11 @@
   allSymsS (WriterStrict.WriterT v) = allSymsS v
 
 -- Identity
-instance AllSyms a => AllSyms (Identity a) where
+instance (AllSyms a) => AllSyms (Identity a) where
   allSymsS (Identity a) = allSymsS a
 
 -- IdentityT
-instance AllSyms (m a) => AllSyms (IdentityT m a) where
+instance (AllSyms (m a)) => AllSyms (IdentityT m a) where
   allSymsS (IdentityT a) = allSymsS a
 
 -- VerificationConditions
diff --git a/src/Grisette/Lib/Control/Monad/Trans/Cont.hs b/src/Grisette/Lib/Control/Monad/Trans/Cont.hs
--- a/src/Grisette/Lib/Control/Monad/Trans/Cont.hs
+++ b/src/Grisette/Lib/Control/Monad/Trans/Cont.hs
@@ -17,6 +17,7 @@
 where
 
 import Control.Monad.Cont
+import Control.Monad.Trans.Class
 import Grisette.Core.Data.Class.Bool
 import Grisette.Core.Data.Class.Mergeable
 import Grisette.Core.Data.Class.SimpleMergeable
@@ -33,6 +34,6 @@
 {-# INLINE mrgEvalContT #-}
 
 -- | 'Control.Monad.Cont.resetT' with 'MergingStrategy' knowledge propagation
-mrgResetT :: (UnionLike m, Mergeable r, Monad m) => Monad m => ContT r m r -> ContT r' m r
+mrgResetT :: (UnionLike m, Mergeable r, Monad m) => (Monad m) => ContT r m r -> ContT r' m r
 mrgResetT = lift . mrgEvalContT
 {-# INLINE mrgResetT #-}
diff --git a/src/Grisette/Utils/Parameterized.hs b/src/Grisette/Utils/Parameterized.hs
--- a/src/Grisette/Utils/Parameterized.hs
+++ b/src/Grisette/Utils/Parameterized.hs
@@ -117,11 +117,11 @@
 
 -- | Construct a runtime representation of a type-level natural number when its
 -- runtime value is known.
-natRepr :: forall n. KnownNat n => NatRepr n
+natRepr :: forall n. (KnownNat n) => NatRepr n
 natRepr = NatRepr (natVal (Proxy @n))
 
 -- | Decrement a 'NatRepr' by 1.
-decNat :: 1 <= n => NatRepr n -> NatRepr (n - 1)
+decNat :: (1 <= n) => NatRepr n -> NatRepr (n - 1)
 decNat (NatRepr n) = NatRepr (n - 1)
 
 -- | Predecessor of a 'NatRepr'
@@ -137,11 +137,11 @@
 addNat (NatRepr m) (NatRepr n) = NatRepr (m + n)
 
 -- | Subtraction of two 'NatRepr's.
-subNat :: n <= m => NatRepr m -> NatRepr n -> NatRepr (m - n)
+subNat :: (n <= m) => NatRepr m -> NatRepr n -> NatRepr (m - n)
 subNat (NatRepr m) (NatRepr n) = NatRepr (m - n)
 
 -- | Division of two 'NatRepr's.
-divNat :: 1 <= n => NatRepr m -> NatRepr n -> NatRepr (Div m n)
+divNat :: (1 <= n) => NatRepr m -> NatRepr n -> NatRepr (Div m n)
 divNat (NatRepr m) (NatRepr n) = NatRepr (m `div` n)
 
 -- | Half of a 'NatRepr'.
@@ -151,10 +151,10 @@
 -- | @'KnownProof n'@ is a type whose values are only inhabited when @n@ has
 -- a known runtime value.
 data KnownProof (n :: Nat) where
-  KnownProof :: KnownNat n => KnownProof n
+  KnownProof :: (KnownNat n) => KnownProof n
 
 -- | Introduces the 'KnownNat' constraint when it's proven.
-withKnownProof :: KnownProof n -> (KnownNat n => r) -> r
+withKnownProof :: KnownProof n -> ((KnownNat n) => r) -> r
 withKnownProof p r = case p of KnownProof -> r
 
 -- | Construct a 'KnownProof' given the runtime value.
@@ -181,10 +181,10 @@
 
 -- | @'LeqProof m n'@ is a type whose values are only inhabited when @m <= n@.
 data LeqProof (m :: Nat) (n :: Nat) where
-  LeqProof :: m <= n => LeqProof m n
+  LeqProof :: (m <= n) => LeqProof m n
 
 -- | Introduces the @m <= n@ constraint when it's proven.
-withLeqProof :: LeqProof m n -> (m <= n => r) -> r
+withLeqProof :: LeqProof m n -> ((m <= n) => r) -> r
 withLeqProof p r = case p of LeqProof -> r
 
 -- | Construct a 'LeqProof'.
diff --git a/test/Grisette/Backend/SBV/Data/SMT/LoweringTests.hs b/test/Grisette/Backend/SBV/Data/SMT/LoweringTests.hs
--- a/test/Grisette/Backend/SBV/Data/SMT/LoweringTests.hs
+++ b/test/Grisette/Backend/SBV/Data/SMT/LoweringTests.hs
@@ -572,7 +572,10 @@
                 testBinaryOpLowering @(IntN 5) @(IntN 5) @(IntN 5) boundedConfig quotBoundedIntegralTerm "quot" SBV.sQuot,
               testCase "Rem - bounded" $ do
                 testBinaryOpLowering @(IntN 5) @(IntN 5) @(IntN 5) unboundedConfig remBoundedIntegralTerm "rem" SBV.sRem
-                testBinaryOpLowering @(IntN 5) @(IntN 5) @(IntN 5) boundedConfig remBoundedIntegralTerm "rem" SBV.sRem
+                testBinaryOpLowering @(IntN 5) @(IntN 5) @(IntN 5) boundedConfig remBoundedIntegralTerm "rem" SBV.sRem,
+              testCase "ToUnsigned" $ do
+                testUnaryOpLowering @(IntN 5) @(WordN 5) unboundedConfig bvToUnsignedTerm "toUnsigned" SBV.sFromIntegral
+                testUnaryOpLowering @(IntN 5) @(WordN 5) boundedConfig bvToUnsignedTerm "toUnsigned" SBV.sFromIntegral
             ],
           testGroup
             "WordN"
@@ -773,6 +776,9 @@
                 testBinaryOpLowering @(WordN 5) @(WordN 5) @(WordN 5) boundedConfig quotIntegralTerm "quot" SBV.sQuot,
               testCase "Rem" $ do
                 testBinaryOpLowering @(WordN 5) @(WordN 5) @(WordN 5) unboundedConfig remIntegralTerm "rem" SBV.sRem
-                testBinaryOpLowering @(WordN 5) @(WordN 5) @(WordN 5) boundedConfig remIntegralTerm "rem" SBV.sRem
+                testBinaryOpLowering @(WordN 5) @(WordN 5) @(WordN 5) boundedConfig remIntegralTerm "rem" SBV.sRem,
+              testCase "ToSigned" $ do
+                testUnaryOpLowering @(WordN 5) @(IntN 5) unboundedConfig bvToSignedTerm "toSigned" SBV.sFromIntegral
+                testUnaryOpLowering @(WordN 5) @(IntN 5) boundedConfig bvToSignedTerm "toSigned" SBV.sFromIntegral
             ]
         ]
diff --git a/test/Grisette/Backend/SBV/Data/SMT/TermRewritingGen.hs b/test/Grisette/Backend/SBV/Data/SMT/TermRewritingGen.hs
--- a/test/Grisette/Backend/SBV/Data/SMT/TermRewritingGen.hs
+++ b/test/Grisette/Backend/SBV/Data/SMT/TermRewritingGen.hs
@@ -5,6 +5,7 @@
 {-# LANGUAGE FunctionalDependencies #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE QuantifiedConstraints #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
@@ -186,10 +187,14 @@
   ( TermRewritingSpec a (bv an),
     TermRewritingSpec b (bv bn),
     TermRewritingSpec c (bv (an + bn)),
+    forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
+    Typeable bv,
     KnownNat an,
     KnownNat bn,
+    KnownNat (an + bn),
     1 <= an,
     1 <= bn,
+    1 <= an + bn,
     SizedBV bv
   ) =>
   a ->
@@ -200,6 +205,8 @@
 bvselectSpec ::
   ( TermRewritingSpec a (bv an),
     TermRewritingSpec b (bv bn),
+    forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
+    Typeable bv,
     KnownNat an,
     KnownNat ix,
     KnownNat bn,
@@ -218,9 +225,12 @@
 bvextendSpec ::
   ( TermRewritingSpec a (bv an),
     TermRewritingSpec b (bv bn),
+    forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
+    Typeable bv,
     KnownNat an,
     KnownNat bn,
     1 <= an,
+    1 <= bn,
     an <= bn,
     SizedBV bv
   ) =>
@@ -470,7 +480,8 @@
 
 dsbv1 ::
   forall proxy bv.
-  ( SupportedBV bv 1,
+  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
+    SupportedBV bv 1,
     SupportedBV bv 2,
     SupportedBV bv 3,
     SupportedBV bv 4,
@@ -521,7 +532,8 @@
 
 dsbv2 ::
   forall proxy bv.
-  ( SupportedBV bv 1,
+  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
+    SupportedBV bv 1,
     SupportedBV bv 2,
     SupportedBV bv 3,
     SupportedBV bv 4,
@@ -572,7 +584,8 @@
 
 dsbv3 ::
   forall proxy bv.
-  ( SupportedBV bv 1,
+  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
+    SupportedBV bv 1,
     SupportedBV bv 2,
     SupportedBV bv 3,
     SupportedBV bv 4,
@@ -622,7 +635,8 @@
 
 dsbv4 ::
   forall proxy bv.
-  ( SupportedBV bv 1,
+  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
+    SupportedBV bv 1,
     SupportedBV bv 2,
     SupportedBV bv 3,
     SupportedBV bv 4,
@@ -673,7 +687,8 @@
 dsbv4 _ _ = error "Should never be called"
 
 instance
-  ( SupportedBV bv 1,
+  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
+    SupportedBV bv 1,
     SupportedBV bv 2,
     SupportedBV bv 3,
     SupportedBV bv 4,
diff --git a/test/Grisette/Core/Data/BVTests.hs b/test/Grisette/Core/Data/BVTests.hs
--- a/test/Grisette/Core/Data/BVTests.hs
+++ b/test/Grisette/Core/Data/BVTests.hs
@@ -37,19 +37,19 @@
   Property
 binaryConform a2b c2d f2e f g x y = ioProperty $ f x y @=? f2e (g (a2b x) (c2d y))
 
-wordUnaryConform :: HasCallStack => (WordN 8 -> WordN 8) -> (Word8 -> Word8) -> Word8 -> Assertion
+wordUnaryConform :: (HasCallStack) => (WordN 8 -> WordN 8) -> (Word8 -> Word8) -> Word8 -> Assertion
 wordUnaryConform f g x = unWordN (f (fromIntegral x)) @=? toInteger (g x)
 
-wordUnaryNonNegIntConform :: HasCallStack => (Int -> WordN 8) -> (Int -> Word8) -> Int -> Assertion
+wordUnaryNonNegIntConform :: (HasCallStack) => (Int -> WordN 8) -> (Int -> Word8) -> Int -> Assertion
 wordUnaryNonNegIntConform f g y = when (y >= 0) $ unWordN (f y) @=? toInteger (g y)
 
-wordBinIntConform :: HasCallStack => (WordN 8 -> Int -> WordN 8) -> (Word8 -> Int -> Word8) -> Word8 -> Int -> Assertion
+wordBinIntConform :: (HasCallStack) => (WordN 8 -> Int -> WordN 8) -> (Word8 -> Int -> Word8) -> Word8 -> Int -> Assertion
 wordBinIntConform f g x y = unWordN (f (fromIntegral x) y) @=? toInteger (g x y)
 
-wordBinNonNegIntConform :: HasCallStack => (WordN 8 -> Int -> WordN 8) -> (Word8 -> Int -> Word8) -> Word8 -> Int -> Assertion
+wordBinNonNegIntConform :: (HasCallStack) => (WordN 8 -> Int -> WordN 8) -> (Word8 -> Int -> Word8) -> Word8 -> Int -> Assertion
 wordBinNonNegIntConform f g x y = when (y >= 0) $ unWordN (f (fromIntegral x) y) @=? toInteger (g x y)
 
-wordBinConform :: HasCallStack => (WordN 8 -> WordN 8 -> WordN 8) -> (Word8 -> Word8 -> Word8) -> Word8 -> Word8 -> Assertion
+wordBinConform :: (HasCallStack) => (WordN 8 -> WordN 8 -> WordN 8) -> (Word8 -> Word8 -> Word8) -> Word8 -> Word8 -> Assertion
 wordBinConform f g x y = unWordN (f (fromIntegral x) (fromIntegral y)) @=? toInteger (g x y)
 
 intN8eqint8 :: IntN 8 -> Int8 -> Assertion
@@ -102,7 +102,7 @@
       testCase "maxBound" $ (maxBound :: typ) @=? fromIntegral (maxBound :: ref)
     ]
 
-shouldThrow :: NFData a => String -> a -> IO ()
+shouldThrow :: (NFData a) => String -> a -> IO ()
 shouldThrow name x = do
   errored <- catch (evaluate $ x `deepseq` True) (\(_ :: SomeException) -> return False)
   when errored $ assertFailure $ name ++ " should throw an exception"