[ty] Check for unsatisfiable bodies before existentially quantifying (astral-sh#29504)

When we existentially quantify a BDD, we calculate `∃X . B` for some set
of typevars `X` and some BDD `B`. If the BDD is never satisfiable, this
is equivalent to `∃X . false`, which can be further simplified to
`false`.

We expect this to be performance neutral at the moment, since
`reduce_inferable` will already simplify the resulting quantified BDD
down to `false` in most cases. We've extracted it for separate review
out of astral-sh#29027, where is has a much more pronounced impact, since it
prevents us from creating existential nodes that we have to repeatedly
walk through during solution extraction.

Author: dcreager

crates/ruff_benchmark/benches/ty_constraint_set.rs

@@ -102,6 +102,44 @@ def combine[T](first: T, second: T, third: T) -> T:
     });
 }
 
+/// Quantify both satisfiable and contradictory bodies containing free variables. The satisfiable
+/// case measures the cost of checking for contradictions when projection still has work to do.
+fn benchmark_constraint_quantification(criterion: &mut Criterion) {
+    const NUM_FUNCTIONS: usize = 128;
+
+    setup_rayon();
+
+    for (name, lower, upper, negation) in [
+        ("satisfiable", "A", "A", ""),
+        ("unsatisfiable", "int", "tuple[A, B]", "not "),
+    ] {
+        let mut code = "from ty_extensions import static_assert\n\
+                        from ty_extensions._internal import ConstraintSet\n\n"
+            .to_string();
+        for i in 0..NUM_FUNCTIONS {
+            writeln!(
+                &mut code,
+                "def check{i}[X, A, B]() -> None:
+    body = ConstraintSet.lower_bound({lower}, X) & ConstraintSet.upper_bound(X, {upper})
+    static_assert({negation}body.exists(tuple[X]))
+"
+            )
+            .ok();
+        }
+
+        criterion.bench_function(
+            &format!("ty_micro[constraint_quantification/{name}]"),
+            |b| {
+                b.iter_batched_ref(
+                    || setup_micro_case(&code),
+                    |Case { db }| assert_eq!(db.check().len(), 0),
+                    BatchSize::SmallInput,
+                );
+            },
+        );
+    }
+}
+
 /// Benchmarks solving many union-bearing upper bounds while inferring a generic call.
 ///
 /// Each callable argument places a distinct union upper bound on `T` through callable-parameter
@@ -680,6 +718,7 @@ criterion_group!(
     constraint_set,
     benchmark_typevar_mapping_large_accumulation,
     benchmark_typevar_mapping_small_accumulations,
+    benchmark_constraint_quantification,
     benchmark_factored_upper_bounds,
     benchmark_many_upper_bound_callbacks,
     benchmark_pandas_tdd,

crates/ty_python_semantic/resources/mdtest/type_properties/constraints.md

@@ -1368,6 +1368,40 @@ def declared_bound[T: str]() -> None:
     static_assert(constraint.solutions(inferable=tuple[T]) is None)
 ```
 
+## Trivial satisfiability checks
+
+The trivial satisfiability checks only recognize the true and false terminal BDDs.
+
+```py
+from ty_extensions import static_assert
+from ty_extensions._internal import ConstraintSet
+
+static_assert(ConstraintSet.always().is_trivially_always_satisfied())
+static_assert(not ConstraintSet.always().is_trivially_never_satisfied())
+static_assert(ConstraintSet.never().is_trivially_never_satisfied())
+static_assert(not ConstraintSet.never().is_trivially_always_satisfied())
+
+def bounded[T]() -> None:
+    constraint = ConstraintSet.equality(T, int)
+    static_assert(not constraint.is_trivially_always_satisfied())
+    static_assert(not constraint.is_trivially_never_satisfied())
+```
+
+Semantic contradictions and tautologies need not be represented as terminal BDDs.
+
+```py
+def nonterminal[T]() -> None:
+    # T = int ∧ T = str
+    impossible = ConstraintSet.equality(T, int) & ConstraintSet.equality(T, str)
+    static_assert(impossible.is_never_satisfied(inferable=tuple[T]))
+    static_assert(not impossible.is_trivially_never_satisfied())
+
+    # ¬(T = int ∧ T = str)
+    tautology = ~impossible
+    static_assert(tautology.is_always_satisfied(inferable=tuple[T]))
+    static_assert(not tautology.is_trivially_always_satisfied())
+```
+
 ## Satisfiability checks exceeding the traversal budget
 
 Independent alternatives can produce too many paths to check within the computation budget. An

crates/ty_python_semantic/resources/mdtest/type_properties/quantification.md

@@ -309,3 +309,72 @@ def alternation[X: (int, str), Y: (int, str)]() -> None:
     missing_str = int_only.exists(tuple[X]).for_all(tuple[Y])
     static_assert(not missing_str)
 ```
+
+## Unsatisfiable bodies with free variables
+
+No type `X` can be both a supertype of `int` and a subtype of `tuple[A, B]`, regardless of what
+types `A` and `B` are specialized to. As an optimization, when quantifying over `X` we detect that
+"eagerly", and reduce the constraint set to the "always false" terminal BDD, instead of evaluating
+the satisfiability of the body each time we solve.
+
+```py
+from ty_extensions import static_assert
+from ty_extensions._internal import ConstraintSet
+
+def impossible[X, A, B]() -> None:
+    body = ConstraintSet.lower_bound(int, X) & ConstraintSet.upper_bound(X, tuple[A, B])
+    # ∃X. int ≤ X ≤ tuple[A, B]
+    impossible = body.exists(tuple[X])
+    # Note that this constraint set is not just never satisfied; it reduces specifically
+    # to the `false` terminal.
+    static_assert(impossible.is_trivially_never_satisfied())
+```
+
+## Satisfiability depends on free variables
+
+There is an `X` satisfying `A ≤ X ≤ int` when `A` is `int`, but not when `A` is `str`. When we
+quantify over `X`, the resulting constraint set must preserve that distinction.
+
+```py
+from ty_extensions._internal import ConstraintSet
+
+def possible[X, A]() -> None:
+    body = ConstraintSet.lower_bound(A, X) & ConstraintSet.upper_bound(X, int)
+    # ∃X. A ≤ X ≤ int
+    quantified = body.exists(tuple[X])
+
+    # (∃X. A ≤ X ≤ int) ∧ A = int
+    valid = quantified & ConstraintSet.equality(A, int)
+    # revealed: tuple[Solution[A=int]]
+    reveal_type(valid.solutions(inferable=tuple[A]))
+
+    # (∃X. A ≤ X ≤ int) ∧ A = str
+    invalid = quantified & ConstraintSet.equality(A, str)
+    # revealed: None
+    reveal_type(invalid.solutions(inferable=tuple[A]))
+```
+
+## Negated inner quantification with free variables
+
+An inner existential can hold for some choices of a free variable and fail for others. Its negation
+must preserve the choices for which it fails when an enclosing existential is evaluated.
+
+```py
+from ty_extensions._internal import ConstraintSet
+
+def nested[X, Y, A]() -> None:
+    # ∃X. X = int ∧ X = A
+    inner = (ConstraintSet.equality(X, int) & ConstraintSet.equality(X, A)).exists(tuple[X])
+    # ∃Y. ¬(∃X. X = int ∧ X = A) ∧ Y = str
+    outer = (~inner & ConstraintSet.equality(Y, str)).exists(tuple[Y])
+
+    # (∃Y. ¬(∃X. X = int ∧ X = A) ∧ Y = str) ∧ A = str
+    valid = outer & ConstraintSet.equality(A, str)
+    # revealed: tuple[Solution[A=str]]
+    reveal_type(valid.solutions(inferable=tuple[A]))
+
+    # (∃Y. ¬(∃X. X = int ∧ X = A) ∧ Y = str) ∧ A = int
+    invalid = outer & ConstraintSet.equality(A, int)
+    # revealed: None
+    reveal_type(invalid.solutions(inferable=tuple[A]))
+```

crates/ty_python_semantic/src/types.rs

@@ -6265,6 +6265,22 @@ impl<'db> Type<'db> {
                     ))
                     .into()
                 }
+                Type::KnownInstance(KnownInstanceType::ConstraintSet(tracked))
+                    if name == "is_trivially_always_satisfied" =>
+                {
+                    Place::bound(Type::KnownBoundMethod(
+                        KnownBoundMethodType::ConstraintSetIsTriviallyAlwaysSatisfied(tracked),
+                    ))
+                    .into()
+                }
+                Type::KnownInstance(KnownInstanceType::ConstraintSet(tracked))
+                    if name == "is_trivially_never_satisfied" =>
+                {
+                    Place::bound(Type::KnownBoundMethod(
+                        KnownBoundMethodType::ConstraintSetIsTriviallyNeverSatisfied(tracked),
+                    ))
+                    .into()
+                }
                 Type::KnownInstance(KnownInstanceType::ConstraintSet(tracked))
                     if name == "with_detailed_display" =>
                 {
@@ -9499,6 +9515,8 @@ impl<'db> Type<'db> {
                         | KnownBoundMethodType::ConstraintSetSolutions(_)
                         | KnownBoundMethodType::ConstraintSetIsAlwaysSatisfied(_)
                         | KnownBoundMethodType::ConstraintSetIsNeverSatisfied(_)
+                        | KnownBoundMethodType::ConstraintSetIsTriviallyAlwaysSatisfied(_)
+                        | KnownBoundMethodType::ConstraintSetIsTriviallyNeverSatisfied(_)
                         | KnownBoundMethodType::ConstraintSetWithDetailedDisplay(_)
                 )
         ) {
@@ -9957,6 +9975,8 @@ impl<'db> Type<'db> {
                 | KnownBoundMethodType::ConstraintSetSolutions(_)
                 | KnownBoundMethodType::ConstraintSetIsAlwaysSatisfied(_)
                 | KnownBoundMethodType::ConstraintSetIsNeverSatisfied(_)
+                | KnownBoundMethodType::ConstraintSetIsTriviallyAlwaysSatisfied(_)
+                | KnownBoundMethodType::ConstraintSetIsTriviallyNeverSatisfied(_)
                 | KnownBoundMethodType::ConstraintSetWithDetailedDisplay(_),
             )
             | Type::DataclassDecorator(_)
@@ -10324,6 +10344,8 @@ impl<'db> Type<'db> {
                 | KnownBoundMethodType::ConstraintSetSolutions(_)
                 | KnownBoundMethodType::ConstraintSetIsAlwaysSatisfied(_)
                 | KnownBoundMethodType::ConstraintSetIsNeverSatisfied(_)
+                | KnownBoundMethodType::ConstraintSetIsTriviallyAlwaysSatisfied(_)
+                | KnownBoundMethodType::ConstraintSetIsTriviallyNeverSatisfied(_)
                 | KnownBoundMethodType::ConstraintSetWithDetailedDisplay(_),
             )
             | Type::DataclassDecorator(_)

crates/ty_python_semantic/src/types/call/bind.rs

@@ -3241,6 +3241,27 @@ impl<'db> Bindings<'db> {
                         ));
                     }
 
+                    Type::KnownBoundMethod(
+                        method @ (KnownBoundMethodType::ConstraintSetIsTriviallyAlwaysSatisfied(
+                            tracked,
+                        )
+                        | KnownBoundMethodType::ConstraintSetIsTriviallyNeverSatisfied(
+                            tracked,
+                        )),
+                    ) => {
+                        let result = tracked.constraints(db).query(|_builder, set| {
+                            if matches!(
+                                method,
+                                KnownBoundMethodType::ConstraintSetIsTriviallyAlwaysSatisfied(_)
+                            ) {
+                                set.is_trivially_always_satisfied()
+                            } else {
+                                set.is_trivially_never_satisfied()
+                            }
+                        });
+                        overload.set_return_type(Type::bool_literal(result));
+                    }
+
                     Type::KnownBoundMethod(KnownBoundMethodType::ConstraintSetSolutions(
                         tracked,
                     )) => {

crates/ty_python_semantic/src/types/constraints.rs

@@ -802,6 +802,29 @@ impl<'db, 'c> ConstraintSet<'db, 'c> {
             return self;
         }
         let mut storage = builder.storage.borrow_mut();
+        // A quantified body is false if no assignment to its locals or free variables can
+        // satisfy it.
+        if let Some(support) = storage.node_support(self.node)
+            && support.is_complete()
+        {
+            let inferable =
+                TypeVarSet::from_typevars(db, support.iter().map(|id| storage.typevar_data(id)));
+            let budget = SolutionBudget::default();
+            let limits = BoundedSolutionLimits {
+                remaining_paths: budget.paths,
+                remaining_visits: budget.visits,
+            };
+            if let ControlFlow::Continue(true) = self.node.is_never_satisfied_with_limits(
+                db,
+                env,
+                &mut storage,
+                inferable,
+                self.source_order,
+                limits,
+            ) {
+                return Self::never(builder);
+            }
+        }
         let (node, derived_source_order) =
             self.node
                 .exists(db, env, &mut storage, to_remove, self.source_order);

crates/ty_python_semantic/src/types/display.rs

@@ -1578,6 +1578,16 @@ impl<'db> FmtDetailed<'db> for DisplayRepresentation<'_, 'db> {
                     KnownBoundMethodType::ConstraintSetWithDetailedDisplay(_) => {
                         return f.write_str("bound method `ConstraintSet.with_detailed_display`");
                     }
+                    KnownBoundMethodType::ConstraintSetIsTriviallyAlwaysSatisfied(_) => {
+                        return f.write_str(
+                            "bound method `ConstraintSet.is_trivially_always_satisfied`",
+                        );
+                    }
+                    KnownBoundMethodType::ConstraintSetIsTriviallyNeverSatisfied(_) => {
+                        return f.write_str(
+                            "bound method `ConstraintSet.is_trivially_never_satisfied`",
+                        );
+                    }
                 };
 
                 f.write_char('<')?;

crates/ty_python_semantic/src/types/infer/comparisons.rs

@@ -393,6 +393,8 @@ impl<'db> Type<'db> {
                         | KnownBoundMethodType::ConstraintSetSolutions(_)
                         | KnownBoundMethodType::ConstraintSetIsAlwaysSatisfied(_)
                         | KnownBoundMethodType::ConstraintSetIsNeverSatisfied(_)
+                        | KnownBoundMethodType::ConstraintSetIsTriviallyAlwaysSatisfied(_)
+                        | KnownBoundMethodType::ConstraintSetIsTriviallyNeverSatisfied(_)
                         | KnownBoundMethodType::ConstraintSetWithDetailedDisplay(_) => {
                             (method, NegativeRetention::Stable)
                         }

crates/ty_python_semantic/src/types/method.rs

@@ -410,6 +410,8 @@ pub enum KnownBoundMethodType<'db> {
     ConstraintSetSolutions(InternedConstraintSet<'db>),
     ConstraintSetIsAlwaysSatisfied(InternedConstraintSet<'db>),
     ConstraintSetIsNeverSatisfied(InternedConstraintSet<'db>),
+    ConstraintSetIsTriviallyAlwaysSatisfied(InternedConstraintSet<'db>),
+    ConstraintSetIsTriviallyNeverSatisfied(InternedConstraintSet<'db>),
     ConstraintSetWithDetailedDisplay(InternedConstraintSet<'db>),
 }
 
@@ -455,6 +457,8 @@ pub(super) fn walk_method_wrapper_type<'db, V: visitor::TypeVisitor<'db> + ?Size
         | KnownBoundMethodType::ConstraintSetSolutions(_)
         | KnownBoundMethodType::ConstraintSetIsAlwaysSatisfied(_)
         | KnownBoundMethodType::ConstraintSetIsNeverSatisfied(_)
+        | KnownBoundMethodType::ConstraintSetIsTriviallyAlwaysSatisfied(_)
+        | KnownBoundMethodType::ConstraintSetIsTriviallyNeverSatisfied(_)
         | KnownBoundMethodType::ConstraintSetWithDetailedDisplay(_) => {}
     }
 }
@@ -519,6 +523,8 @@ impl<'db> KnownBoundMethodType<'db> {
             | KnownBoundMethodType::ConstraintSetSolutions(_)
             | KnownBoundMethodType::ConstraintSetIsAlwaysSatisfied(_)
             | KnownBoundMethodType::ConstraintSetIsNeverSatisfied(_)
+            | KnownBoundMethodType::ConstraintSetIsTriviallyAlwaysSatisfied(_)
+            | KnownBoundMethodType::ConstraintSetIsTriviallyNeverSatisfied(_)
             | KnownBoundMethodType::ConstraintSetWithDetailedDisplay(_) => Some(self),
         }
     }
@@ -547,6 +553,8 @@ impl<'db> KnownBoundMethodType<'db> {
             | KnownBoundMethodType::ConstraintSetSolutions(_)
             | KnownBoundMethodType::ConstraintSetIsAlwaysSatisfied(_)
             | KnownBoundMethodType::ConstraintSetIsNeverSatisfied(_)
+            | KnownBoundMethodType::ConstraintSetIsTriviallyAlwaysSatisfied(_)
+            | KnownBoundMethodType::ConstraintSetIsTriviallyNeverSatisfied(_)
             | KnownBoundMethodType::ConstraintSetWithDetailedDisplay(_) => {
                 KnownClass::ConstraintSet
             }
@@ -834,6 +842,14 @@ impl<'db> KnownBoundMethodType<'db> {
                 )))
             }
 
+            KnownBoundMethodType::ConstraintSetIsTriviallyAlwaysSatisfied(_)
+            | KnownBoundMethodType::ConstraintSetIsTriviallyNeverSatisfied(_) => {
+                Either::Right(std::iter::once(Signature::new(
+                    Parameters::empty(),
+                    KnownClass::Bool.to_instance(db, env),
+                )))
+            }
+
             KnownBoundMethodType::ConstraintSetWithDetailedDisplay(_) => {
                 Either::Right(std::iter::once(Signature::new(
                     Parameters::empty(),
@@ -945,6 +961,14 @@ impl<'c, 'db> TypeRelationChecker<'_, 'c, 'db> {
                 KnownBoundMethodType::ConstraintSetIsNeverSatisfied(_),
                 KnownBoundMethodType::ConstraintSetIsNeverSatisfied(_),
             )
+            | (
+                KnownBoundMethodType::ConstraintSetIsTriviallyAlwaysSatisfied(_),
+                KnownBoundMethodType::ConstraintSetIsTriviallyAlwaysSatisfied(_),
+            )
+            | (
+                KnownBoundMethodType::ConstraintSetIsTriviallyNeverSatisfied(_),
+                KnownBoundMethodType::ConstraintSetIsTriviallyNeverSatisfied(_),
+            )
             | (
                 KnownBoundMethodType::ConstraintSetWithDetailedDisplay(_),
                 KnownBoundMethodType::ConstraintSetWithDetailedDisplay(_),
@@ -972,6 +996,8 @@ impl<'c, 'db> TypeRelationChecker<'_, 'c, 'db> {
                 | KnownBoundMethodType::ConstraintSetSolutions(_)
                 | KnownBoundMethodType::ConstraintSetIsAlwaysSatisfied(_)
                 | KnownBoundMethodType::ConstraintSetIsNeverSatisfied(_)
+                | KnownBoundMethodType::ConstraintSetIsTriviallyAlwaysSatisfied(_)
+                | KnownBoundMethodType::ConstraintSetIsTriviallyNeverSatisfied(_)
                 | KnownBoundMethodType::ConstraintSetWithDetailedDisplay(_),
                 KnownBoundMethodType::FunctionTypeDunderGet(_)
                 | KnownBoundMethodType::DunderCall(_)
@@ -994,6 +1020,8 @@ impl<'c, 'db> TypeRelationChecker<'_, 'c, 'db> {
                 | KnownBoundMethodType::ConstraintSetSolutions(_)
                 | KnownBoundMethodType::ConstraintSetIsAlwaysSatisfied(_)
                 | KnownBoundMethodType::ConstraintSetIsNeverSatisfied(_)
+                | KnownBoundMethodType::ConstraintSetIsTriviallyAlwaysSatisfied(_)
+                | KnownBoundMethodType::ConstraintSetIsTriviallyNeverSatisfied(_)
                 | KnownBoundMethodType::ConstraintSetWithDetailedDisplay(_),
             ) => self.never(),
         }

crates/ty_python_semantic/src/types/relation.rs

@@ -276,6 +276,8 @@ impl<'db> Type<'db> {
                 | KnownBoundMethodType::ConstraintSetSolutions(_)
                 | KnownBoundMethodType::ConstraintSetIsAlwaysSatisfied(_)
                 | KnownBoundMethodType::ConstraintSetIsNeverSatisfied(_)
+                | KnownBoundMethodType::ConstraintSetIsTriviallyAlwaysSatisfied(_)
+                | KnownBoundMethodType::ConstraintSetIsTriviallyNeverSatisfied(_)
                 | KnownBoundMethodType::ConstraintSetWithDetailedDisplay(_),
             )
             | Type::DataclassDecorator(_)