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.

[cpovirk]

(DefaultTypeHierarchy.visitTypeArgs might turn out to be the level at which ? super passes one check and ? extends passes the other.)

[cpovirk]

DefaultTypeHierarchy.visitTypeArgs might turn out to be the level at which ? super passes one check and ? extends passes the other.

Probably:

• ? super: The first isContainedMany check succeeds.
• ? extends: The first isContainedMany check fails, and the second succeeds.

(noting that I'm testing with the changes discussed above)

Here's the code I'm referring to and the JDK 11 spec section it refers to. The specific spec items are:

C<S1,...,Sn>, where Si contains Ti (1 ≤ i ≤ n) (§4.5.1).

Given a generic type declaration C<F1,...,Fn> (n > 0), the direct supertypes of the parameterized type C<R1,...,Rn> where at least one of the Ri (1 ≤ i ≤ n) is a wildcard type argument, are the direct supertypes of the parameterized type C<X1,...,Xn> which is the result of applying capture conversion to C<R1,...,Rn> (§5.1.10).

The former shouldn't apply here at all, since at least one of the type arguments is a wildcard. So the mystery may be why capture-converting the type with ? super produces a type that doesn't act how we'd want in subtyping tests.

In hindsight, I guess I could have seen that coming, given that I previously avoided a problem with plain ? super (in the absence of ? extends in the same parameter) by removing... an applyCaptureConversion call :)

[cpovirk]

OK, I backed out the applyCaptureConversion removal so that I could test with a type that has only ? super in it.

As before, we end up in DefaultTypeHierarchy.visitDeclared_Declared. In my new test, that's with subtype Predicate<capture#154 of ? extends Object* super E>* and supertype Predicate<? super E>, where Predicate is a locally declared, unannotated type (not the JDK type). That leads us again to the second isContainedMany call in visitTypeArgs with essentially the same values:

isCapturedMany(
   /*subtypeTypeArg=*/ capture#154 of ? extends Object* super E,
   /*supertypeTypeArg=*/ ? super E,
   /*covariantArgIndexes=*/ null)

capture#154 of ? extends Object* super E ought to be contained by ? super E, so let's see what's going wrong....

Actually, regardless of what's going wrong there, I think the supertype should have ? super E* (i.e., unspecified nullness on the E bound). I can't see how fixing that would help our cause here, though, nor do I know if the lack of * is anything new from eisop/checker-framework#746 or other recent changes.

My test code is:

package com.google.foo;

import org.jspecify.annotations.NullMarked;
import org.jspecify.annotations.Nullable;

class Foo {
  interface Predicate<E> {}

  interface Super<E> {
    void g(Predicate<? super E> p);
  }

  @NullMarked
  interface Sub<E extends @Nullable Object> extends Super<E> {
    @Override
    void g(Predicate<? super E> p);
  }
}

[cpovirk]

Weird: The debugger shows that we have a previous result for areEqualVisitHistory, which is false. So we... return false immediately?

But areEqualVisitHistory is for checking full-on equality, not containment, right? (It's shared with StructuralEqualityComparer, so probably?) I can understand returning immediately if the answer is true, but if it's false, then we should fall back to the rest of the containment checks, right? For that matter, how can we put into areEqualVisitHistory (which, again, seems to be used for equality checks) based on the results of a containment check? Some of the puts are for "a placeholder in case of recursion, to prevent infinite regress," but then we put a real result at the end. (The part about infinite regress also suggests that we can't "just disable" the history; that is, it's not just a cache.)

@wmdietl, is this something that you understand? I may be totally misunderstanding what the code is doing.

[cpovirk]

...but the check fails even if I tell it to proceed if the history had a false value, so I guess I can still try to figure out where it's failing.

(The bit with areEqualVisitHistory still seems weird.)

[cpovirk]

The failing check is:

isSubtype(outsideLower, inside)

i.e.,

isSubtype(E, capture#541 of ? extends Object* super E)

The Checker Framework DefaultTypeHierarchy.isSubtype (which probably delegates back the the JSpecify implementation for at least part of the check) says that it's a subtype, but then the JSpecify isNullnessSubtype check rejects it.

It looks as if isNullnessSubtype should be succeeding by comparing E to E from this call. But the subtype E is has upperBound Object?, and the supertype E has upperBound Object.

The weird upperBound comes from our friend applyCaptureConversion: checkParameters has:

• the element of overriddenParams as Predicate<? super E*>*, where typeArgs[0] has a superBound E* whose upperBound is Object
• the corresponding capturedParam as Predicate<capture#315 of ? extends Object* super E>*, where typeArgs[0] has a lowerBound E whose upperBound is Object

[cpovirk]

There's a call to leastUpperBound that passes null and E* (with upperBound Object*) but gets back E (with upperBound Object?).

We end up in lubWithNull, starting with the opening else case. otherAsLub (and thus the value of lub immediately thereafter) is computed fine. We don't enter the following if. Then we compute lowerBounds, which is @NullnessUnspecified as desired. Then isSubtypeShallow is true, so we replace lub with the annotation from null, which is minusNull. That's bad, so the question is what the isSubtypeShallow check is doing and what its result should be.

The call is:

qualHierarchy.isSubtypeShallow(upperBound, otherTM, nullAnno, nullTM)

The parameters are:

• @NullnessUnspecified
• E (as a TypeMirror)
• @MinusNull
• null (as a TypeMirror)

Ah, and that calls into our isSubtypeQualifiers, which implements lenient subtyping because we're in lenient mode. So we're, like, sure, @NullnessUnspecified is a subtype of @MinusNull, and thus @MinusNull looks like a least upper bound.

So we don't actually want lenient mode for least-upper-bound computations, or at least we don't want it for this part of the computation. But I'm not sure how easily we can disable that. I guess the thing to try would be to always delegate applyCaptureConversion to the strict-mode factory. That may well break other things, but... it's worth a try?

[cpovirk]

--- a/src/main/java/com/google/jspecify/nullness/NullSpecAnnotatedTypeFactory.java      2024-08-07 16:00:04.000000000 -0400
+++ b/src/main/java/com/google/jspecify/nullness/NullSpecAnnotatedTypeFactory.java      2024-08-07 17:31:35.000000000 -0400
@@ -532,6 +532,14 @@
   }
 
   @Override
+  public AnnotatedTypeMirror applyCaptureConversion(
+      AnnotatedTypeMirror type, TypeMirror typeMirror) {
+    return this == withLeastConvenientWorld
+        ? super.applyCaptureConversion(type, typeMirror)
+        : withLeastConvenientWorld.applyCaptureConversion(type, typeMirror);
+  }
+
+  @Override
   protected TypeHierarchy createTypeHierarchy() {
     return new NullSpecTypeHierarchy(
         checker,

That seems to help.

I then tried building the Google code that we use this checker on, but I discovered that I still need the wonkyness check, so I've restored that. (Having already restored the applyCaptureConversion call, I'm left with only some tweaks to unspecified nullness.) I'm kicking off another run, but I need to get going, so I won't have results to report just yet....

[cpovirk]

Yes, it works in Google, and it fixes 7 unexpected errors in NullSpecTest$Lenient:

SuperTypeVariableUnspec.java:33: error: (argument.type.incompatible)
SuperTypeVariableUnspec.java:65: error: (argument.type.incompatible)
SuperTypeVariableUnspec.java:97: error: (argument.type.incompatible)
SuperTypeVariableUnspec.java:123: error: (argument.type.incompatible)
SuperTypeVariableUnspec.java:126: error: (argument.type.incompatible)
SuperTypeVariableUnspec.java:129: error: (argument.type.incompatible)
SuperVsSuperNullable.java:39: error: (argument.type.incompatible)

I'll create a PR to merge it into main-eisop. I would create a PR for main instead, but there, it leads us to not issue errors in 8 cases in which we should (and currently do):

ToArray.java:25: jspecify_nullness_mismatch
ToArray.java:43: jspecify_nullness_mismatch
ToArray.java:57: jspecify_nullness_mismatch
ToArray.java:74: jspecify_nullness_mismatch
ToArray.java:79: jspecify_nullness_mismatch
ToArray.java:84: jspecify_nullness_mismatch
ToArray.java:89: jspecify_nullness_mismatch
ToArray.java:117: jspecify_nullness_mismatch

Presumably those mixed results are a consequence of how the fix interacts with the eisop changes that revealed the problem.

[cpovirk]

Ah, this must not have gotten automatically closed because it didn't get merged into main, only into main-eisop. But given that the problems were exposed only by changes in main-eisop, it's fair to consider it to be fixed already.

[cpovirk]

Note that the Multisets problem from my original post is not fixed. But that is a very rare problem (which I'll work around in https://github.com/google/guava/pull/7330/files) that may well be fixed as part of upstream's reworking of type inference. But the other problems are fixed, and as you can see from https://github.com/google/guava/pull/7330/files, the recent changes to eisop and/or the reference checker have uncovered some missing annotations in Guava.

[cpovirk]

Correction: Not all the problems I was seeing in Google's repo are fixed by #197. (I keep forgetting that I need to test the extra targets we have for special environments like J2CL....) And I assume that my promised fix to eisop defaulting isn't helpful for those, either.

But it looks like the rest will be fixed once I also land the changes to update our handling of substitution with unspecified types (as discussed in jspecify/jspecify#248). That will require updates to the samples, and it will probably warrant new tests for the handling of @NonNull.

I don't think that even the combination of those things will address the remainder of #200, but one thing at a time :)

[cpovirk]

Or maybe I'm confused yet again? :)

After kevinb9n's post tonight, I am questioning whether jspecify/jspecify#248 should actually be necessary to fix the problems I'm seeing in some of our implementations of Map.merge and computeIfPresent when building against an unannotated Map class. (I just edited more about this into an earlier mega-post.) It might still be, but I am at least now in quite a bit of doubt.

We'll see when I get back to all this....