Support building with mtl-2.3.* (GHC 9.6)

This patch contains two changes needed to make `asl-translator` compile with
GHC 9.6:

* GHC 9.6 bundles `mtl-2.3.*`, which no longer re-exports `Control.Monad`
  and similar modules from `mtl`-related modules.  To accommodate this, various
  imports have been made more explicit.
* I have bumped the following submodules to bring in GHC 9.6–related changes:
  * `crucible`: GaloisInc/crucible#1102
  * `what4`: GaloisInc/what4#235

lib/Data/Parameterized/AssignTree.hs

@@ -43,10 +43,10 @@ module Data.Parameterized.AssignTree
   , revTraverseMapCtxTree
   ) where
 
-import           Unsafe.Coerce
-import           Data.Proxy
+import           Data.Functor.Identity (Identity(..))
 import           Data.Kind
-import           Control.Monad.Identity hiding (zipWithM)
+import           Data.Proxy
+import           Unsafe.Coerce
 
 import           Data.Parameterized.Context hiding (zipWithM)
 import qualified Data.Parameterized.Context as Ctx

lib/Language/ASL/Formulas/Normalize.hs

@@ -73,7 +73,7 @@ import           Prelude hiding ( fail )
 import           GHC.Stack
 import           GHC.TypeLits
 
-import           Control.Monad ( forM, void )
+import           Control.Monad ( forM, liftM, void )
 import           Control.Lens hiding (Index, (:>), Empty)
 import           Control.Monad.Fail
 
@@ -338,7 +338,7 @@ getUsedBVs :: Ctx.Assignment (WB.ExprBoundVar t) args
            -> RebindM t (Set (Some (WB.ExprBoundVar t)))
 getUsedBVs asn expr = do
   let allBvs = Set.fromList $ FC.toListFC Some asn
-  usedbvsSet <- IO.liftIO $ ME.liftM (Set.unions . map snd) $ ST.stToIO $ H.toList =<< WB.boundVars expr
+  usedbvsSet <- IO.liftIO $ liftM (Set.unions . map snd) $ ST.stToIO $ H.toList =<< WB.boundVars expr
   return $ Set.intersection allBvs usedbvsSet
 
 simplifiedSymFn :: forall t rets args

lib/Language/ASL/Translation/Driver.hs

@@ -778,7 +778,7 @@ reportStats sopts sm = do
   when (not (Set.null unexpectedElems)) $ do
     putStrLn $ "Unexpected exceptions:"
     forMwithKey_ (instrExcepts sm) $ \ident -> \e ->
-      E.when (unexpected (KeyInstr ident) e) $ do
+      when (unexpected (KeyInstr ident) e) $ do
         putStrLn $ prettyIdent ident ++ " failed to translate:"
         putStrLn $ show e
     putStrLn "----------------------"
@@ -807,7 +807,7 @@ reportStats sopts sm = do
     if not (Map.member ident (instrExcepts sm)) &&
        Set.null (Set.filter (\dep -> Map.member dep (funExcepts sm)) deps)
     then do
-      E.when (reportSucceedingInstructions sopts) $ putStrLn $ prettyIdent ident
+      when (reportSucceedingInstructions sopts) $ putStrLn $ prettyIdent ident
       return $ Just ident
     else return Nothing) (instrDeps sm)
   putStrLn $ "Number of successfully translated functions: " <> show (Map.size $ r)
@@ -819,7 +819,7 @@ reportStats sopts sm = do
       KeyInstr ident -> putStrLn $ "Instruction: " <> prettyIdent ident
       KeyFun nm -> do
         putStrLn $ "Function: " <> show nm
-        E.when (reportFunctionDependencies sopts) $ do
+        when (reportFunctionDependencies sopts) $ do
           putStrLn $ "Which is depended on by: "
           case Map.lookup nm reverseDependencyMap of
             Just instrs -> mapM_ (\ident -> putStrLn $  "    " <> prettyIdent ident) instrs

lib/Util/Log.hs

@@ -17,7 +17,9 @@ module Util.Log
   , WLog.LogCfg
   ) where
 
-import           Control.Monad.Identity
+import           Control.Monad (when)
+import           Data.Functor (void)
+import           Data.Functor.Identity (Identity)
 
 import qualified Control.Monad.IO.Class as IO