From 8e13765b573f00b3156368a569c8a0b5bcf92332 Mon Sep 17 00:00:00 2001 From: Zanie Blue Date: Mon, 15 Dec 2025 15:36:08 -0600 Subject: [PATCH 1/5] [ty] Use `title` for configuration code fences in ty reference documentation (#21992) Part of https://github.com/astral-sh/ty/pull/1904 --- crates/ruff_dev/src/generate_ty_options.rs | 9 +-- crates/ty/docs/configuration.md | 64 +++++++++++----------- 2 files changed, 37 insertions(+), 36 deletions(-) diff --git a/crates/ruff_dev/src/generate_ty_options.rs b/crates/ruff_dev/src/generate_ty_options.rs index 733af8b00a..6322f65981 100644 --- a/crates/ruff_dev/src/generate_ty_options.rs +++ b/crates/ruff_dev/src/generate_ty_options.rs @@ -166,8 +166,9 @@ fn emit_field(output: &mut String, name: &str, field: &OptionField, parents: &[S output.push('\n'); let _ = writeln!(output, "**Type**: `{}`", field.value_type); output.push('\n'); - output.push_str("**Example usage** (`pyproject.toml`):\n\n"); + output.push_str("**Example usage**:\n\n"); output.push_str(&format_example( + "pyproject.toml", &format_header( field.scope, field.example, @@ -179,11 +180,11 @@ fn emit_field(output: &mut String, name: &str, field: &OptionField, parents: &[S output.push('\n'); } -fn format_example(header: &str, content: &str) -> String { +fn format_example(title: &str, header: &str, content: &str) -> String { if header.is_empty() { - format!("```toml\n{content}\n```\n",) + format!("```toml title=\"{title}\"\n{content}\n```\n",) } else { - format!("```toml\n{header}\n{content}\n```\n",) + format!("```toml title=\"{title}\"\n{header}\n{content}\n```\n",) } } diff --git a/crates/ty/docs/configuration.md b/crates/ty/docs/configuration.md index edbea9c803..ff720a5d8e 100644 --- a/crates/ty/docs/configuration.md +++ b/crates/ty/docs/configuration.md @@ -18,9 +18,9 @@ Valid severities are: **Type**: `dict[RuleName, "ignore" | "warn" | "error"]` -**Example usage** (`pyproject.toml`): +**Example usage**: -```toml +```toml title="pyproject.toml" [tool.ty.rules] possibly-unresolved-reference = "warn" division-by-zero = "ignore" @@ -45,9 +45,9 @@ configuration setting. **Type**: `list[str]` -**Example usage** (`pyproject.toml`): +**Example usage**: -```toml +```toml title="pyproject.toml" [tool.ty.environment] extra-paths = ["./shared/my-search-path"] ``` @@ -76,9 +76,9 @@ This option can be used to point to virtual or system Python environments. **Type**: `str` -**Example usage** (`pyproject.toml`): +**Example usage**: -```toml +```toml title="pyproject.toml" [tool.ty.environment] python = "./custom-venv-location/.venv" ``` @@ -103,9 +103,9 @@ If no platform is specified, ty will use the current platform: **Type**: `"win32" | "darwin" | "android" | "ios" | "linux" | "all" | str` -**Example usage** (`pyproject.toml`): +**Example usage**: -```toml +```toml title="pyproject.toml" [tool.ty.environment] # Tailor type stubs and conditionalized type definitions to windows. python-platform = "win32" @@ -137,9 +137,9 @@ to reflect the differing contents of the standard library across Python versions **Type**: `"3.7" | "3.8" | "3.9" | "3.10" | "3.11" | "3.12" | "3.13" | "3.14" | .` -**Example usage** (`pyproject.toml`): +**Example usage**: -```toml +```toml title="pyproject.toml" [tool.ty.environment] python-version = "3.12" ``` @@ -165,9 +165,9 @@ it will also be included in the first party search path. **Type**: `list[str]` -**Example usage** (`pyproject.toml`): +**Example usage**: -```toml +```toml title="pyproject.toml" [tool.ty.environment] # Multiple directories (priority order) root = ["./src", "./lib", "./vendor"] @@ -185,9 +185,9 @@ bundled as a zip file in the binary **Type**: `str` -**Example usage** (`pyproject.toml`): +**Example usage**: -```toml +```toml title="pyproject.toml" [tool.ty.environment] typeshed = "/path/to/custom/typeshed" ``` @@ -240,9 +240,9 @@ If not specified, defaults to `[]` (excludes no files). **Type**: `list[str]` -**Example usage** (`pyproject.toml`): +**Example usage**: -```toml +```toml title="pyproject.toml" [[tool.ty.overrides]] exclude = [ "generated", @@ -268,9 +268,9 @@ If not specified, defaults to `["**"]` (matches all files). **Type**: `list[str]` -**Example usage** (`pyproject.toml`): +**Example usage**: -```toml +```toml title="pyproject.toml" [[tool.ty.overrides]] include = [ "src", @@ -292,9 +292,9 @@ severity levels or disable them entirely. **Type**: `dict[RuleName, "ignore" | "warn" | "error"]` -**Example usage** (`pyproject.toml`): +**Example usage**: -```toml +```toml title="pyproject.toml" [[tool.ty.overrides]] include = ["src"] @@ -358,9 +358,9 @@ to re-include `dist` use `exclude = ["!dist"]` **Type**: `list[str]` -**Example usage** (`pyproject.toml`): +**Example usage**: -```toml +```toml title="pyproject.toml" [tool.ty.src] exclude = [ "generated", @@ -399,9 +399,9 @@ matches `/src` and not `/test/src`). **Type**: `list[str]` -**Example usage** (`pyproject.toml`): +**Example usage**: -```toml +```toml title="pyproject.toml" [tool.ty.src] include = [ "src", @@ -421,9 +421,9 @@ Enabled by default. **Type**: `bool` -**Example usage** (`pyproject.toml`): +**Example usage**: -```toml +```toml title="pyproject.toml" [tool.ty.src] respect-ignore-files = false ``` @@ -450,9 +450,9 @@ it will also be included in the first party search path. **Type**: `str` -**Example usage** (`pyproject.toml`): +**Example usage**: -```toml +```toml title="pyproject.toml" [tool.ty.src] root = "./app" ``` @@ -471,9 +471,9 @@ Defaults to `false`. **Type**: `bool` -**Example usage** (`pyproject.toml`): +**Example usage**: -```toml +```toml title="pyproject.toml" [tool.ty.terminal] # Error if ty emits any warning-level diagnostics. error-on-warning = true @@ -491,9 +491,9 @@ Defaults to `full`. **Type**: `full | concise` -**Example usage** (`pyproject.toml`): +**Example usage**: -```toml +```toml title="pyproject.toml" [tool.ty.terminal] output-format = "concise" ``` From 298e2dcb4ef976cf1e71794bcd6df6cd7f8f7b71 Mon Sep 17 00:00:00 2001 From: Douglas Creager Date: Sun, 14 Dec 2025 20:19:08 -0500 Subject: [PATCH 2/5] track source_order in PathAssignments --- .../src/types/constraints.rs | 170 ++++++++++-------- 1 file changed, 100 insertions(+), 70 deletions(-) diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs index 82d6c3b0ad..df8a2af480 100644 --- a/crates/ty_python_semantic/src/types/constraints.rs +++ b/crates/ty_python_semantic/src/types/constraints.rs @@ -81,7 +81,7 @@ use crate::types::{ BoundTypeVarIdentity, BoundTypeVarInstance, IntersectionType, Type, TypeVarBoundOrConstraints, UnionType, walk_bound_type_var_type, }; -use crate::{Db, FxOrderSet}; +use crate::{Db, FxOrderMap}; /// An extension trait for building constraint sets from [`Option`] values. pub(crate) trait OptionConstraintsExtension { @@ -1000,8 +1000,9 @@ impl<'db> Node<'db> { // 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 source_order = interior.source_order(db); let true_always_satisfied = path - .walk_edge(db, map, constraint.when_true(), |path, _| { + .walk_edge(db, map, constraint.when_true(), source_order, |path, _| { interior .if_true(db) .is_always_satisfied_inner(db, map, path) @@ -1012,7 +1013,7 @@ impl<'db> Node<'db> { } // Ditto for the if_false branch - path.walk_edge(db, map, constraint.when_false(), |path, _| { + path.walk_edge(db, map, constraint.when_false(), source_order, |path, _| { interior .if_false(db) .is_always_satisfied_inner(db, map, path) @@ -1049,8 +1050,9 @@ impl<'db> Node<'db> { // 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 source_order = interior.source_order(db); let true_never_satisfied = path - .walk_edge(db, map, constraint.when_true(), |path, _| { + .walk_edge(db, map, constraint.when_true(), source_order, |path, _| { interior.if_true(db).is_never_satisfied_inner(db, map, path) }) .unwrap_or(true); @@ -1059,7 +1061,7 @@ impl<'db> Node<'db> { } // Ditto for the if_false branch - path.walk_edge(db, map, constraint.when_false(), |path, _| { + path.walk_edge(db, map, constraint.when_false(), source_order, |path, _| { interior .if_false(db) .is_never_satisfied_inner(db, map, path) @@ -2005,6 +2007,7 @@ impl<'db> InteriorNode<'db> { path: &mut PathAssignments<'db>, ) -> Node<'db> { let self_constraint = self.constraint(db); + let self_source_order = self.source_order(db); if should_remove(self_constraint) { // If we should remove constraints involving this typevar, then we replace this node // with the OR of its if_false/if_true edges. That is, the result is true if there's @@ -2012,67 +2015,85 @@ impl<'db> InteriorNode<'db> { // // 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. We currently reuse the `source_order` of the constraint being - // removed when we add these derived facts. - // - // TODO: This might not be stable enough, if we add more than one derived fact for this - // constraint. If we still see inconsistent test output, we might need a more complex - // way of tracking source order for derived facts. - let self_source_order = self.source_order(db); + // corresponding branch. let if_true = path - .walk_edge(db, map, self_constraint.when_true(), |path, new_range| { - let branch = self - .if_true(db) - .abstract_one_inner(db, should_remove, map, path); - path.assignments[new_range] - .iter() - .filter(|assignment| { - // Don't add back any derived facts if they are ones that we would have - // removed! - !should_remove(assignment.constraint()) - }) - .fold(branch, |branch, assignment| { - branch.and( - db, - Node::new_satisfied_constraint(db, *assignment, self_source_order), - ) - }) - }) + .walk_edge( + db, + map, + self_constraint.when_true(), + self_source_order, + |path, new_range| { + let branch = + self.if_true(db) + .abstract_one_inner(db, should_remove, map, path); + path.assignments[new_range] + .iter() + .filter(|(assignment, _)| { + // Don't add back any derived facts if they are ones that we would have + // removed! + !should_remove(assignment.constraint()) + }) + .fold(branch, |branch, (assignment, source_order)| { + branch.and( + db, + Node::new_satisfied_constraint(db, *assignment, *source_order), + ) + }) + }, + ) .unwrap_or(Node::AlwaysFalse); let if_false = path - .walk_edge(db, map, self_constraint.when_false(), |path, new_range| { - let branch = self - .if_false(db) - .abstract_one_inner(db, should_remove, map, path); - path.assignments[new_range] - .iter() - .filter(|assignment| { - // Don't add back any derived facts if they are ones that we would have - // removed! - !should_remove(assignment.constraint()) - }) - .fold(branch, |branch, assignment| { - branch.and( - db, - Node::new_satisfied_constraint(db, *assignment, self_source_order), - ) - }) - }) + .walk_edge( + db, + map, + self_constraint.when_false(), + self_source_order, + |path, new_range| { + let branch = + self.if_false(db) + .abstract_one_inner(db, should_remove, map, path); + path.assignments[new_range] + .iter() + .filter(|(assignment, _)| { + // Don't add back any derived facts if they are ones that we would have + // removed! + !should_remove(assignment.constraint()) + }) + .fold(branch, |branch, (assignment, source_order)| { + branch.and( + db, + Node::new_satisfied_constraint(db, *assignment, *source_order), + ) + }) + }, + ) .unwrap_or(Node::AlwaysFalse); if_true.or(db, if_false) } else { // Otherwise, we abstract the if_false/if_true edges recursively. let if_true = path - .walk_edge(db, map, self_constraint.when_true(), |path, _| { - self.if_true(db) - .abstract_one_inner(db, should_remove, map, path) - }) + .walk_edge( + db, + map, + self_constraint.when_true(), + self_source_order, + |path, _| { + self.if_true(db) + .abstract_one_inner(db, should_remove, map, path) + }, + ) .unwrap_or(Node::AlwaysFalse); let if_false = path - .walk_edge(db, map, self_constraint.when_false(), |path, _| { - self.if_false(db) - .abstract_one_inner(db, should_remove, map, path) - }) + .walk_edge( + db, + map, + self_constraint.when_false(), + self_source_order, + |path, _| { + self.if_false(db) + .abstract_one_inner(db, should_remove, map, path) + }, + ) .unwrap_or(Node::AlwaysFalse); // NB: We cannot use `Node::new` here, because the recursive calls might introduce new // derived constraints into the result, and those constraints might appear before this @@ -3169,8 +3190,8 @@ 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> { - assignments: FxOrderSet>, +pub(crate) struct PathAssignments<'db> { + assignments: FxOrderMap, usize>, } impl<'db> PathAssignments<'db> { @@ -3201,6 +3222,7 @@ impl<'db> PathAssignments<'db> { db: &'db dyn Db, map: &SequentMap<'db>, assignment: ConstraintAssignment<'db>, + source_order: usize, f: impl FnOnce(&mut Self, Range) -> R, ) -> Option { // Record a snapshot of the assignments that we already knew held — both so that we can @@ -3213,12 +3235,12 @@ impl<'db> PathAssignments<'db> { target: "ty_python_semantic::types::constraints::PathAssignment", before = %format_args!( "[{}]", - self.assignments[..start].iter().map(|assignment| assignment.display(db)).format(", "), + self.assignments[..start].iter().map(|(assignment, _)| assignment.display(db)).format(", "), ), edge = %assignment.display(db), "walk edge", ); - let found_conflict = self.add_assignment(db, map, assignment); + let found_conflict = self.add_assignment(db, map, assignment, source_order); let result = if found_conflict.is_err() { // If that results in the path now being impossible due to a contradiction, return // without invoking the callback. @@ -3233,7 +3255,7 @@ impl<'db> PathAssignments<'db> { target: "ty_python_semantic::types::constraints::PathAssignment", new = %format_args!( "[{}]", - self.assignments[start..].iter().map(|assignment| assignment.display(db)).format(", "), + self.assignments[start..].iter().map(|(assignment, _)| assignment.display(db)).format(", "), ), "new assignments", ); @@ -3248,7 +3270,7 @@ impl<'db> PathAssignments<'db> { } fn assignment_holds(&self, assignment: ConstraintAssignment<'db>) -> bool { - self.assignments.contains(&assignment) + self.assignments.contains_key(&assignment) } /// Adds a new assignment, along with any derived information that we can infer from the new @@ -3259,26 +3281,34 @@ impl<'db> PathAssignments<'db> { db: &'db dyn Db, map: &SequentMap<'db>, assignment: ConstraintAssignment<'db>, + source_order: usize, ) -> 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()) { + if self.assignments.contains_key(&assignment.negated()) { tracing::trace!( target: "ty_python_semantic::types::constraints::PathAssignment", assignment = %assignment.display(db), facts = %format_args!( "[{}]", - self.assignments.iter().map(|assignment| assignment.display(db)).format(", "), + self.assignments.iter().map(|(assignment, _)| assignment.display(db)).format(", "), ), "found contradiction", ); return Err(PathAssignmentConflict); } - if !self.assignments.insert(assignment) { + if self.assignments.insert(assignment, source_order).is_some() { return Ok(()); } - // Then use our sequents to add additional facts that we know to be true. + // Then use our sequents to add additional facts that we know to be true. We currently + // reuse the `source_order` of the "real" constraint passed into `walk_edge` when we add + // these derived facts. + // + // TODO: This might not be stable enough, if we add more than one derived fact for this + // constraint. If we still see inconsistent test output, we might need a more complex + // way of tracking source order for derived facts. + // // 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. We might consider avoiding the // brute-force search. @@ -3292,7 +3322,7 @@ impl<'db> PathAssignments<'db> { ante = %ante.display(db), facts = %format_args!( "[{}]", - self.assignments.iter().map(|assignment| assignment.display(db)).format(", "), + self.assignments.iter().map(|(assignment, _)| assignment.display(db)).format(", "), ), "found contradiction", ); @@ -3311,7 +3341,7 @@ impl<'db> PathAssignments<'db> { ante2 = %ante2.display(db), facts = %format_args!( "[{}]", - self.assignments.iter().map(|assignment| assignment.display(db)).format(", "), + self.assignments.iter().map(|(assignment, _)| assignment.display(db)).format(", "), ), "found contradiction", ); @@ -3324,7 +3354,7 @@ impl<'db> PathAssignments<'db> { if self.assignment_holds(ante1.when_true()) && self.assignment_holds(ante2.when_true()) { - self.add_assignment(db, map, post.when_true())?; + self.add_assignment(db, map, post.when_true(), source_order)?; } } } @@ -3332,7 +3362,7 @@ impl<'db> PathAssignments<'db> { for (ante, posts) in &map.single_implications { for post in posts { if self.assignment_holds(ante.when_true()) { - self.add_assignment(db, map, post.when_true())?; + self.add_assignment(db, map, post.when_true(), source_order)?; } } } From c790aa747478de85c86be0b17c88c9df2eee2202 Mon Sep 17 00:00:00 2001 From: Douglas Creager Date: Mon, 15 Dec 2025 15:54:23 -0500 Subject: [PATCH 3/5] track whether constraints are explicit or not --- .../src/types/constraints.rs | 320 +++++++++++++++--- 1 file changed, 268 insertions(+), 52 deletions(-) diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs index df8a2af480..3f7d52a736 100644 --- a/crates/ty_python_semantic/src/types/constraints.rs +++ b/crates/ty_python_semantic/src/types/constraints.rs @@ -69,7 +69,7 @@ use std::cell::RefCell; use std::cmp::Ordering; use std::fmt::Display; -use std::ops::Range; +use std::ops::{BitAnd, BitOr, Range}; use itertools::Itertools; use rustc_hash::{FxHashMap, FxHashSet}; @@ -205,7 +205,13 @@ impl<'db> ConstraintSet<'db> { upper: Type<'db>, ) -> Self { Self { - node: ConstrainedTypeVar::new_node(db, typevar, lower, upper), + node: ConstrainedTypeVar::new_node( + db, + typevar, + lower, + upper, + ExplicitConstraint::Explicit, + ), } } @@ -501,13 +507,12 @@ impl get_size2::GetSize for ConstrainedTypeVar<'_> {} #[salsa::tracked] impl<'db> ConstrainedTypeVar<'db> { /// Returns a new range constraint. - /// - /// Panics if `lower` and `upper` are not both fully static. fn new_node( db: &'db dyn Db, typevar: BoundTypeVarInstance<'db>, mut lower: Type<'db>, mut upper: Type<'db>, + explicit: ExplicitConstraint, ) -> Node<'db> { // It's not useful for an upper bound to be an intersection type, or for a lower bound to // be a union type. Because the following equivalences hold, we can break these bounds @@ -522,7 +527,7 @@ impl<'db> ConstrainedTypeVar<'db> { for lower_element in lower_union.elements(db) { result = result.and_with_offset( db, - ConstrainedTypeVar::new_node(db, typevar, *lower_element, upper), + ConstrainedTypeVar::new_node(db, typevar, *lower_element, upper, explicit), ); } return result; @@ -537,13 +542,19 @@ impl<'db> ConstrainedTypeVar<'db> { for upper_element in upper_intersection.iter_positive(db) { result = result.and_with_offset( db, - ConstrainedTypeVar::new_node(db, typevar, lower, upper_element), + ConstrainedTypeVar::new_node(db, typevar, lower, upper_element, explicit), ); } for upper_element in upper_intersection.iter_negative(db) { result = result.and_with_offset( db, - ConstrainedTypeVar::new_node(db, typevar, lower, upper_element.negate(db)), + ConstrainedTypeVar::new_node( + db, + typevar, + lower, + upper_element.negate(db), + explicit, + ), ); } return result; @@ -576,6 +587,7 @@ impl<'db> ConstrainedTypeVar<'db> { return Node::new_constraint( db, ConstrainedTypeVar::new(db, typevar, Type::Never, Type::object()), + explicit, 1, ) .negate(db); @@ -628,6 +640,7 @@ impl<'db> ConstrainedTypeVar<'db> { Type::TypeVar(bound), Type::TypeVar(bound), ), + explicit, 1, ) } @@ -639,11 +652,13 @@ impl<'db> ConstrainedTypeVar<'db> { let lower = Node::new_constraint( db, ConstrainedTypeVar::new(db, lower, Type::Never, Type::TypeVar(typevar)), + explicit, 1, ); let upper = Node::new_constraint( db, ConstrainedTypeVar::new(db, upper, Type::TypeVar(typevar), Type::object()), + explicit, 1, ); lower.and(db, upper) @@ -654,12 +669,13 @@ impl<'db> ConstrainedTypeVar<'db> { let lower = Node::new_constraint( db, ConstrainedTypeVar::new(db, lower, Type::Never, Type::TypeVar(typevar)), + explicit, 1, ); let upper = if upper.is_object() { Node::AlwaysTrue } else { - Self::new_node(db, typevar, Type::Never, upper) + Self::new_node(db, typevar, Type::Never, upper, explicit) }; lower.and(db, upper) } @@ -669,17 +685,23 @@ impl<'db> ConstrainedTypeVar<'db> { let lower = if lower.is_never() { Node::AlwaysTrue } else { - Self::new_node(db, typevar, lower, Type::object()) + Self::new_node(db, typevar, lower, Type::object(), explicit) }; let upper = Node::new_constraint( db, ConstrainedTypeVar::new(db, upper, Type::TypeVar(typevar), Type::object()), + explicit, 1, ); lower.and(db, upper) } - _ => Node::new_constraint(db, ConstrainedTypeVar::new(db, typevar, lower, upper), 1), + _ => Node::new_constraint( + db, + ConstrainedTypeVar::new(db, typevar, lower, upper), + explicit, + 1, + ), } } @@ -868,6 +890,7 @@ impl<'db> Node<'db> { constraint: ConstrainedTypeVar<'db>, if_true: Node<'db>, if_false: Node<'db>, + explicit: ExplicitConstraint, source_order: usize, ) -> Self { debug_assert!((if_true.root_constraint(db)).is_none_or(|root_constraint| { @@ -889,6 +912,7 @@ impl<'db> Node<'db> { constraint, if_true, if_false, + explicit, source_order, max_source_order, )) @@ -899,6 +923,7 @@ impl<'db> Node<'db> { fn new_constraint( db: &'db dyn Db, constraint: ConstrainedTypeVar<'db>, + explicit: ExplicitConstraint, source_order: usize, ) -> Self { Self::Interior(InteriorNode::new( @@ -906,6 +931,7 @@ impl<'db> Node<'db> { constraint, Node::AlwaysTrue, Node::AlwaysFalse, + explicit, source_order, source_order, )) @@ -917,6 +943,7 @@ impl<'db> Node<'db> { fn new_satisfied_constraint( db: &'db dyn Db, constraint: ConstraintAssignment<'db>, + explicit: ExplicitConstraint, source_order: usize, ) -> Self { match constraint { @@ -925,6 +952,7 @@ impl<'db> Node<'db> { constraint, Node::AlwaysTrue, Node::AlwaysFalse, + explicit, source_order, source_order, )), @@ -933,6 +961,7 @@ impl<'db> Node<'db> { constraint, Node::AlwaysFalse, Node::AlwaysTrue, + explicit, source_order, source_order, )), @@ -968,6 +997,7 @@ impl<'db> Node<'db> { interior.constraint(db), interior.if_true(db).with_adjusted_source_order(db, delta), interior.if_false(db).with_adjusted_source_order(db, delta), + interior.explicit(db), interior.source_order(db) + delta, ), } @@ -1000,24 +1030,39 @@ impl<'db> Node<'db> { // 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 explicit = interior.explicit(db); let source_order = interior.source_order(db); let true_always_satisfied = path - .walk_edge(db, map, constraint.when_true(), source_order, |path, _| { - interior - .if_true(db) - .is_always_satisfied_inner(db, map, path) - }) + .walk_edge( + db, + map, + constraint.when_true(), + explicit, + source_order, + |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.walk_edge(db, map, constraint.when_false(), source_order, |path, _| { - interior - .if_false(db) - .is_always_satisfied_inner(db, map, path) - }) + path.walk_edge( + db, + map, + constraint.when_false(), + explicit, + source_order, + |path, _| { + interior + .if_false(db) + .is_always_satisfied_inner(db, map, path) + }, + ) .unwrap_or(true) } } @@ -1050,22 +1095,35 @@ impl<'db> Node<'db> { // 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 explicit = interior.explicit(db); let source_order = interior.source_order(db); let true_never_satisfied = path - .walk_edge(db, map, constraint.when_true(), source_order, |path, _| { - interior.if_true(db).is_never_satisfied_inner(db, map, path) - }) + .walk_edge( + db, + map, + constraint.when_true(), + explicit, + source_order, + |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.walk_edge(db, map, constraint.when_false(), source_order, |path, _| { - interior - .if_false(db) - .is_never_satisfied_inner(db, map, path) - }) + path.walk_edge( + db, + map, + constraint.when_false(), + explicit, + source_order, + |path, _| { + interior + .if_false(db) + .is_never_satisfied_inner(db, map, path) + }, + ) .unwrap_or(true) } } @@ -1108,6 +1166,7 @@ impl<'db> Node<'db> { other_interior.constraint(db), Node::AlwaysTrue, Node::AlwaysTrue, + other_interior.explicit(db), other_interior.source_order(db) + other_offset, ), (Node::Interior(self_interior), Node::AlwaysTrue) => Node::new( @@ -1115,6 +1174,7 @@ impl<'db> Node<'db> { self_interior.constraint(db), Node::AlwaysTrue, Node::AlwaysTrue, + self_interior.explicit(db), self_interior.source_order(db), ), (Node::AlwaysFalse, _) => other.with_adjusted_source_order(db, other_offset), @@ -1148,6 +1208,7 @@ impl<'db> Node<'db> { other_interior.constraint(db), Node::AlwaysFalse, Node::AlwaysFalse, + other_interior.explicit(db), other_interior.source_order(db) + other_offset, ), (Node::Interior(self_interior), Node::AlwaysFalse) => Node::new( @@ -1155,6 +1216,7 @@ impl<'db> Node<'db> { self_interior.constraint(db), Node::AlwaysFalse, Node::AlwaysFalse, + self_interior.explicit(db), self_interior.source_order(db), ), (Node::AlwaysTrue, _) => other.with_adjusted_source_order(db, other_offset), @@ -1199,6 +1261,7 @@ impl<'db> Node<'db> { interior.constraint(db), self.iff_inner(db, interior.if_true(db), other_offset), self.iff_inner(db, interior.if_false(db), other_offset), + interior.explicit(db), interior.source_order(db) + other_offset, ), (Node::Interior(interior), Node::AlwaysTrue | Node::AlwaysFalse) => Node::new( @@ -1206,6 +1269,7 @@ impl<'db> Node<'db> { interior.constraint(db), interior.if_true(db).iff_inner(db, other, other_offset), interior.if_false(db).iff_inner(db, other, other_offset), + interior.explicit(db), interior.source_order(db), ), (Node::Interior(a), Node::Interior(b)) => a.iff(db, b, other_offset), @@ -1234,12 +1298,14 @@ impl<'db> Node<'db> { bound_typevar, Type::Never, rhs.bottom_materialization(db), + ExplicitConstraint::Implicit, ), (_, Type::TypeVar(bound_typevar)) => ConstrainedTypeVar::new_node( db, bound_typevar, lhs.top_materialization(db), Type::object(), + ExplicitConstraint::Implicit, ), _ => panic!("at least one type should be a typevar"), }; @@ -1529,8 +1595,18 @@ impl<'db> Node<'db> { // false // // (Note that the `else` branch shouldn't be reachable, but we have to provide something!) - let left_node = Node::new_satisfied_constraint(db, left, left_source_order); - let right_node = Node::new_satisfied_constraint(db, right, right_source_order); + let left_node = Node::new_satisfied_constraint( + db, + left, + ExplicitConstraint::Implicit, + left_source_order, + ); + let right_node = Node::new_satisfied_constraint( + db, + right, + ExplicitConstraint::Implicit, + right_source_order, + ); let right_result = right_node.ite(db, Node::AlwaysFalse, when_left_but_not_right); let left_result = left_node.ite(db, right_result, when_not_left); let result = replacement.ite(db, when_left_and_right, left_result); @@ -1595,8 +1671,18 @@ impl<'db> Node<'db> { // Lastly, verify that the result is consistent with the input. (It must produce the same // results when `left ∨ right`.) If it doesn't, the substitution isn't valid, and we should // return the original BDD unmodified. - let left_node = Node::new_satisfied_constraint(db, left, left_source_order); - let right_node = Node::new_satisfied_constraint(db, right, right_source_order); + let left_node = Node::new_satisfied_constraint( + db, + left, + ExplicitConstraint::Implicit, + left_source_order, + ); + let right_node = Node::new_satisfied_constraint( + db, + right, + ExplicitConstraint::Implicit, + right_source_order, + ); let validity = replacement.iff(db, left_node.or(db, right_node)); let constrained_original = self.and(db, validity); let constrained_replacement = result.and(db, validity); @@ -1753,8 +1839,9 @@ impl<'db> Node<'db> { Node::Interior(interior) => { write!( f, - "{} {}/{}", + "{} {:?} {}/{}", interior.constraint(self.db).display(self.db), + interior.explicit(self.db), interior.source_order(self.db), interior.max_source_order(self.db), )?; @@ -1811,12 +1898,47 @@ impl<'db> RepresentativeBounds<'db> { } } +#[derive(Clone, Copy, Debug, Eq, PartialEq, Hash, get_size2::GetSize, salsa::Update)] +pub(crate) enum ExplicitConstraint { + Implicit, + Explicit, +} + +impl BitAnd for ExplicitConstraint { + type Output = Self; + fn bitand(self, other: Self) -> Self { + match (self, other) { + (ExplicitConstraint::Explicit, ExplicitConstraint::Explicit) => { + ExplicitConstraint::Explicit + } + (ExplicitConstraint::Implicit, _) | (_, ExplicitConstraint::Implicit) => { + ExplicitConstraint::Implicit + } + } + } +} + +impl BitOr for ExplicitConstraint { + type Output = Self; + fn bitor(self, other: Self) -> Self { + match (self, other) { + (ExplicitConstraint::Implicit, ExplicitConstraint::Implicit) => { + ExplicitConstraint::Implicit + } + (ExplicitConstraint::Explicit, _) | (_, ExplicitConstraint::Explicit) => { + ExplicitConstraint::Explicit + } + } + } +} + /// An interior node of a BDD #[salsa::interned(debug, heap_size=ruff_memory_usage::heap_size)] struct InteriorNode<'db> { constraint: ConstrainedTypeVar<'db>, if_true: Node<'db>, if_false: Node<'db>, + explicit: ExplicitConstraint, /// Represents the order in which this node's constraint was added to the containing constraint /// set, relative to all of the other constraints in the set. This starts off at 1 for a simple @@ -1841,6 +1963,7 @@ impl<'db> InteriorNode<'db> { self.constraint(db), self.if_true(db).negate(db), self.if_false(db).negate(db), + self.explicit(db), self.source_order(db), ) } @@ -1857,6 +1980,7 @@ impl<'db> InteriorNode<'db> { .or_inner(db, other.if_true(db), other_offset), self.if_false(db) .or_inner(db, other.if_false(db), other_offset), + self.explicit(db) & other.explicit(db), self.source_order(db), ), Ordering::Less => Node::new( @@ -1866,6 +1990,7 @@ impl<'db> InteriorNode<'db> { .or_inner(db, Node::Interior(other), other_offset), self.if_false(db) .or_inner(db, Node::Interior(other), other_offset), + self.explicit(db), self.source_order(db), ), Ordering::Greater => Node::new( @@ -1873,6 +1998,7 @@ impl<'db> InteriorNode<'db> { other_constraint, Node::Interior(self).or_inner(db, other.if_true(db), other_offset), Node::Interior(self).or_inner(db, other.if_false(db), other_offset), + other.explicit(db), other.source_order(db) + other_offset, ), } @@ -1890,6 +2016,7 @@ impl<'db> InteriorNode<'db> { .and_inner(db, other.if_true(db), other_offset), self.if_false(db) .and_inner(db, other.if_false(db), other_offset), + self.explicit(db) & other.explicit(db), self.source_order(db), ), Ordering::Less => Node::new( @@ -1899,6 +2026,7 @@ impl<'db> InteriorNode<'db> { .and_inner(db, Node::Interior(other), other_offset), self.if_false(db) .and_inner(db, Node::Interior(other), other_offset), + self.explicit(db), self.source_order(db), ), Ordering::Greater => Node::new( @@ -1906,6 +2034,7 @@ impl<'db> InteriorNode<'db> { other_constraint, Node::Interior(self).and_inner(db, other.if_true(db), other_offset), Node::Interior(self).and_inner(db, other.if_false(db), other_offset), + other.explicit(db), other.source_order(db) + other_offset, ), } @@ -1923,6 +2052,7 @@ impl<'db> InteriorNode<'db> { .iff_inner(db, other.if_true(db), other_offset), self.if_false(db) .iff_inner(db, other.if_false(db), other_offset), + self.explicit(db) & other.explicit(db), self.source_order(db), ), Ordering::Less => Node::new( @@ -1932,6 +2062,7 @@ impl<'db> InteriorNode<'db> { .iff_inner(db, Node::Interior(other), other_offset), self.if_false(db) .iff_inner(db, Node::Interior(other), other_offset), + self.explicit(db), self.source_order(db), ), Ordering::Greater => Node::new( @@ -1939,6 +2070,7 @@ impl<'db> InteriorNode<'db> { other_constraint, Node::Interior(self).iff_inner(db, other.if_true(db), other_offset), Node::Interior(self).iff_inner(db, other.if_false(db), other_offset), + other.explicit(db), other.source_order(db) + other_offset, ), } @@ -2008,6 +2140,7 @@ impl<'db> InteriorNode<'db> { ) -> Node<'db> { let self_constraint = self.constraint(db); let self_source_order = self.source_order(db); + let self_explicit = self.explicit(db); if should_remove(self_constraint) { // If we should remove constraints involving this typevar, then we replace this node // with the OR of its if_false/if_true edges. That is, the result is true if there's @@ -2021,6 +2154,7 @@ impl<'db> InteriorNode<'db> { db, map, self_constraint.when_true(), + self_explicit, self_source_order, |path, new_range| { let branch = @@ -2033,10 +2167,15 @@ impl<'db> InteriorNode<'db> { // removed! !should_remove(assignment.constraint()) }) - .fold(branch, |branch, (assignment, source_order)| { + .fold(branch, |branch, (assignment, (explicit, source_order))| { branch.and( db, - Node::new_satisfied_constraint(db, *assignment, *source_order), + Node::new_satisfied_constraint( + db, + *assignment, + *explicit, + *source_order, + ), ) }) }, @@ -2047,6 +2186,7 @@ impl<'db> InteriorNode<'db> { db, map, self_constraint.when_false(), + self_explicit, self_source_order, |path, new_range| { let branch = @@ -2059,10 +2199,15 @@ impl<'db> InteriorNode<'db> { // removed! !should_remove(assignment.constraint()) }) - .fold(branch, |branch, (assignment, source_order)| { + .fold(branch, |branch, (assignment, (explicit, source_order))| { branch.and( db, - Node::new_satisfied_constraint(db, *assignment, *source_order), + Node::new_satisfied_constraint( + db, + *assignment, + *explicit, + *source_order, + ), ) }) }, @@ -2076,6 +2221,7 @@ impl<'db> InteriorNode<'db> { db, map, self_constraint.when_true(), + self_explicit, self_source_order, |path, _| { self.if_true(db) @@ -2088,6 +2234,7 @@ impl<'db> InteriorNode<'db> { db, map, self_constraint.when_false(), + self_explicit, self_source_order, |path, _| { self.if_false(db) @@ -2098,7 +2245,7 @@ impl<'db> InteriorNode<'db> { // NB: We cannot use `Node::new` here, because the recursive calls might introduce new // derived constraints into the result, and those constraints might appear before this // one in the BDD ordering. - Node::new_constraint(db, self_constraint, self.source_order(db)) + Node::new_constraint(db, self_constraint, self_explicit, self_source_order) .ite(db, if_true, if_false) } } @@ -2132,6 +2279,7 @@ impl<'db> InteriorNode<'db> { self_constraint, if_true, if_false, + self.explicit(db), self.source_order(db), ), found_in_true || found_in_false, @@ -2267,16 +2415,23 @@ impl<'db> InteriorNode<'db> { if seen_constraints.contains(&new_constraint) { continue; } - let new_node = Node::new_constraint(db, new_constraint, next_source_order); + let new_node = Node::new_constraint( + db, + new_constraint, + ExplicitConstraint::Implicit, + next_source_order, + ); next_source_order += 1; let positive_left_node = Node::new_satisfied_constraint( db, left_constraint.when_true(), + ExplicitConstraint::Implicit, left_source_order, ); let positive_right_node = Node::new_satisfied_constraint( db, right_constraint.when_true(), + ExplicitConstraint::Implicit, right_source_order, ); let lhs = positive_left_node.and(db, positive_right_node); @@ -2327,11 +2482,13 @@ impl<'db> InteriorNode<'db> { let positive_larger_node = Node::new_satisfied_constraint( db, larger_constraint.when_true(), + ExplicitConstraint::Implicit, larger_source_order, ); let negative_larger_node = Node::new_satisfied_constraint( db, larger_constraint.when_false(), + ExplicitConstraint::Implicit, larger_source_order, ); @@ -2399,11 +2556,13 @@ impl<'db> InteriorNode<'db> { let positive_intersection_node = Node::new_satisfied_constraint( db, intersection_constraint.when_true(), + ExplicitConstraint::Implicit, next_source_order, ); let negative_intersection_node = Node::new_satisfied_constraint( db, intersection_constraint.when_false(), + ExplicitConstraint::Implicit, next_source_order, ); next_source_order += 1; @@ -2411,22 +2570,26 @@ impl<'db> InteriorNode<'db> { let positive_left_node = Node::new_satisfied_constraint( db, left_constraint.when_true(), + ExplicitConstraint::Implicit, left_source_order, ); let negative_left_node = Node::new_satisfied_constraint( db, left_constraint.when_false(), + ExplicitConstraint::Implicit, left_source_order, ); let positive_right_node = Node::new_satisfied_constraint( db, right_constraint.when_true(), + ExplicitConstraint::Implicit, right_source_order, ); let negative_right_node = Node::new_satisfied_constraint( db, right_constraint.when_false(), + ExplicitConstraint::Implicit, right_source_order, ); @@ -2508,11 +2671,13 @@ impl<'db> InteriorNode<'db> { let positive_left_node = Node::new_satisfied_constraint( db, left_constraint.when_true(), + ExplicitConstraint::Implicit, left_source_order, ); let positive_right_node = Node::new_satisfied_constraint( db, right_constraint.when_true(), + ExplicitConstraint::Implicit, right_source_order, ); @@ -3191,7 +3356,7 @@ impl<'db> SequentMap<'db> { /// traversing a BDD. #[derive(Debug, Default)] pub(crate) struct PathAssignments<'db> { - assignments: FxOrderMap, usize>, + assignments: FxOrderMap, (ExplicitConstraint, usize)>, } impl<'db> PathAssignments<'db> { @@ -3222,6 +3387,7 @@ impl<'db> PathAssignments<'db> { db: &'db dyn Db, map: &SequentMap<'db>, assignment: ConstraintAssignment<'db>, + explicit: ExplicitConstraint, source_order: usize, f: impl FnOnce(&mut Self, Range) -> R, ) -> Option { @@ -3240,7 +3406,7 @@ impl<'db> PathAssignments<'db> { edge = %assignment.display(db), "walk edge", ); - let found_conflict = self.add_assignment(db, map, assignment, source_order); + let found_conflict = self.add_assignment(db, map, assignment, explicit, source_order); let result = if found_conflict.is_err() { // If that results in the path now being impossible due to a contradiction, return // without invoking the callback. @@ -3273,6 +3439,15 @@ impl<'db> PathAssignments<'db> { self.assignments.contains_key(&assignment) } + fn assignment_holds_explicitly( + &self, + assignment: ConstraintAssignment<'db>, + ) -> Option { + self.assignments + .get(&assignment) + .map(|(explicit, _)| *explicit) + } + /// 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. @@ -3281,6 +3456,7 @@ impl<'db> PathAssignments<'db> { db: &'db dyn Db, map: &SequentMap<'db>, assignment: ConstraintAssignment<'db>, + explicit: ExplicitConstraint, source_order: usize, ) -> Result<(), PathAssignmentConflict> { // First add this assignment. If it causes a conflict, return that as an error. If we've @@ -3297,7 +3473,11 @@ impl<'db> PathAssignments<'db> { ); return Err(PathAssignmentConflict); } - if self.assignments.insert(assignment, source_order).is_some() { + if self + .assignments + .insert(assignment, (explicit, source_order)) + .is_some() + { return Ok(()); } @@ -3351,18 +3531,31 @@ impl<'db> PathAssignments<'db> { for ((ante1, ante2), posts) in &map.pair_implications { for post in posts { - if self.assignment_holds(ante1.when_true()) - && self.assignment_holds(ante2.when_true()) + if let Some(ante1_explicit) = self.assignment_holds_explicitly(ante1.when_true()) + && let Some(ante2_explicit) = + self.assignment_holds_explicitly(ante2.when_true()) { - self.add_assignment(db, map, post.when_true(), source_order)?; + self.add_assignment( + db, + map, + post.when_true(), + explicit & ante1_explicit & ante2_explicit, + source_order, + )?; } } } for (ante, posts) in &map.single_implications { for post in posts { - if self.assignment_holds(ante.when_true()) { - self.add_assignment(db, map, post.when_true(), source_order)?; + if let Some(ante_explicit) = self.assignment_holds_explicitly(ante.when_true()) { + self.add_assignment( + db, + map, + post.when_true(), + explicit & ante_explicit, + source_order, + )?; } } } @@ -3615,7 +3808,13 @@ impl<'db> BoundTypeVarInstance<'db> { None => Node::AlwaysTrue, Some(TypeVarBoundOrConstraints::UpperBound(bound)) => { let bound = bound.top_materialization(db); - ConstrainedTypeVar::new_node(db, self, Type::Never, bound) + ConstrainedTypeVar::new_node( + db, + self, + Type::Never, + bound, + ExplicitConstraint::Implicit, + ) } Some(TypeVarBoundOrConstraints::Constraints(constraints)) => { let mut specializations = Node::AlwaysFalse; @@ -3624,7 +3823,13 @@ impl<'db> BoundTypeVarInstance<'db> { let constraint_upper = constraint.top_materialization(db); specializations = specializations.or_with_offset( db, - ConstrainedTypeVar::new_node(db, self, constraint_lower, constraint_upper), + ConstrainedTypeVar::new_node( + db, + self, + constraint_lower, + constraint_upper, + ExplicitConstraint::Implicit, + ), ); } specializations @@ -3659,7 +3864,13 @@ impl<'db> BoundTypeVarInstance<'db> { Some(TypeVarBoundOrConstraints::UpperBound(bound)) => { let bound = bound.bottom_materialization(db); ( - ConstrainedTypeVar::new_node(db, self, Type::Never, bound), + ConstrainedTypeVar::new_node( + db, + self, + Type::Never, + bound, + ExplicitConstraint::Implicit, + ), Vec::new(), ) } @@ -3669,8 +3880,13 @@ impl<'db> BoundTypeVarInstance<'db> { for constraint in constraints.elements(db) { let constraint_lower = constraint.bottom_materialization(db); let constraint_upper = constraint.top_materialization(db); - let constraint = - ConstrainedTypeVar::new_node(db, self, constraint_lower, constraint_upper); + let constraint = ConstrainedTypeVar::new_node( + db, + self, + constraint_lower, + constraint_upper, + ExplicitConstraint::Implicit, + ); if constraint_lower == constraint_upper { non_gradual_constraints = non_gradual_constraints.or_with_offset(db, constraint); From 0b6bd9a735cdd8d76c63dc8339b339fc00a284bc Mon Sep 17 00:00:00 2001 From: Douglas Creager Date: Mon, 15 Dec 2025 16:36:53 -0500 Subject: [PATCH 4/5] store this in constraint, not node --- .../src/types/constraints.rs | 357 ++++++++---------- 1 file changed, 147 insertions(+), 210 deletions(-) diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs index 3f7d52a736..8382168dba 100644 --- a/crates/ty_python_semantic/src/types/constraints.rs +++ b/crates/ty_python_semantic/src/types/constraints.rs @@ -496,9 +496,10 @@ impl IntersectionResult<'_> { /// lower and upper bound. #[salsa::interned(debug, heap_size=ruff_memory_usage::heap_size)] pub(crate) struct ConstrainedTypeVar<'db> { - typevar: BoundTypeVarInstance<'db>, - lower: Type<'db>, - upper: Type<'db>, + pub(crate) typevar: BoundTypeVarInstance<'db>, + pub(crate) lower: Type<'db>, + pub(crate) upper: Type<'db>, + pub(crate) explicit: ExplicitConstraint, } // The Salsa heap is tracked separately. @@ -586,8 +587,7 @@ impl<'db> ConstrainedTypeVar<'db> { { return Node::new_constraint( db, - ConstrainedTypeVar::new(db, typevar, Type::Never, Type::object()), - explicit, + ConstrainedTypeVar::new(db, typevar, Type::Never, Type::object(), explicit), 1, ) .negate(db); @@ -639,8 +639,8 @@ impl<'db> ConstrainedTypeVar<'db> { typevar, Type::TypeVar(bound), Type::TypeVar(bound), + explicit, ), - explicit, 1, ) } @@ -651,14 +651,24 @@ impl<'db> ConstrainedTypeVar<'db> { { let lower = Node::new_constraint( db, - ConstrainedTypeVar::new(db, lower, Type::Never, Type::TypeVar(typevar)), - explicit, + ConstrainedTypeVar::new( + db, + lower, + Type::Never, + Type::TypeVar(typevar), + explicit, + ), 1, ); let upper = Node::new_constraint( db, - ConstrainedTypeVar::new(db, upper, Type::TypeVar(typevar), Type::object()), - explicit, + ConstrainedTypeVar::new( + db, + upper, + Type::TypeVar(typevar), + Type::object(), + explicit, + ), 1, ); lower.and(db, upper) @@ -668,8 +678,13 @@ impl<'db> ConstrainedTypeVar<'db> { (Type::TypeVar(lower), _) if typevar.can_be_bound_for(db, lower) => { let lower = Node::new_constraint( db, - ConstrainedTypeVar::new(db, lower, Type::Never, Type::TypeVar(typevar)), - explicit, + ConstrainedTypeVar::new( + db, + lower, + Type::Never, + Type::TypeVar(typevar), + explicit, + ), 1, ); let upper = if upper.is_object() { @@ -689,8 +704,13 @@ impl<'db> ConstrainedTypeVar<'db> { }; let upper = Node::new_constraint( db, - ConstrainedTypeVar::new(db, upper, Type::TypeVar(typevar), Type::object()), - explicit, + ConstrainedTypeVar::new( + db, + upper, + Type::TypeVar(typevar), + Type::object(), + explicit, + ), 1, ); lower.and(db, upper) @@ -698,8 +718,7 @@ impl<'db> ConstrainedTypeVar<'db> { _ => Node::new_constraint( db, - ConstrainedTypeVar::new(db, typevar, lower, upper), - explicit, + ConstrainedTypeVar::new(db, typevar, lower, upper, explicit), 1, ), } @@ -719,6 +738,7 @@ impl<'db> ConstrainedTypeVar<'db> { self.typevar(db), self.lower(db).normalized(db), self.upper(db).normalized(db), + self.explicit(db), ) } @@ -735,7 +755,12 @@ impl<'db> ConstrainedTypeVar<'db> { /// simplifications that we perform that operate on constraints with the same typevar, and this /// ensures that we can find all candidate simplifications more easily. fn ordering(self, db: &'db dyn Db) -> impl Ord { - (self.typevar(db).identity(db), self.as_id()) + ( + self.typevar(db).binding_context(db), + self.typevar(db).identity(db), + self.explicit(db), + self.as_id(), + ) } /// Returns whether this constraint implies another — i.e., whether every type that @@ -767,7 +792,13 @@ impl<'db> ConstrainedTypeVar<'db> { return IntersectionResult::CannotSimplify; } - IntersectionResult::Simplified(Self::new(db, self.typevar(db), lower, upper)) + IntersectionResult::Simplified(Self::new( + db, + self.typevar(db), + lower, + upper, + self.explicit(db) & other.explicit(db), + )) } fn display(self, db: &'db dyn Db) -> impl Display { @@ -890,7 +921,6 @@ impl<'db> Node<'db> { constraint: ConstrainedTypeVar<'db>, if_true: Node<'db>, if_false: Node<'db>, - explicit: ExplicitConstraint, source_order: usize, ) -> Self { debug_assert!((if_true.root_constraint(db)).is_none_or(|root_constraint| { @@ -912,7 +942,6 @@ impl<'db> Node<'db> { constraint, if_true, if_false, - explicit, source_order, max_source_order, )) @@ -923,7 +952,6 @@ impl<'db> Node<'db> { fn new_constraint( db: &'db dyn Db, constraint: ConstrainedTypeVar<'db>, - explicit: ExplicitConstraint, source_order: usize, ) -> Self { Self::Interior(InteriorNode::new( @@ -931,7 +959,6 @@ impl<'db> Node<'db> { constraint, Node::AlwaysTrue, Node::AlwaysFalse, - explicit, source_order, source_order, )) @@ -943,7 +970,6 @@ impl<'db> Node<'db> { fn new_satisfied_constraint( db: &'db dyn Db, constraint: ConstraintAssignment<'db>, - explicit: ExplicitConstraint, source_order: usize, ) -> Self { match constraint { @@ -952,7 +978,6 @@ impl<'db> Node<'db> { constraint, Node::AlwaysTrue, Node::AlwaysFalse, - explicit, source_order, source_order, )), @@ -961,7 +986,6 @@ impl<'db> Node<'db> { constraint, Node::AlwaysFalse, Node::AlwaysTrue, - explicit, source_order, source_order, )), @@ -997,7 +1021,6 @@ impl<'db> Node<'db> { interior.constraint(db), interior.if_true(db).with_adjusted_source_order(db, delta), interior.if_false(db).with_adjusted_source_order(db, delta), - interior.explicit(db), interior.source_order(db) + delta, ), } @@ -1030,39 +1053,24 @@ impl<'db> Node<'db> { // 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 explicit = interior.explicit(db); let source_order = interior.source_order(db); let true_always_satisfied = path - .walk_edge( - db, - map, - constraint.when_true(), - explicit, - source_order, - |path, _| { - interior - .if_true(db) - .is_always_satisfied_inner(db, map, path) - }, - ) + .walk_edge(db, map, constraint.when_true(), source_order, |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.walk_edge( - db, - map, - constraint.when_false(), - explicit, - source_order, - |path, _| { - interior - .if_false(db) - .is_always_satisfied_inner(db, map, path) - }, - ) + path.walk_edge(db, map, constraint.when_false(), source_order, |path, _| { + interior + .if_false(db) + .is_always_satisfied_inner(db, map, path) + }) .unwrap_or(true) } } @@ -1095,35 +1103,22 @@ impl<'db> Node<'db> { // 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 explicit = interior.explicit(db); let source_order = interior.source_order(db); let true_never_satisfied = path - .walk_edge( - db, - map, - constraint.when_true(), - explicit, - source_order, - |path, _| interior.if_true(db).is_never_satisfied_inner(db, map, path), - ) + .walk_edge(db, map, constraint.when_true(), source_order, |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.walk_edge( - db, - map, - constraint.when_false(), - explicit, - source_order, - |path, _| { - interior - .if_false(db) - .is_never_satisfied_inner(db, map, path) - }, - ) + path.walk_edge(db, map, constraint.when_false(), source_order, |path, _| { + interior + .if_false(db) + .is_never_satisfied_inner(db, map, path) + }) .unwrap_or(true) } } @@ -1166,7 +1161,6 @@ impl<'db> Node<'db> { other_interior.constraint(db), Node::AlwaysTrue, Node::AlwaysTrue, - other_interior.explicit(db), other_interior.source_order(db) + other_offset, ), (Node::Interior(self_interior), Node::AlwaysTrue) => Node::new( @@ -1174,7 +1168,6 @@ impl<'db> Node<'db> { self_interior.constraint(db), Node::AlwaysTrue, Node::AlwaysTrue, - self_interior.explicit(db), self_interior.source_order(db), ), (Node::AlwaysFalse, _) => other.with_adjusted_source_order(db, other_offset), @@ -1208,7 +1201,6 @@ impl<'db> Node<'db> { other_interior.constraint(db), Node::AlwaysFalse, Node::AlwaysFalse, - other_interior.explicit(db), other_interior.source_order(db) + other_offset, ), (Node::Interior(self_interior), Node::AlwaysFalse) => Node::new( @@ -1216,7 +1208,6 @@ impl<'db> Node<'db> { self_interior.constraint(db), Node::AlwaysFalse, Node::AlwaysFalse, - self_interior.explicit(db), self_interior.source_order(db), ), (Node::AlwaysTrue, _) => other.with_adjusted_source_order(db, other_offset), @@ -1261,7 +1252,6 @@ impl<'db> Node<'db> { interior.constraint(db), self.iff_inner(db, interior.if_true(db), other_offset), self.iff_inner(db, interior.if_false(db), other_offset), - interior.explicit(db), interior.source_order(db) + other_offset, ), (Node::Interior(interior), Node::AlwaysTrue | Node::AlwaysFalse) => Node::new( @@ -1269,7 +1259,6 @@ impl<'db> Node<'db> { interior.constraint(db), interior.if_true(db).iff_inner(db, other, other_offset), interior.if_false(db).iff_inner(db, other, other_offset), - interior.explicit(db), interior.source_order(db), ), (Node::Interior(a), Node::Interior(b)) => a.iff(db, b, other_offset), @@ -1595,18 +1584,8 @@ impl<'db> Node<'db> { // false // // (Note that the `else` branch shouldn't be reachable, but we have to provide something!) - let left_node = Node::new_satisfied_constraint( - db, - left, - ExplicitConstraint::Implicit, - left_source_order, - ); - let right_node = Node::new_satisfied_constraint( - db, - right, - ExplicitConstraint::Implicit, - right_source_order, - ); + let left_node = Node::new_satisfied_constraint(db, left, left_source_order); + let right_node = Node::new_satisfied_constraint(db, right, right_source_order); let right_result = right_node.ite(db, Node::AlwaysFalse, when_left_but_not_right); let left_result = left_node.ite(db, right_result, when_not_left); let result = replacement.ite(db, when_left_and_right, left_result); @@ -1671,18 +1650,8 @@ impl<'db> Node<'db> { // Lastly, verify that the result is consistent with the input. (It must produce the same // results when `left ∨ right`.) If it doesn't, the substitution isn't valid, and we should // return the original BDD unmodified. - let left_node = Node::new_satisfied_constraint( - db, - left, - ExplicitConstraint::Implicit, - left_source_order, - ); - let right_node = Node::new_satisfied_constraint( - db, - right, - ExplicitConstraint::Implicit, - right_source_order, - ); + let left_node = Node::new_satisfied_constraint(db, left, left_source_order); + let right_node = Node::new_satisfied_constraint(db, right, right_source_order); let validity = replacement.iff(db, left_node.or(db, right_node)); let constrained_original = self.and(db, validity); let constrained_replacement = result.and(db, validity); @@ -1837,11 +1806,12 @@ impl<'db> Node<'db> { Node::AlwaysTrue => write!(f, "always"), Node::AlwaysFalse => write!(f, "never"), Node::Interior(interior) => { + let constraint = interior.constraint(self.db); write!( f, "{} {:?} {}/{}", - interior.constraint(self.db).display(self.db), - interior.explicit(self.db), + constraint.display(self.db), + constraint.explicit(self.db), interior.source_order(self.db), interior.max_source_order(self.db), )?; @@ -1898,7 +1868,9 @@ impl<'db> RepresentativeBounds<'db> { } } -#[derive(Clone, Copy, Debug, Eq, PartialEq, Hash, get_size2::GetSize, salsa::Update)] +#[derive( + Clone, Copy, Debug, Eq, Hash, Ord, PartialEq, PartialOrd, get_size2::GetSize, salsa::Update, +)] pub(crate) enum ExplicitConstraint { Implicit, Explicit, @@ -1938,7 +1910,6 @@ struct InteriorNode<'db> { constraint: ConstrainedTypeVar<'db>, if_true: Node<'db>, if_false: Node<'db>, - explicit: ExplicitConstraint, /// Represents the order in which this node's constraint was added to the containing constraint /// set, relative to all of the other constraints in the set. This starts off at 1 for a simple @@ -1963,7 +1934,6 @@ impl<'db> InteriorNode<'db> { self.constraint(db), self.if_true(db).negate(db), self.if_false(db).negate(db), - self.explicit(db), self.source_order(db), ) } @@ -1980,7 +1950,6 @@ impl<'db> InteriorNode<'db> { .or_inner(db, other.if_true(db), other_offset), self.if_false(db) .or_inner(db, other.if_false(db), other_offset), - self.explicit(db) & other.explicit(db), self.source_order(db), ), Ordering::Less => Node::new( @@ -1990,7 +1959,6 @@ impl<'db> InteriorNode<'db> { .or_inner(db, Node::Interior(other), other_offset), self.if_false(db) .or_inner(db, Node::Interior(other), other_offset), - self.explicit(db), self.source_order(db), ), Ordering::Greater => Node::new( @@ -1998,7 +1966,6 @@ impl<'db> InteriorNode<'db> { other_constraint, Node::Interior(self).or_inner(db, other.if_true(db), other_offset), Node::Interior(self).or_inner(db, other.if_false(db), other_offset), - other.explicit(db), other.source_order(db) + other_offset, ), } @@ -2016,7 +1983,6 @@ impl<'db> InteriorNode<'db> { .and_inner(db, other.if_true(db), other_offset), self.if_false(db) .and_inner(db, other.if_false(db), other_offset), - self.explicit(db) & other.explicit(db), self.source_order(db), ), Ordering::Less => Node::new( @@ -2026,7 +1992,6 @@ impl<'db> InteriorNode<'db> { .and_inner(db, Node::Interior(other), other_offset), self.if_false(db) .and_inner(db, Node::Interior(other), other_offset), - self.explicit(db), self.source_order(db), ), Ordering::Greater => Node::new( @@ -2034,7 +1999,6 @@ impl<'db> InteriorNode<'db> { other_constraint, Node::Interior(self).and_inner(db, other.if_true(db), other_offset), Node::Interior(self).and_inner(db, other.if_false(db), other_offset), - other.explicit(db), other.source_order(db) + other_offset, ), } @@ -2052,7 +2016,6 @@ impl<'db> InteriorNode<'db> { .iff_inner(db, other.if_true(db), other_offset), self.if_false(db) .iff_inner(db, other.if_false(db), other_offset), - self.explicit(db) & other.explicit(db), self.source_order(db), ), Ordering::Less => Node::new( @@ -2062,7 +2025,6 @@ impl<'db> InteriorNode<'db> { .iff_inner(db, Node::Interior(other), other_offset), self.if_false(db) .iff_inner(db, Node::Interior(other), other_offset), - self.explicit(db), self.source_order(db), ), Ordering::Greater => Node::new( @@ -2070,7 +2032,6 @@ impl<'db> InteriorNode<'db> { other_constraint, Node::Interior(self).iff_inner(db, other.if_true(db), other_offset), Node::Interior(self).iff_inner(db, other.if_false(db), other_offset), - other.explicit(db), other.source_order(db) + other_offset, ), } @@ -2140,7 +2101,6 @@ impl<'db> InteriorNode<'db> { ) -> Node<'db> { let self_constraint = self.constraint(db); let self_source_order = self.source_order(db); - let self_explicit = self.explicit(db); if should_remove(self_constraint) { // If we should remove constraints involving this typevar, then we replace this node // with the OR of its if_false/if_true edges. That is, the result is true if there's @@ -2154,7 +2114,6 @@ impl<'db> InteriorNode<'db> { db, map, self_constraint.when_true(), - self_explicit, self_source_order, |path, new_range| { let branch = @@ -2167,15 +2126,10 @@ impl<'db> InteriorNode<'db> { // removed! !should_remove(assignment.constraint()) }) - .fold(branch, |branch, (assignment, (explicit, source_order))| { + .fold(branch, |branch, (assignment, source_order)| { branch.and( db, - Node::new_satisfied_constraint( - db, - *assignment, - *explicit, - *source_order, - ), + Node::new_satisfied_constraint(db, *assignment, *source_order), ) }) }, @@ -2186,7 +2140,6 @@ impl<'db> InteriorNode<'db> { db, map, self_constraint.when_false(), - self_explicit, self_source_order, |path, new_range| { let branch = @@ -2199,15 +2152,10 @@ impl<'db> InteriorNode<'db> { // removed! !should_remove(assignment.constraint()) }) - .fold(branch, |branch, (assignment, (explicit, source_order))| { + .fold(branch, |branch, (assignment, source_order)| { branch.and( db, - Node::new_satisfied_constraint( - db, - *assignment, - *explicit, - *source_order, - ), + Node::new_satisfied_constraint(db, *assignment, *source_order), ) }) }, @@ -2221,7 +2169,6 @@ impl<'db> InteriorNode<'db> { db, map, self_constraint.when_true(), - self_explicit, self_source_order, |path, _| { self.if_true(db) @@ -2234,7 +2181,6 @@ impl<'db> InteriorNode<'db> { db, map, self_constraint.when_false(), - self_explicit, self_source_order, |path, _| { self.if_false(db) @@ -2245,8 +2191,7 @@ impl<'db> InteriorNode<'db> { // NB: We cannot use `Node::new` here, because the recursive calls might introduce new // derived constraints into the result, and those constraints might appear before this // one in the BDD ordering. - Node::new_constraint(db, self_constraint, self_explicit, self_source_order) - .ite(db, if_true, if_false) + Node::new_constraint(db, self_constraint, self_source_order).ite(db, if_true, if_false) } } @@ -2279,7 +2224,6 @@ impl<'db> InteriorNode<'db> { self_constraint, if_true, if_false, - self.explicit(db), self.source_order(db), ), found_in_true || found_in_false, @@ -2410,28 +2354,26 @@ impl<'db> InteriorNode<'db> { _ => continue, }; - let new_constraint = - ConstrainedTypeVar::new(db, constrained_typevar, new_lower, new_upper); + let new_constraint = ConstrainedTypeVar::new( + db, + constrained_typevar, + new_lower, + new_upper, + ExplicitConstraint::Implicit, + ); if seen_constraints.contains(&new_constraint) { continue; } - let new_node = Node::new_constraint( - db, - new_constraint, - ExplicitConstraint::Implicit, - next_source_order, - ); + let new_node = Node::new_constraint(db, new_constraint, next_source_order); next_source_order += 1; let positive_left_node = Node::new_satisfied_constraint( db, left_constraint.when_true(), - ExplicitConstraint::Implicit, left_source_order, ); let positive_right_node = Node::new_satisfied_constraint( db, right_constraint.when_true(), - ExplicitConstraint::Implicit, right_source_order, ); let lhs = positive_left_node.and(db, positive_right_node); @@ -2482,13 +2424,11 @@ impl<'db> InteriorNode<'db> { let positive_larger_node = Node::new_satisfied_constraint( db, larger_constraint.when_true(), - ExplicitConstraint::Implicit, larger_source_order, ); let negative_larger_node = Node::new_satisfied_constraint( db, larger_constraint.when_false(), - ExplicitConstraint::Implicit, larger_source_order, ); @@ -2556,13 +2496,11 @@ impl<'db> InteriorNode<'db> { let positive_intersection_node = Node::new_satisfied_constraint( db, intersection_constraint.when_true(), - ExplicitConstraint::Implicit, next_source_order, ); let negative_intersection_node = Node::new_satisfied_constraint( db, intersection_constraint.when_false(), - ExplicitConstraint::Implicit, next_source_order, ); next_source_order += 1; @@ -2570,26 +2508,22 @@ impl<'db> InteriorNode<'db> { let positive_left_node = Node::new_satisfied_constraint( db, left_constraint.when_true(), - ExplicitConstraint::Implicit, left_source_order, ); let negative_left_node = Node::new_satisfied_constraint( db, left_constraint.when_false(), - ExplicitConstraint::Implicit, left_source_order, ); let positive_right_node = Node::new_satisfied_constraint( db, right_constraint.when_true(), - ExplicitConstraint::Implicit, right_source_order, ); let negative_right_node = Node::new_satisfied_constraint( db, right_constraint.when_false(), - ExplicitConstraint::Implicit, right_source_order, ); @@ -2671,13 +2605,11 @@ impl<'db> InteriorNode<'db> { let positive_left_node = Node::new_satisfied_constraint( db, left_constraint.when_true(), - ExplicitConstraint::Implicit, left_source_order, ); let positive_right_node = Node::new_satisfied_constraint( db, right_constraint.when_true(), - ExplicitConstraint::Implicit, right_source_order, ); @@ -3051,21 +2983,35 @@ impl<'db> SequentMap<'db> { // Case 1 (Type::TypeVar(lower_typevar), Type::TypeVar(upper_typevar)) => { if !lower_typevar.is_same_typevar_as(db, upper_typevar) { - ConstrainedTypeVar::new(db, lower_typevar, Type::Never, upper) + ConstrainedTypeVar::new( + db, + lower_typevar, + Type::Never, + upper, + constraint.explicit(db), + ) } else { return; } } // Case 2 - (Type::TypeVar(lower_typevar), _) => { - ConstrainedTypeVar::new(db, lower_typevar, Type::Never, upper) - } + (Type::TypeVar(lower_typevar), _) => ConstrainedTypeVar::new( + db, + lower_typevar, + Type::Never, + upper, + constraint.explicit(db), + ), // Case 3 - (_, Type::TypeVar(upper_typevar)) => { - ConstrainedTypeVar::new(db, upper_typevar, lower, Type::object()) - } + (_, Type::TypeVar(upper_typevar)) => ConstrainedTypeVar::new( + db, + upper_typevar, + lower, + Type::object(), + constraint.explicit(db), + ), _ => return, }; @@ -3179,8 +3125,13 @@ impl<'db> SequentMap<'db> { _ => return, }; - let post_constraint = - ConstrainedTypeVar::new(db, constrained_typevar, new_lower, new_upper); + let post_constraint = ConstrainedTypeVar::new( + db, + constrained_typevar, + new_lower, + new_upper, + left_constraint.explicit(db) & right_constraint.explicit(db), + ); self.add_pair_implication(db, left_constraint, right_constraint, post_constraint); self.enqueue_constraint(post_constraint); } @@ -3202,14 +3153,28 @@ impl<'db> SequentMap<'db> { (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()) + ConstrainedTypeVar::new( + db, + bound_typevar, + right_lower, + right_upper, + left_constraint.explicit(db) & right_constraint.explicit(db), + ) } + (Type::TypeVar(bound_typevar), _) => ConstrainedTypeVar::new( + db, + bound_typevar, + Type::Never, + right_upper, + left_constraint.explicit(db) & right_constraint.explicit(db), + ), + (_, Type::TypeVar(bound_typevar)) => ConstrainedTypeVar::new( + db, + bound_typevar, + right_lower, + Type::object(), + left_constraint.explicit(db) & right_constraint.explicit(db), + ), _ => return, }; self.add_pair_implication(db, left_constraint, right_constraint, post_constraint); @@ -3356,7 +3321,7 @@ impl<'db> SequentMap<'db> { /// traversing a BDD. #[derive(Debug, Default)] pub(crate) struct PathAssignments<'db> { - assignments: FxOrderMap, (ExplicitConstraint, usize)>, + assignments: FxOrderMap, usize>, } impl<'db> PathAssignments<'db> { @@ -3387,7 +3352,6 @@ impl<'db> PathAssignments<'db> { db: &'db dyn Db, map: &SequentMap<'db>, assignment: ConstraintAssignment<'db>, - explicit: ExplicitConstraint, source_order: usize, f: impl FnOnce(&mut Self, Range) -> R, ) -> Option { @@ -3406,7 +3370,7 @@ impl<'db> PathAssignments<'db> { edge = %assignment.display(db), "walk edge", ); - let found_conflict = self.add_assignment(db, map, assignment, explicit, source_order); + let found_conflict = self.add_assignment(db, map, assignment, source_order); let result = if found_conflict.is_err() { // If that results in the path now being impossible due to a contradiction, return // without invoking the callback. @@ -3439,15 +3403,6 @@ impl<'db> PathAssignments<'db> { self.assignments.contains_key(&assignment) } - fn assignment_holds_explicitly( - &self, - assignment: ConstraintAssignment<'db>, - ) -> Option { - self.assignments - .get(&assignment) - .map(|(explicit, _)| *explicit) - } - /// 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. @@ -3456,7 +3411,6 @@ impl<'db> PathAssignments<'db> { db: &'db dyn Db, map: &SequentMap<'db>, assignment: ConstraintAssignment<'db>, - explicit: ExplicitConstraint, source_order: usize, ) -> Result<(), PathAssignmentConflict> { // First add this assignment. If it causes a conflict, return that as an error. If we've @@ -3473,11 +3427,7 @@ impl<'db> PathAssignments<'db> { ); return Err(PathAssignmentConflict); } - if self - .assignments - .insert(assignment, (explicit, source_order)) - .is_some() - { + if self.assignments.insert(assignment, source_order).is_some() { return Ok(()); } @@ -3531,31 +3481,18 @@ impl<'db> PathAssignments<'db> { for ((ante1, ante2), posts) in &map.pair_implications { for post in posts { - if let Some(ante1_explicit) = self.assignment_holds_explicitly(ante1.when_true()) - && let Some(ante2_explicit) = - self.assignment_holds_explicitly(ante2.when_true()) + if self.assignment_holds(ante1.when_true()) + && self.assignment_holds(ante2.when_true()) { - self.add_assignment( - db, - map, - post.when_true(), - explicit & ante1_explicit & ante2_explicit, - source_order, - )?; + self.add_assignment(db, map, post.when_true(), source_order)?; } } } for (ante, posts) in &map.single_implications { for post in posts { - if let Some(ante_explicit) = self.assignment_holds_explicitly(ante.when_true()) { - self.add_assignment( - db, - map, - post.when_true(), - explicit & ante_explicit, - source_order, - )?; + if self.assignment_holds(ante.when_true()) { + self.add_assignment(db, map, post.when_true(), source_order)?; } } } From 7f7fb50a436b261ad1c313f1700fda7fcb06fb1d Mon Sep 17 00:00:00 2001 From: Carl Meyer Date: Mon, 15 Dec 2025 18:06:47 -0800 Subject: [PATCH 5/5] update expected output for graph display test --- .../src/types/constraints.rs | 24 +++++++++---------- 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs index 8382168dba..d60353d67e 100644 --- a/crates/ty_python_semantic/src/types/constraints.rs +++ b/crates/ty_python_semantic/src/types/constraints.rs @@ -3992,28 +3992,28 @@ mod tests { #[test] fn test_display_graph_output() { let expected = indoc! {r#" - (T = str) 3/4 - ┡━₁ (T = bool) 4/4 - │ ┡━₁ (U = str) 1/2 - │ │ ┡━₁ (U = bool) 2/2 + (T = str) Explicit 3/4 + ┡━₁ (T = bool) Explicit 4/4 + │ ┡━₁ (U = str) Explicit 1/2 + │ │ ┡━₁ (U = bool) Explicit 2/2 │ │ │ ┡━₁ always │ │ │ └─₀ always - │ │ └─₀ (U = bool) 2/2 + │ │ └─₀ (U = bool) Explicit 2/2 │ │ ┡━₁ always │ │ └─₀ never - │ └─₀ (U = str) 1/2 - │ ┡━₁ (U = bool) 2/2 + │ └─₀ (U = str) Explicit 1/2 + │ ┡━₁ (U = bool) Explicit 2/2 │ │ ┡━₁ always │ │ └─₀ always - │ └─₀ (U = bool) 2/2 + │ └─₀ (U = bool) Explicit 2/2 │ ┡━₁ always │ └─₀ never - └─₀ (T = bool) 4/4 - ┡━₁ (U = str) 1/2 - │ ┡━₁ (U = bool) 2/2 + └─₀ (T = bool) Explicit 4/4 + ┡━₁ (U = str) Explicit 1/2 + │ ┡━₁ (U = bool) Explicit 2/2 │ │ ┡━₁ always │ │ └─₀ always - │ └─₀ (U = bool) 2/2 + │ └─₀ (U = bool) Explicit 2/2 │ ┡━₁ always │ └─₀ never └─₀ never