Ensure override compatibility with type variables

[wmdietl]

I want to look whether there is a better fix for this, maybe by moving this check into the override checker. Instead, maybe something is wrong with the logic in the return statement that follows this change. Let me know if this looks familiar.

Fixes #164.

[cpovirk]

Again, LGTM.

I will test this in the Google codebase and report back, but I don't think that even that is a blocker for merging. (If I discover that things somehow break as a result, we can always revert the commit :))

My next thought is that it does seem that this new case "shouldn't be necessary": nullnessEstablishingPathExists should find the "path" from T to T.

Ah, I wonder if somehow those are two different T types, as if the step of "adapting the formal parameter types of N to the type parameters of M" from JLS 8.4.2 is not being applied? That would be my guess: I seem to recall that the Checker Framework will let you override a supermethod <T extends Object> void foo() with a submethod <T extends @Nullable Object> void foo(), similar to how it allows parameter contravariance. Presumably that would require holding two different concepts of T in mind simultaneously when checking that any formal parameters have covariant types. (This is fresh on my mind because I was spreading FUD about it yesterday :)) So the Checker Framework may be checking overrides in a fundamentally different want than the JLS does... but I guess still delegating to isSubtype as part of that? I think that may line up well with my understanding of your fix. Or I could have any number of things totally wrong :)

Anyway, I've now talked myself into at least sort of having a theory about what's going on. And if that theory is right, your fix is probably the best we can do on the jspecify-reference-checker side. If so, it's still possible that something more can be done on the checker-framework side. But I wouldn't worry about it: There's still a decent chance that we end up redoing some of this code as a result of changes in design decisions and/or to make it fit more naturally into the Checker Framework model (instead of having this extensive isSubtype logic in jspecify-reference-checker at all).

[cpovirk]

It looks like I may be seeing fewer "incompatible parameter type" errors, albeit still not zero. It's a bit hard to tell how much of the reduction is because of #159 crashes that hide other problems, but clearly at least some of the reduction is real.

An example of a line on which I'm still seeing a problem is this one:

https://github.com/google/guava/blob/858caf425cdf3183776b61b437ba7a4129b6539b/guava/src/com/google/common/collect/MultimapBuilder.java#L472

Both the "found" type and the "required" type are "Multimap<? extends K, ? extends V>."

[cpovirk]

The remaining issue might be restricted to type parameters that extend other type parameters (and, similarly, wildcards that extend type parameters). Here's an example:

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

@NullMarked
class Issue164Continued {
  interface Super<T extends @Nullable Object> {
    <U extends T> void foo(Lib<? extends U> lib);
  }

  interface Sub<T extends @Nullable Object> extends Super<T> {
    <U extends T> void foo(Lib<? extends U> lib);
  }

  interface Lib<T extends @Nullable Object> {}
}

$ ./demo Issue164Continued.java
Issue164Continued.java:11: error: [override.param.invalid] Incompatible parameter type for lib.
    <U extends T> void foo(Lib<? extends U> lib);
                                            ^
  found   : Lib<? extends U>
  required: Lib<? extends U>
  Consequence: method in Sub<T>
    void foo(Lib<? extends U>)
  cannot override method in Super<T>
    void foo(Lib<? extends U>)
1 error

It's a rare enough problem that I'd feel OK with adding suppressions for it. (I could believe that a proper fix would involve more areCorrespondingTypeVariables+isSubtype checks recursively on the bounds when the bounds are themselves type parameters.)

[cpovirk]

(Well, I guess we'll see how common it really is after the crashes are gone. Maybe it's worse than I think.)

[cpovirk]

At a higher level:

• In addition to helping with various cases, this PR doesn't make anything worse (as far as I can tell).
• If we merge it, and if we then find a fix for #159, and if nothing new breaks at that point, and if the crashes from #159 aren't hiding anything big, then I think we'd be ready to switch Google over, as the problems I reported above and in #172 appear to be minor.
• To get a preview of all that, I applied the hacky checker-framework patch from my comment on #159 to silence the crashes. I didn't notice any new kinds of errors, and the level of errors does appear tolerable. (And I encountered at least a couple errors that were legitimate (if probably harmless), too!)

[wmdietl]

@cpovirk Thanks for the additional test! The override checks seem a bit odd, but let's not try to fight them now. Adding an additional check for the subtype type variable being captured, in https://github.com/jspecify/jspecify-reference-checker/pull/171/commits/9421ef85843ad589c578c721aa35731fd6b90cc2, fixed the additional test and doesn't change the conformance results.

I like using different type variable names for different type variable declarations. That makes it easier to see in messages that it is looking at different types. The areCorrespondingTypeVariables check makes sure the different TVs from the two methods correspond.

If this is producing okay results, I would propose merging and cleaning up the CF interaction and wonkiness separately.