SequencedCollection was added in Java 21 and needs to be handled

[wmdietl]

Yes, that sounds good. After re-reading some things, my impression is that I was treating the problem as "caused by" this PR because this PR required eisop/checker-framework#746—which is the true cause of the problem.

OK, that wasn't actually hard at all, sorry.

$ git clone [email protected]:jspecify/jspecify-reference-checker.git

$ cd jspecify-reference-checker/

$ git checkout main-eisop # 9e4d14d4a19751a7211bf4c02e202126f59c58f3

$ JAVA_HOME=$HOME/jdk-17.0.2 ./gradlew clean assemble

$ ./demo ListSubclass.java
Note: The Checker Framework is tested with JDK 8, 11, 17, and 21. You are using version 22.
ListSubclass.java:8: error: [override.param.invalid] Incompatible parameter type for filter.
  boolean removeIf(Predicate<? super Z> filter);
                                        ^
  found   : Predicate<? super Z>
  required: Predicate<? super Z*>
  Consequence: method in ListSubclass<Z>
    boolean removeIf(Predicate<? super Z>)
  cannot override method in Collection<Z*>
    boolean removeIf(Predicate<? super Z*>)
1 error
Note: 
  =====
  The nullness checker is still early in development.
  It has many rough edges.
  For an introduction, see https://jspecify.dev/docs/user-guide
  =====

In contrast, if I create a fresh clone and build from the main branch (1a7b3ed), I get a success:

$ ./demo ListSubclass.java
warning: Use JDK 8, 11, or 17 to run the Checker Framework.  You are using version 22.
1 warning

          🤦

I managed to notice that just before posting and then still not post it :)

import java.util.List;
import java.util.function.Predicate;
import org.jspecify.annotations.NullMarked;
import org.jspecify.annotations.Nullable;

@NullMarked
interface ListSubclass<Z extends @Nullable Object> extends List<Z> {
  boolean removeIf(Predicate<? super Z> filter);
}

Originally posted by @cpovirk in #178 (comment)

Yes, that sounds good. After re-reading some things, my impression is that I was treating the problem as "caused by" this PR because this PR required eisop/checker-framework#746—which is the true cause of the problem.

[wmdietl]

From the error message it looks to me like @NullMarked in the annotated JDK is not handled. PR eisop/checker-framework#746 probably broke a work-around to the issue here.
Let me try different configurations to test this and see what the actual issue is.

[wmdietl]

@cpovirk I can't reproduce the issue. In a clean directory, I did:

> git clone https://github.com/jspecify/jspecify-reference-checker -b issue-177
> cd jspecify-reference-checker/
> ./gradlew build

All test cases should pass. This uses the issue-177 branch so that tests pass with latest eisop/master.
I then put the code from above in Issue192.java:

> cat Issue192.java 
import java.util.List;
import java.util.function.Predicate;
import org.jspecify.annotations.NullMarked;
import org.jspecify.annotations.Nullable;

@NullMarked
interface ListSubclass<Z extends @Nullable Object> extends List<Z> {
  boolean removeIf(Predicate<? super Z> filter);
}
> ./demo -Astrict Issue192.java

I tried with/without -Astrict and never get an output.

Do these steps produce different output for you?

[wmdietl]

I have one theory: you are not doing the above, but are instead using the rewritten JDK that contains the stub annotations directly. Could that be the case?

[cpovirk]

Hmm, I can reproduce with the commands given above (specifically, the one without -Astrict).

The JDK question is an interesting one. On the one hand, we're seeing the problem during our Bazel builds, which do use a rewritten JDK and which disable the stub files. On the other hand, I'm also seeing the problem with a direct use of the demo script, which uses an unrewritten JDK and a ../checker-framework/checker/dist/checker.jar with appropriate JSpecify stubs for List and Collection.

I do notice that the issue goes away if I change my class to extend Collection directly instead of List.

Aha: It looks like I can reproduce with JDK 21 (or 22) but not with 11 or 17.

[wmdietl]

Ah! I've been trying with JDK 11.
With JDK 21 I can reproduce the problem now.

I think the reason is the following: https://github.com/openjdk/jdk/blob/2f2223d7524c4405cc7ca6ab77da62016bbfa911/src/java.base/share/classes/java/util/List.java#L141
public interface List<E> extends SequencedCollection<E> {

There is this additional interface SequencedCollection between List and Collection.
That SequencedCollection doesn't exist in jspecify/jdk, so it is unmarked.

That unmarked class causes E to become unmarked, as it should.

So I think everything is working as it should and we need to find a way how to deal with SequencedCollection.
One option I see is to mark the whole java.util package, but that would cover other classes that we haven't annotated yet.
Other ideas?

[cpovirk]

Ooo, nice find! That also explains some other errors, like those on our overrides of forEach inside a NavigableSet.

A reasonable Step 1 might be to add SequencedCollection to our stubs and see how that goes. I'll do some experiments.

• Hopefully the Checker Framework would never even look at that stub unless SequencedCollection was available during the compilation, so that might fix the problem with ./demo Issue192.java.
• Our Bazel setup will probably be happy to compile SequencedCollection.java, and I suspect that we made the subsequent rewriting resilient to having stubs for classes that don't exist. (If we haven't, we're going to want to do that eventually, likely as part of some JDK 21 prep that we've started discussing but not made much progress on yet.)

So hopefully there would be no new problems, and then the question would become whether it solves the existing problem. My guess is that it in principle shouldn't but in practice it probably would: Since extends SequencedCollection<E> doesn't appear in the stub file, the checker in principle shouldn't assume that we know that it should be nullness-annotated as extends SequencedCollection<E> and not as extends SequencedCollection<@Nullable E> or extends SequencedCollection<@NonNull E>. However, in practice, that's not how our stub handling works. And in fact it couldn't work that way without effectively applying a @NullnessUnspecified annotation to that usage of E.

If our checkers did actually care about the missing extends SequencedCollection<E>, then I'd wonder what would happen if we change List to extends SequencedCollection<E>, Collection<E>. That seems more likely to cause errors, both in the Checker Framework and in our Bazel setup. And one reason that it could cause errors in our Bazel setup is that sometimes that setup runs without SequencedCollection available. And on that note:

Only after seeing your explanation do I see that the removeIf error occurs only during our Android builds (under which List extends SequencedCollection) and not during our JRE builds (under which that is not yet the case except for people who opt in—though we should support those people, too). If I had noticed that earlier, then maybe I could have figured this out instead of dumping it on you. But I wouldn't count on it :)

One thing that remains interesting is that we still see some other errors involving ? super types, even during our JVM builds. I can reproduce them with JDK 17 (using the command I shared in the other thread). The errors exist under main-eisop (with or without #177) but not under main.

First, I see several errors like this in Streams.java:

/tmp/tmp.OBavpODHqE/guava/guava/src/com/google/common/collect/Streams.java:364: error: [override.param.invalid] Incompatible parameter type for action.
              public boolean tryAdvance(Consumer<? super R> action) {
                                                            ^
  found   : Consumer<? super R>
  required: Consumer<? super R*>
  Consequence: method in 
    boolean tryAdvance(Consumer<? super R>)
  cannot override method in Spliterator<R*>
    boolean tryAdvance(Consumer<? super R*>)

And second, I see two errors like this in TreeMultimap.java:

/tmp/tmp.OBavpODHqE/guava/guava/src/com/google/common/collect/TreeMultimap.java:224: error: [assignment.type.incompatible] incompatible types in assignment.
    keyComparator = requireNonNull((Comparator<? super K>) stream.readObject());
                                  ^
  found   : Comparator<capture#767 of ? super K>
  required: Comparator<? super K>

Finally, I see an error in Multisets.java that only might be related to ? super (which appears in the type of a method that is being called) or might not be:

/tmp/tmp.OBavpODHqE/guava/guava/src/com/google/common/collect/Multisets.java:1123: error: [argument.type.incompatible] incompatible argument for parameter o of Collections.nCopies.
        entry -> Collections.nCopies(entry.getCount(), entry.getElement()).spliterator(),
                                                                       ^
  found   : E*
  required: E

Maybe we should create a separate issue for those (or two separate issues if you're confident that the Multisets one is separate)? That said, I do feel a lot better about suppressing the relatively small number of errors (which I assume are common both both JVM and Android builds) than about suppressing the larger number earlier. [edit: Also, I can probably fix the Streams ones by annotating AbstractSpliterator.] So that issue doesn't need to be a high priority.

[cpovirk]

Oh, and another thing that I wasn't even thinking about today was:

  found   : Predicate<? super Z>
  required: Predicate<? super Z*>

Even with the stray *, that override should be valid (in lenient mode). So presumably we're computing the type correctly everywhere but we've done something in eisop/checker-framework#746 to make subtyping checks more strict than we'd prefer.

That would explain how all these issues could still be related: They might all be about overly strict checking of ? super.

There still remains the additional problem that SequencedCollection is not annotated. (Nor is AbstractSpliterator, which existed even before JDK 21 and which is responsible for the * we see in Streams.) All this is just to attempt to zero in on what else might be going wrong.

[cpovirk]

Yes, adding an annotated SequencedCollection.java appears to solve the problem (without introducing new problems) for both ./demo and Bazel.

We see similar problems with SequencedMap [edit: and SequencedSet], and I assume that a stub will solve them, too.

Let me send you a PR for those, likely another PR for AbstractSpliterator (or Spliterators as a whole), and similar PRs for eisop/jdk. Then I'll take stock of what errors remain, suppress them internally, and post the list here.

[wmdietl]

Thanks for looking into fixing this! Stub files for these newer APIs sound perfect.
I don't think eisop/checker-framework#746 should have changed anything about strictness of subtyping tests - it was just defaulting improvements.
If you could file separate issues for the other issues - ideally without depending on the JDK - I'll look into fixing those errors.

[cpovirk]

• Add stubs for sequenced collections. jdk#65
• Annotate the sequenced collections for nullness. eisop/jdk#90
• New errors (maybe related to ? super) from eisop/checker-framework#746 #193

Still TODO:

• jspecify and eisop PRs for Spliterators, which I have annotated locally but haven't turned into a PR yet [edit: now Annotate Spliterators. jdk#66 and Mark Spliterators as @AnnotatedFor("nullness"). eisop/jdk#91 for those]