Fix lower bound of type variables and unspecified subtypes.

[wmdietl]

Depends on #173 to make sure tests actually run.

The difference is in 651689e

Fixes #172.

There are some changes on the sample output, but many of these are "_but_expect_error" and that error no longer shows up. I still need to look through the other changes, but will wait until the other PRs are merged, in particular also jspecify/jspecify#505.

[wmdietl]

The order of TypeUseLocation enums matters and they are applied in declaration order.
I think what is happening is that the IMPLICIT_LOWER_BOUND default is applied first and then the TYPE_VARIABLE_USE has nothing left to do.
The inconsistency between the two constants is confusing anyways, so I think it makes sense to move this here.

I've filed eisop/checker-framework#741 to think more about this.

[cpovirk]

On eisop/checker-framework#741:

Ah, I do remember issues with the ordering, now that you mention it, probably as documented here:

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

Lines 843 to 847 in fae43cf

	* OTHERWISE covers anything that does not have a more specific default inherited from an
	* enclosing element (or, of course, a more specific default that we set below in this
	* method). If this is a @NullUnmarked element, then it might have a had a @NullMarked
	* enclosing element, which would have set a default for UNBOUNDED_WILDCARD_UPPER_BOUND. So
	* we make sure to override that here.

(And of course this is what the "Ensure that all locations that appear in the defaultLocations" comment above is saying, too. So I'm not saying anything new here :))

In that case, I wanted to override a specific location's value from an enclosing type with a general value at a smaller scope. As a result, I had to also override the specific location's value.

Here, I think we're talking about two values at the same scope, and the overlap is a Venn diagram: Some implicit lower bounds are type-variable uses, and some type-variable uses are implicit lower bounds. (In my case, by contrast, "every UNBOUNDED_WILDCARD_UPPER_BOUND was an OTHERWISE," so to speak.)

I say all that because a possible solution to my problem was to give priority to defaults from smaller scopes. Here, though, that wouldn't help, assuming that I've understood correctly.

---

On this PR more generally:

I would have guessed that there were two separate defaulting steps: one for the lower bound of E and one for the use of E itself. And my thinking is that minusNull is right for the lower bound but that unspecified is right for the use. Is the problem that, once the defaulting system defaults the lower bound, it decides not to default the use of E itself? Does the entire idea of defaulting those two things separately indicate that I'm working from a different mental model than the Checker Framework does?

That's probably it? This may get back into how substitution works differently (currently!) in the Checker Framework and JSpecify: Once the Checker Framework has an annotation for the use of a type variable, I think it applies that annotation to both of the bounds there? In contrast, JSpecify would say that "E" has a lower bound of minusNull but that "this use of E" has unspecified nullness.

(So, backing up to the eisop question for a moment: It's probably not worth trying to accommodate this case unless we decide that we want to keep the JSpecify behavior as it is—and maybe not even then.)

So this seems in line with the other hacks I've put in as part of forcing the weird JSpecify substitution behavior. It might result in slightly weird error messages by our standards (with null* instead of null)—still only when errors are triggered by some separate, real problem—but that's exactly the kind of thing that we can live with. And it may go away as we revisit substitution.

[wmdietl]

This is needed for the NullMarked use in Issue172<Object> p. The type argument needs to be "above" the lower bound and "below" the upper bound. Both bounds are unspecified, but apparently unspecified is no subtype of non-null.
Do you see a more proper fix for this?

[cpovirk]

tl;dr See "My implementation suggestion is this" below. It makes the same change but restricted to null types. We can revisit when we discuss JSpecify's odd substitution behavior again someday.

Dumping details here:

/tmp/tmp.zQJso3R0U8/jspecify-reference-checker/tests/regression/Issue172.java:33:Error: (type.argument.type.incompatible) incompatible type argument for type parameter E of Issue172.
void foo(Issue172<Object> p) {}
                  ^
found   : Object
required: [extends Object* super null*]

Seemingly null* is not a subtype of Object, even in lenient mode. I am now trying to decide whether that makes sense or not....

I think we've seen null* rarely. So we might just not handle it well.

Continuing to think this through in too much detail for a PR comment:

@NullUnmarked
<T> T unspecify(@Nullable T t);

s = unspecify(null);

At that point, I'd expect s to have type null*. Or really, it would have some type that depends on the declaration of s. So if it were a field String s in @NullUnmarked code, then we'd see T inferred to be either String or String*, and the result of the call to unspecify would be of type String*.

I wonder if there is actually any scenario in which we'd see null*? I feel like I once long ago ran all our tests to look for null* in the error messages, and I don't remember whether I found any. Hmm, but I'm pretty sure that I see null types sometimes in the javac APIs, so it probably does come up, at least for types of expressions (though probably still not variables, etc.).

It's weird... if there is no type information available for some call to unspecify, then I think(?) that method can't really fulfill its contract when someone calls unspecify(null)—except by returning null. So there is some sense in not going to any effort to make a null* type behave any differently than null?.

But null* probably can already behave differently than null? in at least some cases, since the latter is always null-inclusive. And clearly null* means neither "the bottom type" nor "null" but some sort of ambiguous state, which might also arise in other ways besides what we've seen here. So I guess null* probably should be a subtype of Object in lenient mode?

Or maybe it still shouldn't? If I tweak my unspecify example above to declare its type parameter as <T extends @Nullable Object>, then, if we infer a null type, then that might make more sense to treat the return type like "T*, where T is still potentially a nullable type?" But now we're back into the weird JSpecify substitution behavior (under which T* can "become nullable" after substitution), so I'm going to get off that train of thought now.

All that I think really need to do here is to get things working, ideally with some general understanding of what we're doing: The checker is already full of as many unprincipled hacks as I could cram in, and I'm OK with that if I feel like I'm learning something. So let's make these tests pass.

My implementation suggestion is this: Change IS_DECLARED_OR_ARRAY to IS_DECLARED_OR_ARRAY_OR_NULL (and IsDeclaredOrArray to IsDeclaredOrArrayOrNull). The "actual" code change will be to add || t.getKind() == NULL to the end of the conditional. Then the check in isNullExclusiveUnderEveryParameterization will do the "right" thing, and we won't need the change here.

The advantage to that, aside from requiring slightly less code, is that it preserves the (again, questionable) JSpecify substitution behavior. For example, it lets the following code remain an error:

interface Foo<E extends @Nullable Object> {
  E e();
}

@NullMarked
class Bar<E extends @Nullable Object> {
  Object o(Foo<E> foo) {
    return foo.e(); // `E*` is not compatible with `Object` even in lenient mode
  }
}

Hopefully that will give you fewer changes in samples behavior to sort through.

[cpovirk]

I have successfully talked myself into liking my implementation suggestion's special case a lot more than I did before.

My claim above was that the checker might analyze an unspecify method and conclude that the method could transform null? into null*—and that that seemed like a promise that it could never fulfill.

But in hindsight, there's an obvious way to fulfill that promise: unspecify just needs to behave like requireNonNull! Such a method is transforming null? into null (to put it in the checker's current format), the bottom type. (I wouldn't be shocked if requireNonNull(null) is considered by our checker to have the type null as things stand today, at least in some contexts. Not that I'd expect to see that particular code—except in some tests of requireNonNull or tools' handling of it!)

And I think I should have reached a similar conclusion by focusing more on pure theory: If I focus on null as the bottom type, which has no values, then clearly it is a subtype of everything. And if null* might "really be" null, then it, too, might be a subtype of everything.

Basically, I had been viewing the existing handling of declared types and array types as the "special case," when in fact they're no different from the null type. Arguably the true "special cases" are those in which we need to "look through" types to their components, as with intersection types, type variables, and wildcards.

(This might actually call for a spec update....)

[cpovirk]

Lots of text below as I try to understand how my hacks are holding up. But this LGTM with a slight implementation change.

[cpovirk]

On eisop/checker-framework#741:

Ah, I do remember issues with the ordering, now that you mention it, probably as documented here:

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

Lines 843 to 847 in fae43cf

	* OTHERWISE covers anything that does not have a more specific default inherited from an
	* enclosing element (or, of course, a more specific default that we set below in this
	* method). If this is a @NullUnmarked element, then it might have a had a @NullMarked
	* enclosing element, which would have set a default for UNBOUNDED_WILDCARD_UPPER_BOUND. So
	* we make sure to override that here.

(And of course this is what the "Ensure that all locations that appear in the defaultLocations" comment above is saying, too. So I'm not saying anything new here :))

In that case, I wanted to override a specific location's value from an enclosing type with a general value at a smaller scope. As a result, I had to also override the specific location's value.

Here, I think we're talking about two values at the same scope, and the overlap is a Venn diagram: Some implicit lower bounds are type-variable uses, and some type-variable uses are implicit lower bounds. (In my case, by contrast, "every UNBOUNDED_WILDCARD_UPPER_BOUND was an OTHERWISE," so to speak.)

I say all that because a possible solution to my problem was to give priority to defaults from smaller scopes. Here, though, that wouldn't help, assuming that I've understood correctly.

---

On this PR more generally:

I would have guessed that there were two separate defaulting steps: one for the lower bound of E and one for the use of E itself. And my thinking is that minusNull is right for the lower bound but that unspecified is right for the use. Is the problem that, once the defaulting system defaults the lower bound, it decides not to default the use of E itself? Does the entire idea of defaulting those two things separately indicate that I'm working from a different mental model than the Checker Framework does?

That's probably it? This may get back into how substitution works differently (currently!) in the Checker Framework and JSpecify: Once the Checker Framework has an annotation for the use of a type variable, I think it applies that annotation to both of the bounds there? In contrast, JSpecify would say that "E" has a lower bound of minusNull but that "this use of E" has unspecified nullness.

(So, backing up to the eisop question for a moment: It's probably not worth trying to accommodate this case unless we decide that we want to keep the JSpecify behavior as it is—and maybe not even then.)

So this seems in line with the other hacks I've put in as part of forcing the weird JSpecify substitution behavior. It might result in slightly weird error messages by our standards (with null* instead of null)—still only when errors are triggered by some separate, real problem—but that's exactly the kind of thing that we can live with. And it may go away as we revisit substitution.

[cpovirk]

tl;dr See "My implementation suggestion is this" below. It makes the same change but restricted to null types. We can revisit when we discuss JSpecify's odd substitution behavior again someday.

Dumping details here:

/tmp/tmp.zQJso3R0U8/jspecify-reference-checker/tests/regression/Issue172.java:33:Error: (type.argument.type.incompatible) incompatible type argument for type parameter E of Issue172.
void foo(Issue172<Object> p) {}
                  ^
found   : Object
required: [extends Object* super null*]

Seemingly null* is not a subtype of Object, even in lenient mode. I am now trying to decide whether that makes sense or not....

I think we've seen null* rarely. So we might just not handle it well.

Continuing to think this through in too much detail for a PR comment:

@NullUnmarked
<T> T unspecify(@Nullable T t);

s = unspecify(null);

At that point, I'd expect s to have type null*. Or really, it would have some type that depends on the declaration of s. So if it were a field String s in @NullUnmarked code, then we'd see T inferred to be either String or String*, and the result of the call to unspecify would be of type String*.

I wonder if there is actually any scenario in which we'd see null*? I feel like I once long ago ran all our tests to look for null* in the error messages, and I don't remember whether I found any. Hmm, but I'm pretty sure that I see null types sometimes in the javac APIs, so it probably does come up, at least for types of expressions (though probably still not variables, etc.).

It's weird... if there is no type information available for some call to unspecify, then I think(?) that method can't really fulfill its contract when someone calls unspecify(null)—except by returning null. So there is some sense in not going to any effort to make a null* type behave any differently than null?.

But null* probably can already behave differently than null? in at least some cases, since the latter is always null-inclusive. And clearly null* means neither "the bottom type" nor "null" but some sort of ambiguous state, which might also arise in other ways besides what we've seen here. So I guess null* probably should be a subtype of Object in lenient mode?

Or maybe it still shouldn't? If I tweak my unspecify example above to declare its type parameter as <T extends @Nullable Object>, then, if we infer a null type, then that might make more sense to treat the return type like "T*, where T is still potentially a nullable type?" But now we're back into the weird JSpecify substitution behavior (under which T* can "become nullable" after substitution), so I'm going to get off that train of thought now.

All that I think really need to do here is to get things working, ideally with some general understanding of what we're doing: The checker is already full of as many unprincipled hacks as I could cram in, and I'm OK with that if I feel like I'm learning something. So let's make these tests pass.

My implementation suggestion is this: Change IS_DECLARED_OR_ARRAY to IS_DECLARED_OR_ARRAY_OR_NULL (and IsDeclaredOrArray to IsDeclaredOrArrayOrNull). The "actual" code change will be to add || t.getKind() == NULL to the end of the conditional. Then the check in isNullExclusiveUnderEveryParameterization will do the "right" thing, and we won't need the change here.

The advantage to that, aside from requiring slightly less code, is that it preserves the (again, questionable) JSpecify substitution behavior. For example, it lets the following code remain an error:

interface Foo<E extends @Nullable Object> {
  E e();
}

@NullMarked
class Bar<E extends @Nullable Object> {
  Object o(Foo<E> foo) {
    return foo.e(); // `E*` is not compatible with `Object` even in lenient mode
  }
}

Hopefully that will give you fewer changes in samples behavior to sort through.

[wmdietl]

@cpovirk Your suggested alternative also fixes #172. I think there were fewer changes in _but_expect_error, but let's investigate those separately.

[cpovirk]

I think there were fewer changes in _but_expect_error, but let's investigate those separately.

Interesting. Separately SGTM, though, yeah.