From 684ad9d11b92008ab6f7874bc7ba19f430ec4b90 Mon Sep 17 00:00:00 2001
From: Simon Marlow <marlowsd@gmail.com>
Date: Wed, 25 Mar 2026 10:35:58 +0000
Subject: [PATCH 1/9] Angle compiler cleanups

- rename `TcQueryGen` to `TcWhere`

- change `TcAll` and `TcNegation` to contain `TcPat` instead of `TcQuery` /
  `[TcStatement]` respectively (this is more uniform and
  consistent, and simplifies some things)

- refactoring in the type checker to unify how we handle
  locality. `oneBranch` is renamed `encloseLocal` and used consistently
  when typechecking `|`, `all`, `!`, and `if`, which all need
  locality. Probably fixes some bugs.

- update a few out-of-date comments
---
 glean/db/Glean/Query/BindOrder.hs       |  22 +--
 glean/db/Glean/Query/Codegen/Types.hs   |  31 ----
 glean/db/Glean/Query/Expand.hs          |  12 +-
 glean/db/Glean/Query/Flatten.hs         |  19 +-
 glean/db/Glean/Query/Prune.hs           |  14 +-
 glean/db/Glean/Query/Typecheck.hs       | 220 +++++++++++-------------
 glean/db/Glean/Query/Typecheck/Types.hs |  13 +-
 glean/db/Glean/Query/Typecheck/Unify.hs |   6 +-
 glean/test/tests/Angle/ErrorTest.hs     |   2 +-
 9 files changed, 138 insertions(+), 201 deletions(-)

diff --git a/glean/db/Glean/Query/BindOrder.hs b/glean/db/Glean/Query/BindOrder.hs
index 8b2240a359..1784ec925e 100644
--- a/glean/db/Glean/Query/BindOrder.hs
+++ b/glean/db/Glean/Query/BindOrder.hs
@@ -33,22 +33,12 @@ import Glean.Query.Vars (VarSet)
 import Glean.RTS.Term as RTS
 
 -- -----------------------------------------------------------------------------
--- Fixing up MatchBind vs. MatchVar
-
--- Substitution can mess up MatchBind and MatchVar - we might end up
--- with multiple MatchBinds for a variable, or a MatchVar before a
--- MatchBind. To fix it up all we need to do is traverse the query in
--- the correct order, keeping track of which variables are in scope,
--- and change MatchBind<->MatchVar as appropriate.
---
--- This is all somewhat suboptimal, because the typechecker has
--- already figured out MatchBind vs. MatchVar and here we mess it up
--- by substitution and then fix it again. Which begs the question: why
--- do we have MatchBind and MatchVar at all, couldn't we leave it
--- until the last minute just before code generation to figure out
--- which variables are binding occurrences?  Yes, but it's nice to be
--- able to give the user out-of-scope error messages from the
--- typechecker.  Maybe we'll change this in the future.
+-- Resolving MatchBind vs. MatchVar
+
+-- Before the Reorder pass, MatchBind and MatchVar are the same (strictly
+-- speaking we should have just one variable form). The reorder pass resolves
+-- statement ordering so that variables are bound before their use;
+-- MatchBind indicates a variable binding and MatchVar indicates a variable use.
 
 data Scope = Scope
   { isScope :: VarSet
diff --git a/glean/db/Glean/Query/Codegen/Types.hs b/glean/db/Glean/Query/Codegen/Types.hs
index fa85bccd48..d2ab7a5847 100644
--- a/glean/db/Glean/Query/Codegen/Types.hs
+++ b/glean/db/Glean/Query/Codegen/Types.hs
@@ -81,7 +81,6 @@ data CgStatement_ var
   | CgAllStatement var (Expr_ var) [CgStatement_ var]
   | CgNegation [CgStatement_ var]
   | CgDisjunction [[CgStatement_ var]]
-  -- ^ For rationale, see Note [why do we have sequential composition?]
   | CgConditional
     { cond :: [CgStatement_ var]
     , then_ :: [CgStatement_ var]
@@ -89,38 +88,8 @@ data CgStatement_ var
     }
   deriving (Show, Functor, Foldable, Traversable)
 
-
 type CgStatement = CgStatement_ Var
 
-{- Note [why do we have sequential composition?]
-
-The issue is that queries for sum types can't necessarily be handled
-by nested generators. Consider
-
-  v = cxx1.FunctionName (name(cxx1.Name "xyz" ) | operator(cxx1.Name "+"))
-
-If we flattened this into nested generators we would get
-
-  x = cxx1.Name "xyz"
-  y = cxx1.Name "+"
-  z = cxx1.FunctionName (name x | operator y)
-
-Now suppose there is no name xyz. This query will match nothing,
-because the generator for cxx1.Name "xyz" would be empty.  (even if
-the generator matched, flattening out the generators like this will
-test too many combinations and do too much work).
-
-With sequential composition of queries we can do it like this:
-
- n = (name x where x = cxx1.Name "xyz") |
-     (operator x where x = cxx1.Name "+")
- v = cxx1.FunctionName n
-
-(Note that this query won't work if you write it because we can't
-typecheck the sub-query "name x where ...", but we can generate the
-AST for it in the JSON query compiler.)
--}
-
 type Generator = Generator_ Var
 
 -- | A generator produces a finite series of terms
diff --git a/glean/db/Glean/Query/Expand.hs b/glean/db/Glean/Query/Expand.hs
index 3d192fbf64..36ff5af176 100644
--- a/glean/db/Glean/Query/Expand.hs
+++ b/glean/db/Glean/Query/Expand.hs
@@ -102,12 +102,12 @@ instantiateWithFreshVariables query numVars = do
     TcElementsOfSet (instantiatePat base pat)
   instantiateTcTerm base (TcElementsUnresolved ty pat) =
     TcElementsUnresolved ty (instantiatePat base pat)
-  instantiateTcTerm base (TcQueryGen query) =
-    TcQueryGen (instantiateQuery base query)
-  instantiateTcTerm base (TcAll query) =
-    TcAll (instantiateQuery base query)
-  instantiateTcTerm base (TcNegation stmts) =
-    TcNegation (map (instantiateStmt base) stmts)
+  instantiateTcTerm base (TcWhere query) =
+    TcWhere (instantiateQuery base query)
+  instantiateTcTerm base (TcAll pat) =
+    TcAll (instantiatePat base pat)
+  instantiateTcTerm base (TcNegation p) =
+    TcNegation (instantiatePat base p)
   instantiateTcTerm base (TcPrimCall op args) =
     TcPrimCall op (map (instantiatePat base) args)
   instantiateTcTerm base (TcIf (Typed ty cond) then_ else_) =
diff --git a/glean/db/Glean/Query/Flatten.hs b/glean/db/Glean/Query/Flatten.hs
index 4b7e0a557e..90764fc390 100644
--- a/glean/db/Glean/Query/Flatten.hs
+++ b/glean/db/Glean/Query/Flatten.hs
@@ -210,20 +210,25 @@ flattenSeqGenerators (Ref (MatchExt (Typed ty match))) = case match of
   TcElementsOfSet pat -> do
     r <- flattenPattern pat
     return [(mempty, stmts, SetElementGenerator ty pat') | (stmts,pat') <- r ]
-  TcQueryGen query -> do
+  TcWhere query -> do
     (group, term, _) <- flattenQuery' query
     return [(floatGroup group, mempty, TermGenerator term)]
-  TcAll query -> do
-    (group, term, _) <- flattenQuery' query
+  TcAll p -> do
+    let elemTy = case derefType ty of
+          Schema.SetTy t -> t
+          _other -> error "TcAll: not SetTy"
+    (group, term, _) <- flattenQuery' $
+      TcQuery elemTy p Nothing [] Angle.Unordered
     var <- fresh ty
     return
       [ (Statements [FlatAllStatement var term group]
       , mempty
       , TermGenerator (Ref (MatchVar var)))]
-  TcNegation stmts -> do
-    (ords, floats) <- mapAndUnzipM flattenStatement stmts
-    let neg = FlatNegation (mkGroup ords floats)
-    return [(oneStmt neg, mempty, TermGenerator $ Tuple [])]
+  TcNegation p -> do
+    (group, _term, _) <- flattenQuery' (TcQuery ty p Nothing [] Angle.Ordered)
+    -- Note: term is discarded. e.g. in !(X where ...) we don't do anything
+    -- with the X.
+    return [(oneStmt (FlatNegation group), mempty, TermGenerator $ Tuple [])]
   TcPrimCall op args -> do
     r <- manyTerms (\args -> PrimCall op args ty) <$> mapM flattenPattern args
     return [ (mempty, float, gen) | (float, gen) <- r ]
diff --git a/glean/db/Glean/Query/Prune.hs b/glean/db/Glean/Query/Prune.hs
index b65b024427..1142b9c17e 100644
--- a/glean/db/Glean/Query/Prune.hs
+++ b/glean/db/Glean/Query/Prune.hs
@@ -155,12 +155,12 @@ prune hasFacts (QueryWithInfo q _ gen t) = do
           Ref . MatchExt . Typed ty . TcElementsOfSet <$> prunePat x
         TcElementsUnresolved ty' x ->
           Ref . MatchExt . Typed ty . TcElementsUnresolved ty' <$> prunePat x
-        TcQueryGen q ->
-          Ref . MatchExt . Typed ty . TcQueryGen <$> pruneTcQuery q
+        TcWhere q ->
+          Ref . MatchExt . Typed ty . TcWhere <$> pruneTcQuery q
         -- we dont' want to handle negation here because if it tries to match
         -- against things that are not in the database it should succeed.
-        TcAll query ->
-          Ref . MatchExt . Typed ty . TcAll <$> pruneTcQuery query
+        TcAll p ->
+          Ref . MatchExt . Typed ty . TcAll <$> prunePat p
         TcNegation{} -> Just pat
         TcPrimCall op xs -> Ref . MatchExt . Typed ty . TcPrimCall op
           <$> traverse prunePat xs
@@ -240,9 +240,9 @@ renumberVars gen ty q =
     TcElementsOfArray x -> TcElementsOfArray <$> renamePat x
     TcElementsOfSet x -> TcElementsOfSet <$> renamePat x
     TcElementsUnresolved ty x -> TcElementsUnresolved ty <$> renamePat x
-    TcQueryGen q -> TcQueryGen <$> renameQuery q
-    TcAll query -> TcAll <$> renameQuery query
-    TcNegation xs -> TcNegation <$> traverse renameStmt xs
+    TcWhere q -> TcWhere <$> renameQuery q
+    TcAll p -> TcAll <$> renamePat p
+    TcNegation p -> TcNegation <$> renamePat p
     TcPrimCall op xs -> TcPrimCall op <$> traverse renamePat xs
     TcIf cond then_ else_ ->
       TcIf <$> traverse renamePat cond <*> renamePat then_ <*> renamePat else_
diff --git a/glean/db/Glean/Query/Typecheck.hs b/glean/db/Glean/Query/Typecheck.hs
index 67c5507046..b931644b71 100644
--- a/glean/db/Glean/Query/Typecheck.hs
+++ b/glean/db/Glean/Query/Typecheck.hs
@@ -87,32 +87,32 @@ typecheck dbSchema opts rtsType query = do
       { tcEnvPredicates = predicatesById dbSchema
       , tcEnvTypes = typesById dbSchema
       }
-  (q@(TcQuery ty _ _ _ _), TypecheckState{..}) <-
+  ((q@(TcQuery ty _ _ _ _), _, _), TypecheckState{..}) <-
     let state = initialTypecheckState tcEnv opts rtsType TcModeQuery in
-    withExceptT (Text.pack . show) $ flip runStateT state $ do
-      modify $ \s -> s { tcVisible = varsQuery query mempty }
-      q@(TcQuery retTy _ _ _ _) <- inferQuery ContextPat query
-        <* freeVariablesAreErrors <* unboundVariablesAreErrors
-      resolvePromote
-      subst <- gets tcSubst
-      whenDebug $ liftIO $ hPutStrLn stderr $ show $
-        vcat [
-          "subst:", indent 2 (vcat
-            [ pretty n <> " := " <> displayDefault ty
-            | (n,ty) <- IntMap.toList subst
-            ]),
-          "query: " <> displayDefault q
-        ]
-      zonkVars
-      zonkTcQuery q
-        `catchError` \_ -> do
-           (head,_,_) <- needsResult query
-           opts <- gets tcDisplayOpts
-           retTy' <- apply retTy
-           prettyErrorAt (sourcePatSpan head) $ vcat
-             [ "query has ambiguous type",
-               indent 4 $ "type: " <> display opts retTy'
-             ]
+    withExceptT (Text.pack . show) $ flip runStateT state $
+      encloseLocal (varsQuery query mempty) $ do
+        q@(TcQuery retTy _ _ _ _) <- inferQuery ContextPat query
+        freeVariablesAreErrors
+        resolvePromote
+        subst <- gets tcSubst
+        whenDebug $ liftIO $ hPutStrLn stderr $ show $
+          vcat [
+            "subst:", indent 2 (vcat
+              [ pretty n <> " := " <> displayDefault ty
+              | (n,ty) <- IntMap.toList subst
+              ]),
+            "query: " <> displayDefault q
+          ]
+        zonkVars
+        zonkTcQuery q
+          `catchError` \_ -> do
+             (head,_,_) <- needsResult query
+             opts <- gets tcDisplayOpts
+             retTy' <- apply retTy
+             prettyErrorAt (sourcePatSpan head) $ vcat
+               [ "query has ambiguous type",
+                 indent 4 $ "type: " <> display opts retTy'
+               ]
   return (QueryWithInfo q tcNextVar Nothing ty, tcPreds)
 
 -- | Typecheck the query for a derived predicate
@@ -136,39 +136,38 @@ typecheckDeriving tcEnv opts rtsType PredicateDetails{..} derivingInfo = do
       case derivingInfo of
         NoDeriving -> return NoDeriving
         Derive deriveWhen q -> do
-          modify $ \s -> s { tcVisible = varsQuery q mempty }
-          -- we typecheck the pattern first, because we know its type.
-          (head, stmts, ord) <- needsResult q
-          let
-            (key, maybeVal) = case head of
-              KeyValue _ key val -> (key, Just val)
-                -- Backwards compat, we had a predicate in schema v4 of the form
-                --   X -> prim.toLower X
-                -- but this doesn't parse if -> binds tighter than application.
-              App _ (KeyValue _ key val) xs ->
-                let end
-                      | null xs   = val
-                      | otherwise = last xs
-                    span = spanBetween (sourcePatSpan val) (sourcePatSpan end)
-                in
-                (key, Just (App span val xs))
-              _other -> (head, Nothing)
-          key' <- typecheckPattern ContextPat predicateKeyType key
-          maybeVal' <- case maybeVal of
-            Nothing
-              | eqType (tcOptAngleVersion opts) unit predicateValueType ->
-                return Nothing
-              | otherwise -> prettyErrorIn head $ nest 4 $ vcat
-                [ "a functional predicate must return a value,"
-                , "i.e. the query should have the form 'X -> Y where .." ]
-            Just val -> Just <$>
-              typecheckPattern ContextPat predicateValueType val
-          stmts' <- mapM typecheckStatement stmts
-          freeVariablesAreErrors
-          unboundVariablesAreErrors
-          resolvePromote
-          zonkVars
-          q <- zonkTcQuery (TcQuery predicateKeyType key' maybeVal' stmts' ord)
+          (q, _, _) <- encloseLocal (varsQuery q mempty) $ do
+            -- we typecheck the pattern first, because we know its type.
+            (head, stmts, ord) <- needsResult q
+            let
+              (key, maybeVal) = case head of
+                KeyValue _ key val -> (key, Just val)
+                  -- Backwards compat, we had a predicate in schema v4 of the form
+                  --   X -> prim.toLower X
+                  -- but this doesn't parse if -> binds tighter than application.
+                App _ (KeyValue _ key val) xs ->
+                  let end
+                        | null xs   = val
+                        | otherwise = last xs
+                      span = spanBetween (sourcePatSpan val) (sourcePatSpan end)
+                  in
+                  (key, Just (App span val xs))
+                _other -> (head, Nothing)
+            key' <- typecheckPattern ContextPat predicateKeyType key
+            maybeVal' <- case maybeVal of
+              Nothing
+                | eqType (tcOptAngleVersion opts) unit predicateValueType ->
+                  return Nothing
+                | otherwise -> prettyErrorIn head $ nest 4 $ vcat
+                  [ "a functional predicate must return a value,"
+                  , "i.e. the query should have the form 'X -> Y where .." ]
+              Just val -> Just <$>
+                typecheckPattern ContextPat predicateValueType val
+            stmts' <- mapM typecheckStatement stmts
+            freeVariablesAreErrors
+            resolvePromote
+            zonkVars
+            zonkTcQuery (TcQuery predicateKeyType key' maybeVal' stmts' ord)
           nextVar <- gets tcNextVar
           return $ Derive deriveWhen $
             QueryWithInfo q nextVar Nothing predicateKeyType
@@ -322,7 +321,7 @@ inferExpr ctx pat = case pat of
     return (Ref (MatchExt (Typed ty (TcOr a' b'))), ty)
   NestedQuery _ q -> do
     q@(TcQuery ty _ _ _ _) <- inferQuery ctx q
-    return (Ref (MatchExt (Typed ty (TcQueryGen q))), ty)
+    return (Ref (MatchExt (Typed ty (TcWhere q))), ty)
   Negation _ _ ->
     (,unit) <$> typecheckPattern ctx unit pat
   IfPattern _ srcCond srcThen srcElse -> do
@@ -361,11 +360,10 @@ inferExpr ctx pat = case pat of
             , "does not have a set type"
             ]
   All _ e -> do
-    (e',elementTy) <- inferExpr ctx e
-    let
-      q = TcQuery elementTy e' Nothing [] Unordered
-      ty = SetTy elementTy
-    return (Ref (MatchExt (Typed ty (TcAll q))), ty)
+    ((e',elementTy), _, _) <-
+      encloseLocal (varsPat e mempty) $ inferExpr ctx e
+    let ty = SetTy elementTy
+    return (Ref (MatchExt (Typed ty (TcAll e'))), ty)
 
   TypeSignature s e ty -> do
     rtsType <- gets tcRtsType
@@ -621,37 +619,13 @@ typecheckPattern ctx typ pat = case (typ, pat) of
     return (Ref (MatchExt (Typed ty (TcIf cond then_ else_))))
 
   (ty, NestedQuery _ query) ->
-    Ref . MatchExt . Typed ty . TcQueryGen <$> typecheckQuery ctx ty query
-
-  (ty, Negation s pat) | ty == unit -> do
-    let startPos = mkSpan (startLoc s) (startLoc s)
-        empty = Tuple startPos []
-        (stmts, ord) = case pat of
-          NestedQuery _ (SourceQuery Nothing stmts _) -> (stmts, ord)
-          other -> ([SourceStatement (Wildcard s) other], Unordered)
-
-        -- A negated pattern must always have type {}.
-        query = SourceQuery (Just empty) stmts ord
-
-        -- Variables bound within a negated query are
-        -- not considered bound outside of it.
-        enclose tc = do
-          before <- get
-          modify $ \s -> s {
-            tcVisible = varsPat pat (tcVisible before)
-          }
-          res <- tc
-          modify $ \after -> after
-            { tcBindings = tcBindings before
-            , tcUses = tcUses after `HashSet.intersection` tcVisible before
-            , tcScope = tcScope after
-                `HashMap.intersection` HashSet.toMap (tcVisible before)
-            , tcVisible = tcVisible before
-            }
-          return res
-
-    TcQuery _ _ _ stmts _ <- enclose $ typecheckQuery ctx unit query
-    return $ Ref (MatchExt (Typed unit (TcNegation stmts)))
+    Ref . MatchExt . Typed ty . TcWhere <$> typecheckQuery ctx ty query
+
+  (ty, Negation _ pat) | ty == unit -> do
+    (pat, _, _) <-
+      encloseLocal (varsPat pat mempty) $
+        typecheckPattern ctx unit (ignoreResult pat)
+    return $ Ref (MatchExt (Typed unit (TcNegation pat)))
 
   (PredicateTy _ _, FactId _ Nothing fid) -> do
     isFactIdAllowed pat
@@ -665,9 +639,9 @@ typecheckPattern ctx typ pat = case (typ, pat) of
     return (f e')
 
   (ty@(SetTy elemTy), All _ query) -> do
-    arg <- typecheckPattern ctx elemTy query
-    let q = TcQuery elemTy arg Nothing [] Unordered
-    return (Ref (MatchExt (Typed ty (TcAll q))))
+    (arg, _, _) <- encloseLocal (varsPat query mempty) $
+      typecheckPattern ctx elemTy query
+    return (Ref (MatchExt (Typed ty (TcAll arg))))
 
   -- A match on a predicate type with a pattern that is not a wildcard,
   -- variable, field selector or dereference matches the key.
@@ -818,13 +792,8 @@ freeVariablesAreErrors = do
       , "This is usually a mistake, so it is disallowed in Angle."
       ]
 
-unboundVariablesAreErrors :: T ()
-unboundVariablesAreErrors = do
-  TypecheckState{..} <- get
-  unboundVariablesAreErrors_ tcUses tcBindings
-
-unboundVariablesAreErrors_ :: VarSet -> VarSet -> T ()
-unboundVariablesAreErrors_ uses binds = do
+unboundVariablesAreErrors :: VarSet -> VarSet -> T ()
+unboundVariablesAreErrors uses binds = do
   case HashSet.toList (uses `HashSet.difference` binds) of
     [] -> return ()
     badGuys -> prettyError $ nest 4 $ vcat
@@ -856,17 +825,19 @@ checkVarCase span name
 -- 2. The set of variables that are considered to be *used* by this
 --    pattern are those that are used in either branch.
 --
-disjunction :: VarSet -> T a -> VarSet -> (a -> T b) -> T (a,b)
+
+disjunction :: VarSet -> T a -> VarSet -> (a -> T b) -> T (a, b)
 disjunction varsA ta varsB tb = do
   state0 <- get
-  (a, usesA, bindsA) <- oneBranch varsA ta
-  (b, usesB, bindsB) <- oneBranch varsB (tb a)
+  (a, usesA, bindsA) <- encloseLocal varsA ta
+  (b, usesB, bindsB) <- encloseLocal varsB (tb a)
+  let binds = bindsA `HashSet.intersection` bindsB
+  let uses = usesA `HashSet.union` usesB
   modify  $ \s -> s {
-    tcBindings = tcBindings state0 `HashSet.union` -- Note (1) above
-      (bindsA `HashSet.intersection` bindsB),
-    tcUses = tcUses state0 `HashSet.union` -- Note (2) above
-      (usesA `HashSet.union` usesB) }
-  return (a,b)
+    tcBindings = tcBindings state0 `HashSet.union` binds, -- Note (1) above
+    tcUses = tcUses state0 `HashSet.union` uses -- Note (2) above
+  }
+  return (a, b)
 
 -- | Typechecking either A or B in A|B
 --
@@ -879,9 +850,9 @@ disjunction varsA ta varsB tb = do
 -- 3. To determine what is local to any nested A|B subterms, we update
 --    tcVisible by finding the visible variables of the current pattern.
 --
-oneBranch :: VarSet -> T a -> T (a, VarSet, VarSet)
-oneBranch branchVars ta = do
-  visibleBefore  <- gets tcVisible
+encloseLocal :: VarSet -> T a -> T (a, VarSet, VarSet)
+encloseLocal branchVars ta = do
+  before@TypecheckState { tcVisible = visibleBefore } <- get
   modify $ \s -> s {
     tcUses = HashSet.empty,
     tcBindings = HashSet.empty,
@@ -892,13 +863,16 @@ oneBranch branchVars ta = do
   let
     localUses = HashSet.difference (tcUses after) visibleBefore
     localBinds = HashSet.difference (tcBindings after) visibleBefore
-  unboundVariablesAreErrors_ localUses localBinds
+  unboundVariablesAreErrors localUses localBinds
   modify $ \s -> s
     { tcScope = HashMap.intersection
         (tcScope after)
         (HashSet.toMap visibleBefore)
        -- See Note (1) above
-    , tcVisible = visibleBefore }
+    , tcUses = tcUses before
+    , tcBindings = tcUses before
+    , tcVisible = tcVisible before
+    }
   let
     extUses = HashSet.intersection (tcUses after) visibleBefore
     extBinds = HashSet.intersection (tcBindings after) visibleBefore
@@ -1038,9 +1012,9 @@ tcQueryDeps q = Set.fromList $ map getRef (overQuery q)
       TcElementsOfArray x -> overPat x
       TcElementsOfSet x -> overPat x
       TcElementsUnresolved _ x -> overPat x
-      TcQueryGen q -> overQuery q
-      TcAll q -> overQuery q
-      TcNegation stmts -> foldMap overStatement stmts
+      TcWhere q -> overQuery q
+      TcAll q -> overPat q
+      TcNegation p -> overPat p
       TcPrimCall _ xs -> foldMap overPat xs
       TcIf (Typed _ x) y z -> foldMap overPat [x, y, z]
       TcDeref _ p -> overPat p
@@ -1095,8 +1069,8 @@ tcTermUsesNegation = \case
   TcElementsOfArray x -> tcPatUsesNegation x
   TcElementsOfSet x -> tcPatUsesNegation x
   TcElementsUnresolved _ p -> tcPatUsesNegation p
-  TcQueryGen q -> tcQueryUsesNegation q
-  TcAll query -> tcQueryUsesNegation query
+  TcWhere q -> tcQueryUsesNegation q
+  TcAll p -> tcPatUsesNegation p
   TcNegation _ -> Just PatternNegation
   TcPrimCall _ xs -> firstJust tcPatUsesNegation xs
   -- one can replicate negation using if statements
diff --git a/glean/db/Glean/Query/Typecheck/Types.hs b/glean/db/Glean/Query/Typecheck/Types.hs
index ae56e4cc87..a73727f253 100644
--- a/glean/db/Glean/Query/Typecheck/Types.hs
+++ b/glean/db/Glean/Query/Typecheck/Types.hs
@@ -59,9 +59,9 @@ data TcTerm
   | TcElementsOfArray TcPat
   | TcElementsOfSet TcPat
   | TcElementsUnresolved Type TcPat
-  | TcQueryGen TcQuery
-  | TcAll TcQuery
-  | TcNegation [TcStatement]
+  | TcWhere TcQuery
+  | TcAll TcPat
+  | TcNegation TcPat
   | TcPrimCall PrimOp [TcPat]
   | TcIf { cond :: Typed TcPat, then_ :: TcPat, else_ :: TcPat }
   | TcDeref Type TcPat
@@ -105,11 +105,10 @@ instance Display TcTerm where
   display opts (TcElementsOfArray arr) = displayAtom opts arr <> "[..]"
   display opts (TcElementsOfSet set) = "elements" <+> parens (display opts set)
   display opts (TcElementsUnresolved _ pat) = displayAtom opts pat <> "[..]"
-  display opts (TcQueryGen q) = parens (display opts q)
+  display opts (TcWhere q) = parens (display opts q)
   display opts (TcAll query)
     = "all" <+> "(" <> display opts query <> ")"
-  display opts (TcNegation q) =
-    "!" <> parens (sep (punctuate ";" (map (display opts) q)))
+  display opts (TcNegation q) = "!" <> parens (display opts q)
   display opts (TcPrimCall op args) =
     hsep (display opts op : map (displayAtom opts) args)
   display opts (TcPromote _ pat) =
@@ -126,7 +125,7 @@ instance Display TcTerm where
     TcOr{} -> parens (display opts pat)
     TcFactGen{} -> parens (display opts pat)
     TcPrimCall{} -> parens (display opts pat)
-    TcQueryGen{} -> parens (display opts pat)
+    TcWhere{} -> parens (display opts pat)
     TcNegation{} -> display opts pat
     TcIf{} -> parens (display opts pat)
     _ -> display opts pat
diff --git a/glean/db/Glean/Query/Typecheck/Unify.hs b/glean/db/Glean/Query/Typecheck/Unify.hs
index adef88e63a..b274422ced 100644
--- a/glean/db/Glean/Query/Typecheck/Unify.hs
+++ b/glean/db/Glean/Query/Typecheck/Unify.hs
@@ -409,9 +409,9 @@ zonkTcTerm t = case t of
   TcFactGen pid k v sec ->
     TcFactGen pid <$> zonkTcPat k <*> zonkTcPat v <*> pure sec
   TcElementsOfArray a -> TcElementsOfArray <$> zonkTcPat a
-  TcQueryGen q -> TcQueryGen <$> zonkTcQuery q
-  TcAll q -> TcAll <$> zonkTcQuery q
-  TcNegation stmts -> TcNegation <$> mapM zonkTcStatement stmts
+  TcWhere q -> TcWhere <$> zonkTcQuery q
+  TcAll p -> TcAll <$> zonkTcPat p
+  TcNegation p -> TcNegation <$> zonkTcPat p
   TcPrimCall op args -> TcPrimCall op <$> mapM zonkTcPat args
   TcIf (Typed ty cond) th el ->
     TcIf
diff --git a/glean/test/tests/Angle/ErrorTest.hs b/glean/test/tests/Angle/ErrorTest.hs
index 22d1d05da7..c46d1a2a92 100644
--- a/glean/test/tests/Angle/ErrorTest.hs
+++ b/glean/test/tests/Angle/ErrorTest.hs
@@ -205,5 +205,5 @@ angleErrorTests = dbTestCase $ \env repo -> do
   assertBool "angle - negation unbound" $
     case r of
       Left (BadQuery x) ->
-        "unbound variable: A" `Text.isInfixOf` x
+        "not bound anywhere: A" `Text.isInfixOf` x
       _ -> False

From 86b6cdeb1fb41a11dca999b10cf391d6a18244da Mon Sep 17 00:00:00 2001
From: Simon Marlow <marlowsd@gmail.com>
Date: Wed, 25 Mar 2026 12:19:58 +0000
Subject: [PATCH 2/9] Add internal query linter

When working on the compiler it's easy to accidentally break something
that results in a segfault. Most of these errors can be detected by
checks on the Codegen IR, in particular correct type-safety and
variable-scoping.

- Add Glean.Query.Lint to implement query consistency checks
- Turn on query linting with `GLEAN_DEBUG=lint` or `--debug-query-lint`
- Linting is automatically enabled for all tests via `withTestEnv`
---
 glean.cabal.in                        |   1 +
 glean/db/Glean/Database/Config.hs     |   5 +-
 glean/db/Glean/Database/Env.hs        |   1 +
 glean/db/Glean/Query/Lint.hs          | 290 ++++++++++++++++++++++++++
 glean/db/Glean/Query/UserQuery.hs     |   7 +
 glean/hs/Glean/RTS/Types.hs           |   1 +
 glean/test/lib/Glean/Database/Test.hs |   9 +-
 glean/website/docs/running.md         |   3 +
 8 files changed, 314 insertions(+), 3 deletions(-)
 create mode 100644 glean/db/Glean/Query/Lint.hs

diff --git a/glean.cabal.in b/glean.cabal.in
index 9e5315b9f8..11f678d3e9 100644
--- a/glean.cabal.in
+++ b/glean.cabal.in
@@ -673,6 +673,7 @@ library db
         Glean.Query.Expand
         Glean.Query.Flatten
         Glean.Query.Flatten.Types
+        Glean.Query.Lint
         Glean.Query.Opt
         Glean.Query.Prune
         Glean.Query.Reorder
diff --git a/glean/db/Glean/Database/Config.hs b/glean/db/Glean/Database/Config.hs
index 54f469bb51..440e9e6dc0 100644
--- a/glean/db/Glean/Database/Config.hs
+++ b/glean/db/Glean/Database/Config.hs
@@ -213,15 +213,17 @@ data Config = Config
 data DebugFlags = DebugFlags
   { tcDebug :: !Bool
   , queryDebug :: !Bool
+  , queryLint :: !Bool
   }
 
 instance Default DebugFlags where
-  def = DebugFlags { tcDebug = False, queryDebug = False }
+  def = DebugFlags { tcDebug = False, queryDebug = False, queryLint = False }
 
 instance Semigroup DebugFlags where
   a <> b = DebugFlags
     { tcDebug = tcDebug a || tcDebug b
     , queryDebug = queryDebug a || queryDebug b
+    , queryLint = queryLint a || queryLint b
     }
 
 instance Monoid DebugFlags where
@@ -576,6 +578,7 @@ options = do
     debugParser = do
       tcDebug <- switch (long "debug-tc")
       queryDebug <- switch (long "debug-query")
+      queryLint <- switch (long "debug-query-lint")
       return DebugFlags{..}
 
     serverConfigThriftSource = option (eitherReader ThriftSource.parse)
diff --git a/glean/db/Glean/Database/Env.hs b/glean/db/Glean/Database/Env.hs
index b71f805ca4..744fc027e7 100644
--- a/glean/db/Glean/Database/Env.hs
+++ b/glean/db/Glean/Database/Env.hs
@@ -166,6 +166,7 @@ getDebugEnv = do
   where
   add "tc" = return def { tcDebug = True }
   add "query" = return def { queryDebug = True }
+  add "lint" = return def { queryLint = True }
   add other = do
     logWarning $ "Unkonwn GLEAN_DEBUG class: " <> other
     return def
diff --git a/glean/db/Glean/Query/Lint.hs b/glean/db/Glean/Query/Lint.hs
new file mode 100644
index 0000000000..9c9f3a1194
--- /dev/null
+++ b/glean/db/Glean/Query/Lint.hs
@@ -0,0 +1,290 @@
+{-
+  Copyright (c) Meta Platforms, Inc. and affiliates.
+  All rights reserved.
+
+  This source code is licensed under the BSD-style license found in the
+  LICENSE file in the root directory of this source tree.
+-}
+
+module Glean.Query.Lint (
+    lintQuery
+  ) where
+
+import Control.Monad
+import Control.Monad.Except
+import Control.Monad.State
+import Data.List (foldl')
+import Data.IntSet (IntSet)
+import qualified Data.IntSet as IntSet
+import Compat.Prettyprinter
+
+import Glean.Angle.Types
+  (Type_(..), latestAngleVersion, tempPredicateId)
+import Glean.Database.Schema.Types
+  (DbSchema, PredicateDetails(..), lookupPid, lookupPredicateId)
+import Glean.Display
+import Glean.Query.Codegen.Types
+import Glean.RTS.Term as RTS
+import Glean.RTS.Types as RTS
+import Glean.Schema.Util (tupleSchema)
+
+-- | The lint monad: tracks the set of bound variable IDs in state,
+-- and can throw a pretty-printed error.
+type L a = StateT IntSet (Except (Doc ())) a
+
+runL :: L a -> Either (Doc ()) a
+runL m = runExcept (evalStateT m IntSet.empty)
+
+lintError :: Doc () -> L a
+lintError = throwError
+
+-- | Record a variable as bound.
+bindVar :: Var -> L ()
+bindVar v = modify (IntSet.insert (varId v))
+
+-- | Check that a variable is currently bound.
+requireBound :: Var -> L ()
+requireBound v = do
+  bound <- get
+  unless (varId v `IntSet.member` bound) $
+    lintError $ "unbound variable:" <+> displayDefault v
+
+-- | Run an action in a nested scope. The bound set is saved and
+-- restored afterwards, so bindings made inside do not escape.
+scoped :: L a -> L a
+scoped m = do
+  saved <- get
+  a <- m
+  put saved
+  return a
+
+{-
+  Check the query for internal consistency. lintQuery will check
+  the following properties of the query:
+
+  - type-correctness, e.g.
+    - in A = B, the types of A and B are equivalent
+    - in FactGenerator and DerivedFactGenerator, the types of the key
+      and value pattern match those of the predicate in the schema
+    - arguments of primitives have the correct type
+  - bind-before-use: for all variables, MatchBind occurs before MatchVar
+
+-}
+lintQuery :: DbSchema -> CodegenQuery -> Either (Doc ()) ()
+lintQuery schema QueryWithInfo{..} = runL $ do
+  let CgQuery head body = qiQuery
+  lintStatements schema body
+  lintPat head
+  case qiGenerator of
+    Nothing -> checkEqType "query head" head qiReturnType
+    Just gen -> do
+      lintGenerator gen
+      lintGeneratorTypes schema head gen
+
+-- ---------------------------------------------------------------------------
+-- Bind-before-use and type checking for statement lists
+
+lintStatements :: DbSchema -> [CgStatement] -> L ()
+lintStatements schema = mapM_ (lintStatement schema)
+
+lintStatement :: DbSchema -> CgStatement -> L ()
+lintStatement schema = \case
+  CgStatement pat gen -> do
+    -- The generator is evaluated first; its patterns can bind variables
+    lintGenerator gen
+    -- Then the LHS pattern matches the generator result, and can use
+    -- variables bound by the generator as well as previously bound ones
+    lintPat pat
+    -- Type check: pattern type should match generator result type
+    lintStmtTypes schema pat gen
+
+  CgAllStatement var expr stmts -> do
+    -- The inner statements are evaluated in a nested scope
+    scoped $ do
+      lintStatements schema stmts
+      lintPat expr
+    -- The variable bound by 'all' is available to subsequent statements
+    bindVar var
+
+  CgNegation stmts ->
+    -- Negation introduces its own scope; bindings do not escape
+    scoped $ lintStatements schema stmts
+
+  CgDisjunction stmtss -> do
+    -- Each branch starts with the same bound set. Variables bound
+    -- in all branches are available afterwards.
+    bounds <- forM stmtss $ \stmts -> scoped $ do
+      lintStatements schema stmts
+      get
+    case bounds of
+      [] -> return ()
+      (b:bs) -> put (foldl' IntSet.intersection b bs)
+
+  CgConditional{..} -> do
+    outer <- get
+    lintStatements schema cond
+    -- then branch sees cond bindings
+    lintStatements schema then_
+    thenBound <- get
+    -- else branch only sees pre-condition bindings
+    put outer
+    lintStatements schema else_
+    elseBound <- get
+    -- Variables bound in both branches are available after
+    put (IntSet.intersection thenBound elseBound)
+
+-- ---------------------------------------------------------------------------
+-- Check uses and record bindings in a single depth-first left-to-right
+-- traversal, so that a MatchBind makes the variable immediately
+-- available for a later MatchVar in the same pattern.
+
+lintPat :: Pat -> L ()
+lintPat = mapM_ lintMatch
+
+lintMatch :: Match () Var -> L ()
+lintMatch = \case
+  MatchBind v -> bindVar v
+  MatchVar v -> requireBound v
+  MatchAnd a b -> do
+    lintPat a
+    lintPat b
+  MatchPrefix _ rest ->
+    lintPat rest
+  MatchArrayPrefix _ pre whole -> do
+    mapM_ lintPat pre
+    lintPat whole
+  _ -> return ()
+
+-- | Lint expression-position subterms of a generator, then bind
+-- pattern-position variables.
+lintGenerator :: Generator -> L ()
+lintGenerator = \case
+  FactGenerator _ kpat vpat _ -> do
+    lintPat kpat
+    lintPat vpat
+  TermGenerator expr ->
+    lintPat expr
+  DerivedFactGenerator _ key value -> do
+    lintPat key
+    lintPat value
+  ArrayElementGenerator _ arr ->
+    lintPat arr
+  SetElementGenerator _ set ->
+    lintPat set
+  PrimCall _ args _ ->
+    mapM_ lintPat args
+
+-- | Type-check the result generator (qiGenerator). The head expression
+-- is the fact ID that the generator will look up.
+lintGeneratorTypes :: DbSchema -> Pat -> Generator -> L ()
+lintGeneratorTypes schema head gen = case gen of
+  FactGenerator pidRef kpat vpat _ -> do
+    mdetails <- lookupPredicate schema pidRef
+    forM_ mdetails $ \details -> do
+      checkEqType
+        ("result generator key of" <+> displayDefault pidRef)
+        kpat (predicateKeyType details)
+      checkEqType
+        ("result generator value of" <+> displayDefault pidRef)
+        vpat (predicateValueType details)
+    checkEqType "result generator fact ID" head (PredicateTy () pidRef)
+  _ -> return ()
+
+-- ---------------------------------------------------------------------------
+-- Type checking
+
+-- | Check the type consistency of a statement: pattern type vs
+-- generator result type, and predicate key/value types for fact
+-- generators.
+lintStmtTypes :: DbSchema -> Pat -> Generator -> L ()
+lintStmtTypes schema pat gen = case gen of
+  FactGenerator pidRef kpat vpat _ -> do
+    mdetails <- lookupPredicate schema pidRef
+    forM_ mdetails $ \details -> do
+      checkEqType
+        ("key of" <+> displayDefault pidRef) kpat (predicateKeyType details)
+      checkEqType
+        ("value of" <+> displayDefault pidRef) vpat (predicateValueType details)
+    -- The LHS pattern matches the fact ID, which has the predicate type
+    checkEqType "fact generator result" pat (PredicateTy () pidRef)
+
+  DerivedFactGenerator pidRef key value -> do
+    mdetails <- lookupPredicate schema pidRef
+    forM_ mdetails $ \details -> do
+      checkEqType
+        ("key of" <+> displayDefault pidRef) key (predicateKeyType details)
+      checkEqType
+        ("value of" <+> displayDefault pidRef) value (predicateValueType details)
+    checkEqType "derived fact generator result" pat (PredicateTy () pidRef)
+
+  TermGenerator expr ->
+    case (patType pat, patType expr) of
+      (Just pty, Just ety) -> typesShouldMatch "term generator" pty ety
+      _ -> return ()
+
+  ArrayElementGenerator eltTy _arr ->
+    checkEqType "array element generator" pat eltTy
+
+  SetElementGenerator eltTy _set ->
+    checkEqType "set element generator" pat eltTy
+
+  PrimCall _op _args retTy ->
+    checkEqType "primcall result" pat retTy
+
+lookupPredicate :: DbSchema -> PidRef -> L (Maybe PredicateDetails)
+lookupPredicate schema (PidRef pid predId)
+  -- The temporary predicate used for derived fact generators is not
+  -- stored in the schema, so skip it.
+  | predId == tempPredicateId = return Nothing
+  | otherwise =
+    case lookupPid pid schema of
+      Nothing -> case lookupPredicateId predId schema of
+        Nothing ->
+          lintError $ "unknown predicate:" <+> displayDefault predId
+        Just details -> return (Just details)
+      Just details -> return (Just details)
+
+-- | Check that the type of a pattern matches an expected type.
+-- When the pattern's type cannot be determined, the check is skipped.
+checkEqType :: Doc () -> Pat -> Type -> L ()
+checkEqType ctx pat expected =
+  case patType pat of
+    Nothing -> return ()
+    Just actual -> typesShouldMatch ctx actual expected
+
+typesShouldMatch :: Doc () -> Type -> Type -> L ()
+typesShouldMatch ctx actual expected
+  | eqType latestAngleVersion actual expected = return ()
+  | otherwise = throwError $ vcat
+      [ "type mismatch in" <+> ctx <> ":"
+      , "  expected:" <+> displayDefault expected
+      , "  actual:" <+> displayDefault actual
+      ]
+
+-- ---------------------------------------------------------------------------
+-- Inferring the type of a pattern
+
+-- | Attempt to determine the type of a pattern. Returns Nothing when
+-- the type cannot be determined from the pattern structure alone
+-- (e.g. an empty array or an Alt without surrounding context).
+patType :: Pat -> Maybe Type
+patType (Byte _) = Just ByteTy
+patType (Nat _) = Just NatTy
+patType (RTS.String _) = Just StringTy
+patType (ByteArray _) = Just (ArrayTy ByteTy)
+patType (Array []) = Nothing
+patType (Array (t:_)) = ArrayTy <$> patType t
+patType (Tuple ts) = tupleSchema <$> traverse patType ts
+patType (Alt _ _) = Nothing
+patType (Ref m) = matchType m
+
+matchType :: Match () Var -> Maybe Type
+matchType (MatchWild ty) = Just ty
+matchType (MatchNever ty) = Just ty
+matchType (MatchBind v) = Just (varType v)
+matchType (MatchVar v) = Just (varType v)
+matchType (MatchFid _) = Nothing
+matchType (MatchAnd a _) = patType a
+matchType (MatchPrefix _ _) = Just StringTy
+matchType (MatchArrayPrefix ty _ _) = Just (ArrayTy ty)
+matchType (MatchExt _) = Nothing
diff --git a/glean/db/Glean/Query/UserQuery.hs b/glean/db/Glean/Query/UserQuery.hs
index 4419e352dc..6b4756abda 100644
--- a/glean/db/Glean/Query/UserQuery.hs
+++ b/glean/db/Glean/Query/UserQuery.hs
@@ -74,6 +74,7 @@ import Glean.Query.Flatten
 import Glean.Query.Opt
 import Glean.Query.Reorder
 import Glean.Query.Incremental (makeIncremental)
+import Glean.Query.Lint (lintQuery)
 import Glean.RTS as RTS
 import Glean.RTS.Bytecode.Disassemble
 import qualified Glean.RTS.Bytecode.Gen.Version as Bytecode
@@ -991,6 +992,12 @@ compileAngleQuery rec ver dbSchema mode source stored debug = do
   reordered <- checkBadQuery id $ runExcept $ reorder dbSchema optimised
   ifDebug $ "reordered query: " <> show (displayDefault (qiQuery reordered))
 
+  when (queryLint debug) $
+    case lintQuery dbSchema reordered of
+      Left err -> throwIO $ Thrift.BadQuery $
+        Text.pack $ show $ "query lint:" <+> err
+      Right () -> return ()
+
   final <- case mode of
     NoExtraSteps -> return reordered
     IncrementalDerivation getStats -> do
diff --git a/glean/hs/Glean/RTS/Types.hs b/glean/hs/Glean/RTS/Types.hs
index 2d865845a7..e08a59b2a1 100644
--- a/glean/hs/Glean/RTS/Types.hs
+++ b/glean/hs/Glean/RTS/Types.hs
@@ -143,6 +143,7 @@ eqType version a b = case (a,b) of
   (NatTy, NatTy) -> True
   (StringTy, StringTy) -> True
   (ArrayTy a, ArrayTy b) -> eqType version a b
+  (SetTy a, SetTy b) -> eqType version a b
   (RecordTy as, RecordTy bs) ->
     let isTuple = all (Text.isInfixOf "tuplefield"  . fieldDefName)
         -- previous to version 7 records were always compared structurally
diff --git a/glean/test/lib/Glean/Database/Test.hs b/glean/test/lib/Glean/Database/Test.hs
index f5840978e4..28a2d8fdb7 100644
--- a/glean/test/lib/Glean/Database/Test.hs
+++ b/glean/test/lib/Glean/Database/Test.hs
@@ -24,6 +24,7 @@ module Glean.Database.Test
   , setUseCheckpoint
   , enableTcDebug
   , enableQueryDebug
+  , enableQueryLint
   , enableRocksDBCache
   , setAclTesting
   , withTestEnv
@@ -143,6 +144,10 @@ enableQueryDebug :: Setting
 enableQueryDebug cfg = cfg
   { cfgDebug = (cfgDebug cfg) { queryDebug = True } }
 
+enableQueryLint :: Setting
+enableQueryLint cfg = cfg
+  { cfgDebug = (cfgDebug cfg) { queryLint = True } }
+
 enableRocksDBCache :: Setting
 enableRocksDBCache cfg = cfg
   { cfgServerConfig = (cfgServerConfig cfg) <&> \scfg -> scfg
@@ -160,12 +165,12 @@ withTestEnv settings action =
       \(cfgAPI :: NullConfigProvider) -> do
     let
       dbConfig = foldl' (\acc f -> f acc)
-        def
+        (enableQueryLint def
           { cfgDataStore = tmpDataStore
           , cfgSchemaLocation = Just schemaLocationFiles
           , cfgServerConfig = ThriftSource.value def
               { ServerConfig.config_db_rocksdb_cache_mb = 0 }
-          }
+          })
         settings
 
     withDatabases evb dbConfig cfgAPI action
diff --git a/glean/website/docs/running.md b/glean/website/docs/running.md
index 31844c8fe4..d84645cdb3 100644
--- a/glean/website/docs/running.md
+++ b/glean/website/docs/running.md
@@ -181,3 +181,6 @@ Enable debugging output for the Angle typechecker.
 
 * `--debug-query`<br />
 Enable debugging output for the Angle query compiler.
+
+* `--debug-query-lint`<br />
+Enable consistency checks on the query before running; catches internal errors in the query compiler.

From 87b4c17d3a20a1df2ffaaf9246290972bf949665 Mon Sep 17 00:00:00 2001
From: Marcelo Lazaroni <lazaronijunior@gmail.com>
Date: Sun, 27 Sep 2026 17:50:10 +0100
Subject: [PATCH 3/9] Register the angle-test-recursion test suite

Summary:
`glean/test/tests/Angle/RecursionTest.hs` exercises the experimental
support for recursive derived predicates (enabled with
`--experimental-recursion`), but it was never listed in `glean.cabal.in`,
so it wasn't built or run by the open-source build.

Add a `test-suite` stanza for it, following `angle-test-derived`. It also
needs `Schema.Lib` and the libraries that module depends on, like the
`schematest` suites.

Both existing test cases pass.
---
 glean.cabal.in | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/glean.cabal.in b/glean.cabal.in
index 11f678d3e9..8132e20a3c 100644
--- a/glean.cabal.in
+++ b/glean.cabal.in
@@ -2049,6 +2049,19 @@ test-suite angle-test-derived
     main-is: Angle/DerivedTest.hs
     ghc-options: -main-is Angle.DerivedTest
 
+test-suite angle-test-recursion
+    import: test, angle-test
+    type: exitcode-stdio-1.0
+    main-is: Angle/RecursionTest.hs
+    other-modules: Schema.Lib
+    ghc-options: -main-is Angle.RecursionTest
+    build-depends:
+        glean:config,
+        glean:if-internal-hs,
+        glean:lib-derive,
+        glean:util,
+        glean:client-hs,
+
 test-suite angle-test-set
     import: test, angle-test
     type: exitcode-stdio-1.0

From ee3a7f5d68acfc459319b392156bce7e8f38656b Mon Sep 17 00:00:00 2001
From: Marcelo Lazaroni <lazaronijunior@gmail.com>
Date: Sun, 27 Sep 2026 17:52:04 +0100
Subject: [PATCH 4/9] Prune mutually recursive derivations together

Summary:
On read-only databases `pruneDerivations` removes branches of derivation
queries that search predicates with no facts. It visited derivations in
topological order, treating a predicate as having facts if it has stored
facts, if its derivation was already visited and kept, or if it is the
predicate being pruned (so direct self-recursion worked).

With mutual recursion there is no topological order. For

    predicate Q : nat
      A where P A
    derive P
      A where Base A | Q A

whichever of P and Q was visited first saw the other as empty. Here Q was
visited first and its only branch was removed, so `Q _` returned nothing,
and P silently lost its recursive `Q A` branch. The result depended on the
visiting order.

Now we prune one strongly connected component of the dependency graph at
a time, in dependency order. For a recursive component we find which
members may have facts by iterating to a least fixed point: start by
assuming none of them has facts and add the members whose derivation
survives pruning until nothing changes. Pruning only ever keeps more when
more predicates are assumed to have facts (negation is never pruned), so
this terminates. Acyclic components are pruned exactly as before.

This also covers the `child == predId` special case for self-recursion,
with one difference: a derivation whose only branches depend on itself
(`X where P X`) is now pruned, since it can never produce facts.

This mostly matters for the experimental recursion support, but
pre-existing cycles are affected too: pairs of `default` derivations used
for schema migration (`derive P.1 default ... P.2`, `derive P.2 default
... P.1`) form a cycle when pruning runs, and are now pruned
deterministically.

Test: a new case in `angle-test-recursion`, where the cycle is closed by a
`derive` declaration in a later schema, fails without this change.
`angle-test-derived`, `angle-test-angle` and `schematest` pass.
---
 glean/db/Glean/Query/Prune.hs           | 76 ++++++++++++++++---------
 glean/test/tests/Angle/RecursionTest.hs | 30 ++++++++++
 2 files changed, 80 insertions(+), 26 deletions(-)

diff --git a/glean/db/Glean/Query/Prune.hs b/glean/db/Glean/Query/Prune.hs
index 1142b9c17e..05df2a2b3e 100644
--- a/glean/db/Glean/Query/Prune.hs
+++ b/glean/db/Glean/Query/Prune.hs
@@ -12,8 +12,8 @@ import Control.Monad
 import Control.Monad.State (State, runState)
 import qualified Control.Monad.State as State
 import Data.Bitraversable (bitraverse)
-import Data.Foldable (asum)
-import Data.Maybe (fromMaybe)
+import Data.Foldable (asum, foldl')
+import Data.Maybe (fromMaybe, isJust)
 import qualified Data.Set as Set
 import qualified Data.Graph as Graph
 import Data.HashMap.Strict (HashMap)
@@ -62,37 +62,61 @@ pruneQueries
   -> HashMap PredicateId TypecheckedQuery
   -> HashMap PredicateId TypecheckedQuery
 pruneQueries hasStoredFacts derivations =
-  foldr add mempty $ topologicalSort derivations
+  -- Components come in reverse topological order, so by the time we
+  -- process a component all components it depends on have been pruned.
+  foldl' addComponent mempty (Graph.stronglyConnComp edges)
   where
-    add :: (PredicateId, TypecheckedQuery)
-        -> HashMap PredicateId TypecheckedQuery
-        -> HashMap PredicateId TypecheckedQuery
-    add (predId, query) derivedWithFacts =
-       case prune (hasFacts predId derivedWithFacts) query of
-          Nothing -> derivedWithFacts
-          Just pruned -> HashMap.insert predId pruned derivedWithFacts
-
-    hasFacts predId derivedWithFacts child =
-      child == predId
-        || hasStoredFacts child
-        || child `HashMap.member` derivedWithFacts
-
-topologicalSort
-  :: HashMap PredicateId TypecheckedQuery
-  -> [(PredicateId, TypecheckedQuery)]
-topologicalSort derivations =
-  [ entry
-  | vertex <- Graph.topSort graph
-  , let (entry,_,_) = fromVertex vertex
-  ]
-  where
-    (graph, fromVertex, _) = Graph.graphFromEdges edges
     edges =
       [ (entry, predId, dependencies)
       | entry@(predId, query) <- HashMap.toList derivations
       , let dependencies = Set.toList $ tcQueryDeps $ qiQuery query
       ]
 
+    addComponent
+      :: HashMap PredicateId TypecheckedQuery
+      -> Graph.SCC (PredicateId, TypecheckedQuery)
+      -> HashMap PredicateId TypecheckedQuery
+    addComponent derivedWithFacts component =
+      foldl' add derivedWithFacts entries
+      where
+        entries = Graph.flattenSCC component
+
+        -- Members of this component that may have facts.
+        inComponent = case component of
+          Graph.AcyclicSCC _ -> Set.empty
+          Graph.CyclicSCC _ -> leastFixpoint Set.empty
+
+        add acc (predId, query) =
+          case prune (hasFacts inComponent) query of
+            Nothing -> acc
+            Just pruned -> HashMap.insert predId pruned acc
+
+        hasFacts withFacts child =
+          hasStoredFacts child
+            || child `HashMap.member` derivedWithFacts
+            || child `Set.member` withFacts
+
+        -- Members of a recursive component depend on each other, so we
+        -- can't prune them one at a time. Instead we start by assuming
+        -- that none of them has facts, and keep adding the ones whose
+        -- derivation survives pruning until nothing changes. Assuming that
+        -- more predicates have facts never causes more to be pruned, so
+        -- this terminates and finds the smallest such set. If we started
+        -- by assuming that all of them have facts, we would keep
+        -- derivations that can never produce anything, like
+        --
+        --   predicate P : nat
+        --     X where P X
+        leastFixpoint withFacts
+          | next == withFacts = withFacts
+          | otherwise = leastFixpoint next
+          where
+            next = Set.fromList
+              [ predId
+              | (predId, query) <- entries
+              , isJust $ prune (hasFacts withFacts) query
+              ]
+
 -- | Remove paths that we know will not yield any result.
 -- This will save us a lot of compilation at query time.
 --
diff --git a/glean/test/tests/Angle/RecursionTest.hs b/glean/test/tests/Angle/RecursionTest.hs
index c346bc47ae..0e8a65ff9c 100644
--- a/glean/test/tests/Angle/RecursionTest.hs
+++ b/glean/test/tests/Angle/RecursionTest.hs
@@ -92,6 +92,36 @@ recursionTest = TestList
           , RTS.Tuple [ RTS.Nat 1, RTS.Nat 5 ]
           ]
           facts
+
+  , TestLabel "cycle closed by a later derive declaration" $ TestCase $ do
+    -- P is declared without a derivation in x.1 and only gets one in x.2,
+    -- closing the cycle P -> Q -> P across schemas.
+    withSchemaAndFacts [enableRecursion]
+      [s|
+        schema x.1 {
+          predicate Base : nat
+          predicate P : nat
+          predicate Q : nat
+            A where x.P.1 A
+        }
+        schema x.2 : x.1 {
+          derive x.P.1
+            A where x.Base.1 A | x.Q.1 A
+        }
+        schema all.1 : x.2 {}
+      |]
+      [ mkBatch (PredicateRef "x.Base" 1)
+          [ [s|{ "key": 1 }|]
+          , [s|{ "key": 2 }|]
+          ]
+      ]
+      $ \env repo schema -> do
+        p <- decodeResultsAs "x.P.1" schema =<< runQ env repo [s| x.P.1 _ |]
+        assertEqual "P uses the derivation from x.2"
+          [ RTS.Nat 1, RTS.Nat 2 ] p
+        q <- decodeResultsAs "x.Q.1" schema =<< runQ env repo [s| x.Q.1 _ |]
+        assertEqual "Q sees P's derivation from x.2"
+          [ RTS.Nat 1, RTS.Nat 2 ] q
   ]
   where
     runQ env repo query =

From d3d7b781f8c35c6cef41c443cf9b9f03c22fcdcf Mon Sep 17 00:00:00 2001
From: Marcelo Lazaroni <lazaronijunior@gmail.com>
Date: Sun, 27 Sep 2026 18:45:07 +0100
Subject: [PATCH 5/9] Test that recursive derivations typecheck

Summary:
Add two cases to `angle-test-recursion` checking that schemas with
recursive derivations are accepted:

* non-linear recursion, where a derivation refers to itself twice
  (`Path { A, X }; Path { X, B }`)
* mutual recursion between two derived predicates (R and S)

Both already pass: all predicates of a schema are in scope before any
derivation is typechecked, and predicate types are declared, so a
derivation can refer to itself or to predicates that refer back to it
without any typechecker changes. These tests guard that property as
recursion support is developed.
---
 glean/test/tests/Angle/RecursionTest.hs | 37 +++++++++++++++++++++++++
 1 file changed, 37 insertions(+)

diff --git a/glean/test/tests/Angle/RecursionTest.hs b/glean/test/tests/Angle/RecursionTest.hs
index 0e8a65ff9c..506b1e5482 100644
--- a/glean/test/tests/Angle/RecursionTest.hs
+++ b/glean/test/tests/Angle/RecursionTest.hs
@@ -93,6 +93,43 @@ recursionTest = TestList
           ]
           facts
 
+  , TestLabel "non-linear recursion typechecks" $ TestCase $ do
+    withSchemaAndFacts [enableRecursion]
+      [s|
+        schema x.1 {
+          type Node = nat
+          predicate Edge : { from: Node, to: Node }
+          predicate Path : { from: Node, to: Node }
+            { A, B } where
+              (Path { A, X }; Path { X, B }) | Edge { A, B }
+        }
+        schema all.1 : x.1 {}
+      |]
+      [ mkBatch (PredicateRef "x.Edge" 1)
+          [ [s|{ "key": { "from": 1, "to": 2 } }|]
+          ]
+      ]
+      $ \_ _ _ -> return ()
+
+  , TestLabel "mutual recursion typechecks" $ TestCase $ do
+    withSchemaAndFacts [enableRecursion]
+      [s|
+        schema x.1 {
+          predicate P : nat
+          predicate Q : nat
+          predicate R : nat
+            A where P A | S A
+          predicate S : nat
+            A where Q A | R A
+        }
+        schema all.1 : x.1 {}
+      |]
+      [ mkBatch (PredicateRef "x.P" 1)
+          [ [s|{ "key": 1 }|]
+          ]
+      ]
+      $ \_ _ _ -> return ()
+
   , TestLabel "cycle closed by a later derive declaration" $ TestCase $ do
     -- P is declared without a derivation in x.1 and only gets one in x.2,
     -- closing the cycle P -> Q -> P across schemas.

From 122e2b84b679277d533d9911e341bb29e2b7a881 Mon Sep 17 00:00:00 2001
From: Marcelo Lazaroni <lazaronijunior@gmail.com>
Date: Sun, 27 Sep 2026 18:55:34 +0100
Subject: [PATCH 6/9] Test more shapes of recursive derivations

Summary:
Add two cases to `angle-test-recursion`:

* A recursive derivation that uses a derived predicate which is not
  itself recursive (`Path` built from `Step`, `Step` from `Edge`). The
  non-recursive predicate is inlined into each expansion of the
  recursive one, and pruning has to handle an acyclic dependency of a
  recursive component.
* A derived predicate whose type refers to itself (`Chain`, which copies
  a linked list of `Node` facts), so the key of each derived fact refers
  to another derived fact.

Both check query results, not just that the schema is accepted. Both
already pass.
---
 glean/test/tests/Angle/RecursionTest.hs | 65 +++++++++++++++++++++++++
 1 file changed, 65 insertions(+)

diff --git a/glean/test/tests/Angle/RecursionTest.hs b/glean/test/tests/Angle/RecursionTest.hs
index 506b1e5482..5a10ca0f25 100644
--- a/glean/test/tests/Angle/RecursionTest.hs
+++ b/glean/test/tests/Angle/RecursionTest.hs
@@ -11,6 +11,7 @@ module Angle.RecursionTest (main) where
 
 import Control.Exception
 import Data.Default (def)
+import Data.List (sort)
 import Data.Text (Text, unpack)
 import Test.HUnit
 
@@ -159,6 +160,70 @@ recursionTest = TestList
         q <- decodeResultsAs "x.Q.1" schema =<< runQ env repo [s| x.Q.1 _ |]
         assertEqual "Q sees P's derivation from x.2"
           [ RTS.Nat 1, RTS.Nat 2 ] q
+
+  , TestLabel "recursion using a non-recursive derived predicate" $
+    TestCase $ do
+    -- Step is derived but not recursive, so it is inlined into each
+    -- expansion of Path.
+    withSchemaAndFacts [enableRecursion]
+      [s|
+        schema x.1 {
+          type Node = nat
+          predicate Edge : { from: Node, to: Node }
+          predicate Step : { from: Node, to: Node }
+            { A, B } where Edge { A, B }
+          predicate Path : { from: Node, to: Node }
+            { A, B } where
+              Step { A, B } | (Path { A, K }; Step { K, B })
+        }
+        schema all.1 : x.1 {}
+      |]
+      [ mkBatch (PredicateRef "x.Edge" 1)
+          [ [s|{ "key": { "from": 1, "to": 2 } }|]
+          , [s|{ "key": { "from": 2, "to": 3 } }|]
+          ]
+      ]
+      $ \env repo schema -> do
+        facts <- decodeResultsAs "x.Path.1" schema =<< runQ env repo
+          [s| x.Path _ |]
+        assertEqual "result content"
+          [ RTS.Tuple [ RTS.Nat 1, RTS.Nat 2 ]
+          , RTS.Tuple [ RTS.Nat 1, RTS.Nat 3 ]
+          , RTS.Tuple [ RTS.Nat 2, RTS.Nat 3 ]
+          ]
+          (sort facts)
+
+  , TestLabel "derived predicate whose type refers to itself" $
+    TestCase $ do
+    -- Chain copies a linked list of Node facts, so the key of each
+    -- derived Chain fact refers to another derived Chain fact.
+    withSchemaAndFacts [enableRecursion]
+      [s|
+        schema x.1 {
+          predicate Node : { label : nat, next : maybe Node }
+          predicate Chain : { label : nat, next : maybe Chain }
+            { L, N } where
+              Node { L, M };
+              (M = nothing; N = nothing) |
+              (M = { just = Node { L2, _ } }; N = { just = Chain { L2, _ } })
+        }
+        schema all.1 : x.1 {}
+      |]
+      -- 1 -> 2 -> 3
+      [ mkBatch (PredicateRef "x.Node" 1)
+          [ [s|{ "id": 1, "key": { "label": 3 } }|]
+          , [s|{ "id": 2, "key": { "label": 2, "next": 1 } }|]
+          , [s|{ "id": 3, "key": { "label": 1, "next": 2 } }|]
+          ]
+      ]
+      $ \env repo schema -> do
+        chains <- decodeResultsAs "x.Chain.1" schema =<< runQ env repo
+          [s| x.Chain _ |]
+        assertEqual "one Chain fact per Node" 3 (length chains)
+        list <- decodeResultsAs "x.Chain.1" schema =<< runQ env repo
+          [s| x.Chain { 1, { just = x.Chain { 2, { just = x.Chain { 3, nothing } } } } } |]
+        assertEqual "Chain facts form the same list as Node facts"
+          1 (length list)
   ]
   where
     runQ env repo query =

From 3e8e110fe8890f6419d7e3cb714ff72e6c01facf Mon Sep 17 00:00:00 2001
From: Marcelo Lazaroni <lazaronijunior@gmail.com>
Date: Sun, 27 Sep 2026 19:23:24 +0100
Subject: [PATCH 7/9] Reject recursion through negation

Summary:
With recursive derivations a predicate could be defined in terms of its
own negation:

    predicate P : nat
      A where Base A; !(Q A)
    predicate Q : nat
      A where P A

Such a schema has no sensible meaning: P 1 exists only if Q 1 doesn't,
and Q 1 exists only if P 1 does. Require schemas to be stratified: no
predicate may depend negatively on itself, directly or through other
predicates. Negating a recursive predicate is still allowed when the
negation isn't part of the recursion, e.g. a recursive `NeedsFlying`
that negates a recursive `LandRoute` which doesn't depend on it.

A dependency is negative when the predicate is searched inside `!(...)`,
in the condition of an `if` (the else branch runs when the condition has
no results), or inside `all (...)` (the set it builds changes as facts
are added). `tcQueryNegativeDeps` collects these.

`checkStratification` finds the recursive components of the derivation
graph and reports every negative dependency between two predicates of
the same component, with the cycle it closes:

    recursion through negation is not allowed. These predicates depend
    on their own negation:
      x.P.1 -> !x.Q.1 -> x.P.1

It runs in `mkDbSchema`, next to the check that stored predicates don't
use negation, so it applies when opening a DB and in `validateSchema`,
independently of `--experimental-recursion`. A schema without recursive
derivations is trivially stratified, and the check only inspects the
queries of predicates in recursive components. Unlike
`checkRecursiveDefinitions` it includes `default` derivations; see
Note [Stratification].

Test: new `stratification` group in `angle-test-recursion` with four
rejected schemas (negation, self-negation, if condition, all), which are
accepted without this change, and the NeedsFlying/LandRoute schema, which
is accepted. Also a recursion test where a recursive `Path` negates a
stored predicate, checking the results. `angle-test-derived`,
`angle-test-angle` (which loads all of `glean/schema/source`) and
`schematest` pass.
---
 glean/db/Glean/Database/Schema.hs       |  97 +++++++++++++++++++
 glean/db/Glean/Query/Typecheck.hs       |  56 +++++++++++
 glean/test/tests/Angle/RecursionTest.hs | 123 +++++++++++++++++++++++-
 3 files changed, 275 insertions(+), 1 deletion(-)

diff --git a/glean/db/Glean/Database/Schema.hs b/glean/db/Glean/Database/Schema.hs
index bc8887765b..240387e0fc 100644
--- a/glean/db/Glean/Database/Schema.hs
+++ b/glean/db/Glean/Database/Schema.hs
@@ -461,6 +461,11 @@ mkDbSchema toList cacheVar knownPids dbContent
             $ "use of " <> feature  <> " is not allowed in a stored predicate: "
             <> showRef (predicateRef d)
 
+    -- Check that no predicate depends on its own negation.
+    -- See Note [Stratification]
+    either (throwIO . Thrift.Exception) return $
+      checkStratification (tcEnvPredicates tcEnv)
+
     let
         predicates = snd <$> toList (tcEnvPredicates tcEnv)
 
@@ -967,6 +972,98 @@ derivationEdges preds =
   , Derive _ (QueryWithInfo query _ _ _)  <- [predicateDeriving details]
   ]
 
+{- Note [Stratification]
+
+Recursive derivations shouldn't let us define a fact in terms of its own
+negation:
+
+  predicate P : nat
+    A where Base A; !(Q A)
+  predicate Q : nat
+    A where P A
+
+Here a fact P 1 exists only if Q 1 doesn't, and Q 1 exists only if P 1
+does, so there's no sensible answer. We rule this out by requiring the
+schema to be stratified: no predicate may depend negatively on itself,
+directly or through other predicates. Negation of a recursive predicate
+is fine as long as the negation isn't part of the recursion, because then
+there is no way to have this kid of contradictory specification.
+
+A dependency is negative when the predicate is searched inside a
+negation, in the condition of an if, or inside `all` (see
+tcQueryNegativeDeps).
+
+Unlike checkRecursiveDefinitions, we include default derivations. Pairs of
+default derivations used for schema migration form cycles, but they don't
+negate each other, and if a default derivation ever were part of a cycle
+through negation it would be unsound whenever it is enabled.
+-}
+
+-- | Check that no predicate depends negatively on itself, directly or
+-- through other predicates. See Note [Stratification].
+checkStratification :: HashMap PredicateId PredicateDetails -> Either Text ()
+checkStratification preds =
+  unless (null violations) $ Left $ Text.unlines $
+    "recursion through negation is not allowed. These predicates depend "
+      <> "on their own negation:"
+    : [ "  " <> Text.intercalate " -> "
+          (showPred ref : ("!" <> showPred neg) : map showPred (drop 1 path))
+      | (ref, neg) <- violations
+      , let path = pathWithin neg ref
+      ]
+    ++ [ "(!P means that P is negated, used in the condition of an if, "
+          <> "or used inside all)" ]
+  where
+    edges = derivationEdges preds
+
+    deps :: HashMap PredicateId [PredicateId]
+    deps = HashMap.fromList [ (ref, ds) | (_, ref, ds) <- edges ]
+
+    depsOf :: PredicateId -> [PredicateId]
+    depsOf p = HashMap.lookupDefault [] p deps
+
+    -- the recursive component that each recursive predicate belongs to
+    componentOf :: HashMap PredicateId Int
+    componentOf = HashMap.fromList
+      [ (ref, n)
+      | (n, CyclicSCC refs) <- zip [0..] components
+      , ref <- refs
+      ]
+      where
+      components = stronglyConnComp [ (ref, ref, ds) | (_, ref, ds) <- edges ]
+
+    sameComponent a b =
+      isJust (HashMap.lookup a componentOf)
+      && HashMap.lookup a componentOf == HashMap.lookup b componentOf
+
+    -- (P, Q) where P's derivation depends negatively on Q and Q is in
+    -- the same recursive component as P.
+    violations :: [(PredicateId, PredicateId)]
+    violations = sort
+      [ (ref, neg)
+      | (query, ref, _) <- edges
+      , HashMap.member ref componentOf
+      , neg <- Set.toList (tcQueryNegativeDeps query)
+      , sameComponent ref neg
+      ]
+
+    -- Shortest path of dependencies from one predicate to another in the
+    -- same recursive component, including both ends.
+    pathWithin :: PredicateId -> PredicateId -> [PredicateId]
+    pathWithin from to = go [(from, [])] (HashSet.singleton from)
+      where
+      go [] _ = [from, to] -- unreachable: they are in the same component
+      go ((p, path) : rest) seen
+        | p == to = reverse (p : path)
+        | otherwise =
+          go (rest ++ [ (n, p : path) | n <- next ])
+            (foldr HashSet.insert seen next)
+        where
+        next =
+          [ n | n <- depsOf p, sameComponent n to, not (HashSet.member n seen) ]
+
+    showPred = showRef . predicateIdRef
+
 -- | Check that the type of a stored predicate doesn't refer to any
 -- derived predicates.
 checkStoredType
diff --git a/glean/db/Glean/Query/Typecheck.hs b/glean/db/Glean/Query/Typecheck.hs
index b931644b71..b3bbcc02af 100644
--- a/glean/db/Glean/Query/Typecheck.hs
+++ b/glean/db/Glean/Query/Typecheck.hs
@@ -21,6 +21,7 @@ module Glean.Query.Typecheck
   , defaultTcOpts
   , emptyTcEnv
   , tcQueryDeps
+  , tcQueryNegativeDeps
   , tcQueryUsesNegation
   , UseOfNegation(..)
   ) where
@@ -1024,6 +1025,61 @@ tcQueryDeps q = Set.fromList $ map getRef (overQuery q)
       TcDemote _ p -> overPat p
       TcStructPat fs -> foldMap overPat (map snd fs)
 
+-- | Predicates that a query depends on negatively. These are the
+-- predicates searched in any context where adding facts of the predicate
+-- can change the query's results, rather than only add to them:
+--
+-- * inside a negation @!(...)@
+-- * in the condition of @if ... then ... else ...@, because the else
+--   branch runs when the condition has no results
+-- * inside @all (...)@, because the set of results it builds changes
+--
+-- A predicate must not depend negatively on itself, directly or through
+-- other predicates (see 'Glean.Database.Schema.checkStratification').
+tcQueryNegativeDeps :: TcQuery -> Set PredicateId
+tcQueryNegativeDeps q = Set.fromList $ map getRef (overQuery False q)
+  where
+    getRef (PidRef _ ref) = ref
+
+    -- The Bool says whether we are in a negative context.
+    overQuery :: Bool -> TcQuery -> [PidRef]
+    overQuery neg (TcQuery _ key mval stmts _) =
+      overPat neg key
+        <> maybe [] (overPat neg) mval
+        <> foldMap (overStatement neg) stmts
+
+    overStatement :: Bool -> TcStatement -> [PidRef]
+    overStatement neg (TcStatement _ lhs rhs) =
+      overPat neg lhs <> overPat neg rhs
+
+    overPat :: Bool -> TcPat -> [PidRef]
+    overPat neg = foldMap (bifoldMap (overTyped neg) (const mempty))
+
+    overTyped :: Bool -> Typed TcTerm -> [PidRef]
+    overTyped neg (Typed _ tcTerm) = overTerm neg tcTerm
+
+    overTerm :: Bool -> TcTerm -> [PidRef]
+    overTerm neg = \case
+      TcFactGen pref x y _ ->
+        [ pref | neg ] <> overPat neg x <> overPat neg y
+      TcNegation p -> overPat True p
+      TcIf (Typed _ x) y z -> overPat True x <> foldMap (overPat neg) [y, z]
+      TcAll p -> overPat True p
+      TcOr x y -> overPat neg x <> overPat neg y
+      TcElementsOfArray x -> overPat neg x
+      TcElementsOfSet x -> overPat neg x
+      TcElementsUnresolved _ x -> overPat neg x
+      TcWhere q -> overQuery neg q
+      TcPrimCall _ xs -> foldMap (overPat neg) xs
+      -- Dereferencing looks up the key of a fact we already have, which
+      -- doesn't change as more facts are added.
+      TcDeref _ p -> overPat neg p
+      TcFieldSelect (Typed _ p) _ -> overPat neg p
+      TcAltSelect (Typed _ p) _ -> overPat neg p
+      TcPromote _ p -> overPat neg p
+      TcDemote _ p -> overPat neg p
+      TcStructPat fs -> foldMap (overPat neg . snd) fs
+
 data UseOfNegation
   = PatternNegation
   | IfStatement
diff --git a/glean/test/tests/Angle/RecursionTest.hs b/glean/test/tests/Angle/RecursionTest.hs
index 5a10ca0f25..d85f8e1e1c 100644
--- a/glean/test/tests/Angle/RecursionTest.hs
+++ b/glean/test/tests/Angle/RecursionTest.hs
@@ -11,13 +11,14 @@ module Angle.RecursionTest (main) where
 
 import Control.Exception
 import Data.Default (def)
-import Data.List (sort)
+import Data.List (isInfixOf, sort)
 import Data.Text (Text, unpack)
 import Test.HUnit
 
 import TestRunner
 import Util.String.Quasi
 
+import Glean.Angle.Types (latestAngleVersion)
 import Glean.Database.Schema.Types
 import Glean.Database.Config (Config(..))
 import Glean.Init
@@ -224,7 +225,42 @@ recursionTest = TestList
           [s| x.Chain { 1, { just = x.Chain { 2, { just = x.Chain { 3, nothing } } } } } |]
         assertEqual "Chain facts form the same list as Node facts"
           1 (length list)
+
+  , TestLabel "accepts negation of a non-recursive predicate in recursion" $
+    TestCase $ do
+    withSchemaAndFacts [enableRecursion]
+      [s|
+        schema x.1 {
+          type Node = nat
+          predicate Edge : { from: Node, to: Node }
+          predicate Blocked : { from: Node, to: Node }
+          predicate Path : { from: Node, to: Node }
+            { A, B } where
+              (x.Edge { A, B }; !(x.Blocked { A, B })) |
+              (x.Path { A, K }; x.Edge { K, B }; !(x.Blocked { K, B }))
+        }
+        schema all.1 : x.1 {}
+      |]
+      -- 1 -> 2 -x-> 3 -> 4
+      [ mkBatch (PredicateRef "x.Edge" 1)
+          [ [s|{ "key": { "from": 1, "to": 2 } }|]
+          , [s|{ "key": { "from": 2, "to": 3 } }|]
+          , [s|{ "key": { "from": 3, "to": 4 } }|]
+          ]
+      , mkBatch (PredicateRef "x.Blocked" 1)
+          [ [s|{ "key": { "from": 2, "to": 3 } }|]
+          ]
+      ]
+      $ \env repo schema -> do
+        facts <- decodeResultsAs "x.Path.1" schema =<< runQ env repo
+          [s| x.Path _ |]
+        assertEqual "result content"
+          [ RTS.Tuple [ RTS.Nat 1, RTS.Nat 2 ]
+          , RTS.Tuple [ RTS.Nat 3, RTS.Nat 4 ]
+          ]
+          (sort facts)
   ]
+
   where
     runQ env repo query =
       try $ userQuery env repo $ def
@@ -261,7 +297,92 @@ recursionTest = TestList
             unpack (showRef ref) <> ": " <> unpack err
           Right details -> predicateKeyType details
 
+stratificationTest :: Test
+stratificationTest = TestList
+  [ TestLabel "rejects recursion through negation" $ TestCase $
+    withSchema latestAngleVersion
+      [s|
+        schema x.1 {
+          predicate Base : nat
+          predicate P : nat
+            A where x.Base A; !(x.Q A)
+          predicate Q : nat
+            A where x.P A
+        }
+        schema all.1 : x.1 {}
+      |]
+      (assertRejected "x.P.1 -> !x.Q.1 -> x.P.1")
+
+  , TestLabel "rejects a predicate negating itself" $ TestCase $
+    withSchema latestAngleVersion
+      [s|
+        schema x.1 {
+          predicate Base : nat
+          predicate P : nat
+            A where x.Base A; !(x.P A)
+        }
+        schema all.1 : x.1 {}
+      |]
+      (assertRejected "x.P.1 -> !x.P.1")
+
+  , TestLabel "rejects recursion through an if condition" $ TestCase $
+    withSchema latestAngleVersion
+      [s|
+        schema x.1 {
+          predicate Base : nat
+          predicate P : nat
+            B where x.Base A; B = if (x.P A) then A else 0
+        }
+        schema all.1 : x.1 {}
+      |]
+      (assertRejected "x.P.1 -> !x.P.1")
+
+  , TestLabel "rejects recursion through all" $ TestCase $
+    withSchema latestAngleVersion
+      [s|
+        schema x.1 {
+          predicate Base : nat
+          predicate P : nat
+            A where x.Base A; _ = all (x.P A)
+        }
+        schema all.1 : x.1 {}
+      |]
+      (assertRejected "x.P.1 -> !x.P.1")
+
+  , TestLabel "accepts negation of a recursive predicate outside its cycle" $
+    TestCase $
+    -- NeedsFlying and LandRoute are both recursive, and NeedsFlying
+    -- negates LandRoute, but LandRoute doesn't depend on NeedsFlying.
+    withSchema latestAngleVersion
+      [s|
+        schema x.1 {
+          type Town = nat
+          predicate Road : { begin : Town, end : Town }
+          predicate FlightRoute : { from : Town, to : Town }
+          predicate LandRoute : { from : Town, to : Town }
+            { From, To } where
+              x.Road { From, To } |
+              (x.LandRoute { From, X }; x.Road { X, To })
+          predicate NeedsFlying : { from : Town, to : Town }
+            { From, To } where
+              !(x.LandRoute { From, To });
+              x.FlightRoute { From, To } |
+              (x.NeedsFlying { From, X }; x.FlightRoute { X, To })
+        }
+        schema all.1 : x.1 {}
+      |]
+      (either (assertFailure . show) return)
+  ]
+  where
+    assertRejected :: String -> Either SomeException () -> IO ()
+    assertRejected expected r = case r of
+      Left err ->
+        assertBool ("error should mention " <> expected <> ":\n" <> show err) $
+          expected `isInfixOf` show err
+      Right () -> assertFailure "schema was accepted"
+
 main :: IO ()
 main = withUnitTest $ testRunner $ TestList
   [ TestLabel "recursion" recursionTest
+  , TestLabel "stratification" stratificationTest
   ]

From 9f07379db694a00d83e8af22c44c506911f6890f Mon Sep 17 00:00:00 2001
From: Marcelo Lazaroni <lazaronijunior@gmail.com>
Date: Sun, 27 Sep 2026 19:42:53 +0100
Subject: [PATCH 8/9] Find uses of negation through recursive derivations

Summary:
Stored predicates may not use negation, directly or through the derived
predicates they depend on (Note [Negation in stored predicates]).
`usesOfNegation` finds those uses by visiting derivations in topological
order and marking a predicate if it uses negation itself or if one of its
already-visited dependencies does.

With a recursive pair P <-> Q where only Q uses negation, whichever of
the two is visited first doesn't see Q marked yet. When P comes first it
is left unmarked, so a stored predicate that depends on P is accepted
even though it depends on negation through Q.

Now we visit one strongly connected component at a time, in dependency
order. Since the members of a recursive component depend on each other,
they all use negation if any of them does, directly or through a
dependency outside the component. Acyclic predicates are handled as
before.

This also drops the branch that deleted a predicate from the map when it
didn't use negation: each predicate is visited once, starting from an
empty map, so there was never anything to delete.

Test: "negation - stored dependency on recursion" in `schematest`
checks a stored predicate depending on a recursive pair, both ways round
so the result can't depend on the visiting order. One of the two was
accepted before this change. `angle-test-recursion`, `angle-test-derived`
and `angle-test-angle` pass.
---
 glean/db/Glean/Database/Schema.hs | 39 +++++++++++++++++++------------
 glean/test/tests/Schema/Basic.hs  | 37 +++++++++++++++++++++++++++++
 2 files changed, 61 insertions(+), 15 deletions(-)

diff --git a/glean/db/Glean/Database/Schema.hs b/glean/db/Glean/Database/Schema.hs
index 240387e0fc..5e3ceed6f7 100644
--- a/glean/db/Glean/Database/Schema.hs
+++ b/glean/db/Glean/Database/Schema.hs
@@ -945,23 +945,32 @@ usesOfNegation
   :: HashMap PredicateId PredicateDetails
   -> HashMap PredicateId UseOfNegation
 usesOfNegation preds =
-  foldl' recordUseOfNegation mempty derivations
+  -- Components come in reverse topological order, so by the time we
+  -- process a component all components it depends on have been processed.
+  foldl' addComponent mempty $
+    stronglyConnComp [ (d, ref, deps) | d@(_, ref, deps) <- derivations ]
   where
-    recordUseOfNegation usesNegation (mUseOfNeg, ref, deps)
-      | Just use <- mUseOfNeg
-      = HashMap.insert ref use usesNegation
-      | Just use <- firstJust (`HashMap.lookup` usesNegation) deps
-      = HashMap.insert ref use usesNegation
-      | otherwise
-      -- remove from Map in case a derived predicate in this schema that does
-      -- not use negation overrode a derived predicate that used negation.
-      = HashMap.delete ref usesNegation
-
-    -- derivations in dependency order with flag for use of negation
+    -- The members of a recursive component depend on each other, so if
+    -- one of them uses negation, directly or through a dependency outside
+    -- the component, they all do.
+    addComponent usesNegation component =
+      case uses of
+        Nothing -> usesNegation
+        Just use -> foldl' (\m ref -> HashMap.insert ref use m) usesNegation
+          [ ref | (_, ref, _) <- members ]
+      where
+      members = flattenSCC component
+      uses =
+        firstJust (\(use, _, _) -> use) members <|>
+        firstJust (`HashMap.lookup` usesNegation)
+          (concat [ deps | (_, _, deps) <- members ])
+
+    -- derivations with flag for use of negation
     derivations :: [(Maybe UseOfNegation, PredicateId, [PredicateId])]
-    derivations = toPred . getNode <$> reverse (topSort graph)
-    (graph, getNode, _) = graphFromEdges $ derivationEdges preds
-    toPred (b, k, ks) = (tcQueryUsesNegation b, k, ks)
+    derivations =
+      [ (tcQueryUsesNegation query, ref, deps)
+      | (query, ref, deps) <- derivationEdges preds
+      ]
 
 derivationEdges
   :: HashMap PredicateId PredicateDetails
diff --git a/glean/test/tests/Schema/Basic.hs b/glean/test/tests/Schema/Basic.hs
index 74e56981a6..c6f58ecc7c 100644
--- a/glean/test/tests/Schema/Basic.hs
+++ b/glean/test/tests/Schema/Basic.hs
@@ -687,6 +687,43 @@ schemaNegation =
           Left e -> "negation is not allowed in a stored predicate"
             `isInfixOf` show e
           _ -> False
+
+  , TestLabel "negation - stored dependency on recursion" $ TestCase $
+    -- Stored depends on one predicate of a recursive pair and only the
+    -- other one uses negation. Check it both ways round, so the result
+    -- can't depend on the order in which the pair is processed.
+    forM_
+      [ [s|
+          schema test.1 {
+            predicate Base : string
+            predicate P : string
+              A where Base A | Q A;
+            predicate Q : string
+              A where P A; !(A = "x"..);
+            predicate Stored : string
+              stored A where P A
+          }
+          schema all.1 : test.1 {}
+        |]
+      , [s|
+          schema test.1 {
+            predicate Base : string
+            predicate P : string
+              A where Base A | Q A; !(A = "x"..);
+            predicate Q : string
+              A where P A;
+            predicate Stored : string
+              stored A where Q A
+          }
+          schema all.1 : test.1 {}
+        |]
+      ] $ \schema ->
+      withSchema latestAngleVersion schema $ \r ->
+      assertBool "schemaNegation - stored dependency on recursion" $
+        case r of
+          Left e -> "negation is not allowed in a stored predicate"
+            `isInfixOf` show e
+          _ -> False
   ]
 
 thinSchemaTest :: Test

From 98a679917721e98a04e4e3dce4a8e64f4033c83a Mon Sep 17 00:00:00 2001
From: Marcelo Lazaroni <lazaronijunior@gmail.com>
Date: Sun, 27 Sep 2026 19:58:43 +0100
Subject: [PATCH 9/9] Reject stored predicates that involve recursion

Summary:
Stored predicates can't be recursive, or depend on recursive
predicates, for now. There are two problems with them:

* A recursive stored predicate depends on itself, and `checkConstraints`
  in `Glean.Query.Derive` only starts a derivation once all dependencies
  are complete. So `glean derive` would refuse it with an unhelpful
  "incomplete dependencies" error naming the predicate itself, and two
  stored predicates in the same cycle would each wait for the other.

* Ownership would be wrong. A derived fact's owners are taken from the
  facts being searched when it is created. A recursive derivation
  searches facts derived earlier in the same query, which live in the
  query's FactSet, and `FactSet::getOwner` returns `INVALID_USET`. So the
  owners of the facts they came from are dropped, and an incremental DB
  could keep derived facts it should exclude. This affects any stored
  predicate whose derivation involves recursion, not only recursive ones.

`checkStoredRecursion` runs in `mkDbSchema` next to the other schema
checks and reports each stored predicate that is recursive or depends on
a recursive predicate:

    recursion is not supported in stored predicates yet:
      x.Reachable.1 depends on the recursive predicate x.Path.1

Default derivations are left out of the graph: a pair of default
derivations that refer to each other (the schema migration pattern) is
never enabled at the same time, so a stored predicate reading such a
predicate doesn't depend on recursion. See
Note [Recursion in stored predicates].

Supporting this later needs ownership for facts derived within a query
(the "Incrementality" part of the recursion design).

Test: new `stored predicates` group in `angle-test-recursion`: a
recursive stored predicate, a stored predicate in a cycle through an
on-demand one, and a stored predicate using a recursive one are rejected
(all accepted without this change); a stored predicate reading a
predicate with a default derivation pair is accepted. `angle-test-derived`,
`angle-test-stored`, `angle-test-angle` (all of `glean/schema/source`) and
`schematest` pass.
---
 glean/db/Glean/Database/Schema.hs       | 77 +++++++++++++++++++++
 glean/test/tests/Angle/RecursionTest.hs | 90 ++++++++++++++++++++++---
 2 files changed, 159 insertions(+), 8 deletions(-)

diff --git a/glean/db/Glean/Database/Schema.hs b/glean/db/Glean/Database/Schema.hs
index 5e3ceed6f7..67869406a1 100644
--- a/glean/db/Glean/Database/Schema.hs
+++ b/glean/db/Glean/Database/Schema.hs
@@ -466,6 +466,11 @@ mkDbSchema toList cacheVar knownPids dbContent
     either (throwIO . Thrift.Exception) return $
       checkStratification (tcEnvPredicates tcEnv)
 
+    -- Check that stored predicates don't involve recursion.
+    -- See Note [Recursion in stored predicates]
+    either (throwIO . Thrift.Exception) return $
+      checkStoredRecursion (tcEnvPredicates tcEnv)
+
     let
         predicates = snd <$> toList (tcEnvPredicates tcEnv)
 
@@ -1073,6 +1078,78 @@ checkStratification preds =
 
     showPred = showRef . predicateIdRef
 
+{- Note [Recursion in stored predicates]
+
+Stored predicates can't be recursive, and can't depend on recursive
+predicates for now ownership would be wrong.
+
+When a derived fact is created, its owners are taken from the facts being
+searched at that point. A recursive derivation searches facts derived earlier
+in the same query, and those live in the query's FactSet, which has no
+ownership information (FactSet::getOwner returns INVALID_USET). So the owners
+of the facts they came from would be lost, and an incremental DB could keep
+derived facts that it should have excluded.
+
+Default derivations are left out. The usual way this is used is where default
+derivations refer to each other but the two aren't enabled at the same time, so
+they don't make the predicates depending on them recursive.
+-}
+
+-- | Check that stored predicates don't involve recursion.
+-- See Note [Recursion in stored predicates].
+checkStoredRecursion :: HashMap PredicateId PredicateDetails -> Either Text ()
+checkStoredRecursion preds =
+  unless (null violations) $ Left $ Text.unlines $
+    "recursion is not supported in stored predicates yet:"
+    : [ "  " <> showPred ref <> problem
+      | (ref, recPred) <- violations
+      , let problem
+              | ref == recPred = " is recursive"
+              | otherwise =
+                " depends on the recursive predicate " <> showPred recPred
+      ]
+  where
+    edges :: [(PredicateId, PredicateId, [PredicateId])]
+    edges =
+      [ (ref, ref, Set.toList (tcQueryDeps query))
+      | (ref, details) <- HashMap.toList preds
+      , Derive when (QueryWithInfo query _ _ _) <- [predicateDeriving details]
+      , case when of
+          DeriveIfEmpty -> False
+          DeriveOnDemand -> True
+          DerivedAndStored -> True
+      ]
+
+    deps :: HashMap PredicateId [PredicateId]
+    deps = HashMap.fromList [ (ref, ds) | (_, ref, ds) <- edges ]
+
+    depsOf :: PredicateId -> [PredicateId]
+    depsOf ref = HashMap.lookupDefault [] ref deps
+
+    -- For each predicate that involves recursion, a recursive predicate
+    -- that it depends on (the predicate itself if it's recursive).
+    -- Components come in reverse topological order, so the dependencies
+    -- of a component have already been added by the time we get to it.
+    recursiveDep :: HashMap PredicateId PredicateId
+    recursiveDep = foldl' add mempty (stronglyConnComp edges)
+      where
+      add m = \case
+        CyclicSCC refs -> foldl' (\m' ref -> HashMap.insert ref ref m') m refs
+        AcyclicSCC ref ->
+          case firstJust (`HashMap.lookup` m) (depsOf ref) of
+            Nothing -> m
+            Just recPred -> HashMap.insert ref recPred m
+
+    violations :: [(PredicateId, PredicateId)]
+    violations = sort
+      [ (ref, recPred)
+      | (ref, details) <- HashMap.toList preds
+      , Derive DerivedAndStored _ <- [predicateDeriving details]
+      , Just recPred <- [HashMap.lookup ref recursiveDep]
+      ]
+
+    showPred = showRef . predicateIdRef
+
 -- | Check that the type of a stored predicate doesn't refer to any
 -- derived predicates.
 checkStoredType
diff --git a/glean/test/tests/Angle/RecursionTest.hs b/glean/test/tests/Angle/RecursionTest.hs
index d85f8e1e1c..528511e91d 100644
--- a/glean/test/tests/Angle/RecursionTest.hs
+++ b/glean/test/tests/Angle/RecursionTest.hs
@@ -18,7 +18,7 @@ import Test.HUnit
 import TestRunner
 import Util.String.Quasi
 
-import Glean.Angle.Types (latestAngleVersion)
+import Glean.Angle.Types (AngleVersion(..), latestAngleVersion)
 import Glean.Database.Schema.Types
 import Glean.Database.Config (Config(..))
 import Glean.Init
@@ -373,16 +373,90 @@ stratificationTest = TestList
       |]
       (either (assertFailure . show) return)
   ]
-  where
-    assertRejected :: String -> Either SomeException () -> IO ()
-    assertRejected expected r = case r of
-      Left err ->
-        assertBool ("error should mention " <> expected <> ":\n" <> show err) $
-          expected `isInfixOf` show err
-      Right () -> assertFailure "schema was accepted"
+
+storedTest :: Test
+storedTest = TestList
+  [ TestLabel "rejects a recursive stored predicate" $ TestCase $
+    withSchema latestAngleVersion
+      [s|
+        schema x.1 {
+          predicate Base : nat
+          predicate P : nat
+            stored A where x.Base A | x.P A
+        }
+        schema all.1 : x.1 {}
+      |]
+      (assertRejected "x.P.1 is recursive")
+
+  , TestLabel "rejects a stored predicate in a cycle" $ TestCase $
+    -- S is stored and R isn't, but deriving S expands R, which refers
+    -- back to S.
+    withSchema latestAngleVersion
+      [s|
+        schema x.1 {
+          predicate Base : nat
+          predicate S : nat
+            stored A where x.R A
+          predicate R : nat
+            A where x.Base A | x.S A
+        }
+        schema all.1 : x.1 {}
+      |]
+      (assertRejected "x.S.1 is recursive")
+
+  , TestLabel "rejects a stored predicate using recursion" $ TestCase $
+    withSchema latestAngleVersion
+      [s|
+        schema x.1 {
+          type Node = nat
+          predicate Edge : { from: Node, to: Node }
+          predicate Path : { from: Node, to: Node }
+            { A, B } where
+              x.Edge { A, B } | (x.Path { A, K }; x.Edge { K, B })
+          predicate Reachable : Node
+            stored B where x.Path { 1, B }
+        }
+        schema all.1 : x.1 {}
+      |]
+      (assertRejected
+        "x.Reachable.1 depends on the recursive predicate x.Path.1")
+
+  , TestLabel "accepts a stored predicate using default derivations" $
+    TestCase $
+    -- P.1 and P.2 derive each other, but only one of the two derivations
+    -- is ever enabled, so Stored doesn't depend on recursion.
+    withSchema (AngleVersion 11)
+      [s|
+        schema test.1 {
+          predicate P : { a : string, b : nat }
+        }
+        schema test.2 : test.1 {
+          predicate P : { a : string, b : nat, c : {} }
+
+          derive test.P.1 default
+            { A, B } where P.2 { A, B, _ }
+
+          derive test.P.2 default
+            { A, B, {} } where test.P.1 { A, B }
+
+          predicate Stored : string
+            stored A where test.P.1 { A, _ }
+        }
+        schema all.1 : test.1, test.2 {}
+      |]
+      (either (assertFailure . show) return)
+  ]
+
+assertRejected :: String -> Either SomeException () -> IO ()
+assertRejected expected r = case r of
+  Left err ->
+    assertBool ("error should mention " <> expected <> ":\n" <> show err) $
+      expected `isInfixOf` show err
+  Right () -> assertFailure "schema was accepted"
 
 main :: IO ()
 main = withUnitTest $ testRunner $ TestList
   [ TestLabel "recursion" recursionTest
   , TestLabel "stratification" stratificationTest
+  , TestLabel "stored predicates" storedTest
   ]