Allow building with GHC 9.12

[sauclovian-g]

This isn't working yet

[RyanGlScott]

There's a rather scary-looking error when compiling crucible-mir with GHC 9.12:

 <no location info>: error:
    compiler/GHC/Core/Opt/Simplify/Iteration.hs:3913:15-36: Non-exhaustive patterns in dmd : cont_dmds

This appears to be a GHC bug, and one that is exclusive to GHC 9.12. I've opened https://gitlab.haskell.org/ghc/ghc/-/issues/27261 to track this. Thus far, the only workaround that I've discovered is to ensure that the calls to error in mkTraitObject are only called in let bindings, not in <- bindings:

diff --git a/crucible-mir/src/Mir/Trans.hs b/crucible-mir/src/Mir/Trans.hs
index a0bb1125b..93748cb51 100644
--- a/crucible-mir/src/Mir/Trans.hs
+++ b/crucible-mir/src/Mir/Trans.hs
@@ -1300,8 +1300,8 @@ mkTraitObject :: forall h s ret.
     MirExp s ->
     MirGenerator h s ret (MirExp s)
 mkTraitObject traitName' vtableName e = do
-    handles <- Maybe.fromMaybe (error $ "missing vtable handles for " ++ show vtableName) <$>
-        use (cs . vtableMap . at vtableName)
+    mbHandles <- use (cs . vtableMap . at vtableName)
+    let handles = Maybe.fromMaybe (error $ "missing vtable handles for " ++ show vtableName) mbHandles

     col <- use $ cs . collection
     vtable <- case col ^. vtables . at vtableName of
@@ -1323,9 +1323,10 @@ mkTraitObject traitName' vtableName e = do
     -- trait.  A mismatch would cause runtime errors at calls to trait methods.
     trait <- Maybe.fromMaybe (error $ "unknown trait " ++ show traitName') <$>
         use (cs . collection . M.traits . at traitName')
-    Some vtableTy' <- case traitVtableType col trait of
-                        Left err -> error ("mkTraitObject: " ++ err)
-                        Right x -> return x
+    let someVtableTy' = case traitVtableType col trait of
+                          Left err -> error ("mkTraitObject: " ++ err)
+                          Right x -> x
+    Some vtableTy' <- pure someVtableTy'
     case testEquality vtableTy vtableTy' of
         Just _ -> return ()
         Nothing -> error $ unwords

[langston-barrett]

I generally like to file issues on the upstream repos and link to them in these comments to make it easier to track whether or not we can remove the allow-newers.

[sauclovian-g]

That is a good idea, I will make sure that gets done if we still need them by the time this gets merged.

[RyanGlScott]

crucible-symio is failing to build on GHC 9.14 due to a rather funky-looking error message:

Details

src/Lang/Crucible/SymIO.hs:266:34: error: [GHC-05617]
Error:     • Could not deduce ‘(args <+> args''4) ~ (args <+> args'')’
      from the context: (IsSymInterface sym, 1 <= wptr)
        bound by the type signature for:
                   closeFileHandle :: forall sym (wptr :: Natural) p arch r
                                             (ret :: CrucibleType) a (args :: Ctx CrucibleType).
                                      (IsSymInterface sym, 1 <= wptr) =>
                                      GlobalVar (FileSystemType wptr)
                                      -> FileHandle sym wptr
                                      -> (forall (args' :: Ctx CrucibleType).
                                          Maybe FileHandleError
                                          -> C.OverrideSim p sym arch r args' ret a)
                                      -> C.OverrideSim p sym arch r args ret a
        at src/Lang/Crucible/SymIO.hs:(260,1)-(265,39)
      Expected: RegMap sym EmptyCtx
                -> FileHandle sym wptr
                -> FileM_ p arch r (args <+> args'') ret sym wptr ()
        Actual: RegMap sym EmptyCtx
                -> FileHandle sym wptr
                -> FileM_ p arch r (args <+> args''4) ret sym wptr ()
      Note: ‘<+>’ is a non-injective type family.
      The type variable ‘args''4’ is ambiguous
    • In the first argument of ‘($)’, namely
        ‘runFileMHandleCont
           fvar fhdl emptyRegMap (\ a -> cont (eitherToMaybeL a))’
      In the expression:
        runFileMHandleCont
          fvar fhdl emptyRegMap (\ a -> cont (eitherToMaybeL a))
          $ \ _ fhdl'
              -> do sz <- getPtrSz
                    sym <- getSym
                    ....
      In an equation for ‘closeFileHandle’:
          closeFileHandle fvar fhdl cont
            = runFileMHandleCont
                fvar fhdl emptyRegMap (\ a -> cont (eitherToMaybeL a))
                $ \ _ fhdl'
                    -> do sz <- getPtrSz
                          ....
    • Relevant bindings include
        closeFileHandle :: GlobalVar (FileSystemType wptr)
                           -> FileHandle sym wptr
                           -> (forall (args' :: Ctx CrucibleType).
                               Maybe FileHandleError -> C.OverrideSim p sym arch r args' ret a)
                           -> C.OverrideSim p sym arch r args ret a
          (bound at src/Lang/Crucible/SymIO.hs:266:1)
    |
266 | closeFileHandle fvar fhdl cont = runFileMHandleCont fvar fhdl emptyRegMap (\a -> cont (eitherToMaybeL a)) $ \_ fhdl' -> do
    |                                  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

As far as I can tell, this is a regression in GHC's typechecker, which I have reported upstream at https://gitlab.haskell.org/ghc/ghc/-/issues/27262. A workaround is to enable {-# LANGUAGE NoDeepSubsumption #-} at the top of the file.