Improved interaction between `@This` and `@MustCall`

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.)

Start with the Java examples and the MustCall diagnostic in the issue, then trace the Checker Framework's MustCall defaulting behavior for methods annotated with @This. Done means the safe Handle implementation type-checks without the awkward @PolyMustCall annotations while preserving the demonstrated closeability guarantees.