From f4e46c9a2c7a10c5eace3b56fcf80810a030bcd9 Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Thu, 13 Nov 2025 08:40:42 -0500
Subject: [PATCH 01/22] add failing test

---
 .../type_properties/implies_subtype_of.md     | 69 ++++++++++++++++++-
 1 file changed, 68 insertions(+), 1 deletion(-)

diff --git a/crates/ty_python_semantic/resources/mdtest/type_properties/implies_subtype_of.md b/crates/ty_python_semantic/resources/mdtest/type_properties/implies_subtype_of.md
index 35768ef76d468..1a72da9464fe8 100644
--- a/crates/ty_python_semantic/resources/mdtest/type_properties/implies_subtype_of.md
+++ b/crates/ty_python_semantic/resources/mdtest/type_properties/implies_subtype_of.md
@@ -173,7 +173,10 @@ def given_constraints[T]():
     static_assert(given_str.implies_subtype_of(T, str))
 ```
 
-This might require propagating constraints from other typevars.
+This might require propagating constraints from other typevars. (Note that we perform the test
+twice, with different variable orderings. Our BDD implementation uses the Salsa IDs of each typevar
+as part of the variable ordering. Reversing the typevar order helps us verify that we don't have any
+BDD logic that is dependent on which variable ordering we end up with.)
 
 ```py
 def mutually_constrained[T, U]():
@@ -183,6 +186,19 @@ def mutually_constrained[T, U]():
     static_assert(not given_int.implies_subtype_of(T, bool))
     static_assert(not given_int.implies_subtype_of(T, str))
 
+    # If [T ≤ U ∧ U ≤ int], then [T ≤ int] must be true as well.
+    given_int = ConstraintSet.range(Never, T, U) & ConstraintSet.range(Never, U, int)
+    static_assert(given_int.implies_subtype_of(T, int))
+    static_assert(not given_int.implies_subtype_of(T, bool))
+    static_assert(not given_int.implies_subtype_of(T, str))
+
+def mutually_constrained[U, T]():
+    # If [T = U ∧ U ≤ int], then [T ≤ int] must be true as well.
+    given_int = ConstraintSet.range(U, T, U) & ConstraintSet.range(Never, U, int)
+    static_assert(given_int.implies_subtype_of(T, int))
+    static_assert(not given_int.implies_subtype_of(T, bool))
+    static_assert(not given_int.implies_subtype_of(T, str))
+
     # If [T ≤ U ∧ U ≤ int], then [T ≤ int] must be true as well.
     given_int = ConstraintSet.range(Never, T, U) & ConstraintSet.range(Never, U, int)
     static_assert(given_int.implies_subtype_of(T, int))
@@ -236,6 +252,22 @@ def mutually_constrained[T, U]():
     static_assert(not given_int.implies_subtype_of(Covariant[T], Covariant[bool]))
     static_assert(not given_int.implies_subtype_of(Covariant[T], Covariant[str]))
 
+    # If (T ≤ U ∧ U ≤ int), then (T ≤ int) must be true as well, and therefore
+    # (Covariant[T] ≤ Covariant[int]).
+    given_int = ConstraintSet.range(Never, T, U) & ConstraintSet.range(Never, U, int)
+    static_assert(given_int.implies_subtype_of(Covariant[T], Covariant[int]))
+    static_assert(not given_int.implies_subtype_of(Covariant[T], Covariant[bool]))
+    static_assert(not given_int.implies_subtype_of(Covariant[T], Covariant[str]))
+
+# Repeat the test with a different typevar ordering
+def mutually_constrained[U, T]():
+    # If (T = U ∧ U ≤ int), then (T ≤ int) must be true as well, and therefore
+    # (Covariant[T] ≤ Covariant[int]).
+    given_int = ConstraintSet.range(U, T, U) & ConstraintSet.range(Never, U, int)
+    static_assert(given_int.implies_subtype_of(Covariant[T], Covariant[int]))
+    static_assert(not given_int.implies_subtype_of(Covariant[T], Covariant[bool]))
+    static_assert(not given_int.implies_subtype_of(Covariant[T], Covariant[str]))
+
     # If (T ≤ U ∧ U ≤ int), then (T ≤ int) must be true as well, and therefore
     # (Covariant[T] ≤ Covariant[int]).
     given_int = ConstraintSet.range(Never, T, U) & ConstraintSet.range(Never, U, int)
@@ -281,6 +313,22 @@ def mutually_constrained[T, U]():
     static_assert(not given_int.implies_subtype_of(Contravariant[bool], Contravariant[T]))
     static_assert(not given_int.implies_subtype_of(Contravariant[str], Contravariant[T]))
 
+    # If (T ≤ U ∧ U ≤ int), then (T ≤ int) must be true as well, and therefore
+    # (Contravariant[int] ≤ Contravariant[T]).
+    given_int = ConstraintSet.range(Never, T, U) & ConstraintSet.range(Never, U, int)
+    static_assert(given_int.implies_subtype_of(Contravariant[int], Contravariant[T]))
+    static_assert(not given_int.implies_subtype_of(Contravariant[bool], Contravariant[T]))
+    static_assert(not given_int.implies_subtype_of(Contravariant[str], Contravariant[T]))
+
+# Repeat the test with a different typevar ordering
+def mutually_constrained[U, T]():
+    # If (T = U ∧ U ≤ int), then (T ≤ int) must be true as well, and therefore
+    # (Contravariant[int] ≤ Contravariant[T]).
+    given_int = ConstraintSet.range(U, T, U) & ConstraintSet.range(Never, U, int)
+    static_assert(given_int.implies_subtype_of(Contravariant[int], Contravariant[T]))
+    static_assert(not given_int.implies_subtype_of(Contravariant[bool], Contravariant[T]))
+    static_assert(not given_int.implies_subtype_of(Contravariant[str], Contravariant[T]))
+
     # If (T ≤ U ∧ U ≤ int), then (T ≤ int) must be true as well, and therefore
     # (Contravariant[int] ≤ Contravariant[T]).
     given_int = ConstraintSet.range(Never, T, U) & ConstraintSet.range(Never, U, int)
@@ -338,6 +386,25 @@ def mutually_constrained[T, U]():
     static_assert(not given_int.implies_subtype_of(Invariant[T], Invariant[bool]))
     static_assert(not given_int.implies_subtype_of(Invariant[T], Invariant[str]))
 
+    # If (T = U ∧ U = int), then (T = int) must be true as well. That is an equality constraint, so
+    # even though T is invariant, it does imply that (Invariant[T] ≤ Invariant[int]).
+    given_int = ConstraintSet.range(U, T, U) & ConstraintSet.range(int, U, int)
+    static_assert(given_int.implies_subtype_of(Invariant[T], Invariant[int]))
+    static_assert(given_int.implies_subtype_of(Invariant[int], Invariant[T]))
+    static_assert(not given_int.implies_subtype_of(Invariant[T], Invariant[bool]))
+    static_assert(not given_int.implies_subtype_of(Invariant[bool], Invariant[T]))
+    static_assert(not given_int.implies_subtype_of(Invariant[T], Invariant[str]))
+    static_assert(not given_int.implies_subtype_of(Invariant[str], Invariant[T]))
+
+# Repeat the test with a different typevar ordering
+def mutually_constrained[U, T]():
+    # If (T = U ∧ U ≤ int), then (T ≤ int) must be true as well. But because T is invariant, that
+    # does _not_ imply that (Invariant[T] ≤ Invariant[int]).
+    given_int = ConstraintSet.range(U, T, U) & ConstraintSet.range(Never, U, int)
+    static_assert(not given_int.implies_subtype_of(Invariant[T], Invariant[int]))
+    static_assert(not given_int.implies_subtype_of(Invariant[T], Invariant[bool]))
+    static_assert(not given_int.implies_subtype_of(Invariant[T], Invariant[str]))
+
     # If (T = U ∧ U = int), then (T = int) must be true as well. That is an equality constraint, so
     # even though T is invariant, it does imply that (Invariant[T] ≤ Invariant[int]).
     given_int = ConstraintSet.range(U, T, U) & ConstraintSet.range(int, U, int)

From ef08334262b2a067bdf61331b48776e92addeb7e Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Thu, 13 Nov 2025 18:45:33 -0500
Subject: [PATCH 02/22] add sequent map

---
 .../src/types/constraints.rs                  | 303 +++++++++++++++++-
 1 file changed, 302 insertions(+), 1 deletion(-)

diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs
index f8b66c33e4aa4..99effabda1a17 100644
--- a/crates/ty_python_semantic/src/types/constraints.rs
+++ b/crates/ty_python_semantic/src/types/constraints.rs
@@ -60,7 +60,7 @@ use std::cmp::Ordering;
 use std::fmt::Display;
 
 use itertools::Itertools;
-use rustc_hash::FxHashSet;
+use rustc_hash::{FxHashMap, FxHashSet};
 use salsa::plumbing::AsId;
 
 use crate::Db;
@@ -1844,6 +1844,307 @@ impl<'db> ConstraintAssignment<'db> {
     }
 }
 
+/// A collection of _sequents_ that describe how the constraints mentioned in a BDD relate to each
+/// other. These are used when evaluating checking satisfiability of a BDD. Both of those
+/// operations involve walking one or more paths from the root node to a terminal node. Each
+/// sequent describes paths that are invalid; these paths are pruned from the search.
+///
+/// We support several kinds of sequent:
+///
+/// - `C₁ ∧ C₂ → false`: This indicates that `C₁` and `C₂` are disjoint: it is not possible for
+///   both to hold. Any path that assumes both is impossible and can be pruned.
+///
+/// - `C₁ ∧ C₂ → D`: This indicates that the intersection of `C₁` and `C₂` can be simplified to
+///   `D`. Any path that assumes both `C₁` and `C₂` hold, but assumes `D` does _not_, is impossible
+///   and can be pruned.
+///
+/// - `C → D`: This indicates that `C` on its own is enough to imply `D`. Any path that assumes `C`
+///   holds but `D` does _not_ is impossible and can be pruned.
+///
+/// XXX: Note that `C`, `C₁`, `C₂`, and `D` are all [`ConstraintAssignment`]s, which means that they can
+/// check whether a [`ConstrainedTypeVar`] is true or false. #[derive(Clone, Debug, Default)]
+#[derive(Debug, Default)]
+struct SequentMap<'db> {
+    /// Sequents of the form `C₁ ∧ C₂ → false`
+    impossibilities: FxHashSet<(ConstrainedTypeVar<'db>, ConstrainedTypeVar<'db>)>,
+    /// Sequents of the form `C₁ ∧ C₂ → D`
+    pair_implications:
+        FxHashMap<(ConstrainedTypeVar<'db>, ConstrainedTypeVar<'db>), Vec<ConstrainedTypeVar<'db>>>,
+    /// Sequents of the form `C₁ ∧ C₂ → D`
+    single_implications: FxHashMap<ConstrainedTypeVar<'db>, Vec<ConstrainedTypeVar<'db>>>,
+    /// Constraints that we have already processed
+    processed: FxHashSet<ConstrainedTypeVar<'db>>,
+}
+
+impl<'db> SequentMap<'db> {
+    fn add(&mut self, db: &'db dyn Db, constraint: ConstrainedTypeVar<'db>) {
+        // If we've already seen this constraint, we can skip it.
+        if !self.processed.insert(constraint) {
+            return;
+        }
+
+        // Otherwise, check this constraint against all of the other ones we've seen so far, seeing
+        // if they're related to each other.
+        let processed = std::mem::take(&mut self.processed);
+        for other in &processed {
+            self.add_sequents_for_pair(db, constraint, *other);
+        }
+        self.processed = processed;
+
+        // And see if we can create any sequents from the constraint on its own.
+        self.add_sequents_for_single(db, constraint);
+    }
+
+    fn pair_key(
+        db: &'db dyn Db,
+        ante1: ConstrainedTypeVar<'db>,
+        ante2: ConstrainedTypeVar<'db>,
+    ) -> (ConstrainedTypeVar<'db>, ConstrainedTypeVar<'db>) {
+        if ante1.ordering(db) < ante2.ordering(db) {
+            (ante1, ante2)
+        } else {
+            (ante2, ante1)
+        }
+    }
+
+    fn add_impossibility(
+        &mut self,
+        db: &'db dyn Db,
+        ante1: ConstrainedTypeVar<'db>,
+        ante2: ConstrainedTypeVar<'db>,
+    ) {
+        self.impossibilities
+            .insert(Self::pair_key(db, ante1, ante2));
+    }
+
+    fn add_pair_implication(
+        &mut self,
+        db: &'db dyn Db,
+        ante1: ConstrainedTypeVar<'db>,
+        ante2: ConstrainedTypeVar<'db>,
+        post: ConstrainedTypeVar<'db>,
+    ) {
+        self.pair_implications
+            .entry(Self::pair_key(db, ante1, ante2))
+            .or_default()
+            .push(post);
+    }
+
+    fn add_single_implication(
+        &mut self,
+        ante: ConstrainedTypeVar<'db>,
+        post: ConstrainedTypeVar<'db>,
+    ) {
+        self.single_implications.entry(ante).or_default().push(post);
+    }
+
+    fn add_sequents_for_single(&mut self, db: &'db dyn Db, constraint: ConstrainedTypeVar<'db>) {
+        // If the lower or upper bound of this constraint is a typevar, we can propagate the
+        // constraint:
+        //
+        //   1. `(S ≤ T ≤ U) → (S ≤ U)`
+        //   2. `(S ≤ T ≤ τ) → (S ≤ τ)`
+        //   3. `(τ ≤ T ≤ U) → (τ ≤ U)`
+        //
+        // Technically, (1) also allows `(S = T) → (S = S)`, but the rhs of that is vacuously true,
+        // so we don't add a sequent for that case.
+
+        let lower = constraint.lower(db);
+        let upper = constraint.upper(db);
+        match (lower, upper) {
+            // Case 1
+            (Type::TypeVar(lower_typevar), Type::TypeVar(upper_typevar))
+                if !lower_typevar.is_same_typevar_as(db, upper_typevar) =>
+            {
+                let post_constraint =
+                    ConstrainedTypeVar::new(db, lower_typevar, Type::Never, upper);
+                self.add_single_implication(constraint, post_constraint);
+            }
+
+            // Case 2
+            (Type::TypeVar(lower_typevar), _) => {
+                let post_constraint =
+                    ConstrainedTypeVar::new(db, lower_typevar, Type::Never, upper);
+                self.add_single_implication(constraint, post_constraint);
+            }
+
+            // Case 3
+            (_, Type::TypeVar(upper_typevar)) => {
+                let post_constraint =
+                    ConstrainedTypeVar::new(db, upper_typevar, lower, Type::object());
+                self.add_single_implication(constraint, post_constraint);
+            }
+
+            _ => {}
+        }
+    }
+
+    fn add_sequents_for_pair(
+        &mut self,
+        db: &'db dyn Db,
+        left_constraint: ConstrainedTypeVar<'db>,
+        right_constraint: ConstrainedTypeVar<'db>,
+    ) {
+        // If either of the constraints has another typevar as a lower/upper bound, the only
+        // sequents we can add are for the transitive closure. For instance, if we have
+        // `(S ≤ T) ∧ (T ≤ int)`, then `(S ≤ int)` will also hold, and we should add a sequent for
+        // this implication. These are the `mutual_sequents` mentioned below — sequents that come
+        // about because two typevars are mutually constrained.
+        //
+        // Complicating things is that `(S ≤ T)` will be encoded differently depending on how `S`
+        // and `T` compare in our arbitrary BDD variable ordering.
+        //
+        // When `S` comes before `T`, `(S ≤ T)` will be encoded as `(Never ≤ S ≤ T)`, and the
+        // overall antecedent will be `(Never ≤ S ≤ T) ∧ (T ≤ int)`. Those two individual
+        // constraints constrain different typevars (`S` and `T`, respectively), and are handled by
+        // `add_mutual_sequents_for_different_typevars`.
+        //
+        // When `T` comes before `S`, `(S ≤ T)` will be encoded as `(S ≤ T ≤ object)`, and the
+        // overall antecedent will be `(S ≤ T ≤ object) ∧ (T ≤ int)`. Those two individual
+        // constraints both constrain `T`, and are handled by
+        // `add_mutual_sequents_for_same_typevars`.
+        //
+        // If all of the lower and upper bounds are concrete (i.e., not typevars), then there
+        // several _other_ sequents that we can add, as handled by `add_concrete_sequents`.
+        let left_typevar = left_constraint.typevar(db);
+        let right_typevar = right_constraint.typevar(db);
+        if !left_typevar.is_same_typevar_as(db, right_typevar) {
+            self.add_mutual_sequents_for_different_typevars(db, left_constraint, right_constraint);
+        } else if left_constraint.lower(db).is_type_var()
+            || left_constraint.upper(db).is_type_var()
+            || right_constraint.lower(db).is_type_var()
+            || right_constraint.upper(db).is_type_var()
+        {
+            self.add_mutual_sequents_for_same_typevars(db, left_constraint, right_constraint);
+        } else {
+            self.add_concrete_sequents(db, left_constraint, right_constraint);
+        }
+    }
+
+    fn add_mutual_sequents_for_different_typevars(
+        &mut self,
+        db: &'db dyn Db,
+        left_constraint: ConstrainedTypeVar<'db>,
+        right_constraint: ConstrainedTypeVar<'db>,
+    ) {
+        // We've structured our constraints so that a typevar's upper/lower bound can only
+        // be another typevar if the bound is "later" in our arbitrary ordering. That means
+        // we only have to check this pair of constraints in one direction — though we do
+        // have to figure out which of the two typevars is constrained, and which one is
+        // the upper/lower bound.
+        let left_typevar = left_constraint.typevar(db);
+        let right_typevar = right_constraint.typevar(db);
+        let (bound_typevar, bound_constraint, constrained_typevar, constrained_constraint) =
+            if left_typevar.can_be_bound_for(db, right_typevar) {
+                (
+                    left_typevar,
+                    left_constraint,
+                    right_typevar,
+                    right_constraint,
+                )
+            } else {
+                (
+                    right_typevar,
+                    right_constraint,
+                    left_typevar,
+                    left_constraint,
+                )
+            };
+
+        // We then look for cases where the "constrained" typevar's upper and/or lower bound
+        // matches the "bound" typevar. If so, we're going to add an implication sequent that
+        // replaces the upper/lower bound that matched with the bound constraint's corresponding
+        // bound.
+        let (new_lower, new_upper) = match (
+            constrained_constraint.lower(db),
+            constrained_constraint.upper(db),
+        ) {
+            // (B ≤ C ≤ B) ∧ (BL ≤ B ≤ BU) → (BL ≤ C ≤ BU)
+            (Type::TypeVar(constrained_lower), Type::TypeVar(constrained_upper))
+                if constrained_lower.is_same_typevar_as(db, bound_typevar)
+                    && constrained_upper.is_same_typevar_as(db, bound_typevar) =>
+            {
+                (bound_constraint.lower(db), bound_constraint.upper(db))
+            }
+
+            // (CL ≤ C ≤ B) ∧ (BL ≤ B ≤ BU) → (CL ≤ C ≤ BU)
+            (constrained_lower, Type::TypeVar(constrained_upper))
+                if constrained_upper.is_same_typevar_as(db, bound_typevar) =>
+            {
+                (constrained_lower, bound_constraint.upper(db))
+            }
+
+            // (B ≤ C ≤ CU) ∧ (BL ≤ B ≤ BU) → (BL ≤ C ≤ CU)
+            (Type::TypeVar(constrained_lower), constrained_upper)
+                if constrained_lower.is_same_typevar_as(db, bound_typevar) =>
+            {
+                (bound_constraint.lower(db), constrained_upper)
+            }
+
+            _ => return,
+        };
+
+        let post_constraint =
+            ConstrainedTypeVar::new(db, constrained_typevar, new_lower, new_upper);
+        self.add_pair_implication(db, left_constraint, right_constraint, post_constraint);
+    }
+
+    fn add_mutual_sequents_for_same_typevars(
+        &mut self,
+        db: &'db dyn Db,
+        left_constraint: ConstrainedTypeVar<'db>,
+        right_constraint: ConstrainedTypeVar<'db>,
+    ) {
+        let mut try_one_direction =
+            |left_constraint: ConstrainedTypeVar<'db>,
+             right_constraint: ConstrainedTypeVar<'db>| {
+                let left_lower = left_constraint.lower(db);
+                let left_upper = left_constraint.upper(db);
+                let right_lower = right_constraint.lower(db);
+                let right_upper = right_constraint.upper(db);
+                let post_constraint = match (left_lower, left_upper) {
+                    (Type::TypeVar(bound_typevar), Type::TypeVar(other_bound_typevar))
+                        if bound_typevar.is_same_typevar_as(db, other_bound_typevar) =>
+                    {
+                        ConstrainedTypeVar::new(db, bound_typevar, right_lower, right_upper)
+                    }
+                    (Type::TypeVar(bound_typevar), _) => {
+                        ConstrainedTypeVar::new(db, bound_typevar, Type::Never, right_upper)
+                    }
+                    (_, Type::TypeVar(bound_typevar)) => {
+                        ConstrainedTypeVar::new(db, bound_typevar, right_lower, Type::object())
+                    }
+                    _ => return,
+                };
+                self.add_pair_implication(db, left_constraint, right_constraint, post_constraint);
+            };
+
+        try_one_direction(left_constraint, right_constraint);
+        try_one_direction(right_constraint, left_constraint);
+    }
+
+    fn add_concrete_sequents(
+        &mut self,
+        db: &'db dyn Db,
+        left_constraint: ConstrainedTypeVar<'db>,
+        right_constraint: ConstrainedTypeVar<'db>,
+    ) {
+        match left_constraint.intersect(db, right_constraint) {
+            Some(intersection_constraint) => {
+                self.add_pair_implication(
+                    db,
+                    left_constraint,
+                    right_constraint,
+                    intersection_constraint,
+                );
+            }
+            None => {
+                self.add_impossibility(db, left_constraint, right_constraint);
+            }
+        }
+    }
+}
+
 /// A single clause in the DNF representation of a BDD
 #[derive(Clone, Debug, Default, Eq, PartialEq)]
 struct SatisfiedClause<'db> {

From f9f04260a1ee076c4bc7d54c2b2e895a302df252 Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Fri, 14 Nov 2025 09:34:51 -0500
Subject: [PATCH 03/22] sequent paths

---
 .../src/types/constraints.rs                  | 87 +++++++++++++++++++
 1 file changed, 87 insertions(+)

diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs
index 99effabda1a17..aca4de35bfdda 100644
--- a/crates/ty_python_semantic/src/types/constraints.rs
+++ b/crates/ty_python_semantic/src/types/constraints.rs
@@ -2145,6 +2145,93 @@ impl<'db> SequentMap<'db> {
     }
 }
 
+#[derive(Debug)]
+struct SequentPath<'db> {
+    path: Vec<ConstraintAssignment<'db>>,
+}
+
+impl<'db> SequentPath<'db> {
+    fn with_assignment<R>(
+        &mut self,
+        db: &'db dyn Db,
+        map: &SequentMap<'db>,
+        assignment: ConstraintAssignment<'db>,
+        f: impl FnOnce(&mut Self) -> R,
+    ) -> Option<R> {
+        self.path.push(assignment);
+        let result = if self.path_should_be_pruned(db, map) {
+            None
+        } else {
+            Some(f(self))
+        };
+        self.path.pop();
+        result
+    }
+
+    fn path_contains_assignment(
+        &self,
+        db: &'db dyn Db,
+        assignment: ConstraintAssignment<'db>,
+    ) -> bool {
+        // The `path` is guaranteed to be in sorted order (by the `ConstrainedTypeVar` of each
+        // assignment), due to the inherent structure of the BDD that we're walking.
+        self.path
+            .binary_search_by(|path_element| {
+                path_element
+                    .constraint()
+                    .ordering(db)
+                    .cmp(&assignment.constraint().ordering(db))
+            })
+            .is_ok()
+    }
+
+    fn path_should_be_pruned(&self, db: &'db dyn Db, map: &SequentMap<'db>) -> bool {
+        // TODO: This is very naive at the moment, partly for expediency, and partly because we
+        // don't anticipate the sequent maps to be very large. That said, the `path` is guaranteed
+        // to be in sorted order, due to the inherent structure of the BDD that we're walking, so
+        // we should be able to build up state about which sequents have been partially matched,
+        // avoiding the need to do this brute force search each time.
+
+        for (ante1, ante2) in &map.impossibilities {
+            if self.path_contains_assignment(db, ante1.when_true())
+                && self.path_contains_assignment(db, ante2.when_true())
+            {
+                // The sequent map says (ante1 ∧ ante2) is an impossible combination, and the
+                // current path asserts that both are true.
+                return true;
+            }
+        }
+
+        for ((ante1, ante2), posts) in &map.pair_implications {
+            for post in posts {
+                if self.path_contains_assignment(db, ante1.when_true())
+                    && self.path_contains_assignment(db, ante2.when_true())
+                    && self.path_contains_assignment(db, post.when_false())
+                {
+                    // The sequent map says (ante1 ∧ ante2 → post) must hold, and the current path
+                    // asserts that ante1 and ante2 are true, and that post is false. That violates
+                    // the implication.
+                    return true;
+                }
+            }
+        }
+
+        for (ante, posts) in &map.single_implications {
+            for post in posts {
+                if self.path_contains_assignment(db, ante.when_true())
+                    && self.path_contains_assignment(db, post.when_false())
+                {
+                    // The sequent map says (ante1 → post) must hold, and the current path asserts
+                    // that ante is true and that post is false. That violates the implication.
+                    return true;
+                }
+            }
+        }
+
+        false
+    }
+}
+
 /// A single clause in the DNF representation of a BDD
 #[derive(Clone, Debug, Default, Eq, PartialEq)]
 struct SatisfiedClause<'db> {

From cd87da208f8ab5954f4578470aeba5fe771d74d5 Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Fri, 14 Nov 2025 10:19:54 -0500
Subject: [PATCH 04/22] use sequent map

---
 .../src/types/constraints.rs                  | 120 ++++++++++++++++--
 1 file changed, 109 insertions(+), 11 deletions(-)

diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs
index aca4de35bfdda..60c94305744f5 100644
--- a/crates/ty_python_semantic/src/types/constraints.rs
+++ b/crates/ty_python_semantic/src/types/constraints.rs
@@ -716,10 +716,34 @@ impl<'db> Node<'db> {
         match self {
             Node::AlwaysTrue => true,
             Node::AlwaysFalse => false,
-            Node::Interior(_) => {
-                let domain = self.domain(db);
-                let restricted = self.and(db, domain);
-                restricted == domain
+            Node::Interior(interior) => {
+                let map = interior.sequent_map(db);
+                let mut path = SequentPath::default();
+                self.is_always_satisfied_inner(db, map, &mut path)
+            }
+        }
+    }
+
+    fn is_always_satisfied_inner(
+        self,
+        db: &'db dyn Db,
+        map: &SequentMap<'db>,
+        path: &mut SequentPath<'db>,
+    ) -> bool {
+        match self {
+            Node::AlwaysTrue => true,
+            Node::AlwaysFalse => false,
+            Node::Interior(interior) => {
+                let constraint = interior.constraint(db);
+                path.assignment_satisfied(db, map, constraint.when_true(), |path| {
+                    interior
+                        .if_true(db)
+                        .is_always_satisfied_inner(db, map, path)
+                }) && path.assignment_satisfied(db, map, constraint.when_false(), |path| {
+                    interior
+                        .if_false(db)
+                        .is_always_satisfied_inner(db, map, path)
+                })
             }
         }
     }
@@ -1405,6 +1429,17 @@ impl<'db> InteriorNode<'db> {
         }
     }
 
+    /// Returns a sequent map for this BDD, which records the relationships between the constraints
+    /// that appear in the BDD.
+    #[salsa::tracked(returns(ref), heap_size=ruff_memory_usage::heap_size)]
+    fn sequent_map(self, db: &'db dyn Db) -> SequentMap<'db> {
+        let mut map = SequentMap::default();
+        Node::Interior(self).for_each_constraint(db, &mut |constraint| {
+            map.add(db, constraint);
+        });
+        map
+    }
+
     /// Returns a simplified version of a BDD, along with the BDD's domain.
     ///
     /// Both are calculated by looking at the relationships that exist between the constraints that
@@ -1863,7 +1898,7 @@ impl<'db> ConstraintAssignment<'db> {
 ///
 /// XXX: Note that `C`, `C₁`, `C₂`, and `D` are all [`ConstraintAssignment`]s, which means that they can
 /// check whether a [`ConstrainedTypeVar`] is true or false. #[derive(Clone, Debug, Default)]
-#[derive(Debug, Default)]
+#[derive(Debug, Default, Eq, PartialEq, get_size2::GetSize, salsa::Update)]
 struct SequentMap<'db> {
     /// Sequents of the form `C₁ ∧ C₂ → false`
     impossibilities: FxHashSet<(ConstrainedTypeVar<'db>, ConstrainedTypeVar<'db>)>,
@@ -2137,32 +2172,95 @@ impl<'db> SequentMap<'db> {
                     right_constraint,
                     intersection_constraint,
                 );
+                self.add_single_implication(intersection_constraint, left_constraint);
+                self.add_single_implication(intersection_constraint, right_constraint);
             }
             None => {
                 self.add_impossibility(db, left_constraint, right_constraint);
             }
         }
     }
+
+    fn display<'a>(&'a self, db: &'db dyn Db, prefix: &'a dyn Display) -> impl Display + 'a {
+        struct DisplaySequentMap<'a, 'db> {
+            map: &'a SequentMap<'db>,
+            prefix: &'a dyn Display,
+            db: &'db dyn Db,
+        }
+
+        impl Display for DisplaySequentMap<'_, '_> {
+            fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+                let mut first = true;
+                let mut maybe_write_prefix = |f: &mut std::fmt::Formatter<'_>| {
+                    if first {
+                        first = false;
+                        Ok(())
+                    } else {
+                        write!(f, "\n{}", self.prefix)
+                    }
+                };
+
+                for (ante1, ante2) in &self.map.impossibilities {
+                    maybe_write_prefix(f)?;
+                    write!(
+                        f,
+                        "{} ∧ {} → false",
+                        ante1.display(self.db),
+                        ante2.display(self.db),
+                    )?;
+                }
+
+                for ((ante1, ante2), posts) in &self.map.pair_implications {
+                    for post in posts {
+                        maybe_write_prefix(f)?;
+                        write!(
+                            f,
+                            "{} ∧ {} → {}",
+                            ante1.display(self.db),
+                            ante2.display(self.db),
+                            post.display(self.db),
+                        )?;
+                    }
+                }
+
+                for (ante, posts) in &self.map.single_implications {
+                    for post in posts {
+                        maybe_write_prefix(f)?;
+                        write!(f, "{} → {}", ante.display(self.db), post.display(self.db))?;
+                    }
+                }
+
+                Ok(())
+            }
+        }
+
+        DisplaySequentMap {
+            map: self,
+            prefix,
+            db,
+        }
+    }
 }
 
-#[derive(Debug)]
+#[derive(Debug, Default)]
 struct SequentPath<'db> {
     path: Vec<ConstraintAssignment<'db>>,
 }
 
 impl<'db> SequentPath<'db> {
-    fn with_assignment<R>(
+    fn assignment_satisfied(
         &mut self,
         db: &'db dyn Db,
         map: &SequentMap<'db>,
         assignment: ConstraintAssignment<'db>,
-        f: impl FnOnce(&mut Self) -> R,
-    ) -> Option<R> {
+        f: impl FnOnce(&mut Self) -> bool,
+    ) -> bool {
         self.path.push(assignment);
         let result = if self.path_should_be_pruned(db, map) {
-            None
+            // A pruned path is vacuously satisfied
+            true
         } else {
-            Some(f(self))
+            f(self)
         };
         self.path.pop();
         result

From fec701e92d9e881d60275905a5c2eca30b1a8b70 Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Fri, 14 Nov 2025 10:18:00 -0500
Subject: [PATCH 05/22] don't include unhelpful sequents

---
 crates/ty_python_semantic/src/types/constraints.rs | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs
index 60c94305744f5..131be7828feaa 100644
--- a/crates/ty_python_semantic/src/types/constraints.rs
+++ b/crates/ty_python_semantic/src/types/constraints.rs
@@ -1922,7 +1922,9 @@ impl<'db> SequentMap<'db> {
         // if they're related to each other.
         let processed = std::mem::take(&mut self.processed);
         for other in &processed {
-            self.add_sequents_for_pair(db, constraint, *other);
+            if constraint != *other {
+                self.add_sequents_for_pair(db, constraint, *other);
+            }
         }
         self.processed = processed;
 
@@ -1959,6 +1961,9 @@ impl<'db> SequentMap<'db> {
         ante2: ConstrainedTypeVar<'db>,
         post: ConstrainedTypeVar<'db>,
     ) {
+        if ante1 == post || ante2 == post {
+            return;
+        }
         self.pair_implications
             .entry(Self::pair_key(db, ante1, ante2))
             .or_default()
@@ -1970,6 +1975,9 @@ impl<'db> SequentMap<'db> {
         ante: ConstrainedTypeVar<'db>,
         post: ConstrainedTypeVar<'db>,
     ) {
+        if ante == post {
+            return;
+        }
         self.single_implications.entry(ante).or_default().push(post);
     }
 

From 206ef2527f951620f4f86ec807c0126879bcfff7 Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Fri, 14 Nov 2025 10:18:14 -0500
Subject: [PATCH 06/22] fix path containment check

---
 .../ty_python_semantic/src/types/constraints.rs | 17 +++++++++--------
 1 file changed, 9 insertions(+), 8 deletions(-)

diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs
index 131be7828feaa..3644ffac77909 100644
--- a/crates/ty_python_semantic/src/types/constraints.rs
+++ b/crates/ty_python_semantic/src/types/constraints.rs
@@ -2281,14 +2281,15 @@ impl<'db> SequentPath<'db> {
     ) -> bool {
         // The `path` is guaranteed to be in sorted order (by the `ConstrainedTypeVar` of each
         // assignment), due to the inherent structure of the BDD that we're walking.
-        self.path
-            .binary_search_by(|path_element| {
-                path_element
-                    .constraint()
-                    .ordering(db)
-                    .cmp(&assignment.constraint().ordering(db))
-            })
-            .is_ok()
+        let Ok(index) = self.path.binary_search_by(|path_element| {
+            path_element
+                .constraint()
+                .ordering(db)
+                .cmp(&assignment.constraint().ordering(db))
+        }) else {
+            return false;
+        };
+        self.path[index] == assignment
     }
 
     fn path_should_be_pruned(&self, db: &'db dyn Db, map: &SequentMap<'db>) -> bool {

From 68e1b9675baec9ddffc7112750bbc560dd43ceea Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Fri, 14 Nov 2025 10:31:46 -0500
Subject: [PATCH 07/22] back to customizable return type

---
 .../src/types/constraints.rs                  | 25 +++++++++++--------
 1 file changed, 14 insertions(+), 11 deletions(-)

diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs
index 3644ffac77909..10e9fccf1621c 100644
--- a/crates/ty_python_semantic/src/types/constraints.rs
+++ b/crates/ty_python_semantic/src/types/constraints.rs
@@ -735,15 +735,19 @@ impl<'db> Node<'db> {
             Node::AlwaysFalse => false,
             Node::Interior(interior) => {
                 let constraint = interior.constraint(db);
-                path.assignment_satisfied(db, map, constraint.when_true(), |path| {
+                path.with_assignment(db, map, constraint.when_true(), |path| {
                     interior
                         .if_true(db)
                         .is_always_satisfied_inner(db, map, path)
-                }) && path.assignment_satisfied(db, map, constraint.when_false(), |path| {
-                    interior
-                        .if_false(db)
-                        .is_always_satisfied_inner(db, map, path)
                 })
+                .unwrap_or(true)
+                    && path
+                        .with_assignment(db, map, constraint.when_false(), |path| {
+                            interior
+                                .if_false(db)
+                                .is_always_satisfied_inner(db, map, path)
+                        })
+                        .unwrap_or(true)
             }
         }
     }
@@ -2256,19 +2260,18 @@ struct SequentPath<'db> {
 }
 
 impl<'db> SequentPath<'db> {
-    fn assignment_satisfied(
+    fn with_assignment<R>(
         &mut self,
         db: &'db dyn Db,
         map: &SequentMap<'db>,
         assignment: ConstraintAssignment<'db>,
-        f: impl FnOnce(&mut Self) -> bool,
-    ) -> bool {
+        f: impl FnOnce(&mut Self) -> R,
+    ) -> Option<R> {
         self.path.push(assignment);
         let result = if self.path_should_be_pruned(db, map) {
-            // A pruned path is vacuously satisfied
-            true
+            None
         } else {
-            f(self)
+            Some(f(self))
         };
         self.path.pop();
         result

From ea0bffb5715e8b1fe55c820125adf2063f5fc413 Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Fri, 14 Nov 2025 10:52:02 -0500
Subject: [PATCH 08/22] never too

---
 .../src/types/constraints.rs                  | 44 ++++++++++++++++---
 1 file changed, 39 insertions(+), 5 deletions(-)

diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs
index 10e9fccf1621c..77b710fbc058d 100644
--- a/crates/ty_python_semantic/src/types/constraints.rs
+++ b/crates/ty_python_semantic/src/types/constraints.rs
@@ -206,8 +206,8 @@ impl<'db> ConstraintSet<'db> {
     }
 
     /// Returns whether this constraint set never holds
-    pub(crate) fn is_never_satisfied(self, _db: &'db dyn Db) -> bool {
-        self.node.is_never_satisfied()
+    pub(crate) fn is_never_satisfied(self, db: &'db dyn Db) -> bool {
+        self.node.is_never_satisfied(db)
     }
 
     /// Returns whether this constraint set always holds
@@ -753,8 +753,42 @@ impl<'db> Node<'db> {
     }
 
     /// Returns whether this BDD represent the constant function `false`.
-    fn is_never_satisfied(self) -> bool {
-        matches!(self, Node::AlwaysFalse)
+    fn is_never_satisfied(self, db: &'db dyn Db) -> bool {
+        match self {
+            Node::AlwaysTrue => false,
+            Node::AlwaysFalse => true,
+            Node::Interior(interior) => {
+                let map = interior.sequent_map(db);
+                let mut path = SequentPath::default();
+                self.is_never_satisfied_inner(db, map, &mut path)
+            }
+        }
+    }
+
+    fn is_never_satisfied_inner(
+        self,
+        db: &'db dyn Db,
+        map: &SequentMap<'db>,
+        path: &mut SequentPath<'db>,
+    ) -> bool {
+        match self {
+            Node::AlwaysTrue => false,
+            Node::AlwaysFalse => true,
+            Node::Interior(interior) => {
+                let constraint = interior.constraint(db);
+                path.with_assignment(db, map, constraint.when_true(), |path| {
+                    interior.if_true(db).is_never_satisfied_inner(db, map, path)
+                })
+                .unwrap_or(true)
+                    && path
+                        .with_assignment(db, map, constraint.when_false(), |path| {
+                            interior
+                                .if_false(db)
+                                .is_never_satisfied_inner(db, map, path)
+                        })
+                        .unwrap_or(true)
+            }
+        }
     }
 
     /// Returns the negation of this BDD.
@@ -891,7 +925,7 @@ impl<'db> Node<'db> {
                 .satisfies(db, self)
                 .and(db, specializations)
                 .simplify(db);
-            !when_satisfied.is_never_satisfied()
+            !when_satisfied.is_never_satisfied(db)
         };
 
         // Returns if all specializations satisfy this constraint set.

From 4b7f75adaeeedabdf6f71ff26cffbf6f3082e22d Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Fri, 14 Nov 2025 11:22:02 -0500
Subject: [PATCH 09/22] restructure this a bit

---
 .../src/types/constraints.rs                  | 52 ++++++++++++-------
 1 file changed, 34 insertions(+), 18 deletions(-)

diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs
index 77b710fbc058d..64bcf81c28b71 100644
--- a/crates/ty_python_semantic/src/types/constraints.rs
+++ b/crates/ty_python_semantic/src/types/constraints.rs
@@ -734,20 +734,28 @@ impl<'db> Node<'db> {
             Node::AlwaysTrue => true,
             Node::AlwaysFalse => false,
             Node::Interior(interior) => {
+                // with_assignment will return None if this node's constraint causes the if_true
+                // edge to become impossible. We want to ignore impossible paths, and so we treat
+                // them as passing the "always satisfied" check.
                 let constraint = interior.constraint(db);
-                path.with_assignment(db, map, constraint.when_true(), |path| {
+                let true_always_satisfied = path
+                    .with_assignment(db, map, constraint.when_true(), |path| {
+                        interior
+                            .if_true(db)
+                            .is_always_satisfied_inner(db, map, path)
+                    })
+                    .unwrap_or(true);
+                if !true_always_satisfied {
+                    return false;
+                }
+
+                // Ditto for the if_false branch
+                path.with_assignment(db, map, constraint.when_false(), |path| {
                     interior
-                        .if_true(db)
+                        .if_false(db)
                         .is_always_satisfied_inner(db, map, path)
                 })
                 .unwrap_or(true)
-                    && path
-                        .with_assignment(db, map, constraint.when_false(), |path| {
-                            interior
-                                .if_false(db)
-                                .is_always_satisfied_inner(db, map, path)
-                        })
-                        .unwrap_or(true)
             }
         }
     }
@@ -775,18 +783,26 @@ impl<'db> Node<'db> {
             Node::AlwaysTrue => false,
             Node::AlwaysFalse => true,
             Node::Interior(interior) => {
+                // with_assignment will return None if this node's constraint causes the if_true
+                // edge to become impossible. We want to ignore impossible paths, and so we treat
+                // them as passing the "never satisfied" check.
                 let constraint = interior.constraint(db);
-                path.with_assignment(db, map, constraint.when_true(), |path| {
-                    interior.if_true(db).is_never_satisfied_inner(db, map, path)
+                let true_never_satisfied = path
+                    .with_assignment(db, map, constraint.when_true(), |path| {
+                        interior.if_true(db).is_never_satisfied_inner(db, map, path)
+                    })
+                    .unwrap_or(true);
+                if !true_never_satisfied {
+                    return false;
+                }
+
+                // Ditto for the if_false branch
+                path.with_assignment(db, map, constraint.when_false(), |path| {
+                    interior
+                        .if_false(db)
+                        .is_never_satisfied_inner(db, map, path)
                 })
                 .unwrap_or(true)
-                    && path
-                        .with_assignment(db, map, constraint.when_false(), |path| {
-                            interior
-                                .if_false(db)
-                                .is_never_satisfied_inner(db, map, path)
-                        })
-                        .unwrap_or(true)
             }
         }
     }

From fafb19619aec7439bdec2c2c5a08045820780538 Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Fri, 14 Nov 2025 12:34:43 -0500
Subject: [PATCH 10/22] don't most simplifies

---
 crates/ty_python_semantic/src/types/constraints.rs | 12 +++---------
 1 file changed, 3 insertions(+), 9 deletions(-)

diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs
index 64bcf81c28b71..83eecdad26383 100644
--- a/crates/ty_python_semantic/src/types/constraints.rs
+++ b/crates/ty_python_semantic/src/types/constraints.rs
@@ -916,7 +916,7 @@ impl<'db> Node<'db> {
             _ => panic!("at least one type should be a typevar"),
         };
 
-        self.satisfies(db, constraint)
+        self.implies(db, constraint)
     }
 
     fn satisfied_by_all_typevars(
@@ -937,19 +937,13 @@ impl<'db> Node<'db> {
 
         // Returns if some specialization satisfies this constraint set.
         let some_specialization_satisfies = move |specializations: Node<'db>| {
-            let when_satisfied = specializations
-                .satisfies(db, self)
-                .and(db, specializations)
-                .simplify(db);
+            let when_satisfied = specializations.implies(db, self).and(db, specializations);
             !when_satisfied.is_never_satisfied(db)
         };
 
         // Returns if all specializations satisfy this constraint set.
         let all_specializations_satisfy = move |specializations: Node<'db>| {
-            let when_satisfied = specializations
-                .satisfies(db, self)
-                .and(db, specializations)
-                .simplify(db);
+            let when_satisfied = specializations.implies(db, self).and(db, specializations);
             when_satisfied
                 .iff(db, specializations)
                 .is_always_satisfied(db)

From 55e7ede2cf8dd2d353261d3850c575baef50abaa Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Fri, 14 Nov 2025 13:42:04 -0500
Subject: [PATCH 11/22] transitive closure

---
 .../src/types/constraints.rs                  | 104 +++++++++---------
 1 file changed, 51 insertions(+), 53 deletions(-)

diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs
index 83eecdad26383..b7da7b809a8c7 100644
--- a/crates/ty_python_semantic/src/types/constraints.rs
+++ b/crates/ty_python_semantic/src/types/constraints.rs
@@ -718,7 +718,7 @@ impl<'db> Node<'db> {
             Node::AlwaysFalse => false,
             Node::Interior(interior) => {
                 let map = interior.sequent_map(db);
-                let mut path = SequentPath::default();
+                let mut path = PathAssignments::default();
                 self.is_always_satisfied_inner(db, map, &mut path)
             }
         }
@@ -728,7 +728,7 @@ impl<'db> Node<'db> {
         self,
         db: &'db dyn Db,
         map: &SequentMap<'db>,
-        path: &mut SequentPath<'db>,
+        path: &mut PathAssignments<'db>,
     ) -> bool {
         match self {
             Node::AlwaysTrue => true,
@@ -739,7 +739,7 @@ impl<'db> Node<'db> {
                 // them as passing the "always satisfied" check.
                 let constraint = interior.constraint(db);
                 let true_always_satisfied = path
-                    .with_assignment(db, map, constraint.when_true(), |path| {
+                    .with_assignment(map, constraint.when_true(), |path| {
                         interior
                             .if_true(db)
                             .is_always_satisfied_inner(db, map, path)
@@ -750,7 +750,7 @@ impl<'db> Node<'db> {
                 }
 
                 // Ditto for the if_false branch
-                path.with_assignment(db, map, constraint.when_false(), |path| {
+                path.with_assignment(map, constraint.when_false(), |path| {
                     interior
                         .if_false(db)
                         .is_always_satisfied_inner(db, map, path)
@@ -767,7 +767,7 @@ impl<'db> Node<'db> {
             Node::AlwaysFalse => true,
             Node::Interior(interior) => {
                 let map = interior.sequent_map(db);
-                let mut path = SequentPath::default();
+                let mut path = PathAssignments::default();
                 self.is_never_satisfied_inner(db, map, &mut path)
             }
         }
@@ -777,7 +777,7 @@ impl<'db> Node<'db> {
         self,
         db: &'db dyn Db,
         map: &SequentMap<'db>,
-        path: &mut SequentPath<'db>,
+        path: &mut PathAssignments<'db>,
     ) -> bool {
         match self {
             Node::AlwaysTrue => false,
@@ -788,7 +788,7 @@ impl<'db> Node<'db> {
                 // them as passing the "never satisfied" check.
                 let constraint = interior.constraint(db);
                 let true_never_satisfied = path
-                    .with_assignment(db, map, constraint.when_true(), |path| {
+                    .with_assignment(map, constraint.when_true(), |path| {
                         interior.if_true(db).is_never_satisfied_inner(db, map, path)
                     })
                     .unwrap_or(true);
@@ -797,7 +797,7 @@ impl<'db> Node<'db> {
                 }
 
                 // Ditto for the if_false branch
-                path.with_assignment(db, map, constraint.when_false(), |path| {
+                path.with_assignment(map, constraint.when_false(), |path| {
                     interior
                         .if_false(db)
                         .is_never_satisfied_inner(db, map, path)
@@ -2299,93 +2299,91 @@ impl<'db> SequentMap<'db> {
 }
 
 #[derive(Debug, Default)]
-struct SequentPath<'db> {
-    path: Vec<ConstraintAssignment<'db>>,
+struct PathAssignments<'db> {
+    /// The assignments that we know are true at a certain point when traversing a BDD.
+    assignments: FxHashSet<ConstraintAssignment<'db>>,
 }
 
-impl<'db> SequentPath<'db> {
+impl<'db> PathAssignments<'db> {
     fn with_assignment<R>(
         &mut self,
-        db: &'db dyn Db,
         map: &SequentMap<'db>,
         assignment: ConstraintAssignment<'db>,
         f: impl FnOnce(&mut Self) -> R,
     ) -> Option<R> {
-        self.path.push(assignment);
-        let result = if self.path_should_be_pruned(db, map) {
+        let old_assignments = self.assignments.clone();
+        let result = if self.add_assignment(map, assignment).is_err() {
             None
         } else {
             Some(f(self))
         };
-        self.path.pop();
+        self.assignments = old_assignments;
         result
     }
 
-    fn path_contains_assignment(
-        &self,
-        db: &'db dyn Db,
-        assignment: ConstraintAssignment<'db>,
-    ) -> bool {
-        // The `path` is guaranteed to be in sorted order (by the `ConstrainedTypeVar` of each
-        // assignment), due to the inherent structure of the BDD that we're walking.
-        let Ok(index) = self.path.binary_search_by(|path_element| {
-            path_element
-                .constraint()
-                .ordering(db)
-                .cmp(&assignment.constraint().ordering(db))
-        }) else {
-            return false;
-        };
-        self.path[index] == assignment
+    fn assignment_holds(&self, assignment: ConstraintAssignment<'db>) -> bool {
+        self.assignments.contains(&assignment)
     }
 
-    fn path_should_be_pruned(&self, db: &'db dyn Db, map: &SequentMap<'db>) -> bool {
+    fn add_assignment(
+        &mut self,
+        map: &SequentMap<'db>,
+        assignment: ConstraintAssignment<'db>,
+    ) -> Result<(), PathAssignmentConflict> {
+        // First add this assignment. If it causes a conflict, return that as an error. If we've
+        // already know this assignment holds, just return.
+        if self.assignments.contains(&assignment.negated()) {
+            return Err(PathAssignmentConflict);
+        }
+        if !self.assignments.insert(assignment) {
+            return Ok(());
+        }
+
+        // Then use our sequents to add additional facts that we know to be true.
         // TODO: This is very naive at the moment, partly for expediency, and partly because we
-        // don't anticipate the sequent maps to be very large. That said, the `path` is guaranteed
-        // to be in sorted order, due to the inherent structure of the BDD that we're walking, so
-        // we should be able to build up state about which sequents have been partially matched,
-        // avoiding the need to do this brute force search each time.
+        // don't anticipate the sequent maps to be very large. We might consider avoiding the
+        // brute-force search.
 
         for (ante1, ante2) in &map.impossibilities {
-            if self.path_contains_assignment(db, ante1.when_true())
-                && self.path_contains_assignment(db, ante2.when_true())
+            if self.assignment_holds(ante1.when_true()) && self.assignment_holds(ante2.when_true())
             {
                 // The sequent map says (ante1 ∧ ante2) is an impossible combination, and the
                 // current path asserts that both are true.
-                return true;
+                return Err(PathAssignmentConflict);
             }
         }
 
         for ((ante1, ante2), posts) in &map.pair_implications {
             for post in posts {
-                if self.path_contains_assignment(db, ante1.when_true())
-                    && self.path_contains_assignment(db, ante2.when_true())
-                    && self.path_contains_assignment(db, post.when_false())
+                if self.assignment_holds(ante1.when_true())
+                    && self.assignment_holds(ante2.when_true())
                 {
-                    // The sequent map says (ante1 ∧ ante2 → post) must hold, and the current path
-                    // asserts that ante1 and ante2 are true, and that post is false. That violates
-                    // the implication.
-                    return true;
+                    self.add_assignment(map, post.when_true())?;
                 }
             }
         }
 
         for (ante, posts) in &map.single_implications {
             for post in posts {
-                if self.path_contains_assignment(db, ante.when_true())
-                    && self.path_contains_assignment(db, post.when_false())
-                {
-                    // The sequent map says (ante1 → post) must hold, and the current path asserts
-                    // that ante is true and that post is false. That violates the implication.
-                    return true;
+                if self.assignment_holds(ante.when_true()) {
+                    self.add_assignment(map, post.when_true())?;
                 }
             }
         }
 
-        false
+        Ok(())
     }
 }
 
+#[derive(Debug)]
+struct PathAssignmentConflict;
+
+enum PathAssignmentOutcome {
+    Added,
+    Existing,
+    Conflict,
+}
+
 /// A single clause in the DNF representation of a BDD
 #[derive(Clone, Debug, Default, Eq, PartialEq)]
 struct SatisfiedClause<'db> {

From c3fbe0269f2821cf6aea4f0f5b79176bd0bf6e67 Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Fri, 14 Nov 2025 16:08:10 -0500
Subject: [PATCH 12/22] use sequents in exists

---
 .../src/types/constraints.rs                  | 112 +++++++++++++++---
 1 file changed, 95 insertions(+), 17 deletions(-)

diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs
index b7da7b809a8c7..6beb8c3854b4d 100644
--- a/crates/ty_python_semantic/src/types/constraints.rs
+++ b/crates/ty_python_semantic/src/types/constraints.rs
@@ -58,17 +58,18 @@
 
 use std::cmp::Ordering;
 use std::fmt::Display;
+use std::ops::Range;
 
 use itertools::Itertools;
 use rustc_hash::{FxHashMap, FxHashSet};
 use salsa::plumbing::AsId;
 
-use crate::Db;
 use crate::types::generics::InferableTypeVars;
 use crate::types::{
     BoundTypeVarIdentity, BoundTypeVarInstance, IntersectionType, Type, TypeRelation,
     TypeVarBoundOrConstraints, UnionType,
 };
+use crate::{Db, FxOrderSet};
 
 /// An extension trait for building constraint sets from [`Option`] values.
 pub(crate) trait OptionConstraintsExtension<T> {
@@ -739,7 +740,7 @@ impl<'db> Node<'db> {
                 // them as passing the "always satisfied" check.
                 let constraint = interior.constraint(db);
                 let true_always_satisfied = path
-                    .with_assignment(map, constraint.when_true(), |path| {
+                    .with_assignment(map, constraint.when_true(), |path, _| {
                         interior
                             .if_true(db)
                             .is_always_satisfied_inner(db, map, path)
@@ -750,7 +751,7 @@ impl<'db> Node<'db> {
                 }
 
                 // Ditto for the if_false branch
-                path.with_assignment(map, constraint.when_false(), |path| {
+                path.with_assignment(map, constraint.when_false(), |path, _| {
                     interior
                         .if_false(db)
                         .is_always_satisfied_inner(db, map, path)
@@ -788,7 +789,7 @@ impl<'db> Node<'db> {
                 // them as passing the "never satisfied" check.
                 let constraint = interior.constraint(db);
                 let true_never_satisfied = path
-                    .with_assignment(map, constraint.when_true(), |path| {
+                    .with_assignment(map, constraint.when_true(), |path, _| {
                         interior.if_true(db).is_never_satisfied_inner(db, map, path)
                     })
                     .unwrap_or(true);
@@ -797,7 +798,7 @@ impl<'db> Node<'db> {
                 }
 
                 // Ditto for the if_false branch
-                path.with_assignment(map, constraint.when_false(), |path| {
+                path.with_assignment(map, constraint.when_false(), |path, _| {
                     interior
                         .if_false(db)
                         .is_never_satisfied_inner(db, map, path)
@@ -995,7 +996,7 @@ impl<'db> Node<'db> {
     ) -> Self {
         bound_typevars
             .into_iter()
-            .fold(self.simplify(db), |abstracted, bound_typevar| {
+            .fold(self, |abstracted, bound_typevar| {
                 abstracted.exists_one(db, bound_typevar)
             })
     }
@@ -1008,6 +1009,20 @@ impl<'db> Node<'db> {
         }
     }
 
+    fn exists_one_inner(
+        self,
+        db: &'db dyn Db,
+        bound_typevar: BoundTypeVarIdentity<'db>,
+        map: &SequentMap<'db>,
+        path: &mut PathAssignments<'db>,
+    ) -> Self {
+        match self {
+            Node::AlwaysTrue => Node::AlwaysTrue,
+            Node::AlwaysFalse => Node::AlwaysFalse,
+            Node::Interior(interior) => interior.exists_one_inner(db, bound_typevar, map, path),
+        }
+    }
+
     /// Returns a new BDD that returns the same results as `self`, but with some inputs fixed to
     /// particular values. (Those variables will not be checked when evaluating the result, and
     /// will not be present in the result.)
@@ -1423,25 +1438,87 @@ impl<'db> InteriorNode<'db> {
 
     #[salsa::tracked(heap_size=ruff_memory_usage::heap_size)]
     fn exists_one(self, db: &'db dyn Db, bound_typevar: BoundTypeVarIdentity<'db>) -> Node<'db> {
+        let map = self.sequent_map(db);
+        let mut path = PathAssignments::default();
+        self.exists_one_inner(db, bound_typevar, map, &mut path)
+    }
+
+    fn exists_one_inner(
+        self,
+        db: &'db dyn Db,
+        bound_typevar: BoundTypeVarIdentity<'db>,
+        map: &SequentMap<'db>,
+        path: &mut PathAssignments<'db>,
+    ) -> Node<'db> {
         let self_constraint = self.constraint(db);
-        let self_typevar = self_constraint.typevar(db).identity(db);
-        match bound_typevar.cmp(&self_typevar) {
+        let self_typevar = self_constraint.typevar(db);
+        match bound_typevar.cmp(&self_typevar.identity(db)) {
             // If the typevar that this node checks is "later" than the typevar we're abstracting
             // over, then we have reached a point in the BDD where the abstraction can no longer
             // affect the result, and we can return early.
             Ordering::Less => Node::Interior(self),
+
             // If the typevar that this node checks _is_ the typevar we're abstracting over, then
             // we replace this node with the OR of its if_false/if_true edges. That is, the result
             // is true if there's any assignment of this node's constraint that is true.
+            //
+            // We also have to check if there are any derived facts that depend on the constraint
+            // we're about to remove. If so, we need to "remember" them by AND-ing them in with the
+            // corresponding branch.
             Ordering::Equal => {
-                let if_true = self.if_true(db).exists_one(db, bound_typevar);
-                let if_false = self.if_false(db).exists_one(db, bound_typevar);
+                let if_true = path
+                    .with_assignment(map, self_constraint.when_true(), |path, new_range| {
+                        let branch =
+                            self.if_true(db)
+                                .exists_one_inner(db, bound_typevar, map, path);
+                        path.assignments[new_range]
+                            .iter()
+                            .filter(|assignment| {
+                                !assignment
+                                    .constraint()
+                                    .typevar(db)
+                                    .is_same_typevar_as(db, self_typevar)
+                            })
+                            .fold(branch, |branch, assignment| {
+                                branch.and(db, Node::new_satisfied_constraint(db, *assignment))
+                            })
+                    })
+                    .unwrap_or(Node::AlwaysFalse);
+                let if_false = path
+                    .with_assignment(map, self_constraint.when_false(), |path, new_range| {
+                        let branch =
+                            self.if_false(db)
+                                .exists_one_inner(db, bound_typevar, map, path);
+                        path.assignments[new_range]
+                            .iter()
+                            .filter(|assignment| {
+                                !assignment
+                                    .constraint()
+                                    .typevar(db)
+                                    .is_same_typevar_as(db, self_typevar)
+                            })
+                            .fold(branch, |branch, assignment| {
+                                branch.and(db, Node::new_satisfied_constraint(db, *assignment))
+                            })
+                    })
+                    .unwrap_or(Node::AlwaysFalse);
                 if_true.or(db, if_false)
             }
+
             // Otherwise, we abstract the if_false/if_true edges recursively.
             Ordering::Greater => {
-                let if_true = self.if_true(db).exists_one(db, bound_typevar);
-                let if_false = self.if_false(db).exists_one(db, bound_typevar);
+                let if_true = path
+                    .with_assignment(map, self_constraint.when_true(), |path, _| {
+                        self.if_true(db)
+                            .exists_one_inner(db, bound_typevar, map, path)
+                    })
+                    .unwrap_or(Node::AlwaysFalse);
+                let if_false = path
+                    .with_assignment(map, self_constraint.when_false(), |path, _| {
+                        self.if_false(db)
+                            .exists_one_inner(db, bound_typevar, map, path)
+                    })
+                    .unwrap_or(Node::AlwaysFalse);
                 Node::new(db, self_constraint, if_true, if_false)
             }
         }
@@ -2301,7 +2378,7 @@ impl<'db> SequentMap<'db> {
 #[derive(Debug, Default)]
 struct PathAssignments<'db> {
     /// The assignments that we know are true at a certain point when traversing a BDD.
-    assignments: FxHashSet<ConstraintAssignment<'db>>,
+    assignments: FxOrderSet<ConstraintAssignment<'db>>,
 }
 
 impl<'db> PathAssignments<'db> {
@@ -2309,15 +2386,16 @@ impl<'db> PathAssignments<'db> {
         &mut self,
         map: &SequentMap<'db>,
         assignment: ConstraintAssignment<'db>,
-        f: impl FnOnce(&mut Self) -> R,
+        f: impl FnOnce(&mut Self, Range<usize>) -> R,
     ) -> Option<R> {
-        let old_assignments = self.assignments.clone();
+        let start = self.assignments.len();
         let result = if self.add_assignment(map, assignment).is_err() {
             None
         } else {
-            Some(f(self))
+            let end = self.assignments.len();
+            Some(f(self, start..end))
         };
-        self.assignments = old_assignments;
+        self.assignments.truncate(start);
         result
     }
 

From 5159068838ac7caffe1f12d8e6f37d8f456ab253 Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Fri, 14 Nov 2025 13:50:21 -0500
Subject: [PATCH 13/22] remove unused stuff

---
 .../src/types/constraints.rs                  | 20 +------------------
 1 file changed, 1 insertion(+), 19 deletions(-)

diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs
index 6beb8c3854b4d..4f040c7af4136 100644
--- a/crates/ty_python_semantic/src/types/constraints.rs
+++ b/crates/ty_python_semantic/src/types/constraints.rs
@@ -885,13 +885,6 @@ impl<'db> Node<'db> {
             .or(db, self.negate(db).and(db, else_node))
     }
 
-    fn satisfies(self, db: &'db dyn Db, other: Self) -> Self {
-        let simplified_self = self.simplify(db);
-        let implication = simplified_self.implies(db, other);
-        let (simplified, domain) = implication.simplify_and_domain(db);
-        simplified.and(db, domain)
-    }
-
     fn implies_subtype_of(self, db: &'db dyn Db, lhs: Type<'db>, rhs: Type<'db>) -> Self {
         // When checking subtyping involving a typevar, we can turn the subtyping check into a
         // constraint (i.e, "is `T` a subtype of `int` becomes the constraint `T ≤ int`), and then
@@ -1196,12 +1189,6 @@ impl<'db> Node<'db> {
         simplified
     }
 
-    /// Returns the domain (the set of allowed inputs) for a BDD.
-    fn domain(self, db: &'db dyn Db) -> Self {
-        let (_, domain) = self.simplify_and_domain(db);
-        domain
-    }
-
     /// Returns clauses describing all of the variable assignments that cause this BDD to evaluate
     /// to `true`. (This translates the boolean function that this BDD represents into DNF form.)
     fn satisfied_clauses(self, db: &'db dyn Db) -> SatisfiedClauses<'db> {
@@ -2314,6 +2301,7 @@ impl<'db> SequentMap<'db> {
         }
     }
 
+    #[expect(dead_code)] // Keep this around for debugging purposes
     fn display<'a>(&'a self, db: &'db dyn Db, prefix: &'a dyn Display) -> impl Display + 'a {
         struct DisplaySequentMap<'a, 'db> {
             map: &'a SequentMap<'db>,
@@ -2456,12 +2444,6 @@ impl<'db> PathAssignments<'db> {
 #[derive(Debug)]
 struct PathAssignmentConflict;
 
-enum PathAssignmentOutcome {
-    Added,
-    Existing,
-    Conflict,
-}
-
 /// A single clause in the DNF representation of a BDD
 #[derive(Clone, Debug, Default, Eq, PartialEq)]
 struct SatisfiedClause<'db> {

From e6499e233fbd813933f16ae97843d9efb85a401a Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Fri, 14 Nov 2025 16:20:51 -0500
Subject: [PATCH 14/22] clarify comment

---
 crates/ty_python_semantic/src/types/constraints.rs | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs
index 4f040c7af4136..3ca30dfeedd8d 100644
--- a/crates/ty_python_semantic/src/types/constraints.rs
+++ b/crates/ty_python_semantic/src/types/constraints.rs
@@ -735,9 +735,9 @@ impl<'db> Node<'db> {
             Node::AlwaysTrue => true,
             Node::AlwaysFalse => false,
             Node::Interior(interior) => {
-                // with_assignment will return None if this node's constraint causes the if_true
-                // edge to become impossible. We want to ignore impossible paths, and so we treat
-                // them as passing the "always satisfied" check.
+                // with_assignment will return None if this node's constraint (or anything we can
+                // derive from it) causes the if_true edge to become impossible. We want to ignore
+                // impossible paths, and so we treat them as passing the "always satisfied" check.
                 let constraint = interior.constraint(db);
                 let true_always_satisfied = path
                     .with_assignment(map, constraint.when_true(), |path, _| {
@@ -784,9 +784,9 @@ impl<'db> Node<'db> {
             Node::AlwaysTrue => false,
             Node::AlwaysFalse => true,
             Node::Interior(interior) => {
-                // with_assignment will return None if this node's constraint causes the if_true
-                // edge to become impossible. We want to ignore impossible paths, and so we treat
-                // them as passing the "never satisfied" check.
+                // with_assignment will return None if this node's constraint (or anything we can
+                // derive from it) causes the if_true edge to become impossible. We want to ignore
+                // impossible paths, and so we treat them as passing the "never satisfied" check.
                 let constraint = interior.constraint(db);
                 let true_never_satisfied = path
                     .with_assignment(map, constraint.when_true(), |path, _| {

From efcef459dc3fb930fb75e83c632079f1ca931ab5 Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Fri, 14 Nov 2025 16:36:56 -0500
Subject: [PATCH 15/22] :fire: domain

---
 .../src/types/constraints.rs                  | 44 ++++---------------
 1 file changed, 8 insertions(+), 36 deletions(-)

diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs
index 3ca30dfeedd8d..6183196eeb83b 100644
--- a/crates/ty_python_semantic/src/types/constraints.rs
+++ b/crates/ty_python_semantic/src/types/constraints.rs
@@ -1175,20 +1175,14 @@ impl<'db> Node<'db> {
         interior.if_false(db).for_each_constraint(db, f);
     }
 
-    /// Returns a simplified version of a BDD, along with the BDD's domain.
-    fn simplify_and_domain(self, db: &'db dyn Db) -> (Self, Self) {
+    /// Simplifies a BDD, replacing constraints with simpler or smaller constraints where possible.
+    fn simplify(self, db: &'db dyn Db) -> Self {
         match self {
-            Node::AlwaysTrue | Node::AlwaysFalse => (self, Node::AlwaysTrue),
+            Node::AlwaysTrue | Node::AlwaysFalse => self,
             Node::Interior(interior) => interior.simplify(db),
         }
     }
 
-    /// Simplifies a BDD, replacing constraints with simpler or smaller constraints where possible.
-    fn simplify(self, db: &'db dyn Db) -> Self {
-        let (simplified, _) = self.simplify_and_domain(db);
-        simplified
-    }
-
     /// Returns clauses describing all of the variable assignments that cause this BDD to evaluate
     /// to `true`. (This translates the boolean function that this BDD represents into DNF form.)
     fn satisfied_clauses(self, db: &'db dyn Db) -> SatisfiedClauses<'db> {
@@ -1552,14 +1546,13 @@ impl<'db> InteriorNode<'db> {
         map
     }
 
-    /// Returns a simplified version of a BDD, along with the BDD's domain.
+    /// Returns a simplified version of a BDD.
     ///
-    /// Both are calculated by looking at the relationships that exist between the constraints that
+    /// This is calculated by looking at the relationships that exist between the constraints that
     /// are mentioned in the BDD. For instance, if one constraint implies another (`x → y`), then
-    /// `x ∧ ¬y` is not a valid input, and is excluded from the BDD's domain. At the same time, we
-    /// can rewrite any occurrences of `x ∨ y` into `y`.
+    /// `x ∧ ¬y` is not a valid input, and we can rewrite any occurrences of `x ∨ y` into `y`.
     #[salsa::tracked(heap_size=ruff_memory_usage::heap_size)]
-    fn simplify(self, db: &'db dyn Db) -> (Node<'db>, Node<'db>) {
+    fn simplify(self, db: &'db dyn Db) -> Node<'db> {
         // To simplify a non-terminal BDD, we find all pairs of constraints that are mentioned in
         // the BDD. If any of those pairs can be simplified to some other BDD, we perform a
         // substitution to replace the pair with the simplification.
@@ -1586,7 +1579,6 @@ impl<'db> InteriorNode<'db> {
         // Repeatedly pop constraint pairs off of the visit queue, checking whether each pair can
         // be simplified.
         let mut simplified = Node::Interior(self);
-        let mut domain = Node::AlwaysTrue;
         while let Some((left_constraint, right_constraint)) = to_visit.pop() {
             // If the constraints refer to different typevars, the only simplifications we can make
             // are of the form `S ≤ T ∧ T ≤ int → S ≤ int`.
@@ -1659,9 +1651,6 @@ impl<'db> InteriorNode<'db> {
                 let positive_right_node =
                     Node::new_satisfied_constraint(db, right_constraint.when_true());
                 let lhs = positive_left_node.and(db, positive_right_node);
-                let implication = lhs.implies(db, new_node);
-                domain = domain.and(db, implication);
-
                 let intersection = new_node.ite(db, lhs, Node::AlwaysFalse);
                 simplified = simplified.and(db, intersection);
                 continue;
@@ -1695,13 +1684,6 @@ impl<'db> InteriorNode<'db> {
                 let negative_larger_node =
                     Node::new_satisfied_constraint(db, larger_constraint.when_false());
 
-                let positive_smaller_node =
-                    Node::new_satisfied_constraint(db, smaller_constraint.when_true());
-
-                // smaller → larger
-                let implication = positive_smaller_node.implies(db, positive_larger_node);
-                domain = domain.and(db, implication);
-
                 // larger ∨ smaller = larger
                 simplified = simplified.substitute_union(
                     db,
@@ -1767,11 +1749,6 @@ impl<'db> InteriorNode<'db> {
                     let negative_right_node =
                         Node::new_satisfied_constraint(db, right_constraint.when_false());
 
-                    // (left ∧ right) → intersection
-                    let implication = (positive_left_node.and(db, positive_right_node))
-                        .implies(db, positive_intersection_node);
-                    domain = domain.and(db, implication);
-
                     // left ∧ right = intersection
                     simplified = simplified.substitute_intersection(
                         db,
@@ -1836,11 +1813,6 @@ impl<'db> InteriorNode<'db> {
                     let positive_right_node =
                         Node::new_satisfied_constraint(db, right_constraint.when_true());
 
-                    // (left ∧ right) → false
-                    let implication = (positive_left_node.and(db, positive_right_node))
-                        .implies(db, Node::AlwaysFalse);
-                    domain = domain.and(db, implication);
-
                     // left ∧ right = false
                     simplified = simplified.substitute_intersection(
                         db,
@@ -1878,7 +1850,7 @@ impl<'db> InteriorNode<'db> {
             }
         }
 
-        (simplified, domain)
+        simplified
     }
 }
 

From 8bb819a8745eab0b415463c24f754883b17aeecd Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Fri, 14 Nov 2025 16:56:19 -0500
Subject: [PATCH 16/22] add historical note

---
 .../src/types/constraints.rs                  | 22 ++++++++++++++++++-
 1 file changed, 21 insertions(+), 1 deletion(-)

diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs
index 6183196eeb83b..07df513540d09 100644
--- a/crates/ty_python_semantic/src/types/constraints.rs
+++ b/crates/ty_python_semantic/src/types/constraints.rs
@@ -1176,7 +1176,27 @@ impl<'db> Node<'db> {
     }
 
     /// Simplifies a BDD, replacing constraints with simpler or smaller constraints where possible.
-    fn simplify(self, db: &'db dyn Db) -> Self {
+    ///
+    /// TODO: [Historical note] This is now used only for display purposes, but previously was also
+    /// used to ensure that we added the "transitive closure" to each BDD. The constraints in a BDD
+    /// are not independent; some combinations of constraints can imply other constraints. This
+    /// affects us in two ways: First, it means that certain combinations are impossible. (If
+    /// `a → b` then `a ∧ ¬b` can never happen.) Second, it means that certain constraints can be
+    /// inferred even if they do not explicitly appear in the BDD. It is important to take this
+    /// into account in several BDD operations (satisfiability, existential quantification, etc).
+    /// Before, we used this method to _add_ the transitive closure to a BDD, in an attempt to make
+    /// sure that it holds "all the facts" that would be needed to satisfy any query we might make.
+    /// We also used this method to calculate the "domain" of the BDD to help rule out invalid
+    /// inputs. However, this was at odds with using this method for display purposes, where our
+    /// goal is to _remove_ redundant information, so as to not clutter up the display. To resolve
+    /// this dilemma, all of the correctness uses have been refactored to use [`SequentMap`]
+    /// instead. It tracks the same information in a more efficient and lazy way, and never tries
+    /// to remove redundant information. For expediency, however, we did not make any changes to
+    /// this method, other than to stop tracking the domain (which was never used for display
+    /// purposes). That means we have some tech debt here, since there is a lot of duplicate logic
+    /// between `simplify_for_display` and `SequentMap`. It would be nice to update our display
+    /// logic to use the sequenet map as much as possible. But that can happen later.
+    fn simplify_for_display(self, db: &'db dyn Db) -> Self {
         match self {
             Node::AlwaysTrue | Node::AlwaysFalse => self,
             Node::Interior(interior) => interior.simplify(db),

From f853aad5e97d05755815dd99fd96dd9702ccf034 Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Fri, 14 Nov 2025 16:56:28 -0500
Subject: [PATCH 17/22] this is no longer true

---
 crates/ty_python_semantic/src/types/constraints.rs | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs
index 07df513540d09..d3ff9be0589a0 100644
--- a/crates/ty_python_semantic/src/types/constraints.rs
+++ b/crates/ty_python_semantic/src/types/constraints.rs
@@ -1999,9 +1999,6 @@ impl<'db> ConstraintAssignment<'db> {
 ///
 /// - `C → D`: This indicates that `C` on its own is enough to imply `D`. Any path that assumes `C`
 ///   holds but `D` does _not_ is impossible and can be pruned.
-///
-/// XXX: Note that `C`, `C₁`, `C₂`, and `D` are all [`ConstraintAssignment`]s, which means that they can
-/// check whether a [`ConstrainedTypeVar`] is true or false. #[derive(Clone, Debug, Default)]
 #[derive(Debug, Default, Eq, PartialEq, get_size2::GetSize, salsa::Update)]
 struct SequentMap<'db> {
     /// Sequents of the form `C₁ ∧ C₂ → false`

From eb451dc7eb957161920a0726e18063bfab5566c0 Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Fri, 14 Nov 2025 17:17:30 -0500
Subject: [PATCH 18/22] document sequent map more

---
 .../src/types/constraints.rs                  | 77 +++++++++++++++----
 1 file changed, 60 insertions(+), 17 deletions(-)

diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs
index d3ff9be0589a0..01cbfa56cb57f 100644
--- a/crates/ty_python_semantic/src/types/constraints.rs
+++ b/crates/ty_python_semantic/src/types/constraints.rs
@@ -735,12 +735,12 @@ impl<'db> Node<'db> {
             Node::AlwaysTrue => true,
             Node::AlwaysFalse => false,
             Node::Interior(interior) => {
-                // with_assignment will return None if this node's constraint (or anything we can
-                // derive from it) causes the if_true edge to become impossible. We want to ignore
+                // walk_edge will return None if this node's constraint (or anything we can derive
+                // from it) causes the if_true edge to become impossible. We want to ignore
                 // impossible paths, and so we treat them as passing the "always satisfied" check.
                 let constraint = interior.constraint(db);
                 let true_always_satisfied = path
-                    .with_assignment(map, constraint.when_true(), |path, _| {
+                    .walk_edge(map, constraint.when_true(), |path, _| {
                         interior
                             .if_true(db)
                             .is_always_satisfied_inner(db, map, path)
@@ -751,7 +751,7 @@ impl<'db> Node<'db> {
                 }
 
                 // Ditto for the if_false branch
-                path.with_assignment(map, constraint.when_false(), |path, _| {
+                path.walk_edge(map, constraint.when_false(), |path, _| {
                     interior
                         .if_false(db)
                         .is_always_satisfied_inner(db, map, path)
@@ -784,12 +784,12 @@ impl<'db> Node<'db> {
             Node::AlwaysTrue => false,
             Node::AlwaysFalse => true,
             Node::Interior(interior) => {
-                // with_assignment will return None if this node's constraint (or anything we can
-                // derive from it) causes the if_true edge to become impossible. We want to ignore
+                // walk_edge will return None if this node's constraint (or anything we can derive
+                // from it) causes the if_true edge to become impossible. We want to ignore
                 // impossible paths, and so we treat them as passing the "never satisfied" check.
                 let constraint = interior.constraint(db);
                 let true_never_satisfied = path
-                    .with_assignment(map, constraint.when_true(), |path, _| {
+                    .walk_edge(map, constraint.when_true(), |path, _| {
                         interior.if_true(db).is_never_satisfied_inner(db, map, path)
                     })
                     .unwrap_or(true);
@@ -798,7 +798,7 @@ impl<'db> Node<'db> {
                 }
 
                 // Ditto for the if_false branch
-                path.with_assignment(map, constraint.when_false(), |path, _| {
+                path.walk_edge(map, constraint.when_false(), |path, _| {
                     interior
                         .if_false(db)
                         .is_never_satisfied_inner(db, map, path)
@@ -1468,7 +1468,7 @@ impl<'db> InteriorNode<'db> {
             // corresponding branch.
             Ordering::Equal => {
                 let if_true = path
-                    .with_assignment(map, self_constraint.when_true(), |path, new_range| {
+                    .walk_edge(map, self_constraint.when_true(), |path, new_range| {
                         let branch =
                             self.if_true(db)
                                 .exists_one_inner(db, bound_typevar, map, path);
@@ -1486,7 +1486,7 @@ impl<'db> InteriorNode<'db> {
                     })
                     .unwrap_or(Node::AlwaysFalse);
                 let if_false = path
-                    .with_assignment(map, self_constraint.when_false(), |path, new_range| {
+                    .walk_edge(map, self_constraint.when_false(), |path, new_range| {
                         let branch =
                             self.if_false(db)
                                 .exists_one_inner(db, bound_typevar, map, path);
@@ -1509,13 +1509,13 @@ impl<'db> InteriorNode<'db> {
             // Otherwise, we abstract the if_false/if_true edges recursively.
             Ordering::Greater => {
                 let if_true = path
-                    .with_assignment(map, self_constraint.when_true(), |path, _| {
+                    .walk_edge(map, self_constraint.when_true(), |path, _| {
                         self.if_true(db)
                             .exists_one_inner(db, bound_typevar, map, path)
                     })
                     .unwrap_or(Node::AlwaysFalse);
                 let if_false = path
-                    .with_assignment(map, self_constraint.when_false(), |path, _| {
+                    .walk_edge(map, self_constraint.when_false(), |path, _| {
                         self.if_false(db)
                             .exists_one_inner(db, bound_typevar, map, path)
                     })
@@ -1984,9 +1984,11 @@ impl<'db> ConstraintAssignment<'db> {
 }
 
 /// A collection of _sequents_ that describe how the constraints mentioned in a BDD relate to each
-/// other. These are used when evaluating checking satisfiability of a BDD. Both of those
-/// operations involve walking one or more paths from the root node to a terminal node. Each
-/// sequent describes paths that are invalid; these paths are pruned from the search.
+/// other. These are used in several BDD operations that need to know about "derived facts" even if
+/// they are not mentioned in the BDD directly. These operations involve walking one or more paths
+/// from the root node to a terminal node. Each sequent describes paths that are invalid (which are
+/// pruned from the search), and new constraints that we can assume to be true even if we haven't
+/// seen them directly.
 ///
 /// We support several kinds of sequent:
 ///
@@ -2352,26 +2354,64 @@ impl<'db> SequentMap<'db> {
     }
 }
 
+/// The collection of constraints that we know to be true or false at a certain point when
+/// traversing a BDD.
 #[derive(Debug, Default)]
 struct PathAssignments<'db> {
-    /// The assignments that we know are true at a certain point when traversing a BDD.
     assignments: FxOrderSet<ConstraintAssignment<'db>>,
 }
 
 impl<'db> PathAssignments<'db> {
-    fn with_assignment<R>(
+    /// Walks one of the outgoing edges of an internal BDD node. `assignment` describes the
+    /// constraint that the BDD node checks, and whether we are following the `if_true` or
+    /// `if_false` edge.
+    ///
+    /// This new assignment might cause this path to become impossible — for instance, if we were
+    /// already assuming (from an earlier edge in the path) a constraint that is disjoint with this
+    /// one. We might also be able to infer _other_ assignments that do not appear in the BDD
+    /// directly, but which are implied from a combination of constraints that we _have_ seen.
+    ///
+    /// To handle all of this, you provide a callback. If the path has become impossible, we will
+    /// return `None` _without invoking the callback_. If the path does not contain any
+    /// contradictions, we will invoke the callback and return its result (wrapped in `Some`).
+    ///
+    /// Your callback will also be provided a slice of all of the constraints that we were able to
+    /// infer from `assignment` combined with the information we already knew. (For borrow-check
+    /// reasons, we provide this as a [`Range`]; use that range to index into `self.assignments` to
+    /// get the list of all of the assignments that we learned from this edge.)
+    ///
+    /// You will presumably end up making a recursive call of some kind to keep progressing through
+    /// the BDD. You should make this call from inside of your callback, so that as you get further
+    /// down into the BDD structure, we remember all of the information that we have learned from
+    /// the path we're on.
+    fn walk_edge<R>(
         &mut self,
         map: &SequentMap<'db>,
         assignment: ConstraintAssignment<'db>,
         f: impl FnOnce(&mut Self, Range<usize>) -> R,
     ) -> Option<R> {
+        // Record a snapshot of the assignments that we already knew held — both so that we can
+        // pass along the range of which assignments are new, and so that we can reset back to this
+        // point before returning.
         let start = self.assignments.len();
+
+        // Add the new assignment and anything we can derive from it.
         let result = if self.add_assignment(map, assignment).is_err() {
+            // If that results in the path now being impossible due to a contradiction, return
+            // without invoking the callback.
             None
         } else {
+            // Otherwise invoke the callback to keep traversing the BDD. The callback will likely
+            // traverse additional edges, which might add more to our `assignments` set. But even
+            // if that happens, `start..end` will mark the assignments that were added by the
+            // `add_assignment` call above — that is, the new assignment for this edge along with
+            // the derived information we inferred from it.
             let end = self.assignments.len();
             Some(f(self, start..end))
         };
+
+        // Reset back to where we were before following this edge, so that the caller can reuse a
+        // single instance for the entire BDD traversal.
         self.assignments.truncate(start);
         result
     }
@@ -2380,6 +2420,9 @@ impl<'db> PathAssignments<'db> {
         self.assignments.contains(&assignment)
     }
 
+    /// Adds a new assignment, along with any derived information that we can infer from the new
+    /// assignment combined with the assignments we've already seen. If any of this causes the path
+    /// to become invalid, due to a contradiction, returns a [`PathAssignmentConflict`] error.
     fn add_assignment(
         &mut self,
         map: &SequentMap<'db>,

From 137a057a72212c069c553e2d24370682f7dbb1b0 Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Fri, 14 Nov 2025 17:46:37 -0500
Subject: [PATCH 19/22] one more comment for the road

---
 crates/ty_python_semantic/src/types/constraints.rs | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs
index 01cbfa56cb57f..076dbbd8f0f7b 100644
--- a/crates/ty_python_semantic/src/types/constraints.rs
+++ b/crates/ty_python_semantic/src/types/constraints.rs
@@ -1475,6 +1475,8 @@ impl<'db> InteriorNode<'db> {
                         path.assignments[new_range]
                             .iter()
                             .filter(|assignment| {
+                                // Don't add back any derived facts if they reference the typevar
+                                // that we're trying to remove!
                                 !assignment
                                     .constraint()
                                     .typevar(db)
@@ -1493,6 +1495,8 @@ impl<'db> InteriorNode<'db> {
                         path.assignments[new_range]
                             .iter()
                             .filter(|assignment| {
+                                // Don't add back any derived facts if they reference the typevar
+                                // that we're trying to remove!
                                 !assignment
                                     .constraint()
                                     .typevar(db)

From 1b94bbdd451a00f502db05b86e89faa080a2d403 Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Fri, 14 Nov 2025 17:52:05 -0500
Subject: [PATCH 20/22] whopps

---
 crates/ty_python_semantic/src/types/constraints.rs | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs
index 076dbbd8f0f7b..fd1d43a0ce886 100644
--- a/crates/ty_python_semantic/src/types/constraints.rs
+++ b/crates/ty_python_semantic/src/types/constraints.rs
@@ -326,7 +326,7 @@ impl<'db> ConstraintSet<'db> {
     }
 
     pub(crate) fn display(self, db: &'db dyn Db) -> impl Display {
-        self.node.simplify(db).display(db)
+        self.node.simplify_for_display(db).display(db)
     }
 }
 
@@ -2346,6 +2346,9 @@ impl<'db> SequentMap<'db> {
                     }
                 }
 
+                if first {
+                    f.write_str("[no sequents]")?;
+                }
                 Ok(())
             }
         }

From b700a3124b12449d6b6973b0808970f45827c46e Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Mon, 17 Nov 2025 14:20:52 -0500
Subject: [PATCH 21/22] move if guard

---
 crates/ty_python_semantic/src/types/constraints.rs | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs
index fd1d43a0ce886..ad4d660d578a3 100644
--- a/crates/ty_python_semantic/src/types/constraints.rs
+++ b/crates/ty_python_semantic/src/types/constraints.rs
@@ -2103,12 +2103,12 @@ impl<'db> SequentMap<'db> {
         let upper = constraint.upper(db);
         match (lower, upper) {
             // Case 1
-            (Type::TypeVar(lower_typevar), Type::TypeVar(upper_typevar))
-                if !lower_typevar.is_same_typevar_as(db, upper_typevar) =>
-            {
-                let post_constraint =
-                    ConstrainedTypeVar::new(db, lower_typevar, Type::Never, upper);
-                self.add_single_implication(constraint, post_constraint);
+            (Type::TypeVar(lower_typevar), Type::TypeVar(upper_typevar)) => {
+                if !lower_typevar.is_same_typevar_as(db, upper_typevar) {
+                    let post_constraint =
+                        ConstrainedTypeVar::new(db, lower_typevar, Type::Never, upper);
+                    self.add_single_implication(constraint, post_constraint);
+                }
             }
 
             // Case 2

From a87c3d9ec86ef79e5c0a2d7e354cb4adfb7c2068 Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Mon, 17 Nov 2025 14:57:46 -0500
Subject: [PATCH 22/22] fix docs

---
 crates/ty_python_semantic/src/types/constraints.rs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs
index ad4d660d578a3..d76b965bd3610 100644
--- a/crates/ty_python_semantic/src/types/constraints.rs
+++ b/crates/ty_python_semantic/src/types/constraints.rs
@@ -1195,7 +1195,7 @@ impl<'db> Node<'db> {
     /// this method, other than to stop tracking the domain (which was never used for display
     /// purposes). That means we have some tech debt here, since there is a lot of duplicate logic
     /// between `simplify_for_display` and `SequentMap`. It would be nice to update our display
-    /// logic to use the sequenet map as much as possible. But that can happen later.
+    /// logic to use the sequent map as much as possible. But that can happen later.
     fn simplify_for_display(self, db: &'db dyn Db) -> Self {
         match self {
             Node::AlwaysTrue | Node::AlwaysFalse => self,
@@ -2012,7 +2012,7 @@ struct SequentMap<'db> {
     /// Sequents of the form `C₁ ∧ C₂ → D`
     pair_implications:
         FxHashMap<(ConstrainedTypeVar<'db>, ConstrainedTypeVar<'db>), Vec<ConstrainedTypeVar<'db>>>,
-    /// Sequents of the form `C₁ ∧ C₂ → D`
+    /// Sequents of the form `C → D`
     single_implications: FxHashMap<ConstrainedTypeVar<'db>, Vec<ConstrainedTypeVar<'db>>>,
     /// Constraints that we have already processed
     processed: FxHashSet<ConstrainedTypeVar<'db>>,