Skip to content

Commit 31f0afd

Browse files
N5N3N5N3
committed
Intersect: try normal+reverse+existential subtyping during intersection
fix #57429 #41561 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.
1 parent 0fb5fa0 commit 31f0afd

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
@@ -2678,31 +2678,22 @@ static void set_bound(jl_value_t **bound, jl_value_t *val, jl_tvar_t *v, jl_sten
26782678
// subtype, treating all vars as existential
26792679
static int subtype_in_env_existential(jl_value_t *x, jl_value_t *y, jl_stenv_t *e)
26802680
{
2681-
jl_varbinding_t *v = e->vars;
2682-
int len = 0;
26832681
if (x == jl_bottom_type || y == (jl_value_t*)jl_any_type)
26842682
return 1;
2685-
while (v != NULL) {
2686-
len++;
2687-
v = v->prev;
2688-
}
2689-
int8_t *rs = (int8_t*)malloc_s(len);
2683+
int8_t *rs = (int8_t*)alloca(current_env_length(e));
2684+
jl_varbinding_t *v = e->vars;
26902685
int n = 0;
2691-
v = e->vars;
2692-
while (n < len) {
2693-
assert(v != NULL);
2686+
while (v != NULL) {
26942687
rs[n++] = v->right;
26952688
v->right = 1;
26962689
v = v->prev;
26972690
}
26982691
int issub = subtype_in_env(x, y, e);
26992692
n = 0; v = e->vars;
2700-
while (n < len) {
2701-
assert(v != NULL);
2693+
while (v != NULL) {
27022694
v->right = rs[n++];
27032695
v = v->prev;
27042696
}
2705-
free(rs);
27062697
return issub;
27072698
}
27082699

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

27522743

2744+
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);
2745+
27532746
static jl_value_t *intersect_var(jl_tvar_t *b, jl_value_t *a, jl_stenv_t *e, int8_t R, int param)
27542747
{
27552748
jl_varbinding_t *bb = lookup(e, b);
@@ -2761,20 +2754,14 @@ static jl_value_t *intersect_var(jl_tvar_t *b, jl_value_t *a, jl_stenv_t *e, int
27612754
return R ? intersect(a, bb->lb, e, param) : intersect(bb->lb, a, e, param);
27622755
if (!jl_is_type(a) && !jl_is_typevar(a))
27632756
return set_var_to_const(bb, a, e, R);
2764-
jl_savedenv_t se;
27652757
if (param == 2) {
27662758
jl_value_t *ub = NULL;
27672759
JL_GC_PUSH1(&ub);
27682760
if (!jl_has_free_typevars(a)) {
2769-
save_env(e, &se, 1);
2770-
int issub = subtype_in_env_existential(bb->lb, a, e);
2771-
restore_env(e, &se, 1);
2772-
if (issub) {
2773-
issub = subtype_in_env_existential(a, bb->ub, e);
2774-
restore_env(e, &se, 1);
2775-
}
2776-
free_env(&se);
2777-
if (!issub) {
2761+
if (R) flip_offset(e);
2762+
int ccheck = intersect_var_ccheck_in_env(bb->lb, bb->ub, a, a, e, !R);
2763+
if (R) flip_offset(e);
2764+
if (!ccheck) {
27782765
JL_GC_POP();
27792766
return jl_bottom_type;
27802767
}
@@ -2784,6 +2771,7 @@ static jl_value_t *intersect_var(jl_tvar_t *b, jl_value_t *a, jl_stenv_t *e, int
27842771
e->triangular++;
27852772
ub = R ? intersect_aside(a, bb->ub, e, bb->depth0) : intersect_aside(bb->ub, a, e, bb->depth0);
27862773
e->triangular--;
2774+
jl_savedenv_t se;
27872775
save_env(e, &se, 1);
27882776
int issub = subtype_in_env_existential(bb->lb, ub, e);
27892777
restore_env(e, &se, 1);
@@ -3856,6 +3844,89 @@ static int subtype_by_bounds(jl_value_t *x, jl_value_t *y, jl_stenv_t *e) JL_NOT
38563844
return compareto_var(x, (jl_tvar_t*)y, e, -1) || compareto_var(y, (jl_tvar_t*)x, e, 1);
38573845
}
38583846

3847+
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)
3848+
{
3849+
int easy_check1 = xlb == jl_bottom_type ||
3850+
yub == (jl_value_t *)jl_any_type ||
3851+
(e->Loffset == 0 && obviously_in_union(yub, xlb));
3852+
int easy_check2 = ylb == jl_bottom_type ||
3853+
xub == (jl_value_t *)jl_any_type ||
3854+
(e->Loffset == 0 && obviously_in_union(xub, ylb));
3855+
int nofree1 = 0, nofree2 = 0;
3856+
if (!easy_check1) {
3857+
nofree1 = !jl_has_free_typevars(xlb) && !jl_has_free_typevars(yub);
3858+
if (nofree1 && e->Loffset == 0) {
3859+
easy_check1 = jl_subtype(xlb, yub);
3860+
if (!easy_check1)
3861+
return 0;
3862+
}
3863+
}
3864+
if (!easy_check2) {
3865+
nofree2 = !jl_has_free_typevars(ylb) && !jl_has_free_typevars(xub);
3866+
if (nofree2 && e->Loffset == 0) {
3867+
easy_check2 = jl_subtype(ylb, xub);
3868+
if (!easy_check2)
3869+
return 0;
3870+
}
3871+
}
3872+
if (easy_check1 && easy_check2)
3873+
return 1;
3874+
int ccheck = 0;
3875+
if ((easy_check1 || nofree1) && (easy_check2 || nofree2)) {
3876+
jl_varbinding_t *vars = e->vars;
3877+
e->vars = NULL;
3878+
ccheck = easy_check1 || subtype_in_env(xlb, yub, e);
3879+
if (ccheck && !easy_check2) {
3880+
flip_offset(e);
3881+
ccheck = subtype_in_env(ylb, xub, e);
3882+
flip_offset(e);
3883+
}
3884+
e->vars = vars;
3885+
return ccheck;
3886+
}
3887+
jl_savedenv_t se;
3888+
save_env(e, &se, 1);
3889+
// first try normal flip.
3890+
if (flip) flip_vars(e);
3891+
ccheck = easy_check1 || subtype_in_env(xlb, yub, e);
3892+
if (ccheck && !easy_check2) {
3893+
flip_offset(e);
3894+
ccheck = subtype_in_env(ylb, xub, e);
3895+
flip_offset(e);
3896+
}
3897+
if (flip) flip_vars(e);
3898+
if (!ccheck) {
3899+
// then try reverse flip.
3900+
restore_env(e, &se, 1);
3901+
if (!flip) flip_vars(e);
3902+
ccheck = easy_check1 || subtype_in_env(xlb, yub, e);
3903+
if (ccheck && !easy_check2) {
3904+
flip_offset(e);
3905+
ccheck = subtype_in_env(ylb, xub, e);
3906+
flip_offset(e);
3907+
}
3908+
if (!flip) flip_vars(e);
3909+
}
3910+
if (!ccheck) {
3911+
// then try existential.
3912+
restore_env(e, &se, 1);
3913+
if (easy_check1)
3914+
ccheck = 1;
3915+
else {
3916+
ccheck = subtype_in_env_existential(xlb, yub, e);
3917+
restore_env(e, &se, 1);
3918+
}
3919+
if (ccheck && !easy_check2) {
3920+
flip_offset(e);
3921+
ccheck = subtype_in_env_existential(ylb, xub, e);
3922+
flip_offset(e);
3923+
restore_env(e, &se, 1);
3924+
}
3925+
}
3926+
free_env(&se);
3927+
return ccheck;
3928+
}
3929+
38593930
static int has_typevar_via_env(jl_value_t *x, jl_tvar_t *t, jl_stenv_t *e)
38603931
{
38613932
if (e->Loffset == 0) {
@@ -3988,14 +4059,8 @@ static jl_value_t *intersect(jl_value_t *x, jl_value_t *y, jl_stenv_t *e, int pa
39884059
ccheck = 1;
39894060
}
39904061
else {
3991-
if (R) flip_vars(e);
3992-
ccheck = subtype_in_env(xlb, yub, e);
3993-
if (ccheck) {
3994-
flip_offset(e);
3995-
ccheck = subtype_in_env(ylb, xub, e);
3996-
flip_offset(e);
3997-
}
3998-
if (R) flip_vars(e);
4062+
// try many subtype check to avoid false `Union{}`
4063+
ccheck = intersect_var_ccheck_in_env(xlb, xub, ylb, yub, e, R);
39994064
}
40004065
if (R) flip_offset(e);
40014066
if (!ccheck)

‎test/subtype.jl‎

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

16981696
module I31703
16991697
using Test, LinearAlgebra
@@ -1745,8 +1743,7 @@ end
17451743
Tuple{Type{SA{2, L}}, Type{SA{2, L}}} where L)
17461744
@testintersect(Tuple{Type{SA{2, L}}, Type{SA{2, 16}}} where L,
17471745
Tuple{Type{<:SA{N, L}}, Type{<:SA{N, L}}} where {N,L},
1748-
# TODO: this could be narrower
1749-
Tuple{Type{SA{2, L}}, Type{SA{2, 16}}} where L)
1746+
Tuple{Type{SA{2, 16}}, Type{SA{2, 16}}})
17501747

17511748
# issue #31993
17521749
@testintersect(Tuple{Type{<:AbstractVector{T}}, Int} where T,
@@ -1851,9 +1848,9 @@ c32703(::Type{<:Str{C}}, str::Str{C}) where {C<:CSE} = str
18511848
Tuple{Type{<:Str{C}}, Str{C}} where {C<:CSE},
18521849
Union{})
18531850
@test c32703(UTF16Str, ASCIIStr()) == 42
1854-
@test_broken typeintersect(Tuple{Vector{Vector{Float32}},Matrix,Matrix},
1855-
Tuple{Vector{V},Matrix{Int},Matrix{S}} where {S, V<:AbstractVector{S}}) ==
1856-
Tuple{Array{Array{Float32,1},1},Array{Int,2},Array{Float32,2}}
1851+
@testintersect(Tuple{Vector{Vector{Float32}},Matrix,Matrix},
1852+
Tuple{Vector{V},Matrix{Int},Matrix{S}} where {S, V<:AbstractVector{S}},
1853+
Tuple{Array{Array{Float32,1},1},Array{Int,2},Array{Float32,2}})
18571854

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

2469+
#issue 41561
2470+
@testintersect(Tuple{Vector{VT}, Vector{VT}} where {N1, VT<:AbstractVector{N1}},
2471+
Tuple{Vector{VN} where {N, VN<:AbstractVector{N}}, Vector{Vector{Float64}}},
2472+
Tuple{Vector{Vector{Float64}}, Vector{Vector{Float64}}})
2473+
24722474
@testset "known subtype/intersect issue" begin
24732475
#issue 45874
24742476
let S = Pair{Val{P}, AbstractVector{<:Union{P,<:AbstractMatrix{P}}}} where P,
24752477
T = Pair{Val{R}, AbstractVector{<:Union{P,<:AbstractMatrix{P}}}} where {P,R}
24762478
@test S <: T
24772479
end
24782480

2479-
#issue 41561
2480-
@test_broken typeintersect(Tuple{Vector{VT}, Vector{VT}} where {N1, VT<:AbstractVector{N1}},
2481-
Tuple{Vector{VN} where {N, VN<:AbstractVector{N}}, Vector{Vector{Float64}}}) !== Union{}
24822481
#issue 40865
24832482
@test Tuple{Set{Ref{Int}}, Set{Ref{Int}}} <: Tuple{Set{KV}, Set{K}} where {K,KV<:Union{K,Ref{K}}}
24842483
@test Tuple{Set{Val{Int}}, Set{Val{Int}}} <: Tuple{Set{KV}, Set{K}} where {K,KV<:Union{K,Val{K}}}
@@ -2746,3 +2745,15 @@ end
27462745
Val{Tuple{T,R,S}} where {T,R<:Vector{T},S<:Vector{R}},
27472746
Val{Tuple{Int, Vector{Int}, T}} where T<:Vector{Vector{Int}},
27482747
)
2748+
2749+
#issue 57429
2750+
@testintersect(
2751+
Pair{<:Any, <:Tuple{Int}},
2752+
Pair{N, S} where {N, NTuple{N,Int}<:S<:NTuple{M,Int} where {M}},
2753+
!Union{}
2754+
)
2755+
@testintersect(
2756+
Pair{N, T} where {N,NTuple{N,Int}<:T<:NTuple{N,Int}},
2757+
Pair{N, T} where {N,NTuple{N,Int}<:T<:Tuple{Int,Vararg{Int}}},
2758+
!Union{}
2759+
)

0 commit comments

Comments
 (0)