JSpecify JDK models: Collection.toArray() cannot be both called and overridden #1728

Version

NullAway 0.14.0, and current master (21f02dd). Error Prone 2.50.0, JDK 21.

Flags: -XepOpt:NullAway:JSpecifyMode=true -XepOpt:NullAway:JSpecifyJDKModels=true -XDaddTypeAnnotationsToSymbol=true. JSpecifyJDKModels defaults to JSpecifyExperimental, so JSpecifyExperimental=true turns it on too.

Summary

A call to Collection.toArray() yields @Nullable Object[], taken from the JSpecify JDK model. An override of the same method is checked against Object[], taken from javac. The two disagree, so a class that both implements List and delegates to another list's toArray() has no signature that satisfies both.

The override check does not consult the JDK model at all: with -XepOpt:NullAway:JSpecifyJDKModels=false the call-site error disappears and the override error stays.

Reproducer

package foo;

import java.util.AbstractList;
import java.util.List;
import org.jspecify.annotations.NullMarked;
import org.jspecify.annotations.Nullable;

@NullMarked
class Test {
  static Object[] call(List<String> list) {
    // BUG: Diagnostic contains: incompatible types: @Nullable Object [] cannot be converted to Object []
    return list.toArray();
  }

  static class MyList extends AbstractList<String> {
    @Override public String get(int index) { return ""; }
    @Override public int size() { return 0; }

    // BUG: Diagnostic contains: Method returns @Nullable Object [], but overridden method returns Object []
    @Override public @Nullable Object[] toArray() { return new Object[0]; }
  }
}

Test.java:11: warning: [NullAway] incompatible types: @Nullable Object [] cannot be converted to Object []
    return list.toArray();
                       ^
Test.java:19: warning: [NullAway] Method returns @Nullable Object [], but overridden method returns Object [], which has mismatched type parameter nullability
    @Override public @Nullable Object[] toArray() { return new Object[0]; }
                                        ^

The second one is the clearer defect on its own: the override spells exactly the signature the model gives List.toArray(), and it is rejected.

The combination that has no answer

static class MyList extends AbstractList<String> {
  private final List<String> delegate;

  MyList(List<String> delegate) { this.delegate = delegate; }

  @Override public String get(int index) { return delegate.get(index); }
  @Override public int size() { return delegate.size(); }

  // BUG: Diagnostic contains: incompatible types: @Nullable Object [] cannot be converted to Object []
  @Override public Object[] toArray() { return delegate.toArray(); }
}

Object[] is the only return type the override check accepts, and the delegated call produces @Nullable Object[].

What does and does not report

The last two rows are worth contrasting with the rest: for toArray(T[]) the override check does see the model, and rejects an override whose type variable is non-null bounded where java.util.List.toArray has a @Nullable upper bound. So models reach the override check for type-variable bounds, and the array-element annotation is what goes missing.

Expected

The call site and the override should agree on one signature for the same method. Either the override check reads the model's @Nullable Object[] — which makes the identical-signature override above legal, while Object[] stays legal as a covariant narrowing — or the model's return type follows the collection's element type, which would also settle the call site.

Workaround

Cast the call's result. Calcite has a helper for it, org.apache.calcite.linq4j.Nullness.castNonNullArray.

Where we hit it

FlatLists, which both implements List and delegates to another list's toArray, while replacing the Checker Framework with NullAway in Apache Calcite (apache/calcite#5213).