[ty] Introduce `Recursive` types and fully support recursive implicit type aliases (#28425)
## Summary
Closes https://github.com/astral-sh/ty/issues/1738
(While this PR also resolves the error in the code provided in
https://github.com/astral-sh/ty/issues/1846, I consider the broader
issue under discussion to still be unresolved)
To fully support implicit type aliases, this PR introduces `Recursive`
types. These represent *structural recursive types*. In other words,
they are anonymous recursive types implicitly constructed through type
inference, rather than a nominally defined recursive type like PEP 695
recursive type aliases.
This is what was being discussed in
https://github.com/astral-sh/ruff/pull/24252#issuecomment-4172655350. We
are not introducing recursive types solely for implicit type aliases;
this is the first step toward completely replacing the current
`Divergent`-based approximate recursive type inference with a full
implementation.
Initially, I planned to completely remove the `Divergent` type alongside
the introduction of `Recursive` types, but because the scope of the
impact was far too large, I decided to replace it incrementally. Both
will coexist until the replacement is complete, but eventually,
everything should be replaced by `Recursive` types.
Following this PR, I plan to use the newly introduced `Recursive` types
to replace various forms of recursive type inference.
## Design
Currently, we approximate and treat recursive type structures generated
by recursive type inference as gradual types containing `Divergent`. For
example, a subscript on `x: Divergent` results in `x[n]: Divergent`.
Consequently, we get:
```
x: list[Divergent]
x[n]: Divergent
x[n][n]: Divergent
```
As a result, the type after subscripting loses the information that `x`
was a recursive list type. We solve this problem by introducing
recursive types.
`RecursiveType` is a binder for a body type that contains a recursive
variable. In other words, it roughly has the following structure:
```rust
struct RecursiveType<'db> {
id: salsa::Id,
body: Type<'db>,
arguments: Option<Specialization<'db>>,
}
struct RecursiveVar<'db> {
id: salsa::Id,
arguments: Option<Specialization<'db>>,
}
enum Type<'db> {
Recursive(RecursiveType<'db>),
RecursiveVar(RecursiveVar<'db>),
...
}
```
For example, for the following implicit type alias:
```python
Tree = tuple[T, "Tree[list[T]] | None"]
# = μF. λT. tuple[T, F[list[T]] | None]
```
the constructed `RecursiveType` looks like this:
```rust
RecursiveType {
id,
body: tuple[T, RecursiveVar { id, arguments: [list[T]] } | None],
arguments: [T]
}
```
Unlike `Divergent`, the recursive variable `RecursiveVar` has no type
properties on its own. Attempting to access this variable immediately
unfolds the recursive type, so questioning the typing properties of the
variable itself is meaningless. Therefore, if any type operation on
`RecursiveVar` appears, it should be a bug.
To infer the container subscript `x[1]` for `x: Tree[int]`, first unfold
`x`'s type. Unfolding replaces references to the recursive binder with
the recursive type itself. Writing `B[a := R]` for capture-avoiding
substitution of `R` for `a` in `B`:
```text
unfold(μa. B) = B[a := μa. B]
```
For `Tree[int]`, substitute the constructor for `F`, then apply `T :=
int`:
```text
unfold((μF. λT. tuple[T, F[list[T]] | None])[int])
= tuple[int, (μF. λT. tuple[T, F[list[T]] | None])[list[int]] | None]
(= tuple[int, Tree[list[int]] | None])
```
Tuple subscripting then selects the element at index 1: `x[1]:
Tree[list[int]] | None`.
## Test Plan
mdtest updated
---------
Co-authored-by: Carl Meyer <carl@astral.sh>
ruff
160ffbf2 - [ty] Introduce `Recursive` types and fully support recursive implicit type aliases (#28425)
