Skip to content

Commit 0d9c72d

Browse files
authored
fix #32386, type intersection bug in var bounds (#32425)
might be related to #24333 and/or #21153
1 parent 8ff014f commit 0d9c72d

File tree

2 files changed

+57
-26
lines changed

2 files changed

+57
-26
lines changed

src/subtype.c

Lines changed: 52 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -92,7 +92,8 @@ typedef struct jl_stenv_t {
9292
jl_value_t **envout; // for passing caller the computed bounds of right-side variables
9393
int envsz; // length of envout
9494
int envidx; // current index in envout
95-
int invdepth; // current number of invariant constructors we're nested in
95+
int invdepth; // # of invariant constructors we're nested in on the left
96+
int Rinvdepth; // # of invariant constructors we're nested in on the right
9697
int ignore_free; // treat free vars as black boxes; used during intersection
9798
int intersection; // true iff subtype is being called from intersection
9899
int emptiness_only; // true iff intersection only needs to test for emptiness
@@ -535,7 +536,7 @@ static void record_var_occurrence(jl_varbinding_t *vb, jl_stenv_t *e, int param)
535536
{
536537
if (vb != NULL && param) {
537538
// saturate counters at 2; we don't need values bigger than that
538-
if (param == 2 && e->invdepth > vb->depth0 && vb->occurs_inv < 2)
539+
if (param == 2 && (vb->right ? e->Rinvdepth : e->invdepth) > vb->depth0 && vb->occurs_inv < 2)
539540
vb->occurs_inv++;
540541
else if (vb->occurs_cov < 2)
541542
vb->occurs_cov++;
@@ -554,7 +555,7 @@ static int var_outside(jl_stenv_t *e, jl_tvar_t *x, jl_tvar_t *y)
554555
return 0;
555556
}
556557

557-
static jl_value_t *intersect_aside(jl_value_t *x, jl_value_t *y, jl_stenv_t *e, int depth);
558+
static jl_value_t *intersect_aside(jl_value_t *x, jl_value_t *y, jl_stenv_t *e, int R, int d);
558559

559560
// check that type var `b` is <: `a`, and update b's upper bound.
560561
static int var_lt(jl_tvar_t *b, jl_value_t *a, jl_stenv_t *e, int param)
@@ -572,7 +573,7 @@ static int var_lt(jl_tvar_t *b, jl_value_t *a, jl_stenv_t *e, int param)
572573
// for this to work we need to compute issub(left,right) before issub(right,left),
573574
// since otherwise the issub(a, bb.ub) check in var_gt becomes vacuous.
574575
if (e->intersection) {
575-
jl_value_t *ub = intersect_aside(bb->ub, a, e, bb->depth0);
576+
jl_value_t *ub = intersect_aside(bb->ub, a, e, 0, bb->depth0);
576577
if (ub != (jl_value_t*)b)
577578
bb->ub = ub;
578579
}
@@ -687,7 +688,8 @@ typedef int (*tvar_callback)(void*, int8_t, jl_stenv_t *, int);
687688

688689
static int with_tvar(tvar_callback callback, void *context, jl_unionall_t *u, int8_t R, jl_stenv_t *e, int param)
689690
{
690-
jl_varbinding_t vb = { u->var, u->var->lb, u->var->ub, R, NULL, 0, 0, 0, 0, e->invdepth, 0, NULL, e->vars };
691+
jl_varbinding_t vb = { u->var, u->var->lb, u->var->ub, R, NULL, 0, 0, 0, 0,
692+
R ? e->Rinvdepth : e->invdepth, 0, NULL, e->vars };
691693
JL_GC_PUSH4(&u, &vb.lb, &vb.ub, &vb.innervars);
692694
e->vars = &vb;
693695
int ans;
@@ -854,8 +856,10 @@ static int check_vararg_length(jl_value_t *v, ssize_t n, jl_stenv_t *e)
854856
jl_value_t *nn = jl_box_long(n);
855857
JL_GC_PUSH1(&nn);
856858
e->invdepth++;
859+
e->Rinvdepth++;
857860
int ans = subtype(nn, N, e, 2) && subtype(N, nn, e, 0);
858861
e->invdepth--;
862+
e->Rinvdepth--;
859863
JL_GC_POP();
860864
if (!ans)
861865
return 0;
@@ -955,6 +959,7 @@ static int subtype_tuple_varargs(struct subtype_tuple_env *env, jl_stenv_t *e, i
955959

956960
// Vararg{T,N} <: Vararg{T2,N2}; equate N and N2
957961
e->invdepth++;
962+
e->Rinvdepth++;
958963
JL_GC_PUSH2(&xp1, &yp1);
959964
if (jl_is_long(xp1) && env->vx != 1)
960965
xp1 = jl_box_long(jl_unbox_long(xp1) - env->vx + 1);
@@ -963,6 +968,7 @@ static int subtype_tuple_varargs(struct subtype_tuple_env *env, jl_stenv_t *e, i
963968
int ans = forall_exists_equal(xp1, yp1, e);
964969
JL_GC_POP();
965970
e->invdepth--;
971+
e->Rinvdepth--;
966972
return ans;
967973
}
968974

@@ -1146,9 +1152,11 @@ static int subtype_naked_vararg(jl_datatype_t *xd, jl_datatype_t *yd, jl_stenv_t
11461152
if (!subtype(xp1, yp1, e, 1)) return 0;
11471153
if (!subtype(xp1, yp1, e, 1)) return 0;
11481154
e->invdepth++;
1155+
e->Rinvdepth++;
11491156
// Vararg{T,N} <: Vararg{T2,N2}; equate N and N2
11501157
int ans = forall_exists_equal(xp2, yp2, e);
11511158
e->invdepth--;
1159+
e->Rinvdepth--;
11521160
return ans;
11531161
}
11541162

@@ -1287,13 +1295,15 @@ static int subtype(jl_value_t *x, jl_value_t *y, jl_stenv_t *e, int param)
12871295
size_t i, np = jl_nparams(xd);
12881296
int ans = 1;
12891297
e->invdepth++;
1298+
e->Rinvdepth++;
12901299
for (i=0; i < np; i++) {
12911300
jl_value_t *xi = jl_tparam(xd, i), *yi = jl_tparam(yd, i);
12921301
if (!(xi == yi || forall_exists_equal(xi, yi, e))) {
12931302
ans = 0; break;
12941303
}
12951304
}
12961305
e->invdepth--;
1306+
e->Rinvdepth--;
12971307
return ans;
12981308
}
12991309
if (jl_is_type(y))
@@ -1404,7 +1414,7 @@ static void init_stenv(jl_stenv_t *e, jl_value_t **env, int envsz)
14041414
if (envsz)
14051415
memset(env, 0, envsz*sizeof(void*));
14061416
e->envidx = 0;
1407-
e->invdepth = 0;
1417+
e->invdepth = e->Rinvdepth = 0;
14081418
e->ignore_free = 0;
14091419
e->intersection = 0;
14101420
e->emptiness_only = 0;
@@ -1750,20 +1760,31 @@ JL_DLLEXPORT int jl_subtype_env(jl_value_t *x, jl_value_t *y, jl_value_t **env,
17501760
return subtype;
17511761
}
17521762

1753-
static int subtype_in_env(jl_value_t *x, jl_value_t *y, jl_stenv_t *e)
1763+
static int subtype_in_env_(jl_value_t *x, jl_value_t *y, jl_stenv_t *e, int invdepth, int Rinvdepth)
17541764
{
17551765
jl_stenv_t e2;
17561766
init_stenv(&e2, NULL, 0);
17571767
e2.vars = e->vars;
17581768
e2.intersection = e->intersection;
17591769
e2.ignore_free = e->ignore_free;
1760-
e2.invdepth = e->invdepth;
1770+
e2.invdepth = invdepth;
1771+
e2.Rinvdepth = Rinvdepth;
17611772
e2.envsz = e->envsz;
17621773
e2.envout = e->envout;
17631774
e2.envidx = e->envidx;
17641775
return forall_exists_subtype(x, y, &e2, 0);
17651776
}
17661777

1778+
static int subtype_in_env(jl_value_t *x, jl_value_t *y, jl_stenv_t *e)
1779+
{
1780+
return subtype_in_env_(x, y, e, e->invdepth, e->Rinvdepth);
1781+
}
1782+
1783+
static int subtype_bounds_in_env(jl_value_t *x, jl_value_t *y, jl_stenv_t *e, int R, int d)
1784+
{
1785+
return subtype_in_env_(x, y, e, R ? e->invdepth : d, R ? d : e->Rinvdepth);
1786+
}
1787+
17671788
JL_DLLEXPORT int jl_subtype(jl_value_t *x, jl_value_t *y)
17681789
{
17691790
return jl_subtype_env(x, y, NULL, 0);
@@ -1978,22 +1999,24 @@ static jl_value_t *intersect(jl_value_t *x, jl_value_t *y, jl_stenv_t *e, int pa
19781999
static jl_value_t *intersect_all(jl_value_t *x, jl_value_t *y, jl_stenv_t *e);
19792000

19802001
// intersect in nested union environment, similar to subtype_ccheck
1981-
static jl_value_t *intersect_aside(jl_value_t *x, jl_value_t *y, jl_stenv_t *e, int depth)
2002+
static jl_value_t *intersect_aside(jl_value_t *x, jl_value_t *y, jl_stenv_t *e, int R, int d)
19822003
{
19832004
// band-aid for #30335
19842005
if (x == (jl_value_t*)jl_any_type && !jl_is_typevar(y))
19852006
return y;
19862007
if (y == (jl_value_t*)jl_any_type && !jl_is_typevar(x))
19872008
return x;
19882009

1989-
int savedepth = e->invdepth;
19902010
jl_unionstate_t oldRunions = e->Runions;
1991-
e->invdepth = depth;
2011+
int savedepth = e->invdepth, Rsavedepth = e->Rinvdepth;
2012+
// TODO: this doesn't quite make sense
2013+
e->invdepth = e->Rinvdepth = d;
19922014

19932015
jl_value_t *res = intersect_all(x, y, e);
19942016

19952017
e->Runions = oldRunions;
19962018
e->invdepth = savedepth;
2019+
e->Rinvdepth = Rsavedepth;
19972020
return res;
19982021
}
19992022

@@ -2037,12 +2060,12 @@ static jl_value_t *set_var_to_const(jl_varbinding_t *bb, jl_value_t *v JL_MAYBE_
20372060
return v;
20382061
}
20392062

2040-
static int try_subtype_in_env(jl_value_t *a, jl_value_t *b, jl_stenv_t *e)
2063+
static int try_subtype_in_env(jl_value_t *a, jl_value_t *b, jl_stenv_t *e, int R, int d)
20412064
{
20422065
jl_value_t *root=NULL; jl_savedenv_t se;
20432066
JL_GC_PUSH1(&root);
20442067
save_env(e, &root, &se);
2045-
int ret = subtype_in_env(a, b, e);
2068+
int ret = subtype_bounds_in_env(a, b, e, R, d);
20462069
restore_env(e, root, &se);
20472070
free(se.buf);
20482071
JL_GC_POP();
@@ -2064,7 +2087,7 @@ static void set_bound(jl_value_t **bound, jl_value_t *val, jl_tvar_t *v, jl_sten
20642087
}
20652088

20662089
// subtype, treating all vars as existential
2067-
static int subtype_in_env_existential(jl_value_t *x, jl_value_t *y, jl_stenv_t *e)
2090+
static int subtype_in_env_existential(jl_value_t *x, jl_value_t *y, jl_stenv_t *e, int R, int d)
20682091
{
20692092
jl_varbinding_t *v = e->vars;
20702093
int len = 0;
@@ -2083,7 +2106,7 @@ static int subtype_in_env_existential(jl_value_t *x, jl_value_t *y, jl_stenv_t *
20832106
v->right = 1;
20842107
v = v->prev;
20852108
}
2086-
int issub = subtype_in_env(x, y, e);
2109+
int issub = subtype_bounds_in_env(x, y, e, R, d);
20872110
n = 0; v = e->vars;
20882111
while (n < len) {
20892112
assert(v != NULL);
@@ -2098,15 +2121,15 @@ static jl_value_t *intersect_var(jl_tvar_t *b, jl_value_t *a, jl_stenv_t *e, int
20982121
{
20992122
jl_varbinding_t *bb = lookup(e, b);
21002123
if (bb == NULL)
2101-
return R ? intersect_aside(a, b->ub, e, 0) : intersect_aside(b->ub, a, e, 0);
2124+
return R ? intersect_aside(a, b->ub, e, 1, 0) : intersect_aside(b->ub, a, e, 0, 0);
21022125
if (bb->lb == bb->ub && jl_is_typevar(bb->lb) && bb->lb != (jl_value_t*)b)
21032126
return intersect(a, bb->lb, e, param);
21042127
if (!jl_is_type(a) && !jl_is_typevar(a))
21052128
return set_var_to_const(bb, a, NULL);
21062129
int d = bb->depth0;
21072130
jl_value_t *root=NULL; jl_savedenv_t se;
21082131
if (param == 2) {
2109-
if (!(subtype_in_env_existential(bb->lb, a, e) && subtype_in_env_existential(a, bb->ub, e)))
2132+
if (!(subtype_in_env_existential(bb->lb, a, e, 0, d) && subtype_in_env_existential(a, bb->ub, e, 1, d)))
21102133
return jl_bottom_type;
21112134
jl_value_t *ub = a;
21122135
if (ub != (jl_value_t*)b) {
@@ -2131,17 +2154,17 @@ static jl_value_t *intersect_var(jl_tvar_t *b, jl_value_t *a, jl_stenv_t *e, int
21312154
}
21322155
else if (bb->constraintkind == 0) {
21332156
if (!jl_is_typevar(bb->ub) && !jl_is_typevar(a)) {
2134-
if (try_subtype_in_env(bb->ub, a, e))
2157+
if (try_subtype_in_env(bb->ub, a, e, 0, d))
21352158
return (jl_value_t*)b;
21362159
}
2137-
return R ? intersect_aside(a, bb->ub, e, d) : intersect_aside(bb->ub, a, e, d);
2160+
return R ? intersect_aside(a, bb->ub, e, 1, d) : intersect_aside(bb->ub, a, e, 0, d);
21382161
}
21392162
else if (bb->concrete || bb->constraintkind == 1) {
2140-
jl_value_t *ub = R ? intersect_aside(a, bb->ub, e, d) : intersect_aside(bb->ub, a, e, d);
2163+
jl_value_t *ub = R ? intersect_aside(a, bb->ub, e, 1, d) : intersect_aside(bb->ub, a, e, 0, d);
21412164
JL_GC_PUSH1(&ub);
21422165
if (ub == jl_bottom_type ||
21432166
// this fixes issue #30122. TODO: better fix for R flag.
2144-
(!R && !subtype_in_env(bb->lb, a, e))) {
2167+
(!R && !subtype_bounds_in_env(bb->lb, a, e, 0, d))) {
21452168
JL_GC_POP();
21462169
return jl_bottom_type;
21472170
}
@@ -2152,7 +2175,7 @@ static jl_value_t *intersect_var(jl_tvar_t *b, jl_value_t *a, jl_stenv_t *e, int
21522175
else if (bb->constraintkind == 2) {
21532176
// TODO: removing this case fixes many test_brokens in test/subtype.jl
21542177
// but breaks other tests.
2155-
if (!subtype_in_env(a, bb->ub, e)) {
2178+
if (!subtype_bounds_in_env(a, bb->ub, e, 1, d)) {
21562179
// mark var as unsatisfiable by making it circular
21572180
bb->lb = (jl_value_t*)b;
21582181
return jl_bottom_type;
@@ -2162,7 +2185,7 @@ static jl_value_t *intersect_var(jl_tvar_t *b, jl_value_t *a, jl_stenv_t *e, int
21622185
return a;
21632186
}
21642187
assert(bb->constraintkind == 3);
2165-
jl_value_t *ub = R ? intersect_aside(a, bb->ub, e, d) : intersect_aside(bb->ub, a, e, d);
2188+
jl_value_t *ub = R ? intersect_aside(a, bb->ub, e, 1, d) : intersect_aside(bb->ub, a, e, 0, d);
21662189
if (ub == jl_bottom_type)
21672190
return jl_bottom_type;
21682191
if (jl_is_typevar(a))
@@ -2180,7 +2203,7 @@ static jl_value_t *intersect_var(jl_tvar_t *b, jl_value_t *a, jl_stenv_t *e, int
21802203
root = NULL;
21812204
JL_GC_PUSH2(&root, &ub);
21822205
save_env(e, &root, &se);
2183-
jl_value_t *ii = R ? intersect_aside(a, bb->lb, e, d) : intersect_aside(bb->lb, a, e, d);
2206+
jl_value_t *ii = R ? intersect_aside(a, bb->lb, e, 1, d) : intersect_aside(bb->lb, a, e, 0, d);
21842207
if (ii == jl_bottom_type) {
21852208
restore_env(e, root, &se);
21862209
ii = (jl_value_t*)b;
@@ -2414,7 +2437,8 @@ static jl_value_t *intersect_unionall(jl_value_t *t, jl_unionall_t *u, jl_stenv_
24142437
{
24152438
jl_value_t *res=NULL, *res2=NULL, *save=NULL, *save2=NULL;
24162439
jl_savedenv_t se, se2;
2417-
jl_varbinding_t vb = { u->var, u->var->lb, u->var->ub, R, NULL, 0, 0, 0, 0, e->invdepth, 0, NULL, e->vars };
2440+
jl_varbinding_t vb = { u->var, u->var->lb, u->var->ub, R, NULL, 0, 0, 0, 0,
2441+
R ? e->Rinvdepth : e->invdepth, 0, NULL, e->vars };
24182442
JL_GC_PUSH6(&res, &save2, &vb.lb, &vb.ub, &save, &vb.innervars);
24192443
save_env(e, &save, &se);
24202444
res = intersect_unionall_(t, u, e, R, param, &vb);
@@ -2619,8 +2643,10 @@ static jl_value_t *intersect_invariant(jl_value_t *x, jl_value_t *y, jl_stenv_t
26192643
return (jl_subtype(x,y) && jl_subtype(y,x)) ? y : NULL;
26202644
}
26212645
e->invdepth++;
2646+
e->Rinvdepth++;
26222647
jl_value_t *ii = intersect(x, y, e, 2);
26232648
e->invdepth--;
2649+
e->Rinvdepth--;
26242650
if (jl_is_typevar(x) && jl_is_typevar(y) && (jl_is_typevar(ii) || !jl_is_type(ii)))
26252651
return ii;
26262652
if (ii == jl_bottom_type) {
@@ -2748,7 +2774,7 @@ static jl_value_t *intersect(jl_value_t *x, jl_value_t *y, jl_stenv_t *e, int pa
27482774
}
27492775
jl_value_t *ub=NULL, *lb=NULL;
27502776
JL_GC_PUSH2(&lb, &ub);
2751-
ub = intersect_aside(xub, yub, e, xx ? xx->depth0 : 0);
2777+
ub = intersect_aside(xub, yub, e, 0, xx ? xx->depth0 : 0);
27522778
lb = simple_join(xlb, ylb);
27532779
if (yy) {
27542780
if (lb != y)

test/subtype.jl

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1606,3 +1606,8 @@ end
16061606
# S = Type{T} where T<:Tuple{E, Vararg{E}} where E
16071607
# @test @elapsed (@test T != S) < 5
16081608
#end
1609+
1610+
# issue #32386
1611+
# TODO: intersect currently returns a bad answer here (it has free typevars)
1612+
@test typeintersect(Type{S} where S<:(Array{Pair{_A,N} where N, 1} where _A),
1613+
Type{Vector{T}} where T) != Union{}

0 commit comments

Comments
 (0)