Cannot assign MonotonicNonNull to MonotonicNonNull (monotonic type)

[GoogleCodeExporter]

------------------- Sample file
import checkers.nullness.quals.MonotonicNonNull;

public class MonoBugExample {
  @MonotonicNonNull Object x;

  static <T> T check(T var) {
    return var;
  }

  void fakeMethod() {
    check(x);
  }
}

------------------- Error message
MonoBugExample.java:13: error: [monotonic.type.incompatible] cannot assign 
checkers.nullness.quals.MonotonicNonNull to 
checkers.nullness.quals.MonotonicNonNull (monotonic type).
    check(x);
          ^
  full type found: @Initialized @MonotonicNonNull Object

------------------- Extra details
Using: Linux, Checker version from March 2014

Found similar report here: 
https://groups.google.com/forum/#!topic/checker-framework-discuss/tZqeGoGxuGE

Part of code that probably emits the error (the condition in if looks strange, 
but I am not really familiar with the code):
https://code.google.com/p/checker-framework/source/browse/framework/src/org/chec
kerframework/common/basetype/BaseTypeVisitor.java#1517

Original issue reported on code.google.com by hau...@google.com on 24 Mar 2014 at 6:59

[GoogleCodeExporter]

Thanks for the bug report!
I've added a test case at checker-framework/checker/tests/nullness/Issue306.java

The issue is that monotonic qualifiers are not reflexive - two different uses 
might be in different states. In your example, @MonotonicNonNull is the most 
specific type inferred for the type argument of "check". However, the type 
system cannot keep track of whether that type came from x or somewhere else. 
Therefore, it conservatively rejects the code.
I've added a few more examples into the test case. In particular, at the moment
an "x = x" assignment is forbidden for the same reason; however, I think "x = 
x" is a code pattern we can ignore.

As a quick fix, you can specify @Nullable Object as type argument to "check":

Issue306.<@Nullable Object>check(x);

We need a way to make type argument inference aware of monotonic qualifiers, in 
order to not use them as inferred type arguments. This can be done by looking 
for the @MonotonicQualifier meta-annotation on a qualifier and then trying a 
supertype.
Does anyone see a better solution?

Original comment by wdi...@gmail.com on 25 Mar 2014 at 7:08

• Changed state: Accepted

[GoogleCodeExporter]

As Werner noted, forbidding the assignment is by design -- allowing all 
assignments from @MonotonicNonNull to @MononoticNonNull would be unsound.

An enhancement request to make the type-checker less conservative in the case 
of type argument inference is a reasonable request.  Thanks for bringing it to 
our attention.

Original comment by michael.ernst@gmail.com on 26 Mar 2014 at 4:32

• Added labels: Type-Enhancement
• Removed labels: Type-Defect