Support building with GHC 9.6

Making SAW build with GHC 9.6 is almost entirely a matter of being more precise
with `mtl`-related imports to account for `mtl-2.3.1` not re-exporting as many
identifiers from `Control.Monad`, `Control.Monad.IO.Class`, etc.

I have also bumped the following submodules and `source-repository-package`s to
allow them to build with GHC 9.6:

* `cryptol`: GaloisInc/cryptol#1572
* `hobbits`: eddywestbrook/hobbits#9

cabal.project

@@ -48,4 +48,4 @@ packages:
 source-repository-package
     type: git
     location: https://github.com/eddywestbrook/hobbits.git
-    tag: b88cbfcad607a5ad05d9134e1f0b2461dd68c3d7
+    tag: 5fc80ffdce596ca81bf3b6583b1062891d16452c

crucible-mir-comp/src/Mir/Compositional/Clobber.hs

@@ -8,7 +8,8 @@ module Mir.Compositional.Clobber
 where
 
 import Control.Lens ((^.), (^?), ix)
-import Control.Monad.Except
+import Control.Monad (forM_)
+import Control.Monad.IO.Class (MonadIO(..))
 import qualified Data.Map as Map
 import qualified Data.Parameterized.Context as Ctx
 import Data.Parameterized.TraversableFC

cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs

@@ -77,9 +77,12 @@ import Data.Map.Strict (Map)
 import qualified Data.Map.Strict as Map
 import Data.IntMap.Strict (IntMap)
 import qualified Data.IntMap.Strict as IntMap
-import Control.Monad.Reader
-import Control.Monad.State
-import Control.Monad.Cont
+import Control.Monad ((>=>), foldM, forM_, zipWithM)
+import Control.Monad.Cont (Cont, cont, runCont)
+import Control.Monad.IO.Class (MonadIO(..))
+import Control.Monad.Reader (MonadReader(..), ReaderT(..))
+import Control.Monad.State (MonadState(..), StateT(..), evalStateT, modify)
+import Control.Monad.Trans (MonadTrans(..))
 import qualified Control.Monad.Fail as Fail
 -- import Control.Monad.IO.Class (MonadIO, liftIO)
 import qualified Data.Text as T

heapster-saw/src/Verifier/SAW/Heapster/CruUtil.hs

@@ -32,7 +32,7 @@ import Numeric
 import Numeric.Natural
 import qualified Data.BitVector.Sized as BV
 import System.FilePath
-import GHC.TypeNats
+import GHC.TypeNats (KnownNat, natVal)
 import Data.Functor.Product
 import Control.Lens hiding ((:>), Index, Empty, ix, op)
 import qualified Control.Monad.Fail as Fail

heapster-saw/src/Verifier/SAW/Heapster/GenMonad.hs

@@ -18,7 +18,8 @@ module Verifier.SAW.Heapster.GenMonad (
   ) where
 
 import Data.Binding.Hobbits ( nuMulti, nuMultiWithElim1, Mb, Name, RAssign )
-import Control.Monad.State ( ap, MonadState(get, put) )
+import Control.Monad ( ap )
+import Control.Monad.State ( MonadState(get, put) )
 import Control.Monad.Trans.Class ( MonadTrans(lift) )
 import Control.Monad.Trans.Reader
 import Data.Proxy

heapster-saw/src/Verifier/SAW/Heapster/IRTTranslation.hs

@@ -34,9 +34,10 @@ module Verifier.SAW.Heapster.IRTTranslation (
 import Numeric.Natural
 import Data.Functor.Const
 import GHC.TypeLits
-import Control.Monad.Reader
-import Control.Monad.State
-import Control.Monad.Except
+import Control.Monad (zipWithM)
+import Control.Monad.Except (MonadError(..))
+import Control.Monad.Reader (MonadReader(..), ReaderT(..), withReaderT)
+import Control.Monad.State (MonadState(..), State, evalState)
 
 import qualified Data.Type.RList as RL
 import Data.Binding.Hobbits

heapster-saw/src/Verifier/SAW/Heapster/Implication.hs

@@ -34,11 +34,13 @@ import Data.List
 import Data.Functor.Compose
 import Data.Reflection
 import qualified Data.BitVector.Sized as BV
-import GHC.TypeLits
+import GHC.TypeLits (KnownNat)
 import Control.Lens hiding ((:>), ix)
-import Control.Applicative
+import qualified Control.Applicative as App
+import Control.Monad (forM_)
 import Control.Monad.Extra (concatMapM)
-import Control.Monad.State.Strict hiding (ap)
+import Control.Monad.State.Strict (MonadState(..), State, StateT, evalState, execStateT)
+import Control.Monad.Trans.Class (MonadTrans(..))
 
 import qualified Data.Type.RList as RL
 import Data.Binding.Hobbits.MonadBind
@@ -316,7 +318,7 @@ instance Applicative SomeEqProof where
   liftA2 f (SomeEqProofRefl a) some_eqp = fmap (f a) some_eqp
   liftA2 f some_eqp (SomeEqProofRefl b) = fmap (flip f b) some_eqp
   liftA2 f (SomeEqProofCons eqp1 step1) (SomeEqProofCons eqp2 step2) =
-    SomeEqProofCons (liftA2 f eqp1 eqp2) (eqProofStepLiftA2 f step1 step2)
+    SomeEqProofCons (App.liftA2 f eqp1 eqp2) (eqProofStepLiftA2 f step1 step2)
 
 -- | An 'EqProofStep' with an existentially quantified list of permissions
 data SomeEqProofStep a = forall ps. SomeEqProofStep (EqProofStep ps a)
@@ -6085,7 +6087,7 @@ instance ProveEq (LLVMFramePerm w) where
     | mbLift mb_i == i =
       do eqp1 <- proveEq e mb_e
          eqp2 <- proveEq fperms mb_fperms
-         pure (liftA2 (\x y -> (x,i):y) eqp1 eqp2)
+         pure (App.liftA2 (\x y -> (x,i):y) eqp1 eqp2)
   proveEq perms mb =
     use implStatePPInfo >>>= \ppinfo ->
       implFailM $ EqualityProofError

heapster-saw/src/Verifier/SAW/Heapster/LLVMGlobalConst.hs

@@ -12,8 +12,10 @@ module Verifier.SAW.Heapster.LLVMGlobalConst (
 
 import Data.Bits
 import Data.List
-import Control.Monad.Reader
-import GHC.TypeLits
+import Control.Monad (MonadPlus(..))
+import Control.Monad.Reader (MonadReader(..), ReaderT(..))
+import Control.Monad.Trans.Class (MonadTrans(..))
+import GHC.TypeLits (KnownNat)
 import qualified Text.PrettyPrint.HughesPJ as PPHPJ
 
 import qualified Data.BitVector.Sized as BV

heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs

@@ -46,17 +46,18 @@ import Data.Functor.Compose
 import qualified Data.BitVector.Sized as BV
 import Data.BitVector.Sized (BV)
 import Numeric.Natural
-import GHC.TypeLits
+import GHC.TypeLits (KnownNat, natVal)
 import Data.Kind
 import Data.Map.Strict (Map)
 import qualified Data.Map.Strict as Map
 import Data.Set (Set)
 import qualified Data.Set as Set
 import Control.Applicative hiding (empty)
+import Control.Monad (MonadPlus(..))
 import Control.Monad.Extra (concatMapM)
-import Control.Monad.Identity hiding (ap)
-import Control.Monad.State hiding (ap)
-import Control.Monad.Reader hiding (ap)
+import Control.Monad.Identity ()
+import Control.Monad.Reader (MonadReader(..), Reader, ReaderT(..), runReader)
+import Control.Monad.State (MonadState(..), State, evalState, modify)
 import Control.Lens hiding ((:>), Index, Empty, ix, op)
 
 import Data.Binding.Hobbits hiding (sym)

heapster-saw/src/Verifier/SAW/Heapster/RustTypes.hs

@@ -36,9 +36,11 @@ import GHC.TypeLits
 import qualified Data.BitVector.Sized as BV
 import Data.Functor.Constant
 import Data.Functor.Product
-import Control.Applicative
-import Control.Monad.Reader
-import Control.Monad.Except
+import qualified Control.Applicative as App
+import Control.Monad (MonadPlus(..))
+import Control.Monad.Except (Except, MonadError(..), runExcept)
+import Control.Monad.Reader (MonadReader(..), ReaderT(..), asks)
+import Control.Monad.Trans.Class (MonadTrans(..))
 import Control.Monad.Trans.Maybe
 import qualified Control.Monad.Fail as Fail
 
@@ -1313,7 +1315,7 @@ data SomeMbWithPerms a where
 instance Functor SomeMbWithPerms where
   fmap f (SomeMbWithPerms ctx ps mb_a) = SomeMbWithPerms ctx ps (fmap f mb_a)
 
-instance Applicative SomeMbWithPerms where
+instance App.Applicative SomeMbWithPerms where
   pure a = SomeMbWithPerms CruCtxNil (emptyMb MNil) $ emptyMb a
   liftA2 f (SomeMbWithPerms ctx1 mb_ps1 mb_a1) (SomeMbWithPerms ctx2 mb_ps2 mb_a2) =
     SomeMbWithPerms (appendCruCtx ctx1 ctx2)

heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs

@@ -36,16 +36,17 @@ import Data.Maybe
 import Numeric.Natural
 import Data.List hiding (inits)
 import Data.Text (pack)
-import GHC.TypeLits
+import GHC.TypeLits (KnownNat, natVal)
 import Data.BitVector.Sized (BV)
 import qualified Data.BitVector.Sized as BV
 import Data.Functor.Compose
-import Control.Applicative
+import qualified Control.Applicative as App
 import Control.Lens hiding ((:>), Index, ix, op)
-import Control.Monad.Reader hiding (ap)
-import Control.Monad.Writer hiding (ap)
-import Control.Monad.State hiding (ap)
+import Control.Monad (MonadPlus(..), zipWithM)
+import Control.Monad.Reader (MonadReader(..), Reader, runReader, withReader)
+import Control.Monad.State (MonadState(..), StateT, evalStateT)
 import Control.Monad.Trans.Maybe
+import Control.Monad.Writer (MonadWriter(..), Writer, runWriter)
 import qualified Control.Monad.Fail as Fail
 
 import What4.ProgramLoc
@@ -212,7 +213,7 @@ strictTupleTypeTrans ttrans =
 -- | Build a type translation for a list of translations
 listTypeTrans :: [TypeTrans tr] -> TypeTrans [tr]
 listTypeTrans [] = pure []
-listTypeTrans (trans:transs) = liftA2 (:) trans $ listTypeTrans transs
+listTypeTrans (trans:transs) = App.liftA2 (:) trans $ listTypeTrans transs
 
 
 -- | The result of translating a 'PermExpr' at 'CrucibleType' @a@. This is a
@@ -879,7 +880,7 @@ instance TransInfo info =>
   translate mb_ctx = case mbMatch mb_ctx of
     [nuMP| CruCtxNil |] -> return $ mkTypeTrans0 MNil
     [nuMP| CruCtxCons ctx tp |] ->
-      liftA2 (:>:) <$> translate ctx <*> translate tp
+      App.liftA2 (:>:) <$> translate ctx <*> translate tp
 
 -- | Translate all types in a Crucible context and lambda-abstract over them
 lambdaExprCtx :: TransInfo info => CruCtx ctx -> TransM info ctx OpenTerm ->
@@ -1985,7 +1986,7 @@ instance TransInfo info =>
   translate mb_ps = case mbMatch mb_ps of
     [nuMP| ValPerms_Nil |] -> return $ mkTypeTrans0 MNil
     [nuMP| ValPerms_Cons ps p |] ->
-      liftA2 (:>:) <$> translate ps <*> translate p
+      App.liftA2 (:>:) <$> translate ps <*> translate p
 
 -- Translate a DistPerms by translating its corresponding ValuePerms
 instance TransInfo info =>

heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs

@@ -38,15 +38,18 @@ import Data.Type.Equality
 import Data.Kind
 import Data.Reflection
 import qualified Data.BitVector.Sized as BV
-import GHC.TypeLits
+import GHC.TypeLits (KnownNat)
 
 import What4.ProgramLoc
 import What4.FunctionName
 import What4.Interface (StringLiteral(..))
 
 import Control.Lens hiding ((:>), Index, ix)
-import Control.Monad.State.Strict hiding (ap)
-import Control.Monad.Reader hiding (ap)
+import Control.Monad ((>=>), foldM, forM, forM_)
+import Control.Monad.Reader (MonadReader(..), ReaderT(..))
+import Control.Monad.State.Strict (MonadState(..), State, evalState, execState,
+                                   gets, modify, runState)
+import Control.Monad.Trans.Class (MonadTrans(..))
 
 import Prettyprinter as PP
 

heapster-saw/src/Verifier/SAW/Heapster/Widening.hs

@@ -31,11 +31,13 @@ module Verifier.SAW.Heapster.Widening where
 
 import Data.Maybe
 import Data.List
+import Data.Functor (void)
 import Data.Functor.Constant
 import Data.Functor.Product
-import Control.Monad.State
--- import Control.Monad.Cont
-import GHC.TypeLits
+import Control.Monad (ap, zipWithM)
+import Control.Monad.State (MonadState(..), StateT(..), modify)
+import Control.Monad.Trans.Class (MonadTrans(..))
+import GHC.TypeLits (KnownNat)
 import Control.Lens hiding ((:>), Index, Empty, ix, op)
 import Control.Monad.Extra (concatMapM)
 

saw-core-coq/src/Verifier/SAW/Translation/Coq.hs

@@ -21,7 +21,6 @@ module Verifier.SAW.Translation.Coq (
   translateSAWModule,
   ) where
 
-import           Control.Monad.Reader                          hiding (fail)
 import           Data.String.Interpolate                       (i)
 import           Prelude                                       hiding (fail)
 import           Prettyprinter

saw-core-coq/src/Verifier/SAW/Translation/Coq/Monad.hs

@@ -22,8 +22,8 @@ module Verifier.SAW.Translation.Coq.Monad
   ) where
 
 import qualified Control.Monad.Except as Except
-import Control.Monad.Reader hiding (fail)
-import Control.Monad.State hiding (fail, state)
+import Control.Monad.Reader (MonadReader, ReaderT(..))
+import Control.Monad.State (MonadState, StateT(..))
 import Prelude hiding (fail)
 
 import Verifier.SAW.SharedTerm

saw-core-coq/src/Verifier/SAW/Translation/Coq/SAWModule.hs

@@ -25,7 +25,7 @@ Portability : portable
 module Verifier.SAW.Translation.Coq.SAWModule where
 
 import qualified Control.Monad.Except                          as Except
-import           Control.Monad.Reader                          hiding (fail)
+import           Control.Monad.Reader                          (asks)
 import           Prelude                                       hiding (fail)
 import           Prettyprinter                                 (Doc, pretty)
 

saw-core-coq/src/Verifier/SAW/Translation/Coq/Term.hs

@@ -30,10 +30,11 @@ Portability : portable
 module Verifier.SAW.Translation.Coq.Term where
 
 import           Control.Lens                                  (makeLenses, over, set, to, view)
+import           Control.Monad                                 (forM)
 import qualified Control.Monad.Except                          as Except
 import qualified Control.Monad.Fail                            as Fail
-import           Control.Monad.Reader                          hiding (fail, fix)
-import           Control.Monad.State                           hiding (fail, fix, state)
+import           Control.Monad.Reader                          (MonadReader(ask, local), asks)
+import           Control.Monad.State                           (MonadState(get), modify)
 import           Data.Char                                     (isDigit)
 import           Data.IntMap.Strict (IntMap)
 import qualified Data.IntMap.Strict                            as IntMap

saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs

@@ -59,8 +59,9 @@ import Data.Traversable as T
 #if !MIN_VERSION_base(4,8,0)
 import Control.Applicative
 #endif
+import Control.Monad ((<=<), (>=>), foldM, unless, void)
 import Control.Monad.IO.Class
-import Control.Monad.State as ST
+import Control.Monad.State as ST (MonadState(..), StateT(..), evalStateT, modify)
 import Numeric.Natural (Natural)
 
 import qualified Verifier.SAW.Prim as Prim

saw-core-what4/src/Verifier/SAW/Simulator/What4.hs

@@ -79,7 +79,9 @@ import Data.Traversable as T
 import Control.Applicative
 #endif
 import qualified Control.Exception as X
-import Control.Monad.State as ST
+import Control.Monad ((<=<), foldM, unless)
+import Control.Monad.State as ST (MonadState(..), StateT(..), evalStateT, modify)
+import Control.Monad.Trans.Class (MonadTrans(..))
 import Numeric.Natural (Natural)
 
 -- saw-core

saw-core-what4/src/Verifier/SAW/Simulator/What4/PosNat.hs

@@ -42,7 +42,7 @@
 module Verifier.SAW.Simulator.What4.PosNat where
 -- TODO: find the right place for this code
 
-import GHC.TypeNats
+import GHC.TypeNats (KnownNat, Nat)
 import Data.Parameterized.NatRepr
 import Data.Parameterized.Some(Some(..))
 

saw-core/src/Verifier/SAW/Change.hs

@@ -24,7 +24,7 @@ module Verifier.SAW.Change
   , flatten
   ) where
 
-import Control.Applicative (liftA2)
+import qualified Control.Applicative as App (liftA2)
 import Control.Monad (liftM)
 import Control.Monad.Trans
 
@@ -110,7 +110,7 @@ instance Functor m => Functor (ChangeT m) where
 
 instance Applicative m => Applicative (ChangeT m) where
   pure x = ChangeT (pure (Original x))
-  ChangeT m1 <*> ChangeT m2 = ChangeT (liftA2 (<*>) m1 m2)
+  ChangeT m1 <*> ChangeT m2 = ChangeT (App.liftA2 (<*>) m1 m2)
 
 instance Monad m => Monad (ChangeT m) where
   return = pure

saw-core/src/Verifier/SAW/ExternalFormat.hs

@@ -17,7 +17,9 @@ module Verifier.SAW.ExternalFormat (
   scWriteExternal, scReadExternal
   ) where
 
-import Control.Monad.State.Strict as State
+import Control.Monad (forM)
+import qualified Control.Monad.State.Strict as State
+import Control.Monad.Trans.Class (MonadTrans(..))
 #if !MIN_VERSION_base(4,8,0)
 import Data.Traversable
 #endif
@@ -221,7 +223,7 @@ scReadExternal sc input =
          tf <- parse tokens
          t <- lift $ scTermF sc tf
          (ts, nms, vs) <- State.get
-         put (Map.insert i t ts, nms, vs)
+         State.put (Map.insert i t ts, nms, vs)
     go [] = pure () -- empty lines are ignored
 
     readM :: forall a. Read a => String -> ReadM a

saw-core/src/Verifier/SAW/FiniteValue.hs

@@ -17,7 +17,7 @@ import Data.Traversable
 #endif
 
 import GHC.Generics (Generic)
-import Control.Monad (mzero)
+import Control.Monad (replicateM, mzero)
 import Control.Monad.Trans (lift)
 import Control.Monad.Trans.Maybe
 import qualified Control.Monad.State as S
@@ -355,7 +355,7 @@ readFiniteValue' en ft =
                      case bs of
                        []      -> S.lift Nothing
                        b : bs' -> S.put bs' >> return (FVBit b)
-    FTVec n t  -> (fvVec t . fixup) <$> S.replicateM (fromIntegral n) (readFiniteValue' en t)
+    FTVec n t  -> (fvVec t . fixup) <$> replicateM (fromIntegral n) (readFiniteValue' en t)
                     where fixup = case (t, en) of
                                     (FTBit, LittleEndian) -> reverse
                                     _ -> id

saw-core/src/Verifier/SAW/ParserUtils.hs

@@ -27,7 +27,9 @@ module Verifier.SAW.ParserUtils
 #if !MIN_VERSION_base(4,8,0)
 import Control.Applicative
 #endif
-import Control.Monad.State
+import Control.Monad (forM_)
+import Control.Monad.State (StateT, execStateT, modify)
+import Control.Monad.Trans.Class (MonadTrans(..))
 import qualified Data.ByteString.Lazy as BL
 #if !MIN_VERSION_template_haskell(2,8,0)
 import qualified Data.ByteString.Lazy.UTF8 as UTF8