Skip to content

Commit

Permalink
fix #26131, unsound updating of variable upper bounds in subtyping
Browse files Browse the repository at this point in the history
  • Loading branch information
JeffBezanson committed May 28, 2018
1 parent 746d08f commit 02d4fdd
Show file tree
Hide file tree
Showing 2 changed files with 36 additions and 4 deletions.
37 changes: 33 additions & 4 deletions src/subtype.c
Original file line number Diff line number Diff line change
Expand Up @@ -368,6 +368,37 @@ static jl_value_t *simple_join(jl_value_t *a, jl_value_t *b)
return jl_new_struct(jl_uniontype_type, a, b);
}

// compute a greatest lower bound of `a` and `b`
// in many cases, we need to over-estimate this by returning `b`.
static jl_value_t *simple_meet(jl_value_t *a, jl_value_t *b)
{
if (a == (jl_value_t*)jl_any_type || b == jl_bottom_type)
return b;
if (b == (jl_value_t*)jl_any_type || a == jl_bottom_type)
return a;
if (!(jl_is_type(a) || jl_is_typevar(a)) || !(jl_is_type(b) || jl_is_typevar(b)))
return jl_bottom_type;
if (jl_is_uniontype(a) && in_union(a, b))
return b;
if (jl_is_uniontype(b) && in_union(b, a))
return a;
if (jl_is_kind(a) && jl_is_type_type(b) && jl_typeof(jl_tparam0(b)) == a)
return b;
if (jl_is_kind(b) && jl_is_type_type(a) && jl_typeof(jl_tparam0(a)) == b)
return a;
if (jl_is_typevar(a) && obviously_egal(b, ((jl_tvar_t*)a)->ub))
return a;
if (jl_is_typevar(b) && obviously_egal(a, ((jl_tvar_t*)b)->ub))
return b;
if (obviously_disjoint(a, b, 0))
return jl_bottom_type;
if (!jl_has_free_typevars(a) && !jl_has_free_typevars(b)) {
if (jl_subtype(a, b)) return a;
if (jl_subtype(b, a)) return b;
}
return b;
}

static jl_unionall_t *rename_unionall(jl_unionall_t *u)
{
jl_tvar_t *v = jl_new_typevar(u->var->name, u->var->lb, u->var->ub);
Expand Down Expand Up @@ -462,17 +493,15 @@ static int var_lt(jl_tvar_t *b, jl_value_t *a, jl_stenv_t *e, int param)
return 1;
if (!((bb->lb == jl_bottom_type && !jl_is_type(a) && !jl_is_typevar(a)) || subtype_ccheck(bb->lb, a, e)))
return 0;
// for contravariance we would need to compute a meet here, but
// because of invariance bb.ub ⊓ a == a here always. however for this
// to work we need to compute issub(left,right) before issub(right,left),
// for this to work we need to compute issub(left,right) before issub(right,left),
// since otherwise the issub(a, bb.ub) check in var_gt becomes vacuous.
if (e->intersection) {
jl_value_t *ub = intersect_ufirst(bb->ub, a, e, bb->depth0);
if (ub != (jl_value_t*)b)
bb->ub = ub;
}
else {
bb->ub = a; // meet(bb->ub, a)
bb->ub = simple_meet(bb->ub, a);
}
assert(bb->ub != (jl_value_t*)b);
if (jl_is_typevar(a)) {
Expand Down
3 changes: 3 additions & 0 deletions test/subtype.jl
Original file line number Diff line number Diff line change
Expand Up @@ -1238,6 +1238,9 @@ struct A23764_2{T, N, S} <: AbstractArray{Union{Ref{T}, S}, N}; end
@test Tuple{A23764_2{T, 1, Nothing} where T} <: Tuple{AbstractArray{T,N}} where {T,N}
@test Tuple{A23764_2{T, 1, Nothing} where T} <: Tuple{AbstractArray{T,N} where {T,N}}

# issue #26131
@test !(Vector{Vector{Number}} <: Vector{Union{Vector{Number}, Vector{S}}} where S<:Integer)

# issue #24305
f24305(x) = [g24305(x) g24305(x) g24305(x) g24305(x); g24305(x) g24305(x) 0 0];
@test_throws UndefVarError f24305(1)
Expand Down

0 comments on commit 02d4fdd

Please sign in to comment.