Skip to content

Commit 2253945

Browse files
N5N3KristofferC
authored andcommitted
Intersect: try normal+reverse+existential subtyping during intersection (#57476)
Typevars are all existential (in the sense of variable lb/ub) during intersection. This fix is somehow costly as we have to perform 3 times check to prove a false result. But a single existential <: seems too dangerous as it cause many circular env in the past. fix #57429 fix #41561 (cherry picked from commit beb928b)
1 parent 1a1dd13 commit 2253945

File tree

2 files changed

+118
-42
lines changed

2 files changed

+118
-42
lines changed

src/subtype.c

Lines changed: 96 additions & 31 deletions
Original file line numberDiff line numberDiff line change
@@ -2616,31 +2616,22 @@ static void set_bound(jl_value_t **bound, jl_value_t *val, jl_tvar_t *v, jl_sten
26162616
// subtype, treating all vars as existential
26172617
static int subtype_in_env_existential(jl_value_t *x, jl_value_t *y, jl_stenv_t *e)
26182618
{
2619-
jl_varbinding_t *v = e->vars;
2620-
int len = 0;
26212619
if (x == jl_bottom_type || y == (jl_value_t*)jl_any_type)
26222620
return 1;
2623-
while (v != NULL) {
2624-
len++;
2625-
v = v->prev;
2626-
}
2627-
int8_t *rs = (int8_t*)malloc_s(len);
2621+
int8_t *rs = (int8_t*)alloca(current_env_length(e));
2622+
jl_varbinding_t *v = e->vars;
26282623
int n = 0;
2629-
v = e->vars;
2630-
while (n < len) {
2631-
assert(v != NULL);
2624+
while (v != NULL) {
26322625
rs[n++] = v->right;
26332626
v->right = 1;
26342627
v = v->prev;
26352628
}
26362629
int issub = subtype_in_env(x, y, e);
26372630
n = 0; v = e->vars;
2638-
while (n < len) {
2639-
assert(v != NULL);
2631+
while (v != NULL) {
26402632
v->right = rs[n++];
26412633
v = v->prev;
26422634
}
2643-
free(rs);
26442635
return issub;
26452636
}
26462637

@@ -2688,6 +2679,8 @@ static int check_unsat_bound(jl_value_t *t, jl_tvar_t *v, jl_stenv_t *e) JL_NOTS
26882679
}
26892680

26902681

2682+
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);
2683+
26912684
static jl_value_t *intersect_var(jl_tvar_t *b, jl_value_t *a, jl_stenv_t *e, int8_t R, int param)
26922685
{
26932686
jl_varbinding_t *bb = lookup(e, b);
@@ -2699,20 +2692,14 @@ static jl_value_t *intersect_var(jl_tvar_t *b, jl_value_t *a, jl_stenv_t *e, int
26992692
return R ? intersect(a, bb->lb, e, param) : intersect(bb->lb, a, e, param);
27002693
if (!jl_is_type(a) && !jl_is_typevar(a))
27012694
return set_var_to_const(bb, a, e, R);
2702-
jl_savedenv_t se;
27032695
if (param == 2) {
27042696
jl_value_t *ub = NULL;
27052697
JL_GC_PUSH1(&ub);
27062698
if (!jl_has_free_typevars(a)) {
2707-
save_env(e, &se, 1);
2708-
int issub = subtype_in_env_existential(bb->lb, a, e);
2709-
restore_env(e, &se, 1);
2710-
if (issub) {
2711-
issub = subtype_in_env_existential(a, bb->ub, e);
2712-
restore_env(e, &se, 1);
2713-
}
2714-
free_env(&se);
2715-
if (!issub) {
2699+
if (R) flip_offset(e);
2700+
int ccheck = intersect_var_ccheck_in_env(bb->lb, bb->ub, a, a, e, !R);
2701+
if (R) flip_offset(e);
2702+
if (!ccheck) {
27162703
JL_GC_POP();
27172704
return jl_bottom_type;
27182705
}
@@ -2722,6 +2709,7 @@ static jl_value_t *intersect_var(jl_tvar_t *b, jl_value_t *a, jl_stenv_t *e, int
27222709
e->triangular++;
27232710
ub = R ? intersect_aside(a, bb->ub, e, bb->depth0) : intersect_aside(bb->ub, a, e, bb->depth0);
27242711
e->triangular--;
2712+
jl_savedenv_t se;
27252713
save_env(e, &se, 1);
27262714
int issub = subtype_in_env_existential(bb->lb, ub, e);
27272715
restore_env(e, &se, 1);
@@ -3654,6 +3642,89 @@ static int subtype_by_bounds(jl_value_t *x, jl_value_t *y, jl_stenv_t *e) JL_NOT
36543642
return compareto_var(x, (jl_tvar_t*)y, e, -1) || compareto_var(y, (jl_tvar_t*)x, e, 1);
36553643
}
36563644

3645+
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)
3646+
{
3647+
int easy_check1 = xlb == jl_bottom_type ||
3648+
yub == (jl_value_t *)jl_any_type ||
3649+
(e->Loffset == 0 && obviously_in_union(yub, xlb));
3650+
int easy_check2 = ylb == jl_bottom_type ||
3651+
xub == (jl_value_t *)jl_any_type ||
3652+
(e->Loffset == 0 && obviously_in_union(xub, ylb));
3653+
int nofree1 = 0, nofree2 = 0;
3654+
if (!easy_check1) {
3655+
nofree1 = !jl_has_free_typevars(xlb) && !jl_has_free_typevars(yub);
3656+
if (nofree1 && e->Loffset == 0) {
3657+
easy_check1 = jl_subtype(xlb, yub);
3658+
if (!easy_check1)
3659+
return 0;
3660+
}
3661+
}
3662+
if (!easy_check2) {
3663+
nofree2 = !jl_has_free_typevars(ylb) && !jl_has_free_typevars(xub);
3664+
if (nofree2 && e->Loffset == 0) {
3665+
easy_check2 = jl_subtype(ylb, xub);
3666+
if (!easy_check2)
3667+
return 0;
3668+
}
3669+
}
3670+
if (easy_check1 && easy_check2)
3671+
return 1;
3672+
int ccheck = 0;
3673+
if ((easy_check1 || nofree1) && (easy_check2 || nofree2)) {
3674+
jl_varbinding_t *vars = e->vars;
3675+
e->vars = NULL;
3676+
ccheck = easy_check1 || subtype_in_env(xlb, yub, e);
3677+
if (ccheck && !easy_check2) {
3678+
flip_offset(e);
3679+
ccheck = subtype_in_env(ylb, xub, e);
3680+
flip_offset(e);
3681+
}
3682+
e->vars = vars;
3683+
return ccheck;
3684+
}
3685+
jl_savedenv_t se;
3686+
save_env(e, &se, 1);
3687+
// first try normal flip.
3688+
if (flip) flip_vars(e);
3689+
ccheck = easy_check1 || subtype_in_env(xlb, yub, e);
3690+
if (ccheck && !easy_check2) {
3691+
flip_offset(e);
3692+
ccheck = subtype_in_env(ylb, xub, e);
3693+
flip_offset(e);
3694+
}
3695+
if (flip) flip_vars(e);
3696+
if (!ccheck) {
3697+
// then try reverse flip.
3698+
restore_env(e, &se, 1);
3699+
if (!flip) flip_vars(e);
3700+
ccheck = easy_check1 || subtype_in_env(xlb, yub, e);
3701+
if (ccheck && !easy_check2) {
3702+
flip_offset(e);
3703+
ccheck = subtype_in_env(ylb, xub, e);
3704+
flip_offset(e);
3705+
}
3706+
if (!flip) flip_vars(e);
3707+
}
3708+
if (!ccheck) {
3709+
// then try existential.
3710+
restore_env(e, &se, 1);
3711+
if (easy_check1)
3712+
ccheck = 1;
3713+
else {
3714+
ccheck = subtype_in_env_existential(xlb, yub, e);
3715+
restore_env(e, &se, 1);
3716+
}
3717+
if (ccheck && !easy_check2) {
3718+
flip_offset(e);
3719+
ccheck = subtype_in_env_existential(ylb, xub, e);
3720+
flip_offset(e);
3721+
restore_env(e, &se, 1);
3722+
}
3723+
}
3724+
free_env(&se);
3725+
return ccheck;
3726+
}
3727+
36573728
static int has_typevar_via_env(jl_value_t *x, jl_tvar_t *t, jl_stenv_t *e)
36583729
{
36593730
if (e->Loffset == 0) {
@@ -3786,14 +3857,8 @@ static jl_value_t *intersect(jl_value_t *x, jl_value_t *y, jl_stenv_t *e, int pa
37863857
ccheck = 1;
37873858
}
37883859
else {
3789-
if (R) flip_vars(e);
3790-
ccheck = subtype_in_env(xlb, yub, e);
3791-
if (ccheck) {
3792-
flip_offset(e);
3793-
ccheck = subtype_in_env(ylb, xub, e);
3794-
flip_offset(e);
3795-
}
3796-
if (R) flip_vars(e);
3860+
// try many subtype check to avoid false `Union{}`
3861+
ccheck = intersect_var_ccheck_in_env(xlb, xub, ylb, yub, e, R);
37973862
}
37983863
if (R) flip_offset(e);
37993864
if (!ccheck)

test/subtype.jl

Lines changed: 22 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -1689,9 +1689,7 @@ CovType{T} = Union{AbstractArray{T,2},
16891689
# issue #31703
16901690
@testintersect(Pair{<:Any, Ref{Tuple{Ref{Ref{Tuple{Int}}},Ref{Float64}}}},
16911691
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,
1692-
Pair{T, Ref{Tuple{Ref{Ref{Tuple{Int}}},Ref{Float64}}}} where T)
1693-
# TODO: should be able to get this result
1694-
# Pair{Float64, Ref{Tuple{Ref{Ref{Tuple{Int}}},Ref{Float64}}}}
1692+
Pair{Float64, Ref{Tuple{Ref{Ref{Tuple{Int}}},Ref{Float64}}}})
16951693

16961694
module I31703
16971695
using Test, LinearAlgebra
@@ -1743,8 +1741,7 @@ end
17431741
Tuple{Type{SA{2, L}}, Type{SA{2, L}}} where L)
17441742
@testintersect(Tuple{Type{SA{2, L}}, Type{SA{2, 16}}} where L,
17451743
Tuple{Type{<:SA{N, L}}, Type{<:SA{N, L}}} where {N,L},
1746-
# TODO: this could be narrower
1747-
Tuple{Type{SA{2, L}}, Type{SA{2, 16}}} where L)
1744+
Tuple{Type{SA{2, 16}}, Type{SA{2, 16}}})
17481745

17491746
# issue #31993
17501747
@testintersect(Tuple{Type{<:AbstractVector{T}}, Int} where T,
@@ -1849,9 +1846,9 @@ c32703(::Type{<:Str{C}}, str::Str{C}) where {C<:CSE} = str
18491846
Tuple{Type{<:Str{C}}, Str{C}} where {C<:CSE},
18501847
Union{})
18511848
@test c32703(UTF16Str, ASCIIStr()) == 42
1852-
@test_broken typeintersect(Tuple{Vector{Vector{Float32}},Matrix,Matrix},
1853-
Tuple{Vector{V},Matrix{Int},Matrix{S}} where {S, V<:AbstractVector{S}}) ==
1854-
Tuple{Array{Array{Float32,1},1},Array{Int,2},Array{Float32,2}}
1849+
@testintersect(Tuple{Vector{Vector{Float32}},Matrix,Matrix},
1850+
Tuple{Vector{V},Matrix{Int},Matrix{S}} where {S, V<:AbstractVector{S}},
1851+
Tuple{Array{Array{Float32,1},1},Array{Int,2},Array{Float32,2}})
18551852

18561853
@testintersect(Tuple{Pair{Int, DataType}, Any},
18571854
Tuple{Pair{A, B} where B<:Type, Int} where A,
@@ -2447,16 +2444,18 @@ end
24472444
abstract type P47654{A} end
24482445
@test Wrapper47654{P47654, Vector{Union{P47654,Nothing}}} <: Wrapper47654
24492446

2447+
#issue 41561
2448+
@testintersect(Tuple{Vector{VT}, Vector{VT}} where {N1, VT<:AbstractVector{N1}},
2449+
Tuple{Vector{VN} where {N, VN<:AbstractVector{N}}, Vector{Vector{Float64}}},
2450+
Tuple{Vector{Vector{Float64}}, Vector{Vector{Float64}}})
2451+
24502452
@testset "known subtype/intersect issue" begin
24512453
#issue 45874
24522454
let S = Pair{Val{P}, AbstractVector{<:Union{P,<:AbstractMatrix{P}}}} where P,
24532455
T = Pair{Val{R}, AbstractVector{<:Union{P,<:AbstractMatrix{P}}}} where {P,R}
24542456
@test S <: T
24552457
end
24562458

2457-
#issue 41561
2458-
@test_broken typeintersect(Tuple{Vector{VT}, Vector{VT}} where {N1, VT<:AbstractVector{N1}},
2459-
Tuple{Vector{VN} where {N, VN<:AbstractVector{N}}, Vector{Vector{Float64}}}) !== Union{}
24602459
#issue 40865
24612460
@test Tuple{Set{Ref{Int}}, Set{Ref{Int}}} <: Tuple{Set{KV}, Set{K}} where {K,KV<:Union{K,Ref{K}}}
24622461
@test Tuple{Set{Val{Int}}, Set{Val{Int}}} <: Tuple{Set{KV}, Set{K}} where {K,KV<:Union{K,Val{K}}}
@@ -2695,3 +2694,15 @@ end
26952694
Val{Tuple{T,R,S}} where {T,R<:Vector{T},S<:Vector{R}},
26962695
Val{Tuple{Int, Vector{Int}, T}} where T<:Vector{Vector{Int}},
26972696
)
2697+
2698+
#issue 57429
2699+
@testintersect(
2700+
Pair{<:Any, <:Tuple{Int}},
2701+
Pair{N, S} where {N, NTuple{N,Int}<:S<:NTuple{M,Int} where {M}},
2702+
!Union{}
2703+
)
2704+
@testintersect(
2705+
Pair{N, T} where {N,NTuple{N,Int}<:T<:NTuple{N,Int}},
2706+
Pair{N, T} where {N,NTuple{N,Int}<:T<:Tuple{Int,Vararg{Int}}},
2707+
!Union{}
2708+
)

0 commit comments

Comments
 (0)