main-eisop: Fix new incorrect errors involving wildcards

[cpovirk]

See jspecify/jspecify#583 (review).

[cpovirk]

I'd hoped that removing the "wonkyness" workaround (discussed at that link) would help. It does not.

[cpovirk]

I had also said:

I had some other memory of hacking up the fork to disable some check on the grounds that it should be unnecessary. I think it may have been related to capture conversion, too?

I am pretty sure that I am thinking of this: https://github.com/jspecify/checker-framework/blob/b84882d9b2f77c99081118cc7ad095dfcc3484f5/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeValidator.java#L561-L570

Here's the corresponding section in eisop: https://github.com/eisop/checker-framework/blob/d30ebee6d096acfbc03bf6eec8672770d046cd77/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeValidator.java#L587

If I recall correctly, the Checker Framework used to have a relatively understandable-to-me justification for requiring that type arguments be in bounds because it didn't implement capture conversion (which would otherwise bring them "effectively" into bounds). But when it implemented capture conversion, that justification became less clear to me. Yet... possibly that's when the check I short-circuited was added?? Maybe the check is addressing some subtlety like what happens if you, say, declare a type parameter like in class Foo<T extends List<String>> but then write class Foo<? extends List<@Nullable String>? (I think I once made a half-hearted attempt to find the justification for an error for such code in the JLS but didn't find one, so I may just not know what the relevant JLS section is.)

Maybe eisop could provide a way to disable that check, or maybe I can figure out whether it should be succeeding yet isn't. If anything, I would have hoped that the fixes for intersection types would have helped us here....

[cpovirk]

I got to wondering if the errors have existed on main-eisop all this time or whether they're new. (I guess that's a reason to add all the necessary jspecify_but_... lines soon so that we can track any future changes :))

I tried some things. (Spoiler: I didn't figure it out.)

Reverting the defaulting change from https://github.com/jspecify/jspecify-reference-checker/pull/178/files only makes the results for the samples worse. (It looks like it may roughly (but seemingly not exactly) break the tests that I'd marked as fixed in jspecify/jspecify#584, but I'm just guessing based on numbers of failures, not on any specific details of the failures.)

Additionally changing the areBoundsValid implementation to always return true didn't help. (I'm not sure it hurt, either, I guess because we don't let you specify both bounds of a wildcard or type variable? I mean, if you tried, the checker would probably still recognize it [edit: since we haven't ripped out this code in eisop the way we did in our fork], though it should also produce an error.)

The next thing to try might have been to undo eisop/checker-framework#746. But that looks potentially invasive, so I'm not going to go down that road: All I was looking for was any potential obvious lead on what was wrong. Without such a lead, it makes sense to just fire up the debugger.

[cpovirk]

Here's one set of unexpected diagnostics from strict mode:

      CaptureConvertedToObject.java:47: error: (return.type.incompatible)
      CaptureConvertedToObject.java:50: error: (type.argument.type.incompatible)
      CaptureConvertedToObject.java:55: error: (type.argument.type.incompatible)
      CaptureConvertedToObject.java:64: error: (type.argument.type.incompatible)

Those correspond to these lines in the samples.

At first glance, I'd say:

• In at least the first error, capture conversion apparently isn't producing a subtype of Lib. Perhaps the unspecified nullness from the bound is winning out? I would have hoped that that is exactly the kind of thing that #197 would have fixed, except that #197 shouldn't even have been necessary because we're already operating in strict mode.
• The other 3 errors look like what I'd expect if we were requiring the wildcard's bound to be within the type parameter's bound. But in light of the first error, I wonder if the checker is performing capture conversion and then performing the check on the result (as discussed above) but that the capture conversion isn't producing the right type in the first place.

It may be that this mess in our checker-framework fork was previously saving us in this situation. Until I looked at it just now, I had been thinking that its main purpose was to handle a strange case with unspecified nullness, which I think we'll no longer need after the discussion earlier this year on jspecify/jspecify#248. But that is probably only part of the story, unless "the weird way we do substitution and type variables" is referring exclusively to that. (I think it's probably more general.)

I could try copying and pasting that in to see what happens. But again, I think I'll probably fire up the debugger first, assuming that I still have time left today to do so :)

[cpovirk]

Oh, I decided I should actually finish skimming the diffs in our checker-framework fork. I haven't tried to list them all below, just those that struck me as potentially worth revisiting (even including a few where I talked myself out of it along the way).

• https://github.com/jspecify/checker-framework/blob/b84882d9b2f77c99081118cc7ad095dfcc3484f5/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeMirror.java#L1609
• https://github.com/jspecify/checker-framework/blob/b84882d9b2f77c99081118cc7ad095dfcc3484f5/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeMirror.java#L1731
• (and an additional similar change for wildcards later in the file)

Also:

• https://github.com/jspecify/checker-framework/blob/b84882d9b2f77c99081118cc7ad095dfcc3484f5/framework/src/main/java/org/checkerframework/framework/type/AsSuperVisitor.java#L588
• and again a similar change for wildcards

And:

• https://github.com/jspecify/checker-framework/blob/b84882d9b2f77c99081118cc7ad095dfcc3484f5/framework/src/main/java/org/checkerframework/framework/type/SupertypeFinder.java#L303

And:

• https://github.com/jspecify/checker-framework/blob/b84882d9b2f77c99081118cc7ad095dfcc3484f5/framework/src/main/java/org/checkerframework/framework/type/TypeFromTypeTreeVisitor.java#L186 (Note that that replaces a more direct mutation operation that did additional stuff, I think here.)

And, for the record:

• https://github.com/jspecify/checker-framework/blob/b84882d9b2f77c99081118cc7ad095dfcc3484f5/framework/src/main/java/org/checkerframework/framework/type/typeannotator/PropagationTypeAnnotator.java#L135 (probably handled in another way in https://github.com/eisop/checker-framework/blob/d30ebee6d096acfbc03bf6eec8672770d046cd77/framework/src/main/java/org/checkerframework/framework/type/typeannotator/PropagationTypeAnnotator.java#L144 at this point)
• https://github.com/jspecify/checker-framework/blob/b84882d9b2f77c99081118cc7ad095dfcc3484f5/framework/src/main/java/org/checkerframework/framework/util/AnnotatedTypes.java#L238 (similarly: https://github.com/eisop/checker-framework/blob/d30ebee6d096acfbc03bf6eec8672770d046cd77/framework/src/main/java/org/checkerframework/framework/util/AnnotatedTypes.java#L1528)

If we're very lucky, most of those became unnecessary after changes in eisop to handle type variables and other things more correctly (and also changes in our checker, such as #197). But at least now I have the links handy in case they do turn out to look relevant.

[edit: I might be able to see all these remaining relevant changes with git diff origin/upstream framework/src/main.]

[cpovirk]

Here's a more modern, trimmed down file for the first error:

import org.jspecify.annotations.NullMarked;

class CaptureConvertedToObject {
  @NullMarked
  Object x6(UnspecBounded<? extends Lib> x) {
    return x.get();
  }

  interface UnspecBounded<T> {
    T get();
  }

  interface Lib {}
}

And the output:

CaptureConvertedToObject.java:21: error: [nullness] incompatible types in return.
    return x.get();
                ^
  type of expression: {capture#649 of ? extends Lib* super null*}*
  method return type: Object

I'm now debugging with ./demo -Astrict -Aignorejdkastub -J-agentlib:jdwp=transport=dt_socket,server=y,suspend=y,address=5009 CaptureConvertedToObject.java (bearing in mind that I wanted to assemble first myself with JAVA_HOME=/usr/lib/jvm/java-17-openjdk-amd64 ./gradlew jspecifySamplesTest --include-build ../jspecify --include-build ../checker-framework and bearing in mind that demo won't rebuild when I make changes). [edit: I edited -Aignorejdkastub in after the fact so that I can more easily set breakpoints without having them trip during JDK parsing. My other workaround had been to rename the type parameter to "Z" and to make the breakpoints conditional on something like type.underlyingType.toString().equals("T"), but that sounds expensive.]

[cpovirk]

One thing that I notice is that the type of expression has super null* at the end. We would want super null instead (which our formatter would omit from the error message entirely): Even in null-unmarked code, a wildcard or type parameter can have only one bound under JSpecify semantics, aside from those created by a capture conversion that "combines" two different kinds of bounds. And here, the capture conversion should start with two extends bounds and nothing else:

• UnspecBounded<? extends Lib> has its extends bound, so it should have no super bound (or, in Checker Framework terms, a super bound of null).
• The type parameter in interface UnspecBounded<T>, like all type parameters in the JSpecify model, has only an extends bound, never a super bound (again, possibly represented internally differently in Checker Framework terms).

I would have guessed that that was what #178 would accomplish in its change to defaultLocationsMinusNull, but seemingly it hasn't fully? Maybe that's what the comment that referred to eisop/checker-framework#741 was about? Maybe we should keep that comment until a fix lands?

I could imagine that this could explain many of the wildcard errors (though probably not the specific one I'm looking at now, as shown in the previous post).

(@wmdietl for any thoughts)

[cpovirk]

In methodFromUse(MethodInvocationTree), receiverType is UnspecBounded<? extends Lib>. Good.

After applyCaptureConversion, it's UnspecBounded<capture#810 of ? extends Lib>. Good.

Something then goes wrong inside methodFromUse(ExpressionTree, ExecutableElement, AnnotatedTypeMirror), which returns the broken type.

Inside that method:

getAnnotatedType(methodElt) [edit: i.e., memberTypeWithoutOverrides] is T* get(). Good—sort of:

• returnType is shown as T*, but lowerBound is already null*. That's bad, as discussed above. We don't see that in the normal string output because our formatter doesn't output lower bounds except in case of capture conversion (since it shouldn't be necessary to do so). Anyway, that's related to the lower-bound problem discussed above. I'm more interested in the moment in the upper-bound problem.
• I notice that receiverType is UnspecBounded<T*>. (Again, the "T*" formatting obscures that there's also an unspecified lower bound, but let's continue to set that aside.) I would want it to be just UnspecBounded<T>: We're uncertain about a lot of things in null-unmarked code, but we're sure that the enclosing object is an UnspecBounded<T>, even though we don't know anything about the bounds of T with certainty. Our fork has some special code to make that happen. (I didn't include that code in my list above because I had written it off as part of "defaulting for type-variable usages," which eisop now otherwise solves for us.)

I'll keep stepping through things, but that seems like a large enough dump of information for its own post :)

[cpovirk]

memberTypeWithOverrides ends up the same as memberTypeWithoutOverrides because applyFakeOverrides and applyRecordTypesToAccessors aren't relevant here, nor is methodFromUsePreSubstitution (I think; it seems to be about @PolyNull), and there's no viewpointAdapter.

So the step where something goes wrong is AnnotatedTypes.asMemberOf (unless it turns out that the problem getAnnotatedType(methodElt) result is enough to explain things already). We can narrow that further to asMemberOfImpl and then to substituteTypeVariables.

(Note that for these calls, we have a receiverType of UnspecBounded<capture#648 of ? extends Lib>. That receiver is fine; it's the receiver "of the original declaration" that I've been worried about.)

We end up with mappings containing a mapping from T to capture#648 of ? extends Lib. Good. So the problem must lie inside substitute (or, again, in the much earlier receiverType).

OK, AnnotatedTypeCopier.visitExecutable copies the receiver type from the "original"—which is to say the receiver "of the original declaration" to the copy that we will eventually return. I was momentarily confused at what is conceptually going on there, but I think it's explained quite well by "receiver type": This is presumably where receiver-parameter type-argument annotations would be relevant. (And this relates to our past discussions about whether, in a world in which JSpecify supports receiver-parameter type-argument annotations, every call to a method declared on a null-unmarked generic class would be an error in a strict mode, since that method might have been "meant to have" receiver-parameter type-argument annotations.) So I think there is conceptually sense in copying these annotations; we just haven't embraced receiver-parameter type-argument annotations in JSpecify. (I'd still have to think more about how such annotations should affect the output of substitution, but I won't do that now.)

So I do I think that the earlier receiverType problem is enough to explain what I'm seeing. I will look at how hard it would be to insert special logic into eisop similar to what we have in the fork. (It would be good if this also were to solve the null* problem, but I haven't thought about whether to expect that.)

[cpovirk]

Just as my comment in the "special code" linked above suggests that an isDeclaration() check is insufficient, so too do I gather that the isDeclaration() check in eisop is insufficient. I'll poke around in there a bit. (I had also tried commenting out a few if (shouldBeAnnotated) { addAnnotation } blocks that looked potentially relevant, but (as expected) that did not solve the problem.)

[cpovirk]

Perhaps applyDefaultsElement can say "If annotationScope is a ClassSymbol (/TypeElement), then preemptively apply the parametric qualifier (if there is one) to any type arguments (while still letting normal defaulting apply to everywhere else, including anywhere that type variables might appear)?" I'm hoping that that would affect only declarations and not usages, but I'm not sure. We could always try applying the rule further up, such as in addComputedTypeAnnotations, but that seems harder, especially if we have to worry about both the Element overload and the Tree overload?

[cpovirk]

Wait, it looks like we don't have a call for the ClassSymbol in that case, just for the method? I think I made this or a similar mistake before. (Not that I'd totally rule out that we at least sometimes use a cached value from when we did look at the class declaration.) We're just looking at the receiver type along the way. Maybe the simplest thing is to short-circuit annotating the receiver type at all (maybe by overriding visitExecutable to never visit getReceiverType()?), as I should perhaps have realized a while back? It's possible that that will cause other problems, but maybe we can arrange a way to let us "turn off receiver parameters" entirely?

[cpovirk]

My override of visitExecutable didn't solve the problem. I guess it's possible that I need multiple fixes, so I should have looked into stacking them.

Maybe I can handle it in typeAnnotator (since the reference checker already provides our own) before the defaults even come into the picture?

But maybe all this would be too general, given that addComputedTypeAnnotations (which is what uses typeAnnotator and the other code under discussion) is also used by postDirectSuperTypes, where presumably we want defaults to apply? In other words, thanks to that case, we might have a ClassSymbol even if we're not looking at the class declaration, only a usage. But I'm very confused about this whole system. Who knows how much of what we compute gets cached and reused elsewhere?