Poly Annotation on method receiver's type argument

[aosen-xiong]

Poly annotations are useful for associating the receiver type argument with the return type.

For example, the toArray method below associates the elements from the collection with the return array's element type.

@PolyNull @PolySigned Object[] toArray(Collection<@PolyNull @PolySigned E> this);

Example taken from https://github.com/eisop/jdk/blob/9d40ad20e43217893af1fa818edbe45ec8d11f4e/src/java.base/share/classes/java/util/Collection.java#L353.

In #793, we try to add a subtyping check for type arguments when invoking a method.

However, invoking such a method with a receiver whose type argument has different bounds is disallowed.

public class A<T> {
    void toArray(A<@PolyNull T> this){}

    void test1(A<T> a){
        a.toArray(); // disallowed, a's type is A @NonNull T extends @Nullable Object
                     // the requried receiver is A @Nullable T extends @Nullable Object
    }

    void test2(A<?> a){
        a.toArray(); // disallowed, a's type is A @NonNull ? extends @Nullable Object
                     // the requried receiver is A @Nullable captured extends @Nullable Object
    }
}

Overall, the solution currently is to disable the method receiver subtyping check when the declared method receiver has a poly annotation on its type argument. Is this sound?

Do we have an issue that keeps track of poly-annotations on method receiver type arguments? If not, please open one - we should discuss what needs to be checked to be sound. Add a link to that issue here.

Originally posted by @wmdietl in #793

[aosen-xiong]

At the moment, we don't have full confidence that skip receiver type argument subtyping is sound.

Three issues remain for discussion:

1. Assignment. Is it sound to allow such an assignment? Currently, Nullness Checker rejects the following code. I traced back to some relevant issue with poly on type args and found https://github.com/typetools/checker-framework/pull/2876. But it does not cover the following case.

class MyBox<E extends @Nullable Object> {
  E f;
  void captureIn(MyBox<@PolyNull E> this, @PolyNull E in) {
    this.f = in; // error, found: E extends @PolyNull Object, required: E extends @NonNull Object
  }
}

2. Soundness. If we allow the above assignment, skipping the subtyping on the method receiver would be unsound. The following code captures a null value in the

void demoUnsound(MyBox<String> mbs) {
  mbs.captureIn(null); // unsound because the mbs.f is set to null and mbs.f gives @NonNull String.
}

3. Behaviour consistency. Instead of poly anno on method receiver type argument, poly anno is on a formal parameter, the type argument subtyping is not skipped right now.

class MyBox<E extends @Nullable Object> {
  E f;
  void captureInParameter(MyBox<@PolyNull E> box, @PolyNull E in) {
      this.f = in;
  }

  void demoUnsound(MyBox<E> mbe) {
      captureInParameter(mbe, null); // error, mbe is @NonNull MyBox<E [ extends @Nullable Object super @NonNull NullType ]> and required type is @NonNull MyBox<E [ extends @Nullable Object super @Nullable NullType ]>.
  }
}