Nullness Checker error message uses incorrect parameter name

[msridhar]

Test case:

import org.checkerframework.checker.nullness.qual.Nullable;
class Test {
    interface A<T1 extends @Nullable Object> {
        String fn(T1 o);
    }
    static String foo(Object o) { return o.toString(); }
    static void testPositive() {
        A<@Nullable Object> p = Test::foo;
    }
}

Error output from the Nullness Checker:

/tmp/Test.java:8: error: [methodref.param] Incompatible parameter type for o
        A<@Nullable Object> p = Test::foo;
                                ^
  found   : @Initialized @NonNull Object
  required: @Initialized @Nullable Object
  Consequence: method in @Initialized @NonNull Test
    @Initialized @NonNull String foo(@Initialized @NonNull Object p0)
  is not a valid method reference for method in @UnknownInitialization @Nullable A<@Initialized @Nullable Object>
    @Initialized @NonNull String fn(@Initialized @NonNull A<@Initialized @Nullable Object> this, @Initialized @Nullable Object p0)
1 error

In a couple of places the error message refers to p0 which is not the name of any variable in the program.

I also find the error message somewhat hard to read with all the (irrelevant) initializer annotations, but perhaps that is a separate issue.

[smillst]

The p0 is coming from here:

checker-framework/framework/src/main/java/org/checkerframework/framework/type/DefaultAnnotatedTypeFormatter.java

Lines 347 to 348 in 0b8da55

	// Output some parameter names to make it look more like a method.
	// TODO: go to the element and look up real parameter names, maybe.

There will still be cases where the parameter name is not in the element, but the parameter names for your test case will be there since they are from source.

I also find the error message somewhat hard to read with all the (irrelevant) initializer annotations, but perhaps that is a separate issue.

We have an issue for this: #2276. It's not actually too hard to fix, we just haven't done it.