diff --git a/Data/SBV.hs b/Data/SBV.hs
index fe6a4a38..92625070 100644
--- a/Data/SBV.hs
+++ b/Data/SBV.hs
@@ -145,13 +145,15 @@
 -- get in touch if there is a solver you'd like to see included.
 -----------------------------------------------------------------------------
 
-{-# LANGUAGE DataKinds            #-}
-{-# LANGUAGE FlexibleContexts     #-}
-{-# LANGUAGE FlexibleInstances    #-}
-{-# LANGUAGE ScopedTypeVariables  #-}
-{-# LANGUAGE TypeApplications     #-}
-{-# LANGUAGE TypeFamilies         #-}
-{-# LANGUAGE TypeOperators        #-}
+{-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE DefaultSignatures     #-}
+{-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+{-# LANGUAGE TypeApplications      #-}
+{-# LANGUAGE TypeFamilies          #-}
+{-# LANGUAGE TypeOperators         #-}
 
 {-# OPTIONS_GHC -Wall -Werror #-}
 
@@ -421,6 +423,9 @@ module Data.SBV (
   , isConcrete, isSymbolic, isConcretely, mkSymVal
   , MonadSymbolic(..), Symbolic, SymbolicT, label, output, runSMT, runSMTWith
 
+  -- * Queriable values
+  , Queriable(..), freshVar, freshVar_, getValue
+
   -- * Module exports
   -- $moduleExportIntro
 
@@ -430,7 +435,8 @@ module Data.SBV (
   , module Data.Ratio
   ) where
 
-import Control.Monad (when)
+import Control.Monad       (when)
+import Control.Monad.Trans (MonadIO)
 
 import Data.SBV.Core.AlgReals
 import Data.SBV.Core.Data       hiding (free, free_, mkFreeVars,
@@ -488,11 +494,14 @@ import Data.Ratio
 import Data.Word
 
 import Data.SBV.SMT.Utils (SBVException(..))
+
 import Data.SBV.Control.Types (SMTReasonUnknown(..), Logic(..))
+import Data.SBV.Control.Utils (getValue, freshVar, freshVar_)
 
 import qualified Data.SBV.Utils.CrackNum as CN
 
 import Data.Proxy (Proxy(..))
+import Data.Kind  (Type)
 import GHC.TypeLits (KnownNat, type (<=), type (+), type (-))
 
 import Prelude hiding((+), (-)) -- to avoid the haddock ambiguity
@@ -1752,4 +1761,34 @@ optIndependentWith config p = do
      _                   -> error $ "An independent optimization call resulted in a bad result:"
                                   ++ "\n" ++ show res
 
+-- | An queriable value: Mapping between concrete/symbolic values. If your type is traversable and simply embeds
+-- symbolic equivalents for one type, then you can simply define 'create'. (Which is the most common case.)
+class Queriable m a where
+  type QueryResult a :: Type
+
+  -- | ^ Create a new symbolic value of type @a@
+  create  :: QueryT m a
+
+  -- | ^ Extract the current value in a SAT context
+  project :: a -> QueryT m (QueryResult a)
+
+  -- | ^ Create a literal value. Morally, 'embed' and 'project' are inverses of each other
+  -- via the 'QueryT' monad transformer.
+  embed   :: QueryResult a -> QueryT m a
+
+  default project :: (a ~ t (SBV e), QueryResult a ~ t e, Traversable t, MonadIO m, SymVal e) => a -> QueryT m (QueryResult a)
+  project = mapM getValue
+
+  default embed :: (a ~ t (SBV e), QueryResult a ~ t e, Traversable t, MonadIO m, SymVal e) => QueryResult a -> QueryT m a
+  embed = pure . fmap literal
+  {-# MINIMAL create #-}
+
+-- | Generic 'Queriable' instance for 'SymVal' values
+instance {-# OVERLAPPABLE #-} (MonadIO m, SymVal a) => Queriable m (SBV a) where
+  type QueryResult (SBV a) = a
+
+  create  = freshVar_
+  project = getValue
+  embed   = return . literal
+
 {- HLint ignore module "Use import/export shortcut" -}
diff --git a/Data/SBV/Control.hs b/Data/SBV/Control.hs
index 4f53b6e6..476acb6d 100644
--- a/Data/SBV/Control.hs
+++ b/Data/SBV/Control.hs
@@ -9,20 +9,13 @@
 -- Control sublanguage for interacting with SMT solvers.
 -----------------------------------------------------------------------------
 
-{-# LANGUAGE ConstraintKinds       #-}
-{-# LANGUAGE DefaultSignatures     #-}
-{-# LANGUAGE FlexibleInstances     #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE TypeFamilies          #-}
-{-# LANGUAGE TypeOperators         #-}
-
 {-# OPTIONS_GHC -Wall -Werror #-}
 
 module Data.SBV.Control (
      -- $queryIntro
 
      -- * User queries
-       ExtractIO(..), MonadQuery(..), Queriable(..), Query, query
+       ExtractIO(..), MonadQuery(..), Query, query
 
      -- * Create a fresh variable
      , freshVar_, freshVar
@@ -88,46 +81,10 @@ import Data.SBV.Control.Utils (registerUISMTFunction, registerSMTType)
 
 import qualified Data.SBV.Control.Utils as Trans
 
-import Data.SBV.Core.Data (SymVal, SBV, literal)
-
-import Control.Monad.Trans (MonadIO)
-import Data.Kind (Type)
-
-
 -- | Run a custom query
 query :: Query a -> Symbolic a
 query = Trans.executeQuery QueryExternal
 
--- | An queriable value: Mapping between concrete/symbolic values. If your type is traversable and simply embeds
--- symbolic equivalents for one type, then you can simply define 'create'. (Which is the most common case.)
-class Queriable m a where
-  type QueryResult a :: Type
-
-  -- | ^ Create a new symbolic value of type @a@
-  create  :: QueryT m a
-
-  -- | ^ Extract the current value in a SAT context
-  project :: a -> QueryT m (QueryResult a)
-
-  -- | ^ Create a literal value. Morally, 'embed' and 'project' are inverses of each other
-  -- via the 'QueryT' monad transformer.
-  embed   :: QueryResult a -> QueryT m a
-
-  default project :: (a ~ t (SBV e), QueryResult a ~ t e, Traversable t, MonadIO m, SymVal e) => a -> QueryT m (QueryResult a)
-  project = mapM getValue
-
-  default embed :: (a ~ t (SBV e), QueryResult a ~ t e, Traversable t, MonadIO m, SymVal e) => QueryResult a -> QueryT m a
-  embed = pure . fmap literal
-  {-# MINIMAL create #-}
-
--- | Generic 'Queriable' instance for 'SymVal' values
-instance {-# OVERLAPPABLE #-} (MonadIO m, SymVal a) => Queriable m (SBV a) where
-  type QueryResult (SBV a) = a
-
-  create  = freshVar_
-  project = getValue
-  embed   = return . literal
-
 {- $queryIntro
 In certain cases, the user might want to take over the communication with the solver, programmatically
 querying the engine and issuing commands accordingly. Queries can be extremely powerful as
diff --git a/Documentation/SBV/Examples/ProofTools/BMC.hs b/Documentation/SBV/Examples/ProofTools/BMC.hs
index b57f4268..abb440e7 100644
--- a/Documentation/SBV/Examples/ProofTools/BMC.hs
+++ b/Documentation/SBV/Examples/ProofTools/BMC.hs
@@ -30,7 +30,6 @@ module Documentation.SBV.Examples.ProofTools.BMC where
 
 import Data.SBV
 import Data.SBV.Tools.BMC
-import Data.SBV.Control
 
 -- * System state
 
diff --git a/Documentation/SBV/Examples/ProofTools/Fibonacci.hs b/Documentation/SBV/Examples/ProofTools/Fibonacci.hs
index a0349a6b..5e92ee79 100644
--- a/Documentation/SBV/Examples/ProofTools/Fibonacci.hs
+++ b/Documentation/SBV/Examples/ProofTools/Fibonacci.hs
@@ -34,7 +34,6 @@ module Documentation.SBV.Examples.ProofTools.Fibonacci where
 
 import Data.SBV
 import Data.SBV.Tools.Induction
-import Data.SBV.Control
 
 -- * System state
 
diff --git a/Documentation/SBV/Examples/ProofTools/Strengthen.hs b/Documentation/SBV/Examples/ProofTools/Strengthen.hs
index 5abe95cf..022e541d 100644
--- a/Documentation/SBV/Examples/ProofTools/Strengthen.hs
+++ b/Documentation/SBV/Examples/ProofTools/Strengthen.hs
@@ -41,7 +41,6 @@ module Documentation.SBV.Examples.ProofTools.Strengthen where
 
 import Data.SBV
 import Data.SBV.Tools.Induction
-import Data.SBV.Control
 
 -- * System state
 
diff --git a/Documentation/SBV/Examples/ProofTools/Sum.hs b/Documentation/SBV/Examples/ProofTools/Sum.hs
index b4e81701..1df9b4bb 100644
--- a/Documentation/SBV/Examples/ProofTools/Sum.hs
+++ b/Documentation/SBV/Examples/ProofTools/Sum.hs
@@ -33,7 +33,6 @@ module Documentation.SBV.Examples.ProofTools.Sum where
 
 import Data.SBV
 import Data.SBV.Tools.Induction
-import Data.SBV.Control
 
 -- * System state
 
diff --git a/Documentation/SBV/Examples/Puzzles/DieHard.hs b/Documentation/SBV/Examples/Puzzles/DieHard.hs
index 5812dc61..b3ace0f0 100644
--- a/Documentation/SBV/Examples/Puzzles/DieHard.hs
+++ b/Documentation/SBV/Examples/Puzzles/DieHard.hs
@@ -26,7 +26,6 @@
 module Documentation.SBV.Examples.Puzzles.DieHard where
 
 import Data.SBV
-import Data.SBV.Control
 import Data.SBV.Tools.BMC
 
 -- | Possible actions
diff --git a/Documentation/SBV/Examples/WeakestPreconditions/Append.hs b/Documentation/SBV/Examples/WeakestPreconditions/Append.hs
index 5bfc7042..12717508 100644
--- a/Documentation/SBV/Examples/WeakestPreconditions/Append.hs
+++ b/Documentation/SBV/Examples/WeakestPreconditions/Append.hs
@@ -25,7 +25,7 @@
 module Documentation.SBV.Examples.WeakestPreconditions.Append where
 
 import Data.SBV
-import Data.SBV.Control
+import Data.SBV.Tools.WeakestPreconditions
 
 import Prelude hiding ((++))
 import qualified Prelude as P
@@ -33,8 +33,6 @@ import qualified Prelude as P
 import           Data.SBV.List ((++))
 import qualified Data.SBV.List as L
 
-import Data.SBV.Tools.WeakestPreconditions
-
 import GHC.Generics (Generic)
 
 -- * Program state
diff --git a/Documentation/SBV/Examples/WeakestPreconditions/Basics.hs b/Documentation/SBV/Examples/WeakestPreconditions/Basics.hs
index e930385a..33834309 100644
--- a/Documentation/SBV/Examples/WeakestPreconditions/Basics.hs
+++ b/Documentation/SBV/Examples/WeakestPreconditions/Basics.hs
@@ -25,8 +25,6 @@
 module Documentation.SBV.Examples.WeakestPreconditions.Basics where
 
 import Data.SBV
-import Data.SBV.Control
-
 import Data.SBV.Tools.WeakestPreconditions
 
 import GHC.Generics (Generic)
diff --git a/Documentation/SBV/Examples/WeakestPreconditions/Fib.hs b/Documentation/SBV/Examples/WeakestPreconditions/Fib.hs
index 004654bd..13000afa 100644
--- a/Documentation/SBV/Examples/WeakestPreconditions/Fib.hs
+++ b/Documentation/SBV/Examples/WeakestPreconditions/Fib.hs
@@ -26,8 +26,6 @@
 module Documentation.SBV.Examples.WeakestPreconditions.Fib where
 
 import Data.SBV
-import Data.SBV.Control
-
 import Data.SBV.Tools.WeakestPreconditions
 
 import GHC.Generics (Generic)
diff --git a/Documentation/SBV/Examples/WeakestPreconditions/GCD.hs b/Documentation/SBV/Examples/WeakestPreconditions/GCD.hs
index 93b137b1..bb80f2c1 100644
--- a/Documentation/SBV/Examples/WeakestPreconditions/GCD.hs
+++ b/Documentation/SBV/Examples/WeakestPreconditions/GCD.hs
@@ -28,8 +28,6 @@
 module Documentation.SBV.Examples.WeakestPreconditions.GCD where
 
 import Data.SBV
-import Data.SBV.Control
-
 import Data.SBV.Tools.WeakestPreconditions
 
 import GHC.Generics (Generic)
diff --git a/Documentation/SBV/Examples/WeakestPreconditions/IntDiv.hs b/Documentation/SBV/Examples/WeakestPreconditions/IntDiv.hs
index 9567ad17..d2f48e91 100644
--- a/Documentation/SBV/Examples/WeakestPreconditions/IntDiv.hs
+++ b/Documentation/SBV/Examples/WeakestPreconditions/IntDiv.hs
@@ -24,8 +24,6 @@
 module Documentation.SBV.Examples.WeakestPreconditions.IntDiv where
 
 import Data.SBV
-import Data.SBV.Control
-
 import Data.SBV.Tools.WeakestPreconditions
 
 import GHC.Generics (Generic)
diff --git a/Documentation/SBV/Examples/WeakestPreconditions/IntSqrt.hs b/Documentation/SBV/Examples/WeakestPreconditions/IntSqrt.hs
index 62f023de..52f5e4b6 100644
--- a/Documentation/SBV/Examples/WeakestPreconditions/IntSqrt.hs
+++ b/Documentation/SBV/Examples/WeakestPreconditions/IntSqrt.hs
@@ -26,8 +26,6 @@
 module Documentation.SBV.Examples.WeakestPreconditions.IntSqrt where
 
 import Data.SBV
-import Data.SBV.Control
-
 import Data.SBV.Tools.WeakestPreconditions
 
 import GHC.Generics (Generic)
diff --git a/Documentation/SBV/Examples/WeakestPreconditions/Length.hs b/Documentation/SBV/Examples/WeakestPreconditions/Length.hs
index a7c9e791..95d8e7a9 100644
--- a/Documentation/SBV/Examples/WeakestPreconditions/Length.hs
+++ b/Documentation/SBV/Examples/WeakestPreconditions/Length.hs
@@ -23,12 +23,10 @@
 module Documentation.SBV.Examples.WeakestPreconditions.Length where
 
 import Data.SBV
-import Data.SBV.Control
+import Data.SBV.Tools.WeakestPreconditions
 
 import qualified Data.SBV.List as L
 
-import Data.SBV.Tools.WeakestPreconditions
-
 import GHC.Generics (Generic)
 
 -- * Program state
diff --git a/Documentation/SBV/Examples/WeakestPreconditions/Sum.hs b/Documentation/SBV/Examples/WeakestPreconditions/Sum.hs
index c4c49da3..35b3f2fc 100644
--- a/Documentation/SBV/Examples/WeakestPreconditions/Sum.hs
+++ b/Documentation/SBV/Examples/WeakestPreconditions/Sum.hs
@@ -25,8 +25,6 @@
 module Documentation.SBV.Examples.WeakestPreconditions.Sum where
 
 import Data.SBV
-import Data.SBV.Control
-
 import Data.SBV.Tools.WeakestPreconditions
 
 import GHC.Generics (Generic)