Skip to content

subtype: save some union stack space for ∃ free cases. #58159

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Apr 20, 2025
Merged

subtype: save some union stack space for ∃ free cases. #58159

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
34 changes: 25 additions & 9 deletions src/subtype.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -139,7 +139,7 @@ static jl_varbinding_t *lookup(jl_stenv_t *e, jl_tvar_t *v) JL_GLOBALLY_ROOTED J

static int statestack_get(jl_unionstate_t *st, int i) JL_NOTSAFEPOINT
{
assert(i >= 0 && i <= 32767); // limited by the depth bit.
assert(i >= 0 && i < 32767); // limited by the depth bit.
// get the `i`th bit in an array of 32-bit words
jl_bits_stack_t *stack = &st->stack;
while (i >= sizeof(stack->data) * 8) {
Expand All @@ -153,7 +153,7 @@ static int statestack_get(jl_unionstate_t *st, int i) JL_NOTSAFEPOINT

static void statestack_set(jl_unionstate_t *st, int i, int val) JL_NOTSAFEPOINT
{
assert(i >= 0 && i <= 32767); // limited by the depth bit.
assert(i >= 0 && i < 32767); // limited by the depth bit.
jl_bits_stack_t *stack = &st->stack;
while (i >= sizeof(stack->data) * 8) {
if (__unlikely(stack->next == NULL)) {
Expand Down Expand Up @@ -1448,11 +1448,14 @@ static int subtype(jl_value_t *x, jl_value_t *y, jl_stenv_t *e, int param)
}
if (jl_is_unionall(y)) {
jl_varbinding_t *xb = lookup(e, (jl_tvar_t*)x);
if (xb == NULL ? !e->ignore_free : !xb->right) {
jl_value_t *xub = xb == NULL ? ((jl_tvar_t *)x)->ub : xb->ub;
if ((xb == NULL ? !e->ignore_free : !xb->right) && xub != y) {
// We'd better unwrap `y::UnionAll` eagerly if `x` isa ∀-var.
// This makes sure the following cases work correct:
// 1) `∀T <: Union{∃S, SomeType{P}} where {P}`: `S == Any` ==> `S >: T`
// 2) `∀T <: Union{∀T, SomeType{P}} where {P}`:
// note: if xub == y we'd better try `subtype_var` as `subtype_left_var`
// hit `==` based fast path.
return subtype_unionall(x, (jl_unionall_t*)y, e, 1, param);
}
}
Expand Down Expand Up @@ -1590,6 +1593,8 @@ static int has_exists_typevar(jl_value_t *x, jl_stenv_t *e) JL_NOTSAFEPOINT
return env != NULL && jl_has_bound_typevars(x, env);
}

static int forall_exists_subtype(jl_value_t *x, jl_value_t *y, jl_stenv_t *e, int param);

static int local_forall_exists_subtype(jl_value_t *x, jl_value_t *y, jl_stenv_t *e, int param, int limit_slow)
{
int16_t oldRmore = e->Runions.more;
Expand All @@ -1603,7 +1608,18 @@ static int local_forall_exists_subtype(jl_value_t *x, jl_value_t *y, jl_stenv_t
return jl_subtype(x, y);
int has_exists = (!kindx && has_exists_typevar(x, e)) ||
(!kindy && has_exists_typevar(y, e));
if (has_exists && (is_exists_typevar(x, e) != is_exists_typevar(y, e))) {
if (!has_exists) {
// We can use ∀_∃_subtype safely for ∃ free inputs.
// This helps to save some bits in union stack.
jl_saved_unionstate_t oldRunions; push_unionstate(&oldRunions, &e->Runions);
e->Lunions.used = e->Runions.used = 0;
e->Lunions.depth = e->Runions.depth = 0;
e->Lunions.more = e->Runions.more = 0;
sub = forall_exists_subtype(x, y, e, param);
pop_unionstate(&e->Runions, &oldRunions);
return sub;
}
if (is_exists_typevar(x, e) != is_exists_typevar(y, e)) {
e->Lunions.used = 0;
while (1) {
e->Lunions.more = 0;
Expand All @@ -1617,7 +1633,7 @@ static int local_forall_exists_subtype(jl_value_t *x, jl_value_t *y, jl_stenv_t
if (limit_slow == -1)
limit_slow = kindx || kindy;
jl_savedenv_t se;
save_env(e, &se, has_exists);
save_env(e, &se, 1);
int count, limited = 0, ini_count = 0;
jl_saved_unionstate_t latestLunions = {0, 0, 0, NULL};
while (1) {
Expand All @@ -1635,26 +1651,26 @@ static int local_forall_exists_subtype(jl_value_t *x, jl_value_t *y, jl_stenv_t
limited = 1;
if (!sub || !next_union_state(e, 0))
break;
if (limited || !has_exists || e->Runions.more == oldRmore) {
if (limited || e->Runions.more == oldRmore) {
// re-save env and freeze the ∃decision for previous ∀Union
// Note: We could ignore the rest `∃Union` decisions if `x` and `y`
// contain no ∃ typevar, as they have no effect on env.
ini_count = count;
push_unionstate(&latestLunions, &e->Lunions);
re_save_env(e, &se, has_exists);
re_save_env(e, &se, 1);
e->Runions.more = oldRmore;
}
}
if (sub || e->Runions.more == oldRmore)
break;
assert(e->Runions.more > oldRmore);
next_union_state(e, 1);
restore_env(e, &se, has_exists); // also restore Rdepth here
restore_env(e, &se, 1); // also restore Rdepth here
e->Runions.more = oldRmore;
}
if (!sub)
assert(e->Runions.more == oldRmore);
else if (limited || !has_exists)
else if (limited)
e->Runions.more = oldRmore;
free_env(&se);
return sub;
Expand Down
14 changes: 14 additions & 0 deletions test/subtype.jl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2768,3 +2768,17 @@ end
Tuple{Type{Complex{T}} where T, Type{Complex{T}} where T, Type{String}},
Tuple{Type{Complex{T}}, Type{Complex{T}}, Type{String}} where T
)

#issue 58129
for k in 1:500
@eval struct $(Symbol(:T58129, k)){T} end
end
let Tvar = TypeVar(:Tvar)
V = UnionAll(Tvar, Union{(@eval($(Symbol(:T58129, k)){$Tvar}) for k in 1:500)...})
@test Set{<:V} <: AbstractSet{<:V}
end
let Tvar1 = TypeVar(:Tvar1), Tvar2 = TypeVar(:Tvar2)
V1 = UnionAll(Tvar1, Union{(@eval($(Symbol(:T58129, k)){$Tvar1}) for k in 1:100)...})
V2 = UnionAll(Tvar2, Union{(@eval($(Symbol(:T58129, k)){$Tvar2}) for k in 1:100)...})
@test Set{<:V2} <: AbstractSet{<:V1}
end
Loading