-
Notifications
You must be signed in to change notification settings - Fork 1.6k
[ty] WIP: handle recursive type inference properly #20566
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
base: main
Are you sure you want to change the base?
Conversation
|
|
||
| #[allow(private_interfaces)] | ||
| #[derive(Clone, Debug, Eq, Hash, PartialEq, salsa::Update, get_size2::GetSize)] | ||
| pub enum DivergenceKind<'db> { |
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 seems we only use the identity of the divergent type and don't care that much about about its content. Could we use a u64 instead (with a global counter of the last issued id)?
|
What are the salsa features that are required for this PR to land? |
|
I put up a PR that implements the extensions that I think are needed for this to work:
I didn't understand this part or the semantics of the join operation. Specifically, how the join operation is different from With those features in place, is this PR something you could drive forward? I'm asking because we're most likely going to land #20988 as is because it unblocks type of self with a minimal regression but it would be great to have a proper fix in place. |
|
One thing I wonder. Should queries be allowed to customize So maybe,
|
Thanks, it'll be helpful, but I'll have to elaborate on my thoughts.
@carljm had a similar question, and my answer is given here.
For the reason stated above, I believe that simply providing a "last provisional value" in the cycle_recovery function will not achieve fully-converged type inference.
In my opinion, there is no need to set a "threshold" at which to give up on further type inference and switch to |
I think that leaving the decision of convergence to the user risks making inference unstable: that is, salsa users may force (or erroneously) declare convergence when it has not actually converged, leading to non-determinism. |
Yeah, agree. But I think we can enable this functionality by comparing if the value returned by
I read that conversation and it's the part I don't understand. It also seems specific to return type inference because the lattice isn't monotonic. Which seems different from diverging cases that continue going forever. Edit: Instead of having specific handling in many places. Could the cycle function instead: If the previous value contains Replace all instance of This is a no-op for The change I proposed in Salsa upstream to consider a cycle head as converged when the |
Consider inferring the return type of the following function: # 0th: Divergent (cycle_initial)
# 1st: None | tuple[Divergent]
# 2nd: None | tuple[None | tuple[Divergent]]
# ...
def div(x: int):
if x == 0:
return None
else:
return (div(x-1),)If the values from the previous and current cycles do not match, then the from typing import overload
class A: ...
class B(A): ...
@overload
def flip(x: B) -> A: ...
@overload
def flip(x: A) -> B: ...
def flip(x): ...
class C:
def __init__(self, x: B):
self.x = x
def flip(self):
# 0th: Divergent
# 1st: B
# 2nd: A
# 3rd: B
# ...
self.x = flip(self.x)
reveal_type(C(B()).x)Therefore, I believe the correct approach here is to allow |
I think the new salsa version supports this now. The |
Ah, so you've made it so that the equality test is performed again after the fallback. I overlooked that. So, I think there's no problem and and I can move this PR forward. |
Diagnostic diff on typing conformance testsChanges were detected when running ty on typing conformance tests--- old-output.txt 2025-11-07 06:03:21.954184401 +0000
+++ new-output.txt 2025-11-07 06:03:24.974194889 +0000
@@ -1,4 +1,3 @@
-fatal[panic] Panicked at /home/runner/.cargo/git/checkouts/salsa-e6f3bb7c2a062968/05a9af7/src/function/execute.rs:451:17 when checking `/home/runner/work/ruff/ruff/typing/conformance/tests/aliases_typealiastype.py`: `infer_definition_types(Id(18b71)): execute: too many cycle iterations`
_directives_deprecated_library.py:15:31: error[invalid-return-type] Function always implicitly returns `None`, which is not assignable to return type `int`
_directives_deprecated_library.py:30:26: error[invalid-return-type] Function always implicitly returns `None`, which is not assignable to return type `str`
_directives_deprecated_library.py:36:41: error[invalid-return-type] Function always implicitly returns `None`, which is not assignable to return type `Self@__add__`
@@ -74,6 +73,23 @@
aliases_type_statement.py:79:7: error[too-many-positional-arguments] Too many positional arguments: expected 2, got 3
aliases_type_statement.py:80:7: error[too-many-positional-arguments] Too many positional arguments: expected 2, got 3
aliases_type_statement.py:80:37: error[invalid-type-form] List literals are not allowed in this context in a type expression: Did you mean `tuple[int, str]`?
+aliases_typealiastype.py:32:7: error[unresolved-attribute] Object of type `typing.TypeAliasType` has no attribute `other_attrib`
+aliases_typealiastype.py:39:26: error[invalid-type-form] List literals are not allowed in this context in a type expression: Did you mean `tuple[int, str]`?
+aliases_typealiastype.py:52:40: error[invalid-type-form] Function calls are not allowed in type expressions
+aliases_typealiastype.py:53:40: error[invalid-type-form] List literals are not allowed in this context in a type expression: Did you mean `tuple[int, str]`?
+aliases_typealiastype.py:54:42: error[invalid-type-form] Tuple literals are not allowed in this context in a type expression
+aliases_typealiastype.py:54:43: error[invalid-type-form] Tuple literals are not allowed in this context in a type expression: Did you mean `tuple[int, str]`?
+aliases_typealiastype.py:55:42: error[invalid-type-form] List comprehensions are not allowed in type expressions
+aliases_typealiastype.py:56:42: error[invalid-type-form] Dict literals are not allowed in type expressions
+aliases_typealiastype.py:57:42: error[invalid-type-form] Function calls are not allowed in type expressions
+aliases_typealiastype.py:58:48: error[invalid-type-form] Int literals are not allowed in this context in a type expression
+aliases_typealiastype.py:59:42: error[invalid-type-form] `if` expressions are not allowed in type expressions
+aliases_typealiastype.py:60:42: error[invalid-type-form] Variable of type `Literal[3]` is not allowed in a type expression
+aliases_typealiastype.py:61:42: error[invalid-type-form] Boolean literals are not allowed in this context in a type expression
+aliases_typealiastype.py:62:42: error[invalid-type-form] Int literals are not allowed in this context in a type expression
+aliases_typealiastype.py:63:42: error[invalid-type-form] Boolean operations are not allowed in type expressions
+aliases_typealiastype.py:64:42: error[invalid-type-form] F-strings are not allowed in type expressions
+aliases_typealiastype.py:66:47: error[unresolved-reference] Name `BadAlias21` used when not defined
aliases_variance.py:18:24: error[non-subscriptable] Cannot subscript object of type `<class 'ClassA[typing.TypeVar]'>` with no `__class_getitem__` method
aliases_variance.py:28:16: error[non-subscriptable] Cannot subscript object of type `<class 'ClassA[typing.TypeVar]'>` with no `__class_getitem__` method
aliases_variance.py:44:16: error[non-subscriptable] Cannot subscript object of type `<class 'ClassB[typing.TypeVar, typing.TypeVar]'>` with no `__class_getitem__` method
@@ -1002,5 +1018,4 @@
typeddicts_usage.py:28:17: error[missing-typed-dict-key] Missing required key 'name' in TypedDict `Movie` constructor
typeddicts_usage.py:28:18: error[invalid-key] Invalid key for TypedDict `Movie`: Unknown key "title"
typeddicts_usage.py:40:24: error[invalid-type-form] The special form `typing.TypedDict` is not allowed in type expressions. Did you mean to use a concrete TypedDict or `collections.abc.Mapping[str, object]` instead?
-Found 1004 diagnostics
-WARN A fatal error occurred while checking some files. Not all project files were analyzed. See the diagnostics list above for details.
+Found 1020 diagnostics |
82d9580 to
d9eac53
Compare
CodSpeed Performance ReportMerging #20566 will improve performances by 9.32%Comparing Summary
Benchmarks breakdown
|
|
Ohh... do we also need to pass the id to the initial function? |
d9eac53 to
041bb24
Compare
Yes. For now I'm using https://github.com/mtshiba/salsa/tree/input_id?rev=9ea5289bc6a87943b8a8620df8ff429062c56af0, but is there a better way? There will be a lot of changes. |
No, I don't think there's a better way. It's a breaking change that requires updating all cycle initial functions. Do you want to put up a Salsa PR (Claude's really good at updating the function signatures, but not very fast :)) |
|
|
Hmm, it looks like the problem is still not solved... MRE: class ManyCycles:
def __init__(self: "ManyCycles"):
self.x1 = 0
self.x2 = 0
self.x3 = 1
def f(self: "ManyCycles"):
self.x1 = self.x2 + self.x3 + 1
self.x2 = self.x1 + self.x3 + 2
self.x3 = self.x1 + self.x2 + 3
m = ManyCycles()
reveal_type(m.x1) # should be: Unknown | int, but: Unknown | int | Divergent | Divergent
reveal_type(m.x2) # should be: Unknown | int, but: Unknown | int | Divergent
reveal_type(m.x3) # should be: Unknown | int, but: Unknown | int | Divergent | Divergenttracing output |
…current provisional type
Were you able to figure out what's happening? Is the issue that the |
|
This example might make it easier to see what's happening. class A: ...
class B: ...
class C: ...
class Foo:
def __init__(self):
self.a = A()
self.b = B()
self.c = C()
def f1(self):
self.a = self.b
def f2(self, cond: bool):
self.b = self.c if cond else self.a
def f3(self):
self.c = self.b
# outermost cycle head
# 0th: Divergent(Foo.a)
# 1st: Unknown | A | B | C | Divergent(Foo.a) ->(strip divergent) Unknown | A | B | C
# 2nd: Unknown | A | B | C | Divergent(Foo.a) -> Unknown | A | B | C
reveal_type(Foo().a)
# iterated as part of the outer cycle implicit_attribute_inner(Foo.a)
# 0th: Divergent(Foo.b)
# 1st: Unknown | B | C | Divergent(Foo.b) | Divergent(Foo.a) -> Unknown | B | C | Divergent(Foo.a)
# 2nd: Unknown | B | C | Divergent(Foo.a) | A -> Unknown | B | C | Divergent(Foo.a) | A
# 3rd: Unknown | B | C | Divergent(Foo.a) | A -> Unknown | B | C | Divergent(Foo.a) | A
reveal_type(Foo().b)
# not a cycle head
# 0th: Unknown | C | Divergent(Foo.b)
# 1st: Unknown | C | B | Divergent(Foo.a)
# 2nd: Unknown | C | B | Divergent(Foo.a) | A
# 3rd: Unknown | C | B | Divergent(Foo.a) | A
reveal_type(Foo().c)graph LR
Foo.a-->Foo.b
Foo.b-->Foo.c
Foo.b-->Foo.a
Foo.c-->Foo.b
The cycle recovery function for |
…and the current provisional type" This reverts commit ab84bdf.
915dd92 to
682a2e8
Compare
Can't we replace all |
The cycle recovery function cannot remove |
|
As a PoC, I modified salsa so that the cycle recovery function receives This is something we wanted to avoid, but it seems to work. |
It's not clear to me how this is different from removing all divergent types. As in, you can only see |
|
ff59ea0 to
2393f6a
Compare
|
For my understanding. Are we now removing all instances of I'm asking because there are instances where a cycle head in iteration N becomes a normal cycle participant (not a head) in |
Summary
Derived from #17371
Fixes astral-sh/ty#256
Fixes astral-sh/ty#1415
Fixes astral-sh/ty#1433
Properly handles any kind of recursive inference and prevents panics.
The discussion in #17371 (comment) revealed that additional changes to the salsa API are required to complete this PR, and I will update this PR as soon as those changes are made.
Let me explain techniques for converging fixed-point iterations during recursive type inference.
There are two types of type inference that naively don't converge (causing salsa to panic): divergent type inference and oscillating type inference.
Divergent type inference
Divergent type inference occurs when eagerly expanding a recursive type. A typical example is this:
To solve this problem, we have already introduced
Divergenttypes (#20312).Divergenttypes are treated as a kind of dynamic type 1.When a query function that returns a type enters a cycle, it sets
Divergentas the cycle initial value (instead ofNever). Then, in the cycle recovery function, it reduces the nesting of types containingDivergentto converge.Each cycle recovery function for each query should operate only on the
Divergenttype originating from that query.For this reason, while
Divergentappears the same asAnyto the user, it internally carries some information: the location where the cycle occurred. Previously, we roughly identified this by having the scope where the cycle occurred, but with the update to salsa, functions that create cycle initial values can now receive asalsa::Id(salsa-rs/salsa#1012). This is an opaque ID that uniquely identifies the cycle head (the query that is the starting point for the fixed-point iteration).Divergentnow has thissalsa::Id.Oscillating type inference
Now, another thing to consider is oscillating type inference. Oscillating type inference arises from the fact that monotonicity is broken. Monotonicity here means that for a query function, if it enters a cycle, the calculation must start from a "bottom value" and progress towards the final result with each cycle. Monotonicity breaks down in type systems that have features like overloading and overriding.
Naive fixed-point iteration results in
Divergent -> Sub -> Base -> Sub -> ..., which oscillates forever without diverging or converging. To address this, the salsa API has been modified so that the cycle recovery function receives the value of the previous revision (salsa-rs/salsa#1012).The cycle recovery function returns the union of the type of the current revision and the previous revision. Therefore, the value for each cycle is
Divergent -> Sub -> Base (= Sub | Base) -> Base, which converges.The final result of oscillating type inference does not contain
DivergentbecauseDivergentthat appears in a union type can be removed, as is clear from the expansion. This simplification is performed at the same time as nesting reduction.Test Plan
All samples listed in astral-sh/ty#256 are tested and passed without any panic!
Footnotes
In theory, it may be possible to strictly treat types containing
Divergenttypes as recursive types, but we probably shouldn't go that deep yet. (AFAIK, there are no PEPs that specify how to handle implicitly recursive types that aren't named by type aliases) ↩