[ty] Check constraint equivalence by searching for counterexamples (#30093)
## Summary
When matching a union of `TypedDict` types against a protocol, ty can
end up checking whether two sets of type-variable constraints accept
exactly the same assignments. We used to build a decision diagram for
the entire equivalence before asking the solver to prove it.
We now look for an assignment that satisfies `A` but not `B`, then one
that satisfies `B` but not `A`. If neither exists, the constraints are
equivalent. This lets the solver rule out each direction independently.
<!-- ty-pinned-project-instructions:start -->
The table shows median instructions per cold `ty check`. Change and
range compare paired PR and parent runs. Negative values mean fewer
instructions. [Pinned
projects](https://github.com/astral-sh/ty/blob/1b1d9c40e9d9ca08e0028d672c6b0c1eff34796a/BENCHMARKS.md)
| Project | Parent instructions | PR instructions | Change | Paired
range |
|---|---:|---:|---:|---:|
|
[Black](https://github.com/psf/black/tree/55996d1fb8342725c8a19b6023cd9439c3c1d6f7)
| 3,373,003,124 | 3,374,298,156 | +0.02% | -0.19% to +0.22% |
|
[discord.py](https://github.com/Rapptz/discord.py/tree/65232c38702be5844cf2ce865a4777eb1928b5d0)
| 8,609,910,100 | 8,611,446,072 | +0.03% | -0.08% to +0.10% |
|
[Django](https://github.com/django/django/tree/b501b8493f31cf8cba31211d59b3b78642b8cb02)
| 14,681,129,624 | 14,688,783,746 | +0.03% | -0.18% to +0.29% |
|
[FastAPI](https://github.com/fastapi/fastapi/tree/7a0a3f0b286c6c865cf4398ea0e957a87b8bffa4)
| 3,250,575,784 | 3,250,752,614 | +0.02% | -0.02% to +0.07% |
|
[HTTPX](https://github.com/encode/httpx/tree/b5addb64f0161ff6bfe94c124ef76f6a1fba5254)
| 1,786,163,665 | 1,789,062,196 | +0.20% | +0.11% to +0.28% |
|
[isort](https://github.com/pycqa/isort/tree/a514c71ed86c2216d0040c7d60e302ed76a4f7ab)
| 2,146,151,374 | 2,145,087,152 | -0.02% | -0.12% to +0.16% |
|
[Jinja](https://github.com/pallets/jinja/tree/5ef70112a1ff19c05324ff889dd30405b1002044)
| 1,948,559,228 | 1,948,950,055 | +0.02% | -0.46% to +0.49% |
|
[NumPy](https://github.com/numpy/numpy/tree/f9f1772ce010001208475f751d19253469788410)
| 14,391,964,252 | 14,414,602,883 | +0.14% | -0.45% to +0.56% |
| [OpenAI Python
SDK](https://github.com/openai/openai-python/tree/f6e8480f9a5b2a4d02b17a1da54a1e57964bc312)
| 18,221,101,986 | 16,993,814,373 | -6.73% | -7.69% to -5.76% |
|
[pandas](https://github.com/pandas-dev/pandas/tree/a0225b65720018f4654390bb16d254daa6ee5e54)
| 30,420,091,094 | 30,428,421,949 | +0.03% | -0.02% to +0.13% |
|
[pandas-stubs](https://github.com/pandas-dev/pandas-stubs/tree/8dd6d91b1c05b26e30f7ddbe3dc3d4042a92bdd6)
| 3,622,834,166 | 3,621,655,386 | -0.04% | -0.15% to +0.19% |
|
[Prefect](https://github.com/PrefectHQ/prefect/tree/a9452ac21852755311913cb27887b083b5007c03)
| 5,143,475,814 | 5,143,079,378 | +0.01% | -0.05% to +0.05% |
|
[pytest](https://github.com/pytest-dev/pytest/tree/8b005ed7f972987033ec34dc1e68b0635fb8142b)
| 8,758,923,634 | 8,764,544,465 | +0.09% | +0.02% to +0.24% |
|
[PyTorch](https://github.com/pytorch/pytorch/tree/ab92945cea42e47ae398aead69af0872d340ea0f)
| 99,295,248,976 | 99,249,639,278 | 0.00% | -0.13% to 0.00% |
|
[Rich](https://github.com/Textualize/rich/tree/9d8f9a372cc5916fd4781fec207ced7ddac2f08f)
| 2,810,730,702 | 2,804,439,801 | -0.21% | -0.53% to +0.23% |
|
[SQLAlchemy](https://github.com/sqlalchemy/sqlalchemy/tree/10f4d1e2d706a7722ca78e79ce05b00333a7aa5b)
| 21,322,337,398 | 21,323,692,710 | 0.00% | -0.04% to +0.24% |
|
[SymPy](https://github.com/sympy/sympy/tree/85d3998a4517ffbc8a9709b8efa769bb417c174a)
| 47,949,159,864 | 47,984,374,333 | +0.07% | 0.00% to +0.13% |
<!-- ty-pinned-project-instructions:end -->
Co-authored-by: Charlie Marsh <charliemarsh@openai.com>
ruff
cdc5f2c4 - [ty] Check constraint equivalence by searching for counterexamples (#30093)
