Forbid annotations on supertype

[aosen-xiong]

Fixes #1059. BaseTypeVisitor now reports annotation.on.supertype when a supported
qualifier is written on a supertype in an extends/implements clause. Only qualifiers
from the active checker are flagged, and at most one error is reported per clause.

The check lives in a new protected helper checkAnnotationOnSupertype(Tree), called
from checkExtendsOrImplements. Checkers that allow annotations on supertypes
(currently only the Tainting Checker) override this helper with an empty body.

Earlier iterations used a separate checkSupertypeAnnotations method, then a boolean
flag on checkExtendsOrImplements. Both conflated the annotation check with the
subtyping check; the dedicated helper keeps the two concerns cleanly separated.

[aosen-xiong]

@wmdietl Should we also forbid annotation on supertype's type parameter? For example

public static class NullSupplier extends Supplier<@Nullable String> {}

nvm, looks like there is a reason we should allow annotation on supertype's type parameter. https://eisop.github.io/cf/manual/manual.html#annotations-are-a-contract

[wmdietl]

Thanks for the update!

[wmdietl]

This doesn't follow our usual naming convention. This should be something that starts with check.
But there already is such a method: checkExtendsOrImplements.
What is the relation between this check and what checkExtendsOrImplements already does?
The two checks seem conflicting: this raises an error if there is an annotation on extends/implements vs. checkExtendsOrImplements raises and error when the class declaration annotation is inconsistent with an annotation on the extends/implements.
How are both checks as default behavior meaningful?

[aosen-xiong]

The two checks seem conflicting: this raises an error if there is an annotation on extends/implements vs. checkExtendsOrImplements raises and error when the class declaration annotation is inconsistent with an annotation on the extends/implements.

Well, I think we can either keep the two checks here or use an additional flag to indicate we don't allow annotation on supertype and we don't do the consistency checks or we allow annotation on supertype and we do consistency checks.

Which one will be nicer?

[wmdietl]

Adding a new checkSupertypeAnnotations in addition to the existing checkExtendsOrImplements seems very confusing. They both basically look at the same thing and the name does not make clear when to use which method.
There is no cross-reference between the methods that would help the user decide.

With the current code, checkSupertypeAnnotations forbids annotations in a location, but then checkExtendsOrImplements checks for a subtyping relation, which also is tricky to follow. Then TaintingVisitor overrides checkSupertypeAnnotations and says do nothing, which is confusing, as this now enables the check in checkExtendsOrImplements.

So try your other suggestion: have one checkExtendsOrImplements that has a boolean whether lenient or strict checks are desired. (If there is enough common code. Maybe you can just have two separate method.)
Then the current checkExtendsOrImplements will call the method with a boolean (or the strict method). And TaintingVisitor can override the method and change the behavior.

[wmdietl]

Please go through the English in your comments and try to polish it.

[Copilot]

Pull request overview

This PR implements issue #1059 by forbidding type-qualifier annotations on extends/implements supertypes in class declarations, reporting a dedicated annotation.on.supertype error from the shared BaseTypeVisitor logic.

Changes:

• Added a new annotation.on.supertype diagnostic and a BaseTypeVisitor check that flags supported qualifiers on annotated supertypes.
• Updated Nullness behavior to rely on the shared base-type check (removing the Nullness-specific nullness.on.supertype message and visitor logic).
• Added an override in the Tainting checker to explicitly allow annotated supertypes, and updated the Nullness test accordingly.

Reviewed changes

Copilot reviewed 7 out of 7 changed files in this pull request and generated 2 comments.

Show a summary per file

File	Description
framework/src/main/java/org/checkerframework/common/basetype/messages.properties	Adds the new annotation.on.supertype message key.
framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java	Introduces the shared “forbid annotated supertypes” check and a new overload to toggle it.
docs/CHANGELOG.md	Documents the new behavior and how to disable it in checkers.
checker/tests/nullness/AnnotatedSupertype.java	Updates expected diagnostics to the new shared error key.
checker/src/main/java/org/checkerframework/checker/tainting/TaintingVisitor.java	Overrides the check to allow annotated supertypes for the Tainting checker.
checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitVisitor.java	Removes the old Nullness-specific supertype-annotation check.
checker/src/main/java/org/checkerframework/checker/nullness/messages.properties	Removes the now-obsolete nullness.on.supertype message key.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.