Questions about cast expressions [working decision: only type components are nullness-applicable]

[kevinb9n]

For what kinds of usages within cast expressions would JSpecify annotations (@Nullable/@NonNull) be required/prohibited/optional?

JSpecify has a much higher priority to standardize how APIs are annotated than to do the same for implementation code. That seems to argue for leaving this tool-dependent. But, pre-1.0, it would seem smarter to at least attempt agreement first, and then back off if/when tool owners sufficiently protest.

So:

1. Can the root type of the cast type be annotated @NonNull? The user's goal must be to signal to an analyzer that an expression seen as nullable can't actually have a null value, so that it can be safely assigned to a non-null type (or, I suppose, dereferenced). But there seem to be plenty of good ways to do that already: a conditional, an assertion, passing it through checkNotNull, or suppression. (Plus a less-good-but-okay option too: passing it through a method like uncheckedCastToNonNull which just returns its argument.) Plus, even if it was legal, it should generate a warning anyway, by analogy with (T) o -- both violate the expectation that (non-widening) casts are fully validated at runtime. So little is gained by allowing it.

2. Can the root type in the cast expression be annotated @Nullable? As a widening cast... where would this ever be needed? Perhaps for some type inference scenario?

3. When the user is casting "anyway" (i.e. from one base type to another), should the appropriate non-root usages of @Nullable (i.e., that you expect in the resulting type) be mandatory/explicit, or optional but inferrable, or prohibited and only inferred? (Or heaven forbid, ignored and only inferred?) My first question is whether they always can be inferred. Mandatory/explicit also helps preserve the general notion that "string means string".

3b. If 3 is answered mandatory or optional, how are these to be validated?

4. Would we allow casting a base type to itself, altering only the nullness of type arguments? One argument, which might be flawed (?): either the cast is widening and thus unnecessary, or it's not and thus would need to produce a warning anyway. So what has been gained by the cast? And again, casts "should" be a visual suggestion that something is being validated at runtime.

[kevinb9n]

Looking for feedback from tool owners @msridhar @lazaroclapp @wmdietl @artempyanykh @akozlova. I expect library owners to not care strongly about this one.

[msridhar]

I personally don't have a strong opinion here right now. We don't currently support such casts in NullAway and I don't immediately see why we would need to. Something might arise in the context of generics support; other tool owners can comment on that. If at the spec level we are going to prohibit @NonNull on locals, maybe it makes sense to do the same on casts as well.

[kevinb9n]

@msridhar I can see not supporting 1/2/4, but the way 3 is worded, one of the approaches listed must apply to you, I think. Which is it, I'd be curious to know? Same for other tools.

[msridhar]

@msridhar I can see not supporting 1/2/4, but the way 3 is worded, one of the approaches listed must apply to you, I think. Which is it, I'd be curious to know? Same for other tools.

Sorry, I'm having a hard time following 3, could you give a code example?

[kevinb9n]

Surely.

Iterable<@Nullable Map<String, @Nullable Integer>> it = ...;
if (iterable instanceof List) {
  doSomethingWith((List<__??__ Map<String, __??__ Integer>>) it);
}

We don't worry about the nullness of the list itself; an analyzer knows it to be non-null inside the if, and even if it didn't it would just carry over what it knows about the nullness of it.

It seems we want the result of the cast to have the type List<@Nullable Map<String, @Nullable Integer>>, since per # 4 above we wouldn't allow altering the nullness information only, so why let it "ride along" with a base-type cast.

And if that doesn't suitably match doSomethingWith's parameter type, we expect a nullness warning, which might be suppressed.

But the question is:

• is it mandatory that the user repeat the nullness annotations (exactly) in the cast type itself (insert @Nullable for each __??__)
• or must they be omitted and automatically carried over from the input type (remove both __??__)?
• or something in between?
• or some weirder rule?

Pro-mandatory: we're training users to see Foo<Bar> as meaning "foo of non-null bar" and this would become an unnecessary exception to that.

Pro-optional: this is a case where nullness information does not need to be declarative, it's fully inferrable.

I could be misunderstanding things, of course.

[artempyanykh]

Perhaps I'm failing to see some angle specific to casts here, but the question about casts in my head is closely related to variable declarations and method calls where we also need to decide 'when we infer and when we don't'.

What we settled on is the following:

1. We try to infer types only in situations where Java would do the inference too; so diamonds and generic method calls without explicit type args.
2. We ignore root-nullness on locals. IF Java had var declarations sooner we might have reconsidered this; but this train is long gone.
3. Explicit type arguments are treated as 'augmented', iow. a user is expected to specify the nullness they need as it won't be inferred.

For instance,

List<String> ls = List.of("Hello", null);

1. On RHS we have a generic method without type arguments; we do infer its type based on formal args as List<@Nullable String>.
2. On LHS we have a variable declaration, so the type of ls is List<String>.
3. Because List<@Nullable String> is not a subtype of List<String> we generate a warning about an unsafe assignment.

We treat casts the same way.

On the subject of possibility of inference: in our experience Java's "target typing" makes inference really hard in certain situations; at least it doesn't play nicely with the kind of forward analysis of CFG we use in Nullsafe. This is another reason why we treat explicit type declarations as the source of truth.

[msridhar]

We haven't dug into this in as much detail as @artempyanykh but I am 100% in favor of decisions that do not make the difficult inference problem even more so. So I'm on board with requiring repetition of nullness annotations in casts.

[kevinb9n]

I think I have some new clarity on what I'm really driving at here.

The hope: to keep things simple for users, ideally, all type usages will be neatly classifiable (by simple rules) into just one of these two buckets:

• Nullness annotations are applicable. Here, @Nullable always means nullable, @NonNull always means non-null, and "neither annotation" means... whichever of unspecified/parametric/non-null applies from context. (I think this equates to the phrase "treated as augmented" above.)
• Nullness annotations are inapplicable. Here, @Nullable/@NonNull are deemed irrelevant/unrecognized (or redundant), and a surrounding @NullMarked has no impact. JSpecify "has nothing to say about nullness" in these cases.

I'm aware of these inapplicable cases only:

• categorically non-null type usages (including usages of primitive types)
• local variable root types
• any part of a receiver-parameter type

The "hope" (above) is that we can complete that list and then make the applicable cases list be:

• everything else

This issue and #261 are runs at this goal; I want to nail down which bucket they go in, or whether a new third bucket is forced.

---

I think these original questions are both answerable "no":

1. Can the root type of the cast type be annotated @NonNull?
2. Can the root type in the cast expression be annotated @Nullable?

I will claim that this "no" is in fact already explained by the list above, because the type in a cast expression qualifies as a "categorically non-null type usage". (Sure, the expression will cast null to null, but that's just its standard behavior; the type "operand" in the expression has no bearing on it.)

So it's down to the non-root type usages in the cast expression.

I'm not sure there's any useful or meaningful way that you can "alter" these nullness bits between the from and to types. If you tried to alter any annotation between the from and to types, I suspect this is either safely "widening", so you shouldn't need to cast; or not widening, so casting only trades one warning for another anyway.

(widening example: casting from Comparator<? super @Nullable String> to Comparator<? super String>)

So our choice is maybe between:

• All these type usages are "nullness applicable" and you must annotate them as expected (though you have little choice in the matter).
• All these type usages are not "nullness applicable" and you may not annotate them; what is known about the source type will carry over.
• The dreaded new third bucket.

---

Aside: every time I come back to this and #261 and get myself confused again, I try again to persuade myself that we can just throw up our hands and say "it's implementation code, we don't have to care". But, it would feel a lot better if we were leaving things undefined to accommodate genuine disagreements between the priorities of different tools, and not just because someone got too confused when trying to discuss the issue at all. :-) So, I am trying to hold fast to what I said here:

JSpecify has a much higher priority to standardize how APIs are annotated than to do the same for implementation code. That seems to argue for leaving this tool-dependent. But, pre-1.0, it would seem smarter to at least attempt agreement first, and then back off if/when tool owners sufficiently protest.

[kevinb9n]

So it's down to the non-root type usages in the cast expression.

So who would support this option?

• All these type usages are "nullness applicable" and you must annotate them as expected (though you have little choice in the matter).

Most casts would provide exactly the expected annotations, but by making them be specified explicitly, the code won't be misleading. Some casts might alter them in safe ways that don't need a warning -- this sees like a real edge case, but maybe it could help with type inference in cases? Lastly, most variations of the annotations should produce a warning; as far as I know, it could still be that the cast helps with type inference somehow.

[cpovirk]

(Sounds good!)

maybe it could help with type inference in cases

Ah, I thought I had done a search for this before, but it looks like I hadn't. Here's some code in Guava:

return ((Comparator<@Nullable Object>) comparator).compare(o1, o2);

I want to say that @Nullable is necessary there: I don't think normal Java type inference can "look ahead" to the subsequent call to compare, as it would need to do to figure out that the comparator needs to be a Comparator<@Nullable Object> rather than a Comparator<Object>. (This is the same reason we need to write things like ImmutableMap.<Foo, Bar>builder().put(foo, bar).)

That said... the way we usually do that is indeed the "trading one warning for another" scenario:

SortedSet<@Nullable Object> self = (SortedSet<@Nullable Object>) this;

That is, we extract a local variable so that we can localize the @SuppressWarnings. Once we've done that, the cast expression has a clear target type (hopefully my terminology there is reasonable?), so an analyzer could reasonably be expected to infer the @Nullable in the cast type.

[kevinb9n]

While I'd still be happy to hear from @wmdietl @artempyanykh @msridhar and others, I think we can consider this working-decided for now.

In a cast expression, the root type is "nullness-inapplicable" and other component types are "nullness-applicable", as explained 3 comments up.

[artempyanykh]

Somewhat belated, but I'm in favour of the current working decision 👍

[kevinb9n]

Let me propose a slight restatement:

On non-root type components, which as decided here are nullness-applicable, their nullness (?, !, %, *) can differ from what would otherwise have been inferred, and an analyzer can use that new information. It's only that the analyzer should also produce a finding in that location [edit: at least, if the type was made more specific]. (The user might suppress that finding, and that seems like a valid enough way for them to alter the nullness.)

Of course, I still maintain that it's not sensible to permit this on the root type at all, as there is a reference-or-lack-of-reference sitting right there that can simply be checked. I am still happy about cleanly defining such locations to be nullness-inapplicable.

[netdpb]

Current decision: @Nullable and @NonNull are applicable to non-root type components of local variable declarations and cast expressions.

Argument for changing: No strong case.

Timing: This must be decided before version 1.0 of the spec.

Proposal for 1.0: Finalize the current decision. If you agree, please add a thumbs-up emoji (👍) to this comment. If you disagree, please add a thumbs-down emoji (👎) to this comment and briefly explain your disagreement. Please only add a thumbs-down if you feel you can make a strong case why this decision will be materially worse for users or tool providers than an alternative.

[kevinb9n]

FWIW, my last restatement had two parts and we only voted on the second part.