Which part of the JLS specifies that you can't cast from List<? extends List<Superclass>> to List<List<Subclass>>?

Question

(This question is inspired by this question, which I incorrectly answered.)

This code does not compile:

List<? extends List<Number>> list = new ArrayList<>();
List<List<Double>> anotherList = (List<List<Double>>) list;

Note that IntelliJ doesn't report any errors. It only fails to compile when I click "Run".

I understand why this doesn't compile on a conceptual level. list is a list of "something that extends List<Number>", and that "something" can never be List<Double>, because List<Double> is not a subtype of List<Number>, and because no type can implement both since they have the same erasure.

However, when I tried to follow the wording in the language specification to determine whether this cast is valid, I found that the language spec seems to say that this is a valid cast!

Here is my reasoning:

The cast fulfils all three requirements for there to be a Narrowing Reference Conversion from S (List<? extends List<Number>>) to T (List<List<Double>>).

5.1.6.1. Allowed Narrowing Reference Conversion

A narrowing reference conversion exists from reference type S to reference type T if all of the following are true:

• S is not a subtype of T

• If there exists a parameterized type X that is a supertype of T, and a parameterized type Y that is a supertype of S, such that the erasures of X and Y are the same, then X and Y are not provably distinct (§4.5).

• One of the following cases applies:

  • S and T are interface types.
  • [...]

The first and third points are trivially true. To show that the second point is true, we take Collection<List<Double>> to be a parameterised super type of List<List<Double>>, and Collection<? extends List<Number>> to be a parameterised super type of List<? extends List<Number>>. They both erase to the same type Collection. Now we need to show that Collection<? extends List<Number>> and Collection<List<Double>> are not provably distinct (§4.5). The same argument also works for Iterable<...>.

_{Edit: I just realised that the supertypes of List<List<Double>> also include things like List<? extends List<Double>>, not just the superinterfaces of List. But I don't think that will invalidate this argument, as the point is that 1. out of X and Y there is at least one wildcard 2. the wildcard bounds/type arguments of X and Y are subtypes of each other.}

Two parameterized types are provably distinct if either of the following is true:

• They are parameterizations of distinct generic type declarations.

• Any of their type arguments are provably distinct.

Clearly, since they both erase to the same type, the first condition can't be true. We only need to show that the second condition is false.

In §4.5.1, the spec defines "type arguments are provably distinct":

Two type arguments are provably distinct if one of the following is true:

• [...]
• One type argument is a type variable or wildcard, with an upper bound (from capture conversion (§5.1.10), if necessary) of S; and the other type argument T is not a type variable or wildcard; and neither |S| <: |T| nor |T| <: |S| (§4.8, §4.10).

(The other (trivially false) conditions are not shown for brevity) Here, S is List<Number> and T is List<Double>. Both |S| <: |T| and |T| <: |S| holds, as |S| and |T| are the same type. Yes, the subtype relation is reflexive, because the super type relation is reflexive (it's defined as the reflexive and transitive closure on the direct supertype relation).

Therefore the type arguments of Collection<? extends List<Number>> and Collection<List<Double>> are not provably distinct, and so List<? extends List<Number>> and List<List<Double>> are not provably distinct, and so there is (or should be) a conversion from List<? extends List<Number>> to List<List<Double>>!

Where is the error in my reasoning? Is there some other part of the spec that I missed?

Answer 1

Well, I'll just say it after Holger's confirmation and answer: JLS is underspecified (at least) at this location. There are some related JDK bugs that work around the same idea, noticeable this one, that directly hits your question via:

.... Otherwise, map wildcards and type variables to their upper bounds, and then test whether their erasures are related classes or interfaces (that is, one erased type is a subtype of the other)

Only to immediately start the next sentence with:

This is unsound...

So, that bug admits that JLS needs some corrections around this chapter(s).

What I have been struggling with too from your quotes of the JLS are two points:

• One type argument is a type variable or wildcard, with an upper bound (from capture conversion (§5.1.10), if necessary)...

  I do know what capture conversion is, but I was not aware it might be optional to be performed (via that "if necessary"). I always thought that it is performed at each location, all the time.

• What is an upper bound from a captured conversion type?

  In your case, is that upper bound List<Number> or List<?>, for example? In my understanding (or lack of precise JLS explanation), this could be understood either way.

All these (+ your great scrape of the JLS) makes me wonder about the correctness of the JLS here, especially since javac is not following these exact same rules.