Type constraint ignored by typeintersect and function ambiguity check

[yuyichao]

(I was going to wait for the original reporter to report it here but since I don't want to spam the mailing list with update of my minimum test case, I decided to report it here myself)

See the mailing list thread here

Minimum working example

type A
end

type B
end

f{T}(::T, ::T) = nothing
f{T<:B}(::A, ::T) = nothing

g{T<:B}(::A, ::T) = nothing
g{T}(::T, ::T) = nothing

t1 = f.env.defs.sig
t2 = f.env.defs.next.sig

println("Signatures: $t1, $t2")
println("Intersect: $(typeintersect(t1, t2))")
println("Intersect: $(typeintersect(t2, t1))")

Output after fixing the ambigious error output formatting.

Warning: New definition 
    f(A, T<:B) at /home/yuyichao/tmp/julia/type_intersect.jl:10
is ambiguous with: 
    f(T, T) at /home/yuyichao/tmp/julia/type_intersect.jl:9.
To fix, define 
    f(A, A)
before the new definition.
Signatures: Tuple{T,T}, Tuple{A,T<:B}
Intersect: Union()
Intersect: Tuple{A,A}

[yuyichao]

As mentioned in the mailing list thread,

1. Whether A and B are abstract or not doesn't matter
2. This seems to be a regression since 0.3

[yuyichao]

Possibly related #8652 (not sure if that one was a regression as well):

The following simplified version of the code from #8652 does not produce a warning when it should....

julia> type A; end

julia> f{T}(::T, ::T) = 1
f (generic function with 1 method)

julia> f{T}(::T, ::A) = 2
f (generic function with 2 methods)

Edit: This bug is indeed a regression compare to 0.3.7 while #8652 is not...

[yuyichao]

Just for clarification, am I right that f{T}(::T, ::T) and f{T}(::T, ::A) should be ambigious here?

AFAICT, as long as the set of types either signature matches is not a subset of the other one and the two set also have common elements, the two method should be ambigious. If this is true, then since only f{T}(::T, ::A) matches {Int, A}, only f{T}(::T, ::T) matches {Int, Int} and they both matches {A, A} they should be ambigious.

Different from what is reported in #8652, the result from the example above seems to be the same indepent of the order the methods are defined though....

[timholy]

Yes, I think the second should be ambiguous and the first not. I'm still a little hazy on these things, though.

While this doesn't answer the question of what's wrong, this gets at the internal machinations:

julia> ams(a, b) = ccall(:jl_args_morespecific, Cint, (Any,Any), a, b)
ams (generic function with 1 method)

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

julia> type A; end

julia> type B; end

julia> t1 = Tuple{T, A}
Tuple{T,A}

julia> t2 = Tuple{T, T}
Tuple{T,T}

julia> ams(t1,t2)
1

julia> ams(t2,t1)
0

julia> TB = TypeVar(:T, B, true)
T<:B

julia> t3 = Tuple{A, TB}
Tuple{A,T<:B}

julia> ams(t3,t2)
0

julia> ams(t2,t3)
0

[yuyichao]

IMHO, this is probably the reason (at some level) for #8652 and t1 shouldn't be more specific than t2. I think ams is right here that none of t2 and t3 are more specific than each other but then the typeintersect incorrectly determines that they can both match to Tuple{A, A}

[timholy]

I haven't taken the time to check what's going on with gdb, but the thing that puzzles me is that check_ambiguous calls jl_type_intersect .

[yuyichao]

That's the reason I mentioned typeintersect in my original report. Is it not meant to handle this?

[yuyichao]

The document doesn't say much about typeintersect and TypeVar. Actually the following part is the only place I find TypeVar in the document.

“Leaf Type” :: A group of related data that includes a type-tag, is managed by the Julia GC, and is defined by object-identity. The type parameters of a leaf type must be fully defined (no TypeVars are allowed) in order for the instance to be constructed.

[yuyichao]

Also should typeintersect be commutative? The name seems to suggest it is, but apparently not in this case.

[timholy]

Ah, I hadn't noticed the non-commutivity, sorry for not reading carefully enough. (I should add: your bug reports and investigations of underlying causes---not to mention your fixes---are exemplary.) I'll bet that's the underlying issue. Yes, typeintersect should be commutative. I had a bug due to the same problem, #10911 (comment).

The document doesn't say much about typeintersect and TypeVar.

I agree. Having finally gotten the hang of them in just the last couple of weeks myself, I'm in the middle of a pretty big documentation project. I was going to finish it in one monolithic go, but let me know if you want it sooner and I'll push some pieces.

[pao]

Non-commutative typeintersect seems like a good reason to mention @JeffBezanson by name.

[mauro3]

Jeff once commented in one of my issues that TypeVars shouldn't be used: #9043 (comment). Maybe that could be one of the reasons that they are not documented. Anyway, looking forward to @timholy documentation.

[yuyichao]

@mauro3 I think @timholy 's document on TypeVar is already merged and can be found here It's very helpful in general (not only for TypeVar) to understand the type system (in additional to Jeff's thesis, which is great but a little bit too long =P. )

Edit: Ahh, yeah, he mentioned me but didn't refer to this PR so the PR for the doc didn't appear in the timeline of this PR. Anyway, here was the PR #11185

[mauro3]

Cool!

[timholy]

I wouldn't use TypeVars in actual code, but knowing a bit about them is irreplaceable if you want to, for example, isolate & fix bugs in the type system.

[aviks]

The original problem the referenced email thread in this issue manifested itself when using JavaCall. I can confirm that this is fixed with the latest master. Thanks @timholy !