Skip to content

Commit

Permalink
fix some bugs in diagonal subtyping
Browse files Browse the repository at this point in the history 
fixes #31824, fixes #24166
  • Loading branch information
@JeffBezanson
JeffBezanson committed Jun 24, 2019
1 parent f6049d6 commit 48fe2ef
Show file tree
Hide file tree
Showing 7 changed files with 182 additions and 37 deletions.
3 changes: 3 additions & 0 deletions NEWS.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,9 @@ New language features
Language changes
----------------

* Converting arbitrary tuples to `NTuple`, e.g. `convert(NTuple, (1, ""))` now gives an error,
where it used to be incorrectly allowed. This is because `NTuple` refers only to homogeneous
tuples (this meaning has not changed) ([#31833]).

Multi-threading changes
-----------------------
Expand Down
16 changes: 12 additions & 4 deletions base/essentials.jl
View file
Original file line number Diff line number Diff line change
Expand Up @@ -306,10 +306,18 @@ convert(::Type{T}, x::T) where {T<:AtLeast1} = x
convert(::Type{T}, x::AtLeast1) where {T<:AtLeast1} =
(convert(tuple_type_head(T), x[1]), convert(tuple_type_tail(T), tail(x))...)

# converting to Vararg tuple types
convert(::Type{Tuple{Vararg{V}}}, x::Tuple{Vararg{V}}) where {V} = x
convert(T::Type{Tuple{Vararg{V}}}, x::Tuple) where {V} =
(convert(tuple_type_head(T), x[1]), convert(T, tail(x))...)
# converting to other tuple types, including Vararg tuple types
_bad_tuple_conversion(T, x) = (@_noinline_meta; throw(MethodError(convert, (T, x))))
function convert(::Type{T}, x::AtLeast1) where {T<:Tuple}
if x isa T
return x
end
y = (convert(tuple_type_head(T), x[1]), convert(tuple_type_tail(T), tail(x))...)
if !(y isa T)
_bad_tuple_conversion(T, x)
end
return y
end

# used for splatting in `new`
convert_prefix(::Type{Tuple{}}, x::Tuple) = x
Expand Down
38 changes: 30 additions & 8 deletions doc/src/devdocs/types.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -403,27 +403,49 @@ f(nothing, 2.0)
These examples are telling us something: when `x` is `nothing::Nothing`, there are no
extra constraints on `y`.
It is as if the method signature had `y::Any`.
This means that whether a variable is diagonal is not a static property based on
where it appears in a type.
Rather, it depends on where a variable appears when the subtyping algorithm *uses* it.
When `x` has type `Nothing`, we don't need to use the `T` in `Union{Nothing,T}`, so `T`
does not "occur".
Indeed, we have the following type equivalence:

```julia
(Tuple{Union{Nothing,T},T} where T) == Union{Tuple{Nothing,Any}, Tuple{T,T} where T}
```

The general rule is: a concrete variable in covariant position acts like it's
not concrete if the subtyping algorithm only *uses* it once.
When `x` has type `Nothing`, we don't need to use the `T` in `Union{Nothing,T}`;
we only use it in the second slot.
This arises naturally from the observation that in `Tuple{T} where T` restricting
`T` to concrete types makes no difference; the type is equal to `Tuple{Any}` either way.

However, appearing in *invariant* position disqualifies a variable from being concrete
whether that appearance of the variable is used or not.
Otherwise types become incoherent, behaving differently depending on which other types
they are compared to. For example, consider

Tuple{Int,Int8,Vector{Integer}} <: Tuple{T,T,Vector{Union{Integer,T}}} where T

If the `T` inside the Union is ignored, then `T` is concrete and the answer is "false"
since the first two types aren't the same.
But consider instead

Tuple{Int,Int8,Vector{Any}} <: Tuple{T,T,Vector{Union{Integer,T}}} where T

Now we cannot ignore the `T` in the Union (we must have T == Any), so `T` is not
concrete and the answer is "true".
That would make the concreteness of `T` depend on the other type, which is not
acceptable since a type must have a clear meaning on its own.
Therefore the appearance of `T` inside `Vector` is considered in both cases.

## Subtyping diagonal variables

The subtyping algorithm for diagonal variables has two components:
(1) identifying variable occurrences, and (2) ensuring that diagonal
variables range over concrete types only.

The first task is accomplished by keeping counters `occurs_inv` and `occurs_cov`
The first task is accomplished by keeping the counter `occurs_cov`
(in `src/subtype.c`) for each variable in the environment, tracking the number
of invariant and covariant occurrences, respectively.
A variable is diagonal when `occurs_inv == 0 && occurs_cov > 1`.
of covariant occurrences.
A variable is diagonal when `occurs_cov > 1` and the variable does not appear
in invariant position anywhere in the type.

The second task is accomplished by imposing a condition on a variable's lower bound.
As the subtyping algorithm runs, it narrows the bounds of each variable
Expand Down
109 changes: 94 additions & 15 deletions src/subtype.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -64,6 +64,7 @@ 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
int8_t upper_bounded; // var upper bound has been constrained
// in covariant position, we need to try constraining a variable in different ways:
// 0 - unconstrained
// 1 - less than
Expand Down Expand Up @@ -145,7 +146,7 @@ static void save_env(jl_stenv_t *e, jl_value_t **root, jl_savedenv_t *se)
v = v->prev;
}
*root = (jl_value_t*)jl_alloc_svec(len*3);
se->buf = (int8_t*)(len ? malloc(len*2) : NULL);
se->buf = (int8_t*)(len ? malloc(len*3) : NULL);
#ifdef __clang_analyzer__
if (len)
memset(se->buf, 0, len*2);
Expand All @@ -157,6 +158,7 @@ static void save_env(jl_stenv_t *e, jl_value_t **root, jl_savedenv_t *se)
jl_svecset(*root, i++, (jl_value_t*)v->innervars);
se->buf[j++] = v->occurs_inv;
se->buf[j++] = v->occurs_cov;
se->buf[j++] = v->upper_bounded;
v = v->prev;
}
se->rdepth = e->Runions.depth;
Expand All @@ -176,13 +178,46 @@ static void restore_env(jl_stenv_t *e, jl_value_t *root, jl_savedenv_t *se) JL_N
assert(se->buf);
v->occurs_inv = se->buf[j++];
v->occurs_cov = se->buf[j++];
v->upper_bounded = se->buf[j++];
v = v->prev;
}
e->Runions.depth = se->rdepth;
if (e->envout && e->envidx < e->envsz)
memset(&e->envout[e->envidx], 0, (e->envsz - e->envidx)*sizeof(void*));
}

// restore just occurs_inv and occurs_cov from `se` back to `e`
static void restore_var_counts(jl_stenv_t *e, jl_savedenv_t *se) JL_NOTSAFEPOINT
{
jl_varbinding_t *v = e->vars;
int j = 0;
while (v != NULL) {
assert(se->buf);
v->occurs_inv = se->buf[j++];
v->occurs_cov = se->buf[j++];
j++;
v = v->prev;
}
}

// compute the maximum of the occurence counts in `e` and `se`, storing them in `se`
static void max_var_counts(jl_stenv_t *e, jl_savedenv_t *se) JL_NOTSAFEPOINT
{
jl_varbinding_t *v = e->vars;
int j = 0;
while (v != NULL) {
assert(se->buf);
if (v->occurs_inv > se->buf[j])
se->buf[j] = v->occurs_inv;
j++;
if (v->occurs_cov > se->buf[j])
se->buf[j] = v->occurs_cov;
j++;
j++;
v = v->prev;
}
}

// type utilities

// quickly test that two types are identical
Expand Down Expand Up @@ -535,10 +570,13 @@ static void record_var_occurrence(jl_varbinding_t *vb, jl_stenv_t *e, int param)
{
if (vb != NULL && param) {
// saturate counters at 2; we don't need values bigger than that
if (param == 2 && e->invdepth > vb->depth0 && vb->occurs_inv < 2)
vb->occurs_inv++;
else if (vb->occurs_cov < 2)
if (param == 2 && e->invdepth > vb->depth0) {
if (vb->occurs_inv < 2)
vb->occurs_inv++;
}
else if (vb->occurs_cov < 2) {
vb->occurs_cov++;
}
}
}

Expand All @@ -565,8 +603,10 @@ static int var_lt(jl_tvar_t *b, jl_value_t *a, jl_stenv_t *e, int param)
record_var_occurrence(bb, e, param);
if (!bb->right) // check ∀b . b<:a
return subtype_left_var(bb->ub, a, e);
if (bb->ub == a)
if (bb->ub == a) {
bb->upper_bounded = 1;
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 this to work we need to compute issub(left,right) before issub(right,left),
Expand All @@ -579,6 +619,7 @@ static int var_lt(jl_tvar_t *b, jl_value_t *a, jl_stenv_t *e, int param)
else {
bb->ub = simple_meet(bb->ub, a);
}
bb->upper_bounded = 1;
assert(bb->ub != (jl_value_t*)b);
if (jl_is_typevar(a)) {
jl_varbinding_t *aa = lookup(e, (jl_tvar_t*)a);
Expand Down Expand Up @@ -687,7 +728,7 @@ typedef int (*tvar_callback)(void*, int8_t, jl_stenv_t *, int);

static int with_tvar(tvar_callback callback, void *context, jl_unionall_t *u, int8_t R, jl_stenv_t *e, int param)
{
jl_varbinding_t vb = { u->var, u->var->lb, u->var->ub, R, NULL, 0, 0, 0, 0, e->invdepth, 0, NULL, e->vars };
jl_varbinding_t vb = { u->var, u->var->lb, u->var->ub, R, NULL, 0, 0, 0, 0, 0, e->invdepth, 0, NULL, e->vars };
JL_GC_PUSH4(&u, &vb.lb, &vb.ub, &vb.innervars);
e->vars = &vb;
int ans;
Expand All @@ -701,7 +742,9 @@ static int with_tvar(tvar_callback callback, void *context, jl_unionall_t *u, in
// fill variable values into `envout` up to `envsz`
if (e->envidx < e->envsz) {
jl_value_t *val;
if (!vb.occurs_inv && vb.lb != jl_bottom_type)
if (vb.lb == vb.ub && vb.upper_bounded)
val = vb.lb;
else if (!vb.occurs_inv && vb.lb != jl_bottom_type)
val = is_leaf_bound(vb.lb) ? vb.lb : (jl_value_t*)jl_new_typevar(u->var->name, jl_bottom_type, vb.lb);
else if (vb.lb == vb.ub)
val = vb.lb;
Expand Down Expand Up @@ -732,7 +775,7 @@ static int with_tvar(tvar_callback callback, void *context, jl_unionall_t *u, in
// ( Tuple{Int, Int} <: Tuple{T, T} where T) but
// !( Tuple{Int, String} <: Tuple{T, T} where T)
// Then check concreteness by checking that the lower bound is not an abstract type.
int diagonal = !vb.occurs_inv && vb.occurs_cov > 1;
int diagonal = vb.occurs_cov > 1 && (!vb.occurs_inv && !var_occurs_inside(u->body, u->var, 0, 1));
if (ans && (vb.concrete || (diagonal && is_leaf_typevar(u->var)))) {
if (vb.concrete && !diagonal && !is_leaf_bound(vb.ub)) {
// a non-diagonal var can only be a subtype of a diagonal var if its
Expand All @@ -750,7 +793,7 @@ static int with_tvar(tvar_callback callback, void *context, jl_unionall_t *u, in
else if (!is_leaf_bound(vb.lb)) {
ans = 0;
}
if (ans) {
if (ans && vb.lb != vb.ub) {
// if we occur as another var's lower bound, record the fact that we
// were concrete so that subtype can return true for that var.
/*
Expand All @@ -761,6 +804,17 @@ static int with_tvar(tvar_callback callback, void *context, jl_unionall_t *u, in
btemp = btemp->prev;
}
*/
// a diagonal var cannot be >: another diagonal var at a different invariant depth, e.g.
// Ref{Tuple{T,T} where T} !<: Ref{Tuple{T,T}} where T
jl_varbinding_t *btemp = vb.prev;
while (btemp != NULL) {
if (btemp->lb == (jl_value_t*)u->var && btemp->depth0 != vb.depth0 &&
(btemp->concrete || (btemp->occurs_cov > 1 && btemp->occurs_inv == 0))) {
ans = 0;
break;
}
btemp = btemp->prev;
}
}
}

Expand Down Expand Up @@ -1130,7 +1184,7 @@ static int subtype_tuple(jl_datatype_t *xd, jl_datatype_t *yd, jl_stenv_t *e, in
}
}

param = (param == 0 ? 1 : param);
param = 1;
env.lastx = env.lasty=NULL;
env.vtx = env.vty=NULL;
return subtype_tuple_tail(&env, 0, e, param);
Expand Down Expand Up @@ -1305,6 +1359,12 @@ static int forall_exists_equal(jl_value_t *x, jl_value_t *y, jl_stenv_t *e)
{
if (obviously_egal(x, y)) return 1;

jl_savedenv_t se; // original env
jl_savedenv_t me; // for accumulating maximum var counts
jl_value_t *saved=NULL;
save_env(e, &saved, &se);
save_env(e, &saved, &me);

jl_unionstate_t oldLunions = e->Lunions;
memset(e->Lunions.stack, 0, sizeof(e->Lunions.stack));
int sub;
Expand Down Expand Up @@ -1334,11 +1394,27 @@ static int forall_exists_equal(jl_value_t *x, jl_value_t *y, jl_stenv_t *e)
statestack_set(&e->Lunions, i, 0);
lastset = set - 1;
statestack_set(&e->Lunions, lastset, 1);
// take the maximum of var counts over all choices, to identify
// diagonal variables better.
max_var_counts(e, &me);
restore_var_counts(e, &se);
}
}

e->Lunions = oldLunions;
return sub && subtype(y, x, e, 0);
if (sub) {
// avoid double-counting variables when we check subtype in both directions.
// e.g. in `Ref{Tuple{T}}` the `T` occurs once even though we recursively
// call `subtype` on it twice.
max_var_counts(e, &me);
restore_var_counts(e, &se);
sub = subtype(y, x, e, 2);
max_var_counts(e, &me);
restore_var_counts(e, &me);
}
free(se.buf);
free(me.buf);
return sub;
}

static int exists_subtype(jl_value_t *x, jl_value_t *y, jl_stenv_t *e, jl_value_t *saved, jl_savedenv_t *se, int param)
Expand Down Expand Up @@ -2213,9 +2289,11 @@ static int var_occurs_inside(jl_value_t *v, jl_tvar_t *var, int inside, int want
}
else if (jl_is_datatype(v)) {
size_t i;
int ins = inside || !want_inv || !jl_is_tuple_type(v);
int ins = !jl_is_tuple_type(v) || !want_inv;
int va = jl_is_vararg_type(v);
for (i=0; i < jl_nparams(v); i++) {
if (var_occurs_inside(jl_tparam(v,i), var, ins, want_inv))
int ins_i = va && i == 0 ? !want_inv : ins;
if (var_occurs_inside(jl_tparam(v,i), var, ins_i, want_inv))
return 1;
}
}
Expand Down Expand Up @@ -2376,7 +2454,8 @@ static jl_value_t *intersect_unionall_(jl_value_t *t, jl_unionall_t *u, jl_stenv
else {
res = intersect(u->body, t, e, param);
}
vb->concrete |= (!vb->occurs_inv && vb->occurs_cov > 1 && is_leaf_typevar(u->var));
vb->concrete |= (vb->occurs_cov > 1 && !vb->occurs_inv && !var_occurs_inside(u->body, u->var, 0, 1) &&
is_leaf_typevar(u->var));

// handle the "diagonal dispatch" rule, which says that a type var occurring more
// than once, and only in covariant position, is constrained to concrete types. E.g.
Expand Down Expand Up @@ -2414,7 +2493,7 @@ static jl_value_t *intersect_unionall(jl_value_t *t, jl_unionall_t *u, jl_stenv_
{
jl_value_t *res=NULL, *res2=NULL, *save=NULL, *save2=NULL;
jl_savedenv_t se, se2;
jl_varbinding_t vb = { u->var, u->var->lb, u->var->ub, R, NULL, 0, 0, 0, 0, e->invdepth, 0, NULL, e->vars };
jl_varbinding_t vb = { u->var, u->var->lb, u->var->ub, R, NULL, 0, 0, 0, 0, 0, e->invdepth, 0, NULL, e->vars };
JL_GC_PUSH6(&res, &save2, &vb.lb, &vb.ub, &save, &vb.innervars);
save_env(e, &save, &se);
res = intersect_unionall_(t, u, e, R, param, &vb);
Expand Down
4 changes: 0 additions & 4 deletions test/ambiguous.jl
View file
Original file line number Diff line number Diff line change
Expand Up @@ -269,8 +269,6 @@ end
@test_broken need_to_handle_undef_sparam == Set()
pop!(need_to_handle_undef_sparam, which(Core.Compiler._cat, Tuple{Any, AbstractArray}))
pop!(need_to_handle_undef_sparam, first(methods(Core.Compiler.same_names)))
pop!(need_to_handle_undef_sparam, which(Core.Compiler.convert, Tuple{Type{Tuple{Vararg{Int}}}, Tuple{}}))
pop!(need_to_handle_undef_sparam, which(Core.Compiler.convert, Tuple{Type{Tuple{Vararg{Int}}}, Tuple{Int8}}))
@test need_to_handle_undef_sparam == Set()
end
let need_to_handle_undef_sparam =
Expand All @@ -292,8 +290,6 @@ end
pop!(need_to_handle_undef_sparam, which(Base.oneunit, Tuple{Type{Union{Missing, T}} where T}))
pop!(need_to_handle_undef_sparam, which(Base.convert, (Type{Union{Some{T}, Nothing}} where T, Some)))
pop!(need_to_handle_undef_sparam, which(Base.convert, (Type{Union{T, Nothing}} where T, Some)))
pop!(need_to_handle_undef_sparam, which(Base.convert, Tuple{Type{Tuple{Vararg{Int}}}, Tuple{}}))
pop!(need_to_handle_undef_sparam, which(Base.convert, Tuple{Type{Tuple{Vararg{Int}}}, Tuple{Int8}}))
pop!(need_to_handle_undef_sparam, which(Base.convert, Tuple{Type{Union{Nothing,T}},Union{Nothing,T}} where T))
pop!(need_to_handle_undef_sparam, which(Base.convert, Tuple{Type{Union{Missing,T}},Union{Missing,T}} where T))
pop!(need_to_handle_undef_sparam, which(Base.convert, Tuple{Type{Union{Missing,Nothing,T}},Union{Missing,Nothing,T}} where T))
Expand Down
Loading

0 comments on commit 48fe2ef

Please sign in to comment.