Add subtyping check to receiver type argument for method invocation

[aosen-xiong]

Fixes #104

Note that the implementation ignores the subtyping check when the receiver type argument has a poly annotation. See PolyQualifierOnTypeArgument.java

[wmdietl]

As discussed, please add a jtreg test.

[wmdietl]

Maybe this would fix #104? Can you try with tests from that issue?

[aosen-xiong]

Maybe this would fix #104? Can you try with tests from that issue?

Just checked, this did not fix it.

[wmdietl]

Thanks for starting to look into this. We should look at this properly and fix #104 while we touch this code.

[wmdietl]

Maybe these checks should also go into checkMethodInvocability?
In that method, there is a comment Static methods don't have a receiver to check. The check here already excludes static methods, so we should raise an error if the receiver is still null.

(And undo the white-space only change.)

[aosen-xiong]

is the purpose for !ElementUtils.isStatic(invokedMethodElement) && !TreeUtils.isSuperConstructorCall(tree)

the same as

methodReceiver != null and method.getElement().getKind() != ElementKind.CONSTRUCTOR?

I am wondering which checks should be kept in checkMethodInvocability.

[wmdietl]

They seem different.
ElementUtils.isStatic(invokedMethodElement) seems higher-level and more declarative, whereas the null check is lower-level and implementation focussed. Maybe something went wrong and the receiver is null? So I would prefer the first one.

For the constructors, they are different and we need to figure out which one we actually want. The first one only excludes super(...) calls, not this(...) calls. Why? The second one checks whether the element is any constructor. Can you think through which is better?

[aosen-xiong]

Okay.

Use the second constructor filter seems safer to me.

I don't understand the todo comment We must not use the self type, but instead should find a way to determine the receiver of the enclosing constructor.

Does it mean the self.something() call below should use @B for the receiver subtyping checking instead of @A? Or is it a problem for the inner class's constructor?

 class Foo {
      @A Foo() { 
          this(42);
          self.something(); 
      }
      @B Foo(int x) { ... }
  }

[wmdietl]

Thanks, some follow-up comments.

[wmdietl]

Why can't this not simply use methodReceiver or treeReceiver that we calculate below? What is different about this receiver? Or maybe you can use invokedMethodElement?
In any case, the variable names are rather non-descriptive, making the distinction invisible.

[aosen-xiong]

I renamed the variable to methodDefPreSubstitution.

methodReceiver or method's poly annotation already got substituted. I need the receiver before substitution.

[aosen-xiong]

@wmdietl We have two options for this PR.

1. Enable all method receiver type argument subtyping checks and add error/suppression to daikon and plume-lib.
2. Disable the method receiver type argument when the declared method has a poly type argument.

Which one do you like？

[Copilot]

Pull request overview

This PR fixes #104 by ensuring that method invocations validate the receiver’s annotated type arguments via a full subtyping check, so annotations like Box<@NonNull T> this are no longer ignored at call sites.

Changes:

• Update receiver invocability checking to perform a subtype check on the full receiver type (including type arguments) rather than on erased types.
• Add Nullness tests that (a) reproduces the original bug and (b) documents/guards the special-case behavior for polymorphic annotations on receiver type arguments.
• Document the user-visible behavior change in the changelog and list the closed issue.

Reviewed changes

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

File	Description
framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java	Implements receiver type-argument subtyping check during method invocation, with a poly-annotation skip.
docs/CHANGELOG.md	Notes the new receiver type-argument subtyping behavior and adds the closed issue entry.
checker/tests/nullness/ReceiverTypeArgs.java	New regression test demonstrating the previously-missed invalid receiver invocation.
checker/tests/nullness-genericwildcard/PolyQualifierOnTypeArgument.java	New test covering the “skip when receiver type arg is polymorphic” behavior.

---

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

[Copilot]

visitMethodInvocation already computes preInference = atypeFactory.methodFromUseWithoutTypeArgInference(tree); checkMethodInvocability recomputes the same value, which duplicates non-trivial work per method call and risks a noticeable performance regression. Consider reusing the already-computed preInference (e.g., pass it in via an overload or refactor the poly-receiver check to avoid a second factory call).

[aosen-xiong]

Good point. But we haven't decide we want to exclude the check when poly is present. Let's leave it for now.