Skip to content

Commit

Permalink
fix some cases of diagonal subtyping when a var also appears invariantly
Browse files Browse the repository at this point in the history 
fix #26108, fix #26716
  • Loading branch information
@JeffBezanson
JeffBezanson committed Jan 6, 2020
1 parent 1878343 commit 8653d6f
Show file tree
Hide file tree
Showing 3 changed files with 100 additions and 17 deletions.
31 changes: 26 additions & 5 deletions doc/src/devdocs/types.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -403,17 +403,38 @@ 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:
Expand Down
49 changes: 40 additions & 9 deletions src/subtype.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -516,7 +516,7 @@ static int subtype_ccheck(jl_value_t *x, jl_value_t *y, jl_stenv_t *e)
return sub;
}

static int subtype_left_var(jl_value_t *x, jl_value_t *y, jl_stenv_t *e)
static int subtype_left_var(jl_value_t *x, jl_value_t *y, jl_stenv_t *e, int param)
{
if (x == y)
return 1;
Expand All @@ -528,7 +528,7 @@ static int subtype_left_var(jl_value_t *x, jl_value_t *y, jl_stenv_t *e)
return 1;
if (x == (jl_value_t*)jl_any_type && jl_is_datatype(y))
return 0;
return subtype(x, y, e, 0);
return subtype(x, y, e, param);
}

// use the current context to record where a variable occurred, for the purpose
Expand Down Expand Up @@ -566,10 +566,10 @@ static int var_lt(jl_tvar_t *b, jl_value_t *a, jl_stenv_t *e, int param)
{
jl_varbinding_t *bb = lookup(e, b);
if (bb == NULL)
return e->ignore_free || subtype_left_var(b->ub, a, e);
return e->ignore_free || subtype_left_var(b->ub, a, e, param);
record_var_occurrence(bb, e, param);
if (!bb->right) // check ∀b . b<:a
return subtype_left_var(bb->ub, a, e);
return subtype_left_var(bb->ub, a, e, param);
if (bb->ub == a)
return 1;
if (!((bb->lb == jl_bottom_type && !jl_is_type(a) && !jl_is_typevar(a)) || subtype_ccheck(bb->lb, a, e)))
Expand All @@ -590,7 +590,7 @@ static int var_lt(jl_tvar_t *b, jl_value_t *a, jl_stenv_t *e, int param)
if (aa && !aa->right && in_union(bb->lb, a) && bb->depth0 != aa->depth0 && var_outside(e, b, (jl_tvar_t*)a)) {
// an "exists" var cannot equal a "forall" var inside it unless the forall
// var has equal bounds.
return subtype_left_var(aa->ub, aa->lb, e);
return subtype_left_var(aa->ub, aa->lb, e, param);
}
}
return 1;
Expand All @@ -601,10 +601,10 @@ static int var_gt(jl_tvar_t *b, jl_value_t *a, jl_stenv_t *e, int param)
{
jl_varbinding_t *bb = lookup(e, b);
if (bb == NULL)
return e->ignore_free || subtype_left_var(a, b->lb, e);
return e->ignore_free || subtype_left_var(a, b->lb, e, param);
record_var_occurrence(bb, e, param);
if (!bb->right) // check ∀b . b>:a
return subtype_left_var(a, bb->lb, e);
return subtype_left_var(a, bb->lb, e, param);
if (bb->lb == bb->ub) {
if (jl_is_typevar(bb->lb) && !jl_is_type(a) && !jl_is_typevar(a))
return var_gt((jl_tvar_t*)bb->lb, a, e, param);
Expand All @@ -618,7 +618,7 @@ static int var_gt(jl_tvar_t *b, jl_value_t *a, jl_stenv_t *e, int param)
if (jl_is_typevar(a)) {
jl_varbinding_t *aa = lookup(e, (jl_tvar_t*)a);
if (aa && !aa->right && bb->depth0 != aa->depth0 && param == 2 && var_outside(e, b, (jl_tvar_t*)a))
return subtype_left_var(aa->ub, aa->lb, e);
return subtype_left_var(aa->ub, aa->lb, e, param);
}
return 1;
}
Expand Down Expand Up @@ -690,12 +690,42 @@ static int var_occurs_inside(jl_value_t *v, jl_tvar_t *var, int inside, int want

typedef int (*tvar_callback)(void*, int8_t, jl_stenv_t *, int);

static int var_occurs_invariant(jl_value_t *v, jl_tvar_t *var, int inv) JL_NOTSAFEPOINT
{
if (v == (jl_value_t*)var) {
return inv;
}
else if (jl_is_uniontype(v)) {
return var_occurs_invariant(((jl_uniontype_t*)v)->a, var, inv) ||
var_occurs_invariant(((jl_uniontype_t*)v)->b, var, inv);
}
else if (jl_is_unionall(v)) {
jl_unionall_t *ua = (jl_unionall_t*)v;
if (ua->var == var)
return 0;
if (var_occurs_invariant(ua->var->lb, var, inv) || var_occurs_invariant(ua->var->ub, var, inv))
return 1;
return var_occurs_invariant(ua->body, var, inv);
}
else if (jl_is_datatype(v)) {
size_t i;
int ins = !jl_is_tuple_type(v);
int va = jl_is_vararg_type(v);
for (i=0; i < jl_nparams(v); i++) {
if (var_occurs_invariant(jl_tparam(v,i), var, va && i == 0 ? 0 : ins))
return 1;
}
}
return 0;
}

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,
R ? e->Rinvdepth : e->invdepth, 0, NULL, 0, e->vars };
JL_GC_PUSH4(&u, &vb.lb, &vb.ub, &vb.innervars);
e->vars = &vb;
vb.occurs_inv = var_occurs_invariant(u->body, u->var, 0);
int ans;
if (R) {
e->envidx++;
Expand Down Expand Up @@ -2494,7 +2524,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));
int static_occurs_inv = var_occurs_invariant(u->body, u->var, 0);
vb->concrete |= (!static_occurs_inv && vb->occurs_cov > 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
37 changes: 34 additions & 3 deletions test/subtype.jl
View file
Original file line number Diff line number Diff line change
Expand Up @@ -136,6 +136,30 @@ function test_diagonal()
@test issub(Tuple{Tuple{T, T}} where T>:Int, Tuple{Tuple{T, T} where T>:Int})
@test issub(Vector{Tuple{T, T} where Number<:T<:Number},
Vector{Tuple{Number, Number}})

@test !issub(Type{Tuple{T,Any} where T}, Type{Tuple{T,T}} where T)
@test !issub(Type{Tuple{T,Any,T} where T}, Type{Tuple{T,T,T}} where T)
@test_broken issub(Type{Tuple{T} where T}, Type{Tuple{T}} where T)
@test_broken issub(Ref{Tuple{T} where T}, Ref{Tuple{T}} where T)
@test !issub(Type{Tuple{T,T} where T}, Type{Tuple{T,T}} where T)
@test !issub(Type{Tuple{T,T,T} where T}, Type{Tuple{T,T,T}} where T)
@test isequal_type(Ref{Tuple{T, T} where Int<:T<:Int},
Ref{Tuple{S, S}} where Int<:S<:Int)

let A = Tuple{Int,Int8,Vector{Integer}},
B = Tuple{T,T,Vector{T}} where T>:Integer,
C = Tuple{T,T,Vector{Union{Integer,T}}} where T
@test A <: B
@test B == C
@test A <: C
@test Tuple{Int,Int8,Vector{Any}} <: C
end

# #26108
@test !issub((Tuple{T, T, Array{T, 1}} where T), Tuple{T, T, Any} where T)

# #26716
@test !issub((Union{Tuple{Int,Bool}, Tuple{P,Bool}} where P), Tuple{Union{T,Int}, T} where T)
end

# level 3: UnionAll
Expand Down Expand Up @@ -1475,12 +1499,19 @@ let U = Tuple{Union{LT, LT1},Union{R, R1},Int} where LT1<:R1 where R1<:Tuple{Int
end

# issue #31082 and #30741
@testintersect(Tuple{T, Ref{T}, T} where T,
Tuple{Ref{S}, S, S} where S,
Union{})
@test typeintersect(Tuple{T, Ref{T}, T} where T,
Tuple{Ref{S}, S, S} where S) != Union{}
@testintersect(Tuple{Pair{B,C},Union{C,Pair{B,C}},Union{B,Real}} where {B,C},
Tuple{Pair{B,C},C,C} where {B,C},
Tuple{Pair{B,C},C,C} where C<:Union{Real, B} where B)
f31082(::Pair{B, C}, ::Union{C, Pair{B, C}}, ::Union{B, Real}) where {B, C} = 0
f31082(::Pair{B, C}, ::C, ::C) where {B, C} = 1
@test f31082(""=>1, 2, 3) == 1
@test f31082(""=>1, 2, "") == 0
@test f31082(""=>1, 2, 3.0) == 0
@test f31082(Pair{Any,Any}(1,2), 1, 2) == 1
@test f31082(Pair{Any,Any}(1,2), Pair{Any,Any}(1,2), 2) == 1
@test f31082(Pair{Any,Any}(1,2), 1=>2, 2.0) == 1

# issue #31115
@testintersect(Tuple{Ref{Z} where Z<:(Ref{Y} where Y<:Tuple{<:B}), Int} where B,
Expand Down

0 comments on commit 8653d6f

Please sign in to comment.