Treat polymorphic types more precisely for classes with upper bound

Consider a class with an @Untainted upper bound. All instances of this class are guaranteed to be @Untainted. Thus, if we have an instance of @PolyTainted MyClass, we actually know that it will be @Untainted. Consider this class that uses @PolyTainted,

import org.checkerframework.checker.tainting.qual.*;


public @Untainted class MyClass {
    public void requiresUntainted(@Untainted MyClass this) {
    }

    public void f(@PolyTainted MyClass this) {
        this.requiresUntainted();
    }
}

When I run the tainting checker javac -processor TaintingChecker MyClass.java, one of the errors I get is

MyClass.java:9: error: [method.invocation.invalid] call to requiresUntainted() not allowed on the given receiver.
        this.requiresUntainted();
                              ^
  found   : @PolyTainted MyClass
  required: @Untainted MyClass

The call to requiresUntainted is okay, because the receiver of f will always be @Untainted. So, to improve precision the framework could treat polymorphic instances of a class @A MyClass as if it could only take values with type @A or a subtype. That is, treat it as if it could only take on annotations in the range bottom to @A.

In the above example, we could declare f to take a receiver of type @Untainted to fix the issue. This is not always an option when subtyping is involved. Suppose we have a type system with three annotations, @C extends @B extends @A and a polymorphic qualifier @MyPoly. Then, suppose in the annotated JDK for this checker we have the declaration

@MyPoly String toString(@MyPoly Object this);

Then, in a subtype we may have

public @B class MyClass {

    public void requiresB(@B MyClass this) {
    }

    public @MyPoly String toString(@MyPoly MyClass this) {
        this.requiresB();
        return super.toString();
    }
}

We may want the annotations in the JDK to be as general as possible, hence the use of polymorphism. However, there may be subtypes that will all be of type @B or below, but we would still need toString to take a @MyPoly receiver. Declaring it @B would break subtyping rules.

Note, if @MyClass had instead been declared @C, the bottom type, we could have even declared the return type of toString as @C, rather than @MyPoly. If the upper bound is not the bottom type, though, we have to keep the generality of a polymorphic return type because the receiver could be of type @B or @C and we would want the return type to be @B or @C accordingly.

Start by reproducing the reported javac command with MyClass.java and the TaintingChecker entry point, then trace how polymorphic receiver qualifiers are interpreted for classes with annotated upper bounds. Done means the receiver call is accepted when the class bound guarantees @Untainted, while polymorphic return and subtyping behavior remains valid in the described @A/@B/@C case.