Improved interaction between @This and @MustCall

[Calvin-L]

I recently encountered some code structured like this:

import org.checkerframework.common.returnsreceiver.qual.This;

import java.io.Closeable;

interface Interface {
    @This Interface f();
}

public class Handle implements Interface, Closeable {

    @Override
    public @This Handle f() {
        return this;
    }

    @Override
    public void close() {
    }

    public static void exampleUsage() {
        try (var x = new Handle()) {
            x.f().f(); // no need to close the intermediate results
        }
    }

}

Checker Framework 3.47.0 reports

Handle.java:[12,17] error: [override.return] Incompatible return type.
  found   : @MustCall("close") Handle
  required: @MustCall Interface
  Consequence: method in @MustCall("close") Handle
    @MustCall("close") Handle f(@MustCall("close") Handle this)
  cannot override method in @MustCall("close") Interface
    @MustCall Interface f(@MustCall Interface this)

Fair enough: Handle is @MustCall("close"), so you can't return a Handle in place of an @MustCall({}) Interface.

But this code is safe. It is even possible to annotate correctly, but doing so is very awkward:

interface Interface {
    @This @PolyMustCall Interface f(@PolyMustCall Interface this);
}

public class Handle implements Interface, Closeable {
    @Override
    public @This @PolyMustCall Handle f(@PolyMustCall Handle this) {
        return this;
    }
    // ...
}

Because the method returns this, its return value must have the same @MustCall as the receiver. With the additional @PolyMustCall annotations, the Checker Framework approves.

Is it possible to adjust the MustCall defaulting rules to do this automatically for methods returning @This?

(Actually, this probably generalizes to other type systems, but I expect it will be most useful for the MustCall checker.)

[Calvin-L]

(Related, although less important: with the @PolyMustCall annotations in place, the Checker Framework reports some spurious warnings like

Handle.java:[13,38] [mustcallalias.method.return.and.param] @MustCallAlias annotations must appear in pairs (one on a return type and one on a parameter type).
  But no parameter has a @MustCallAlias annotation, even though the return type is annotated with @MustCallAlias

I suspect it is not checking the implicit this parameter.)

(On that note, would @MustCallAlias be more precise than @PolyMustCall in my example?)