diff --git a/Documentation/SBV/Examples/ProofTools/BMC.hs b/Documentation/SBV/Examples/ProofTools/BMC.hs
index ca6efc3b..5fa5840d 100644
--- a/Documentation/SBV/Examples/ProofTools/BMC.hs
+++ b/Documentation/SBV/Examples/ProofTools/BMC.hs
@@ -18,7 +18,6 @@
 -- What if @y@ starts at @11@?
 -----------------------------------------------------------------------------
 
-{-# LANGUAGE DeriveTraversable     #-}
 {-# LANGUAGE FlexibleInstances     #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE NamedFieldPuns        #-}
@@ -36,7 +35,6 @@ import Data.SBV.Control
 
 -- | System state, containing the two integers.
 data S a = S { x :: a, y :: a }
-         deriving (Functor, Foldable, Traversable)
 
 -- | Show the state as a pair
 instance Show a => Show (S a) where
@@ -50,9 +48,9 @@ instance EqSymbolic a => EqSymbolic (S a) where
 instance Queriable IO (S SInteger) where
   type QueryResult (S SInteger) = S Integer
 
-  create  = S <$> freshVar_ <*> freshVar_
-  project = mapM getValue
-  embed   = return . fmap literal
+  create          = S <$> freshVar_ <*> freshVar_
+  project S{x, y} = getValue x >>= \vx -> getValue y >>= \vy -> pure S{x = vx, y = vy}
+  embed   S{x, y} = pure S{x = literal x, y = literal y}
 
 -- * Encoding the problem
 
diff --git a/Documentation/SBV/Examples/ProofTools/Fibonacci.hs b/Documentation/SBV/Examples/ProofTools/Fibonacci.hs
index ab04f956..9aa3d378 100644
--- a/Documentation/SBV/Examples/ProofTools/Fibonacci.hs
+++ b/Documentation/SBV/Examples/ProofTools/Fibonacci.hs
@@ -22,9 +22,6 @@
 -- uninterpreted function.
 -----------------------------------------------------------------------------
 
-{-# LANGUAGE DeriveAnyClass        #-}
-{-# LANGUAGE DeriveGeneric         #-}
-{-# LANGUAGE DeriveTraversable     #-}
 {-# LANGUAGE FlexibleInstances     #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE NamedFieldPuns        #-}
@@ -38,22 +35,19 @@ import Data.SBV
 import Data.SBV.Tools.Induction
 import Data.SBV.Control
 
-import GHC.Generics hiding (S)
-
 -- * System state
 
 -- | System state. We simply have two components, parameterized
 -- over the type so we can put in both concrete and symbolic values.
-data S a = S { i :: a, k :: a, m :: a, n :: a }
-         deriving (Show, Mergeable, Generic, Functor, Foldable, Traversable)
+data S a = S { i :: a, k :: a, m :: a, n :: a } deriving Show
 
 -- | 'Queriable instance for our state
 instance Queriable IO (S SInteger) where
   type QueryResult (S SInteger) = S Integer
 
-  create  = S <$> freshVar_ <*> freshVar_ <*> freshVar_ <*> freshVar_
-  project = mapM getValue
-  embed   = return . fmap literal
+  create                = S <$> freshVar_ <*> freshVar_ <*> freshVar_ <*> freshVar_
+  project S{i, k, m, n} = getValue i >>= \vi -> getValue k >>= \vk -> getValue m >>= \vm -> getValue n >>= \vn -> pure S{i = vi, k = vk, m = vm, n = vn}
+  embed   S{i, k, m, n} = pure S{i = literal i, k = literal k, m = literal m, n = literal n}
 
 -- | Encoding partial correctness of the sum algorithm. We have:
 --
diff --git a/Documentation/SBV/Examples/ProofTools/Strengthen.hs b/Documentation/SBV/Examples/ProofTools/Strengthen.hs
index 3c8bc9e5..ba9e7bfd 100644
--- a/Documentation/SBV/Examples/ProofTools/Strengthen.hs
+++ b/Documentation/SBV/Examples/ProofTools/Strengthen.hs
@@ -29,7 +29,6 @@
 -- in Bradley's paper quite closely.
 -----------------------------------------------------------------------------
 
-{-# LANGUAGE DeriveTraversable     #-}
 {-# LANGUAGE FlexibleInstances     #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE NamedFieldPuns        #-}
@@ -47,16 +46,15 @@ import Data.SBV.Control
 
 -- | System state. We simply have two components, parameterized
 -- over the type so we can put in both concrete and symbolic values.
-data S a = S { x :: a, y :: a }
-         deriving (Show, Functor, Foldable, Traversable)
+data S a = S { x :: a, y :: a } deriving Show
 
 -- | 'Queriable instance for our state
 instance Queriable IO (S SInteger) where
   type QueryResult (S SInteger) = S Integer
 
-  create  = S <$> freshVar_ <*> freshVar_
-  project = mapM getValue
-  embed   = return . fmap literal
+  create          = S <$> freshVar_ <*> freshVar_
+  project S{x, y} = getValue x >>= \vx -> getValue y >>= \vy -> pure S{x = vx, y = vy}
+  embed   S{x, y} = pure S{x = literal x, y = literal y}
 
 -- * Encoding the problem
 
diff --git a/Documentation/SBV/Examples/ProofTools/Sum.hs b/Documentation/SBV/Examples/ProofTools/Sum.hs
index aed7f204..40064dbc 100644
--- a/Documentation/SBV/Examples/ProofTools/Sum.hs
+++ b/Documentation/SBV/Examples/ProofTools/Sum.hs
@@ -21,9 +21,6 @@
 -- @s@ is the sum of all numbers up to and including @n@ upon termination.
 -----------------------------------------------------------------------------
 
-{-# LANGUAGE DeriveAnyClass        #-}
-{-# LANGUAGE DeriveGeneric         #-}
-{-# LANGUAGE DeriveTraversable     #-}
 {-# LANGUAGE FlexibleInstances     #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE NamedFieldPuns        #-}
@@ -37,21 +34,19 @@ import Data.SBV
 import Data.SBV.Tools.Induction
 import Data.SBV.Control
 
-import GHC.Generics hiding (S)
-
 -- * System state
 
 -- | System state. We simply have two components, parameterized
 -- over the type so we can put in both concrete and symbolic values.
-data S a = S { s :: a, i :: a, n :: a } deriving (Show, Mergeable, Generic, Functor, Foldable, Traversable)
+data S a = S { s :: a, i :: a, n :: a } deriving Show
 
 -- | 'Queriable instance for our state
 instance Queriable IO (S SInteger) where
   type QueryResult (S SInteger) = S Integer
 
-  create  = S <$> freshVar_ <*> freshVar_ <*> freshVar_
-  project = mapM getValue
-  embed   = return . fmap literal
+  create             = S <$> freshVar_ <*> freshVar_ <*> freshVar_
+  project S{s, i, n} = getValue s >>= \vs -> getValue i >>= \vi -> getValue n >>= \vn -> pure S{s = vs, i = vi, n = vn}
+  embed   S{s, i, n} = pure S{s = literal s, i = literal i, n = literal n}
 
 -- | Encoding partial correctness of the sum algorithm. We have:
 --
diff --git a/Documentation/SBV/Examples/Puzzles/DieHard.hs b/Documentation/SBV/Examples/Puzzles/DieHard.hs
index 3f64701c..37157a70 100644
--- a/Documentation/SBV/Examples/Puzzles/DieHard.hs
+++ b/Documentation/SBV/Examples/Puzzles/DieHard.hs
@@ -13,7 +13,6 @@
 
 {-# LANGUAGE DeriveAnyClass        #-}
 {-# LANGUAGE DeriveDataTypeable    #-}
-{-# LANGUAGE DeriveTraversable     #-}
 {-# LANGUAGE FlexibleInstances     #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE NamedFieldPuns        #-}
@@ -61,15 +60,15 @@ instance Queriable IO SState where
   project State{big, small, action} = do b <- getValue big
                                          s <- getValue small
                                          a <- getValue action
-                                         pure $ State { big    = b
-                                                      , small  = s
-                                                      , action = a
-                                                      }
-
-  embed State{big, small, action} = pure $ State { big    = literal big
-                                                 , small  = literal small
-                                                 , action = literal action
-                                                 }
+                                         pure State{ big    = b
+                                                   , small  = s
+                                                   , action = a
+                                                   }
+
+  embed State{big, small, action} = pure State{ big    = literal big
+                                              , small  = literal small
+                                              , action = literal action
+                                              }
 
 -- | Solve the problem using a BMC search. We have:
 --
diff --git a/Documentation/SBV/Examples/WeakestPreconditions/Append.hs b/Documentation/SBV/Examples/WeakestPreconditions/Append.hs
index 67aaf95d..93c8c257 100644
--- a/Documentation/SBV/Examples/WeakestPreconditions/Append.hs
+++ b/Documentation/SBV/Examples/WeakestPreconditions/Append.hs
@@ -39,36 +39,27 @@ import GHC.Generics (Generic)
 -- * Program state
 
 -- | The state of the length program, paramaterized over the element type @a@
-data AppS a = AppS { xs :: SList a  -- ^ The first input list
-                   , ys :: SList a  -- ^ The second input list
-                   , ts :: SList a  -- ^ Temporary variable
-                   , zs :: SList a  -- ^ Output
+data AppS a = AppS { xs :: a  -- ^ The first input list
+                   , ys :: a  -- ^ The second input list
+                   , ts :: a  -- ^ Temporary variable
+                   , zs :: a  -- ^ Output
                    }
                    deriving (Generic, Mergeable)
 
--- | The concrete counterpart of 'AppS'. Again, we can't simply use the duality between
--- @SBV a@ and @a@ due to the difference between @SList a@ and @[a]@.
-data AppC a = AppC [a] [a] [a] [a]
-
--- | Show instance for 'AppS'. The above deriving clause would work just as well,
--- but we want it to be a little prettier here, and hence the @OVERLAPS@ directive.
-instance {-# OVERLAPS #-} (SymVal a, Show a) => Show (AppS a) where
-  show (AppS xs ys ts zs) = "{xs = " P.++ sh xs P.++ ", ys = " P.++ sh ys P.++ ", ts = " P.++ sh ts P.++ ", zs = " P.++ sh zs P.++ "}"
-    where sh v = maybe "<symbolic>" show (unliteral v)
-
 -- | Show instance, a bit more prettier than what would be derived:
-instance Show a => Show (AppC a) where
-  show (AppC xs ys ts zs) = "{xs = " P.++ show xs P.++ ", ys = " P.++ show ys P.++ ", ts = " P.++ show ts P.++ ", zs = " P.++ show zs P.++ "}"
+instance Show (f a) => Show (AppS (f a)) where
+  show AppS{xs, ys, ts, zs} = "{xs = " P.++ show xs P.++ ", ys = " P.++ show ys P.++ ", ts = " P.++ show ts P.++ ", zs = " P.++ show zs P.++ "}"
 
 -- | 'Queriable' instance for the program state
-instance Queriable IO (AppS Integer) where
-  type QueryResult (AppS Integer) = AppC Integer
-  create                     = AppS <$> freshVar_   <*> freshVar_   <*> freshVar_   <*> freshVar_
-  project (AppS xs ys ts zs) = AppC <$> getValue xs <*> getValue ys <*> getValue ts <*> getValue zs
-  embed   (AppC xs ys ts zs) = return $ AppS (literal xs) (literal ys) (literal ts) (literal zs)
+instance Queriable IO (AppS (SList Integer)) where
+  type QueryResult (AppS (SList Integer)) = AppS [Integer]
+
+  create                       = AppS <$> freshVar_  <*> freshVar_  <*> freshVar_  <*> freshVar_
+  project AppS{xs, ys, ts, zs} = getValue xs >>= \vxs -> getValue ys >>= \vxy -> getValue ts >>= \vts -> getValue zs >>= \vzs -> pure AppS{xs = vxs, ys = vxy, ts = vts, zs = vzs}
+  embed   AppS{xs, ys, ts, zs} = pure AppS{xs = literal xs, ys = literal ys, ts = literal ts, zs = literal zs}
 
 -- | Helper type synonym
-type A = AppS Integer
+type A = AppS (SList Integer)
 
 -- * The algorithm
 
@@ -122,5 +113,5 @@ imperativeAppend = Program { setup         = return ()
 -- >>> correctness
 -- Total correctness is established.
 -- Q.E.D.
-correctness :: IO (ProofResult (AppC Integer))
+correctness :: IO (ProofResult (AppS [Integer]))
 correctness = wpProveWith defaultWPCfg{wpVerbose=True} imperativeAppend
diff --git a/Documentation/SBV/Examples/WeakestPreconditions/Basics.hs b/Documentation/SBV/Examples/WeakestPreconditions/Basics.hs
index a5ee4581..a78462ff 100644
--- a/Documentation/SBV/Examples/WeakestPreconditions/Basics.hs
+++ b/Documentation/SBV/Examples/WeakestPreconditions/Basics.hs
@@ -14,7 +14,6 @@
 {-# LANGUAGE CPP                   #-}
 {-# LANGUAGE DeriveAnyClass        #-}
 {-# LANGUAGE DeriveGeneric         #-}
-{-# LANGUAGE DeriveTraversable     #-}
 {-# LANGUAGE FlexibleInstances     #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE NamedFieldPuns        #-}
@@ -45,7 +44,7 @@ import GHC.Generics (Generic)
 data IncS a = IncS { x :: a    -- ^ Input value
                    , y :: a    -- ^ Output
                    }
-                   deriving (Show, Generic, Mergeable, Functor, Foldable, Traversable)
+                   deriving (Show, Generic, Mergeable)
 
 -- | Show instance for 'IncS'. The above deriving clause would work just as well,
 -- but we want it to be a little prettier here, and hence the @OVERLAPS@ directive.
@@ -57,9 +56,9 @@ instance {-# OVERLAPS #-} (SymVal a, Show a) => Show (IncS (SBV a)) where
 instance Queriable IO (IncS SInteger) where
   type QueryResult (IncS SInteger) = IncS Integer
 
-  create  = IncS <$> freshVar_ <*> freshVar_
-  project = mapM getValue
-  embed   = return . fmap literal
+  create             = IncS <$> freshVar_ <*> freshVar_
+  project IncS{x, y} = getValue x >>= \vx -> getValue y >>= \vy -> pure IncS{x = vx, y = vy}
+  embed   IncS{x, y} = pure IncS{x = literal x, y = literal y}
 
 -- | Helper type synonym
 type I = IncS SInteger
diff --git a/Documentation/SBV/Examples/WeakestPreconditions/Fib.hs b/Documentation/SBV/Examples/WeakestPreconditions/Fib.hs
index 5467d1fc..c54e97ba 100644
--- a/Documentation/SBV/Examples/WeakestPreconditions/Fib.hs
+++ b/Documentation/SBV/Examples/WeakestPreconditions/Fib.hs
@@ -15,7 +15,6 @@
 {-# LANGUAGE CPP                   #-}
 {-# LANGUAGE DeriveAnyClass        #-}
 {-# LANGUAGE DeriveGeneric         #-}
-{-# LANGUAGE DeriveTraversable     #-}
 {-# LANGUAGE FlexibleInstances     #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE NamedFieldPuns        #-}
@@ -48,7 +47,7 @@ data FibS a = FibS { n :: a    -- ^ The input value
                    , k :: a    -- ^ tracks @fib (i+1)@
                    , m :: a    -- ^ tracks @fib i@
                    }
-                   deriving (Show, Generic, Mergeable, Functor, Foldable, Traversable)
+                   deriving (Show, Generic, Mergeable)
 
 -- | Show instance for 'FibS'. The above deriving clause would work just as well,
 -- but we want it to be a little prettier here, and hence the @OVERLAPS@ directive.
@@ -60,9 +59,9 @@ instance {-# OVERLAPS #-} (SymVal a, Show a) => Show (FibS (SBV a)) where
 instance Queriable IO (FibS SInteger) where
   type QueryResult (FibS SInteger) = FibS Integer
 
-  create  = FibS <$> freshVar_ <*> freshVar_ <*> freshVar_ <*> freshVar_
-  project = mapM getValue
-  embed   = return . fmap literal
+  create                   = FibS <$> freshVar_  <*> freshVar_ <*> freshVar_ <*> freshVar_
+  project FibS{n, i, k, m} = getValue n >>= \vn -> getValue i >>= \vi -> getValue k >>= \vk -> getValue m >>= \vm -> pure FibS{n = vn, i = vi, k = vk, m = vm}
+  embed   FibS{n, i, k, m} = pure FibS{n = literal n, i = literal i, k = literal k, m = literal m}
 
 -- | Helper type synonym
 type F = FibS SInteger
diff --git a/Documentation/SBV/Examples/WeakestPreconditions/GCD.hs b/Documentation/SBV/Examples/WeakestPreconditions/GCD.hs
index 9d687e33..49287667 100644
--- a/Documentation/SBV/Examples/WeakestPreconditions/GCD.hs
+++ b/Documentation/SBV/Examples/WeakestPreconditions/GCD.hs
@@ -17,7 +17,6 @@
 {-# LANGUAGE CPP                   #-}
 {-# LANGUAGE DeriveAnyClass        #-}
 {-# LANGUAGE DeriveGeneric         #-}
-{-# LANGUAGE DeriveTraversable     #-}
 {-# LANGUAGE FlexibleInstances     #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE NamedFieldPuns        #-}
@@ -54,7 +53,7 @@ data GCDS a = GCDS { x :: a    -- ^ First value
                    , i :: a    -- ^ Copy of x to be modified
                    , j :: a    -- ^ Copy of y to be modified
                    }
-                   deriving (Show, Generic, Mergeable, Functor, Foldable, Traversable)
+                   deriving (Show, Generic, Mergeable)
 
 -- | Show instance for 'GCDS'. The above deriving clause would work just as well,
 -- but we want it to be a little prettier here, and hence the @OVERLAPS@ directive.
@@ -66,9 +65,9 @@ instance {-# OVERLAPS #-} (SymVal a, Show a) => Show (GCDS (SBV a)) where
 instance Queriable IO (GCDS SInteger) where
   type QueryResult (GCDS SInteger) = GCDS Integer
 
-  create  = GCDS <$> freshVar_ <*> freshVar_ <*> freshVar_ <*> freshVar_
-  project = mapM getValue
-  embed   = return . fmap literal
+  create                   = GCDS <$> freshVar_ <*> freshVar_ <*> freshVar_ <*> freshVar_
+  project GCDS{x, y, i, j} = getValue x >>= \vx -> getValue y >>= \vy -> getValue i >>= \vi -> getValue j >>= \vj -> pure GCDS{x = vx, y = vy, i = vi, j = vj}
+  embed   GCDS{x, y, i, j} = pure GCDS{x = literal x, y = literal y, i = literal i, j = literal j}
 
 -- | Helper type synonym
 type G = GCDS SInteger
diff --git a/Documentation/SBV/Examples/WeakestPreconditions/IntDiv.hs b/Documentation/SBV/Examples/WeakestPreconditions/IntDiv.hs
index 40f1e3e0..ac0473c5 100644
--- a/Documentation/SBV/Examples/WeakestPreconditions/IntDiv.hs
+++ b/Documentation/SBV/Examples/WeakestPreconditions/IntDiv.hs
@@ -13,7 +13,6 @@
 
 {-# LANGUAGE DeriveAnyClass        #-}
 {-# LANGUAGE DeriveGeneric         #-}
-{-# LANGUAGE DeriveTraversable     #-}
 {-# LANGUAGE FlexibleInstances     #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE NamedFieldPuns        #-}
@@ -38,7 +37,7 @@ data DivS a = DivS { x :: a   -- ^ The dividend
                    , q :: a   -- ^ The quotient
                    , r :: a   -- ^ The remainder
                    }
-                   deriving (Show, Generic, Mergeable, Functor, Foldable, Traversable)
+                   deriving (Show, Generic, Mergeable)
 
 -- | Show instance for 'DivS'. The above deriving clause would work just as well,
 -- but we want it to be a little prettier here, and hence the @OVERLAPS@ directive.
@@ -50,9 +49,9 @@ instance {-# OVERLAPS #-} (SymVal a, Show a) => Show (DivS (SBV a)) where
 instance SymVal a => Queriable IO (DivS (SBV a)) where
   type QueryResult (DivS (SBV a)) = DivS a
 
-  create  = DivS <$> freshVar_  <*> freshVar_ <*> freshVar_ <*> freshVar_
-  project = mapM getValue
-  embed   = return . fmap literal
+  create                   = DivS <$> freshVar_  <*> freshVar_ <*> freshVar_ <*> freshVar_
+  project DivS{x, y, q, r} = getValue x >>= \vx -> getValue y >>= \vy -> getValue q >>= \vq -> getValue r >>= \vr -> pure DivS{x = vx, y = vy, q = vq, r = vr}
+  embed   DivS{x, y, q, r} = pure DivS{x = literal x, y = literal y, q = literal q, r = literal r}
 
 -- | Helper type synonym
 type D = DivS SInteger
diff --git a/Documentation/SBV/Examples/WeakestPreconditions/IntSqrt.hs b/Documentation/SBV/Examples/WeakestPreconditions/IntSqrt.hs
index e97146c9..b2b1d8bb 100644
--- a/Documentation/SBV/Examples/WeakestPreconditions/IntSqrt.hs
+++ b/Documentation/SBV/Examples/WeakestPreconditions/IntSqrt.hs
@@ -15,7 +15,6 @@
 
 {-# LANGUAGE DeriveAnyClass        #-}
 {-# LANGUAGE DeriveGeneric         #-}
-{-# LANGUAGE DeriveTraversable     #-}
 {-# LANGUAGE FlexibleInstances     #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE NamedFieldPuns        #-}
@@ -42,7 +41,7 @@ data SqrtS a = SqrtS { x    :: a   -- ^ The input
                      , i    :: a   -- ^ Successive squares, as the sum of j's
                      , j    :: a   -- ^ Successive odds
                      }
-                     deriving (Show, Generic, Mergeable, Functor, Foldable, Traversable)
+                     deriving (Show, Generic, Mergeable)
 
 -- | Show instance for 'SqrtS'. The above deriving clause would work just as well,
 -- but we want it to be a little prettier here, and hence the @OVERLAPS@ directive.
@@ -54,9 +53,9 @@ instance {-# OVERLAPS #-} (SymVal a, Show a) => Show (SqrtS (SBV a)) where
 instance SymVal a => Queriable IO (SqrtS (SBV a)) where
   type QueryResult (SqrtS (SBV a)) = SqrtS a
 
-  create  = SqrtS <$> freshVar_ <*> freshVar_ <*> freshVar_ <*> freshVar_
-  project = mapM getValue
-  embed   = return . fmap literal
+  create                       = SqrtS <$> freshVar_  <*> freshVar_ <*> freshVar_ <*> freshVar_
+  project SqrtS{x, sqrt, i, j} = getValue x >>= \vx -> getValue sqrt >>= \vsqrt -> getValue i >>= \vi -> getValue j >>= \vj -> pure SqrtS{x = vx, sqrt = vsqrt, i = vi, j = vj}
+  embed   SqrtS{x, sqrt, i, j} = pure SqrtS{x = literal x, sqrt = literal sqrt, i = literal i, j = literal j}
 
 -- | Helper type synonym
 type S = SqrtS SInteger
diff --git a/Documentation/SBV/Examples/WeakestPreconditions/Length.hs b/Documentation/SBV/Examples/WeakestPreconditions/Length.hs
index 3a7ca0d2..a7c9e791 100644
--- a/Documentation/SBV/Examples/WeakestPreconditions/Length.hs
+++ b/Documentation/SBV/Examples/WeakestPreconditions/Length.hs
@@ -34,39 +34,27 @@ import GHC.Generics (Generic)
 -- * Program state
 
 -- | The state of the length program, paramaterized over the element type @a@
-data LenS a = LenS { xs :: SList a  -- ^ The input list
-                   , ys :: SList a  -- ^ Copy of input
-                   , l  :: SInteger -- ^ Running length
-                   }
-                   deriving (Generic, Mergeable)
-
--- | The concrete counterpart to 'LenS'. Note that we can no longer use the duality
--- between @SBV a@ and @a@ as in other examples and just use one datatype for both.
--- This is because @SList a@ and @[a]@ are fundamentally different types. This can
--- be a bit confusing at first, but the point is that it is the list that is symbolic
--- in case of an @SList a@, not that we have a concrete list with symbolic elements
--- in it. Subtle difference, but it is important to keep these two separate.
-data LenC a = LenC [a] [a] Integer
+data LenS a b = LenS { xs :: a  -- ^ The input list
+                     , ys :: a  -- ^ Copy of input
+                     , l  :: b  -- ^ Running length
+                     }
+                     deriving (Generic, Mergeable)
 
 -- | Show instance: A simplified version of what would otherwise be generated.
-instance (SymVal a, Show a) => Show (LenS a) where
-  show (LenS xs ys l) = "{xs = " ++ sh xs ++ ", ys = " ++ sh ys ++ ", l = " ++ sh l ++ "}"
-    where sh v = maybe "<symbolic>" show (unliteral v)
-
--- | Show instance: Similarly, we want to be a bit more concise here.
-instance Show a => Show (LenC a) where
-  show (LenC xs ys l) = "{xs = " ++ show xs ++ ", ys = " ++ show ys ++ ", l = " ++ show l ++ "}"
+instance (SymVal a, Show (f a), Show b) => Show (LenS (f a) b) where
+  show LenS{xs, ys, l} = "{xs = " ++ show xs ++ ", ys = " ++ show ys ++ ", l = " ++ show l ++ "}"
 
 -- | We have to write the bijection between 'LenS' and 'LenC' explicitly. Luckily, the
 -- definition is more or less boilerplate.
-instance Queriable IO (LenS Integer) where
-  type QueryResult (LenS Integer) = LenC Integer
-  create                 = LenS <$> freshVar_   <*> freshVar_   <*> freshVar_
-  project (LenS xs ys l) = LenC <$> getValue xs <*> getValue ys <*> getValue l
-  embed   (LenC xs ys l) = return $ LenS (literal xs) (literal ys) (literal l)
+instance Queriable IO (LenS (SList Integer) SInteger) where
+  type QueryResult (LenS (SList Integer) SInteger) = LenS [Integer] Integer
+
+  create                  = LenS <$> freshVar_   <*> freshVar_   <*> freshVar_
+  project LenS{xs, ys, l} = getValue xs >>= \vxs -> getValue ys >>= \vys -> getValue l >>= \vl -> pure LenS{xs = vxs, ys = vys, l = vl}
+  embed   LenS{xs, ys, l} = pure LenS{xs = literal xs, ys = literal ys, l = literal l}
 
 -- | Helper type synonym
-type S = LenS Integer
+type S = LenS (SList Integer) SInteger
 
 -- * The algorithm
 
diff --git a/Documentation/SBV/Examples/WeakestPreconditions/Sum.hs b/Documentation/SBV/Examples/WeakestPreconditions/Sum.hs
index 0e40abfa..0d4cb591 100644
--- a/Documentation/SBV/Examples/WeakestPreconditions/Sum.hs
+++ b/Documentation/SBV/Examples/WeakestPreconditions/Sum.hs
@@ -14,7 +14,6 @@
 {-# LANGUAGE CPP                   #-}
 {-# LANGUAGE DeriveAnyClass        #-}
 {-# LANGUAGE DeriveGeneric         #-}
-{-# LANGUAGE DeriveTraversable     #-}
 {-# LANGUAGE FlexibleInstances     #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE NamedFieldPuns        #-}
@@ -44,7 +43,7 @@ data SumS a = SumS { n :: a    -- ^ The input value
                    , i :: a    -- ^ Loop counter
                    , s :: a    -- ^ Running sum
                    }
-                   deriving (Show, Generic, Mergeable, Functor, Foldable, Traversable)
+                   deriving (Show, Generic, Mergeable)
 
 -- | Show instance for 'SumS'. The above deriving clause would work just as well,
 -- but we want it to be a little prettier here, and hence the @OVERLAPS@ directive.
@@ -56,9 +55,9 @@ instance {-# OVERLAPS #-} (SymVal a, Show a) => Show (SumS (SBV a)) where
 instance Queriable IO (SumS SInteger) where
   type QueryResult (SumS SInteger) = SumS Integer
 
-  create  = SumS <$> freshVar_ <*> freshVar_ <*> freshVar_
-  project = mapM getValue
-  embed   = return . fmap literal
+  create                = SumS <$> freshVar_ <*> freshVar_ <*> freshVar_
+  project SumS{n, i, s} = getValue n >>= \vn -> getValue i >>= \vi -> getValue s >>= \vs -> pure SumS{n = vn, i = vi, s = vs}
+  embed   SumS{n, i, s} = pure SumS{n = literal n, i = literal i, s = literal s}
 
 -- | Helper type synonym
 type S = SumS SInteger
diff --git a/sbv.cabal b/sbv.cabal
index 7bc3132c..c218cd16 100644
--- a/sbv.cabal
+++ b/sbv.cabal
@@ -39,7 +39,6 @@ common common-settings
                      DeriveDataTypeable
                      DeriveFunctor
                      DeriveGeneric
-                     DeriveTraversable
                      DerivingStrategies
                      ExistentialQuantification
                      FlexibleContexts