More warning cleanup and fixes for GHC 9.6

src/Pate/Discovery/PLT.hs

@@ -7,6 +7,7 @@
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE TypeOperators #-}
 
 module Pate.Discovery.PLT (
     PLTStubInfo(..)

src/Pate/ExprMappable.hs

@@ -16,8 +16,6 @@
 {-# LANGUAGE DefaultSignatures #-}
 {-# LANGUAGE LambdaCase #-}
 
--- must come after TypeFamilies, see also https://gitlab.haskell.org/ghc/ghc/issues/18006
-{-# LANGUAGE NoMonoLocalBinds #-}
 {-# OPTIONS_GHC -fno-warn-simplifiable-class-constraints #-}
 
 module Pate.ExprMappable (
@@ -63,7 +61,6 @@ import qualified Lang.Crucible.Utils.MuxTree as MT
 import Data.Parameterized.Map (MapF)
 import qualified Data.Parameterized.TraversableF as TF
 import Data.Text
-import Control.Monad (forM)
 
 -- Expression binding
 

src/Pate/Ground.hs

@@ -28,8 +28,6 @@ Grounding symbolic expressions
 {-# LANGUAGE MultiWayIf #-}
 {-# LANGUAGE ImplicitParams #-}
 
--- must come after TypeFamilies, see also https://gitlab.haskell.org/ghc/ghc/issues/18006
-{-# LANGUAGE NoMonoLocalBinds #-}
 
 module Pate.Ground 
   ( IsGroundSym

src/Pate/IOReplay.hs

@@ -73,7 +73,7 @@ data IOAction ret = IOActionValue ret =>
   IOAction { ioActionArgs  :: [IOActionArg], ioActionRet :: ret }
 
 data IOActionStore = 
-  IOActionStore { storeQueued :: [T.Text], storeActions :: [Some IOAction], storeDesync :: Bool }
+  IOActionStore { _storeQueued :: [T.Text], _storeActions :: [Some IOAction], _storeDesync :: Bool }
 
 ioActionStore :: MVar IOActionStore
 ioActionStore = unsafePerformIO (newMVar (IOActionStore [] [] False))

src/Pate/Solver.hs

@@ -2,6 +2,7 @@
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeOperators #-}
 -- | Definitions of solvers usable in the pate verifier
 module Pate.Solver (
     Solver(..)
@@ -26,7 +27,6 @@ import qualified What4.Solver as WS
 
 import qualified Lang.Crucible.Backend as CB
 import qualified Lang.Crucible.Backend.Online as CBO
-import Data.Data (Typeable)
 import qualified What4.JSON as W4S
 
 -- | The solvers supported by the pate verifier

src/Pate/TraceTree.hs

@@ -916,7 +916,7 @@ choice_ header name label v f = do
 
 getChoice ::
   forall k m nm_choice a.
-  MonadIO m =>
+  IO.MonadIO m =>
   --IsTreeBuilder k e m =>
   [Choice k nm_choice a] ->
   m (Maybe a)
@@ -1014,7 +1014,7 @@ class Monad m => MonadTreeBuilder k m | m -> k where
   withTreeBuilder :: forall a. TreeBuilder k -> m a -> m a
 
 newtype NoTreeBuilder k m a = NoTreeBuilder (m a)
-  deriving (Applicative, Functor, Monad, MonadIO, MonadThrow)
+  deriving (Applicative, Functor, Monad, IO.MonadIO, MonadThrow)
 
 instance Monad m => MonadTreeBuilder k (NoTreeBuilder k m) where
   getTreeBuilder = return $ noTreeBuilder

src/Pate/Verification/Override.hs

@@ -1,6 +1,7 @@
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeOperators #-}
 module Pate.Verification.Override (
     Override(..)
   , SomeOverride(..)

src/What4/ExprHelpers.hs

@@ -84,15 +84,11 @@ import           Unsafe.Coerce ( unsafeCoerce ) -- for mulMono axiom
 import           Control.Lens ( (.~), (&), (^.) )
 
 import           Control.Applicative
-import           Control.Monad (foldM)
 import           Control.Monad.Except
-import           Control.Monad.IO.Class (MonadIO, liftIO)
 import qualified Control.Monad.IO.Class as IO
 import qualified Control.Monad.IO.Unlift as IO
 import           Control.Monad.ST ( RealWorld, stToIO )
 import qualified Control.Monad.Writer as CMW
-import qualified Control.Monad.State as CMS
-import           Control.Monad.Trans (lift)
 import           Control.Monad.Trans.Maybe (MaybeT, runMaybeT)
 import qualified System.IO as IO
 
@@ -133,7 +129,6 @@ import qualified What4.Utils.AbstractDomains as W4AD
 
 import           Data.Parameterized.SetF (SetF)
 import qualified Data.Parameterized.SetF as SetF
-import Data.Maybe (fromMaybe)
 
 -- | Sets the abstract domain of the given integer to assume
 --   that it is positive. 

src/What4/JSON.hs

@@ -31,7 +31,7 @@ module What4.JSON
   , (.=~)
   ) where
 
-import           Control.Monad.State (MonadState (..), State, modify, evalState, runState)
+import           Control.Monad.State (MonadState (..), modify)
 
 import qualified Data.Map.Ordered as OMap
 import           Data.Map (Map)
@@ -47,13 +47,11 @@ import qualified What4.Serialize.Printer as W4S
 import qualified What4.Serialize.Parser as W4D
 import qualified What4.Expr.Builder as W4B
 import qualified Data.Map as Map
-import Control.Monad (forM)
 import qualified What4.PredMap as W4P
 import Data.Parameterized.HasRepr
 import qualified What4.Concrete as W4
 import qualified Data.Text as T
-import GHC.IO (catch, evaluate, unsafePerformIO)
-import GHC.IO.Exception (IOException)
+import GHC.IO (evaluate)
 import Control.DeepSeq (force)
 import Data.Parameterized.Map (MapF)
 import qualified Data.Parameterized.Map as MapF

src/What4/PathCondition.hs

@@ -36,8 +36,6 @@ module What4.PathCondition
 
 import           Control.Applicative
 import           Control.Monad.Except
-import           Control.Monad.Plus
-import           Control.Monad.IO.Class (liftIO)
 import qualified Control.Monad.IO.Class as IO
 import qualified Control.Monad.Reader as CMR
 import qualified Control.Monad.State as CMS