Wrongly empty typeintersect if a TypeVar needs to fixed to a non-type

[martinholters]

julia> foo{N}(::Val{N}, ::Type{Val{N}}) = true
foo (generic function with 1 method)

julia> methods(foo, (Val{0}, Type{Val{N}} where N))
# 0 methods for generic function "foo":

but for N==0, the one method we have actually does match. This can lead inference astray:

julia> foo{N1,N2}(::Val{N1}, ::Type{Val{N2}}) = "mismatch"
foo (generic function with 2 methods)

julia> bar(n) = foo(Val{0}(), Val{n})
bar (generic function with 1 method)

julia> bar(0)
true

julia> Base.return_types(bar, (Int,))
1-element Array{Any,1}:
 String

That should of course be Union{Bool, String}, but inference only sees the second method of foo.

This affects e.g. ntuple and rdims:

julia> Base.return_types(ntuple, (typeof(identity), Type{Val{N}} where N))
1-element Array{Any,1}:
 Tuple{Int64,Int64,Int64,Int64,Int64,Int64,Int64,Int64,Int64,Int64,Int64,Int64,Int64,Int64,Vararg{Any,N}} where N

[martinholters]

Type intersection gets it wrong here:

julia> typeintersect(Tuple{Base.Val{0}, Type{Base.Val{N}} where N}, Tuple{Base.Val{N}, Type{Base.Val{N}}} where N)
Union{}

while of course

julia> Tuple{Base.Val{0}, Type{Base.Val{0}}} <: Tuple{Base.Val{0}, Type{Base.Val{N}} where N}
true

julia> Tuple{Base.Val{0}, Type{Base.Val{0}}} <: Tuple{Base.Val{N}, Type{Base.Val{N}}} where N
true

[martinholters]

Actually, it seems it has nothing to do with Type:

julia> typeintersect(Tuple{Array{Int,0}, Array{Array{Int,N}} where N}, Tuple{Array{Int,N}, Array{Array{Int,N}}} where N)
Union{}

julia> typeintersect(Tuple{Array{Int,0}, Array{Array{T,0}} where T}, Tuple{Array{T,0}, Array{Array{T,0}}} where T)
Tuple{Array{Int64,0},Array{Array{Int64,0},N} where N}

It seems sufficient that the TypeVar needs to be fixed to a non-type and one of the tuple elements has two layers of nesting. Quite obvious here:

julia> typeintersect(Tuple{Val{0}, Val{Val{N}}} where N, Tuple{Val{N}, Val{Val{N}}} where N)
Union{} # should be Tuple{Val{0},Val{Val{0}}}

julia> typeintersect(Tuple{Val{Int}, Val{Val{N}}} where N, Tuple{Val{N}, Val{Val{N}}} where N)
Tuple{Val{Int64},Val{Val{Int64}}} # ok

julia> typeintersect(Tuple{Val{0}, Val{N}} where N, Tuple{Val{N}, Val{N}} where N)
Tuple{Val{0},Val{0}} # ok

[martinholters]

After some time with gdb, I think I have an idea of what is going wrong. When calling typeintersect(Tuple{Val{0}, Val{Val{N1}}} where N1, Tuple{Val{N2}, Val{Val{N2}}} where N2), intersecting the second tuple members eventually brings me to this backtrace:

#0  var_gt (b=N2, a=N1, e=0x7ffe26a75da0, param=2)
    at julia/src/subtype.c:391
#1  0x00007fda6fef451f in subtype (x=N1, y=N2, 
    e=0x7ffe26a75da0, param=2) at julia/src/subtype.c:727
#2  0x00007fda6fef4da4 in forall_exists_equal (x=N1, 
    y=N2, e=0x7ffe26a75da0)
    at julia/src/subtype.c:830
#3  0x00007fda6fef4c3a in subtype (x=Val{N1}, y=Val{N2}, 
    e=0x7ffe26a75da0, param=0) at julia/src/subtype.c:809
#4  0x00007fda6fef4f1d in exists_subtype (x=Val{N1}, y=Val{N2}, 
    e=0x7ffe26a75da0, saved=0x7fd86d314a00, se=0x7ffe26a75d30)
    at julia/src/subtype.c:852
#5  0x00007fda6fef50c7 in forall_exists_subtype (x=Val{N1}, 
    y=Val{N2}, e=0x7ffe26a75da0)
    at julia/src/subtype.c:880
#6  0x00007fda6fef5479 in subtype_in_env (x=Val{N1}, y=Val{N2}, 
    e=0x7ffe26a76990) at julia/src/subtype.c:946
#7  0x00007fda6fef8967 in intersect_invariant (x=Val{N1}, 
    y=Val{N2}, e=0x7ffe26a76990)
    at julia/src/subtype.c:1580
#8  0x00007fda6fef9f8c in intersect (x=Val{Val{N1}}, y=Val{Val{N1}}, 
    e=0x7ffe26a76990, param=1) at julia/src/subtype.c:1806

At this point, upper and lower bounds on N1 and N2 have all been correctly deduced as 0. But then, var_gt replaces the lower bound of N2 with simple_join(0, N1), which gives Any. And with Any as a lower bound, the intersection fails, of course. Unfortunately, I'm at a loss as to where things should take another turn. Should var_gt be even called in this case?

[martinholters]

This seems to fix it:

--- a/src/subtype.c
+++ b/src/subtype.c
@@ -701,6 +701,8 @@ static int subtype(jl_value_t *x, jl_value_t *y, jl_stenv_t *e, int param)
             if (x == y) return 1;
             jl_varbinding_t *xx = lookup(e, (jl_tvar_t*)x);
             jl_varbinding_t *yy = lookup(e, (jl_tvar_t*)y);
+            if (xx && yy && xx->ub == xx->lb && xx->lb == yy->ub && yy->ub == yy->lb)
+                return 1;
             jl_value_t *xub = xx ? xx->ub : ((jl_tvar_t*)x)->ub;
             jl_value_t *ylb = yy ? yy->lb : ((jl_tvar_t*)y)->lb;
             if (e->intersection) {

Bullshit or PR-worthy?

[JeffBezanson]

Thanks for digging into this. It's great to have more people familiar with the subtyping code. That change looks safe to me; if it passes tests you should PR it.

[martinholters]

While safe, that fix also seems to be overly specific, as some very similar cases still fail:

julia> typeintersect(Tuple{Val{0}, Val{Val{N}}} where N, Tuple{Val{N}, Val{Val{N}}} where N)
Tuple{Val{0},Val{Val{0}}} # fixed by patch above

julia> typeintersect(Tuple{Val{N}, Val{Val{N}}} where N, Tuple{Val{0}, Val{Val{N}}} where N)
Tuple{Val{0},Val{Val{0}}} # fixed by patch above

julia> typeintersect(Tuple{Val{N}, Val{Val{0}}} where N, Tuple{Val{N}, Val{Val{N}}} where N)
Union{}

julia> typeintersect(Tuple{Val{N}, Val{Val{N}}} where N, Tuple{Val{N}, Val{Val{0}}} where N)
Tuple{Val{0},Val{Val{0}}} # already works on master

julia> typeintersect(Tuple{Val{Val{0}}, Val{N}} where N, Tuple{Val{Val{N}}, Val{N}} where N)
Tuple{Val{Val{0}},Val{0}} # already works on master

julia> typeintersect(Tuple{Val{Val{N}}, Val{N}} where N, Tuple{Val{Val{0}}, Val{N}} where N)
Tuple{Val{Val{0}},Val{0}} # already works on master

julia> typeintersect(Tuple{Val{Val{N}}, Val{0}} where N, Tuple{Val{Val{N}}, Val{N}} where N)
Union{}

julia> typeintersect(Tuple{Val{Val{N}}, Val{N}} where N, Tuple{Val{Val{N}}, Val{0}} where N)
Tuple{Val{Val{0}},Val{0}} # fixed by patch above

I'll try digging a little deeper and will open a PR if I get the two remaining cases to work, too.

[martinholters]

Fixed by #21010.