New errors (maybe related to `? super`) from eisop/checker-framework#746

[cpovirk]

Using the command given here to test with main-eisop:

/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

E* should be a valid substitute for E in lenient mode.

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

I'm not totally sure what's up with that one, nor even that these two errors are closely related.

Previous discussions (which also touched on the problem that SequencedCollection and friends are unannotated):

• Introduce a NullSpecTypeValidator to ensure unspecified type variables are ok #178 (comment)
• Clarify defaulting of type variable uses eisop/checker-framework#746 (comment)
• SequencedCollection was added in Java 21 and needs to be handled #192

I have promised to try to produce a smaller repro of this problem. For now, I'm filing this issue as a placeholder.

[wmdietl]

I tried minimizing a test case with ? super TV that doesn't depend on the JDK:

> cat Issue193.java 
import org.jspecify.annotations.NullMarked;
import org.jspecify.annotations.Nullable;

class Box<B extends @Nullable Object> {}

interface MyList<T extends @Nullable Object> {
  boolean removeIf(Box<? super T> b);
}

@NullMarked
interface ListSubclass<Z extends @Nullable Object> extends MyList<Z> {
  boolean removeIf(Box<? super Z> b);
}

> ./demo Issue193.java
Issue193.java:12: error: [override.param.invalid] Incompatible parameter type for b.
  boolean removeIf(Box<? super Z> b);
                                  ^
  found   : Box<? super Z>
  required: Box<? super Z*>*
  Consequence: method in ListSubclass<Z>
    boolean removeIf(Box<? super Z>)
  cannot override method in MyList<Z*>
    boolean removeIf(Box<? super Z*>*)
1 error

There is quite some unspecified nullness, but I think they are expected in MyList:

• the * on the Box parameter type itself is because the code is in unmarked scope.
• the Z* is because type variable uses in unmarked scope are unspecified:

  jspecify-reference-checker/src/main/java/com/google/jspecify/nullness/NullSpecAnnotatedTypeFactory.java

  Line 162 in af9dfbc

  TypeUseLocation.TYPE_VARIABLE_USE,

• maybe up for discussion is the cannot override method in MyList<Z*>, which is from the substitution of the nullmarked Z into the unmarked MyList

So the types themselves look correct. What is unclear is why the nullmarked signature is not allowed as override for the unspecified method.
If I use Box<?> as parameter type, the override is accepted - so the top-level subtype test seems okay.
So maybe something with the type hierarchy for ? super and unspecified nullness doesn't work as we want it to.

@cpovirk Do the types themselves look correct to you?

[cpovirk]

I left some more comments on #178 (comment) before coming back here....

I might continue to postpone looking at this further until maybe Tuesday (when I'll be in a better position to attach a debugger), but I wonder if we need to expand our existing special case for ? extends to also cover ? super:

jspecify-reference-checker/src/main/java/com/google/jspecify/nullness/NullSpecAnnotatedTypeFactory.java

Lines 662 to 669 in af9dfbc

	// Work around wonkyness of CF override checks.
	AnnotatedTypeVariable subTV = (AnnotatedTypeVariable) subtype;
	if (isCapturedTypeVariable(subTV.getUnderlyingType())) {
	AnnotatedTypeMirror subTVBnd = subTV.getUpperBound();
	if (subTVBnd instanceof AnnotatedTypeVariable) {
	subTV = (AnnotatedTypeVariable) subTVBnd;
	}
	}

On the need for the special case, I think I once concluded:

• The Checker Framework (to this day) performs capture conversion on the supermethod's arguments.
• The JLS just wants you to perform essentially a substitution.
• The difference might have something to do with a Checker Framework goal of letting you loosen type-parameter bounds in submethods where that's safe?? (Such loosening would be similar in spirit to contravariant parameter types.)

It looks like our Checker Framework fork had its own checking of parameters for overrides. I don't know if that sort of approach would help us here or not, but even if it did, it would be piling hacks upon hacks :)

[cpovirk]

Actually, wait, my mistake: That JLS citation is just for method-level type parameters, not the class-level ones we're dealing with here. And there might actually be a place for capture conversion in override checking, though I still suspect it would happen at an earlier step (during computing the value of overridden?).

The JLS section about class-level type parameters is probably "as a member of the supertype of C that names I" in 8.4.8.1. I think that "as a member of" refers to 4.5.2. There we can apply capture conversion but only if we are getting the members of a Foo<? extends ...> or similar. In our example, we're getting the members of a Foo<...> (with no ? extends). (That's probably always the case when checking method declarations but maybe not always when checking member references?) So I don't think we want to apply capture conversion at all when checking method declarations for overriding.

In theory, we could override createOverrideChecker to return our own instance, which could set a global variable that changes the behavior of applyCaptureConversion (to make it only apply substitution) during checking.... Or maybe substitution has already been performed? If so, great, but that doesn't exactly make the solution any less hacky :)

I have no pressing need to import #178 into Google to use there (and eisop/checker-framework#746 alone produces much more limited fallout), so I'm not sure how hard I want to think about this. I still dream that someday we can rewrite override checking and more in a simpler way if we don't need to support the full generality of the Checker Framework....

[cpovirk]

If we do want to import this, another option might be to arrange for our compilations that currently see unannotated JDK APIs to see annotated JDK APIs instead. (That's actually what I did last time :)) That would probably mean annotating all the major collection interfaces. In particular, as we know from our experience with SequencedCollection, it's not likely to be enough to just annotate, e.g., removeIf without also annotating List itself (to cover its extends Collection<E>).

[cpovirk]

Removing the capture-conversion step I mentioned above helps more (apparently without creating other problems) but somehow still doesn't solve the problem fully :) I still have problems with replaceAll and computeIfAbsent (and one other method not from the JDK), but I no longer have problems with compute, for example. Maybe now ? super is OK but ? extends is still broken—but only ? extends T, not ? extends @Nullable T / ? extends @NonNull T?

(Certainly we're now at least at the point that I could easily go with suppressions and/or annotating a couple more JDK APIs.)

I sat down intending to run a quick test, and obviously I ended up poking around a little more than that... :) But I'm going to try to stop here for now.

[cpovirk]

I observe that no tests fail (./gradlew clean assemble test) in either typetools or eisop [edit: but it turns out that that part proves nothing] if I remove that applyCaptureConversion call. Nor do any nullness checks in Google's codebase.

I think I've convinced myself that the applyCaptureConversion call should be unnecessary but mostly(?) harmless: The result of capture conversion should always be a subtype of the original type, and the Checker Framework is checking parameters for subtyping, not equality (though the final JSpecify story may be more complex, and that's another reason to consider removing applyCaptureConversion). The fact that it's apparently not harmless in this case does seem like a sign that we're still getting something wrong in the JSpecify subtyping checking. That's the kind of thing that I'll try to look into on ~Tuesday.

[edit: That line dates from the implementation of capture conversion.]

[cpovirk]

I have somehow still not gotten around to attaching a debugger, but I'll note some things here:

I've been testing with a few combinations but now primarily with:

• no wonkyness workaround
• no applyCaptureConversion call
• various tweaks to treat unspecified nullness as if it one of the possibilities is that it was "intended to be" non-nullable
• a @NullMarked type with <E extends @Nullable Object> that extends an unmarked type with just <E>

From what I'm seeing, I think that:

• ? super is fine alone or in combination with other ? super arguments.
• ? extends is fine alone or in combination with other ? extends arguments.
• A type that contains both ? super and ? extends is a problem, whether it's ? super T+? extends T or ? super A+? extends B.

-AatfDoNotCache doesn't help (nor hurt).

My assumption at this point is that ? super passes the first of the two distinct parameter checks and that ? extends passes the second (or vice versa), so together they fail. Hopefully that assumption will turn out to be correct, and hopefully I won't get confused along the way by the two separate checks and results :)

[cpovirk]

I observe that no tests fail (./gradlew clean assemble test) in either typetools or eisop if I remove that applyCaptureConversion call.

Oh, I get the impression that I probably need to perform more testing than that to really see if it's working: I can change checkParameters() to always set success to false, and nothing breaks in ./gradlew clean assemble test. [edit: And in fact I can break Checker Framework tests through the applyCaptureConversion change (or other changes) if I run more tests.]

This slightly undercuts my claim above (though I do still have the significant Google testing to fall back on!) and definitely undercuts my attempt to figure out which of the "two distinct parameter checks" actually matters (at least without also testing on Google's codebase).

[cpovirk]

My assumption at this point is that ? super passes the first of the two distinct parameter checks and that ? extends passes the second (or vice versa), so together they fail. Hopefully that assumption will turn out to be correct

Nope! :) I see the same result if I change checkParameters() to use only...

boolean success = typeHierarchy.isSubtype(overriddenParams.get(i), overriderParams.get(i));

...i.e., without the testTypevarContainment case. (I'm also still omitting the applyCaptureConversion call, as before.)

Incidentally, if I keep only testTypevarContainment, I get errors even for plain ? extends and ? super (though I should probably restore the "wonkyness workaround" if I want to give that a fair shake).

I'm still interested in whether the current Checker Framework override checking could be simplified. (Maybe some of it is a holdover from before the implementation of capture conversion, for example?) To that end, I've put together eisop/checker-framework#829 to test the approach that would work if my dreams came through.

But I will try to actually do the debugger thing shortly... :) After the implosion of my latest theory, I now have no theory about what's happening.

[cpovirk]

OK, I got the debugger hooked up. I've gotten as far as DefaultTypeHierarchy.visitTypeArgs. There, subtype (like subtypeAsSuper) is Function<? super A*, ? extends B*>*, and supertype is Function<? super A, ? extends B>, both as expected from my example. It doesn't look like we end up in the catch (Exception e) case there, so the question would be which of the two isContainedMany calls should be returning true but isn't. But that's it for today.