Skip to content

Commit

Permalink
Some small patch for typeintersect. (#48224)
Browse files Browse the repository at this point in the history
* Add missing var-substitution in omit_bad_union.

follow up 3037342

* Also check free typevar's bounds in `reachable_var`

They might be recreated in `finish_unionall`, (thus `lookup` returns false.)
But their bounds might still live in the current env.

close #44395.
(#44395 could also be fixed by the fast path added in #48221.
This commit would skip more `intersect_var` under circular constraint.)

* Disallow more circulation once we set `lb`==`ub`.

close #26487.
This should be valid as we never set `X<:Y<:X` (assuming `Y` is the outer var).
  • Loading branch information
N5N3 committed Jan 12, 2023
1 parent 793eaa3 commit 3933f90
Show file tree
Hide file tree
Showing 2 changed files with 36 additions and 37 deletions.
54 changes: 26 additions & 28 deletions src/subtype.c
Original file line number Diff line number Diff line change
Expand Up @@ -2406,43 +2406,31 @@ static int subtype_in_env_existential(jl_value_t *x, jl_value_t *y, jl_stenv_t *
}

// See if var y is reachable from x via bounds; used to avoid cycles.
static int _reachable_var(jl_value_t *x, jl_tvar_t *y, jl_stenv_t *e)
static int _reachable_var(jl_value_t *x, jl_tvar_t *y, jl_stenv_t *e, jl_typeenv_t *log)
{
if (in_union(x, (jl_value_t*)y))
return 1;
if (jl_is_uniontype(x))
return _reachable_var(((jl_uniontype_t *)x)->a, y, e) ||
_reachable_var(((jl_uniontype_t *)x)->b, y, e);
return _reachable_var(((jl_uniontype_t *)x)->a, y, e, log) ||
_reachable_var(((jl_uniontype_t *)x)->b, y, e, log);
if (!jl_is_typevar(x))
return 0;
jl_typeenv_t *t = log;
while (t != NULL) {
if (x == (jl_value_t *)t->var)
return 0;
t = t->prev;
}
jl_varbinding_t *xv = lookup(e, (jl_tvar_t*)x);
if (xv == NULL || xv->right)
return 0;
xv->right = 1;
return _reachable_var(xv->ub, y, e) || _reachable_var(xv->lb, y, e);
jl_value_t *lb = xv == NULL ? ((jl_tvar_t*)x)->lb : xv->lb;
jl_value_t *ub = xv == NULL ? ((jl_tvar_t*)x)->ub : xv->ub;
jl_typeenv_t newlog = { (jl_tvar_t*)x, NULL, log };
return _reachable_var(ub, y, e, &newlog) || _reachable_var(lb, y, e, &newlog);
}

static int reachable_var(jl_value_t *x, jl_tvar_t *y, jl_stenv_t *e)
{
int len = current_env_length(e);
int8_t *rs = (int8_t*)malloc_s(len);
int n = 0;
jl_varbinding_t *v = e->vars;
while (n < len) {
assert(v != NULL);
rs[n++] = v->right;
v->right = 0;
v = v->prev;
}
int res = _reachable_var(x, y, e);
n = 0; v = e->vars;
while (n < len) {
assert(v != NULL);
v->right = rs[n++];
v = v->prev;
}
free(rs);
return res;
return _reachable_var(x, y, e, NULL);
}

// check whether setting v == t implies v == SomeType{v}, which is unsatisfiable.
Expand Down Expand Up @@ -2630,8 +2618,10 @@ static jl_value_t *omit_bad_union(jl_value_t *u, jl_tvar_t *t)
ub = omit_bad_union(ub, t);
body = omit_bad_union(body, t);
if (ub != NULL && body != NULL && !jl_has_typevar(var->lb, t)) {
if (ub != var->ub)
if (ub != var->ub) {
var = jl_new_typevar(var->name, var->lb, ub);
body = jl_substitute_var(body, ((jl_unionall_t *)u)->var, (jl_value_t *)var);
}
res = jl_new_struct(jl_unionall_type, var, body);
}
JL_GC_POP();
Expand Down Expand Up @@ -3259,7 +3249,15 @@ static jl_value_t *intersect(jl_value_t *x, jl_value_t *y, jl_stenv_t *e, int pa
return jl_bottom_type;
}
int ccheck;
if (yub == xub ||
if (xlb == xub && ylb == yub &&
jl_has_typevar(xlb, (jl_tvar_t *)y) &&
jl_has_typevar(ylb, (jl_tvar_t *)x)) {
// specical case for e.g.
// 1) Val{Y}<:X<:Val{Y} && Val{X}<:Y<:Val{X}
// 2) Y<:X<:Y && Val{X}<:Y<:Val{X} => Val{Y}<:Y<:Val{Y}
ccheck = 0;
}
else if (yub == xub ||
(subtype_by_bounds(xlb, yub, e) && subtype_by_bounds(ylb, xub, e))) {
ccheck = 1;
}
Expand Down
19 changes: 10 additions & 9 deletions test/subtype.jl
Original file line number Diff line number Diff line change
Expand Up @@ -2352,6 +2352,16 @@ let S = Tuple{Type{T1}, T1, Val{T1}} where T1<:(Val{S1} where S1<:Val),
@test_broken I2 <: T
end

#issue 44395
@testintersect(Tuple{Type{T}, T} where {T <: Vector{Union{T, R}} where {R<:Real, T<:Real}},
Tuple{Type{Vector{Union{T, R}}}, Matrix{Union{T, R}}} where {R<:Real, T<:Real},
Union{})

#issue 26487
@testintersect(Tuple{Type{Tuple{T,Val{T}}}, Val{T}} where T,
Tuple{Type{Tuple{Val{T},T}}, Val{T}} where T,
Union{})

@testset "known subtype/intersect issue" begin
#issue 45874
# Causes a hang due to jl_critical_error calling back into malloc...
Expand All @@ -2361,12 +2371,6 @@ end
# @test_broken typeintersect(S,T) === S
# end

#issue 44395
@test_broken typeintersect(
Tuple{Type{T}, T} where {T <: Vector{Union{T, R}} where {R<:Real, T<:Real}},
Tuple{Type{Vector{Union{T, R}}}, Matrix{Union{T, R}}} where {R<:Real, T<:Real},
) === Union{}

#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{}
Expand All @@ -2385,9 +2389,6 @@ end
#issue 33137
@test_broken (Tuple{Q,Int} where Q<:Int) <: Tuple{T,T} where T

#issue 26487
@test_broken typeintersect(Tuple{Type{Tuple{T,Val{T}}}, Val{T}} where T, Tuple{Type{Tuple{Val{T},T}}, Val{T}} where T) <: Any

# issue 24333
@test_broken (Type{Union{Ref,Cvoid}} <: Type{Union{T,Cvoid}} where T)

Expand Down

0 comments on commit 3933f90

Please sign in to comment.