Incompilable instanceof with super-bound

[Maurizio Cimadamore]

On 16/03/2023 11:13, Tagir Valeev wrote:

> Also fails (with same error). Now, there are two questions here:
>
>  1. should the cast be statically rejected - this means asking whether
>     |Sub<?>| and |Super<? super Box<?>>| are provably distinct
>     parameterized types;
>  2. should the cast be allowed without warnings - this means proving
>     that there is only one possible way to go from a |Super<? super
>     Box<?>>| down to a |Sub<?>|;
>
Before I dive into the actual rules, I must pause for a second, and 
tackle the elephant in the room: there is a long-standing discrepancy 
between javac and Eclipse - in that javac static checks around casts go 
beyond what is specified by the JLS. This can result in some casts being 
/rejected/, rather than simply flagged with an unchecked warning. We are 
in one such case here.

Back to the example, we have to prove that there exists a narrowing 
reference conversion (5.1.6.1) between |Super<#CAP1>|, where |#CAP1 :> 
Box<?>| (note the capture conversion here) and |Sub<?>|. To do that we 
have to prove that there is /no/ supertype X of |Super<#CAP1>| and Y of 
|Sub<?>| such that X and Y are provably distinct (4.5). To establish 
that, we need to first find a supertype of |Sub<?>| that can be 
compared  against |Super<#CAP1>|. That supertype is |Super<#CAP2>| where 
|#CAP1 <: Object| (that's the direct supertype of |Sub<?>|). So, are 
|Super<#CAP1>| and |Super<#CAP2>| provably distinct? From the definition:

> Two type arguments are provably distinct if one of the following is true:
>
>     Neither argument is a type variable or wildcard, and the two 
> arguments are not the same type.
>
>     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).
>
>     Each type argument is a type variable or wildcard, with upper 
> bounds (from capture conversion, if necessary) of S and T; and neither 
> |S| <: |T| nor |T| <: |S|.
>
Since the upper bounds of |#CAP1| and |#CAP2| are compatible (after all, 
|Box<?> <: Object| ), we can conclude that, from a JLS perspective, 
|Super<#CAP1>| and |Super<#CAP2>| are /not/ provably distinct. So a 
narrowing reference conversion exists, and the cast should be allowed.

Should there be a warning? This depends on whether the narrowing 
reference conversion is checked - which is defined in 5.1.6.2:

> The unchecked narrowing reference conversions are as follows:
>
>     A narrowing reference conversion from a type S to a parameterized 
> class or interface type T is unchecked, unless at least one of the 
> following is true:
>
>         All of the type arguments of T are unbounded wildcards.
>
>         T <: S, and S has no subtype X other than T where the type 
> arguments of X are not contained in the type arguments of T.

Since here the target T is |Sub<?>|, which contains only unbounded 
wildcards, the conversion should /not/ be unchecked (meaning no warning 
should be generated). This also means that |Sub<?>| is a valid type test 
pattern for the instanceof.

Back to javac, the reason as to why javac disallows the cast (and hence, 
the instanceof) is that javac doesn’t think that you can write a 
well-formed witness of |Super<? super Box<?>>| that is /also/ compatible 
with |Sub<?>|. I believe javac is correct in its assertion: the only two 
witnesses I can think of are |Super<Box<?>>| and |Super<Box>|, neither 
of which seems compatible with |Sub<?>| (as |Sub<T> extends 
Super<Box<T>>|, and there’s no value you can replace for T to make the 
resulting type match with either |Super<Box>| or |Super<Box<?>>|). Which 
is exactly the same reason as to why javac doesn’t think (inside the 
|main| method) that there’s a way for |new Sub<>| to be inferred such 
that the inferred type is compatible with |Super<? super Box<?>>|.

Now, while there are some discrepancies between what the JLS say and 
what javac does with respect to narrowing reference conversions, there 
should be no such discrepancies when it comes to inference. Note that 
the same failure with |new Sub<>| can be reproduced even w/o method 
call, as in:

|Super<? super Box<?>> s = new Sub<>(); |

In this case the compiler has to prove that:

|Sub<alpha> <: Super<? super Box<?>> --> Super<Box<alpha>> <: Super<? 
super Box<?>> --> Box<alpha> <= ? super Box<?> --> Box<?> <: Box<alpha> 
--> ? <= alpha --> false |

(that’s because 18.2.3 doesn’t have any notion of how to reduce the 
above type containment).

In other words, there’s no instantiation for alpha which makes the above 
proof correct, so infererence must fail.

Summing up, we know there are difference between how Eclipse, JLS and 
javac deal with narrowing reference conversions. But, typically the 
mismatches have to do with corner cases where no concrete witness for 
the cast can be produced. So I think the most important question here is 
whether |isSub(new Sub<>())| should succeed at all. I don’t think it 
should (see above) - and if that’s the case, this seems “just” another 
case where javac eagerly rejects a cast that seems unsound anyway.

Cheers

Maurizio

​
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mail.openjdk.org/pipermail/compiler-dev/attachments/20230316/842dff4c/attachment-0001.htm>