深入 ty 类型检查器：ConstraintSet 约束集求解的顺序稳定性与 BDD 变量排序-开发者社区

深入 ty 类型检查器：ConstraintSet 约束集求解的顺序稳定性与 BDD 变量排序

【免费下载链接】ruffAn extremely fast Python linter and code formatter, written in Rust.项目地址: https://gitcode.com/GitHub_Trending/ru/ruff

ty是 Ruff 仓库中基于 Rust 实现的类型检查器。在类型推断过程中，约束求解器会把"在一组约束下某个类型性质成立"的状态表示为约束集（ConstraintSet），其底层由BDD（二元决策图）承载。本篇以 constraint_set_ordering.md 这份 mdtest 回归测试规格为核心，系统讲解ty如何保证约束集求解结果不依赖 BDD 变量的内部排序、solutions/solutions_for的语义差异、TY_CONSTRAINT_SET_ORDER环境变量如何打乱变量顺序以暴露不稳定输出，并逐条剖析文档中覆盖的 12 类稳定性测试场景。读完本文，你将理解 ty 约束求解器"确定性输出"的测试方法论，并能自行运行、扩展这些稳定性回归用例。

一、背景：约束集、路径与 BDD

1.1 什么是 ConstraintSet

在ty的类型推断管线中，求解过程并不是逐个类型变量独立进行的，而是维护一组同时成立的约束。源码中对这一抽象有明确定义：

结构体 ConstraintSet（定义于crates/ty_python_semantic/src/types/constraints.rs）注释中说明，它是一组"在该约束下某个类型性质成立"的约束集合，在论文记号中记为𝒮（"set of constraint sets"），对应 POPL 2015 年发表的约束求解相关理论框架；
其内部由三部分组成：node（表示该约束集的 BDD 根节点）、source_order（约束在约束集中被加入的源码顺序，终结节点上为None）、以及指向ConstraintSetBuilder的引用。source_order的存在说明约束集在语义之外还保留着约束引入时的源码先后顺序——这正是本文主题"顺序稳定性"的数据基础。

从源码结构可以推断：BDD 的变量（即单个约束）顺序会影响中间规约路径的形态；而约束集的source_order机制则用于在求解时尽量还原"源码顺序"，从而缓解变量排序对输出的扰动。

1.2 solutions 与 solutions_for 的区别

文档开篇即点明两个关键 API 的差异：

ConstraintSet.solutions_for：逐类型变量地暴露每一个显式解（explicit per-typevar solution），即针对某个指定类型变量返回它在各 BDD 路径上的解；
ConstraintSet.solutions：在solutions_for的基础上额外保留路径顺序（path order）与绑定顺序（binding order），使得在路径被 union 合并时本会消失的重复解与Never解依然可见。

两者的实现都汇聚在 projection.rs 的solutions与solutions_with中：solutions_with先把 BDD 展开为带边界的有界路径（bounded_path_bounds），再通过调用方提供的选择器choose对每条路径求解，最后按源码顺序汇总。也就是说，投影（projection）的确定性既依赖 BDD 展开的稳定，也依赖后续路径排序的稳定。

二、为什么要做顺序稳定性测试

文档明确指出当前实现的状态：

当前实现是stable的——对同一份源码多次运行ty会得到相同结果；但仍有一些残留位置，其输出依赖于选定的 BDD 变量顺序。

换句话说，"多运行几次结果一致"（运行间确定性）已经达成，但"无论内部采用哪种变量排序结果都一致"（排序无关性）尚未完全达成。文档中的每个# TODO: sometimes:注释都记录了一个在不同变量排序下可能出现的替代输出，而注释下方的# revealed:则是默认稳定排序下期望的输出。

这正是该 mdtest 回归文件的定位：用可执行用例锁定"默认排序下"的稳定输出，同时用 TODO 注释记录"其他排序下"可能出现的偏差，防止未经察觉的回归。对于类型检查器而言，输出不稳定意味着相同的源码在不同调用路径、不同缓存状态或未来版本中可能得到不同的类型诊断，因此这类测试直接关系到用户体验与结果可复现性。

三、核心测试开关：TY_CONSTRAINT_SET_ORDER

文档给出了验证方法：设置环境变量TY_CONSTRAINT_SET_ORDER为reverse或一个整数，即可在每次运行ty时选择不同的变量排列；仓库还提供wobbling-ty-constraint-order这一 Agent 技能来自动化该流程。

该环境变量在 env_vars.rs 中注册：

设为reverse时，反转builder 局部的类型变量/约束 ID；
设为整数时，选择对自然变量顺序的任意一个置换（通过按位异或掩码实现）。

其底层实现是 constraints.rs 中的wobble_index函数：

fn wobble_index(index: usize) -> usize { #[derive(Clone, Copy)] enum Order { Normal, Reverse, Xor(usize), } // ... match *ORDER { Order::Normal => index, Order::Reverse => !index, Order::Xor(mask) => index ^ mask, } }

wobble_index通过一个LazyLock<Order>惰性读取环境变量，随后把index映射为三种模式之一。这个函数有两个关键使用点：

BoundTypeVarInstance::can_be_bound_for（constraints.rs）：判定某个类型变量能否作为另一个类型变量的界。约束集强制对类型变量施加（任意的）全序，并保证一个约束的界在该序中"晚于"被约束的类型变量，从而无环地构造传递关系；wobble_index会同时作用于界与类型变量，进而改变 BDD 中约束的排布；
构造 BDD 节点时，约束/类型变量 ID 经wobble_index变换后决定变量在 BDD 中的层级位置。

因此，只要对同一段源码分别以默认值、reverse和不同整数掩码运行ty，再比较reveal_type输出，就能快速发现排序敏感点。mdtest 用例文件头部使用 TOML 声明运行环境：

[environment] python-version = "3.13"

表示这些用例在 Python 3.13 语义环境下执行。

四、稳定性测试用例逐条解析

以下 12 个场景全部来自 constraint_set_ordering.md，每个用例都通过ty_extensions._internal.ConstraintSet构造约束，并用reveal_type断言求解结果。&表示约束合取（and），|表示析取（or），~表示取反（negation）。

4.1 约束吸收与源码顺序无关

约束吸收（absorption）是布尔代数性质：x & (x | y) == x。该用例验证：(scalar & (scalar | tuple_))与((scalar | tuple_) & scalar)两种写法虽然源码顺序不同，但都应当化简为scalar，从而只产生Solution[T=str]：

from ty_extensions._internal import ConstraintSet def absorption[T]() -> None: scalar = ConstraintSet.lower_bound(str, T) tuple_ = ConstraintSet.lower_bound(tuple[str, ...], T) # revealed: tuple[Solution[T=str]] reveal_type((scalar & (scalar | tuple_)).solutions_for(T, inferable=tuple[T])) # revealed: tuple[Solution[T=str]] reveal_type(((scalar | tuple_) & scalar).solutions_for(T, inferable=tuple[T])) # A genuine alternative still produces both solutions; absorption does not prefer one match. # revealed: tuple[Solution[T=str], Solution[T=tuple[str, ...]]] reveal_type((scalar | tuple_).solutions_for(T, inferable=tuple[T]))

要点：吸收律的化简不应"偏向"某一边——真正保留两个分支的scalar | tuple_仍然同时产出T=str与T=tuple[str, ...]两个解；而发生了吸收的表达式必须稳定地只剩一个解。

4.2 解绑定顺序遵循约束源码顺序

约束(T = int) ∧ (U = str) ∧ (V = bytes)本身是合取的、顺序无关的，但解对象中绑定的排列顺序必须稳定：绑定顺序应当跟随"首次引入该类型变量的那条约束"的源码顺序。

from ty_extensions._internal import ConstraintSet def bindings_tuv[T, U, V]() -> None: # (T = int) ∧ (U = str) ∧ (V = bytes) constraints = ConstraintSet.equality(T, int) & ConstraintSet.equality(U, str) & ConstraintSet.equality(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.equality(T, int) & ConstraintSet.equality(U, str) & ConstraintSet.equality(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.equality(V, bytes) & ConstraintSet.equality(U, str) & ConstraintSet.equality(T, int) # revealed: tuple[Solution[V=bytes, U=str, T=int]] reveal_type(constraints.solutions(inferable=tuple[T, U, V])) def bindings_absorbed[T, U, X]() -> None: t = ConstraintSet.lower_bound(str, T) u = ConstraintSet.lower_bound(bytes, U) x = ConstraintSet.lower_bound(int, X) # ((X ≥ int) ∧ (T ≥ str) ∧ (U ≥ bytes)) | ((U ≥ bytes) ∧ (T ≥ str)) constraints = (x & t & u) | (u & t) # revealed: tuple[Solution[T=str, U=bytes]] reveal_type(constraints.solutions(inferable=tuple[T, U, X]))

三个函数分别验证了：类型变量声明顺序（bindings_tuvvsbindings_vtu）、约束书写顺序（bindings_reverse_source）、以及路径吸收后绑定顺序（bindings_absorbed）都不会导致绑定排列漂移。注意bindings_reverse_source中绑定顺序变成了V, U, T——绑定顺序跟随的是约束的源码出现顺序，而不是类型变量声明顺序。

4.3 嵌套传递约束与无关替代

约束((T ≤ list[U]) ∧ (U ≤ int) ∧ (list[int] ≤ T)) | (bytes ≤ V)中，union 两侧完全独立：T、U的解不应影响V的解，反之亦然。由于两侧用|组合，求解器有权选择"解出T、U"或"解出V"，但没有义务三者全部解出。因此默认排序下只保留两个解：左分支的解与右分支的解。

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.upper_bound(T, list[U]) & ConstraintSet.upper_bound(U, int) & ConstraintSet.lower_bound(list[int], T) ) | ConstraintSet.lower_bound(bytes, 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[]] # 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]))

文档以 TODO 形式记录了其他排序下的替代输出（例如出现Solution[T=Never]、重复的Solution[V=bytes]或空解Solution[]），这些都属于尚未完全消除的排序敏感残留，需要用TY_CONSTRAINT_SET_ORDER主动暴露。

4.4 否定替代不推断正证据

约束¬((T ≤ int) ∨ (T ≤ str)) | (bytes ≤ U)：union 左侧是取反后的约束，不应给T施加任何正面的限制。同理，由于 union 两侧无需同时满足，任何包含bytes ≤ U的解都不应顺带为T产出解。

from ty_extensions._internal import ConstraintSet def negated_alternative[T, U]() -> None: # ¬((T ≤ int) ∨ (T ≤ str)) | (bytes ≤ U) constraints = ~(ConstraintSet.upper_bound(T, int) | ConstraintSet.upper_bound(T, str)) | ConstraintSet.lower_bound(bytes, U) # 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]))

默认输出中T的解始终是空的（Solution[]），说明取反分支没有为正分支贡献证据。

4.5 独立具体解保持稳定

当两个类型变量互不相关、只是各自的界恰好包含同一具体类型时，不应因为"界中出现了相同的具体类型"而在两者间建立额外关系：

from ty_extensions._internal import ConstraintSet def independent_solution[U, T]() -> None: # (U ≤ int) ∧ (int ≤ T) ∧ ((T ≤ int) | (T ≤ str)) constraints = ( ConstraintSet.upper_bound(U, int) & ConstraintSet.lower_bound(int, T) & (ConstraintSet.upper_bound(T, int) | ConstraintSet.upper_bound(T, str)) ) # revealed: tuple[Solution[T=int]] reveal_type(constraints.solutions_for(T, inferable=tuple[T, U])) # revealed: tuple[Solution[U=int]] reveal_type(constraints.solutions_for(U, inferable=tuple[T, U]))

T与U各自得到独立且确定的解int，且与类型变量的声明顺序（[U, T]）无关。

4.6 裸类型变量方向与绑定源码顺序

S ≤ T既可以表示成对S的约束（upper_bound(S, T)），也可以表示成对T的约束（lower_bound(S, T)）；S ≤ T ≤ U既可以是一个range(S, T, U)，也可以是两条链接约束upper_bound(S, T) & upper_bound(T, U)。这些写法在逻辑上等价，因此等价关系的判定与解元素顺序必须在两种声明顺序（[S, T]与[T, S]）下都保持稳定：

from ty_extensions import static_assert from ty_extensions._internal import ConstraintSet def orientation_st[S, T]() -> None: lower = ConstraintSet.upper_bound(S, T) upper = ConstraintSet.lower_bound(S, T) # TODO: sometimes: error [static-assert-error] "Static assertion error: argument evaluates to `False`" static_assert(lower == upper) equality_st = ConstraintSet.equality(S, T) equality_ts = ConstraintSet.equality(T, S) static_assert(equality_st == equality_ts) def orientation_ts[T, S]() -> None: lower = ConstraintSet.upper_bound(S, T) upper = ConstraintSet.lower_bound(S, T) # TODO: sometimes: error [static-assert-error] "Static assertion error: argument evaluates to `False`" static_assert(lower == upper) equality_st = ConstraintSet.equality(S, T) equality_ts = ConstraintSet.equality(T, S) static_assert(equality_st == equality_ts) def chain_stu[S, T, U]() -> None: chain = ConstraintSet.range(S, T, U) linked = ConstraintSet.upper_bound(S, T) & ConstraintSet.upper_bound(T, U) # TODO: sometimes: error [static-assert-error] "Static assertion error: argument evaluates to `False`" static_assert(chain == linked) constraints = chain & ConstraintSet.lower_bound(int, S) & ConstraintSet.upper_bound(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=int | T@chain_stu | 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=S@chain_stu | int | T@chain_stu]] 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.upper_bound(S, T) & ConstraintSet.upper_bound(T, U) # TODO: sometimes: error [static-assert-error] "Static assertion error: argument evaluates to `False`" static_assert(chain == linked) constraints = chain & ConstraintSet.lower_bound(int, S) & ConstraintSet.upper_bound(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=int | T@chain_uts | 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=S@chain_uts | int | T@chain_uts]] reveal_type(constraints.solutions_for(U, inferable=tuple[S, T, U]))

注意这里的输出形如Solution[T=S@chain_stu | int | U@chain_stu]——联合类型中的元素顺序同样属于需要稳定的输出面。文档同时用 TODO 指出一个独立于排序的问题：inferable中的类型变量不应残留在"具体解"里。

4.7 抽象与非推断类型变量

for_all是ConstraintSet上的全称量化（universal abstraction）操作（实现位于 constraints.rs 附近）：对指定类型变量做抽象，等价于把这些变量从解中"抹去"。文档说明，移除非推断（non-inferable）类型变量会用ite重建 TDD（真值决策图），此时无关的正决策不能泄漏到存活路径上；对替代分支做全称抽象则只能留下无关分支：

from ty_extensions import static_assert from ty_extensions._internal import ConstraintSet def noninferable_nested[T, U, V]() -> None: constraints = ( ConstraintSet.upper_bound(T, list[U]) & ConstraintSet.upper_bound(U, int) & ConstraintSet.lower_bound(list[int], T) ) | ConstraintSet.lower_bound(bytes, V) # `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.lower_bound(bytes, V) 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.upper_bound(T, int) | ConstraintSet.upper_bound(T, str)) | ConstraintSet.lower_bound(bytes, U) quantified = constraints.for_all(tuple[T]) expected = ConstraintSet.lower_bound(bytes, U) static_assert(quantified == expected) # revealed: tuple[Solution[U=bytes]] reveal_type(quantified.solutions_for(U, inferable=tuple[U]))

这里U被故意排除在inferable之外：默认输出中第一个解仍保留U=int（对应 TODO 指出的已知问题），但对T、V的逐变量求解以及for_all抽象后的结果都必须稳定。

4.8 调用点上界保持交集顺序

从逆变可调用参数推断出的上界，按调用点源码顺序求交集；这条路径直接走UpperBound插入逻辑，与"序列（sequent）推导出的界"相互独立：

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))

关键断言是：P & Q与Q & P的元素顺序跟随参数源码顺序——accepts_p在前则交集中P在前，反之亦然。这再次印证约束求解必须保留源码顺序信息。

4.9 泛型回调通过类型别名推断

将泛型函数关联到泛型回调时，推断出的联合类型内容一致，但联合的展示顺序目前仍依赖约束排序：

from collections.abc import Callable type Items = tuple[int] | tuple[str] def identityT -> T: return value def extractT -> T: raise NotImplementedError result = extract(identity) # TODO: sometimes: revealed int | str # revealed: str | int reveal_type(result)

extract(identity)正确推断出int | str，但元素顺序（str | intvsint | str）在不同变量排序下可能翻转——这是文档明确记录的排序敏感点之一。

4.10 泛型可调用与协议关系约束

关系（relation）检查可能在类型变量被全称量化掉之前引入新的类型变量与嵌套不变约束。一个TypedDict联合用例额外练习了"公共约束探测"与"回退协议推断路径"，两者都不应依赖 TDD 顺序：

from typing import Callable, Literal, Protocol, TypeVar, TypedDict from ty_extensions import static_assert from ty_extensions._internal import ConstraintSet, TypeOf def listifyT -> list[T]: return [value] def invariant_callable[U, V]() -> None: constraints = ConstraintSet.range(bool, U, int) & ConstraintSet.equality(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: revealed int # revealed: object reveal_type(get_value(value))

implies_subtype_of（定义于 constraints.rs）在此验证listify与Callable[[U], list[V]]的子类型蕴含关系。TODO 同时暴露了两个独立问题：可调用对象"新鲜类型变量"的存在性归约目前有损（导致static_assert不报错），以及ValueA | ValueB在协议推断回退路径下应得到int却得到object。

4.11 递归派生关系保持环安全

派生约束可以递归地触发关系检查；共归纳（coinductive）的 owned-set 环边界在排序变化时必须仍然终止，且不能错误接受一个不兼容的非递归成员：

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 -> S: return self def __pos__S -> S: return self def marker(self) -> str: return "" def convertT -> Array: return cast(Array, value) # error: [disjoint-cast] # error: [invalid-assignment] invalid: Array = Concrete[int]()

Concrete[T]的marker返回str，与Array.marker -> int不兼容，因此它不应被判定为Array的成员。用例期望稳定的两个错误：disjoint-cast与invalid-assignment，同时验证递归关系检查不会因变量顺序变化而陷入循环或改变结论。

4.12 高扇出序列与推断联合截断

最后这个用例把 12 个下界关系与 12 个上界关系做笛卡尔积，耗尽共享的"序列燃料预算"（sequent fuel budget）。剩余解、其元素顺序以及被截断的诊断展示所保留的元素，都不能依赖"哪条蕴含先被处理"：

from typing import Literal 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) # ... 共 12 条 range 约束 & ConstraintSet.range(Literal[11], L11, P) ) upper = ( ConstraintSet.upper_bound(P, R0) & ConstraintSet.upper_bound(P, R1) # ... 共 12 条 upper_bound 约束 & ConstraintSet.upper_bound(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. # revealed: tuple[Solution[P=L0@high_fanout | L1@high_fanout | Literal[2, 3, 4, 5, 6, 7, 8, 9, 10, 11] | ...]] reveal_type(pivot) # revealed: tuple[Solution[R11=L1@high_fanout | Literal[2, 3, 4, 5, 6, 7, 8, 9, 10, 11] | ... | P@high_fanout]] reveal_type(result) impossible = constraints & ConstraintSet.upper_bound(R11, Literal[0]) # TODO: sometimes: revealed tuple[Solution[R11=P@high_fanout]] # revealed: None reveal_type(impossible.solutions_for(R11, inferable=inferable))

（为节省篇幅，上例中 12 条range/upper_bound约束在文中以注释省略，完整内容见 constraint_set_ordering.md。）

文档为pivot与result记录了多个# TODO: sometimes:的替代输出（不同排序下Literal[...]的元素取舍各不相同），默认输出则是其中确定的一组。最关键的断言是最后一段：在constraints上再叠加R11 ≤ Literal[0]后，约束变为不可满足，期望输出是None——但某些排序下会错误地得到Solution[R11=P@high_fanout]，这正是"高扇出预算截断"与"变量排序耦合"交织出的经典不稳定点。

五、如何运行与验证这些用例

这些用例以 mdtest 格式编写，可直接纳入ty_python_semantic的 mdtest 测试体系执行。相关的运行与自动化方式包括：

常规回归：按仓库既有 mdtest 流程运行（相关基础设施位于 mdtest crate 与 ty_python_semantic/mdtest.py），在默认排序下断言# revealed:输出，保证稳定输出不回归；
排序抖动测试：分别用TY_CONSTRAINT_SET_ORDER=reverse和不同的整数值（如1、3）运行同一批用例，观察是否出现 TODO 注释中记录的"sometimes"输出，从而定位排序敏感点；
自动化抖动：文档推荐使用wobbling-ty-constraint-orderAgent 技能批量自动化上述过程，避免手工逐个设置环境变量。

从源码看，wobble_index通过 EnvVars::TY_CONSTRAINT_SET_ORDER 读取环境变量，其取值语义为：reverse→ 按位取反全部 ID；正整数n→ 每个 ID 与n做异或（index ^ mask）。由于reverse与Xor都是对 ID 的确定性置换，它们足以构造多种截然不同的 BDD 变量排布，是验证"求解结果与变量排序无关"这一性质的高性价比手段。

六、小结

ty的约束求解器以 BDD 为内核（ConstraintSet直接持有node: NodeId），但通过source_order保留约束的源码顺序，并在投影阶段（solutions/solutions_for）尽量按源码顺序呈现路径与绑定。当前实现已保证"同源码多次运行输出一致"的运行间确定性，而 constraint_set_ordering.md 这份回归规格的目标，是把"不同 BDD 变量排序下输出一致"的排序无关性也逐步收口：

约束吸收、独立具体解、裸类型变量方向、等价判定（static_assert(lower == upper)、chain == linked）等语义层面的稳定性已经达成；
解元素/绑定的展示顺序（如str | intvsint | str、P & QvsQ & P）部分场景仍随排序变化，文档用# TODO: sometimes:逐一标记；
高扇出、预算截断、非推断类型变量与全称抽象（for_all）等路径层的边界行为，是排序敏感残留最集中的区域。

对类型检查器开发者而言，这套用例提供了三层价值：一是可执行的回归基线，锁定默认排序下的期望输出；二是排序敏感点的完整清单，借助TY_CONSTRAINT_SET_ORDER环境变量可随时复现；三是求解器内部机制的教学标本——从wobble_index的变量置换、can_be_bound_for的无环全序，到solutions_with的路径投影，完整串起了"约束 → BDD → 路径 → 解"的推理链路。

【免费下载链接】ruffAn extremely fast Python linter and code formatter, written in Rust.项目地址: https://gitcode.com/GitHub_Trending/ru/ruff

创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考