Skip to content

Commit

Permalink
simplify and improve type intersection algorithm a bit
Browse files Browse the repository at this point in the history 
This removes some code and makes a class of results more conservative,
fixing some potential cases of unsoundness.
  • Loading branch information
@JeffBezanson
JeffBezanson committed Aug 16, 2021
1 parent f9338aa commit b06f813
Show file tree
Hide file tree
Showing 3 changed files with 78 additions and 92 deletions.
6 changes: 5 additions & 1 deletion base/compiler/utilities.jl
View file
Original file line number Diff line number Diff line change
Expand Up @@ -156,7 +156,11 @@ function subst_trivial_bounds(@nospecialize(atypes))
end
v = atypes.var
if isconcretetype(v.ub) || v.lb === v.ub
return subst_trivial_bounds(atypes{v.ub})
try
return subst_trivial_bounds(atypes{v.ub})
catch
# Note in rare cases a var bound might not be valid to substitute.
end
end
return UnionAll(v, subst_trivial_bounds(atypes.body))
end
Expand Down
111 changes: 34 additions & 77 deletions src/subtype.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -60,13 +60,11 @@ typedef struct jl_varbinding_t {
int8_t occurs_inv; // occurs in invariant position
int8_t occurs_cov; // # of occurrences in covariant position
int8_t concrete; // 1 if another variable has a constraint forcing this one to be concrete
// in covariant position, we need to try constraining a variable in different ways:
// 0 - unconstrained
// 1 - less than
// 2 - greater than
// 3 - inexpressible - occurs when the var has non-trivial overlap with another type,
// and we would need to return `intersect(var,other)`. in this case
// we choose to over-estimate the intersection by returning the var.
// constraintkind: in covariant position, we try three different ways to compute var ∩ type:
// let ub = var.ub ∩ type
// 0 - var.ub <: type ? var : ub
// 1 - var.ub = ub; return var
// 2 - either (var.ub = ub; return var), or return ub
int8_t constraintkind;
int depth0; // # of invariant constructors nested around the UnionAll type for this var
// when this variable's integer value is compared to that of another,
Expand Down Expand Up @@ -2285,67 +2283,31 @@ static jl_value_t *intersect_var(jl_tvar_t *b, jl_value_t *a, jl_stenv_t *e, int
JL_GC_POP();
return ub;
}
else if (bb->constraintkind == 0) {
if (!jl_is_typevar(bb->ub) && !jl_is_typevar(a)) {
if (try_subtype_in_env(bb->ub, a, e, 0, d))
return (jl_value_t*)b;
}
return R ? intersect_aside(a, bb->ub, e, 1, d) : intersect_aside(bb->ub, a, e, 0, d);
}
else if (bb->concrete || bb->constraintkind == 1) {
jl_value_t *ub = R ? intersect_aside(a, bb->ub, e, 1, d) : intersect_aside(bb->ub, a, e, 0, d);
if (ub == jl_bottom_type)
return jl_bottom_type;
JL_GC_PUSH1(&ub);
if (!R && !subtype_bounds_in_env(bb->lb, a, e, 0, d)) {
// this fixes issue #30122. TODO: better fix for R flag.
JL_GC_POP();
return jl_bottom_type;
}
JL_GC_POP();
set_bound(&bb->ub, ub, b, e);
return (jl_value_t*)b;
}
else if (bb->constraintkind == 2) {
// TODO: removing this case fixes many test_brokens in test/subtype.jl
// but breaks other tests.
if (!subtype_bounds_in_env(a, bb->ub, e, 1, d)) {
// mark var as unsatisfiable by making it circular
bb->lb = (jl_value_t*)b;
return jl_bottom_type;
}
jl_value_t *lb = simple_join(bb->lb, a);
set_bound(&bb->lb, lb, b, e);
return a;
}
assert(bb->constraintkind == 3);
jl_value_t *ub = R ? intersect_aside(a, bb->ub, e, 1, d) : intersect_aside(bb->ub, a, e, 0, d);
if (ub == jl_bottom_type)
return jl_bottom_type;
if (jl_is_typevar(a))
return (jl_value_t*)b;
if (ub == a) {
if (bb->lb == jl_bottom_type) {
set_bound(&bb->ub, a, b, e);
if (bb->constraintkind == 0) {
JL_GC_PUSH1(&ub);
if (!jl_is_typevar(a) && try_subtype_in_env(bb->ub, a, e, 0, d)) {
JL_GC_POP();
return (jl_value_t*)b;
}
JL_GC_POP();
return ub;
}
else if (bb->ub == bb->lb) {
return ub;
else if (bb->constraintkind == 1) {
set_bound(&bb->ub, ub, b, e);
return (jl_value_t*)b;
}
root = NULL;
JL_GC_PUSH2(&root, &ub);
save_env(e, &root, &se);
jl_value_t *ii = R ? intersect_aside(a, bb->lb, e, 1, d) : intersect_aside(bb->lb, a, e, 0, d);
if (ii == jl_bottom_type) {
restore_env(e, root, &se);
ii = (jl_value_t*)b;
assert(bb->constraintkind == 2);
if (!jl_is_typevar(a)) {
if (ub == a && bb->lb != jl_bottom_type)
return ub;
else if (jl_egal(bb->ub, bb->lb))
return ub;
set_bound(&bb->ub, ub, b, e);
}
free_env(&se);
JL_GC_POP();
return ii;
return (jl_value_t*)b;
}

// test whether `var` occurs inside constructors. `want_inv` tests only inside
Expand Down Expand Up @@ -2389,7 +2351,7 @@ static int var_occurs_inside(jl_value_t *v, jl_tvar_t *var, int inside, int want
}

// Caller might not have rooted `res`
static jl_value_t *finish_unionall(jl_value_t *res JL_MAYBE_UNROOTED, jl_varbinding_t *vb, jl_stenv_t *e)
static jl_value_t *finish_unionall(jl_value_t *res JL_MAYBE_UNROOTED, jl_varbinding_t *vb, jl_unionall_t *u, jl_stenv_t *e)
{
jl_value_t *varval = NULL;
jl_tvar_t *newvar = vb->var;
Expand All @@ -2402,7 +2364,10 @@ static jl_value_t *finish_unionall(jl_value_t *res JL_MAYBE_UNROOTED, jl_varbind
// given x<:T<:x, substitute x for T
varval = vb->ub;
}
else if (!vb->occurs_inv && is_leaf_bound(vb->ub)) {
// TODO: `vb.occurs_cov == 1` here allows substituting Tuple{<:X} => Tuple{X},
// which is valid but changes some ambiguity errors so we don't need to do it yet.
else if ((/*vb->occurs_cov == 1 || */is_leaf_bound(vb->ub)) &&
!var_occurs_invariant(u->body, u->var, 0)) {
// replace T<:x with x in covariant position when possible
varval = vb->ub;
}
Expand All @@ -2422,7 +2387,7 @@ static jl_value_t *finish_unionall(jl_value_t *res JL_MAYBE_UNROOTED, jl_varbind

// prefer generating a fresh typevar, to avoid repeated renaming if the result
// is compared to one of the intersected types later.
if (!varval)
if (!varval && (vb->lb != vb->var->lb || vb->ub != vb->var->ub))
newvar = jl_new_typevar(vb->var->name, vb->lb, vb->ub);

// remove/replace/rewrap free occurrences of this var in the environment
Expand Down Expand Up @@ -2540,7 +2505,7 @@ static jl_value_t *intersect_unionall_(jl_value_t *t, jl_unionall_t *u, jl_stenv
int envsize = 0;
while (btemp != NULL) {
envsize++;
if (envsize > 150)
if (envsize > 70)
return t;
if (btemp->var == u->var || btemp->lb == (jl_value_t*)u->var ||
btemp->ub == (jl_value_t*)u->var) {
Expand Down Expand Up @@ -2591,7 +2556,7 @@ static jl_value_t *intersect_unionall_(jl_value_t *t, jl_unionall_t *u, jl_stenv
}
if (res != jl_bottom_type)
// res is rooted by callee
res = finish_unionall(res, vb, e);
res = finish_unionall(res, vb, u, e);
JL_GC_POP();
return res;
}
Expand All @@ -2609,7 +2574,7 @@ static jl_value_t *intersect_unionall(jl_value_t *t, jl_unionall_t *u, jl_stenv_
if (vb.concrete || vb.occurs_inv>1 || u->var->lb != jl_bottom_type || (vb.occurs_inv && vb.occurs_cov)) {
restore_env(e, NULL, &se);
vb.occurs_cov = vb.occurs_inv = 0;
vb.constraintkind = 3;
vb.constraintkind = vb.concrete ? 1 : 2;
res = intersect_unionall_(t, u, e, R, param, &vb);
}
else if (vb.occurs_cov) {
Expand All @@ -2619,17 +2584,10 @@ static jl_value_t *intersect_unionall(jl_value_t *t, jl_unionall_t *u, jl_stenv_
vb.lb = u->var->lb; vb.ub = u->var->ub;
vb.constraintkind = 1;
res2 = intersect_unionall_(t, u, e, R, param, &vb);
if (res2 == jl_bottom_type) {
restore_env(e, save, &se);
vb.occurs_cov = vb.occurs_inv = 0;
vb.lb = u->var->lb; vb.ub = u->var->ub;
vb.constraintkind = 2;
res2 = intersect_unionall_(t, u, e, R, param, &vb);
if (res2 == jl_bottom_type)
restore_env(e, save2, &se2);
}
if (res2 != jl_bottom_type)
res = res2;
else
restore_env(e, save2, &se2);
free_env(&se2);
}
}
Expand Down Expand Up @@ -3016,14 +2974,13 @@ static jl_value_t *intersect(jl_value_t *x, jl_value_t *y, jl_stenv_t *e, int pa
jl_value_t *ub=NULL, *lb=NULL;
JL_GC_PUSH2(&lb, &ub);
ub = intersect_aside(xub, yub, e, 0, xx ? xx->depth0 : 0);
if (xlb == y)
if (reachable_var(xlb, (jl_tvar_t*)y, e))
lb = ylb;
else
lb = simple_join(xlb, ylb);
if (yy) {
if (!subtype_by_bounds(lb, y, e))
yy->lb = lb;
if (!subtype_by_bounds(y, ub, e))
yy->lb = lb;
if (!reachable_var(ub, (jl_tvar_t*)y, e))
yy->ub = ub;
assert(yy->ub != y);
assert(yy->lb != y);
Expand Down
53 changes: 39 additions & 14 deletions test/subtype.jl
View file
Original file line number Diff line number Diff line change
Expand Up @@ -587,7 +587,7 @@ function test_old()
@test !(Type{Tuple{Nothing}} <: Tuple{Type{Nothing}})
end

const menagerie =
const easy_menagerie =
Any[Bottom, Any, Int, Int8, Integer, Real,
Array{Int,1}, AbstractArray{Int,1},
Tuple{Int,Vararg{Integer}}, Tuple{Integer,Vararg{Int}}, Tuple{},
Expand All @@ -607,22 +607,29 @@ const menagerie =
Array{(@UnionAll T<:Int T), 1},
(@UnionAll T<:Real @UnionAll S<:AbstractArray{T,1} Tuple{T,S}),
Union{Int,Ref{Union{Int,Int8}}},
(@UnionAll T Union{Tuple{T,Array{T,1}}, Tuple{T,Array{Int,1}}}),
]

let new = Any[]
# add variants of each type
for T in menagerie
const hard_menagerie =
Any[(@UnionAll T Union{Tuple{T,Array{T,1}}, Tuple{T,Array{Int,1}}})]

function add_variants!(types)
new = Any[]
for T in types
push!(new, Ref{T})
push!(new, Tuple{T})
push!(new, Tuple{T,T})
push!(new, Tuple{Vararg{T}})
push!(new, @UnionAll S<:T S)
push!(new, @UnionAll S<:T Ref{S})
end
append!(menagerie, new)
append!(types, new)
end

add_variants!(easy_menagerie)
add_variants!(hard_menagerie)

const menagerie = [easy_menagerie; hard_menagerie]

function test_properties()
x→y = !x || y
¬T = @UnionAll X>:T Ref{X}
Expand Down Expand Up @@ -1057,14 +1064,15 @@ function test_intersection()
end

function test_intersection_properties()
approx = Tuple{Vector{Vector{T}} where T, Vector{Vector{T}} where T}
for T in menagerie
for S in menagerie
for i in eachindex(menagerie)
T = menagerie[i]
for j in eachindex(menagerie)
S = menagerie[j]
I = _type_intersect(T,S)
I2 = _type_intersect(S,T)
@test isequal_type(I, I2)
if I == approx
# TODO: some of these cases give a conservative answer
if i > length(easy_menagerie) || j > length(easy_menagerie)
# TODO: these cases give a conservative answer
@test issub(I, T) || issub(I, S)
else
@test issub(I, T) && issub(I, S)
Expand Down Expand Up @@ -1796,7 +1804,7 @@ let X1 = Tuple{AlmostLU, Vector{T}} where T,
# TODO: the quality of this intersection is not great; for now just test that it
# doesn't stack overflow
@test I<:X1 || I<:X2
actual = Tuple{AlmostLU{S, X} where X<:Matrix{S}, Vector{S}} where S<:Union{Float32, Float64}
actual = Tuple{Union{AlmostLU{S, X} where X<:Matrix{S}, AlmostLU{S, <:Matrix}}, Vector{S}} where S<:Union{Float32, Float64}
@test I == actual
end

Expand Down Expand Up @@ -1898,8 +1906,8 @@ end
# issue #39948
let A = Tuple{Array{Pair{T, JT} where JT<:Ref{T}, 1} where T, Vector},
I = typeintersect(A, Tuple{Vararg{Vector{T}}} where T)
@test_broken I <: A
@test_broken !Base.has_free_typevars(I)
@test I <: A
@test !Base.has_free_typevars(I)
end

# issue #8915
Expand Down Expand Up @@ -1927,3 +1935,20 @@ let A = Tuple{Ref{T}, Vararg{T}} where T,
J = typeintersect(A, C)
@test_broken J != Union{}
end

let A = Tuple{Dict{I,T}, I, T} where T where I,
B = Tuple{AbstractDict{I,T}, T, I} where T where I
# TODO: we should probably have I == T here
@test typeintersect(A, B) == Tuple{Dict{I,T}, I, T} where {I, T}
end

let A = Tuple{UnionAll, Vector{Any}},
B = Tuple{Type{T}, T} where T<:AbstractArray,
I = typeintersect(A, B)
@test !isconcretetype(I)
@test_broken I == Tuple{Type{T}, Vector{Any}} where T<:AbstractArray
end

@testintersect(Tuple{Type{Vector{<:T}}, T} where {T<:Integer},
Tuple{Type{T}, AbstractArray} where T<:Array,
Bottom)

0 comments on commit b06f813

Please sign in to comment.