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

[Stephan Herrmann]

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>)
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