Merge branch 'develop-ghc-9.6.3'. Close #491.

**Description**

`copilot-theorem` is failing to compile with GHC 9.6.3. This is because
the module `Control.Monad.State` no longer re-exports `Control.Monad`,
so the functions `ap`, `forM`, `when`, `liftM` and `liftM2` are not in
scope. Another issue is that `System.Directory` can no longer be
imported safely. These errors are causing the build to fail on hackage,
which uses GHC 9.6.3.

**Type**

- Bug: Failure to compile with version of dependency.

**Additional context**

- haskell/directory#147

**Requester**

- Ivan Perez

**Method to check presence of bug**

The following Dockerfile checks whether Copilot can be installed with
GHC 9.6, in which case it prints the message Success:

```Dockerfile
FROM ubuntu:focal

RUN apt-get update

RUN apt-get install --yes libz-dev
RUN apt-get install --yes git

RUN apt-get install --yes wget
RUN mkdir -p $HOME/.ghcup/bin
RUN wget https://downloads.haskell.org/~ghcup/0.1.17.7/x86_64-linux-ghcup-0.1.17.7 -O $HOME/.ghcup/bin/ghcup

RUN chmod a+x $HOME/.ghcup/bin/ghcup
ENV PATH=$PATH:/root/.ghcup/bin/
ENV PATH=$PATH:/root/.cabal/bin/
RUN apt-get install --yes curl
RUN apt-get install --yes gcc g++ make libgmp3-dev

RUN ghcup install ghc 9.6.3
RUN ghcup install cabal 3.4
RUN ghcup set ghc 9.6.3
RUN cabal update

SHELL ["/bin/bash", "-c"]
CMD git clone $REPO \
    && cd $NAME \
    && git checkout $COMMIT \
    && cabal install --lib copilot**/ \
    && echo Success
```

Command (substitute variables based on new path after merge):
```
$ docker run -e "REPO=https://github.com/Copilot-Language/copilot" -e "NAME=copilot" -e "COMMIT=<HASH>" -it copilot-verify-491
```

**Expected result**

Compiling with GHC 9.6 succeeds. Running the above image prints the
message Success, indicating that Copilot can be compile with GHC 9.6.3.

**Solution implemented**

Modify `copilot-theorem` to import `Control.Monad` explicitly, instead of via
re-exports from other modules.

Modify the module that imports `System.Directory` so that it is marked
as trustworthy instead of Safe.

**Further notes**

None.

Author: ivanperez-keera

copilot-theorem/CHANGELOG

@@ -1,3 +1,6 @@
+2024-01-07
+        * Adjust to work with GHC 9.6. (#491)
+
 2024-01-07
         * Version bump (3.18). (#487)
         * Introduce testing infrastructure for Copilot.Theorem.What4. (#474)

copilot-theorem/src/Copilot/Theorem/IL/Translate.hs

@@ -14,6 +14,7 @@ import qualified Copilot.Core as C
 
 import qualified Data.Map.Strict as Map
 
+import Control.Monad       (forM, liftM2, when)
 import Control.Monad.State
 
 import Data.Char

copilot-theorem/src/Copilot/Theorem/Misc/Utils.hs

@@ -1,4 +1,4 @@
-{-# LANGUAGE Safe #-}
+{-# LANGUAGE Trustworthy #-}
 
 -- | Utility / auxiliary functions.
 module Copilot.Theorem.Misc.Utils

copilot-theorem/src/Copilot/Theorem/Prove.hs

@@ -22,6 +22,7 @@ import qualified Copilot.Core as Core
 
 import Data.List (intercalate)
 import Control.Applicative (liftA2)
+import Control.Monad        (ap, liftM)
 import Control.Monad.Writer
 
 -- | Output produced by a prover, containing the 'Status' of the proof and

copilot-theorem/src/Copilot/Theorem/TransSys/Translate.hs

@@ -47,6 +47,7 @@ import Copilot.Theorem.TransSys.Spec
 import Copilot.Theorem.TransSys.Cast
 import Copilot.Theorem.Misc.Utils
 
+import Control.Monad            (liftM, liftM2, unless)
 import Control.Monad.State.Lazy
 
 import Data.Char (isNumber)

copilot-theorem/src/Copilot/Theorem/What4.hs

@@ -57,6 +57,7 @@ import qualified What4.InterpretedFloatingPoint as WFP
 import qualified What4.Solver                   as WS
 import qualified What4.Solver.DReal             as WS
 
+import Control.Monad (forM)
 import Control.Monad.State
 import qualified Data.BitVector.Sized as BV
 import Data.Foldable (foldrM)

copilot/CHANGELOG

@@ -1,3 +1,6 @@
+2024-01-07
+        * Update README to reflect support for GHC 9.6. (#491)
+
 2024-01-07
         * Version bump (3.18). (#487)
         * Enable tests for copilot-theorem in CI script. (#474)

copilot/README.md

@@ -81,7 +81,7 @@ ghci> ghci> Leaving GHCi.
 On other Linux distributions or older Debian-based distributions, to use
 Copilot you must install a Haskell compiler (GHC) and the package manager
 Cabal. We currently support all versions of GHC from 8.6.5 to modern versions
-(9.4 as of this writing). You can install the toolchain using
+(9.6 as of this writing). You can install the toolchain using
 [ghcup](https://www.haskell.org/ghcup/) or, if you are on Debian/Ubuntu,
 directly with `apt-get`:
 
@@ -111,7 +111,7 @@ ghci> ghci> Leaving GHCi.
 
 To use Copilot you must have a Haskell compiler (GHC) and the package manager
 Cabal. We currently support all versions of GHC from 8.6.5 to modern versions
-(9.4 as of this writing). You can install the toolchain using
+(9.6 as of this writing). You can install the toolchain using
 [ghcup](https://www.haskell.org/ghcup/), as well as with Homebrew:
 
 ```sh