mirror of
https://github.com/astral-sh/ruff.git
synced 2026-10-28 10:45:37 +08:00
[ty] Audit remaining sources of non-determinism in constraint set solutions (#26896)
We are considering moving back to using salsa, instead of hand-rolled caches, to memoize the BDD structure of the constraint sets that we produce. We orignally moved to hand-rolled caches in https://github.com/astral-sh/ruff/pull/23538 to remove non-determinism in our tests and diagnostic output. That means that if we want to go back to salsa caching, we need to properly address that non-determinism. I have had Codex [perform an audit](https://gist.github.com/dcreager/b97decb3698cfcd553c316de5423a872) of those sources of non-determinism. This PR adds some additional testing infrastructure to exercise those sources: - The new `regression/constraint_set_ordering.md` mdtest includes tests of everything identified in the audit (including places where we are already correctly robust to variable ordering). This required adding a couple of additional `ty_extension` methods for interrogating constraint sets. - The new `TY_CONSTRAINT_SET_ORDER` environment variable lets you arbitrarily permute (or "wobble") the variable ordering that we choose for the constraint sets we create in a particular run of `ty`. Setting this is very likely to cause the new mdtest file to fail! Once we fix all of the non-determinism "for real", that file should pass regardless of which variable ordering permutation is chosen. - The new agent skill makes it easier to automate this process in an agent loop. Note that this does not fix any of the open sources of non-determinism! It just lets us more easily see what they are.
This commit is contained in:
Douglas Creager authored and GitHub committed
1 parent
38a96fc995
commit
150377d518
16 files changed
+1111
-14
No files matched your search
@@ -0,0 +1,75 @@
|
||||
---
|
||||
name: wobbling-ty-constraint-order
|
||||
description: >
|
||||
Use when a user asks to wobble ty constraint ordering, check constraint-set or TDD ordering
|
||||
determinism, test reversed constraint/typevar IDs, or investigate nondeterministic ty inference
|
||||
and mdtest results.
|
||||
compatibility: >
|
||||
Requires Cargo, mktemp, and a POSIX-compatible shell; uses cargo-nextest when available and
|
||||
otherwise falls back to cargo test.
|
||||
---
|
||||
|
||||
# Wobbling ty constraint order
|
||||
|
||||
`TY_CONSTRAINT_SET_ORDER` perturbs both the builder-local TDD-variable order and the local typevar order used to orient typevar-to-typevar constraints. The setting is fixed for the lifetime of each test process.
|
||||
|
||||
- unset/`0`: normal ordering;
|
||||
- `reverse`: reverse both orderings;
|
||||
- an integer: XOR each local ID with that mask. Small masks immediately perturb dense arena IDs: `1` swaps adjacent IDs, `3` reverses blocks of four, and powers of two exchange neighboring blocks.
|
||||
|
||||
This deliberately changes internal TDD shape. Run **mdtests only**: graph-structure unit snapshots are expected to differ. Never enable snapshot updates for a wobble run, since updating would hide the failures being sought.
|
||||
|
||||
## Run
|
||||
|
||||
From the Ruff root, first establish the normal baseline, then run the reversed and XOR-masked orders sequentially. Set `TY_CONSTRAINT_ORDER_LOG_DIR` to retain logs in a particular writable directory; otherwise `mktemp` chooses an appropriate temporary directory (respecting the environment's temporary-directory configuration).
|
||||
|
||||
```bash
|
||||
set -u
|
||||
|
||||
if test -n "${TY_CONSTRAINT_ORDER_LOG_DIR:-}"; then
|
||||
log_dir="$TY_CONSTRAINT_ORDER_LOG_DIR"
|
||||
mkdir -p "$log_dir"
|
||||
else
|
||||
log_dir="$(mktemp -d -t ty-constraint-order.XXXXXXXX)"
|
||||
fi
|
||||
printf '%s\n' "logs: $log_dir"
|
||||
|
||||
if cargo nextest --version >/dev/null 2>&1; then
|
||||
runner=nextest
|
||||
else
|
||||
runner=test
|
||||
fi
|
||||
printf '%s\n' "runner: cargo $runner"
|
||||
|
||||
export CARGO_PROFILE_DEV_OPT_LEVEL=1
|
||||
export CARGO_PROFILE_DEV_DEBUG=line-tables-only
|
||||
export INSTA_UPDATE=no
|
||||
export MDTEST_UPDATE_SNAPSHOTS=0
|
||||
unset INSTA_FORCE_PASS || true
|
||||
|
||||
for order in normal reverse 1 2 3 4 7 8 15; do
|
||||
if test "$order" = normal; then
|
||||
unset TY_CONSTRAINT_SET_ORDER || true
|
||||
else
|
||||
export TY_CONSTRAINT_SET_ORDER="$order"
|
||||
fi
|
||||
|
||||
log="$log_dir/ty-constraint-order-${order}.log"
|
||||
if test "$runner" = nextest; then
|
||||
cargo nextest run -p ty_python_semantic --test mdtest \
|
||||
--no-fail-fast --status-level fail --failure-output immediate-final \
|
||||
>"$log" 2>&1
|
||||
else
|
||||
cargo test -p ty_python_semantic --test mdtest >"$log" 2>&1
|
||||
fi
|
||||
status=$?
|
||||
|
||||
printf '%-7s exit=%s\n' "$order" "$status"
|
||||
grep -E 'Summary \[|test result:' "$log" | tail -1 || true
|
||||
printf '%s\n' " log: $log"
|
||||
done
|
||||
```
|
||||
|
||||
Read each failing log and report the mdtest file, section, line, expected result, and actual diagnostic/revealed type. A wobble failure is evidence that inference semantics or displayed solution types still depend on ordering; do not update the mdtest expectations merely to make the wobble run green.
|
||||
|
||||
The knob does **not** perturb hashing of Salsa-backed values. The `Solution binding order follows constraint source order` section of `regression/constraint_set_ordering.md` separately varies typevar declaration order to catch binding-order changes caused by draining an `FxHashMap<BoundTypeVarInstance, ...>`.
|
||||
Generated
+1
@@ -4905,6 +4905,7 @@ dependencies = [
|
||||
"ty_module_resolver",
|
||||
"ty_python_core",
|
||||
"ty_site_packages",
|
||||
"ty_static",
|
||||
"ty_test",
|
||||
"ty_vendored",
|
||||
]
|
||||
|
||||
@@ -26,6 +26,7 @@ ruff_text_size = { workspace = true }
|
||||
ty_module_resolver = { workspace = true }
|
||||
ty_site_packages = { workspace = true }
|
||||
ty_python_core = { workspace = true }
|
||||
ty_static = { workspace = true }
|
||||
|
||||
bitflags = { workspace = true }
|
||||
char_str = { workspace = true }
|
||||
|
||||
@@ -0,0 +1,484 @@
|
||||
# Constraint set ordering
|
||||
|
||||
This file verifies that constraint set solutions are deterministic, even in the presence of
|
||||
different variable orderings in their underlying BDDs.
|
||||
|
||||
The current implementation is _stable_ in the sense that multiple runs of `ty` against the same
|
||||
source will produce the same result. But there are still some lingering places where the output
|
||||
depends on the particular BDD variable ordering that is chosen.
|
||||
|
||||
The diagnostic expectations show the output that is produced by the default stable ordering, so that
|
||||
if you are not explicitly testing constraint set stability, mdtests should pass. We also include
|
||||
TODO comments showing the other potential outputs that might be produced, under different variable
|
||||
orderings. (`ConstraintSet.solutions_for` exposes each explicit per-typevar solution;
|
||||
`ConstraintSet.solutions` additionally preserves path and binding order. This keeps duplicate and
|
||||
`Never` solutions visible when they would otherwise disappear as paths are unioned.)
|
||||
|
||||
To test this, you can set the `TY_CONSTRAINT_SET_ORDER` environment variable to either `reverse` or
|
||||
to an integer. This lets you choose a different permutation for each run of `ty`. You can also use
|
||||
the `wobbling-ty-constraint-order` agent skill to automate this process.
|
||||
|
||||
```toml
|
||||
[environment]
|
||||
python-version = "3.13"
|
||||
```
|
||||
|
||||
## Solution binding order follows constraint source order
|
||||
|
||||
The order of bindings within a path must follow the first constraint that introduced each typevar.
|
||||
Reversing either the typevar declaration order or the constraint source order exercises both sides
|
||||
of this requirement.
|
||||
|
||||
```py
|
||||
from ty_extensions._internal import ConstraintSet
|
||||
|
||||
def bindings_tuv[T, U, V]() -> None:
|
||||
# (T = int) ∧ (U = str) ∧ (V = bytes)
|
||||
constraints = ConstraintSet.range(int, T, int) & ConstraintSet.range(str, U, str) & ConstraintSet.range(bytes, V, bytes)
|
||||
# revealed: tuple[Solution[T=int, U=str, V=bytes]]
|
||||
reveal_type(constraints.solutions(inferable=tuple[T, U, V]))
|
||||
|
||||
def bindings_vtu[V, T, U]() -> None:
|
||||
# (T = int) ∧ (U = str) ∧ (V = bytes)
|
||||
constraints = ConstraintSet.range(int, T, int) & ConstraintSet.range(str, U, str) & ConstraintSet.range(bytes, V, bytes)
|
||||
# revealed: tuple[Solution[T=int, U=str, V=bytes]]
|
||||
reveal_type(constraints.solutions(inferable=tuple[T, U, V]))
|
||||
|
||||
def bindings_reverse_source[T, U, V]() -> None:
|
||||
# (V = bytes) ∧ (U = str) ∧ (T = int)
|
||||
constraints = ConstraintSet.range(bytes, V, bytes) & ConstraintSet.range(str, U, str) & ConstraintSet.range(int, T, int)
|
||||
# revealed: tuple[Solution[V=bytes, U=str, T=int]]
|
||||
reveal_type(constraints.solutions(inferable=tuple[T, U, V]))
|
||||
```
|
||||
|
||||
## Nested transitive constraints and an unrelated alternative
|
||||
|
||||
In `((T ≤ list[U]) ∧ (U ≤ int) ∧ (list[int] ≤ T)) | (bytes ≤ V)`, the two sides of the union are
|
||||
completely independent: the solutions for `T` and `U` should not influence the solutions for `V`,
|
||||
and vice versa. Because we combine them with union, we are allowed to _either_ find a solution for
|
||||
`T` and `U`, _or_ find a solution for `V`. We are not _obligated_ to find a solution for all three.
|
||||
|
||||
```py
|
||||
from typing import Never
|
||||
from ty_extensions._internal import ConstraintSet
|
||||
|
||||
def nested_transitive[T, U, V]() -> None:
|
||||
# ((T ≤ list[U]) ∧ (U ≤ int) ∧ (list[int] ≤ T)) | (bytes ≤ V)
|
||||
constraints = (
|
||||
ConstraintSet.range(Never, T, list[U]) & ConstraintSet.range(Never, U, int) & ConstraintSet.range(list[int], T, object)
|
||||
) | ConstraintSet.range(bytes, V, object)
|
||||
|
||||
# TODO: sometimes: revealed tuple[Solution[T=list[int]], Solution[T=Never], Solution[]]
|
||||
# TODO: sometimes: revealed tuple[Solution[T=list[int]], Solution[T=list[int]], Solution[]]
|
||||
# TODO: sometimes: revealed tuple[Solution[T=list[int]], Solution[], Solution[]]
|
||||
# revealed: tuple[Solution[T=list[int]], Solution[]]
|
||||
reveal_type(constraints.solutions_for(T, inferable=tuple[T, U, V]))
|
||||
|
||||
# TODO: sometimes: revealed tuple[Solution[U=int], Solution[U=Never], Solution[]]
|
||||
# TODO: sometimes: revealed tuple[Solution[U=int], Solution[], Solution[]]
|
||||
# revealed: tuple[Solution[U=int], Solution[]]
|
||||
reveal_type(constraints.solutions_for(U, inferable=tuple[T, U, V]))
|
||||
|
||||
# TODO: sometimes: revealed tuple[Solution[], Solution[V=bytes], Solution[V=bytes]]
|
||||
# revealed: tuple[Solution[], Solution[V=bytes]]
|
||||
reveal_type(constraints.solutions_for(V, inferable=tuple[T, U, V]))
|
||||
|
||||
# TODO: sometimes: revealed tuple[Solution[T=list[int], U=int], Solution[T=Never, V=bytes], Solution[V=bytes]]
|
||||
# TODO: sometimes: revealed tuple[Solution[T=list[int], U=int], Solution[T=list[int], V=bytes], Solution[V=bytes]]
|
||||
# TODO: sometimes: revealed tuple[Solution[T=list[int], U=int], Solution[U=Never, V=bytes], Solution[V=bytes]]
|
||||
# revealed: tuple[Solution[T=list[int], U=int], Solution[V=bytes]]
|
||||
reveal_type(constraints.solutions(inferable=tuple[T, U, V]))
|
||||
```
|
||||
|
||||
## Negated alternatives do not infer positive evidence
|
||||
|
||||
In `¬((T ≤ int) ∨ (T ≤ str)) | (bytes ≤ U)`, the lhs of the union is a negation, and should not
|
||||
place any positive restriction on `T`. Like above, we are not obligated to produce a solution that
|
||||
includes both sides of the union, so any solution that includes `bytes ≤ U` should not include a
|
||||
solution for `T`.
|
||||
|
||||
```py
|
||||
from typing import Never
|
||||
from ty_extensions._internal import ConstraintSet
|
||||
|
||||
def negated_alternative[T, U]() -> None:
|
||||
# ¬((T ≤ int) ∨ (T ≤ str)) | (bytes ≤ U)
|
||||
constraints = ~(ConstraintSet.range(Never, T, int) | ConstraintSet.range(Never, T, str)) | ConstraintSet.range(
|
||||
bytes, U, object
|
||||
)
|
||||
|
||||
# TODO: sometimes: revealed tuple[Solution[], Solution[T=Never], Solution[]]
|
||||
# revealed: tuple[Solution[], Solution[]]
|
||||
reveal_type(constraints.solutions_for(T, inferable=tuple[T, U]))
|
||||
|
||||
# TODO: sometimes: revealed tuple[Solution[], Solution[U=bytes], Solution[U=bytes]]
|
||||
# revealed: tuple[Solution[], Solution[U=bytes]]
|
||||
reveal_type(constraints.solutions_for(U, inferable=tuple[T, U]))
|
||||
|
||||
# TODO: sometimes: revealed tuple[Solution[], Solution[T=Never, U=bytes], Solution[U=bytes]]
|
||||
# revealed: tuple[Solution[], Solution[U=bytes]]
|
||||
reveal_type(constraints.solutions(inferable=tuple[T, U]))
|
||||
```
|
||||
|
||||
## Derived solution element order
|
||||
|
||||
Constructing the constraints in the opposite source order makes the derived union observable. Its
|
||||
elements should not be reordered merely because the TDD-variable order changes.
|
||||
|
||||
```py
|
||||
from typing import Never
|
||||
from ty_extensions._internal import ConstraintSet
|
||||
|
||||
def derived_solution[U, T]() -> None:
|
||||
# (U ≤ int) ∧ (int ≤ T) ∧ ((T ≤ int) | (T ≤ str))
|
||||
constraints = (
|
||||
ConstraintSet.range(Never, U, int)
|
||||
& ConstraintSet.range(int, T, object)
|
||||
& (ConstraintSet.range(Never, T, int) | ConstraintSet.range(Never, T, str))
|
||||
)
|
||||
|
||||
# TODO: The derived relationship should not leave an inferable `U` in the solution for `T`.
|
||||
# TODO: revealed: tuple[Solution[T=int]]
|
||||
# TODO: sometimes: revealed tuple[Solution[T=int | U@derived_solution]]
|
||||
# revealed: tuple[Solution[T=U@derived_solution | int]]
|
||||
reveal_type(constraints.solutions_for(T, inferable=tuple[T, U]))
|
||||
|
||||
# TODO: The derived relationship should not leave an inferable `T` in the solution for `U`.
|
||||
# TODO: revealed: tuple[Solution[U=int]]
|
||||
# revealed: tuple[Solution[U=Never]]
|
||||
reveal_type(constraints.solutions_for(U, inferable=tuple[T, U]))
|
||||
```
|
||||
|
||||
## Bare-typevar orientation and tied source order
|
||||
|
||||
`S ≤ T` can be represented as a constraint on either typevar, and `S ≤ T ≤ U` can be either one
|
||||
range or two linked constraints. Logical equivalence and solution-element order must remain stable
|
||||
in both declaration orders.
|
||||
|
||||
```py
|
||||
from typing import Never
|
||||
from ty_extensions import static_assert
|
||||
from ty_extensions._internal import ConstraintSet
|
||||
|
||||
def orientation_st[S, T]() -> None:
|
||||
lower = ConstraintSet.range(Never, S, T)
|
||||
upper = ConstraintSet.range(S, T, object)
|
||||
# TODO: sometimes: error [static-assert-error] "Static assertion error: argument evaluates to `False`"
|
||||
static_assert(lower == upper)
|
||||
|
||||
equality_st = ConstraintSet.range(T, S, T)
|
||||
equality_ts = ConstraintSet.range(S, T, S)
|
||||
static_assert(equality_st == equality_ts)
|
||||
|
||||
def orientation_ts[T, S]() -> None:
|
||||
lower = ConstraintSet.range(Never, S, T)
|
||||
upper = ConstraintSet.range(S, T, object)
|
||||
# TODO: sometimes: error [static-assert-error] "Static assertion error: argument evaluates to `False`"
|
||||
static_assert(lower == upper)
|
||||
|
||||
equality_st = ConstraintSet.range(T, S, T)
|
||||
equality_ts = ConstraintSet.range(S, T, S)
|
||||
static_assert(equality_st == equality_ts)
|
||||
|
||||
def chain_stu[S, T, U]() -> None:
|
||||
chain = ConstraintSet.range(S, T, U)
|
||||
linked = ConstraintSet.range(Never, S, T) & ConstraintSet.range(Never, T, U)
|
||||
# TODO: sometimes: error [static-assert-error] "Static assertion error: argument evaluates to `False`"
|
||||
static_assert(chain == linked)
|
||||
|
||||
constraints = chain & ConstraintSet.range(int, S, object) & ConstraintSet.range(Never, U, int)
|
||||
# TODO: inferable typevars should not remain in these concrete solutions.
|
||||
# TODO: sometimes: revealed tuple[Solution[S=int | U@chain_stu | T@chain_stu]]
|
||||
# revealed: tuple[Solution[S=T@chain_stu | int | U@chain_stu]]
|
||||
reveal_type(constraints.solutions_for(S, inferable=tuple[S, T, U]))
|
||||
# revealed: tuple[Solution[T=S@chain_stu | int | U@chain_stu]]
|
||||
reveal_type(constraints.solutions_for(T, inferable=tuple[S, T, U]))
|
||||
# revealed: tuple[Solution[U=T@chain_stu | S@chain_stu | int]]
|
||||
reveal_type(constraints.solutions_for(U, inferable=tuple[S, T, U]))
|
||||
|
||||
def chain_uts[U, T, S]() -> None:
|
||||
chain = ConstraintSet.range(S, T, U)
|
||||
linked = ConstraintSet.range(Never, S, T) & ConstraintSet.range(Never, T, U)
|
||||
# TODO: sometimes: error [static-assert-error] "Static assertion error: argument evaluates to `False`"
|
||||
static_assert(chain == linked)
|
||||
|
||||
constraints = chain & ConstraintSet.range(int, S, object) & ConstraintSet.range(Never, U, int)
|
||||
# TODO: inferable typevars should not remain in these concrete solutions.
|
||||
# TODO: sometimes: revealed tuple[Solution[S=int | U@chain_uts | T@chain_uts]]
|
||||
# revealed: tuple[Solution[S=T@chain_uts | int | U@chain_uts]]
|
||||
reveal_type(constraints.solutions_for(S, inferable=tuple[S, T, U]))
|
||||
# revealed: tuple[Solution[T=S@chain_uts | int | U@chain_uts]]
|
||||
reveal_type(constraints.solutions_for(T, inferable=tuple[S, T, U]))
|
||||
# revealed: tuple[Solution[U=T@chain_uts | S@chain_uts | int]]
|
||||
reveal_type(constraints.solutions_for(U, inferable=tuple[S, T, U]))
|
||||
```
|
||||
|
||||
## Abstraction and non-inferable typevars
|
||||
|
||||
Removing non-inferable typevars rebuilds the TDD with `ite`; irrelevant positive decisions must not
|
||||
leak onto the surviving paths. Universal abstraction of an alternative must likewise leave only the
|
||||
unrelated branch.
|
||||
|
||||
```py
|
||||
from typing import Never
|
||||
from ty_extensions import static_assert
|
||||
from ty_extensions._internal import ConstraintSet
|
||||
|
||||
def noninferable_nested[T, U, V]() -> None:
|
||||
constraints = (
|
||||
ConstraintSet.range(Never, T, list[U]) & ConstraintSet.range(Never, U, int) & ConstraintSet.range(list[int], T, object)
|
||||
) | ConstraintSet.range(bytes, V, object)
|
||||
|
||||
# `U` is deliberately non-inferable here.
|
||||
# TODO: We should not include a solution for non-inferable U.
|
||||
# TODO: sometimes: revealed tuple[Solution[T=list[int], U=int], Solution[T=Never, V=bytes], Solution[V=bytes]]
|
||||
# TODO: sometimes: revealed tuple[Solution[T=list[int], U=int], Solution[T=list[int], V=bytes], Solution[V=bytes]]
|
||||
# revealed: tuple[Solution[T=list[int], U=int], Solution[V=bytes]]
|
||||
reveal_type(constraints.solutions(inferable=tuple[T, V]))
|
||||
# TODO: sometimes: revealed tuple[Solution[T=list[int]], Solution[T=Never], Solution[]]
|
||||
# TODO: sometimes: revealed tuple[Solution[T=list[int]], Solution[T=list[int]], Solution[]]
|
||||
# revealed: tuple[Solution[T=list[int]], Solution[]]
|
||||
reveal_type(constraints.solutions_for(T, inferable=tuple[T, V]))
|
||||
# TODO: sometimes: revealed tuple[Solution[], Solution[V=bytes], Solution[V=bytes]]
|
||||
# revealed: tuple[Solution[], Solution[V=bytes]]
|
||||
reveal_type(constraints.solutions_for(V, inferable=tuple[T, V]))
|
||||
|
||||
quantified = constraints.for_all(tuple[T, U])
|
||||
expected = ConstraintSet.range(bytes, V, object)
|
||||
static_assert(quantified == expected)
|
||||
# revealed: tuple[Solution[V=bytes]]
|
||||
reveal_type(quantified.solutions_for(V, inferable=tuple[V]))
|
||||
|
||||
def noninferable_negated[T, U]() -> None:
|
||||
constraints = ~(ConstraintSet.range(Never, T, int) | ConstraintSet.range(Never, T, str)) | ConstraintSet.range(
|
||||
bytes, U, object
|
||||
)
|
||||
|
||||
quantified = constraints.for_all(tuple[T])
|
||||
expected = ConstraintSet.range(bytes, U, object)
|
||||
static_assert(quantified == expected)
|
||||
# revealed: tuple[Solution[U=bytes]]
|
||||
reveal_type(quantified.solutions_for(U, inferable=tuple[U]))
|
||||
```
|
||||
|
||||
## Call-site upper bounds preserve intersection order
|
||||
|
||||
Upper bounds inferred from contravariant callable parameters are intersected in call-site source
|
||||
order. This exercises the direct `UpperBound` insertion path separately from sequent-derived bounds.
|
||||
|
||||
```py
|
||||
from typing import Callable, Protocol, TypeVar
|
||||
|
||||
class P(Protocol):
|
||||
def p(self) -> None: ...
|
||||
|
||||
class Q(Protocol):
|
||||
def q(self) -> None: ...
|
||||
|
||||
T = TypeVar("T")
|
||||
|
||||
def accepts_p(value: P) -> None: ...
|
||||
def accepts_q(value: Q) -> None: ...
|
||||
def infer_from_callbacks(first: Callable[[T], None], second: Callable[[T], None]) -> T:
|
||||
raise NotImplementedError
|
||||
|
||||
# revealed: P & Q
|
||||
reveal_type(infer_from_callbacks(accepts_p, accepts_q))
|
||||
# revealed: Q & P
|
||||
reveal_type(infer_from_callbacks(accepts_q, accepts_p))
|
||||
```
|
||||
|
||||
## Generic-callable and protocol relation constraints
|
||||
|
||||
Relations can introduce fresh typevars and nested invariant constraints before those typevars are
|
||||
quantified away. A `TypedDict` union additionally exercises common-constraint probing and the
|
||||
fallback protocol-inference path; neither should depend on TDD order.
|
||||
|
||||
```py
|
||||
from typing import Callable, Literal, Protocol, TypeVar, TypedDict
|
||||
from ty_extensions import static_assert
|
||||
from ty_extensions._internal import ConstraintSet, TypeOf
|
||||
|
||||
def listify[T](value: T) -> list[T]:
|
||||
return [value]
|
||||
|
||||
def invariant_callable[U, V]() -> None:
|
||||
constraints = ConstraintSet.range(bool, U, int) & ConstraintSet.range(int, V, int)
|
||||
# TODO: no error. Existential reduction of the callable's fresh typevar is currently lossy.
|
||||
# TODO: sometimes: no error
|
||||
# error: [static-assert-error]
|
||||
static_assert(constraints.implies_subtype_of(TypeOf[listify], Callable[[U], list[V]]))
|
||||
|
||||
ConstrainedValue = TypeVar("ConstrainedValue", int, object, covariant=True)
|
||||
|
||||
class GetValue(Protocol[ConstrainedValue]):
|
||||
def __getitem__(self, key: Literal["value"], /) -> ConstrainedValue: ...
|
||||
|
||||
class ValueA(TypedDict):
|
||||
value: int
|
||||
|
||||
class ValueB(TypedDict):
|
||||
value: int
|
||||
|
||||
def get_value(value: GetValue[ConstrainedValue]) -> ConstrainedValue:
|
||||
raise NotImplementedError
|
||||
|
||||
def typed_dict_union(value: ValueA | ValueB) -> None:
|
||||
# TODO: sometimes: revealed object
|
||||
# revealed: int
|
||||
reveal_type(get_value(value))
|
||||
```
|
||||
|
||||
## Recursive derived relations remain cycle-safe
|
||||
|
||||
Derived constraints can recursively invoke relation checking. The coinductive owned-set cycle
|
||||
boundary must continue to terminate without accepting an incompatible non-recursive member when
|
||||
ordering changes.
|
||||
|
||||
```py
|
||||
from __future__ import annotations
|
||||
from typing import Protocol, cast
|
||||
|
||||
class Array(Protocol):
|
||||
def __abs__(self) -> Array: ...
|
||||
def __pos__(self) -> Array: ...
|
||||
def marker(self) -> int: ...
|
||||
|
||||
class Concrete[T]:
|
||||
def __abs__[S](self: S) -> S:
|
||||
return self
|
||||
|
||||
def __pos__[S](self: S) -> S:
|
||||
return self
|
||||
|
||||
def marker(self) -> str:
|
||||
return ""
|
||||
|
||||
def convert[T](value: Concrete[T]) -> Array:
|
||||
return cast(Array, value)
|
||||
|
||||
# error: [invalid-assignment]
|
||||
invalid: Array = Concrete[int]()
|
||||
```
|
||||
|
||||
## High-fanout sequents and inferred-union truncation
|
||||
|
||||
The cross-product between the twelve lower- and twelve upper-bound relationships exhausts the shared
|
||||
sequent fuel budget. The remaining solution, its element order, and the elements retained by
|
||||
truncated diagnostic display must not depend on which implications were encountered first.
|
||||
|
||||
```py
|
||||
from typing import Literal, Never
|
||||
from ty_extensions import static_assert
|
||||
from ty_extensions._internal import ConstraintSet
|
||||
|
||||
def high_fanout[
|
||||
P,
|
||||
L0,
|
||||
L1,
|
||||
L2,
|
||||
L3,
|
||||
L4,
|
||||
L5,
|
||||
L6,
|
||||
L7,
|
||||
L8,
|
||||
L9,
|
||||
L10,
|
||||
L11,
|
||||
R0,
|
||||
R1,
|
||||
R2,
|
||||
R3,
|
||||
R4,
|
||||
R5,
|
||||
R6,
|
||||
R7,
|
||||
R8,
|
||||
R9,
|
||||
R10,
|
||||
R11,
|
||||
]() -> None:
|
||||
lower = (
|
||||
ConstraintSet.range(Literal[0], L0, P)
|
||||
& ConstraintSet.range(Literal[1], L1, P)
|
||||
& ConstraintSet.range(Literal[2], L2, P)
|
||||
& ConstraintSet.range(Literal[3], L3, P)
|
||||
& ConstraintSet.range(Literal[4], L4, P)
|
||||
& ConstraintSet.range(Literal[5], L5, P)
|
||||
& ConstraintSet.range(Literal[6], L6, P)
|
||||
& ConstraintSet.range(Literal[7], L7, P)
|
||||
& ConstraintSet.range(Literal[8], L8, P)
|
||||
& ConstraintSet.range(Literal[9], L9, P)
|
||||
& ConstraintSet.range(Literal[10], L10, P)
|
||||
& ConstraintSet.range(Literal[11], L11, P)
|
||||
)
|
||||
upper = (
|
||||
ConstraintSet.range(Never, P, R0)
|
||||
& ConstraintSet.range(Never, P, R1)
|
||||
& ConstraintSet.range(Never, P, R2)
|
||||
& ConstraintSet.range(Never, P, R3)
|
||||
& ConstraintSet.range(Never, P, R4)
|
||||
& ConstraintSet.range(Never, P, R5)
|
||||
& ConstraintSet.range(Never, P, R6)
|
||||
& ConstraintSet.range(Never, P, R7)
|
||||
& ConstraintSet.range(Never, P, R8)
|
||||
& ConstraintSet.range(Never, P, R9)
|
||||
& ConstraintSet.range(Never, P, R10)
|
||||
& ConstraintSet.range(Never, P, R11)
|
||||
)
|
||||
inferable = tuple[
|
||||
P,
|
||||
L0,
|
||||
L1,
|
||||
L2,
|
||||
L3,
|
||||
L4,
|
||||
L5,
|
||||
L6,
|
||||
L7,
|
||||
L8,
|
||||
L9,
|
||||
L10,
|
||||
L11,
|
||||
R0,
|
||||
R1,
|
||||
R2,
|
||||
R3,
|
||||
R4,
|
||||
R5,
|
||||
R6,
|
||||
R7,
|
||||
R8,
|
||||
R9,
|
||||
R10,
|
||||
R11,
|
||||
]
|
||||
constraints = lower & upper
|
||||
pivot = constraints.solutions_for(P, inferable=inferable)
|
||||
result = constraints.solutions_for(R11, inferable=inferable)
|
||||
|
||||
# TODO: inferred solutions should not retain the intermediate inferable typevars.
|
||||
# TODO: sometimes: revealed tuple[Solution[P=L0@high_fanout | Literal[0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11] | L1@high_fanout | L2@high_fanout | L3@high_fanout | L4@high_fanout | L5@high_fanout | L6@high_fanout | L7@high_fanout | L8@high_fanout | L9@high_fanout | L10@high_fanout | L11@high_fanout]]
|
||||
# TODO: sometimes: revealed tuple[Solution[P=L0@high_fanout | Literal[0, 3, 4, 5, 6, 7, 8, 9, 10, 11] | L1@high_fanout | L2@high_fanout | L3@high_fanout | L4@high_fanout | L5@high_fanout | L6@high_fanout | L7@high_fanout | L8@high_fanout | L9@high_fanout | L10@high_fanout | L11@high_fanout]]
|
||||
# TODO: sometimes: revealed tuple[Solution[P=L0@high_fanout | Literal[0, 1, 4, 5, 6, 7, 8, 9, 10, 11] | L1@high_fanout | L2@high_fanout | L3@high_fanout | L4@high_fanout | L5@high_fanout | L6@high_fanout | L7@high_fanout | L8@high_fanout | L9@high_fanout | L10@high_fanout | L11@high_fanout]]
|
||||
# TODO: sometimes: revealed tuple[Solution[P=L0@high_fanout | Literal[0, 1, 2, 5, 6, 7, 8, 9, 10, 11] | L1@high_fanout | L2@high_fanout | L3@high_fanout | L4@high_fanout | L5@high_fanout | L6@high_fanout | L7@high_fanout | L8@high_fanout | L9@high_fanout | L10@high_fanout | L11@high_fanout]]
|
||||
# TODO: sometimes: revealed tuple[Solution[P=L0@high_fanout | Literal[0, 1, 2, 3, 6, 7, 8, 9, 10, 11] | L1@high_fanout | L2@high_fanout | L3@high_fanout | L4@high_fanout | L5@high_fanout | L6@high_fanout | L7@high_fanout | L8@high_fanout | L9@high_fanout | L10@high_fanout | L11@high_fanout]]
|
||||
# TODO: sometimes: revealed tuple[Solution[P=L0@high_fanout | Literal[0, 1, 2, 3, 4, 5, 6, 9, 10, 11] | L1@high_fanout | L2@high_fanout | L3@high_fanout | L4@high_fanout | L5@high_fanout | L6@high_fanout | L7@high_fanout | L8@high_fanout | L9@high_fanout | L10@high_fanout | L11@high_fanout]]
|
||||
# revealed: tuple[Solution[P=L0@high_fanout | L1@high_fanout | L2@high_fanout | Literal[2, 3, 4, 5, 6, 7, 8, 9, 10, 11] | L3@high_fanout | L4@high_fanout | L5@high_fanout | L6@high_fanout | L7@high_fanout | L8@high_fanout | L9@high_fanout | L10@high_fanout | L11@high_fanout]]
|
||||
reveal_type(pivot)
|
||||
|
||||
# TODO: sometimes: revealed tuple[Solution[R11=P@high_fanout]]
|
||||
# TODO: sometimes: revealed tuple[Solution[R11=L0@high_fanout | L2@high_fanout | Literal[2, 3, 4, 5, 6, 7, 8, 9, 10, 11] | L3@high_fanout | L4@high_fanout | L5@high_fanout | L6@high_fanout | L7@high_fanout | L8@high_fanout | L9@high_fanout | L10@high_fanout | L11@high_fanout | P@high_fanout]]
|
||||
# TODO: sometimes: revealed tuple[Solution[R11=L0@high_fanout | Literal[0, 3, 4, 5, 6, 7, 8, 9, 10, 11] | L2@high_fanout | L3@high_fanout | L4@high_fanout | L5@high_fanout | L6@high_fanout | L7@high_fanout | L8@high_fanout | L9@high_fanout | L10@high_fanout | L11@high_fanout | P@high_fanout]]
|
||||
# TODO: sometimes: revealed tuple[Solution[R11=L0@high_fanout | Literal[0, 1, 4, 5, 6, 7, 8, 9, 10, 11] | L1@high_fanout | L3@high_fanout | L4@high_fanout | L5@high_fanout | L6@high_fanout | L7@high_fanout | L8@high_fanout | L9@high_fanout | L10@high_fanout | L11@high_fanout | P@high_fanout]]
|
||||
# TODO: sometimes: revealed tuple[Solution[R11=L0@high_fanout | Literal[0, 1, 5, 6, 7, 8, 9, 10, 11] | L1@high_fanout | L2@high_fanout | L4@high_fanout | L5@high_fanout | L6@high_fanout | L7@high_fanout | L8@high_fanout | L9@high_fanout | L10@high_fanout | L11@high_fanout | P@high_fanout]]
|
||||
# TODO: sometimes: revealed tuple[Solution[R11=L0@high_fanout | Literal[0, 1, 2, 3, 6, 7, 8, 9, 10, 11] | L1@high_fanout | L2@high_fanout | L3@high_fanout | L5@high_fanout | L6@high_fanout | L7@high_fanout | L8@high_fanout | L9@high_fanout | L10@high_fanout | L11@high_fanout | P@high_fanout]]
|
||||
# TODO: sometimes: revealed tuple[Solution[R11=L0@high_fanout | Literal[0, 1, 2, 3, 4, 5, 6, 9, 10, 11] | L1@high_fanout | L2@high_fanout | L3@high_fanout | L4@high_fanout | L5@high_fanout | L6@high_fanout | L8@high_fanout | L9@high_fanout | L10@high_fanout | L11@high_fanout | P@high_fanout]]
|
||||
# revealed: tuple[Solution[R11=L1@high_fanout | L2@high_fanout | Literal[2, 3, 4, 5, 6, 7, 8, 9, 10, 11] | L3@high_fanout | L4@high_fanout | L5@high_fanout | L6@high_fanout | L7@high_fanout | L8@high_fanout | L9@high_fanout | L10@high_fanout | L11@high_fanout | P@high_fanout]]
|
||||
reveal_type(result)
|
||||
|
||||
impossible = constraints & ConstraintSet.range(Never, R11, Literal[0])
|
||||
# TODO: sometimes: error [static-assert-error] "Static assertion error: argument evaluates to `False`"
|
||||
static_assert(not impossible.satisfied_by_all_typevars(inferable=inferable))
|
||||
```
|
||||
@@ -4089,6 +4089,22 @@ impl<'db> Type<'db> {
|
||||
))
|
||||
.into()
|
||||
}
|
||||
Type::KnownInstance(KnownInstanceType::ConstraintSet(tracked))
|
||||
if name == "solutions_for" =>
|
||||
{
|
||||
Place::bound(Type::KnownBoundMethod(
|
||||
KnownBoundMethodType::ConstraintSetSolutionsFor(tracked),
|
||||
))
|
||||
.into()
|
||||
}
|
||||
Type::KnownInstance(KnownInstanceType::ConstraintSet(tracked))
|
||||
if name == "solutions" =>
|
||||
{
|
||||
Place::bound(Type::KnownBoundMethod(
|
||||
KnownBoundMethodType::ConstraintSetSolutions(tracked),
|
||||
))
|
||||
.into()
|
||||
}
|
||||
Type::KnownInstance(KnownInstanceType::ConstraintSet(tracked))
|
||||
if name == "with_detailed_display" =>
|
||||
{
|
||||
@@ -6203,6 +6219,14 @@ impl<'db> Type<'db> {
|
||||
invalid_expressions: smallvec_inline![InvalidTypeExpression::ConstraintSet],
|
||||
fallback_type: Type::unknown(),
|
||||
}),
|
||||
KnownInstanceType::ConstraintSetSolution(__call__) => {
|
||||
Err(InvalidTypeExpressionError {
|
||||
invalid_expressions: smallvec_inline![
|
||||
InvalidTypeExpression::ConstraintSetSolution
|
||||
],
|
||||
fallback_type: Type::unknown(),
|
||||
})
|
||||
}
|
||||
KnownInstanceType::GenericContext(__call__) => Err(InvalidTypeExpressionError {
|
||||
invalid_expressions: smallvec_inline![InvalidTypeExpression::GenericContext],
|
||||
fallback_type: Type::unknown(),
|
||||
@@ -6497,6 +6521,7 @@ impl<'db> Type<'db> {
|
||||
| KnownInstanceType::Deprecated(_)
|
||||
| KnownInstanceType::Field(_)
|
||||
| KnownInstanceType::ConstraintSet(_)
|
||||
| KnownInstanceType::ConstraintSetSolution(_)
|
||||
| KnownInstanceType::GenericContext(_)
|
||||
| KnownInstanceType::Specialization(_)
|
||||
| KnownInstanceType::Literal(_)
|
||||
@@ -6514,6 +6539,8 @@ impl<'db> Type<'db> {
|
||||
| KnownBoundMethodType::ConstraintSetSatisfies(_)
|
||||
| KnownBoundMethodType::ConstraintSetForAll(_)
|
||||
| KnownBoundMethodType::ConstraintSetSatisfiedByAllTypeVars(_)
|
||||
| KnownBoundMethodType::ConstraintSetSolutionsFor(_)
|
||||
| KnownBoundMethodType::ConstraintSetSolutions(_)
|
||||
| KnownBoundMethodType::ConstraintSetWithDetailedDisplay(_)
|
||||
)
|
||||
) {
|
||||
@@ -6879,6 +6906,8 @@ impl<'db> Type<'db> {
|
||||
| KnownBoundMethodType::ConstraintSetSatisfies(_)
|
||||
| KnownBoundMethodType::ConstraintSetForAll(_)
|
||||
| KnownBoundMethodType::ConstraintSetSatisfiedByAllTypeVars(_)
|
||||
| KnownBoundMethodType::ConstraintSetSolutionsFor(_)
|
||||
| KnownBoundMethodType::ConstraintSetSolutions(_)
|
||||
| KnownBoundMethodType::ConstraintSetWithDetailedDisplay(_)
|
||||
)
|
||||
| Type::DataclassDecorator(_)
|
||||
@@ -7108,6 +7137,7 @@ impl<'db> Type<'db> {
|
||||
| KnownInstanceType::Deprecated(_)
|
||||
| KnownInstanceType::Field(_)
|
||||
| KnownInstanceType::ConstraintSet(_)
|
||||
| KnownInstanceType::ConstraintSetSolution(_)
|
||||
| KnownInstanceType::GenericContext(_)
|
||||
| KnownInstanceType::Specialization(_)
|
||||
| KnownInstanceType::Literal(_)
|
||||
@@ -7144,6 +7174,8 @@ impl<'db> Type<'db> {
|
||||
| KnownBoundMethodType::ConstraintSetSatisfies(_)
|
||||
| KnownBoundMethodType::ConstraintSetForAll(_)
|
||||
| KnownBoundMethodType::ConstraintSetSatisfiedByAllTypeVars(_)
|
||||
| KnownBoundMethodType::ConstraintSetSolutionsFor(_)
|
||||
| KnownBoundMethodType::ConstraintSetSolutions(_)
|
||||
| KnownBoundMethodType::ConstraintSetWithDetailedDisplay(_),
|
||||
)
|
||||
| Type::DataclassDecorator(_)
|
||||
@@ -8316,6 +8348,8 @@ enum InvalidTypeExpression<'db> {
|
||||
Field,
|
||||
/// Same for `ty_extensions._internal.ConstraintSet`
|
||||
ConstraintSet,
|
||||
/// Same for `ty_extensions._internal.ConstraintSetSolution`
|
||||
ConstraintSetSolution,
|
||||
/// Same for `ty_extensions._internal.GenericContext`
|
||||
GenericContext,
|
||||
/// Same for `ty_extensions._internal.Specialization`
|
||||
@@ -8385,6 +8419,10 @@ impl<'db> InvalidTypeExpression<'db> {
|
||||
f,
|
||||
"`ty_extensions._internal.ConstraintSet` is not allowed in {location}s",
|
||||
),
|
||||
InvalidTypeExpression::ConstraintSetSolution => write!(
|
||||
f,
|
||||
"`ty_extensions._internal.ConstraintSetSolution` is not allowed in {location}s",
|
||||
),
|
||||
InvalidTypeExpression::GenericContext => {
|
||||
write!(
|
||||
f,
|
||||
|
||||
@@ -51,7 +51,7 @@ use crate::types::generics::{
|
||||
TypeVarInference,
|
||||
};
|
||||
use crate::types::infer::original_class_type;
|
||||
use crate::types::known_instance::FieldInstance;
|
||||
use crate::types::known_instance::{FieldInstance, InternedConstraintSetSolution};
|
||||
use crate::types::signatures::{
|
||||
CallableSignature, Parameter, ParameterDisplayName, ParameterKind, Parameters, ParametersKind,
|
||||
PartialApplication, PartialSignatureApplication,
|
||||
@@ -2814,6 +2814,78 @@ impl<'db> Bindings<'db> {
|
||||
overload.set_return_type(Type::bool_literal(result));
|
||||
}
|
||||
|
||||
Type::KnownBoundMethod(KnownBoundMethodType::ConstraintSetSolutionsFor(
|
||||
tracked,
|
||||
)) => {
|
||||
let [Some(typevar), Some(inferable)] = overload.parameter_types() else {
|
||||
continue;
|
||||
};
|
||||
let Type::TypeVar(typevar) = typevar.project_type_form(db) else {
|
||||
continue;
|
||||
};
|
||||
let Type::NominalInstance(inferable) = inferable.project_type_form(db)
|
||||
else {
|
||||
continue;
|
||||
};
|
||||
let Some(inferable) = inferable_typevars_from_tuple(db, &inferable) else {
|
||||
continue;
|
||||
};
|
||||
|
||||
let constraints = ConstraintSetBuilder::new();
|
||||
let set = constraints.load(db, tracked.constraints(db));
|
||||
let result = match set.solutions(db, &constraints, inferable) {
|
||||
Solutions::Constrained(paths) => Type::heterogeneous_tuple(
|
||||
db,
|
||||
paths.into_iter().map(|path| {
|
||||
let path: Box<[_]> = path
|
||||
.into_iter()
|
||||
.filter(|binding| binding.bound_typevar == typevar)
|
||||
.collect();
|
||||
Type::KnownInstance(KnownInstanceType::ConstraintSetSolution(
|
||||
InternedConstraintSetSolution::new(db, path),
|
||||
))
|
||||
}),
|
||||
),
|
||||
Solutions::Unsatisfiable => Type::none(db),
|
||||
Solutions::Unconstrained => Type::empty_tuple(db),
|
||||
};
|
||||
overload.set_return_type(result);
|
||||
}
|
||||
|
||||
Type::KnownBoundMethod(KnownBoundMethodType::ConstraintSetSolutions(
|
||||
tracked,
|
||||
)) => {
|
||||
let [Some(inferable)] = overload.parameter_types() else {
|
||||
continue;
|
||||
};
|
||||
let Type::NominalInstance(inferable) = inferable.project_type_form(db)
|
||||
else {
|
||||
continue;
|
||||
};
|
||||
let Some(inferable) = inferable_typevars_from_tuple(db, &inferable) else {
|
||||
continue;
|
||||
};
|
||||
|
||||
let constraints = ConstraintSetBuilder::new();
|
||||
let set = constraints.load(db, tracked.constraints(db));
|
||||
let result = match set.solutions(db, &constraints, inferable) {
|
||||
Solutions::Constrained(paths) => Type::heterogeneous_tuple(
|
||||
db,
|
||||
paths.into_iter().map(|path| {
|
||||
Type::KnownInstance(KnownInstanceType::ConstraintSetSolution(
|
||||
InternedConstraintSetSolution::new(
|
||||
db,
|
||||
path.into_boxed_slice(),
|
||||
),
|
||||
))
|
||||
}),
|
||||
),
|
||||
Solutions::Unsatisfiable => Type::none(db),
|
||||
Solutions::Unconstrained => Type::empty_tuple(db),
|
||||
};
|
||||
overload.set_return_type(result);
|
||||
}
|
||||
|
||||
Type::KnownBoundMethod(
|
||||
KnownBoundMethodType::ConstraintSetWithDetailedDisplay(tracked),
|
||||
) => {
|
||||
|
||||
@@ -148,6 +148,7 @@ pub enum KnownClass {
|
||||
FunctoolsPartial,
|
||||
// ty_extensions
|
||||
ConstraintSet,
|
||||
ConstraintSetSolution,
|
||||
GenericContext,
|
||||
Specialization,
|
||||
TyExtensionsAsyncIterable,
|
||||
@@ -282,6 +283,7 @@ impl KnownClass {
|
||||
| Self::NamedTupleFallback
|
||||
| Self::NamedTupleLike
|
||||
| Self::ConstraintSet
|
||||
| Self::ConstraintSetSolution
|
||||
| Self::GenericContext
|
||||
| Self::Specialization
|
||||
| Self::ProtocolMeta
|
||||
@@ -393,6 +395,7 @@ impl KnownClass {
|
||||
| KnownClass::NamedTupleFallback
|
||||
| KnownClass::NamedTupleLike
|
||||
| KnownClass::ConstraintSet
|
||||
| KnownClass::ConstraintSetSolution
|
||||
| KnownClass::GenericContext
|
||||
| KnownClass::Specialization
|
||||
| KnownClass::TypedDictFallback
|
||||
@@ -504,6 +507,7 @@ impl KnownClass {
|
||||
| KnownClass::NamedTupleFallback
|
||||
| KnownClass::NamedTupleLike
|
||||
| KnownClass::ConstraintSet
|
||||
| KnownClass::ConstraintSetSolution
|
||||
| KnownClass::GenericContext
|
||||
| KnownClass::Specialization
|
||||
| KnownClass::TypedDictFallback
|
||||
@@ -617,6 +621,7 @@ impl KnownClass {
|
||||
| KnownClass::NamedTupleLike
|
||||
| KnownClass::NamedTupleFallback
|
||||
| KnownClass::ConstraintSet
|
||||
| KnownClass::ConstraintSetSolution
|
||||
| KnownClass::GenericContext
|
||||
| KnownClass::Specialization
|
||||
| KnownClass::BuiltinFunctionType
|
||||
@@ -736,6 +741,7 @@ impl KnownClass {
|
||||
| Self::KwOnly
|
||||
| Self::NamedTupleFallback
|
||||
| Self::ConstraintSet
|
||||
| Self::ConstraintSetSolution
|
||||
| Self::GenericContext
|
||||
| Self::Specialization
|
||||
| Self::TypedDictFallback
|
||||
@@ -857,6 +863,7 @@ impl KnownClass {
|
||||
| KnownClass::Path
|
||||
| KnownClass::FunctoolsPartial
|
||||
| KnownClass::ConstraintSet
|
||||
| KnownClass::ConstraintSetSolution
|
||||
| KnownClass::GenericContext
|
||||
| KnownClass::Specialization
|
||||
| KnownClass::PydanticBaseModel
|
||||
@@ -976,6 +983,7 @@ impl KnownClass {
|
||||
Self::NamedTupleFallback => "NamedTupleFallback",
|
||||
Self::NamedTupleLike => "NamedTupleLike",
|
||||
Self::ConstraintSet => "ConstraintSet",
|
||||
Self::ConstraintSetSolution => "ConstraintSetSolution",
|
||||
Self::GenericContext => "GenericContext",
|
||||
Self::Specialization => "Specialization",
|
||||
Self::TypedDictFallback => "TypedDictFallback",
|
||||
@@ -1375,6 +1383,7 @@ impl KnownClass {
|
||||
Self::NamedTupleFallback | Self::TypedDictFallback => KnownModule::TypeCheckerInternals,
|
||||
Self::NamedTupleLike => KnownModule::TyExtensions,
|
||||
Self::ConstraintSet
|
||||
| Self::ConstraintSetSolution
|
||||
| Self::GenericContext
|
||||
| Self::Specialization
|
||||
| Self::TyExtensionsAsyncIterable
|
||||
@@ -1487,6 +1496,7 @@ impl KnownClass {
|
||||
| Self::NamedTupleFallback
|
||||
| Self::NamedTupleLike
|
||||
| Self::ConstraintSet
|
||||
| Self::ConstraintSetSolution
|
||||
| Self::GenericContext
|
||||
| Self::Specialization
|
||||
| Self::TypedDictFallback
|
||||
@@ -1604,6 +1614,7 @@ impl KnownClass {
|
||||
| Self::NamedTupleFallback
|
||||
| Self::NamedTupleLike
|
||||
| Self::ConstraintSet
|
||||
| Self::ConstraintSetSolution
|
||||
| Self::GenericContext
|
||||
| Self::Specialization
|
||||
| Self::TypedDictFallback
|
||||
@@ -1721,6 +1732,7 @@ impl KnownClass {
|
||||
"NamedTupleFallback" => &[Self::NamedTupleFallback],
|
||||
"NamedTupleLike" => &[Self::NamedTupleLike],
|
||||
"ConstraintSet" => &[Self::ConstraintSet],
|
||||
"ConstraintSetSolution" => &[Self::ConstraintSetSolution],
|
||||
"GenericContext" => &[Self::GenericContext],
|
||||
"Specialization" => &[Self::Specialization],
|
||||
"TypedDictFallback" => &[Self::TypedDictFallback],
|
||||
@@ -1820,6 +1832,7 @@ impl KnownClass {
|
||||
| Self::Sentinel
|
||||
| Self::NamedTupleLike
|
||||
| Self::ConstraintSet
|
||||
| Self::ConstraintSetSolution
|
||||
| Self::GenericContext
|
||||
| Self::Specialization
|
||||
| Self::TyExtensionsAsyncIterable
|
||||
|
||||
@@ -228,6 +228,7 @@ impl<'db> ClassBase<'db> {
|
||||
| KnownInstanceType::Deprecated(_)
|
||||
| KnownInstanceType::Field(_)
|
||||
| KnownInstanceType::ConstraintSet(_)
|
||||
| KnownInstanceType::ConstraintSetSolution(_)
|
||||
| KnownInstanceType::Callable(_)
|
||||
| KnownInstanceType::GenericContext(_)
|
||||
| KnownInstanceType::Specialization(_)
|
||||
|
||||
@@ -92,7 +92,7 @@ use std::fmt::{Debug, Display};
|
||||
use std::iter;
|
||||
use std::marker::PhantomData;
|
||||
use std::ops::Range;
|
||||
use std::sync::Arc;
|
||||
use std::sync::{Arc, LazyLock};
|
||||
|
||||
use indexmap::map::Entry;
|
||||
use itertools::Itertools;
|
||||
@@ -100,6 +100,7 @@ use ruff_index::{Idx, IndexVec, newtype_index};
|
||||
use rustc_hash::{FxHashMap, FxHashSet};
|
||||
use smallvec::SmallVec;
|
||||
use ty_python_core::rank::RankBitBox;
|
||||
use ty_static::EnvVars;
|
||||
|
||||
use crate::types::class::GenericAlias;
|
||||
use crate::types::generics::InferableTypeVars;
|
||||
@@ -1337,7 +1338,45 @@ impl<'db> BoundTypeVarInstance<'db> {
|
||||
builder: &ConstraintSetBuilder<'db>,
|
||||
typevar: Self,
|
||||
) -> bool {
|
||||
builder.typevar_id(db, self).index() < builder.typevar_id(db, typevar).index()
|
||||
wobble_index(builder.typevar_id(db, self).index())
|
||||
< wobble_index(builder.typevar_id(db, typevar).index())
|
||||
}
|
||||
}
|
||||
|
||||
/// Optionally applies a transformation to a builder-local typevar or constraint ID, which lets us
|
||||
/// exercise different BDD variable orderings.
|
||||
///
|
||||
/// Under normal operation, the IDs won't be modified, and we will construct BDDs based on the
|
||||
/// (builder-local) source order that we encounter typevars and constraints.
|
||||
///
|
||||
/// Our results _shouldn't_ depend on the BDD variable ordering that we choose. You can use the
|
||||
/// `TY_CONSTRAINT_SET_ORDER` environment variable to artificially choose different permutations of
|
||||
/// the "natural" variable ordering, to ensure that results are consistent.
|
||||
fn wobble_index(index: usize) -> usize {
|
||||
#[derive(Clone, Copy)]
|
||||
enum Order {
|
||||
Normal,
|
||||
Reverse,
|
||||
Xor(usize),
|
||||
}
|
||||
|
||||
static ORDER: LazyLock<Order> = LazyLock::new(|| {
|
||||
let Some(value) = std::env::var_os(EnvVars::TY_CONSTRAINT_SET_ORDER) else {
|
||||
return Order::Normal;
|
||||
};
|
||||
if value == "reverse" {
|
||||
return Order::Reverse;
|
||||
}
|
||||
value
|
||||
.to_str()
|
||||
.and_then(|value| value.parse::<usize>().ok())
|
||||
.map_or(Order::Normal, Order::Xor)
|
||||
});
|
||||
|
||||
match *ORDER {
|
||||
Order::Normal => index,
|
||||
Order::Reverse => !index,
|
||||
Order::Xor(mask) => index ^ mask,
|
||||
}
|
||||
}
|
||||
|
||||
@@ -1964,7 +2003,7 @@ impl ConstraintId {
|
||||
/// empirically that we get smaller BDDs with an ordering that is more aligned with source
|
||||
/// order.
|
||||
fn ordering(self) -> impl Ord {
|
||||
std::cmp::Reverse(self.index())
|
||||
std::cmp::Reverse(wobble_index(self.index()))
|
||||
}
|
||||
|
||||
/// Returns whether this constraint implies another — i.e., whether every type that
|
||||
@@ -3754,8 +3793,8 @@ impl<'db> PathBounds<'db> {
|
||||
});
|
||||
|
||||
let mut result = Vec::with_capacity(sorted_paths.len());
|
||||
let mut mappings: FxHashMap<BoundTypeVarInstance<'db>, ConstraintBoundsBuilder<'db>> =
|
||||
FxHashMap::default();
|
||||
let mut mappings: FxIndexMap<BoundTypeVarInstance<'db>, ConstraintBoundsBuilder<'db>> =
|
||||
FxIndexMap::default();
|
||||
|
||||
for path in sorted_paths {
|
||||
mappings.clear();
|
||||
@@ -3784,7 +3823,7 @@ impl<'db> PathBounds<'db> {
|
||||
}
|
||||
|
||||
let path_bounds = mappings
|
||||
.drain()
|
||||
.drain(..)
|
||||
.map(|(bound_typevar, bounds)| bounds.finish(db, bound_typevar))
|
||||
.collect();
|
||||
result.push(path_bounds);
|
||||
@@ -3844,8 +3883,8 @@ impl<'db> PathBounds<'db> {
|
||||
}
|
||||
}
|
||||
|
||||
let mut mappings: FxHashMap<BoundTypeVarInstance<'db>, ConstraintBoundsBuilder<'db>> =
|
||||
FxHashMap::default();
|
||||
let mut mappings: FxIndexMap<BoundTypeVarInstance<'db>, ConstraintBoundsBuilder<'db>> =
|
||||
FxIndexMap::default();
|
||||
constraints.sort_by_key(|(_, _, source_order)| *source_order);
|
||||
for (typevar, constraint, _) in constraints {
|
||||
let bounds = mappings.entry(typevar).or_default();
|
||||
@@ -3858,7 +3897,7 @@ impl<'db> PathBounds<'db> {
|
||||
}
|
||||
|
||||
let path = mappings
|
||||
.drain()
|
||||
.drain(..)
|
||||
.map(|(bound_typevar, bounds)| bounds.finish(db, bound_typevar))
|
||||
.collect();
|
||||
Some(PathBounds::Constrained(Box::new([path])))
|
||||
@@ -5106,8 +5145,8 @@ pub(crate) enum Solutions<'db> {
|
||||
|
||||
pub(crate) type Solution<'db> = Vec<TypeVarSolution<'db>>;
|
||||
|
||||
#[derive(Clone, Debug, Eq, Hash, PartialEq, get_size2::GetSize)]
|
||||
pub(crate) struct TypeVarSolution<'db> {
|
||||
#[derive(Clone, Debug, Eq, Hash, PartialEq, get_size2::GetSize, salsa::SalsaValue)]
|
||||
pub struct TypeVarSolution<'db> {
|
||||
pub(crate) bound_typevar: BoundTypeVarInstance<'db>,
|
||||
pub(crate) solution: Type<'db>,
|
||||
}
|
||||
@@ -7621,6 +7660,224 @@ mod tests {
|
||||
});
|
||||
}
|
||||
|
||||
#[derive(Clone, Copy)]
|
||||
struct PermutedConstraint<'db>(
|
||||
BoundTypeVarInstance<'db>,
|
||||
Option<Type<'db>>,
|
||||
Option<Type<'db>>,
|
||||
);
|
||||
|
||||
impl<'db> PermutedConstraint<'db> {
|
||||
fn node(self, db: &'db dyn Db, builder: &ConstraintSetBuilder<'db>) -> NodeId {
|
||||
let PermutedConstraint(typevar, lower, upper) = self;
|
||||
Constraint::new_node_with_bounds(db, builder, typevar, lower, upper)
|
||||
}
|
||||
}
|
||||
|
||||
/// Tests that we get the same set of solutions for a constraint set, regardless of the
|
||||
/// variable ordering that is chosen for its "atoms" (the raw constraints that the constraint
|
||||
/// set is built from).
|
||||
///
|
||||
/// TODO: We _don't_ currently get a consistent result for each permutation. Right now,
|
||||
/// `expected` is a list of all of the different results that we get. Once we solve all of the
|
||||
/// sources of nondeterminism, `expected` should become a single string, and we should verify
|
||||
/// that we get that specific result for each permutation.
|
||||
#[track_caller]
|
||||
fn check_solutions_for_constraint_orderings<'db>(
|
||||
db: &'db dyn Db,
|
||||
typevars: &[BoundTypeVarInstance<'db>],
|
||||
atoms: &[PermutedConstraint<'db>],
|
||||
build_bdd: impl Fn(&ConstraintSetBuilder<'db>) -> NodeId,
|
||||
expected: impl IntoIterator<Item = &'static str>,
|
||||
) {
|
||||
let inferable = InferableTypeVars::from_typevars(
|
||||
db,
|
||||
typevars
|
||||
.iter()
|
||||
.map(|typevar| typevar.identity(db))
|
||||
.collect(),
|
||||
);
|
||||
let mut signatures = FxIndexSet::default();
|
||||
|
||||
for constraint_order in (0..atoms.len()).permutations(atoms.len()) {
|
||||
let builder = ConstraintSetBuilder::new();
|
||||
for typevar in typevars {
|
||||
builder.intern_typevar(db, *typevar);
|
||||
}
|
||||
for index in constraint_order {
|
||||
let PermutedConstraint(typevar, lower, upper) = atoms[index];
|
||||
builder.intern_constraint(
|
||||
db,
|
||||
Constraint {
|
||||
typevar,
|
||||
bounds: ConstraintBounds::new(lower, upper),
|
||||
},
|
||||
);
|
||||
}
|
||||
|
||||
let set = ConstraintSet::from_node(&builder, build_bdd(&builder));
|
||||
let solutions = set.solutions(db, &builder, inferable);
|
||||
let mut merged = FxHashMap::default();
|
||||
if let Solutions::Constrained(paths) = &solutions {
|
||||
for path in paths {
|
||||
for binding in path {
|
||||
merged
|
||||
.entry(binding.bound_typevar)
|
||||
.and_modify(|existing| {
|
||||
*existing =
|
||||
UnionType::from_two_elements(db, *existing, binding.solution);
|
||||
})
|
||||
.or_insert(binding.solution);
|
||||
}
|
||||
}
|
||||
}
|
||||
let merged = typevars
|
||||
.iter()
|
||||
.filter_map(|typevar| {
|
||||
merged.get(typevar).map(|ty| {
|
||||
format!("{}={}", typevar.identity(db).display(db), ty.display(db))
|
||||
})
|
||||
})
|
||||
.join(", ");
|
||||
let paths = match &solutions {
|
||||
Solutions::Unsatisfiable => String::from("unsatisfiable"),
|
||||
Solutions::Unconstrained => String::from("unconstrained"),
|
||||
Solutions::Constrained(paths) => paths
|
||||
.iter()
|
||||
.map(|path| {
|
||||
path.iter()
|
||||
.map(|binding| {
|
||||
format!(
|
||||
"{}={}",
|
||||
binding.bound_typevar.identity(db).display(db),
|
||||
binding.solution.display(db)
|
||||
)
|
||||
})
|
||||
.join(", ")
|
||||
})
|
||||
.join("; "),
|
||||
};
|
||||
signatures.insert(format!(
|
||||
"never={} always={} merged=[{merged}] paths=[{paths}]",
|
||||
set.is_never_satisfied(db),
|
||||
set.is_always_satisfied(db),
|
||||
));
|
||||
}
|
||||
|
||||
let expected: FxIndexSet<_> = expected.into_iter().map(String::from).collect();
|
||||
assert_eq!(signatures, expected);
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn constraint_ordering_changes_nested_transitive_solutions() {
|
||||
let db = setup_db();
|
||||
let t = create_typevar(&db, "T");
|
||||
let u = create_typevar(&db, "U");
|
||||
let v = create_typevar(&db, "V");
|
||||
let int = KnownClass::Int.to_instance(&db);
|
||||
let bytes = KnownClass::Bytes.to_instance(&db);
|
||||
let list_u = KnownClass::List.to_specialized_instance(&db, &[Type::TypeVar(u)]);
|
||||
let list_int = KnownClass::List.to_specialized_instance(&db, &[int]);
|
||||
let atoms = [
|
||||
PermutedConstraint(t, None, Some(list_u)),
|
||||
PermutedConstraint(u, None, Some(int)),
|
||||
PermutedConstraint(t, Some(list_int), None),
|
||||
PermutedConstraint(v, Some(bytes), None),
|
||||
];
|
||||
|
||||
check_solutions_for_constraint_orderings(
|
||||
&db,
|
||||
&[t, u, v],
|
||||
&atoms,
|
||||
|builder| {
|
||||
let [t_list_u, u_int, list_int_t, bytes_v] =
|
||||
atoms.map(|atom| atom.node(&db, builder));
|
||||
t_list_u
|
||||
.and_with_offset(builder, u_int)
|
||||
.and_with_offset(builder, list_int_t)
|
||||
.or_with_offset(builder, bytes_v)
|
||||
},
|
||||
// TODO: All permutations should produce the first result. TDD traversal currently
|
||||
// leaks irrelevant positive constraints onto the `V = bytes` alternative.
|
||||
[
|
||||
"never=false always=false merged=[T=list[int], U=int, V=bytes] paths=[T=list[int], U=int; V=bytes]",
|
||||
"never=false always=false merged=[T=list[int], U=int, V=bytes] paths=[T=list[int], U=int; T=list[int], V=bytes; V=bytes]",
|
||||
"never=false always=false merged=[T=list[int], U=int, V=bytes] paths=[T=list[int], U=int; U=int, V=bytes; V=bytes]",
|
||||
"never=false always=false merged=[T=list[int] | list[U], U=int, V=bytes] paths=[T=list[int], U=int; T=list[U], V=bytes; V=bytes]",
|
||||
],
|
||||
);
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn constraint_ordering_changes_negated_alternative_solutions() {
|
||||
let db = setup_db();
|
||||
let t = create_typevar(&db, "T");
|
||||
let u = create_typevar(&db, "U");
|
||||
let int = KnownClass::Int.to_instance(&db);
|
||||
let str = KnownClass::Str.to_instance(&db);
|
||||
let bytes = KnownClass::Bytes.to_instance(&db);
|
||||
let atoms = [
|
||||
PermutedConstraint(t, None, Some(int)),
|
||||
PermutedConstraint(t, None, Some(str)),
|
||||
PermutedConstraint(u, Some(bytes), None),
|
||||
];
|
||||
|
||||
check_solutions_for_constraint_orderings(
|
||||
&db,
|
||||
&[t, u],
|
||||
&atoms,
|
||||
|builder| {
|
||||
let [t_int, t_str, bytes_u] = atoms.map(|atom| atom.node(&db, builder));
|
||||
t_int
|
||||
.or_with_offset(builder, t_str)
|
||||
.negate(builder)
|
||||
.or_with_offset(builder, bytes_u)
|
||||
},
|
||||
// TODO: All permutations should produce the first result. A satisfied alternative
|
||||
// should not infer `T` from unrelated positive decisions made earlier in a BDD path.
|
||||
[
|
||||
"never=false always=false merged=[U=bytes] paths=[; U=bytes]",
|
||||
"never=false always=false merged=[T=str, U=bytes] paths=[; T=str, U=bytes; U=bytes]",
|
||||
"never=false always=false merged=[T=int, U=bytes] paths=[; T=int, U=bytes; U=bytes]",
|
||||
],
|
||||
);
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn constraint_ordering_changes_derived_upper_bound_display() {
|
||||
let db = setup_db();
|
||||
let t = create_typevar(&db, "T");
|
||||
let u = create_typevar(&db, "U");
|
||||
let int = KnownClass::Int.to_instance(&db);
|
||||
let str = KnownClass::Str.to_instance(&db);
|
||||
let atoms = [
|
||||
PermutedConstraint(t, None, Some(int)),
|
||||
PermutedConstraint(t, None, Some(str)),
|
||||
PermutedConstraint(t, Some(int), None),
|
||||
PermutedConstraint(u, None, Some(int)),
|
||||
];
|
||||
|
||||
check_solutions_for_constraint_orderings(
|
||||
&db,
|
||||
&[t, u],
|
||||
&atoms,
|
||||
|builder| {
|
||||
let [t_int, t_str, int_t, u_int] = atoms.map(|atom| atom.node(&db, builder));
|
||||
t_int
|
||||
.or_with_offset(builder, t_str)
|
||||
.and_with_offset(builder, int_t)
|
||||
.and_with_offset(builder, u_int)
|
||||
},
|
||||
// TODO: `SequentMap::for_constraint_pair` can receive its inputs in BDD order, not
|
||||
// source order. That changes which equivalent upper-bound intersection is constructed
|
||||
// first.
|
||||
[
|
||||
"never=false always=false merged=[T=int | U, U=T & int] paths=[T=int | U, U=T & int]",
|
||||
"never=false always=false merged=[T=int | U, U=int & T] paths=[T=int | U, U=int & T]",
|
||||
],
|
||||
);
|
||||
}
|
||||
|
||||
#[track_caller]
|
||||
fn check_display_graph<'db, 'c>(
|
||||
db: &'db dyn Db,
|
||||
|
||||
@@ -1226,6 +1226,12 @@ impl<'db> FmtDetailed<'db> for DisplayRepresentation<'db> {
|
||||
return f
|
||||
.write_str("bound method `ConstraintSet.satisfied_by_all_typevars`");
|
||||
}
|
||||
KnownBoundMethodType::ConstraintSetSolutionsFor(_) => {
|
||||
return f.write_str("bound method `ConstraintSet.solutions_for`");
|
||||
}
|
||||
KnownBoundMethodType::ConstraintSetSolutions(_) => {
|
||||
return f.write_str("bound method `ConstraintSet.solutions`");
|
||||
}
|
||||
KnownBoundMethodType::ConstraintSetWithDetailedDisplay(_) => {
|
||||
return f.write_str("bound method `ConstraintSet.with_detailed_display`");
|
||||
}
|
||||
@@ -3194,17 +3200,19 @@ impl Display for DisplayStringLiteralType<'_> {
|
||||
pub(crate) struct DisplayKnownInstanceRepr<'db> {
|
||||
pub(crate) known_instance: KnownInstanceType<'db>,
|
||||
pub(crate) db: &'db dyn Db,
|
||||
pub(crate) settings: DisplaySettings<'db>,
|
||||
}
|
||||
|
||||
impl<'db> KnownInstanceType<'db> {
|
||||
pub(crate) fn display_with(
|
||||
self,
|
||||
db: &'db dyn Db,
|
||||
_settings: DisplaySettings<'db>,
|
||||
settings: DisplaySettings<'db>,
|
||||
) -> DisplayKnownInstanceRepr<'db> {
|
||||
DisplayKnownInstanceRepr {
|
||||
known_instance: self,
|
||||
db,
|
||||
settings,
|
||||
}
|
||||
}
|
||||
}
|
||||
@@ -3290,6 +3298,21 @@ impl<'db> FmtDetailed<'db> for DisplayKnownInstanceRepr<'db> {
|
||||
f.write_str("[bool]")
|
||||
}
|
||||
}
|
||||
KnownInstanceType::ConstraintSetSolution(solution) => {
|
||||
f.set_invalid_type_annotation();
|
||||
f.with_type(ty).write_str("Solution[")?;
|
||||
for (index, binding) in solution.bindings(self.db).iter().enumerate() {
|
||||
if index > 0 {
|
||||
f.write_str(", ")?;
|
||||
}
|
||||
write!(f, "{}=", binding.bound_typevar.name(self.db))?;
|
||||
binding
|
||||
.solution
|
||||
.display_with(self.db, self.settings.clone())
|
||||
.fmt_detailed(f)?;
|
||||
}
|
||||
f.write_char(']')
|
||||
}
|
||||
KnownInstanceType::GenericContext(generic_context) => {
|
||||
f.with_type(ty)
|
||||
.write_str("ty_extensions._internal.GenericContext")?;
|
||||
|
||||
@@ -1556,6 +1556,18 @@ impl<'db> TypeInferenceBuilder<'db, '_> {
|
||||
}
|
||||
Type::unknown()
|
||||
}
|
||||
KnownInstanceType::ConstraintSetSolution(_) => {
|
||||
if !self.in_string_annotation() {
|
||||
self.infer_expression(slice, TypeContext::default());
|
||||
}
|
||||
if let Some(builder) = self.context.report_lint(&INVALID_TYPE_FORM, subscript) {
|
||||
builder.into_diagnostic(format_args!(
|
||||
"`ty_extensions._internal.ConstraintSetSolution` is not allowed in {}s",
|
||||
self.type_expression_context(),
|
||||
));
|
||||
}
|
||||
Type::unknown()
|
||||
}
|
||||
KnownInstanceType::GenericContext(_) => {
|
||||
if !self.in_string_annotation() {
|
||||
self.infer_expression(slice, TypeContext::default());
|
||||
|
||||
@@ -9,7 +9,7 @@ use crate::{
|
||||
PromotionKind, PromotionMode, StringLiteralType, Type, TypeAliasType, TypeContext,
|
||||
TypeMapping, TypeVarNonce, TypeVarVariance, UnionBuilder,
|
||||
class::NamedTupleSpec,
|
||||
constraints::OwnedConstraintSet,
|
||||
constraints::{OwnedConstraintSet, TypeVarSolution},
|
||||
dedicated::pydantic::ConfigBoolean,
|
||||
generics::{Specialization, walk_generic_context},
|
||||
newtype::NewType,
|
||||
@@ -48,6 +48,16 @@ impl<'db> InternedConstraintSet<'db> {
|
||||
}
|
||||
}
|
||||
|
||||
/// A Salsa-interned solution path exposed to mdtests as `ConstraintSetSolution`.
|
||||
#[salsa::interned(debug, heap_size=ruff_memory_usage::heap_size)]
|
||||
pub struct InternedConstraintSetSolution<'db> {
|
||||
#[returns(ref)]
|
||||
pub(super) bindings: Box<[TypeVarSolution<'db>]>,
|
||||
}
|
||||
|
||||
// The Salsa heap is tracked separately.
|
||||
impl get_size2::GetSize for InternedConstraintSetSolution<'_> {}
|
||||
|
||||
/// A salsa-interned payload for `functools.partial(...)` instances.
|
||||
#[salsa::interned(debug, heap_size=ruff_memory_usage::heap_size)]
|
||||
pub struct FunctoolsPartialInstance<'db> {
|
||||
@@ -99,6 +109,10 @@ pub enum KnownInstanceType<'db> {
|
||||
/// `ty_extensions._internal.ConstraintSet`.
|
||||
ConstraintSet(InternedConstraintSet<'db>),
|
||||
|
||||
/// A solution path, which is exposed in mdtests as an instance of
|
||||
/// `ty_extensions._internal.ConstraintSetSolution`.
|
||||
ConstraintSetSolution(InternedConstraintSetSolution<'db>),
|
||||
|
||||
/// A generic context, which is exposed in mdtests as an instance of
|
||||
/// `ty_extensions._internal.GenericContext`.
|
||||
GenericContext(GenericContext<'db>),
|
||||
@@ -170,6 +184,11 @@ pub(super) fn walk_known_instance_type<'db, V: visitor::TypeVisitor<'db> + ?Size
|
||||
| KnownInstanceType::Specialization(_) => {
|
||||
// Nothing to visit
|
||||
}
|
||||
KnownInstanceType::ConstraintSetSolution(solution) => {
|
||||
for binding in solution.bindings(db) {
|
||||
visitor.visit_type(db, binding.solution);
|
||||
}
|
||||
}
|
||||
KnownInstanceType::Field(field) => {
|
||||
if let Some(default_ty) = field.default_type(db) {
|
||||
visitor.visit_type(db, default_ty);
|
||||
@@ -236,6 +255,7 @@ impl<'db> KnownInstanceType<'db> {
|
||||
Self::Deprecated(deprecated) => Some(Self::Deprecated(deprecated)),
|
||||
Self::Range { is_non_empty } => Some(Self::Range { is_non_empty }),
|
||||
Self::ConstraintSet(set) => Some(Self::ConstraintSet(set)),
|
||||
Self::ConstraintSetSolution(solution) => Some(Self::ConstraintSetSolution(solution)),
|
||||
Self::TypeVar(typevar) => Some(Self::TypeVar(typevar)),
|
||||
Self::TypeAliasType(type_alias) => Some(Self::TypeAliasType(type_alias)),
|
||||
Self::Field(field) => field
|
||||
@@ -296,6 +316,7 @@ impl<'db> KnownInstanceType<'db> {
|
||||
Self::Deprecated(_) => KnownClass::Deprecated,
|
||||
Self::Field(_) => KnownClass::Field,
|
||||
Self::ConstraintSet(_) => KnownClass::ConstraintSet,
|
||||
Self::ConstraintSetSolution(_) => KnownClass::ConstraintSetSolution,
|
||||
Self::GenericContext(_) => KnownClass::GenericContext,
|
||||
Self::Specialization(_) => KnownClass::Specialization,
|
||||
Self::UnionType(_) => KnownClass::UnionType,
|
||||
@@ -449,6 +470,7 @@ impl<'db> KnownInstanceType<'db> {
|
||||
| KnownInstanceType::Deprecated(_)
|
||||
| KnownInstanceType::Field(_)
|
||||
| KnownInstanceType::ConstraintSet(_)
|
||||
| KnownInstanceType::ConstraintSetSolution(_)
|
||||
| KnownInstanceType::GenericContext(_)
|
||||
| KnownInstanceType::Specialization(_)
|
||||
| KnownInstanceType::Literal(_)
|
||||
|
||||
@@ -224,6 +224,8 @@ pub enum KnownBoundMethodType<'db> {
|
||||
ConstraintSetSatisfies(InternedConstraintSet<'db>),
|
||||
ConstraintSetForAll(InternedConstraintSet<'db>),
|
||||
ConstraintSetSatisfiedByAllTypeVars(InternedConstraintSet<'db>),
|
||||
ConstraintSetSolutionsFor(InternedConstraintSet<'db>),
|
||||
ConstraintSetSolutions(InternedConstraintSet<'db>),
|
||||
ConstraintSetWithDetailedDisplay(InternedConstraintSet<'db>),
|
||||
}
|
||||
|
||||
@@ -261,6 +263,8 @@ pub(super) fn walk_method_wrapper_type<'db, V: visitor::TypeVisitor<'db> + ?Size
|
||||
| KnownBoundMethodType::ConstraintSetSatisfies(_)
|
||||
| KnownBoundMethodType::ConstraintSetForAll(_)
|
||||
| KnownBoundMethodType::ConstraintSetSatisfiedByAllTypeVars(_)
|
||||
| KnownBoundMethodType::ConstraintSetSolutionsFor(_)
|
||||
| KnownBoundMethodType::ConstraintSetSolutions(_)
|
||||
| KnownBoundMethodType::ConstraintSetWithDetailedDisplay(_) => {}
|
||||
}
|
||||
}
|
||||
@@ -306,6 +310,8 @@ impl<'db> KnownBoundMethodType<'db> {
|
||||
| KnownBoundMethodType::ConstraintSetSatisfies(_)
|
||||
| KnownBoundMethodType::ConstraintSetForAll(_)
|
||||
| KnownBoundMethodType::ConstraintSetSatisfiedByAllTypeVars(_)
|
||||
| KnownBoundMethodType::ConstraintSetSolutionsFor(_)
|
||||
| KnownBoundMethodType::ConstraintSetSolutions(_)
|
||||
| KnownBoundMethodType::ConstraintSetWithDetailedDisplay(_) => Some(self),
|
||||
}
|
||||
}
|
||||
@@ -326,6 +332,8 @@ impl<'db> KnownBoundMethodType<'db> {
|
||||
| KnownBoundMethodType::ConstraintSetSatisfies(_)
|
||||
| KnownBoundMethodType::ConstraintSetForAll(_)
|
||||
| KnownBoundMethodType::ConstraintSetSatisfiedByAllTypeVars(_)
|
||||
| KnownBoundMethodType::ConstraintSetSolutionsFor(_)
|
||||
| KnownBoundMethodType::ConstraintSetSolutions(_)
|
||||
| KnownBoundMethodType::ConstraintSetWithDetailedDisplay(_) => {
|
||||
KnownClass::ConstraintSet
|
||||
}
|
||||
@@ -511,6 +519,47 @@ impl<'db> KnownBoundMethodType<'db> {
|
||||
)))
|
||||
}
|
||||
|
||||
KnownBoundMethodType::ConstraintSetSolutionsFor(_) => {
|
||||
Either::Right(std::iter::once(Signature::new(
|
||||
Parameters::standard([
|
||||
Parameter::positional_only(Some(Name::new_static("typevar")))
|
||||
.with_annotated_type(object_type_form()),
|
||||
Parameter::keyword_only(Name::new_static("inferable")).with_annotated_type(
|
||||
TypeFormType::from_type_expression(
|
||||
db,
|
||||
Type::homogeneous_tuple(db, Type::object()),
|
||||
),
|
||||
),
|
||||
]),
|
||||
UnionType::from_two_elements(
|
||||
db,
|
||||
Type::homogeneous_tuple(
|
||||
db,
|
||||
KnownClass::ConstraintSetSolution.to_instance(db),
|
||||
),
|
||||
Type::none(db),
|
||||
),
|
||||
)))
|
||||
}
|
||||
|
||||
KnownBoundMethodType::ConstraintSetSolutions(_) => {
|
||||
Either::Right(std::iter::once(Signature::new(
|
||||
Parameters::standard([Parameter::keyword_only(Name::new_static("inferable"))
|
||||
.with_annotated_type(TypeFormType::from_type_expression(
|
||||
db,
|
||||
Type::homogeneous_tuple(db, Type::object()),
|
||||
))]),
|
||||
UnionType::from_two_elements(
|
||||
db,
|
||||
Type::homogeneous_tuple(
|
||||
db,
|
||||
KnownClass::ConstraintSetSolution.to_instance(db),
|
||||
),
|
||||
Type::none(db),
|
||||
),
|
||||
)))
|
||||
}
|
||||
|
||||
KnownBoundMethodType::ConstraintSetWithDetailedDisplay(_) => {
|
||||
Either::Right(std::iter::once(Signature::new(
|
||||
Parameters::empty(),
|
||||
@@ -584,6 +633,14 @@ impl<'c, 'db> TypeRelationChecker<'_, 'c, 'db> {
|
||||
KnownBoundMethodType::ConstraintSetSatisfiedByAllTypeVars(_),
|
||||
KnownBoundMethodType::ConstraintSetSatisfiedByAllTypeVars(_),
|
||||
)
|
||||
| (
|
||||
KnownBoundMethodType::ConstraintSetSolutionsFor(_),
|
||||
KnownBoundMethodType::ConstraintSetSolutionsFor(_),
|
||||
)
|
||||
| (
|
||||
KnownBoundMethodType::ConstraintSetSolutions(_),
|
||||
KnownBoundMethodType::ConstraintSetSolutions(_),
|
||||
)
|
||||
| (
|
||||
KnownBoundMethodType::ConstraintSetWithDetailedDisplay(_),
|
||||
KnownBoundMethodType::ConstraintSetWithDetailedDisplay(_),
|
||||
@@ -603,6 +660,8 @@ impl<'c, 'db> TypeRelationChecker<'_, 'c, 'db> {
|
||||
| KnownBoundMethodType::ConstraintSetSatisfies(_)
|
||||
| KnownBoundMethodType::ConstraintSetForAll(_)
|
||||
| KnownBoundMethodType::ConstraintSetSatisfiedByAllTypeVars(_)
|
||||
| KnownBoundMethodType::ConstraintSetSolutionsFor(_)
|
||||
| KnownBoundMethodType::ConstraintSetSolutions(_)
|
||||
| KnownBoundMethodType::ConstraintSetWithDetailedDisplay(_),
|
||||
KnownBoundMethodType::FunctionTypeDunderGet(_)
|
||||
| KnownBoundMethodType::FunctionTypeDunderCall(_)
|
||||
@@ -617,6 +676,8 @@ impl<'c, 'db> TypeRelationChecker<'_, 'c, 'db> {
|
||||
| KnownBoundMethodType::ConstraintSetSatisfies(_)
|
||||
| KnownBoundMethodType::ConstraintSetForAll(_)
|
||||
| KnownBoundMethodType::ConstraintSetSatisfiedByAllTypeVars(_)
|
||||
| KnownBoundMethodType::ConstraintSetSolutionsFor(_)
|
||||
| KnownBoundMethodType::ConstraintSetSolutions(_)
|
||||
| KnownBoundMethodType::ConstraintSetWithDetailedDisplay(_),
|
||||
) => self.never(),
|
||||
}
|
||||
|
||||
@@ -264,6 +264,8 @@ impl<'db> Type<'db> {
|
||||
| KnownBoundMethodType::ConstraintSetSatisfies(_)
|
||||
| KnownBoundMethodType::ConstraintSetForAll(_)
|
||||
| KnownBoundMethodType::ConstraintSetSatisfiedByAllTypeVars(_)
|
||||
| KnownBoundMethodType::ConstraintSetSolutionsFor(_)
|
||||
| KnownBoundMethodType::ConstraintSetSolutions(_)
|
||||
| KnownBoundMethodType::ConstraintSetWithDetailedDisplay(_),
|
||||
)
|
||||
| Type::DataclassDecorator(_)
|
||||
|
||||
@@ -32,6 +32,13 @@ impl EnvVars {
|
||||
#[attr_hidden]
|
||||
pub const TY_MEMORY_REPORT: &'static str = "TY_MEMORY_REPORT";
|
||||
|
||||
/// Perturbs constraint-set variable ordering to help detect order-dependent inference.
|
||||
///
|
||||
/// Set to `reverse` to reverse builder-local IDs, or to an integer to select an arbitrary
|
||||
/// permutation of the naturally chosen variable ordering.
|
||||
#[attr_hidden]
|
||||
pub const TY_CONSTRAINT_SET_ORDER: &'static str = "TY_CONSTRAINT_SET_ORDER";
|
||||
|
||||
/// Specifies an upper limit for the number of tasks ty is allowed to run in parallel.
|
||||
///
|
||||
/// For example, how many files should be checked in parallel.
|
||||
|
||||
@@ -79,6 +79,9 @@ used by ty and cannot be used in annotations.
|
||||
# Constraints
|
||||
# -----------
|
||||
|
||||
class ConstraintSetSolution:
|
||||
"""One solution path for a constraint set."""
|
||||
|
||||
class ConstraintSet:
|
||||
@staticmethod
|
||||
def range(
|
||||
@@ -129,6 +132,31 @@ class ConstraintSet:
|
||||
constraint set will be considered non-inferable.
|
||||
"""
|
||||
|
||||
def solutions_for(
|
||||
self,
|
||||
typevar: TypeForm[object],
|
||||
*,
|
||||
inferable: TypeForm[tuple[object, ...]],
|
||||
) -> tuple[ConstraintSetSolution, ...] | None:
|
||||
"""
|
||||
Returns the explicit solutions inferred for `typevar` across all paths.
|
||||
|
||||
`inferable` specifies all typevars that should be solved for. Every
|
||||
solution path is preserved, with its bindings filtered to `typevar`.
|
||||
Returns `None` if the constraint set is unsatisfiable.
|
||||
"""
|
||||
|
||||
def solutions(
|
||||
self, *, inferable: TypeForm[tuple[object, ...]]
|
||||
) -> tuple[ConstraintSetSolution, ...] | None:
|
||||
"""
|
||||
Returns all explicit solutions, preserving path and binding order.
|
||||
|
||||
`inferable` specifies all typevars that should be solved for. Each
|
||||
solution contains the bindings inferred on one satisfying path.
|
||||
Returns `None` if the constraint set is unsatisfiable.
|
||||
"""
|
||||
|
||||
def __bool__(self) -> bool: ...
|
||||
def __eq__(self, other: ConstraintSet) -> bool: ...
|
||||
def __ne__(self, other: ConstraintSet) -> bool: ...
|
||||
|
||||
Reference in new issue
Block a user