Handling of type-use annotations on type variables

[kevin1e100]

Issue #45 brought up the idea of sometimes "ignoring" type-use annotations on type variables, or more precisely, union-ing them with other factors when parameterizing generic classes (which effectively means only @Nullable will be fully honored). This affects issues #45, #89, and #90, so trying to split this question out.

[cpovirk]

@kevin1e100 in #89:

If we're right that "projecting" to non-null isn't really a thing then uses of @NonNull T today are probably attempts at specifying a generic class with non-null-only type parameter, e.g., Optional or ImmutableList, where @NonNull(unlessTypeArgumentPermits = true) T is identical to a straight non-null projection (assuming T is declared as <T extends @NonNull Object>). The main concern is probably just that it would seemingly likely surprise users that @NonNull T is not necessarily non-null. But if annotating generic classes is a 5% case, and doing so without default annotations but with nullable type parameters is even rarer, then maybe it's ok if the ergonomics aren't completely clean.

That's a good point.

Here are 2 more things that might help us feel better about making @NonNull T not project to non-null:

FIrst: One of the things I've said against making @NonNull T project to non-null is that it's often used unnecessarily: Instead of marking a type-parameter bound as @NonNull, someone instead annotates every usage of the type. The result is something like this:

class ImmutableSupplier<T extends @Nullable Object> {
  final @NonNull T value;

  ImmutableSupplier(@NonNull T value) {
    this.value = value;
  }

  @NonNull T get() {
    return value;
  }
}

But! I think the main reason that we've seen this historically is that the Checker Framework treats class ImmutableSupplier<T> as having a nullable bound. That is, no one actually writes "class ImmutableSupplier<T extends @Nulllable Object>" for such a class. We, conversely, appear likely to interpret class ImmutableSupplier<T> as having a non-null bound (though of course that discussion is still underway)[1]. So, if users write the simple thing, their code will Just Work, and they'll never get into the business of spraying @NonNull everywhere in an attempt to make the errors go away[2].

Second: If we can encourage tools to follow my "Foo means Foo" rule, then they're likely to display @NonNull T as just plain T. (An unannotated T, then, would be T! or something.) Of course that doesn't help users who are looking at the source or at HTML Javadoc. But it may help in error messages, tooltips, etc.

[1] If we do indeed give it a non-null bound, it will be largely because Java has "forced" our hand by making <T> and <T extends Object> indistinguishable in bytecode. Without that constraint, we may well have gone the other direction. I guess it's nice that we're seeing another advantage of the non-null bound. I guess this one falls under the umbrella of "limiting parametric nullness."

[2] For fun, try an internal search like the following: @NonNull\s+[A-Z]\b[^{};]*@NonNull\s+[A-Z]\b[^{};]*@NonNull\s+[A-Z]\b case:yes lang:java pcre:yes. Much of what you see there, to be fair, is a result of the Checker Framework's treatment of a type parameter definition of the form <@NonNull T>, which ends up equivalent to plain <T>.

[cpovirk]

(I just realized that this thread is possibly part of #13. I don't have much opinion about whether to discuss here or there.)

@kevin1e100 mentioned earlier today that we haven't revisited early decisions about the specific case of @NullnessUnspecified T. (I had forgotten that I'd started that in #74 before -- for better or for worse -- merging that into #45.)

We're talking especially about the following class...

class Foo<T extends @Nullable Object> {
  @NullnessUnspecified T bar();
}

...with the following instantiations...

Foo<@Nullable String> nullable;
Foo<@NullnessUnspecified String> unspecified;
Foo<@NonNull String> nonNull;

The question is: What does bar() return on each of the objects?

I think that the current proposal says @NullnessUnspecified String in all 3 cases.

Note that the current proposal has different treatment for a similar (and much more common) case:

[@DefaultNullnessUnspecified]
class Foo<T> {
  T bar();
}

For that case, the proposal gives nullable.get() a return type of @Nullable String and the other two instantiations a return type of @NullnessUnspecified String.

I think we should apply that behavior to the first case, too: Our certainty about the nullness of the bound for T shouldn't say anything about our certainty about the nullness of the usages of T. (previously)

This fits with the idea that @NullnessUnspecified means "Either @Nullable should be here, or it shouldn't"[*]. (See also another example of applying that model.) Based on that, we can figure out what result we want for the substitution by looking at both cases and applying our current rules for parameterized types:

• If @Nullable is there, then the return type is @Nullable String.
• If it's not, then the return type is just String.

The result of "@Nullable String or String" gets represented as @NullnessUnspecified String.

Such a rule might also help replace the special rule for "assumed parametric nullability" with a general rule (though that depends on other decisions).

[*] This assumes that the file is @DefaultNonNull. If it's not, then it's necessary to first "convert" it from @DefaultNullnessUnspecified to @DefaultNonNull file by "pasting" @NullnessUnspecified onto every unannotated type usage in the file.

[kevinb9n]

Note that I split out the requirements question of whether non-nullable type projections are needed as #86.

(I think we could use more clear separation between requirements and design questions.)

[cpovirk]

I think the discussion here is less over whether it's needed -- I think @kevin1e100 and I, at least, agree that it's not -- as to what to do when a user inevitable writes @NonNull T. Or maybe I'm misunderstanding you?

[cpovirk]

Oh, sorry, you're saying that the other issue is for use cases for "projections to types other than nullable," not "projections to the type non-null." So you're pointing out that we can discuss whether there's a requirement to project to unspecified, doing so on that other issue. That sounds fair. Let me see how I can split this, hopefully on Monday.

[edit: I've posted about projections to non-null and about projections to unspecified nullness.]

[kevin1e100]

Thanks for trying to shift what @Xxx T "should mean" here. I originally filed this issue based on the following assumptions:

• there are type-use annotations @NonNull, @Nullable and @NullnessUnspecified
• because we want to be compatible with standard javac, users will be able to place these annotations on type variables, e.g. @NonNull T

Then the question becomes, what should that mean? Some basic observations:

Case	Observations
@Nullable T	This has a lot of precedence in existing tools and is pretty clearly needed to get the nullable version of any allowed type argument. Kotlin writes this T?.
@NonNull T	Again, this has a lot of precedence in existing tools, where at least in checkerframework, IntelliJ, Kotlin, and Eclipse this is interpreted as the non-null version of any allowed type argument. Note, however, that it's redundant to do this if only non-null type arguments are allowed, and there don't seem to be a lot of compelling cases when nullable type arguments are allowed (see issue #4). Kotlin has no equivalent for this (the above behavior is about seeing the annotation in Java code).
@NullnessUnspecified T	No precendence here. It seems that one would want to use this, for instance, to not make Map.get outright nullable, or more generally, to exempt a particular type variable usage in a class annotated with @DefaultNonNull. @NullnessUnspecified conversely seemingly shouldn't be needed (on type variables or otherwise) when @DefaultNonNull isn't used.

The Map.get example suggests that with @NullnessUnspecified T, we'd probably want for that to become @Nullable Bar when T is substituted with @Nullable Bar and @NullnessUnspecified Bar for substitutions with other qualifiers, as was mentioned above. Issue #45 and issue #89 present arguments for similar treatment of @NonNull T: in that interpretation, type-use annotations on type variables are like a lower bound, i.e., if a type argument that's "more nullable" comes along, we just use the type argument's nullability.

But to me at least it still seems much more natural to think that @NullnessUnspecified T and @NonNull T would denote the so-annotated version of any type argument (regardless of whether we "need" that per issue #86). Existing tools seem to generally treat @NonNull T that way, and treating @NonNull T one way and @NullnessUnspecified T another also seems inconsistent/confusing.

I've been trying to figure out what the issue is. I think in part at least it has to do with the type-use annotations directly corresponding to conceptual "qualifiers" (called "effective nullability specifiers" in the proposal doc) on each base type usage, especially given that "refinement type systems" were a big motivation behind introducing type-use annotations into Java in the first place, IIUC. It seems very natural, then, for type-use annotations to "override" any qualifier on a given type argument.

None of this is supposed to contradict the observations made above and elsewhere that @NullnessUnspecified T and @NonNull T maybe should have a different meaning; but I at least feel nonetheless that that'll be difficult to "stomach".

One issue that particularly worries me is the potential inconsistency with existing spellings of @NonNull (i.e., existing annotations by that name) this would cause. Aside from confusion, an issue I worry about here is people migrating from other annotations to ours. It seems they'd want to just "change imports" assuming that any @Nullable and @NonNull annotations they already have will continue to mean the same thing. But that wouldn't be the case with @NonNull T unless the type parameter bound is also annotated, ie., class Foo<T extends @NonNull Bound>. Migration tooling could help with this. Also, if the bound annotation is missing, it's implicitly class Foo<T extends @NullnessUnspecified Bound>, so Foo<@Nullable Bar> could cause a warning, alerting users that something might be wrong. But we encourage tools to be largely silent on these unchecked conversions, so unclear if there would be warnings, and either way this seems prone to confusing and frustrating users. Specifically, I worry it could turn users off right as they try to use our annotations for the first time. And there don't seem very good choices here:

• we could choose a different annotation name, but users would seemingly just be confused by that also, still do a find-and-replace, and still get issues (aside from that being potentially obfuscating in general as was noted in issue [moved to #230] Decide whether to include a @NonNull annotation #4).
• we could make @NonNull T illegal (assuming issue Non-null projection of a type variable usage #86 lets us). That seems, if anything, worse: users just won't be able to adopt our annotations at all.
• there could be an attribute as mentioned in issue Annotating type parameters and type variables without using default annotations #89, but that again probably only makes sense if issue Non-null projection of a type variable usage #86 says there's a use case for both values of the attribute.

That all seems to say we should figure out issue #86, that is, whether non-null (and nullness-unspecified) "projections" should even be a thing. I've been carrying these thoughts for a while though, so I wanted to dump them before I lose them, especially since they seem to say that even if projections aren't "needed", making @NonNull T to mean anything other than a projection seems somewhat challenging, especially for users migrating from other annotations, even if it's semantically sane.

[wmdietlGC]

I'm not sure this is the best issue for this discussion, but as there was a comparison to CF behavior earlier, I wanted to highlight the following:

The Checker Frameworks makes the bound for j.l.Class @Nullable Object and then uses @NonNull T when using the type parameter. Why didn't we simply make the upper bound @NonNull Object?
I think the reason for this was the typical use case of Class as a type token, such as in:

<T> void foo(Class<T> type, T instance)

Here the default CF behavior makes T have a @Nullable Object upper bound. If Class had a non-null bound, the CF would complain about the type of type.
So the code would have to be rewritten as:

<T extends Object> void foo(Class<T> type, T instance)

making the upper bound non-null. Maybe parameter instance should now be @Nullable T.
As there is a lot of code like that, Class is implemented in the awkward way it is.

I'm not sure all cases with a nullable bound and non-null type variable uses are instances of #78, but that would seem plausible.

If we can continue to expand <T> to <T extends @NonNull Object> we will not run into this problem.

[kevin1e100]

So here's a "trick" that might deserve its own issue:

In the proposal doc there's "special consideration" for type arguments that was kind of inspired by wildcards, namely that any type argument is to be automatically "adjusted" to adhere to the corresponding type parameter's bound (similar to how Java intersects wildcard bounds with the wildcarded type parameter's bounds). The original motivation for that was ImmutableList in the context of DefaultNullable, and even though we abandoned DefaultNullable (for now, see #41) it still seems useful in @DefaultNullnessUnspecified contexts, and maybe to help with the issue you brought up here.

Namely, the motivation was for ImmutableList<String> to mean ImmutableList<@NonNull String> no matter what default. In particular, in @DefaultNullnessUnspecified contexts, ImmutableList<String> would presuably otherwise mean ImmutableList<@NullnessUnspecified String>, which is "fine" if we assume this parameterized type is allowed (which it is but using unchecked conversions), but it still seems unfortunate/undesirable to lose track of the fact that ImmutableList can only contain non-null elements, e.g., when iterating the elements, even in unannotated client code of ImmutableList. One might also argue that this rule creates more consistency between ImmutableList<String>, ImmutableList<? extends String>, and ImmutableList<?>: this rule makes it so all three forms preserve the knowledge that list elements are non-null, regardless of surrounding default.

Following this approach to the letter, the Class<T> example given above would work no matter what T's declared bound is: when used as a type argument for Class, it'll be restricted to non-null as desired (assuming Class declares T bounded to be non-null).

That seems to mean that this rule results in an implicit form of non-null "projection", now that I think about it, in the case where the type argument is itself a type variable. Something like that would happen in the example of an Optional field that came up as well:

class Foo<T extends @Nullable Object> {
  Optional<T> value; // would implicitly use T's non-null version if Optional requires it
}

Maybe that means this rule is problematic, if we don't believe projections should be a thing (#86). Or maybe it actually helps avoid awkward contortions in foo(Class<T> type, T instance), avoiding "needing" explicit non-null projections, and is therefore "working as intended"? (Leaving aside that there is a way of handling this case without projections as @wmdietlGC mentioned above, just maybe an in some cases unnecessarily verbose one.)

Again, the original motivation for this rule, @DefaultNullable, went away, where otherwise people would have to explicitly write ImmutableList<@NonNull String> everywhere, unless we use the same trick for ImmutableList that CF used for Class and Optional. It still seems nice to get non-nullness "for free" in some cases this way, but maybe that's also an anti-feature, as it could cause tool errors in unannotated files, conceivably (#77), though it's hard to imagine any of those errors would be "bad" in the case of ImmutableList at least. It's also apparently not something existing tools do, so could be an implementation challenge. And, of course, the rule is (largely) irrelevant with @DefaultNonNull, where type arguments other than type variables are implicitly non-null anyway. So maybe we should strike it, due to its weird interaction with type variables?

[kevin1e100]

A thought I had on the migration concern mentioned above: we could encourage tools to warn when they see @NonNull T on a type variable whose bound isn't also annotated. I feel like that's reasonable anyway and could help clue in users in particular if we decide that @NonNull T doesn't "project" potential type arguments to non-null.

[kevinb9n]

@cpovirk could you perhaps see whether there's some current action/decision we need to salvage from this historical discussion, and file that if so, and close this either way?

Note that we can assume there will be no @NonNull, i.e., if we do reintroduce that it will be clear we have to resurrect various closed topics then but short of that don't worry about it.

[cpovirk]

This should be pretty well covered (incidentally, even including the groundwork for @Nonnull).

For our current annotations, you can basically view it as the "unioning" approach discussed above, or you can view it as "what Kotlin does." If we introduce @Nonnull (or if you do something particularly unusual today), then some non-"unioning" behaviors can arise, again following what Kotlin does.

[cpovirk]

In an ideal world, I'd find some time to think about #91 (comment) again: If I recall correctly, the "special consideration" for non-nullable type parameters (also previously discussed here):

• complicates our reference checker's implementation
• doesn't match Kotlin (though even if it doesn't match now, we should check again after KT-59138). (But note that there is no exact equivalent to this in pure Kotlin code: You need to involve Java code in order to produce the out-of-bounds type argument. So I don't know how deeply the Kotlin folks felt they needed to think about this.)

On the other hand, I suspect that the "special consideration" catches some bugs. (I would like to have a more compelling example handy, but as an existence proof, it catches the bug in code that calls or(null) on a Guava Optional<String> even when that type is unannotated. Perhaps a better example would involve ConcurrentMap or something.) And I don't think that there's been much argument that that's an overreach (in contrast to, say, #248).

Now maybe there's a way to produce the same effect without hooking into substitution specifically. Like, maybe usages of T can be automatically treated like @NonNull T when appropriate. But that scares me because it's easy to imagine that a checker might enter infinite recursion if it naively tries to evaluate the nullness of T in class Foo<T extends Foo<T>>. [edit: And I believe that kevinb9n has suggested another approach, which is for usages like "Optional<String> in non-null-marked code" to be automatically treated as Optional<@NonNull String>." I think I've had similar concerns about infinite recursion there. Behind both concerns is the idea that this is a "layering violation": The question "What is the nullness specifier for this type?" should not depend on "What is the bound of this type parameter?" since the latter question already depends on the former. My hope is that it's safer for substitution rules to depend on the bound, but I haven't thought that through as deeply as I should.]

One worry would be that, without this "special consideration," it would technically become useful to write the "redundant" "@NonNull T" in place of plain "T" in order to catch bugs like the one discussed above.

In practice, probably most of the danger here comes from cases in which the type argument is unspecified, rather than nullable or parametric (since nullable or parametric would have already produced an error at the site of Optional<@Nullable Foo> or Optional<T>—unless those declarations came from unchecked code!). That at least means that it's clear that tools could choose to add their own rules to turn "unspecified" back into "non-nullable," especially if the only significant downside to doing so is checker complexity. (Contrast that to a rule that would change "nullable" to "non-nullable," which makes a lot of sense for something like dataflow but makes less sense when you're changing the parameter type of a public API to be more restrictive.)

(I do think that there may also have been an argument that it's nice to have the escape hatch of being able to write Foo<@Nullable String> (and get nullable types as a result) if you think that Foo bans nullable type arguments wrongly. However, I don't see that as a very strong argument, given that it's a workaround that works only for generic APIs. If we think that people need a workaround, then they'll need a workaround for non-generic APIs, too. (Typically that workaround is provided by suppression.))

[cpovirk]

There are some similarities here to other cases in which we've argued that non-null types are "special":

• They're the kind that make a guarantee (one that can even be enforced at runtime).
• They may someday sometimes be stored differently, thanks to Valhalla.

But I'm not sure if any such arguments are exceptionally strong in this particular case: If an API is generic, then I don't have a feel for what Valhalla might be able to do in the future. But it's not obvious to me that parameters and return values could be "flattened" in the way that fields can, at least until the type is specialized.

I still like the idea of catching bugs, like in the cases of Optional or ConcurrentMap above (or AutoValue, which automatically inserts null checks even for generic types by default). And I still like the idea that the type remains non-nullable no matter what you try to substitute in. My question is just whether our special consideration complicates implementation enough that we'd at least not choose to specify it, even if we'd encourage it. If we were going to change our tune, then the time to do so would be before "spec 1.0" and while we're getting back to our conformance tests.

(But I'd have to actually look more at our reference checker to see how large the complication is. It might be only #248 that really mucks things up.)