From 3d83e0d8af0fa29ddecd27c9fb4c90128b8ac179 Mon Sep 17 00:00:00 2001
From: Ryan Scott <ryan.gl.scott@gmail.com>
Date: Sun, 2 Apr 2023 07:08:00 -0400
Subject: [PATCH] Support building with GHC 9.4

This contains a variety of tweaks needed to build SAW with GHC 9.4:

* GHC 9.4 is more conservative about inferring superclass constraints that arise
  from functional dependencies (see [this
  section](https://gitlab.haskell.org/ghc/ghc/-/wikis/migration/9.4?version_id=b60e52482a666d25638d59cd7e86851ddf971dc1#constraints-derived-from-superclasses)
  of the GHC 9.4 Migration Guide), so we must add explicit `m ~ Identity`
  constraints to certain parts of `heapster-saw` to make it compile with GHC
  9.4.
* I raised the upper version bounds on `aeson` and `vector` to allow building
  them with GHC 9.4.
* The following submodule changes were brought in to support building with
  GHC 9.4:
  * `argo`: #193
  * `crucible`: GaloisInc/crucible#1073

    (This also requires bumping the `llvm-pretty`, `llvm-pretty-bc-parser`,
    and `what4` submodules as a side effect)
  * `language-sally`: GaloisInc/language-sally#13
  * `macaw`: GaloisInc/macaw#330
  * `parameterized-utils`: GaloisInc/parameterized-utils#146

Fixes #1852.
---
 deps/crucible                                       |  2 +-
 deps/language-sally                                 |  2 +-
 deps/llvm-pretty                                    |  2 +-
 deps/llvm-pretty-bc-parser                          |  2 +-
 deps/macaw                                          |  2 +-
 deps/parameterized-utils                            |  2 +-
 deps/what4                                          |  2 +-
 heapster-saw/heapster-saw.cabal                     |  2 +-
 .../src/Verifier/SAW/Heapster/Implication.hs        | 13 +++++--------
 .../src/Verifier/SAW/Heapster/TypedCrucible.hs      |  8 ++++----
 saw-remote-api/saw-remote-api.cabal                 |  6 +++---
 saw-script.cabal                                    |  2 +-
 12 files changed, 21 insertions(+), 24 deletions(-)

diff --git a/deps/crucible b/deps/crucible
index f4145fbed9..ad4a553487 160000
--- a/deps/crucible
+++ b/deps/crucible
@@ -1 +1 @@
-Subproject commit f4145fbed96245f385a91ef3a32e6737df1075ff
+Subproject commit ad4a553487eeb5c6bbb5abf4bde26af905bf0254
diff --git a/deps/language-sally b/deps/language-sally
index 24d53a963c..b218ac7d4f 160000
--- a/deps/language-sally
+++ b/deps/language-sally
@@ -1 +1 @@
-Subproject commit 24d53a963c2a2d11a118cfaa98956a69f5c8c6d5
+Subproject commit b218ac7d4f39b4d30cf7f2db584efa5ea926a024
diff --git a/deps/llvm-pretty b/deps/llvm-pretty
index 64d43d9375..b13493fda7 160000
--- a/deps/llvm-pretty
+++ b/deps/llvm-pretty
@@ -1 +1 @@
-Subproject commit 64d43d9375a819dc2a2df99fb98df24f049dcfaa
+Subproject commit b13493fda7276835a4e19bf13a9fb1b3e08083a9
diff --git a/deps/llvm-pretty-bc-parser b/deps/llvm-pretty-bc-parser
index cbcf0954c2..d541adf5c1 160000
--- a/deps/llvm-pretty-bc-parser
+++ b/deps/llvm-pretty-bc-parser
@@ -1 +1 @@
-Subproject commit cbcf0954c23da0018df3cc6aae77290ae2efe53b
+Subproject commit d541adf5c12e86058cbc1f211456b4ad4a7011a1
diff --git a/deps/macaw b/deps/macaw
index 0686e5d86b..30fe405a39 160000
--- a/deps/macaw
+++ b/deps/macaw
@@ -1 +1 @@
-Subproject commit 0686e5d86bfd802e04dd94cf8836127127232f8f
+Subproject commit 30fe405a3987fac3a886b66f4de9b9a7e1b25fac
diff --git a/deps/parameterized-utils b/deps/parameterized-utils
index a888f5862b..a58128337e 160000
--- a/deps/parameterized-utils
+++ b/deps/parameterized-utils
@@ -1 +1 @@
-Subproject commit a888f5862b73a1575d36fef9327fcbe3dbcbff51
+Subproject commit a58128337e2a795dd06dd3968b6a7e98dc1b27bf
diff --git a/deps/what4 b/deps/what4
index 6c462cd46e..ffbad75b1c 160000
--- a/deps/what4
+++ b/deps/what4
@@ -1 +1 @@
-Subproject commit 6c462cd46e0ea9ebbfbd6b6ea237984eeb3dc72a
+Subproject commit ffbad75b1ce65577422a19a30a39a5059be8b95f
diff --git a/heapster-saw/heapster-saw.cabal b/heapster-saw/heapster-saw.cabal
index 46a91108dc..1fb04c58b6 100644
--- a/heapster-saw/heapster-saw.cabal
+++ b/heapster-saw/heapster-saw.cabal
@@ -38,7 +38,7 @@ library
     filepath,
     language-rust,
     hobbits ^>= 1.4,
-    aeson >= 1.5 && < 2.1,
+    aeson >= 1.5 && < 2.2,
     th-abstraction,
     template-haskell,
     extra
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs
index 4aded72cb8..7315c6aae1 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs
@@ -2972,7 +2972,7 @@ instance (NuMatching a, Substable PermVarSubst a Identity) =>
     [nuMP| EqProofCons eqp' eq_step |] ->
       EqProofCons <$> genSubst s eqp' <*> genSubst s eq_step
 
-instance SubstVar PermVarSubst m =>
+instance m ~ Identity =>
          Substable PermVarSubst (SimplImpl ps_in ps_out) m where
   genSubst s mb_impl = case mbMatch mb_impl of
     [nuMP| SImpl_Drop x p |] ->
@@ -3251,7 +3251,7 @@ instance SubstVar PermVarSubst m =>
     [nuMP| SImpl_ElimAnyToPtr x fp |] ->
       SImpl_ElimAnyToPtr <$> genSubst s x <*> genSubst s fp
 
-instance SubstVar PermVarSubst m =>
+instance m ~ Identity =>
          Substable PermVarSubst (PermImpl1 ps_in ps_out) m where
   genSubst s mb_impl = case mbMatch mb_impl of
     [nuMP| Impl1_Fail err |] -> Impl1_Fail <$> genSubst s err
@@ -3291,8 +3291,7 @@ instance SubstVar PermVarSubst m =>
       Impl1_TryProveBVProp <$> genSubst s x <*> genSubst s prop <*>
                                return (mbLift prop_str)
 
--- FIXME: shouldn't need the SubstVar PermVarSubst m assumption...
-instance (NuMatchingAny1 r, SubstVar PermVarSubst m,
+instance (NuMatchingAny1 r, m ~ Identity,
           Substable1 PermVarSubst r m) =>
          Substable PermVarSubst (PermImpl r ps) m where
   genSubst s mb_impl = case mbMatch mb_impl of
@@ -3300,8 +3299,7 @@ instance (NuMatchingAny1 r, SubstVar PermVarSubst m,
     [nuMP| PermImpl_Step impl1 mb_impls |] ->
       PermImpl_Step <$> genSubst s impl1 <*> genSubst s mb_impls
 
--- FIXME: shouldn't need the SubstVar PermVarSubst m assumption...
-instance (NuMatchingAny1 r, SubstVar PermVarSubst m,
+instance (NuMatchingAny1 r, m ~ Identity,
           Substable1 PermVarSubst r m) =>
          Substable PermVarSubst (MbPermImpls r bs_pss) m where
   genSubst s mb_impls = case mbMatch mb_impls of
@@ -3317,8 +3315,7 @@ instance SubstVar s m => Substable s (OrListDisj ps a disj) m where
 instance SubstVar s m => Substable1 s (OrListDisj ps a) m where
   genSubst1 = genSubst
 
--- FIXME: shouldn't need the SubstVar PermVarSubst m assumption...
-instance SubstVar PermVarSubst m =>
+instance m ~ Identity =>
          Substable PermVarSubst (LocalPermImpl ps_in ps_out) m where
   genSubst s (mbMatch -> [nuMP| LocalPermImpl impl |]) =
     LocalPermImpl <$> genSubst s impl
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs b/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs
index 1bccc9b380..38c95b1e24 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs
@@ -809,7 +809,7 @@ instance SubstVar PermVarSubst m =>
     [nuMP| TypedRegsCons rs r |] ->
       TypedRegsCons <$> genSubst s rs <*> genSubst s r
 
-instance (NuMatchingAny1 r, SubstVar PermVarSubst m,
+instance (NuMatchingAny1 r, m ~ Identity,
           Substable1 PermVarSubst r m) =>
          Substable PermVarSubst (AnnotPermImpl r ps) m where
   genSubst s (mbMatch -> [nuMP| AnnotPermImpl err impl |]) =
@@ -1003,7 +1003,7 @@ instance SubstVar PermVarSubst m =>
          Substable1 PermVarSubst (TypedJumpTarget blocks tops) m where
   genSubst1 = genSubst
 
-instance SubstVar PermVarSubst m =>
+instance m ~ Identity =>
          Substable PermVarSubst (TypedTermStmt blocks tops rets ps_in) m where
   genSubst s mb_x = case mbMatch mb_x of
     [nuMP| TypedJump impl_tgt |] -> TypedJump <$> genSubst s impl_tgt
@@ -1015,7 +1015,7 @@ instance SubstVar PermVarSubst m =>
     [nuMP| TypedErrorStmt str r |] ->
       TypedErrorStmt (mbLift str) <$> genSubst s r
 
-instance (PermCheckExtC ext exprExt, SubstVar PermVarSubst m) =>
+instance (PermCheckExtC ext exprExt, m ~ Identity) =>
          Substable PermVarSubst (TypedStmtSeq ext blocks tops rets ps_in) m where
   genSubst s mb_x = case mbMatch mb_x of
     [nuMP| TypedImplStmt impl_seq |] ->
@@ -1027,7 +1027,7 @@ instance (PermCheckExtC ext exprExt, SubstVar PermVarSubst m) =>
       TypedTermStmt (mbLift loc) <$> genSubst s term_stmt
 
 
-instance (PermCheckExtC ext exprExt, SubstVar PermVarSubst m) =>
+instance (PermCheckExtC ext exprExt, m ~ Identity) =>
          Substable1 PermVarSubst (TypedStmtSeq ext blocks tops rets) m where
   genSubst1 = genSubst
 
diff --git a/saw-remote-api/saw-remote-api.cabal b/saw-remote-api/saw-remote-api.cabal
index bf987df9e6..5623d8ae9f 100644
--- a/saw-remote-api/saw-remote-api.cabal
+++ b/saw-remote-api/saw-remote-api.cabal
@@ -34,8 +34,8 @@ common errors
     -Werror=overlapping-patterns
 
 common deps
-  build-depends: base >=4.11.1.0 && <4.17,
-                 aeson >= 1.4.2 && < 2.1,
+  build-depends: base >=4.11.1.0 && <4.18,
+                 aeson >= 1.4.2 && < 2.2,
                  aig,
                  argo,
                  base64-bytestring,
@@ -60,7 +60,7 @@ common deps
                  silently,
                  text,
                  unordered-containers,
-                 vector >= 0.12 && < 0.13,
+                 vector >= 0.12 && < 0.14,
                  cryptol-remote-api
   default-language: Haskell2010
 
diff --git a/saw-script.cabal b/saw-script.cabal
index ed3b3257fc..5d02d4d94c 100644
--- a/saw-script.cabal
+++ b/saw-script.cabal
@@ -23,7 +23,7 @@ library
   default-language: Haskell2010
   build-depends:
       base >= 4.9
-    , aeson >= 2.0 && < 2.1
+    , aeson >= 2.0 && < 2.2
     , aig
     , array
     , binary