Handling of declaration annotations in JSpecify mode

[msridhar]

General question, mostly for @msridhar, because I forget context: Did we decide whether JSpecify rules apply only to type use annotations or do they apply to any annotation kind as long as we are on JSpecify mode? I remember the discussion as fairly involved and subtle, but whichever one we chose, either the title or description of this PR are wrong (title says "Type Use", description makes no mention of the distinction). @msridhar I believe we said for consistency the new rules would apply to any nullability annotation, type use or not, so long as JSpecify mode was enabled? (Otherwise it might be too confusing for devs and codebases with mixed JSpecify and javax annotations should be avoided, auto-migrated, anyways...)

Hrm, I see the issue. I think what we wanted was that for JSpecify mode, we would only recognize top-level type annotations in the "right" place for arrays. But, I realize now that with this PR, we are only checking type use annotations. If someone writes @Nullable String [] foo where @Nullable is a declaration annotation (like from javax.annotation) I think we'll still pick it up as applying to the top-level type. (@armughan11 we should add a test for this.)

I'm not sure what we should do about this. It is very confusing that one could write @Nullable String [] foo in two different parts of a code base and have it mean different things depending on whether the imported @Nullable annotation is declaration vs type use. But, if we decided to just ignore declaration annotations on array variable declarations in JSpecify mode, the same problem would still be there. So maybe the approach of this PR is no worse than the alternative? Hrm, or maybe we should (eventually) add a NullAway warning in JSpecify mode for any use of an old-style declaration @Nullable annotation? @lazaroclapp thoughts welcome :-)

And later response from @lazaroclapp:

Hrm, or maybe we should (eventually) add a NullAway warning in JSpecify mode for any use of an old-style declaration @Nullable annotation? @lazaroclapp thoughts welcome :-)

I think this might end up being the safest bet. The other alternatives are: a) inconsistent semantics for @Nullable seemingly only dependent on the annotation FQN, or b) "ignored" @Nullable declaration annotations (guess not ignored per-se, they would just apply to the elements, no?).

Maybe (b) is still better, with the caveat that we really want to flag it as a problem for the developer if they have such mixed annotation types at all... (i.e. any javax... nullability annotation when running on JSpecify mode. Either way, I am fine with those semantics being outside of the scope of this PR.

Originally posted by @msridhar in #850 (comment)

[msridhar]

I think this might end up being the safest bet. The other alternatives are: a) inconsistent semantics for @Nullable seemingly only dependent on the annotation FQN, or b) "ignored" @Nullable declaration annotations (guess not ignored per-se, they would just apply to the elements, no?).

Maybe (b) is still better, with the caveat that we really want to flag it as a problem for the developer if they have such mixed annotation types at all... (i.e. any javax... nullability annotation when running on JSpecify mode.

I think the tricky thing about (b) from an implementation standpoint would be that we'll need a separate code path in the array access support to find declaration annotations and treat them the same way we would treat a type-use annotation on the array element. I'm not sure how ugly that will be. As of now, I'm probably most in favor of warning on any use of declaration @Nullable annotations in JSpecify mode, or at least warning about any confusing use of a declaration annotation (like on an array type). But probably we should think more about the implications here.