From 49623bd294a505b2cafc4e1eedd4a51e2bda3efc Mon Sep 17 00:00:00 2001 From: Jeff Bezanson Date: Sun, 5 Jan 2020 19:34:39 -0500 Subject: [PATCH] fix some cases of diagonal subtyping when a var also appears invariantly fix #26108, fix #26716 --- doc/src/devdocs/types.md | 31 ++++++++++++++--- src/subtype.c | 72 +++++++++++++++++++++++----------------- test/subtype.jl | 37 +++++++++++++++++++-- 3 files changed, 102 insertions(+), 38 deletions(-) diff --git a/doc/src/devdocs/types.md b/doc/src/devdocs/types.md index d18ddad7e7f00..1d3be57230606 100644 --- a/doc/src/devdocs/types.md +++ b/doc/src/devdocs/types.md @@ -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: diff --git a/src/subtype.c b/src/subtype.c index f251f7839f309..b1c49820d9f3e 100644 --- a/src/subtype.c +++ b/src/subtype.c @@ -57,10 +57,6 @@ typedef struct jl_varbinding_t { jl_value_t *lb; jl_value_t *ub; int8_t right; // whether this variable came from the right side of `A <: B` - // if another var that this one depends on is found to be concrete, store it - // here for reference in case that var is popped from the environment before this one. - // TODO: generalize this to multiple variables - jl_tvar_t *concretevar; 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 @@ -516,7 +512,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; @@ -528,7 +524,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 @@ -566,10 +562,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))) @@ -590,7 +586,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; @@ -601,10 +597,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); @@ -618,7 +614,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; } @@ -690,9 +686,38 @@ 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, + jl_varbinding_t vb = { u->var, u->var->lb, u->var->ub, R, 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; @@ -738,7 +763,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 && !var_occurs_invariant(u->body, u->var, 0); 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 @@ -750,24 +775,10 @@ static int with_tvar(tvar_callback callback, void *context, jl_unionall_t *u, in jl_varbinding_t *vlb = lookup(e, v); if (vlb) vlb->concrete = 1; - //else // TODO handle multiple variables in vb.concretevar - // ans = (v == vb.concretevar); } else if (!is_leaf_bound(vb.lb)) { ans = 0; } - if (ans) { - // 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. - /* - btemp = vb.prev; - while (btemp != NULL) { - if (btemp->lb == (jl_value_t*)u->var) - btemp->concretevar = u->var; - btemp = btemp->prev; - } - */ - } } e->vars = vb.prev; @@ -2494,7 +2505,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 && is_leaf_typevar(u->var) && + !var_occurs_invariant(u->body, u->var, 0)); // 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. @@ -2532,7 +2544,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, + jl_varbinding_t vb = { u->var, u->var->lb, u->var->ub, R, 0, 0, 0, 0, R ? e->Rinvdepth : e->invdepth, 0, NULL, 0, e->vars }; JL_GC_PUSH6(&res, &save2, &vb.lb, &vb.ub, &save, &vb.innervars); save_env(e, &save, &se); diff --git a/test/subtype.jl b/test/subtype.jl index 093d1ad096299..1829a96e9a01f 100644 --- a/test/subtype.jl +++ b/test/subtype.jl @@ -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 @@ -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,