Support building with GHC 8.10 with a sprinkle of language extensions

[RyanGlScott]

GHC 8.10 is somewhat pickier about needing to enable the GADTs language extension than in previous versions of GHC. (See this section of the 8.10 Migration Guide for the full story.) As a result, GADTs needs to be enabled in a handful of modules in order to make saw-script compile with 8.10.

In addition, I enabled NoMonoLocalBinds in Crucible.JVM.BuiltinsJVM. This is because MonoLocalBinds (which GADTs automatically enables) causes some local definitions in that module to fail to typecheck:

[69 of 71] Compiling SAWScript.Crucible.JVM.BuiltinsJVM ( src/SAWScript/Crucible/JVM/BuiltinsJVM.hs, interpreted )

src/SAWScript/Crucible/JVM/BuiltinsJVM.hs:181:47: error:
    • Couldn't match type ‘Term’ with ‘Cryptol.Type’
      Expected type: W4.SymExpr
                       (CrucibleSAW.SAWCoreBackend
                          Nonce.GlobalNonceGenerator
                          Yices.Connection
                          (W4.Flags 'What4.Expr.Builder.FloatReal))
                       bt
                     -> IO Cryptol.Type
        Actual type: W4.Expr Nonce.GlobalNonceGenerator bt -> IO Term
    • In the second argument of ‘Crucible.asSymExpr’, namely
        ‘(CrucibleSAW.toSC sym)’
      In a stmt of a 'do' block:
        t <- Crucible.asSymExpr regval (CrucibleSAW.toSC sym) failure
      In the expression:
        do gp <- getGlobalPair opts pr
           let regval = gp ^. Crucible.gpValue
           let regty = Crucible.regType regval
           let failure = fail $ unwords ...
           ....
    |
181 |               t <- Crucible.asSymExpr regval (CrucibleSAW.toSC sym) failure
    |                                               ^^^^^^^^^^^^^^^^^^^^

src/SAWScript/Crucible/JVM/BuiltinsJVM.hs:189:54: error:
    • Couldn't match expected type ‘Term’
                  with actual type ‘Cryptol.Type’
    • In the second argument of ‘TypedTerm’, namely ‘t’
      In the expression: TypedTerm (Cryptol.tMono cty) t
      In an equation for ‘tt’: tt = TypedTerm (Cryptol.tMono cty) t
    |
189 |               let tt = TypedTerm (Cryptol.tMono cty) t
    |                                                      ^

I opted for the simplest approach (disabling MonoLocalBinds) here to fix the issue.

[RyanGlScott]

As noted in the commit message, I opted to just disable MonoLocalBinds rather than do the slightly more invasive fix of giving local definitions top-level type signatures. Let me know if you'd prefer the latter instead.

[atomb]

What would you think of adding a commit enabling 8.10.3 to the CI config? I'd also be happy to do so, if you'd like.

[RyanGlScott]

What would you think of adding a commit enabling 8.10.3 to the CI config?

Sure, I can give that a go. I can't claim that I'm fully versed in the conventions that the CI configuration is using, but in theory, it should be as simple as adding adding new lines to existing YAML files (and possibly adding more freeze/stack.yaml files).

[atomb]

What would you think of adding a commit enabling 8.10.3 to the CI config?

Sure, I can give that a go. I can't claim that I'm fully versed in the conventions that the CI configuration is using, but in theory, it should be as simple as adding adding new lines to existing YAML files (and possibly adding more freeze/stack.yaml files).

It should be enough to add to this list here. There are a few other things we can do, but that should be enough for a first check.

[RyanGlScott]

Alright, I believe everything should be sorted now CI-wise. Surprisingly, I was able to get away without adding a GHC 8.10–compliant version of stack.yaml, but since there appear to be plans to remove the use of stack in the CI, I didn't bother investigating this any further.

Note that I used GHC 8.10.2 rather than the more recent 8.10.3, since setup-haskell's version of ghcup wasn't able to find 8.10.3 for reasons that I don't fully understand. (See this build failure.) This is probably worth looking into, but perhaps not now.

---

How do things look now? As a side note, I lack push access to this repo, so I would need that if you want me to land this change myself.

[atomb]

This looks great to me! And you should have permission to merge it yourself now.

[RyanGlScott]

The only test suite failures involve Travis (which I don't think is working at all presently) or blst (which appears to be flaky). I'm going to be bold and just land this.