diff --git a/what4/src/What4/Interface.hs b/what4/src/What4/Interface.hs
index 010e3456..3a3c8d69 100644
--- a/what4/src/What4/Interface.hs
+++ b/what4/src/What4/Interface.hs
@@ -79,6 +79,8 @@ module What4.Interface
   , IsExprBuilder(..)
   , IsSymExprBuilder(..)
   , SolverEvent(..)
+  , SolverStartSATQuery(..)
+  , SolverEndSATQuery(..)
 
     -- ** Bitvector operations
   , bvJoinVector
@@ -392,11 +394,17 @@ instance HashableF e => HashableF (ArrayResultWrapper e idx) where
 --   installed via @setSolverLogListener@ whenever an interesting
 --   event occurs.
 data SolverEvent
-  = SolverStartSATQuery
+  = SolverStartSATQuery SolverStartSATQuery
+  | SolverEndSATQuery SolverEndSATQuery
+ deriving (Show, Generic)
+
+data SolverStartSATQuery = SolverStartSATQueryRec
     { satQuerySolverName :: !String
     , satQueryReason     :: !String
     }
-  | SolverEndSATQuery
+ deriving (Show, Generic)
+
+data SolverEndSATQuery = SolverEndSATQueryRec
     { satQueryResult     :: !(SatResult () ())
     , satQueryError      :: !(Maybe String)
     }
diff --git a/what4/src/What4/Protocol/Online.hs b/what4/src/What4/Protocol/Online.hs
index e715b18e..065f2918 100644
--- a/what4/src/What4/Protocol/Online.hs
+++ b/what4/src/What4/Protocol/Online.hs
@@ -58,7 +58,9 @@ import           System.Process
                    (ProcessHandle, terminateProcess, waitForProcess)
 
 import           What4.Expr
-import           What4.Interface (SolverEvent(..))
+import           What4.Interface (SolverEvent(..)
+                                 , SolverStartSATQuery(..)
+                                 , SolverEndSATQuery(..) )
 import           What4.ProblemFeatures
 import           What4.Protocol.SMTWriter
 import           What4.SatResult
@@ -320,17 +322,17 @@ checkWithAssumptions proc rsn ps =
          do tms <- forM ps (mkFormula conn)
             nms <- forM tms (freshBoundVarName conn EqualityDefinition [] BoolTypeMap)
             solverLogFn proc
-              SolverStartSATQuery
+              (SolverStartSATQuery $ SolverStartSATQueryRec
               { satQuerySolverName = solverName proc
               , satQueryReason = rsn
-              }
+              })
             addCommands conn (checkWithAssumptionsCommands conn nms)
             sat_result <- getSatResult proc
             solverLogFn proc
-              SolverEndSATQuery
+              (SolverEndSATQuery $ SolverEndSATQueryRec
               { satQueryResult = sat_result
               , satQueryError = Nothing
-              }
+              })
             return (nms, sat_result)
 
 checkWithAssumptionsAndModel ::
@@ -355,17 +357,17 @@ check p rsn =
     Nothing ->
       do let c = solverConn p
          solverLogFn p
-           SolverStartSATQuery
+           (SolverStartSATQuery $ SolverStartSATQueryRec
            { satQuerySolverName = solverName p
            , satQueryReason = rsn
-           }
+           })
          addCommands c (checkCommands c)
          sat_result <- getSatResult p
          solverLogFn p
-           SolverEndSATQuery
+           (SolverEndSATQuery $ SolverEndSATQueryRec
            { satQueryResult = sat_result
            , satQueryError = Nothing
-           }
+           })
          return sat_result
 
 -- | Send a check command to the solver and get the model in the case of a SAT result.
diff --git a/what4/src/What4/Protocol/SMTLib2.hs b/what4/src/What4/Protocol/SMTLib2.hs
index 97644950..6d611621 100644
--- a/what4/src/What4/Protocol/SMTLib2.hs
+++ b/what4/src/What4/Protocol/SMTLib2.hs
@@ -1051,10 +1051,10 @@ class (SMTLib2Tweaks a, Show a) => SMTLib2GenericSolver a where
     -> IO b
   runSolverInOverride solver ack feats sym logData predicates cont = do
     I.logSolverEvent sym
-      I.SolverStartSATQuery
+      (I.SolverStartSATQuery $ I.SolverStartSATQueryRec
         { I.satQuerySolverName = show solver
         , I.satQueryReason     = logReason logData
-        }
+        })
     path <- defaultSolverPath solver sym
     withSolver solver ack feats sym path (logData{logVerbosity=2}) $ \session -> do
       -- Assume the predicates hold.
@@ -1062,10 +1062,10 @@ class (SMTLib2Tweaks a, Show a) => SMTLib2GenericSolver a where
       -- Run check SAT and get the model back.
       runCheckSat session $ \result -> do
         I.logSolverEvent sym
-          I.SolverEndSATQuery
+          (I.SolverEndSATQuery $ I.SolverEndSATQueryRec
             { I.satQueryResult = forgetModelAndCore result
             , I.satQueryError  = Nothing
-            }
+            })
         cont result
 
 -- | A default method for writing SMTLib2 problems without any
diff --git a/what4/src/What4/Solver/DReal.hs b/what4/src/What4/Solver/DReal.hs
index 6ded04e8..31da1ffa 100644
--- a/what4/src/What4/Solver/DReal.hs
+++ b/what4/src/What4/Solver/DReal.hs
@@ -275,10 +275,10 @@ runDRealInOverride sym logData ps modelFn = do
   p <- andAllOf sym folded ps
   solver_path <- findSolverPath drealPath (getConfiguration sym)
   logSolverEvent sym
-    SolverStartSATQuery
+    (SolverStartSATQuery $ SolverStartSATQueryRec
     { satQuerySolverName = "dReal"
     , satQueryReason = logReason logData
-    }
+    })
   withProcessHandles solver_path ["--model", "--in", "--format", "smt2"] Nothing $ \(in_h, out_h, err_h, ph) -> do
 
       -- Log stderr to output.
@@ -338,10 +338,10 @@ runDRealInOverride sym logData ps modelFn = do
           logCallbackVerbose logData 2 "dReal terminated."
 
           logSolverEvent sym
-             SolverEndSATQuery
+             (SolverEndSATQuery $ SolverEndSATQueryRec
              { satQueryResult = forgetModelAndCore res
              , satQueryError  = Nothing
-             }
+             })
 
           return r
         ExitFailure exit_code ->
diff --git a/what4/src/What4/Solver/Yices.hs b/what4/src/What4/Solver/Yices.hs
index 18e1ad2d..8e42d856 100644
--- a/what4/src/What4/Solver/Yices.hs
+++ b/what4/src/What4/Solver/Yices.hs
@@ -1113,10 +1113,10 @@ runYicesInOverride sym logData conditions resultFn = do
   logCallbackVerbose logData 2 "Calling Yices to check sat"
   -- Check Problem features
   logSolverEvent sym
-    SolverStartSATQuery
+    (SolverStartSATQuery $ SolverStartSATQueryRec
     { satQuerySolverName = "Yices"
     , satQueryReason = logReason logData
-    }
+    })
   features <- checkSupportedByYices condition
   enableMCSat <- getOpt =<< getOptionSetting yicesEnableMCSat cfg
   goalTimeout <- SolverGoalTimeout <$> (getOpt =<< getOptionSetting yicesGoalTimeout cfg)
@@ -1168,10 +1168,10 @@ runYicesInOverride sym logData conditions resultFn = do
                              }
       sat_result <- getSatResult yp
       logSolverEvent sym
-        SolverEndSATQuery
+        (SolverEndSATQuery $ SolverEndSATQueryRec
         { satQueryResult = sat_result
         , satQueryError  = Nothing
-        }
+        })
       r <-
          case sat_result of
            Sat () -> resultFn . Sat =<< getModel yp
diff --git a/what4/what4.cabal b/what4/what4.cabal
index 714b35fc..3f7dda81 100644
--- a/what4/what4.cabal
+++ b/what4/what4.cabal
@@ -58,6 +58,7 @@ common bldflags
                -Werror=missing-methods
                -Werror=overlapping-patterns
                -Wcompat
+               -Wpartial-fields
 
 common testdefs
   hs-source-dirs: test