-
Notifications
You must be signed in to change notification settings - Fork 1.6k
[ty] Constraint sets compare generic callables correctly #21392
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.
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
Conversation
This reverts commit 4cea4de.
Diagnostic diff on typing conformance testsNo changes detected when running ty on typing conformance tests ✅ |
|
CodSpeed Performance ReportMerging #21392 will not alter performanceComparing Summary
Footnotes
|
carljm
left a comment
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Nice!
| # TODO: no error | ||
| # error: [static-assert-error] | ||
| static_assert(not constraints.implies_subtype_of(TypeOf[identity2], Callable[[str], int])) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This seems like a significant issue -- is there a next step / plan for how to fix this TODO?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
We will need to alpha-rename the typevars that we add to the inferable set when checking generic signatures. I'll add a TODO
| static_assert(is_assignable_to(TypeOf[identity], Callable[[int], int])) | ||
| static_assert(is_assignable_to(TypeOf[identity], Callable[[str], str])) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Hmm, why do we do better in these tests than in the subtype-of tests below? I don't see any gradual forms, so I would think they should have the same results.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It's because of these lines:
ruff/crates/ty_python_semantic/src/types.rs
Lines 2042 to 2045 in 9269d9a
| (_, Type::TypeVar(typevar)) | |
| if typevar.is_inferable(db, inferable) | |
| && relation.is_assignability() | |
| && typevar.typevar(db).upper_bound(db).is_none_or(|bound| { |
I can remove the is_assignable part of the test, and it does cause the subtype checks to line up with the assignability checks here. But it causes other tests to start failing, because this interacts poorly with the union specialization heuristics here:
ruff/crates/ty_python_semantic/src/types/generics.rs
Lines 1445 to 1455 in 9269d9a
| (Type::Union(formal), _) => { | |
| // Second, if the formal is a union, and precisely one union element is assignable | |
| // from the actual type, then we don't add any type mapping. This handles a case like | |
| // | |
| // ```py | |
| // def f[T](t: T | None): ... | |
| // | |
| // f(None) | |
| // ``` | |
| // | |
| // without specializing `T` to `None`. |
Did I mention that the current setup is very brittle? 😅
I can add a TODO in the code and here calling out that this is a known inconsistency we're working towards removing
crates/ty_python_semantic/resources/mdtest/type_properties/is_subtype_of.md
Show resolved
Hide resolved
| // The typevars in self and other should also be considered inferable when checking whether | ||
| // two signatures are equivalent. | ||
| let self_inferable = | ||
| (self.generic_context).map(|generic_context| generic_context.inferable_typevars(db)); | ||
| let other_inferable = | ||
| (other.generic_context).map(|generic_context| generic_context.inferable_typevars(db)); | ||
| let inferable = inferable.merge(self_inferable.as_ref()); | ||
| let inferable = inferable.merge(other_inferable.as_ref()); | ||
|
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Was this just wrong? Or unnecessary
I don't see any new/changed tests above regarding equivalence of callables, but apparently removing this doesn't break any tests?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Bad copy/pasta. I did at one point think that we only needed to force-to-inferable the typevars of one side of the callable comparison, thinking we needed that to handle a co/contravariance thing. But that's already being handled correctly by how we perform the recursive subtyping calls below, so I think it's correct to mark both sides as inferable. (This is a mumbly explanation since much of that detail has paged out of my memory at this point)
But in the world where that hunch was correct, then we wouldn't do any force-to-inferable marking here, because if we only mark one side in has_relation_to, and is_equivalent_to is akin to has_relation_to in both directions, then neither side is always forced-to-inferable. (That inconsistency was another hint that made me think my first hunch was wrong.)
Co-authored-by: David Peter <sharkdp@users.noreply.github.com>
* origin/main: (59 commits) [ty] Improve diagnostic range for `non-subscriptable` diagnostics (#21461) [ty] Improve literal promotion heuristics (#21439) [ty] Further improve details around which expressions should be deferred in stub files (#21456) [ty] Improve generic class constructor inference (#21442) [ty] Propagate type context through conditional expressions (#21443) [ty] Suppress completions when introducing names with `as` [ty] Add panic-by-default await methods to `TestServer` (#21451) [ty] name is parameter and global is a syntax error (#21312) [ty] Fixup a few details around version-specific dataclass features (#21453) [ty] Support attribute-expression `TYPE_CHECKING` conditionals (#21449) [ty] Support stringified annotations in value-position `Annotated` instances (#21447) [ty] Type inference for genererator expressions (#21437) [ty] Make `__getattr__` available for `ModuleType` instances (#21450) [ty] Increase default receive timeout in tests to 10s (#21448) [ty] Add synthetic members to completions on dataclasses (#21446) [ty] Support legacy `typing` special forms in implicit type aliases (#21433) Bump 0.14.5 (#21435) [ty] Support `type[…]` and `Type[…]` in implicit type aliases (#21421) [ty] Respect notebook cell boundaries when adding an auto import (#21322) Update PyCharm setup instructions (#21409) ...
* dcreager/deep-comparison: (64 commits) assuming SubtypingAssuming implies_subtype_of name tweak Apply suggestions from code review [ty] Improve diagnostic range for `non-subscriptable` diagnostics (#21461) [ty] Improve literal promotion heuristics (#21439) [ty] Further improve details around which expressions should be deferred in stub files (#21456) [ty] Improve generic class constructor inference (#21442) [ty] Propagate type context through conditional expressions (#21443) [ty] Suppress completions when introducing names with `as` [ty] Add panic-by-default await methods to `TestServer` (#21451) [ty] name is parameter and global is a syntax error (#21312) [ty] Fixup a few details around version-specific dataclass features (#21453) [ty] Support attribute-expression `TYPE_CHECKING` conditionals (#21449) [ty] Support stringified annotations in value-position `Annotated` instances (#21447) [ty] Type inference for genererator expressions (#21437) [ty] Make `__getattr__` available for `ModuleType` instances (#21450) [ty] Increase default receive timeout in tests to 10s (#21448) [ty] Add synthetic members to completions on dataclasses (#21446) ...
* origin/main: [ty] Implement constraint implication for compound types (#21366)
| static_assert(constraints.implies_subtype_of(CallableTypeOf[identity], Callable[[int], int])) | ||
| static_assert(constraints.implies_subtype_of(CallableTypeOf[identity], Callable[[str], str])) | ||
| static_assert(not constraints.implies_subtype_of(CallableTypeOf[identity], Callable[[str], int])) | ||
| ``` |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I tried to see if tests like the following would pass here …
type GenericIdentity[T] = Callable[[T], T]
type GenericFunction[T, R] = Callable[[T], R]
static_assert(constraints.implies_subtype_of(TypeOf[identity], GenericIdentity))
static_assert(constraints.implies_subtype_of(CallableTypeOf[identity], GenericFunction))… but I get a panic due to a failing debug assertion
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I traced this a bit, and the issue is that type_alias.value_type is returning a dynamic callable for these type aliases. I think that's a separate issue from this PR, though I will add some logic here to make this not cause a panic!
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
If you do
static_assert(constraints.implies_subtype_of(TypeOf[identity], GenericIdentity[int]))the test passes. value_type is eagerly specializing the type alias to GenericIdentity[Unknown]. So other than the panic, this might be the correct expected behavior?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think it is correct/expected that a not-explicitly-specialized use of a generic type alias in a type expression is implicitly default-specialized.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Fixed the panic and added these as additional tests
* main: [ty] Constraint sets compare generic callables correctly (#21392)
Constraint sets can now track subtyping/assignability/etc of generic callables correctly. For instance:
A generic callable can be considered an intersection of all of its possible specializations, and an assignability check with an intersection as the lhs side succeeds of any of the intersected types satisfies the check. Put another way, if someone expects to receive any function with a signature of
(int) -> int, we can give themidentity.Note that the corresponding check using
is_subtype_ofdirectly does not yet work, since #20093 has not yet hooked up the core typing relationship logic to use constraint sets:To do this, we add a new existential quantification operation on constraint sets. This takes in a list of typevars and removes those typevars from the constraint set. Conceptually, we return a new constraint set that evaluates to
truewhen there was any assignment of the removed typevars that caused the old constraint set to evaluate totrue.When comparing a generic constraint set, we add its typevars to the
inferableset, and figure out whatever constraints would allow any specialization to satisfy the check. We then use the new existential quantification operator to remove those new typevars, since the caller doesn't (and shouldn't) know anything about them.