深入 ty 类型检查器ConstraintSet 约束集求解的顺序稳定性与 BDD 变量排序【免费下载链接】ruffAn extremely fast Python linter and code formatter, written in Rust.项目地址: https://gitcode.com/GitHub_Trending/ru/ruffty是 Ruff 仓库中基于 Rust 实现的类型检查器。在类型推断过程中约束求解器会把在一组约束下某个类型性质成立的状态表示为约束集ConstraintSet其底层由BDD二元决策图承载。本篇以 constraint_set_ordering.md 这份 mdtest 回归测试规格为核心系统讲解ty如何保证约束集求解结果不依赖 BDD 变量的内部排序、solutions/solutions_for的语义差异、TY_CONSTRAINT_SET_ORDER环境变量如何打乱变量顺序以暴露不稳定输出并逐条剖析文档中覆盖的 12 类稳定性测试场景。读完本文你将理解 ty 约束求解器确定性输出的测试方法论并能自行运行、扩展这些稳定性回归用例。一、背景约束集、路径与 BDD1.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通过一个LazyLockOrder惰性读取环境变量随后把index映射为三种模式之一。这个函数有两个关键使用点BoundTypeVarInstance::can_be_bound_forconstraints.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[Tstr]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[Tstr]] reveal_type((scalar (scalar | tuple_)).solutions_for(T, inferabletuple[T])) # revealed: tuple[Solution[Tstr]] reveal_type(((scalar | tuple_) scalar).solutions_for(T, inferabletuple[T])) # A genuine alternative still produces both solutions; absorption does not prefer one match. # revealed: tuple[Solution[Tstr], Solution[Ttuple[str, ...]]] reveal_type((scalar | tuple_).solutions_for(T, inferabletuple[T]))要点吸收律的化简不应偏向某一边——真正保留两个分支的scalar | tuple_仍然同时产出Tstr与Ttuple[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[Tint, Ustr, Vbytes]] reveal_type(constraints.solutions(inferabletuple[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[Tint, Ustr, Vbytes]] reveal_type(constraints.solutions(inferabletuple[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[Vbytes, Ustr, Tint]] reveal_type(constraints.solutions(inferabletuple[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[Tstr, Ubytes]] reveal_type(constraints.solutions(inferabletuple[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[Tlist[int]], Solution[TNever], Solution[]] # TODO: sometimes: revealed tuple[Solution[Tlist[int]], Solution[Tlist[int]], Solution[]] # TODO: sometimes: revealed tuple[Solution[Tlist[int]], Solution[], Solution[]] # revealed: tuple[Solution[Tlist[int]], Solution[]] reveal_type(constraints.solutions_for(T, inferabletuple[T, U, V])) # TODO: sometimes: revealed tuple[Solution[Uint], Solution[UNever], Solution[]] # TODO: sometimes: revealed tuple[Solution[Uint], Solution[], Solution[]] # revealed: tuple[Solution[Uint], Solution[]] reveal_type(constraints.solutions_for(U, inferabletuple[T, U, V])) # TODO: sometimes: revealed tuple[Solution[], Solution[Vbytes], Solution[Vbytes]] # revealed: tuple[Solution[], Solution[Vbytes]] reveal_type(constraints.solutions_for(V, inferabletuple[T, U, V])) # TODO: sometimes: revealed tuple[Solution[Tlist[int], Uint], Solution[TNever, Vbytes], Solution[Vbytes]] # TODO: sometimes: revealed tuple[Solution[Tlist[int], Uint], Solution[Tlist[int], Vbytes], Solution[Vbytes]] # TODO: sometimes: revealed tuple[Solution[Tlist[int], Uint], Solution[UNever, Vbytes], Solution[Vbytes]] # revealed: tuple[Solution[Tlist[int], Uint], Solution[Vbytes]] reveal_type(constraints.solutions(inferabletuple[T, U, V]))文档以 TODO 形式记录了其他排序下的替代输出例如出现Solution[TNever]、重复的Solution[Vbytes]或空解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[TNever], Solution[]] # revealed: tuple[Solution[], Solution[]] reveal_type(constraints.solutions_for(T, inferabletuple[T, U])) # TODO: sometimes: revealed tuple[Solution[], Solution[Ubytes], Solution[Ubytes]] # revealed: tuple[Solution[], Solution[Ubytes]] reveal_type(constraints.solutions_for(U, inferabletuple[T, U])) # TODO: sometimes: revealed tuple[Solution[], Solution[TNever, Ubytes], Solution[Ubytes]] # revealed: tuple[Solution[], Solution[Ubytes]] reveal_type(constraints.solutions(inferabletuple[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[Tint]] reveal_type(constraints.solutions_for(T, inferabletuple[T, U])) # revealed: tuple[Solution[Uint]] reveal_type(constraints.solutions_for(U, inferabletuple[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[Sint | Uchain_stu | Tchain_stu]] # revealed: tuple[Solution[Sint | Tchain_stu | Uchain_stu]] reveal_type(constraints.solutions_for(S, inferabletuple[S, T, U])) # revealed: tuple[Solution[TSchain_stu | int | Uchain_stu]] reveal_type(constraints.solutions_for(T, inferabletuple[S, T, U])) # revealed: tuple[Solution[USchain_stu | int | Tchain_stu]] reveal_type(constraints.solutions_for(U, inferabletuple[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[Sint | Uchain_uts | Tchain_uts]] # revealed: tuple[Solution[Sint | Tchain_uts | Uchain_uts]] reveal_type(constraints.solutions_for(S, inferabletuple[S, T, U])) # revealed: tuple[Solution[TSchain_uts | int | Uchain_uts]] reveal_type(constraints.solutions_for(T, inferabletuple[S, T, U])) # revealed: tuple[Solution[USchain_uts | int | Tchain_uts]] reveal_type(constraints.solutions_for(U, inferabletuple[S, T, U]))注意这里的输出形如Solution[TSchain_stu | int | Uchain_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[Tlist[int], Uint], Solution[TNever, Vbytes], Solution[Vbytes]] # TODO: sometimes: revealed tuple[Solution[Tlist[int], Uint], Solution[Tlist[int], Vbytes], Solution[Vbytes]] # revealed: tuple[Solution[Tlist[int], Uint], Solution[Vbytes]] reveal_type(constraints.solutions(inferabletuple[T, V])) # TODO: sometimes: revealed tuple[Solution[Tlist[int]], Solution[TNever], Solution[]] # TODO: sometimes: revealed tuple[Solution[Tlist[int]], Solution[Tlist[int]], Solution[]] # revealed: tuple[Solution[Tlist[int]], Solution[]] reveal_type(constraints.solutions_for(T, inferabletuple[T, V])) # TODO: sometimes: revealed tuple[Solution[], Solution[Vbytes], Solution[Vbytes]] # revealed: tuple[Solution[], Solution[Vbytes]] reveal_type(constraints.solutions_for(V, inferabletuple[T, V])) quantified constraints.for_all(tuple[T, U]) expected ConstraintSet.lower_bound(bytes, V) static_assert(quantified expected) # revealed: tuple[Solution[Vbytes]] reveal_type(quantified.solutions_for(V, inferabletuple[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[Ubytes]] reveal_type(quantified.solutions_for(U, inferabletuple[U]))这里U被故意排除在inferable之外默认输出中第一个解仍保留Uint对应 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 callables 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, covariantTrue) 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, inferableinferable) result constraints.solutions_for(R11, inferableinferable) # TODO: inferred solutions should not retain the intermediate inferable typevars. # revealed: tuple[Solution[PL0high_fanout | L1high_fanout | Literal[2, 3, 4, 5, 6, 7, 8, 9, 10, 11] | ...]] reveal_type(pivot) # revealed: tuple[Solution[R11L1high_fanout | Literal[2, 3, 4, 5, 6, 7, 8, 9, 10, 11] | ... | Phigh_fanout]] reveal_type(result) impossible constraints ConstraintSet.upper_bound(R11, Literal[0]) # TODO: sometimes: revealed tuple[Solution[R11Phigh_fanout]] # revealed: None reveal_type(impossible.solutions_for(R11, inferableinferable))为节省篇幅上例中 12 条range/upper_bound约束在文中以注释省略完整内容见 constraint_set_ordering.md。文档为pivot与result记录了多个# TODO: sometimes:的替代输出不同排序下Literal[...]的元素取舍各不相同默认输出则是其中确定的一组。最关键的断言是最后一段在constraints上再叠加R11 ≤ Literal[0]后约束变为不可满足期望输出是None——但某些排序下会错误地得到Solution[R11Phigh_fanout]这正是高扇出预算截断与变量排序耦合交织出的经典不稳定点。五、如何运行与验证这些用例这些用例以 mdtest 格式编写可直接纳入ty_python_semantic的 mdtest 测试体系执行。相关的运行与自动化方式包括常规回归按仓库既有 mdtest 流程运行相关基础设施位于 mdtest crate 与 ty_python_semantic/mdtest.py在默认排序下断言# revealed:输出保证稳定输出不回归排序抖动测试分别用TY_CONSTRAINT_SET_ORDERreverse和不同的整数值如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），仅供参考