Re: 18.5.2: ⟨|R| → T⟩ vs ⟨R θ → T⟩

[Dan Smith]

I had set this aside because I had some related javac bugs to look at.  Circling back now.

On Feb 15, 2014, at 1:45 PM, Stephan Herrmann <stephan.herrmann at berlin.de> wrote:

> Is javac right to accept this program?
> (I couldn't find an existing bug for this)
> 
> import java.util.*;
> interface A {}
> interface B extends A {}
> public class Z {
>  static Collection<A> test(B[] array) {
>    Collection<A> collection =
>      Collections.unmodifiableCollection(
>          array == null ? Collections.EMPTY_LIST : Arrays.asList((A[]) array));
>    return collection;
>  }
> }
> 
> While reducing the constraint regarding EMPTY_LIST:
>  List → Collection<? extends T#0>
> we need to apply unchecked conversion, which is remembered for later.
> 
> Then during 18.5.2. we apply bullet 3.1:
>  "If unchecked conversion was necessary for the method to be applicable in 18.5.1 ..."
> creating this constraint:
>  ⟨Collection → Collection<A>⟩
> As all subsequent bullets at that level are skipped
> (due to the "Otherwise, ..." disjunction)
> the parameter A in the target type has no effect on inference.
> 
> Hence parameterization of that method is inferred as:
>   Collection<Object> unmodifiableCollection(Collection<? extends Object>)

Here's where you depart from the spec.  See the last step from 18.5.2.

"Then apply θ' to the type of m. If unchecked conversion was not necessary for the method to be applicable in 18.5.1, then this is the invocation type of m; if unchecked conversion was necessary, then this substitution provides the parameter types of the invocation type, while the return type and thrown types are given by the erasure of m's type (without applying θ')."

(This is a fairly recent tweak, as of 0.9.0 (December).)

—Dan

> This return type is not assignment compatible with the LHS Collection<A>.
> Yet, javac does not report this error.
> 
> It appears javac either doesn't respect the fact that unchecked conversion
> was needed, or it simply falls through to the last "Otherwise" bullet.
> Either bug would result in adding also this constraint:
>  ⟨R θ → T⟩
> which lets us infer
>  Collection<A> unmodifiableCollection(Collection<? extends A>)
> which *is* assignment compatible.
> 
> Additional witness in the library:
> Class java.util.stream.FindOps contains a structure at line 58 (at b129),
> which in my strict interpretation of the spec should be illegal,
> but can be accepted if adding the ⟨R θ → T⟩ constraint.
> 
> 
> What's intended?
> Stephan
>