subtype: isolate Union state in subtype_ccheck to prevent exponential hang

[aviatesk]

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.

[adienes]

Claude and Codex, with iterative cross-review

so applying another seems like fair game 😉. my claude makes a convincing argument that the saved_envout tracking is not required since always e->envidx >= e->envsz within subtype_ccheck

it gives me

this diff

diff --git a/src/subtype.c b/src/subtype.c
index d99e4b79cf..06abd293e7 100644
--- a/src/subtype.c
+++ b/src/subtype.c
@@ -739,8 +739,7 @@ NOINLINE static void ccheck_merge_env(
     jl_value_t *x, jl_value_t *y, jl_stenv_t *e,
     jl_savedenv_t *se,
     jl_saved_unionstate_t *oldLunions,
-    int16_t oldRunions_used,
-    jl_value_t **saved_envout, int envout_n)
+    int16_t oldRunions_used)
 {
     jl_savedenv_t me;
     int nmerge = 0;
@@ -748,9 +747,6 @@ NOINLINE static void ccheck_merge_env(
     nmerge = merge_env(e, &me, se, nmerge);
     while (next_union_state_from(e, 1, oldRunions_used)) {
         restore_env(e, se, 1);
-        if (saved_envout)
-            memcpy(&e->envout[e->envidx], saved_envout,
-                   envout_n * sizeof(jl_value_t *));
         pop_unionstate(&e->Lunions, oldLunions);
         e->Runions.more = 0;
         e->Lunions.more = 0;
@@ -761,9 +757,6 @@ NOINLINE static void ccheck_merge_env(
     if (nmerge > 0) {
         restore_env(e, &me, 1);
         ccheck_restore_metadata(e, se);
-        if (saved_envout)
-            memcpy(&e->envout[e->envidx], saved_envout,
-                   envout_n * sizeof(jl_value_t *));
         free_env(&me);
     }
 }
@@ -798,36 +791,25 @@ static int subtype_ccheck(jl_value_t *x, jl_value_t *y, jl_stenv_t *e)
         return 0;
     if (obviously_in_union(y, x))
         return 1;
+    // Bounds checks happen after all outer-chain right-side UnionAlls have
+    // been entered, so envidx >= envsz and restore_env cannot touch envout.
+    assert(e->envidx >= e->envsz);
     jl_saved_unionstate_t oldLunions; push_unionstate(&oldLunions, &e->Lunions);
     jl_saved_unionstate_t oldRunions; push_unionstate(&oldRunions, &e->Runions);
     jl_savedenv_t se;
     save_env(e, &se, 1);
     int sub = local_forall_exists_subtype(x, y, e, 0, 1);
     if (e->Runions.used > oldRunions.used) {
-        // Right-side Union choices were made. Preserve envout
-        // for subtype_unionall before any env restore.
-        int envout_n = 0;
-        jl_value_t **saved_envout = NULL;
-        if (e->envout && e->envidx < e->envsz) {
-            envout_n = e->envsz - e->envidx;
-            saved_envout = (jl_value_t **)alloca(
-                envout_n * sizeof(jl_value_t *));
-            memcpy(saved_envout, &e->envout[e->envidx],
-                   envout_n * sizeof(jl_value_t *));
-        }
+        // Right-side Union choices were made during the bounds check.
         if (sub && !e->ccheck_merging && !e->intersection) {
             // Merge constraints across all successful ∃ branches
             // (lb via simple_meet, ub via simple_join).
-            ccheck_merge_env(x, y, e, &se, &oldLunions, oldRunions.used,
-                             saved_envout, envout_n);
+            ccheck_merge_env(x, y, e, &se, &oldLunions, oldRunions.used);
         }
         else {
             // sub == 0 or re-entrance/intersection: restore env
             // to clean up stale constraints from the check.
             restore_env(e, &se, 1);
-            if (saved_envout)
-                memcpy(&e->envout[e->envidx], saved_envout,
-                       envout_n * sizeof(jl_value_t *));
         }
     }
     free_env(&se);

this "proof"

Proof: e->envidx >= e->envsz in subtype_ccheck

This proves that the envout save/restore code in subtype_ccheck is dead code:
envidx >= envsz always holds on entry, so restore_env's memset and
subtype_unionall's envout write (both guarded by envidx < envsz) never execute.

Lemma 1: subtype_ccheck is only reachable for right-side variables.

Direct from code: var_lt (line 910) and var_gt (line 951) both return early
via subtype_left_var when !bb->right. The subtype_ccheck calls at lines
914, 955, 1907, 1917 are only reached when bb->right == 1.

Lemma 2: A right-side variable in e->vars was placed there by subtype_unionall(R=1) or intersect_unionall_(R=1), both of which increment envidx.

The only places that push a jl_varbinding_t onto e->vars with right=R:

• subtype_unionall (line 1144-1147): when R=1, envidx++ at line 1150.
• intersect_unionall_ (line 3593-3594): when R=1, envidx++ at line 3597.

One exception: subtype_in_env_existential (line 2906) flips existing variables
to right=1 without pushing new bindings. Addressed in Lemma 5.

Lemma 3: The outer envsz right-side UnionAlls are peeled sequentially before body processing.

The right-side type has the form UnionAll{T1, UnionAll{T2, ..., UnionAll{Tn, Body}}}
where n = envsz. In subtype (line 1694-1700), when the right side is a UnionAll,
subtype_unionall(R=1) peels it and recurses on the body. Similarly in intersect
(line 4421). Each peel increments envidx. After all n peels, envidx = n = envsz.

Lemma 4: A right-side outer-chain variable is only encountered in var_lt/var_gt/equal_var AFTER all envsz UnionAlls are peeled.

Variable Tk from the k-th UnionAll cannot appear as a bare typevar in the
UnionAll{T(k+1), ...} wrapper -- it only appears inside the innermost Body.
When k < n, subtype/intersect dispatches on the structural form of the right
side (which is a UnionAll), calling subtype_unionall(R=1) to peel the next layer
rather than entering var_lt/var_gt processing. The innermost Body is only
reached after all n peels, at which point envidx = envsz. Inner UnionAlls
(beyond the outer chain) further increment envidx above envsz.

Lemma 5: subtype_in_env and subtype_in_env_existential preserve the invariant.

subtype_in_env (line 2491) copies envidx and envsz from the parent. Two cases:

5a. Called after full peeling (envidx >= envsz): Further subtype_unionall(R=1)
calls inside only increase envidx. Invariant maintained.

5b. Called before full peeling (envidx = k < envsz): The right-side argument
is the remaining UnionAll chain. Inside forall_exists_subtype, subtype peels
this chain, incrementing envidx from k to envsz before any variables are
encountered. If the right side doesn't contain the remaining chain (e.g., it's a
concrete type), it doesn't reference the right-side variables, so subtype_ccheck
isn't triggered.

subtype_in_env_existential (line 2906) flips all variables to right=1. All its
call sites (intersect_var line 3003, intersect_invariant lines 4054/4059,
intersect_var_ccheck_in_env lines 4190/4195) are inside the body after full peeling.

Theorem

By Lemmas 1-5, when subtype_ccheck is entered, envidx >= envsz. QED.

Consequences

Since envidx >= envsz:

1. restore_env's memset (line 401-402, guarded by envidx < envsz) never
   executes during ccheck.
2. subtype_unionall's envout write (line 1206, same guard) never executes
   during ccheck.
3. The e->envout && e->envidx < e->envsz check evaluates to false, so
   saved_envout is always NULL and envout_n is always 0.

Both the alloca+memcpy pattern and the envidx trick are provably equivalent
no-ops. The envout handling in subtype_ccheck is defensively correct
belt-and-suspenders code.

[aviatesk]

@adienes Thank you for the suggestion, and for providing a proof! I applied it and confirmed the tests and the MRE of the original issue are still passing as before.

[adienes]

to the extent I can review this I have no other comments. not sure if someone with more than my limited experience with the subtyping algorithm also wants to review

[N5N3]

IIUC, this PR would break Tuple{Union{Int,Int8},Ref{Int},Ref{Int}} <: Tuple{<:Union{S,T},Ref{S},Ref{T}} where {S,T}
(but Tuple{Ref{Int},Ref{Int},Union{Int,Int8}} <: Tuple{Ref{S},Ref{T},<:Union{S,T}} where {S,T} would be correct.)

merge_env was designed for typeintersect only, as it widens env too much, which is typically incorrect during subtyping.

As for this specific hang pattern, perhaps we can monitor whether env changes during the local_forall_exists_subtype process. If it does not, then reset Runion.more to oldRmore.

[aviatesk]

@N5N3 Thanks for the review! I've replaced the previous fix with your suggested approach: monitoring whether env (lb/ub) changes during the bounds check, and resetting Runions.more to its previous value when it does not. This is both simpler and correct (f296c3b).

[adienes]

I'd add the examples
Tuple{Union{Int,Int8},Ref{Int},Ref{Int}} <: Tuple{<:Union{S,T},Ref{S},Ref{T}} where {S,T}
and
Tuple{Ref{Int},Ref{Int},Union{Int,Int8}} <: Tuple{Ref{S},Ref{T},<:Union{S,T}} where {S,T}

as regression tests