Incompilable instanceof with super-bound

[S A]

Hi,

on the topic of ecj, neither javac nor ecj accept the call when passing
Sub<?>:

public static void main(String[] args) {
Sub<?> s = new Sub<Box<String>>();
System.out.println(isSub(new Super<Box<String>>()));
}

The ecj compile error is:

1. ERROR in .../test/Test.java (at line 16)
        System.out.println(isSub(new Super<Box<String>>()));
                           ^^^^^
The method isSub(Test.Super<? super Test.Box<?>>) in the type Test is not
applicable for the arguments (Test.Super<Test.Box<String>>)
----------
1 problem (1 error)

The javac compile error is:

test/Test.java:5: error: incompatible types: Super<CAP#1> cannot be
converted to Sub<?>
                return next instanceof Sub<?>;
                       ^
  where CAP#1 is a fresh type-variable:
    CAP#1 extends Object super: Box<?> from capture of ? super Box<?>
test/Test.java:16: error: incompatible types: Super<Box<String>> cannot be
converted to Super<? super Box<?>>
                System.out.println(isSub(new Super<Box<String>>()))

I've not looked into why the cast is not rejected, but from what I
understand the JLS has enough grey area in that regard. So maybe not
rejecting the cast is OK specification-wise. When in doubt please open an
issue at: https://github.com/eclipse-jdt/eclipse.jdt.core/issues

I hope I didn't misunderstand the questions/comments. If so, sorry for the
noise.

Best regards,
Simeon

On Thu, 16 Mar 2023 at 16:54, Maurizio Cimadamore <
maurizio.cimadamore at oracle.com> wrote:

> 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/1678fd9a/attachment-0001.htm>