[ty] Add new "constraint implication" typing relation #21010

dcreager · 2025-10-21T01:54:25Z

This PR adds the new constraint implication relationship between types, aka is_subtype_of_given, which tests whether one type is a subtype of another assuming that the constraints in a particular constraint set hold.

For concrete types, constraint implication is exactly the same as subtyping. (A concrete type is any fully static type that is not a typevar. It can contain a typevar, though — list[T] is considered concrete.)

The interesting case is typevars. The other typing relationships (TODO: will) all "punt" on the question when considering a typevar, by translating the desired relationship into a constraint set. At some point, though, we need to resolve a constraint set; at that point, we can no longer punt on the question. Unlike with concrete types, the answer will depend on the constraint set that we are considering.

github-actions · 2025-10-21T01:56:35Z

Diagnostic diff on typing conformance tests

No changes detected when running ty on typing conformance tests ✅

github-actions · 2025-10-21T01:57:48Z

`mypy_primer` results

No ecosystem changes detected ✅
No memory usage changes detected ✅

dcreager · 2025-10-23T19:42:17Z

crates/ty_python_semantic/src/types.rs

I had originally written this as a new TypeRelation variant, but that was too heavy-handed, given that constraint implication is exactly the same as subtyping for everything except for typevars.

This reverts commit 8cecafc.

This reverts commit 943a7b3.

dcreager · 2025-10-24T17:48:23Z

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

+The interesting case is typevars. The other typing relationships (TODO: will) all "punt" on the
+question when considering a typevar, by translating the desired relationship into a constraint set.


This TODO is #20093

dcreager · 2025-10-24T17:50:11Z

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

+    static_assert(is_subtype_of_given(given_str, T, str))
+```
+
+This might require propagating constraints from other typevars.


This will be involved enough that I'm tackling it separately, in #21068

dcreager · 2025-10-24T17:52:34Z

crates/ty_python_semantic/src/types.rs

 /// A type variable that has been bound to a generic context, and which can be specialized to a
 /// concrete type.
 #[salsa::interned(debug, heap_size=ruff_memory_usage::heap_size)]
-#[derive(PartialOrd, Ord)]


We should always be comparing a typevar's identity, and this makes it harder to accidentally compare specific instances of a typevar.

crates/ty_python_semantic/src/types/type_ordering.rs

MichaReiser · 2025-10-27T09:33:42Z

crates/ty_vendored/ty_extensions/ty_extensions.pyi

+def is_subtype_of_given(
+    constraints: bool | ConstraintSet, ty: Any, of: Any
+) -> ConstraintSet:
+    """Returns a constraint set that is satisfied when `ty` is a `subtype`_ of `of`,
+    assuming that all of the constraints in `constraints` hold.


I just wanted to suggest making this a method on ConstraintSet but that doesn't work because you also want to allow bool as constraints.

I'm not sure I fully understand the semantics here. Is this roughly if and only if constraints semantics? If that's the case, I think I'd find is_subtype_of_iff(ty, of, constraints) easier to understand.

But I don't think that's what this API does after reading the mdtests. Hmm :)

I'm asking because I first assumed the relation between is_subtype_of and is_subtype_of_given is similar to std::mem::size_of and std::mem::size_of_val where the latter takes a value. I don't think this is the case here because constraints would than have to be a subtype of ty, which the API doesn't require.

I just wanted to suggest making this a method on ConstraintSet but that doesn't work because you also want to allow bool as constraints.

Yeah, I thought the same thing, but our KnownFunction machinery is focused on top-level functions in a module. I had considered adding support for "known methods of a class", but that seemed like it would be out of scope for this PR. I can open an issue to track that.

I'm not sure I fully understand the semantics here. Is this roughly if and only if constraints semantics? If that's the case, I think I'd find is_subtype_of_iff(ty, of, constraints) easier to understand.

I can copy over more of the commentary from the mdtest to explain the method better.

Done. I put the expanded documentation on the Rust side, to be consistent with where we are documenting the other typing internals.

Yeah, I thought the same thing, but our KnownFunction machinery is focused on top-level functions in a module. I had considered adding support for "known methods of a class", but that seemed like it would be out of scope for this PR. I can open an issue to track that.

astral-sh/ty#1447

MichaReiser · 2025-10-27T09:35:27Z

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

+    static_assert(not is_subtype_of(bool, str))
+    static_assert(not is_subtype_of_given(True, bool, str))


Is is_subtype_of(T, V) guaranteed to always be the same as is_subtype_of(True, T, V). If so, maybe that's something you could add to the documentation of is_subtype_of_given

This is a great catch! I was in the middle of writing that this would not be true when comparing typevars — but you're right, and it is true even then:

is_subtype_of(bool, int) # yes is_subtype_of_given(True, bool, int) # yes is_subtype_of_given(False, bool, int) # yes def f[T](): is_subtype_of(T, int) # no (T could be anything!) is_subtype_of_given(True, T, int) # also no (T could be anything!)

This also made me realize that I don't need to (and shouldn't) project away the other typevars like I was doing.

crates/ty_python_semantic/src/types.rs

MichaReiser · 2025-10-27T09:41:59Z

crates/ty_python_semantic/src/types/constraints.rs

+        relation: TypeRelation,
+    ) -> Self {
+        let (lower, upper) = match relation {
+            // TODO: Is this the correct constraint for redundancy?


@AlexWaygood do you have thoughts here? I was thinking that we should treat redundancy the same as subtyping here. Adding more context, the question is, if you call is_redundant_with(T, list[Any]), what constraint should we turn that into? For is_subtype_of(T, list[Any]), we turn it into T ≤ Bottom[list[Any]], since for subtyping, the relationship has to hold for all materializations. For is_assignable_to(T, list[Any]), we turn it into T ≤ Top[list[Any]], since the relationship only has to hold for some materialization.

Happy to take a look at this, but might not get to it until Wednesday as I'm busy travelling tomorrow. Don't feel you have to wait for me before merging!

In general, if we're in doubt about how redundancy should behave, the safe thing to do in that situation is always to treat it like subtyping

Thanks! This isn't hooked up to anything yet except isolated mdtests, so no urgency.

(But I will still probably merge this and address anything you might find in a follow-on PR)

crates/ty_python_semantic/src/types/constraints.rs

crates/ty_python_semantic/src/types/type_ordering.rs

* origin/main: Respect `--output-format` with `--watch` (#21097) [`pyflakes`] Revert to stable behavior if imports for module lie in alternate branches for `F401` (#20878) Fix finding keyword range for clause header after statement ending with semicolon (#21067) [ty] Fix bug where ty would think all types had an `__mro__` attribute (#20995) Restore `indent.py` (#21094) [`flake8-django`] Apply `DJ001` to annotated fields (#20907) Clearer error message when `line-length` goes beyond threshold (#21072) Update upload and download artifacts github actions (#21083) Update dependency mdformat-mkdocs to v4.4.2 (#21088) Update cargo-bins/cargo-binstall action to v1.15.9 (#21086) Update Rust crate clap to v4.5.50 (#21090) Update Rust crate get-size2 to v0.7.1 (#21091) Update Rust crate bstr to v1.12.1 (#21089) Add missing docstring sections to the numpy list (#20931) [`pydoclint`] Fix false positive on explicit exception re-raising (`DOC501`, `DOC502`) (#21011) [ty] Use constructor parameter types as type context (#21054)

…l-constraint-sets * dcreager/refactor-constraint-mdtests: (60 commits) add static_asserts move all reveal diagnostics to separate line add more gradual tests better comment restructure a bit better names/comments simplify before implication two typevars! mdformat rename mdtest move is_subtype_of_given into ConstraintSet move where we grab these add ConstraintSet.{always,never} move range_constraint into ConstraintSet class [ty] Rename `inner` query for better debugging experience (#21106) [ty] Add new "constraint implication" typing relation (#21010) [semantic error tests]: refactor semantic error tests to separate files (#20926) Respect `--output-format` with `--watch` (#21097) [`pyflakes`] Revert to stable behavior if imports for module lie in alternate branches for `F401` (#20878) Fix finding keyword range for clause header after statement ending with semicolon (#21067) ...

…between two typevars (#21068) It's possible for a constraint to mention two typevars. For instance, in the body of ```py def f[S: int, T: S](): ... ``` the baseline constraint set would be `(T ≤ S) ∧ (S ≤ int)`. That is, `S` must specialize to some subtype of `int`, and `T` must specialize to a subtype of the type that `S` specializes to. This PR updates the new "constraint implication" relationship from #21010 to work on these kinds of constraint sets. For instance, in the example above, we should be able to see that `T ≤ int` must always hold: ```py def f[S, T](): constraints = ConstraintSet.range(Never, S, int) & ConstraintSet.range(Never, T, S) static_assert(constraints.implies_subtype_of(T, int)) # now succeeds! ``` This did not require major changes to the implementation of `implies_subtype_of`. That method already relies on how our `simplify` and `domain` methods expand a constraint set to include the transitive closure of the constraints that it mentions, and to mark certain combinations of constraints as impossible. Previously, that transitive closure logic only looked at pairs of constraints that constrain the same typevar. (For instance, to notice that `(T ≤ bool) ∧ ¬(T ≤ int)` is impossible.) Now we also look at pairs of constraints that constraint different typevars, if one of the constraints is bound by the other — that is, pairs of the form `T ≤ S` and `S ≤ something`, or `S ≤ T` and `something ≤ S`. In those cases, transitivity lets us add a new derived constraint that `T ≤ something` or `something ≤ T`, respectively. Having done that, our existing `implies_subtype_of` logic finds and takes into account that derived constraint.

dcreager added ty Multi-file analysis & type inference internal An internal refactor or improvement labels Oct 21, 2025

dcreager force-pushed the dcreager/constraint-display branch from 4c937b5 to 671582a Compare October 21, 2025 13:56

dcreager force-pushed the dcreager/new-relation branch 2 times, most recently from e3803a5 to 0827f40 Compare October 21, 2025 20:55

Base automatically changed from dcreager/constraint-display to main October 22, 2025 17:39

dcreager force-pushed the dcreager/new-relation branch 2 times, most recently from 9d07e4d to 86f2b08 Compare October 23, 2025 19:14

dcreager changed the base branch from main to dcreager/simplify October 23, 2025 19:15

dcreager commented Oct 23, 2025

View reviewed changes

dcreager force-pushed the dcreager/new-relation branch from 1b9e4f5 to af813e7 Compare October 23, 2025 22:50

Base automatically changed from dcreager/simplify to main October 24, 2025 17:37

dcreager added 16 commits October 24, 2025 13:40

constraint implication

f27ee34

this is a todo for now

4172baa

add tests for constraint implication

73ec885

this should check the constraints too

b4468d8

construct constraints with typevars in fixed order

f3c699c

mdformat

8954ae1

this has to be instance after all

d923bec

render equivalences consistently too

ed1d05c

check relation in match patterns

f86f271

check constraint implication by updating BDD

9cf299b

Revert "check relation in match patterns"

f1074e4

This reverts commit 8cecafc.

Revert "constraint implication"

73539e0

This reverts commit 943a7b3.

fix the build

d58674c

implies, not and

f9e2d58

these tests pass now!

a4d0f67

rename

e061f04

dcreager added 6 commits October 24, 2025 13:40

refactor a bit

e741e8d

refactor this too

a6db701

and not implies

0a45929

no given in display

6e3a561

remove ord from BoundTypeVarInstance

89ab773

whoops

3c7950c

dcreager force-pushed the dcreager/new-relation branch from ab271f0 to 3c7950c Compare October 24, 2025 17:44

dcreager mentioned this pull request Oct 24, 2025

[ty] Update "constraint implication" relation to work on constraints between two typevars #21068

Merged

dcreager commented Oct 24, 2025

View reviewed changes

use opposite order

8a2573a

dcreager marked this pull request as ready for review October 24, 2025 18:19

dcreager requested review from AlexWaygood, MichaReiser, carljm and sharkdp as code owners October 24, 2025 18:19

dcreager added 2 commits October 24, 2025 15:24

project instance

67a6c31

is_same_typevar_as

e17dd92

MichaReiser approved these changes Oct 27, 2025

View reviewed changes

dcreager added 7 commits October 27, 2025 15:02

don't need to project after all

18f1d42

is_same_typevar_as

8779dae

document special case

14b636a

rename params

f42cf93

more tests

0395ae9

document better

362658b

dcreager mentioned this pull request Oct 27, 2025

Extend KnownFunction machinery to work with class methods astral-sh/ty#1447

Closed

dcreager merged commit 29462ea into main Oct 28, 2025
41 checks passed

dcreager deleted the dcreager/new-relation branch October 28, 2025 02:01

		The interesting case is typevars. The other typing relationships (TODO: will) all "punt" on the
		question when considering a typevar, by translating the desired relationship into a constraint set.

		static_assert(not is_subtype_of(bool, str))
		static_assert(not is_subtype_of_given(True, bool, str))

[ty] Add new "constraint implication" typing relation #21010

[ty] Add new "constraint implication" typing relation #21010

Uh oh!

Conversation

dcreager commented Oct 21, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Oct 21, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Diagnostic diff on typing conformance tests

Uh oh!

github-actions bot commented Oct 21, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

mypy_primer results

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

dcreager Oct 27, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

dcreager commented Oct 21, 2025 •

edited

Loading

github-actions bot commented Oct 21, 2025 •

edited

Loading

github-actions bot commented Oct 21, 2025 •

edited

Loading

`mypy_primer` results

dcreager Oct 27, 2025 •

edited

Loading