subtype: isolate `Union` state in `subtype_ccheck` to prevent exponential hang (#61316)
Investigation of aviatesk/JETLS.jl#509 revealed that the root cause is a
hang in the subtyping algorithm. A minimal reproducer has been added to
`test/subtype.jl`, which does not terminate in a reasonable time on the
current master branch.
The fix was developed using Claude and Codex, with iterative
cross-review between the two to arrive at what I believe is the most
sound approach. However, I am not very familiar with the subtype
algorithm implementation, so there may be implementation issues I have
not caught. Note that the bulk of this patch was written by AI.
---
`subtype_ccheck` calls `local_forall_exists_subtype`, which leaks
right-side Union choices (via `pick_union_decision`) into the shared
`Runions` statestack. When many
Union-bounded type parameters share a common variable (e.g. 6 parameters
all bounded by `Union{Ref{F},Val{F}}`), each bounds check adds decisions
that `exists_subtype` must iterate over combinatorially, causing O(2^N)
iterations.
Make `subtype_ccheck` save and restore both the `Runions` state and
variable environment (`save_env`/`restore_env`).
When `pick_union_decision` added new entries during the check (detected
via `Runions.used` growth) and the check succeeded, a merge loop
(`ccheck_merge_env`) enumerates all successful right-side ∃ branches and
merges their variable constraints via `simple_meet` (lb) / `simple_join`
(ub). This yields the widest constraints valid across any successful
branch, instead of discarding all constraints. A separate
`ccheck_restore_metadata` step then overrides the metadata fields
(`occurs_inv`, `occurs_cov`,
`max_offset`, `innervars`) with the original values, since `merge_env`'s
metadata merging (max for occurs, min for max_offset) tightens
constraints — the opposite of what `subtype_ccheck` needs.
The merge loop uses `next_union_state_from` to iterate only the ccheck's
own ∃ decisions (starting from
`oldRunions.used`), avoiding interference with outer Union iteration.
Each branch runs a full ∀∃ check via
`local_forall_exists_subtype`. The `ccheck_merging` flag prevents
re-entrant merge loops from nested `subtype_ccheck` calls; the
`!e->intersection` guard avoids conflicts with `intersect_all`'s own
`merge_env` handling.
When no Union splitting occurred, the variable constraints are
deterministic and safe to keep; restoring them unconditionally
introduces false negatives that break the `obvious_subtype` invariant.
The `envout` array is preserved across the restore because inner
`subtype_unionall` calls may have already written inferred
type-parameter values that must survive.
Known limitation: detection via `Runions.used` growth is imperfect —
`local_forall_exists_subtype`'s exists-free path (path 1) internally
pushes/pops its own `Runions`, so Union choices made there do not
increase the outer `Runions.used`. Currently harmless because
exists-free inputs have no exists-variable constraints to corrupt, but
the detection mechanism has a structural gap.
Fixes aviatesk/JETLS.jl#509.
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>