subtype <: wrong inside function in some cases

[mauro3]

Julia 0.4 gets subtype relation wrong inside a function scope with tuple types:

immutable FakeMethod
    sig::Type{Tuple}  # no error below if leaving the type declaration off!
end

fmm = methods(sin, (Complex{Float16},))[1]
_sin(::String) = Float64()
tmm = methods(_sin, (String,))[1]
@assert !( tmm.sig<:fmm.sig)

tm = FakeMethod(tmm.sig)
fm = FakeMethod(fmm.sig)
# In global scope all works:
@show tmm.sig, fmm.sig
@show tm.sig, fm.sig
@show tm.sig<:fm.sig # true
@show fm.sig<:tm.sig # true
@show fm.sig==tm.sig  # false
@show fm.sig===tm.sig # false
@assert !( tm.sig<:fm.sig )

function f(tmm, fmm)
    println("\nInside function:")
    tm = FakeMethod(tmm.sig)
    fm = FakeMethod(fmm.sig)

    @show tmm.sig, fmm.sig
    @show tm.sig, fm.sig
    @show tm.sig<:fm.sig # true!!!!!!!!!
    @show fm.sig<:tm.sig # true!!!!!!!!!
    @show fm.sig==tm.sig  # false (true before #10380)
    @show fm.sig===tm.sig # false
    @assert !( tm.sig<:fm.sig ) # throws an error here
end
f(tmm,fmm)

Note that it works fine if the type is declared as:

immutable FakeMethod
    sig
end

[carnaval]

The error is not in the <: computation, but in the fact that you can construct this type with any thing else than FakeMethod(Tuple) because Tuple is the only inhabitant of Type{Tuple}.

[mauro3]

So what would be the correct type for sig? Concerning <:, shouldn't

tm.sig <: fm.sig # = true
fm.sig <: tm.sig # = true

imply

fm.sig == tm.sig # = true

? Or is that also part of the issue you refer to?

[carnaval]

Well if you want the tightest type for the field type I'm pretty sure you have to add a parameter like :

immutable A{T}
   sig :: Type{T}
end

The reason why it is answering strange things in a function is because the a<:b will be eliminated by codegen since inference will say that a::Type{Tuple} and b::Type{Tuple} which implies a === b === Tuple. This is not true here of course because you were allowed to store an object of the wrong type in this field.

I'll look at it this afternoon.

[carnaval]

Smaller repro :

abstract A
abstract B <: A
f{T}(::Type{T},x::T) = x
Base.return_types(f, (Type{Type{A}}, Type{B})) # => Type{A}
f(Type{A},B) # => B

in this issue the f was the implicit convert call in the constructor. The return type was inferred incorrectly.

[carnaval]

seems like a dispatch error caused by the parameter matching algo. I'm not too familiar with the current state of this so maybe its a dup of something.

@timholy could you have a look since apparently you are having fun with this part of the codebase these days :-)

[timholy]

I'll try to check it out later this week.

[vtjnash]

probably a duplicate of #9765
or related to #11015

[mauro3]

(The reference to this issue in my above commit should instead point to #10930)

[timholy]

Partial progress (I have to abandon this for now due to other constraints):

julia> abstract A

julia> abstract B <: A

julia> T = TypeVar(:T, true)
T

julia> typeintersect(Tuple{Type{T}, T}, Tuple{Type{A}, B})
Tuple{Type{A},_<:B}

Setting a breakpoint in jl_type_intersection_matching suggests that there's a failure (I think) in solve_tvar_constraints:

1424        if (!solve_tvar_constraints(&env, &eqc)) {
(gdb) p env->n
$1 = 6
(gdb) p eqc->n
$2 = 2
(gdb) call jl_(env->data[0])
#T<:Any
(gdb) call jl_(env->data[1])
Main.B
(gdb) call jl_(env->data[2])
_<:Main.B
(gdb) call jl_(env->data[3])
Main.B
(gdb) call jl_(env->data[4])
_<:Main.B
(gdb) call jl_(env->data[5])
#T<:Any
(gdb) call jl_(eqc->data[0])
#T<:Any
(gdb) call jl_(eqc->data[1])
Main.A
(gdb) n                                  # run solve_tvar_constraints
1431        int env0 = eqc.n;
(gdb) p eqc->n
$3 = 6
(gdb) call jl_(eqc->data[0])
#T<:Any
(gdb) call jl_(eqc->data[1])
Main.A
(gdb) call jl_(eqc->data[2])
_<:Main.B
(gdb) call jl_(eqc->data[3])
_<:Main.B
(gdb) call jl_(eqc->data[4])
_<:Main.B
(gdb) call jl_(eqc->data[5])
_<:Main.A

[timholy]

julia> T = TypeVar(:T, true)
T

julia> typeintersect(Tuple{T,T},Tuple{Float64,FloatingPoint})
Tuple{Float64,Float64}

julia> typeintersect(Tuple{Type{T},T},Tuple{Type{Float64},FloatingPoint})
Tuple{Type{Float64},Float64}

julia> typeintersect(Tuple{Type{T},T},Tuple{Type{FloatingPoint},FloatingPoint})
Tuple{Type{FloatingPoint},_<:FloatingPoint}

julia> typeintersect(Tuple{Type{T},T},Tuple{Type{FloatingPoint},Float64})
Tuple{Type{FloatingPoint},Float64}

julia> typeintersect(Tuple{T,Type{T}},Tuple{Float64, Type{FloatingPoint}})
Tuple{Float64,Type{FloatingPoint}}

Since isa(Float64, Type{FloatingPoint}) == false, is it fair to say that the last two should be Bottom?

[timholy]

Wow, this is looking like more of a rabbit hole than I expected. I can solve my typeintersect demo above with this:

@@ -1263,7 +1265,24 @@ static int solve_tvar_constraints(cenv_t *env, cenv_t *soln)
             }
         }

-        // 3. given T, let S´ = intersect(all S s.t. (T=S) or (S=T) ∈ env). add (T=S´) to soln.
+        // 3. check compatibility of T==S && T<:R (requires S<:R)
+        for(int i=0; i < soln->n; i+=2) {
+            jl_value_t *tv = soln->data[i];
+            if (jl_is_typevar(tv)) {
+                jl_value_t *ts = soln->data[i+1];
+                for (int j=0; j < env->n; j+=2) {
+                    jl_value_t *tvj = env->data[j];
+                    if (tv == tvj)
+                        if (!jl_subtype(ts, env->data[j+1], 0)) {
+                            return 0;
+                        }
+                }
+            }
+        }
+
+        // 4. given T, let S´ = intersect(all S s.t. (T=S) or (S=T) ∈ env). add (T=S´) to soln.
         for(int i=0; i < env->n; i+=2) {
             jl_value_t *T = env->data[i];
             jl_value_t **pS = &env->data[i+1];

but then it turns out we've been depending on this behavior for things as simple as

convert(Any, x)

where x is actually more specific than Any. (EDIT: currently this matches convert{T}(::Type{T}, x::T) which doesn't seem right.) You can build base simply by adding

diff --git a/base/essentials.jl b/base/essentials.jl
index 702dd82..5688a4b 100644
--- a/base/essentials.jl
+++ b/base/essentials.jl
@@ -43,6 +43,7 @@ call{T}(::Type{T}, arg) = convert(T, arg)::T
 call{T}(::Type{T}, args...) = convert(T, args...)::T

 convert{T}(::Type{T}, x::T) = x
+convert{T}(::Type{T}, x) = x  # fallback

 convert(::Type{Tuple{}}, ::Tuple{}) = ()
 convert(::Type{Tuple}, x::Tuple) = x

but in running the tests there turn out to be other such instances (e.g., A_mul_B!, etc). It makes one wonder how many packages are also relying on this.

[timholy]

For the original problem, one might also have to delete or modify this, because it converts Type{B} into DataType.

[JeffBezanson]

I think this problem is specific to Type{ }, where you can have a concrete type that is a strict subtype of another. The solution is to be very clear about how static parameters are inferred. The following function:

f{T}(x::T) = T

is equivalent to typeof. f(B) gives DataType. Therefore given

f{T}(::Type{T},x::T) = x
f(Type{A}, B)

the first argument gives T = Type{A}. But the type of x is DataType, which is not a subtype of Type{A}, so the method should not be applicable.

[timholy]

I could be wrong, but I worry it's not that specific to Type:

julia> abstract A

julia> abstract B <: A

julia> T = TypeVar(:T, true)
T

julia> typeintersect(Tuple{Ptr{T}, T}, Tuple{Ptr{A}, B})
Tuple{Ptr{A},_<:B}

(EDIT: Array{T,1} works just as well.)

Presumably the result here should be Union()?

[JeffBezanson]

No, that's correct: T=A, and everything that matches T is a subtype of it. One could dislike this behavior, but it's sound. The case with Type{ } is actually unsound, because we are passing something to an argument slot of type T that is not of type T.

[timholy]

OK, good. Glad you're tackling this; I was going in entirely the wrong direction.

[vtjnash]

it looks like the original issue was fixed by 9de38dc

carnaval's followup (#11327 (comment)) appears to still be valid (may be a duplicate of #11015 however)