diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,12 @@
 # Revision history for quickcheck-lockstep
 
+## 0.4.0 -- 2024-02-17
+
+* BREAKING: Counter-examples now produce valid code. To facilitate this,
+  `HasVariables` and `Show` instances have changed, and a new `unsafeMkGVar`
+  smart constructor is exposed.
+* Add compatibility with ghc-9.8
+
 ## 0.3.0 -- 2023-10-17
 
 * BREAKING: Update `quickcheck-dynamic` dependency to `>=3.3`.
diff --git a/quickcheck-lockstep.cabal b/quickcheck-lockstep.cabal
--- a/quickcheck-lockstep.cabal
+++ b/quickcheck-lockstep.cabal
@@ -1,6 +1,6 @@
 cabal-version:      2.4
 name:               quickcheck-lockstep
-version:            0.3.0
+version:            0.4.0
 license:            BSD-3-Clause
 license-file:       LICENSE
 author:             Edsko de Vries
@@ -13,7 +13,7 @@
                     APIs calls, then execute them both against the system under
                     test and against a model, and compare responses up to some
                     notion of observability.
-tested-with:        GHC ==8.10 || ==9.0 || ==9.2 || ==9.4 || ==9.6
+tested-with:        GHC ==8.10 || ==9.0 || ==9.2 || ==9.4 || ==9.6 || ==9.8
 
 source-repository head
   type:     git
@@ -59,7 +59,7 @@
       Test.QuickCheck.StateModel.Lockstep.GVar
   build-depends:
       -- quickcheck-dynamic requires ghc 8.10 minimum
-      base               >= 4.14   && < 4.19
+      base               >= 4.14   && < 4.20
     , constraints        >= 0.13   && < 0.14
     , mtl                >= 2.2    && < 2.4
     , containers         >= 0.6    && < 0.7
diff --git a/src/Test/QuickCheck/StateModel/Lockstep.hs b/src/Test/QuickCheck/StateModel/Lockstep.hs
--- a/src/Test/QuickCheck/StateModel/Lockstep.hs
+++ b/src/Test/QuickCheck/StateModel/Lockstep.hs
@@ -24,6 +24,7 @@
     -- * Variables
   , GVar -- opaque
   , AnyGVar(..)
+  , unsafeMkGVar
   , lookUpGVar
   , mapGVar
     -- ** Operations
diff --git a/src/Test/QuickCheck/StateModel/Lockstep/Defaults.hs b/src/Test/QuickCheck/StateModel/Lockstep/Defaults.hs
--- a/src/Test/QuickCheck/StateModel/Lockstep/Defaults.hs
+++ b/src/Test/QuickCheck/StateModel/Lockstep/Defaults.hs
@@ -137,12 +137,13 @@
 instance HasVariables (Lockstep state) where
   getAllVariables _ = Set.empty
 
--- | Ignore variables for lockstep actions.
+-- | Do not ignore variables for lockstep actions.
 --
--- We largely ignore @quickcheck-dynamic@'s variables in the lockstep framework,
--- since it does its own accounting of model variables.
-instance HasVariables (Action (Lockstep state) a) where
-  getAllVariables _ = Set.empty
+-- @quickcheck-dynamic@ prints counterexamples as code that is more or less
+-- runnable, which requires a sensible 'HasVariables' instance for lockstep
+-- actions.
+instance InLockstep state => HasVariables (Action (Lockstep state) a) where
+  getAllVariables = Set.unions . fmap getAllVariables . usedVars
 
 {-------------------------------------------------------------------------------
   Internal auxiliary
diff --git a/src/Test/QuickCheck/StateModel/Lockstep/GVar.hs b/src/Test/QuickCheck/StateModel/Lockstep/GVar.hs
--- a/src/Test/QuickCheck/StateModel/Lockstep/GVar.hs
+++ b/src/Test/QuickCheck/StateModel/Lockstep/GVar.hs
@@ -7,6 +7,7 @@
     GVar -- opaque
   , AnyGVar(..)
     -- * Construction
+  , unsafeMkGVar
   , fromVar
   , mapGVar
     -- * Interop with 'Env'
@@ -21,8 +22,10 @@
 import Data.Maybe (isJust, fromJust)
 import Data.Typeable
 
-import Test.QuickCheck.StateModel (Var, LookUp, Realized)
+import GHC.Show
 
+import Test.QuickCheck.StateModel (Var, LookUp, Realized, HasVariables (..))
+
 import Test.QuickCheck.StateModel.Lockstep.EnvF (EnvF)
 import Test.QuickCheck.StateModel.Lockstep.EnvF qualified as EnvF
 import Test.QuickCheck.StateModel.Lockstep.Op
@@ -41,7 +44,13 @@
 data AnyGVar op where
   SomeGVar :: GVar op y -> AnyGVar op
 
-deriving instance (forall x. Show (op x a)) => Show (GVar op a)
+instance (forall x. Show (op x a)) => Show (GVar op a) where
+  showsPrec n (GVar v op) =
+      showParen (n >= 11)
+      $ showString "unsafeMkGVar "
+      . showsPrec 11 v
+      . showSpace
+      . showsPrec 11 op
 
 instance (forall x. Eq (op x a)) => Eq (GVar op a) where
   (==) = \(GVar x op) (GVar x' op') -> aux x x' op op'
@@ -54,9 +63,19 @@
             Nothing   -> False
             Just Refl -> (x, op) == (x', op')
 
+instance HasVariables (GVar op f) where
+  getAllVariables (GVar v _) = getAllVariables v
+
+instance HasVariables (AnyGVar op) where
+  getAllVariables (SomeGVar v) = getAllVariables v
+
 {-------------------------------------------------------------------------------
   Construction
 -------------------------------------------------------------------------------}
+
+-- | Only for pretty-printing counter-examples, do not use directly
+unsafeMkGVar :: Typeable a => Var a -> op a b -> GVar op b
+unsafeMkGVar = GVar
 
 fromVar :: (Operation op, Typeable a) => Var a -> GVar op a
 fromVar var = GVar var opIdentity
diff --git a/src/Test/QuickCheck/StateModel/Lockstep/Op.hs b/src/Test/QuickCheck/StateModel/Lockstep/Op.hs
--- a/src/Test/QuickCheck/StateModel/Lockstep/Op.hs
+++ b/src/Test/QuickCheck/StateModel/Lockstep/Op.hs
@@ -1,3 +1,5 @@
+{-# LANGUAGE TypeOperators #-}
+
 module Test.QuickCheck.StateModel.Lockstep.Op (
     Operation(..)
   , InterpretOp(..)
diff --git a/src/Test/QuickCheck/StateModel/Lockstep/Op/SumProd.hs b/src/Test/QuickCheck/StateModel/Lockstep/Op/SumProd.hs
--- a/src/Test/QuickCheck/StateModel/Lockstep/Op/SumProd.hs
+++ b/src/Test/QuickCheck/StateModel/Lockstep/Op/SumProd.hs
@@ -93,10 +93,9 @@
       _        -> go op
     where
       go :: Op x y -> String -> String
-      go OpId         = showString "id"
-      go OpFst        = showString "fst"
-      go OpSnd        = showString "snd"
-      go OpLeft       = showString "fromLeft"
-      go OpRight      = showString "fromRight"
-      go (OpComp g f) = go g . showString " . " . go f
-
+      go OpId         = showString "OpId"
+      go OpFst        = showString "OpFst"
+      go OpSnd        = showString "OpSnd"
+      go OpLeft       = showString "OpLeft"
+      go OpRight      = showString "OpRight"
+      go (OpComp g f) = go g . showString " `OpComp` " . go f