diff --git a/glean.cabal.in b/glean.cabal.in
index 9e5315b9f8..8132e20a3c 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
@@ -2048,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
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/Database/Schema.hs b/glean/db/Glean/Database/Schema.hs
index bc8887765b..67869406a1 100644
--- a/glean/db/Glean/Database/Schema.hs
+++ b/glean/db/Glean/Database/Schema.hs
@@ -461,6 +461,16 @@ 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)
+
+    -- 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)
 
@@ -940,23 +950,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
@@ -967,6 +986,170 @@ 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
+
+{- 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/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/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/Prune.hs b/glean/db/Glean/Query/Prune.hs
index b65b024427..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.
 --
@@ -155,12 +179,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 +264,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..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
@@ -87,32 +88,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 +137,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 +322,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 +361,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 +620,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 +640,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 +793,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 +826,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 +851,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 +864,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 +1013,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
@@ -1050,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
@@ -1095,8 +1125,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/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/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
diff --git a/glean/test/tests/Angle/RecursionTest.hs b/glean/test/tests/Angle/RecursionTest.hs
index c346bc47ae..528511e91d 100644
--- a/glean/test/tests/Angle/RecursionTest.hs
+++ b/glean/test/tests/Angle/RecursionTest.hs
@@ -11,12 +11,14 @@ module Angle.RecursionTest (main) where
 
 import Control.Exception
 import Data.Default (def)
+import Data.List (isInfixOf, sort)
 import Data.Text (Text, unpack)
 import Test.HUnit
 
 import TestRunner
 import Util.String.Quasi
 
+import Glean.Angle.Types (AngleVersion(..), latestAngleVersion)
 import Glean.Database.Schema.Types
 import Glean.Database.Config (Config(..))
 import Glean.Init
@@ -92,7 +94,173 @@ recursionTest = TestList
           , RTS.Tuple [ RTS.Nat 1, RTS.Nat 5 ]
           ]
           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.
+    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
+
+  , 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)
+
+  , 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
@@ -129,7 +297,166 @@ 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)
+  ]
+
+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
   ]
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
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.