Support building with GHC 9.4

.github/workflows/gen_matrix.pl

@@ -92,6 +92,7 @@
 
 version(ubuntu, "ubuntu-latest").
 
+version(ghc, "9.4.4").
 version(ghc, "9.2.2").
 version(ghc, "9.0.2").
 version(ghc, "8.10.7").

.github/workflows/test.yml

@@ -103,6 +103,7 @@ jobs:
             8.6.5) GHC_NIXPKGS=github:nixos/nixpkgs/20.09 ;;
             9.0.2) GHC_NIXPKGS=github:nixos/nixpkgs/nixos-22.05 ;;
             9.2.2) GHC_NIXPKGS=github:nixos/nixpkgs/nixos-22.05 ;;
+            9.4.4) GHC_NIXPKGS=github:nixos/nixpkgs/nixos-unstable ;;
             *)     GHC_NIXPKGS=github:nixos/nixpkgs/21.11 ;;
           esac
           echo NS="nix shell ${GHC_NIXPKGS}#cabal-install ${GHC_NIXPKGS}#${GHC} nixpkgs#gmp nixpkgs#zlib nixpkgs#zlib.dev" >> $GITHUB_ENV

what4-abc/what4-abc.cabal

@@ -17,7 +17,7 @@ Description:
 
 library
   build-depends:
-    base >= 4.7 && < 4.17,
+    base >= 4.7 && < 4.18,
     aig,
     abcBridge >= 0.11,
     bv-sized >= 1.0.0,

what4-blt/what4-blt.cabal

@@ -26,7 +26,7 @@ common bldflags
 library
   import: bldflags
   build-depends:
-    base >= 4.7 && < 4.17,
+    base >= 4.7 && < 4.18,
     blt >= 0.12.1,
     containers,
     what4 >= 0.4,

what4-transition-system/what4-transition-system.cabal

@@ -13,7 +13,7 @@ build-type:    Simple
 common dependencies
   build-depends:
     , ansi-wl-pprint       ^>=0.6
-    , base                 >=4.12 && <4.17
+    , base                 >=4.12 && <4.18
     , bytestring
     , containers           ^>=0.6
     , io-streams

what4/CHANGES.md

@@ -1,8 +1,15 @@
 # next (TBA)
 
+* Allow building with GHC 9.4.
+
+* Remove the `MonadFail` instance for `VarRecorder`, as this instance is no
+  longer straightforward to define due to upstream changes in `base-4.17.0.0`.
+  This instance ultimately called `error` anyways, so any uses of `fail` at type
+  `VarRecorder` can be replaced with `error` without any change in behavior.
+
 * Remove a dependency on `data-binary-ieee754`, which has been deprecated.
 
-* Deprecated `allSupported` which represents the SMT logic `ALL_SUPPORTED`, 
+* Deprecated `allSupported` which represents the SMT logic `ALL_SUPPORTED`,
   and added `allLogic` instead which represents the SMTLib standard logic `ALL`.
 
 * Added support for the cvc5 SMT solver.

what4/src/What4/Expr/VarIdentification.hs

@@ -138,7 +138,6 @@ newtype VarRecorder s t a
   deriving ( Functor
            , Applicative
            , Monad
-           , MonadFail
            , MonadST s
            )
 
@@ -194,7 +193,7 @@ addExistVar ExistsOnly p e q v x = do
   VR $ existQuantifiers %= Map.insert e (Some info)
   recordAssertionVars ExistsOnly p x
 addExistVar ExistsForall _ _ _ _ _ = do
-  fail $ "what4 does not allow existental variables to appear inside forall quantifier."
+  error $ "what4 does not allow existental variables to appear inside forall quantifier."
 
 addForallVar :: BM.Polarity -- ^ Polarity of formula
              -> NonceAppExpr t BaseBoolType -- ^ Top term
@@ -229,7 +228,7 @@ addBothVar ExistsOnly e q v x = do
   VR $ forallQuantifiers %= Map.insert e (Some info)
   recordExprVars ExistsForall x
 addBothVar ExistsForall _ _ _ _ = do
-  fail $ "what4 does not allow existental variables to appear inside forall quantifier."
+  error $ "what4 does not allow existental variables to appear inside forall quantifier."
 
 -- | Record variables in a predicate that we are checking satisfiability of.
 recordAssertionVars :: Scope

what4/src/What4/Protocol/VerilogWriter.hs

@@ -1,4 +1,5 @@
 {-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
 {-
 Module           : What4.Protocol.VerilogWriter.AST
 Copyright        : (c) Galois, Inc 2020

what4/src/What4/Solver/CVC5.hs

@@ -15,6 +15,7 @@
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeOperators #-}
 
 module What4.Solver.CVC5
   ( CVC5(..)

what4/src/What4/Solver/Z3.hs

@@ -14,7 +14,7 @@
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE TypeApplications #-}
-
+{-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE GADTs #-}
 module What4.Solver.Z3
   ( Z3(..)

what4/src/What4/Utils/AbstractDomains.hs

@@ -26,6 +26,7 @@ precision.
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE ViewPatterns #-}
 
 module What4.Utils.AbstractDomains

what4/src/What4/Utils/OnlyIntRepr.hs

@@ -8,6 +8,7 @@ Defines a GADT for indicating a base type must be an integer.  Used for
 restricting index types in MATLAB arrays.
 -}
 {-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeOperators #-}
 module What4.Utils.OnlyIntRepr
   ( OnlyIntRepr(..)
   , toBaseTypeRepr

what4/test/InvariantSynthesis.hs

@@ -3,6 +3,7 @@
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeOperators #-}
 
 import           ProbeSolvers
 import           Test.Tasty

what4/test/OnlineSolverTest.hs

@@ -12,6 +12,7 @@
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeOperators #-}
 {-# OPTIONS_GHC -fno-warn-orphans #-} -- for TestShow instance
 
 import           Control.Concurrent ( threadDelay )

what4/what4.cabal

@@ -126,11 +126,11 @@ library
     stm,
     temporary >= 1.2,
     template-haskell,
-    text >= 1.2.4.0 && < 1.3,
+    text >= 1.2.4.0 && < 2.1,
     th-abstraction >=0.1 && <0.5,
     th-lift >= 0.8.2 && < 0.9,
     th-lift-instances >= 0.1 && < 0.2,
-    time >= 1.8 && < 1.12,
+    time >= 1.8 && < 1.13,
     transformers >= 0.4,
     unliftio >= 0.2 && < 0.3,
     unordered-containers >= 0.2.10,