Skip to content

[ty] Fix non-determinism in ConstraintSet.specialize_constrained #21744

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
dcreager merged 11 commits into from
Dec 3, 2025
Merged

[ty] Fix non-determinism in ConstraintSet.specialize_constrained #21744

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
11 commits
Select commit Hold shift + click to select a range
5300d11
add failing test
dcreager Dec 1, 2025
8086805
add sequent map tracing
dcreager Dec 1, 2025
80bf666
add tracing for PathAssignment
dcreager Dec 1, 2025
89cec13
quasi-reduced
dcreager Dec 1, 2025
c53f7bc
update docs
dcreager Dec 1, 2025
32d2f40
don't worry about display impl
dcreager Dec 1, 2025
4bed171
document tracing
dcreager Dec 1, 2025
d3d1bc1
clippy
dcreager Dec 1, 2025
9e5ea4b
fix test
dcreager Dec 1, 2025
e432558
Merge remote-tracking branch 'origin/main' into dcreager/nondeterminism
dcreager Dec 3, 2025
948a9fb
mark this TODO
dcreager Dec 3, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
29 changes: 27 additions & 2 deletions crates/ty_python_semantic/resources/mdtest/generics/specialize_constrained.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -41,7 +41,8 @@ def unbounded[T]():
# revealed: None
reveal_type(generic_context(unbounded).specialize_constrained(ConstraintSet.range(bool, T, bool) & ConstraintSet.range(Never, T, str)))

# revealed: ty_extensions.Specialization[T@unbounded = int]
# TODO: revealed: ty_extensions.Specialization[T@unbounded = int]
# revealed: ty_extensions.Specialization[T@unbounded = bool]
Copy link
Member Author

@dcreager dcreager Dec 2, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think this test (and the other changed one below) were other possible points of nondeterminism, since the result could depend on whether T ≤ bool was kept in the BDD or simplified away as described in the PR body.

Copy link
Contributor

@carljm carljm Dec 3, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm not sure I understand why we solve this to bool. The constraints are T <= int | T <= bool, which seems equivalent to T <= int. Why do we prefer solving to bool when there's the additional (seemingly redundant) constraint present?

Copy link
Member Author

@dcreager dcreager Dec 3, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is because of our current heuristic for handling multiple paths in a BDD. T ≤ int ∨ T ≤ bool ends up looking like this now:

(T ≤ int)
┡━₁ (T ≤ bool)
│   ┡━₁ true
│   └─₀ true
└─₀ (T ≤ bool)
    ┡━₁ impossible
    └─₀ false

There are two paths to the true terminal, one representing T ≤ bool and one representing bool < T ≤ int. T = bool and T = int are the largest types that satisfy each respective path. Our current heuristic says that if there's a type that satisfies all paths, we choose that. (That is, if the intersection of the specializations is non-empty, use it.)

I'm very much open to changing that heuristic, but think that should be follow-on work. I'll mark this as a TODO that we'd rather produce T = int here.

reveal_type(generic_context(unbounded).specialize_constrained(ConstraintSet.range(Never, T, int) | ConstraintSet.range(Never, T, bool)))
# revealed: ty_extensions.Specialization[T@unbounded = Never]
reveal_type(generic_context(unbounded).specialize_constrained(ConstraintSet.range(Never, T, int) | ConstraintSet.range(Never, T, str)))
Expand Down Expand Up @@ -175,7 +176,7 @@ def constrained_by_gradual[T: (Base, Any)]():
# revealed: ty_extensions.Specialization[T@constrained_by_gradual = Base]
reveal_type(generic_context(constrained_by_gradual).specialize_constrained(ConstraintSet.always()))
# TODO: revealed: ty_extensions.Specialization[T@constrained_by_gradual = Any]
# revealed: ty_extensions.Specialization[T@constrained_by_gradual = object]
# revealed: ty_extensions.Specialization[T@constrained_by_gradual = Base]
reveal_type(generic_context(constrained_by_gradual).specialize_constrained(ConstraintSet.range(Never, T, object)))
# revealed: None
reveal_type(generic_context(constrained_by_gradual).specialize_constrained(ConstraintSet.never()))
Expand Down Expand Up @@ -251,6 +252,30 @@ def constrained_by_gradual_list[T: (list[Base], list[Any])]():
# revealed: ty_extensions.Specialization[T@constrained_by_gradual_list = list[Sub]]
reveal_type(generic_context(constrained_by_gradual_list).specialize_constrained(ConstraintSet.range(list[Sub], T, list[Sub])))

# Same tests as above, but with the typevar constraints in a different order, to make sure the
# results do not depend on our BDD variable ordering.
def constrained_by_gradual_list_reverse[T: (list[Any], list[Base])]():
Comment on lines +255 to +257
Copy link
Member Author

@dcreager dcreager Dec 2, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This test failed before these fixes, reproducing the test failure in the macOS CI job

# revealed: ty_extensions.Specialization[T@constrained_by_gradual_list_reverse = list[Base]]
reveal_type(generic_context(constrained_by_gradual_list_reverse).specialize_constrained(ConstraintSet.always()))
# revealed: None
reveal_type(generic_context(constrained_by_gradual_list_reverse).specialize_constrained(ConstraintSet.never()))

# revealed: ty_extensions.Specialization[T@constrained_by_gradual_list_reverse = list[Base]]
reveal_type(generic_context(constrained_by_gradual_list_reverse).specialize_constrained(ConstraintSet.range(Never, T, list[Base])))
# TODO: revealed: ty_extensions.Specialization[T@constrained_by_gradual = list[Any]]
# revealed: ty_extensions.Specialization[T@constrained_by_gradual_list_reverse = list[Unrelated]]
reveal_type(generic_context(constrained_by_gradual_list_reverse).specialize_constrained(ConstraintSet.range(Never, T, list[Unrelated])))

# TODO: revealed: ty_extensions.Specialization[T@constrained_by_gradual = list[Any]]
# revealed: ty_extensions.Specialization[T@constrained_by_gradual_list_reverse = list[Super]]
reveal_type(generic_context(constrained_by_gradual_list_reverse).specialize_constrained(ConstraintSet.range(Never, T, list[Super])))
# TODO: revealed: ty_extensions.Specialization[T@constrained_by_gradual = list[Any]]
# revealed: ty_extensions.Specialization[T@constrained_by_gradual_list_reverse = list[Super]]
reveal_type(generic_context(constrained_by_gradual_list_reverse).specialize_constrained(ConstraintSet.range(list[Super], T, list[Super])))
# TODO: revealed: ty_extensions.Specialization[T@constrained_by_gradual = list[Any]]
# revealed: ty_extensions.Specialization[T@constrained_by_gradual_list_reverse = list[Sub]]
reveal_type(generic_context(constrained_by_gradual_list_reverse).specialize_constrained(ConstraintSet.range(list[Sub], T, list[Sub])))

def constrained_by_two_gradual_lists[T: (list[Any], list[Any])]():
# TODO: revealed: ty_extensions.Specialization[T@constrained_by_gradual = list[Any]]
# revealed: ty_extensions.Specialization[T@constrained_by_two_gradual_lists = Top[list[Any]]]
Expand Down
Loading
Loading