Adapt to NuMatchingAny1 becoming a quantified constraint

This makes the necessary changes to adapt to eddywestbrook/hobbits#8,
which turns `NuMatchingAny1` into an alias for a quantified `NuMatching`
constraint. See #1742 and https://gitlab.haskell.org/ghc/ghc/-/issues/22492 for
the motivation behind this.

One unfortunate hiccup with this patch is that combining quantified superclasses
and `TypeFamilies` doesn't quite work out of the box on pre-9.2 GHCs due to
https://gitlab.haskell.org/ghc/ghc/-/issues/14860. As a result, I have to
introduce explicit equality constraints to work around the issue. I have added
a `Note [QuantifiedConstraints + TypeFamilies trick]` to describe why the
workaround is necessary.

Credit goes to Matthew Pickering for helping me identify this issue and for
authoring a separate fix. I have tweaked his fix and turned it into this patch,
adding him as a co-author in the process.

Fixes #1742.

Co-authored-by: Matthew Pickering <matthewtpickering@gmail.com>

cabal.project

@@ -41,7 +41,8 @@ packages:
     deps/cryptol/cryptol-remote-api
     deps/language-rust
 
+-- TODO: Change the `location` once the patch is merged into upstream `hobbits`
 source-repository-package
     type: git
-    location: https://github.com/eddywestbrook/hobbits.git
-    tag: e49911ce987c4e0fea8c63608d16638b243b051f
+    location: https://github.com/RyanGlScott/hobbits.git
+    tag: bb5d94070ba7627dbb0bec113c6c5d440cf77bb5

heapster-saw/src/Verifier/SAW/Heapster/CruUtil.hs

@@ -1,3 +1,4 @@
+{-# LANGUAGE CPP #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE QuasiQuotes #-}
@@ -14,6 +15,7 @@
 {-# LANGUAGE ViewPatterns #-}
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE PatternGuards #-}
+{-# LANGUAGE QuantifiedConstraints #-}
 
 {-# OPTIONS_GHC -fno-warn-orphans #-}
 
@@ -315,13 +317,6 @@ instance Liftable EndianForm where
   mbLift = unClosed . mbLift . fmap toClosed
 
 $(mkNuMatching [t| forall f. NuMatchingAny1 f => Some f |])
-
-instance NuMatchingAny1 BaseTypeRepr where
-  nuMatchingAny1Proof = nuMatchingProof
-
-instance NuMatchingAny1 TypeRepr where
-  nuMatchingAny1Proof = nuMatchingProof
-
 $(mkNuMatching [t| forall f ctx . NuMatchingAny1 f => AssignView f ctx |])
 
 viewToAssign :: AssignView f ctx -> Assignment f ctx
@@ -336,9 +331,6 @@ instance NuMatchingAny1 f => NuMatching (Assignment f ctx) where
     -- here?
     isoMbTypeRepr viewAssign viewToAssign
 
-instance NuMatchingAny1 f => NuMatchingAny1 (Assignment f) where
-  nuMatchingAny1Proof = nuMatchingProof
-
 instance Closable (Assignment TypeRepr ctx) where
   toClosed = unsafeClose
 
@@ -347,10 +339,6 @@ instance Liftable (Assignment TypeRepr ctx) where
 
 
 $(mkNuMatching [t| forall f tp. NuMatchingAny1 f => BaseTerm f tp |])
-
-instance NuMatchingAny1 f => NuMatchingAny1 (BaseTerm f) where
-  nuMatchingAny1Proof = nuMatchingProof
-
 $(mkNuMatching [t| forall a. NuMatching a => NonEmpty a |])
 $(mkNuMatching [t| forall p v. (NuMatching p, NuMatching v) => Partial p v |])
 $(mkNuMatching [t| X86_80Val |])
@@ -359,10 +347,18 @@ $(mkNuMatching [t| forall w. BV.BV w |])
 $(mkNuMatching [t| Word16String |])
 $(mkNuMatching [t| forall s. StringLiteral s |])
 $(mkNuMatching [t| forall s. StringInfoRepr s |])
+
+#if __GLASGOW_HASKELL__ >= 902
 $(mkNuMatching [t| forall ext f tp.
                 (NuMatchingAny1 f, NuMatchingAny1 (ExprExtension ext f)) =>
                 App ext f tp |])
-
+#else
+-- See Note [QuantifiedConstraints + TypeFamilies trick]
+$(mkNuMatching [t| forall ext f tp exprExt.
+                ( NuMatchingAny1 f
+                , exprExt ~ ExprExtension ext f, NuMatchingAny1 exprExt
+                ) => App ext f tp |])
+#endif
 
 $(mkNuMatching [t| Bytes |])
 $(mkNuMatching [t| forall v. NuMatching v => Field v |])
@@ -385,9 +381,6 @@ $(mkNuMatching [t| forall blocks tp. BlockID blocks tp |])
 instance NuMatching (EmptyExprExtension f tp) where
   nuMatchingProof = unsafeMbTypeRepr
 
-instance NuMatchingAny1 (EmptyExprExtension f) where
-  nuMatchingAny1Proof = nuMatchingProof
-
 $(mkNuMatching [t| AVXOp1 |])
 $(mkNuMatching [t| forall f tp. NuMatchingAny1 f => ExtX86 f tp |])
 
@@ -404,9 +397,6 @@ $(mkNuMatching [t| forall tp. GlobalVar tp |])
 $(mkNuMatching [t| forall f tp. NuMatchingAny1 f =>
                 LLVMExtensionExpr f tp |])
 
-instance NuMatchingAny1 f => NuMatchingAny1 (LLVMExtensionExpr f) where
-  nuMatchingAny1Proof = nuMatchingProof
-
 {-
 $(mkNuMatching [t| forall w f tp. NuMatchingAny1 f => LLVMStmt w f tp |])
 -}
@@ -476,9 +466,6 @@ data Typed f a = Typed { typedType :: TypeRepr a, typedObj :: f a }
 
 $(mkNuMatching [t| forall f a. NuMatching (f a) => Typed f a |])
 
-instance NuMatchingAny1 f => NuMatchingAny1 (Typed f) where
-  nuMatchingAny1Proof = nuMatchingProof
-
 -- | Cast an existential 'Typed' to a particular type or raise an error
 castTypedM :: Fail.MonadFail m => String -> TypeRepr a -> Some (Typed f) -> m (f a)
 castTypedM _ tp (Some (Typed tp' f))
@@ -577,9 +564,6 @@ unKnownReprObj (KnownReprObj :: KnownReprObj f a) = knownRepr :: f a
 
 $(mkNuMatching [t| forall f a. KnownReprObj f a |])
 
-instance NuMatchingAny1 (KnownReprObj f) where
-  nuMatchingAny1Proof = nuMatchingProof
-
 instance Liftable (KnownReprObj f a) where
   mbLift (mbMatch -> [nuMP| KnownReprObj |]) = KnownReprObj
 
@@ -834,3 +818,35 @@ termStmtRegs (Return reg) = [Some reg]
 termStmtRegs (TailCall reg _ regs) =
   Some reg : foldMapFC (\r -> [Some r]) regs
 termStmtRegs (ErrorStmt reg) = [Some reg]
+
+{-
+Note [QuantifiedConstraints + TypeFamilies trick]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+GHC 9.2 and later are reasonably adept and combining TypeFamilies with type
+classes that have quantified superclasses. This is important, as there are
+several places in heapster-saw that require constraints of the form
+`NuMatchingAny1 (ExprExtension ext f)`, where NuMatchingAny1 has a quantified
+superclass and ExprExtension is a type family.
+
+Unfortunately, GHC 9.0 and earlier suffer from a bug where constraints of the
+form `NuMatchingAny1 (ExprExtension ext f)`. See
+https://gitlab.haskell.org/ghc/ghc/-/issues/14860. Thankfully, it is relatively
+straightforward to work around the bug. Instead of writing instances like
+these:
+
+  instance forall ext f.
+           NuMatchingAny1 (ExprExtension ext f) =>
+           NuMatchingAny (Foo ext f tp)
+
+We instead write instances like these, introducing an intermediate `exprExt`
+type variable that is used in conjunction with an equality constraint:
+
+  instance forall ext f exprExt.
+           (exprExt ~ ExprExtension ext f, NuMatchingAny1 exprExt) =>
+           NuMatchingAny (Foo ext f tp)
+
+A bit tedious, but this version actually works on pre-9.2 GHCs, which is nice.
+
+I have guarded each use of this trick with CPP so that we remember to remove
+this workaround when we drop support for pre-9.2 GHCs.
+-}

heapster-saw/src/Verifier/SAW/Heapster/Implication.hs

@@ -461,7 +461,7 @@ data SimplImpl ps_in ps_out where
 
   -- | For any unit-typed variable @x@ and unit-type expression @e@, prove
   -- @x:eq(e)@
-  -- 
+  --
   -- > (x:unit,e:unit) . -o x:eq(e)
   SImpl_UnitEq :: ExprVar UnitType -> PermExpr UnitType ->
                   SimplImpl RNil (RNil :> UnitType)
@@ -1596,15 +1596,6 @@ idLocalPermImpl = LocalPermImpl $ PermImpl_Done $ LocalImplRet Refl
 
 -- type IsLLVMPointerTypeList w ps = RAssign ((:~:) (LLVMPointerType w)) ps
 
-instance NuMatchingAny1 EqPerm where
-  nuMatchingAny1Proof = nuMatchingProof
-
-instance NuMatchingAny1 (LocalImplRet ps) where
-  nuMatchingAny1Proof = nuMatchingProof
-
-instance NuMatchingAny1 (OrListDisj ps a) where
-  nuMatchingAny1Proof = nuMatchingProof
-
 -- Many of these types are mutually recursive. Moreover, Template Haskell
 -- declaration splices strictly separate top-level groups, so if we were to
 -- write each $(mkNuMatching [t| ... |]) splice individually, the splices
@@ -2659,7 +2650,7 @@ orListPerm or_list = foldr1 ValPerm_Or $ orListDisjs or_list
 mbOrListPerm :: Mb ctx (OrList ps a disj) -> Mb ctx (ValuePerm a)
 mbOrListPerm = mbMapCl $(mkClosed [| orListPerm |])
 
--- | Build an 'MbPermSets' 
+-- | Build an 'MbPermSets'
 orListMbPermSets :: PermSet (ps :> a) -> ExprVar a -> OrList ps a disjs ->
                     MbPermSets disjs
 orListMbPermSets _ _ MNil = MbPermSets_Nil

heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs

@@ -53,6 +53,7 @@ import qualified Data.Map.Strict as Map
 import Data.Set (Set)
 import qualified Data.Set as Set
 import Control.Applicative hiding (empty)
+import Control.Monad.Extra (concatMapM)
 import Control.Monad.Identity hiding (ap)
 import Control.Monad.State hiding (ap)
 import Control.Monad.Reader hiding (ap)
@@ -897,45 +898,38 @@ data PermEnv = PermEnv {
 -- * Template Haskell–generated instances
 ----------------------------------------------------------------------
 
-instance NuMatchingAny1 PermExpr where
-  nuMatchingAny1Proof = nuMatchingProof
-
-instance NuMatchingAny1 ValuePerm where
-  nuMatchingAny1Proof = nuMatchingProof
-
-instance NuMatchingAny1 VarAndPerm where
-  nuMatchingAny1Proof = nuMatchingProof
-
-instance NuMatchingAny1 ExprAndPerm where
-  nuMatchingAny1Proof = nuMatchingProof
-
-instance NuMatchingAny1 DistPerms where
-  nuMatchingAny1Proof = nuMatchingProof
-
-$(mkNuMatching [t| forall a . BVFactor a |])
-$(mkNuMatching [t| RWModality |])
-$(mkNuMatching [t| forall b args w. NamedShapeBody b args w |])
-$(mkNuMatching [t| forall b args w. NamedShape b args w |])
-$(mkNuMatching [t| forall w . LLVMFieldShape w |])
-$(mkNuMatching [t| forall a . PermExpr a |])
-$(mkNuMatching [t| forall w. BVRange w |])
-$(mkNuMatching [t| forall a. MbRangeForType a |])
-$(mkNuMatching [t| forall a. NuMatching a => SomeTypedMb a |])
-$(mkNuMatching [t| forall w. BVProp w |])
-$(mkNuMatching [t| forall w sz . LLVMFieldPerm w sz |])
-$(mkNuMatching [t| forall w . LLVMArrayBorrow w |])
-$(mkNuMatching [t| forall w . LLVMArrayPerm w |])
-$(mkNuMatching [t| forall w . LLVMBlockPerm w |])
-$(mkNuMatching [t| forall ns. NameSortRepr ns |])
-$(mkNuMatching [t| forall ns args a. NameReachConstr ns args a |])
-$(mkNuMatching [t| forall ns args a. NamedPermName ns args a |])
-$(mkNuMatching [t| forall a. PermOffset a |])
-$(mkNuMatching [t| forall ghosts args gouts ret. FunPerm ghosts args gouts ret |])
-$(mkNuMatching [t| forall a . AtomicPerm a |])
-$(mkNuMatching [t| forall a . ValuePerm a |])
--- $(mkNuMatching [t| forall as. ValuePerms as |])
-$(mkNuMatching [t| forall a . VarAndPerm a |])
-$(mkNuMatching [t| forall a . ExprAndPerm a |])
+-- Many of these types are mutually recursive. Moreover, Template Haskell
+-- declaration splices strictly separate top-level groups, so if we were to
+-- write each $(mkNuMatching [t| ... |]) splice individually, the splices
+-- involving mutually recursive types would not typecheck. As a result, we
+-- must put everything into a single splice so that it forms a single top-level
+-- group.
+$(concatMapM mkNuMatching
+  [ [t| forall a . BVFactor a |]
+  , [t| RWModality |]
+  , [t| forall b args w. NamedShapeBody b args w |]
+  , [t| forall b args w. NamedShape b args w |]
+  , [t| forall w . LLVMFieldShape w |]
+  , [t| forall a . PermExpr a |]
+  , [t| forall w. BVRange w |]
+  , [t| forall a. MbRangeForType a |]
+  , [t| forall a. NuMatching a => SomeTypedMb a |]
+  , [t| forall w. BVProp w |]
+  , [t| forall w sz . LLVMFieldPerm w sz |]
+  , [t| forall w . LLVMArrayBorrow w |]
+  , [t| forall w . LLVMArrayPerm w |]
+  , [t| forall w . LLVMBlockPerm w |]
+  , [t| forall ns. NameSortRepr ns |]
+  , [t| forall ns args a. NameReachConstr ns args a |]
+  , [t| forall ns args a. NamedPermName ns args a |]
+  , [t| forall a. PermOffset a |]
+  , [t| forall ghosts args gouts ret. FunPerm ghosts args gouts ret |]
+  , [t| forall a . AtomicPerm a |]
+  , [t| forall a . ValuePerm a |]
+  -- , [t| forall as. ValuePerms as |]
+  , [t| forall a . VarAndPerm a |]
+  , [t| forall a . ExprAndPerm a |]
+  ])
 
 $(mkNuMatching [t| forall w . LLVMArrayIndex w |])
 $(mkNuMatching [t| forall args ret. SomeFunPerm args ret |])
@@ -2206,7 +2200,7 @@ mbRangeFTDelete
     bvRangeDelete rng1 rng2
 mbRangeFTDelete mb_rng _ = [mb_rng]
 
--- | Delete all ranges in any of a list of ranges from 
+-- | Delete all ranges in any of a list of ranges from
 mbRangeFTsDelete :: [MbRangeForType a] -> [MbRangeForType a] ->
                     [MbRangeForType a]
 mbRangeFTsDelete rngs_l rngs_r =