subtyping regression: Vector{T} is not considered concrete

[julbinb]

This example used to work in julia 0.6.0 and 0.6.2 but now is broken by the commit 88a4db2:

julia> (Tuple{Vector{T}, Vector{T}} where T) <: Tuple{T,T} where T
false

Should be true because Vector{T} is concrete for any instantiation of T.

[vtjnash]

This was an intentional change.

(Tuple{Vector{T}, Vector{T}} where T) consists of the elements (Tuple{Vector{T}, Union{}}, Tuple{Union{}, Vector{T}}, Tuple{Vector{T}, Vector{T}}, Tuple{Union{}, Union{}})

while

Tuple{T,T} where T is only the latter two (Tuple{Vector{T}, Vector{T}}, Tuple{Union{}, Union{}})

So we can see that they aren't equivalent.

[julbinb]

Should it be Vector{Union{}} instead of Union{} everywhere in the example?

[julbinb]

Let's try a more restrictive example:

(Tuple{Vector{T}, Vector{T}} where T<:Int) <: Tuple{S,S} where S<:Vector{Q} where Q<:Int

My understanding is that the left type Tuple{Vector{T}, Vector{T}} where T<:Int is semantically equivalent to

Union{
  Tuple{Vector{Int}, Vector{Int}},
  Tuple{Vector{Union{}}, Vector{Union{}}}
}

because T ∈ {Union{}, Int} and we just enumerate all possible instances of T to get a respective where-type.

The type on the right Tuple{S,S} where S<:Vector{Q} where Q<:Int is semantically equivalent to

Union{
  Tuple{Vector{Int}, Vector{Int}},
  Tuple{Vector{Union{}}, Vector{Union{}}}
}

Because Q ∈ {Int, Union{}}, and therefore S ∈ {Vector{Int}, Vector{Union{}}, Union{}}, but since S should be concrete we throw out Union{}.

Type such as Tuple{Vector{Int}, Union{}} is certainly subsumed by Tuple{Vector{Int}, Vector{Int}}, but I don't see why it should be initially considered an element of Tuple{Vector{T}, Vector{T}} where T<:Int.

[martinholters]

Isn't Tuple{Vector{Int},Union{}} a subtype of of any two-element Tuple where the first element is a supertype of Vector{Int}, unless it is constrained by the diagonal rule?

[vtjnash]

Should it be Vector{Union{}} instead of Union{} everywhere in the example?

Vector{T} includes Vector{Union{}}

is semantically equivalent to

Not precisely. There's also the diagonal constraint, which states that the types must be the same.

since S should be concrete we throw out Union{}

This isn't necessarily true, but it's subtle, since it starts to run up against the question of how we define the term "concrete", and then simply becomes a tautology. Instead, consider by analogy that Vector{Union{}} is a concrete type, so we should expect that Tuple{Union{}} is too. But it's simply just not an inhabited concrete type (e.g. it can't be constructed). However, subtyping doesn't care if a type is inhabited, only if it is valid. We can similarly also observe that if Julia allowed null references, it would be inhabited, so this isn't relevant for subtyping.

[julbinb]

@vtjnash I totally agree with the last paragraph, but I still don't see why we should somehow explicitly consider Tuple{Vector{T}, Union{}} belonging to Tuple{Vector{T}, Vector{T}}.

When we say that (Tuple{Vector{T}, Vector{T}} where T) <: Tuple{T,T} where T is false because the LHS type includes Tuple{Vector{T}, Union{}},
why don't we say that Tuple{Int,Int} includes Tuple{Int,Union{}} and, therefore, Tuple{Int,Int} <: Tuple{T,T} where T is also false?

I don't see the difference between Vector{T} and Int that would justify including Union{} into the former type and not-including it into the latter one.

[martinholters]

julia> (Tuple{Vector{T},Union{}} where T) <: (Tuple{Vector{T},Vector{T}} where T)
true

julia> Tuple{Vector{T} where T,Union{}} == (Tuple{Vector{T},Union{}} where T)
true

But Vector{T} where T is not concrete.

[vtjnash]

Yes, I agree that's a problem. We currently have no way to identify that Tuple{Int, Int} means exactly that (and not Tuple{Int, Union{}}) in dispatch. However, this result is needed for dispatch, so it has to be computed wrongly. Looking back at the issue martinholters opened about this, I see he talked about this specific case: #24614 (comment)

[julbinb]

@martinholters @vtjnash Oh, I think I finally see what you are saying. Since

julia> Tuple{Vector{T} where T, Union{}} <: Tuple{Vector{Q}, Vector{Q}} where Q
true

it is bad to have (Tuple{Vector{Q}, Vector{Q}} where Q) <: Tuple{S,S} where S because it breaks transitivity in

julia> Tuple{Vector{T} where T, Union{}} <: Tuple{S, S} where S
false

Is that right?

[martinholters]

At least, that is what was trying to say, yes.

[vtjnash]

Right. Another possible option would be prohibit forming types with Union{} as a type-parameter – this appears to have been the path taken by Rust, for example (only ref I have for this is https://github.com/rust-lang/rfcs/blame/master/text/1216-bang-type.md#L345) – then compute whether any of the type-parameters might have a subtype after apply_type (this is what the code attempted to do before 88a4db2).

[julbinb]

Just more discussion.
After some thinking it seems that the problem here stems from inconsistency in subtyping between diagonal types and tuple-where types.

If we don't have diagonality, then it always holds that Tuple{t where T, ...} == Tuple{t, ...} where T. Including this:

julia> (Tuple{Vector{T}, Union{}} where T) == Tuple{Vector{T} where T, Union{}}
true

However, the following subtype relations are not consistent (in julia 0.6.2):

julia> (Tuple{Vector{T}, Union{}} where T) <: Tuple{S, S} where S
true

julia> Tuple{Vector{T} where T, Union{}} <: Tuple{S, S} where S
false

You fixed this by making the first relation false. Another way would be to make the second true.

The second approach would work naturally if subtyping was defined on "normalized" types exclusively. Where normalization makes Tuple{t where T, ...} ==> Tuple{t, ...} where T.