Subtyping rules for array types

[cpovirk]

I presume that we'll follow Java's precedent, which would let "array of non-null strings" be assigned to "array of possibly null strings," even though that's unsound.

[kevinb9n]

To be far, what made Java's precedent of array covariance tolerable (in the beginning) was that at the worst you'd reliably get an ASE at runtime.

Since we don't have that, then it's how generics was mixed into that that probably forms a more useful precedent for us. There, creating an array of a parameterized type causes a warning (but only a warning). That said, I'm not actually sure how that should translate to our world.

I would say that a method returning an array for the caller to write into, or accepting an array parameter for its own implementation to write into, is probably irregular/unusual/already-problematic enough that it is not worth fitting the design to that case. And that says that continuing to treat arrays as covariant for our purposes is a defensible choice for usability reasons.

But does that go as far as wanting our semantics to actually dictate the following to be incorrect?

class Super { @NotNull String[] foo(); }
class Sub extends Super { @Nullable String[] foo(); }

Not sure.

[kevinb9n]

I think we are probably best to just embrace array covariance. Because arrays are exchanged in APIs far more often to be read than to be written to (I would bet > 20:1), and because Java already treats them as covariant, I think that the code snippet above should indeed be deemed incorrect. That seems like the cleanest thing to do.

I don't think the stakes are high on getting this decision perfect, because object arrays are already grossly inferior to collections (in every single way except as special-case optimizations), and type annotations already make that even worse (no one will ever find @A String @B [] as readable as @B List<@A String>).

Propose to resolve.

[cpovirk]

For API purposes, I'm all for setting on covariance as good enough. (Are there any existing checkers that do anything different? It sounds like the Checker Framework treats them as covariant by default (with an option to treat them as invariant).)

While we're on the subject, though, I looked into some of the questions that affect implementation code.

It's possible to create an array of a parameterized type with just a warning (well, 2 warnings):

List<String>[] a = makeArray(asList("foo"));
...

static <T> T[] makeArray(T... objects) {
  return objects;
}

GenericArrayCast2.java:10: warning: [unchecked] unchecked generic array creation for varargs parameter of type List<String>[]
    List<String>[] a = makeArray(asList("foo"));
                                ^
GenericArrayCast2.java:16: warning: [unchecked] Possible heap pollution from parameterized vararg type T
  static <T> T[] makeArray(T... objects) {
                                ^
  where T is a type-variable:
    T extends Object declared in method <T>makeArray(T...)
2 warnings

(And you can hide the one with @SafeVarargs -- not that it would be appropriate to do so on a method like this, which returns the array to the caller.)

But the more direct way of creating one is an error:

GenericArrayCast2.java:5: error: generic array creation
    List<String>[] a = new List<String>[1];
                       ^

So you have to use a wildcard and an unchecked cast:

List<String>[] a = (List<String>[]) new List<?>[1];

Or, if you don't mind having both an unchecked warning and a rawtypes warning, you can do it in less code:

List<String>[] a = new List[1];

Once you have a List<String>[], it's easy to set up a latent ClassCastException with no further warnings:

List<? super String>[] b = a;
b[0] = asList(0);
String s = a[0].get(0);

Exception in thread "main" java.lang.ClassCastException: java.lang.Integer cannot be cast to java.lang.String
  at GenericArrayCast2.main(GenericArrayCast2.java:10)

I, too, am not sure exactly how to apply all this to nullness yet. Certainly an attempt to create an array of non-null objects is at best "aspirational":

@NotNull String[] totallyDoesNotContainNull = new @NotNull String[1];

(If @NotNull is the default, then it could be omitted. Perhaps it would be surprising for a line with no nullness annotations and no preexisting objects to produce a warning or even error?)

(Another effect of the weird @Nullable String[] syntax is that it looks like you have to annotate the variable -- normally not required by flow-sensitive nullness analysis -- because in fact you're annotating the element type.)

Following the precedent of generics might mean requiring the following and issuing a warning:

String[] totallyDoesNotContainNull = (String[]) new @Nullable String[1];

(There's no "rawtypes workaround" in the case of String[].)

(Maybe it would be more honest for the code to store the array in a variable of type @Nullable String[], fill it in, and then perform the unchecked cast to @NotNull String[]. I suppose that libraries could even provide a casting helper that performs a runtime check of the contents, though that still can't protect against future mutation through the original variable (edit: or after assigning to a new variable of type Nullable String[]?).)

I was going to say that we could special-case creating an empty array, as in new Foo[0], but:

• It's hard to imagine that that's worth a special case. (I guess a few people are stuck calling toArray(T[]), though, and maybe it helps them?)
• I suspect that that can be turned into a latent NullPointerException by using Arrays.copyOf(empty, someNonZeroSize). (Not that we're trying to be 100% sound.) [edit: Is this solvable by making copyOf return a @Nullable T[] when given a T[]?]

[edit: another matter of implementation code: the type of Foo[].class: Class<Foo[]> or Class<@Nullable Foo[]>? See jspecify/jdk@71d8267]

[wmdietlGC]

@cpovirk already mentioned how the Checker Framework handles array covariance in the previous comment, see https://checkerframework.org/manual/#invariant-arrays

By default the CF allows the creation of arrays with non-null component types, but provides an option to be stricter: https://checkerframework.org/manual/#nullness-arrays
and a castNonNullDeep helper method to ensure correct initialization at runtime:
https://github.com/typetools/checker-framework/blob/master/checker/src/main/java/org/checkerframework/checker/nullness/NullnessUtil.java#L82

[cpovirk]

Checker Framework also has special handling of Collection.toArray -- both overloads, I think. Certainly it's a weird API. Maybe we can take the easy way out (though I haven't even thought about this enough to say what that is :))

[wmdietlGC]

Following-up to my earlier comment at #33 (comment):

What about an unspecified library method that returns a @NullUnspec String[]? I would expect a warning when trying to assign that result to a @NotNull String[], but none when assigning to @nullable String[].

The assignment of @NullUnspec String[] to @Nullable String[] should also produce a warning: the legacy code might assume that no null value is contained in that array and this client could break that.

[kevinb9n]

Certainly receiving an array across an API boundary and then writing to it is a thing that can happen, and therefore a soundness analyzer will want to generate the warning you describe (unless it wants to deem the assignment safe anyway from context). So we should not say anything that sounds like we are preventing it from doing that.

I think we should also not say anything that prevents the non-soundness-based checker from deciding to privilege the much more common use case over the other, because there are big advantages to most users for doing that.

Unfortunately we can't just leave this all up to checkers, because an API owner needs a single answer on whether they can safely make a method return @Nullable String[] if it already has overrides returning @NullUnspec String[] or @NotNull String[].

[wmdietlGC]

Wasn't our approach to handling sound tools vs bugfinders that we specify certain things as hard errors and other things as various kinds of warnings. Certain warnings, like these warnings for conversions to/from @NullUnspec could be ignored by default by certain tools. Other tools could elect to make them hard errors.

[kevinb9n]

We know that we require the one kind of "warning" discussed in #33 (and the newly filed #73). I am not sure whether we want to get into "various kinds" of warnings at the level of this project or not. This one discussed here would be a different kind.

[cpovirk]

A related issue: How much do we plan to encourage "lying" about array nullability when we annotate APIs (directly, like for Guava, or in stub files, like for the JDK)?

As an example, take this method:

... class ImmutableCollection<E> ... {
  ...
  public final Object[] toArray() { ... }
}

(As noted above, Collection.toArray is arguably its own special thing, perhaps especially toArray(T[]). But let's pretend that Collection.toArray doesn't exist and that we're just defining our own method. If that's hard to do, then consider FluentIterable.toArray, which does define its own method, instead.)

The returned array will never contain null. However, as soon as we hand the user a @NotNull Object[] (an array of not-null objects; hopefully I got the syntax right), we've opened up a type-system hole. (Well, probably. It depends on the decisions discussed in this issue.)

Object[] notNullObjects = immutableCollection.toArray();
@Nullable Object[] nullableObjects = notNullObjects;
nullableObjects[0] = null;
notNullObjects[0].toString(); // boom

The technically correct thing is going to be to return @Nullable Object[]. But are we willing to put users through that? Maybe: If we're putting users of Map.get through that (#71), then is this really any worse? (Maybe it is: At least with Map.get, you can call requireNonNull on the result. Here, you have to suppress or manually loop if you want to pass an array to a method like ImmutableList.copyOf.)

[cpovirk]

...and I suppose we can ask the same question about parameter types:

... class ImmutableList<E> ... {
  ...
  public static <E> ImmutableList<E> copyOf(E[] elements) { ... }
}

Do we:

• require a @NotNull E[] when there's really "no such thing" and someone has to suppress a warning to obtain a reference of such a type -- though maybe the suppression will be performed often by libraries, as discussed in my previous post?
• accept any @Nullable E[] when we know that we would throw NPE if the array contained null? (This is somewhat like the Joiner case, in which appeared willing to use a signature that would permit NPE, but in that case, not all uses of null elements would NPE.)

[kevinb9n]

(First a boilerplate reminder that using object arrays will be approximately equally painful no matter what we do here.)

I suspect that for most array writes in existence it is relatively easy to verify that the array reference can't have undergone a covariant assignment (usually because it was locally initialized to new SameType[]). All those writes are safe. All the trouble comes from the other writes, which I currently suspect to be a small minority.

I think we don't want to let those naughty writes become a tail that wags the dog here. So I think we can embrace array covariance, to the point of saying:

1. Anything that should be safe as long as those naughty writes aren't happening somewhere is safe enough for us; a checker can always choose to be more concerned about that risk.

2. Anything that tries to treat an array as contravariant though is right out.

[kevinb9n]

so, re: the specific question just asked, I definitely very much want those APIs to be able to say @NotNull E[]. That's good documentation even if it were nothing else.