LVTI: as per spec upward projection couldn't have resulted in a '? extends' parameterization

[Georgiy Rakov]

HelloDan,

let's consider following code:

    class C0 {}
         class C1 extends C0 {}
             class C2 extends C1 {}

    public class Shell<T extends C1> {
         void set(T t) {}
         T get() {return null;}

         public static void main(String args[]) {
             Shell<? extends C0> y = new Shell<C1>();

             var z = y; //upward projection is applied here

             z = new Shell<C1>(); //compilation succeeds
             z = new Shell<C2>(); //compilation succeeds
             z = new C0();        //obviously compilation error

             C0 c0 = z.get(); //compilation succeeds
             C1 c1 = z.get(); //compilation succeeds
             C2 c2 = z.get(); //compilation error
         }
    }

When compiling this code by javac from jdk10 build 25 we receive 
following output:

    Shell.java:16: error: incompatible types: C0 cannot be converted to
    Shell<? extends C1>
                     z = new C0();        //obviously compilation error
                         ^
    Shell.java:20: error: incompatible types: CAP#1 cannot be converted
    to C2
                     C2 c2 = z.get(); //compilation error
                                  ^
       where CAP#1 is a fresh type-variable:
         CAP#1 extends C1 from capture of ? extends C1
    2 errors

 From this output and the fact which lines compile and which don't it 
follows that the type of 'z' variable was inferred as Shell<? extends 
C1>. However according to spec [1] this couldn't have happened because 
of the following reasoning.

1. Let's consider assertion below from [1]:

    *If /LocalVariableType/ is |var|, then let /T/ be the type of the
    initializer expression when treated as if it did not appear in an
    assignment context, and were thus a standalone expression (15.2
    <https://docs.oracle.com/javase/specs/jls/se9/html/jls-15.html#jls-15.2>).
    The type of the local variable is the upward projection of /T/ with
    respect to all synthetic type variables mentioned by /T/ (4.10.5
    <http://cr.openjdk.java.net/%7Edlsmith/local-var-inference.html#jep286-4.10.5>).*
    **

according to this assertion:*
*type_of(z) = upward_projection(type_of(y)) = 
upward_projection(capture_conversion(Shell<? extends C0>)) = 
upward_projection(Shell<CAP>)
where CAP is a capture variable with following bounds:
NULL_TYPE <: CAP <: glb(C0, C1) =>
NULL_TYPE <: CAP <: C1

2. When applying upward projection to Shell<CAP>, T is Shell<CAP> and 
restricted type variables include just CAP.

3. During upward projection assertions below from [1] are touched:**
**

    *If T is a parameterized class type or a parameterized interface
    type, G<A1, ..., An>, then the result is G<A1', ..., An'>, where,
    for 1 ≤ i ≤ n, Ai' is derived from Ai as follows:
       ...
       If Ai is a type that mentions a restricted type variable, then
    Ai' is a wildcard. Let U be the upward projection of Ai. There are
    three cases:
    *

Here we have just A1 which is CAP so 
U=upward_projection(A1)=upward_projection(CAP)=upward_projection(C1)=C1

4. Afterwards following assertion from [1] is touched:

    *If /U/ is not |Object|, and if either the declared bound of the ith
    parameter of /G/, /Bi/, mentions a type parameter of /G/, or /Bi/ is
    not a subtype of /U/, then /Ai'/ is an upper-bounded wildcard, /|?
    extends| U/.*
    **

Here we have just B1 which is C1, so:
**a. "*/U/ is not |Object|*" is _true_ since U is C1;
b. "*the declared bound of the ith parameter of /G/, /Bi/, mentions a 
type parameter of /G/*" is _false_ since B1 is C1 - no type parameters 
are mentioned;
c. "*/Bi/ is not a subtype of /U/*" is _false_ because both B1 and U are 
C1 so B1 is a subtype of U since a class is always a subtype of itself.

For this reason A1' cannot be defined by this assertion as ? extends C1 
which would make upward projection to result in Shell<? extends C1>, so 
none of other assertions can do either.

This looks like a spec issue because the result of upper projection 
provided by javac looks reasonable. Is it really a spec issue?

It's not quite clear why "*/Bi/ is not a subtype of /U/*" was added to 
the specification. Some examples clarifying this point would be highly 
appreciated.

[1] http://cr.openjdk.java.net/~dlsmith/local-var-inference.html

Thank you,
Georgiy
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.openjdk.java.net/pipermail/compiler-dev/attachments/20171011/82d17701/attachment.html>