[ty] Decide satisfiability of simple typevar-free conjunctions directly (#27178)
## Summary
Fixes astral-sh/ty#4089, where `ty check` took O(n²) time in the size of
a literal union such as `mypy_boto3_ec2`'s `InstanceTypeType` (~1200
string literals).
Checking iteration over `Sequence[Literal[...]]` builds a constraint set
that is a single conjunction with one lower-bound constraint per union
element. Deciding its satisfiability walks the BDD with
`PathAssignments`, whose `discover_constraint` computes sequents for
every pair of constraints ā quadratic in the number of constraints. For
lower-bound-only pairs, each pair computation also eagerly builds a
`Literal[a] | Literal[b]` union in `ConstraintId::intersect`, only for
the result to be discarded as `CannotSimplify`, so the entire quadratic
pass produces empty sequent maps.
This PR adds a linear fast path to `is_never_satisfied` for BDDs that
are a single all-positive conjunction with typevar-free bounds: per
typevar occurrence, check that the union of the lower bounds is
assignable to each upper-bound clause. Assignability distributes over
the union on the left and the intersection clauses on the right, so this
finds exactly the contradictions that the walk's pairwise disjointness
sequents detect. Bounds are grouped by occurrence identity so
differently materialized instances of the same typevar are handled
together. Type aliases and protocols can hide typevars in lazy
attributes, so bounds containing either conservatively fall back to the
general walk; this also avoids expanding recursively specialized aliases
in the fast path.
The existing `compute_simple_bound_conjunction` fast path used for
solution extraction is updated to use the same identity and lazy-bound
handling. For typevars with only upper-bound evidence, it skips
quadratic per-clause redundancy pruning and lets the final intersection
determine the solution.
Timings for the issue's reproducer (debug build): 4.6s ā 0.03s against
an installed `mypy_boto3_ec2`, 2.3s ā 0.03s for a synthetic 1200-literal
union, and the runtime is now flat in the union size (5000 literals also
check in ~0.03s).
## Test plan
- Added benchmarks covering `Sequence[Literal[...]]` access and many
contravariant callback arguments that produce upper-bound-only
constraints.
- Added unit tests covering satisfiable and contradictory simple
conjunctions without sequent-cache growth, equivalence with the general
path walk, differently materialized instances of the same typevar,
hidden typevars in lazy aliases, and large upper-bound-only
conjunctions.
- The `ty_python_semantic` test suite passes.
- Stable type property tests pass with 2000 generated cases.
- Manually verified the issue's reproducer and upper-bound-only scaling.
---------
Co-authored-by: Carl Meyer <carl@astral.sh>
Co-authored-by: Douglas Creager <dcreager@dcreager.net>