Skip to content

Intersect: try normal+reverse+existential subtyping during intersection #57476

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
Mar 6, 2025
Merged

Intersect: try normal+reverse+existential subtyping during intersection #57476

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
127 changes: 96 additions & 31 deletions src/subtype.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2678,31 +2678,22 @@ static void set_bound(jl_value_t **bound, jl_value_t *val, jl_tvar_t *v, jl_sten
// subtype, treating all vars as existential
static int subtype_in_env_existential(jl_value_t *x, jl_value_t *y, jl_stenv_t *e)
{
jl_varbinding_t *v = e->vars;
int len = 0;
if (x == jl_bottom_type || y == (jl_value_t*)jl_any_type)
return 1;
while (v != NULL) {
len++;
v = v->prev;
}
int8_t *rs = (int8_t*)malloc_s(len);
int8_t *rs = (int8_t*)alloca(current_env_length(e));
jl_varbinding_t *v = e->vars;
int n = 0;
v = e->vars;
while (n < len) {
assert(v != NULL);
while (v != NULL) {
rs[n++] = v->right;
v->right = 1;
v = v->prev;
}
int issub = subtype_in_env(x, y, e);
n = 0; v = e->vars;
while (n < len) {
assert(v != NULL);
while (v != NULL) {
v->right = rs[n++];
v = v->prev;
}
free(rs);
return issub;
}

Expand Down Expand Up @@ -2750,6 +2741,8 @@ static int check_unsat_bound(jl_value_t *t, jl_tvar_t *v, jl_stenv_t *e) JL_NOTS
}


static int intersect_var_ccheck_in_env(jl_value_t *xlb, jl_value_t *xub, jl_value_t *ylb, jl_value_t *yub, jl_stenv_t *e, int flip);

static jl_value_t *intersect_var(jl_tvar_t *b, jl_value_t *a, jl_stenv_t *e, int8_t R, int param)
{
jl_varbinding_t *bb = lookup(e, b);
Expand All @@ -2761,20 +2754,14 @@ static jl_value_t *intersect_var(jl_tvar_t *b, jl_value_t *a, jl_stenv_t *e, int
return R ? intersect(a, bb->lb, e, param) : intersect(bb->lb, a, e, param);
if (!jl_is_type(a) && !jl_is_typevar(a))
return set_var_to_const(bb, a, e, R);
jl_savedenv_t se;
if (param == 2) {
jl_value_t *ub = NULL;
JL_GC_PUSH1(&ub);
if (!jl_has_free_typevars(a)) {
save_env(e, &se, 1);
int issub = subtype_in_env_existential(bb->lb, a, e);
restore_env(e, &se, 1);
if (issub) {
issub = subtype_in_env_existential(a, bb->ub, e);
restore_env(e, &se, 1);
}
free_env(&se);
if (!issub) {
if (R) flip_offset(e);
int ccheck = intersect_var_ccheck_in_env(bb->lb, bb->ub, a, a, e, !R);
if (R) flip_offset(e);
if (!ccheck) {
JL_GC_POP();
return jl_bottom_type;
}
Expand All @@ -2784,6 +2771,7 @@ static jl_value_t *intersect_var(jl_tvar_t *b, jl_value_t *a, jl_stenv_t *e, int
e->triangular++;
ub = R ? intersect_aside(a, bb->ub, e, bb->depth0) : intersect_aside(bb->ub, a, e, bb->depth0);
e->triangular--;
jl_savedenv_t se;
save_env(e, &se, 1);
int issub = subtype_in_env_existential(bb->lb, ub, e);
restore_env(e, &se, 1);
Expand Down Expand Up @@ -3856,6 +3844,89 @@ static int subtype_by_bounds(jl_value_t *x, jl_value_t *y, jl_stenv_t *e) JL_NOT
return compareto_var(x, (jl_tvar_t*)y, e, -1) || compareto_var(y, (jl_tvar_t*)x, e, 1);
}

static int intersect_var_ccheck_in_env(jl_value_t *xlb, jl_value_t *xub, jl_value_t *ylb, jl_value_t *yub, jl_stenv_t *e, int flip)
{
int easy_check1 = xlb == jl_bottom_type ||
yub == (jl_value_t *)jl_any_type ||
(e->Loffset == 0 && obviously_in_union(yub, xlb));
int easy_check2 = ylb == jl_bottom_type ||
xub == (jl_value_t *)jl_any_type ||
(e->Loffset == 0 && obviously_in_union(xub, ylb));
int nofree1 = 0, nofree2 = 0;
if (!easy_check1) {
nofree1 = !jl_has_free_typevars(xlb) && !jl_has_free_typevars(yub);
if (nofree1 && e->Loffset == 0) {
easy_check1 = jl_subtype(xlb, yub);
if (!easy_check1)
return 0;
}
}
if (!easy_check2) {
nofree2 = !jl_has_free_typevars(ylb) && !jl_has_free_typevars(xub);
if (nofree2 && e->Loffset == 0) {
easy_check2 = jl_subtype(ylb, xub);
if (!easy_check2)
return 0;
}
}
if (easy_check1 && easy_check2)
return 1;
int ccheck = 0;
if ((easy_check1 || nofree1) && (easy_check2 || nofree2)) {
jl_varbinding_t *vars = e->vars;
e->vars = NULL;
ccheck = easy_check1 || subtype_in_env(xlb, yub, e);
if (ccheck && !easy_check2) {
flip_offset(e);
ccheck = subtype_in_env(ylb, xub, e);
flip_offset(e);
}
e->vars = vars;
return ccheck;
}
jl_savedenv_t se;
save_env(e, &se, 1);
// first try normal flip.
if (flip) flip_vars(e);
ccheck = easy_check1 || subtype_in_env(xlb, yub, e);
if (ccheck && !easy_check2) {
flip_offset(e);
ccheck = subtype_in_env(ylb, xub, e);
flip_offset(e);
}
if (flip) flip_vars(e);
if (!ccheck) {
// then try reverse flip.
restore_env(e, &se, 1);
if (!flip) flip_vars(e);
ccheck = easy_check1 || subtype_in_env(xlb, yub, e);
if (ccheck && !easy_check2) {
flip_offset(e);
ccheck = subtype_in_env(ylb, xub, e);
flip_offset(e);
}
if (!flip) flip_vars(e);
}
if (!ccheck) {
// then try existential.
restore_env(e, &se, 1);
if (easy_check1)
ccheck = 1;
else {
ccheck = subtype_in_env_existential(xlb, yub, e);
restore_env(e, &se, 1);
}
if (ccheck && !easy_check2) {
flip_offset(e);
ccheck = subtype_in_env_existential(ylb, xub, e);
flip_offset(e);
restore_env(e, &se, 1);
}
}
free_env(&se);
return ccheck;
}

static int has_typevar_via_env(jl_value_t *x, jl_tvar_t *t, jl_stenv_t *e)
{
if (e->Loffset == 0) {
Expand Down Expand Up @@ -3988,14 +4059,8 @@ static jl_value_t *intersect(jl_value_t *x, jl_value_t *y, jl_stenv_t *e, int pa
ccheck = 1;
}
else {
if (R) flip_vars(e);
ccheck = subtype_in_env(xlb, yub, e);
if (ccheck) {
flip_offset(e);
ccheck = subtype_in_env(ylb, xub, e);
flip_offset(e);
}
if (R) flip_vars(e);
// try many subtype check to avoid false `Union{}`
ccheck = intersect_var_ccheck_in_env(xlb, xub, ylb, yub, e, R);
}
if (R) flip_offset(e);
if (!ccheck)
Expand Down
33 changes: 22 additions & 11 deletions test/subtype.jl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1691,9 +1691,7 @@ CovType{T} = Union{AbstractArray{T,2},
# issue #31703
@testintersect(Pair{<:Any, Ref{Tuple{Ref{Ref{Tuple{Int}}},Ref{Float64}}}},
Pair{T, S} where S<:(Ref{A} where A<:(Tuple{C,Ref{T}} where C<:(Ref{D} where D<:(Ref{E} where E<:Tuple{FF}) where FF<:B)) where B) where T,
Pair{T, Ref{Tuple{Ref{Ref{Tuple{Int}}},Ref{Float64}}}} where T)
# TODO: should be able to get this result
# Pair{Float64, Ref{Tuple{Ref{Ref{Tuple{Int}}},Ref{Float64}}}}
Pair{Float64, Ref{Tuple{Ref{Ref{Tuple{Int}}},Ref{Float64}}}})

module I31703
using Test, LinearAlgebra
Expand Down Expand Up @@ -1745,8 +1743,7 @@ end
Tuple{Type{SA{2, L}}, Type{SA{2, L}}} where L)
@testintersect(Tuple{Type{SA{2, L}}, Type{SA{2, 16}}} where L,
Tuple{Type{<:SA{N, L}}, Type{<:SA{N, L}}} where {N,L},
# TODO: this could be narrower
Tuple{Type{SA{2, L}}, Type{SA{2, 16}}} where L)
Tuple{Type{SA{2, 16}}, Type{SA{2, 16}}})

# issue #31993
@testintersect(Tuple{Type{<:AbstractVector{T}}, Int} where T,
Expand Down Expand Up @@ -1851,9 +1848,9 @@ c32703(::Type{<:Str{C}}, str::Str{C}) where {C<:CSE} = str
Tuple{Type{<:Str{C}}, Str{C}} where {C<:CSE},
Union{})
@test c32703(UTF16Str, ASCIIStr()) == 42
@test_broken typeintersect(Tuple{Vector{Vector{Float32}},Matrix,Matrix},
Tuple{Vector{V},Matrix{Int},Matrix{S}} where {S, V<:AbstractVector{S}}) ==
Tuple{Array{Array{Float32,1},1},Array{Int,2},Array{Float32,2}}
@testintersect(Tuple{Vector{Vector{Float32}},Matrix,Matrix},
Tuple{Vector{V},Matrix{Int},Matrix{S}} where {S, V<:AbstractVector{S}},
Tuple{Array{Array{Float32,1},1},Array{Int,2},Array{Float32,2}})

@testintersect(Tuple{Pair{Int, DataType}, Any},
Tuple{Pair{A, B} where B<:Type, Int} where A,
Expand Down Expand Up @@ -2469,16 +2466,18 @@ end
abstract type P47654{A} end
@test Wrapper47654{P47654, Vector{Union{P47654,Nothing}}} <: Wrapper47654

#issue 41561
@testintersect(Tuple{Vector{VT}, Vector{VT}} where {N1, VT<:AbstractVector{N1}},
Tuple{Vector{VN} where {N, VN<:AbstractVector{N}}, Vector{Vector{Float64}}},
Tuple{Vector{Vector{Float64}}, Vector{Vector{Float64}}})

@testset "known subtype/intersect issue" begin
#issue 45874
let S = Pair{Val{P}, AbstractVector{<:Union{P,<:AbstractMatrix{P}}}} where P,
T = Pair{Val{R}, AbstractVector{<:Union{P,<:AbstractMatrix{P}}}} where {P,R}
@test S <: T
end

#issue 41561
@test_broken typeintersect(Tuple{Vector{VT}, Vector{VT}} where {N1, VT<:AbstractVector{N1}},
Tuple{Vector{VN} where {N, VN<:AbstractVector{N}}, Vector{Vector{Float64}}}) !== Union{}
#issue 40865
@test Tuple{Set{Ref{Int}}, Set{Ref{Int}}} <: Tuple{Set{KV}, Set{K}} where {K,KV<:Union{K,Ref{K}}}
@test Tuple{Set{Val{Int}}, Set{Val{Int}}} <: Tuple{Set{KV}, Set{K}} where {K,KV<:Union{K,Val{K}}}
Expand Down Expand Up @@ -2746,3 +2745,15 @@ end
Val{Tuple{T,R,S}} where {T,R<:Vector{T},S<:Vector{R}},
Val{Tuple{Int, Vector{Int}, T}} where T<:Vector{Vector{Int}},
)

#issue 57429
@testintersect(
Pair{<:Any, <:Tuple{Int}},
Pair{N, S} where {N, NTuple{N,Int}<:S<:NTuple{M,Int} where {M}},
!Union{}
)
@testintersect(
Pair{N, T} where {N,NTuple{N,Int}<:T<:NTuple{N,Int}},
Pair{N, T} where {N,NTuple{N,Int}<:T<:Tuple{Int,Vararg{Int}}},
!Union{}
)
Loading