Where does the Java spec say List<T> assigns to List<? super T>?

Question

Assume class B inherits from class A. The following is legal Java:

List<A> x;
List<? super B> y = x;

In terms of the specification, this means that List<A> assignsTo List<? super B>. However, I am having trouble finding the part of the spec that says this is legal. In particular, I believe we should have the subtype relation

List<A>  <:  List<? super B>

but section 4.10 of the Java 8 spec defines the subtype relation as the transitive closure of a direct supertype relation S >1 T, and it defines the direct supertype relation in terms of a finite function which computes a set of supertypes of T. There is no bounded function which on input List<A> can produce List<? super B> since there might be an arbitrary number of Bs that inherit from A, so the spec's subtype definition seems to break down for super wildcards. Section 4.10.2 on "Subtyping among class and interface types" does mention wildcards, but it handles only the other direction where the wildcard appears in the potential subtype (this direction fits into the computed direct supertype mechanism).

Question: What part of the spec says that the above code is legal?

The motivation is for compiler code, so it's not enough to understand why it is legal intuitively or come up with an algorithm that handles it. Since the general subtyping problem in Java is undecidable, I would like to handle exactly the same cases as the spec, and therefore want the part of the spec that handles this case.

Answer 1

List<? super B> is defined to be a supertype of List<A> by §4.10.2. Subtyping among Class and Interface Types:

The direct supertypes of the parameterized type C<T1,...,Tn>, where Ti (1 ≤ i ≤ n) is a type, are all of the following:

• D<U1 θ,...,Uk θ>, where D<U1,...,Uk> is a direct supertype of C<T1,...,Tn> and θ is the substitution [F1:=T1,...,Fn:=Tn].

• C<S1,...,Sn>, where Si contains Ti (1 ≤ i ≤ n) (§4.5.1).

Let C<T1,...,Tn> = List<A> and C<S1,...,Sn> = List<? super B>. According to the second bullet, List<? super B> is a supertype of List<A> if ? super B contains A.

The contains relation is defined in §4.5.1. Type Arguments and Wildcards:

A type argument T1 is said to contain another type argument T2, written T2 <= T1, if the set of types denoted by T2 is provably a subset of the set of types denoted by T1 under the reflexive and transitive closure of the following rules (where <: denotes subtyping (§4.10)):

• ? extends T <= ? extends S if T <: S

• ? super T <= ? super S if S <: T

• T <= T

• T <= ? extends T

• T <= ? super T

By the second bullet, we can see that ? super B contains ? super A. By the last bullet, we see that ? super A contains A. Transitively, we therefore know that ? super B contains A.