From e068194188b38cbcf3b10aa52f0574a4480418bb Mon Sep 17 00:00:00 2001
From: Langston Barrett <langston.barrett@gmail.com>
Date: Fri, 16 Aug 2024 16:43:28 -0400
Subject: [PATCH] cli: Allow clients to know `sym ~ ExprBuilder` for
 `ExtensionImpl`

---
 crucible-cli/src/Lang/Crucible/CLI.hs         | 6 ++++--
 crucible-cli/src/Lang/Crucible/CLI/Options.hs | 5 ++++-
 2 files changed, 8 insertions(+), 3 deletions(-)

diff --git a/crucible-cli/src/Lang/Crucible/CLI.hs b/crucible-cli/src/Lang/Crucible/CLI.hs
index b4ec6e1f1..13fde1727 100644
--- a/crucible-cli/src/Lang/Crucible/CLI.hs
+++ b/crucible-cli/src/Lang/Crucible/CLI.hs
@@ -114,7 +114,8 @@ defaultSimulateProgramHooks = SimulateProgramHooks
 
 simulateProgramWithExtension
    :: (IsSyntaxExtension ext, ?parserHooks :: ParserHooks ext)
-   => (forall sym bak. IsSymBackend sym bak => bak -> IO (ExtensionImpl () sym ext))
+   => (forall sym bak t st fs. (IsSymBackend sym bak, sym ~ ExprBuilder t st fs) =>
+        bak -> IO (ExtensionImpl () sym ext))
    -> FilePath -- ^ The name of the input (appears in source locations)
    -> Text     -- ^ The contents of the input
    -> Handle   -- ^ A handle that will receive the output
@@ -257,7 +258,8 @@ data Command
 -- line), and this function takes care of the rest.
 execCommand :: 
   (IsSyntaxExtension ext, ?parserHooks :: ParserHooks ext) =>
-  (forall sym bak. IsSymBackend sym bak => bak -> IO (ExtensionImpl () sym ext)) ->
+  (forall sym bak t st fs. (IsSymBackend sym bak, sym ~ ExprBuilder t st fs) =>
+    bak -> IO (ExtensionImpl () sym ext)) ->
   SimulateProgramHooks ext ->
   Command ->
   IO ()
diff --git a/crucible-cli/src/Lang/Crucible/CLI/Options.hs b/crucible-cli/src/Lang/Crucible/CLI/Options.hs
index f50f6b4ef..2d688f4b1 100644
--- a/crucible-cli/src/Lang/Crucible/CLI/Options.hs
+++ b/crucible-cli/src/Lang/Crucible/CLI/Options.hs
@@ -1,5 +1,6 @@
 {-# LANGUAGE ImplicitParams #-}
 {-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeOperators #-}
 
 module Lang.Crucible.CLI.Options (main) where
 
@@ -14,6 +15,8 @@ import           Options.Applicative ( (<**>) )
 
 import           Lang.Crucible.CLI
 
+import What4.Expr (ExprBuilder)
+
 file :: String -> Opt.Parser FilePath
 file which = Opt.strArgument (Opt.metavar "FILE" <> Opt.help ("The " <> which <> " file"))
 
@@ -53,7 +56,7 @@ parseCheck =
 main ::
   (?parserHooks :: ParserHooks ext, IsSyntaxExtension ext) =>
   String ->
-  (forall sym bak. IsSymBackend sym bak => bak -> IO (ExtensionImpl () sym ext)) ->
+  (forall sym bak t st fs. (IsSymBackend sym bak, sym ~ ExprBuilder t st fs) => bak -> IO (ExtensionImpl () sym ext)) ->
   SimulateProgramHooks ext ->
   IO ()
 main name ext simulationHooks =