`@MustCall` subtyping

[mernst]

This code passes the Must Call Checker:

  @MustCall({"toString"}) String foo(@MustCall({"hashCode"}) String arg) {
    return arg;
  }

However, it seems wrong to permit one @MustCall type to be permitted to be used as another.

A test case appears in MustCallSubtypingTest.java.

[kelloggm]

This is expected behavior: arg is a non-owning parameter, so its @MustCall type is ignored.

The manual section for the Must Call Checker doesn't explain this behavior, specifically, and I can see how it might be confusing. We could view this issue as a request for better documentation.

Alternatively, maybe the checker should warn about explicit @MustCall annotations that are ignored due to being written on a non-owning parameter? Or, we could modify the checker's rules to implicitly make such parameters @Owning, which might conform better to user expectations when writing an @MustCall annotation?

@mernst what would be your preferred action to take to address this confusion? Would better documentation be enough, or would you like us to do more?

[mernst]

Thanks for the explanation.

the checker should warn about explicit @MustCall annotations that are ignored due to being written on a non-owning parameter

I think this is the best behavior.

we could modify the checker's rules to implicitly make such parameters @Owning, which might conform better to user expectations when writing an @MustCall annotation?

I fear this would be surprising. It would also make separate compilation (with regular javac) behave differently than compiling every file together while running the Checker Framework, which I would like to avoid.