checker-framework icon indicating copy to clipboard operation
checker-framework copied to clipboard

Nullness checker handling of implicit type variable bounds - difference between <T> and <T extends @Nullable Object>

Open cushon opened this issue 3 years ago • 3 comments

In the following example, the nullness checker rejects an input that contains a type variable with an explicit extends @Nullable Object bound, and accepts the same example if the explicit bound is removed.

The CLIMB-to-top defaults say implicit type variable bounds are interpreted as equivalent extends @Nullable Object, is this a bug?

import org.checkerframework.checker.nullness.qual.Nullable;

class A<V extends @Nullable Object> {
  I<V> i() {
    return new B<>(this);
  }
}

class B<K, V> implements I<V> {
  B(A<V> a) {}
}

interface I<V> {}

With Checker Framework 3.21.3:

$ ./checker-framework-3.21.3/checker/bin/javac -processor nullness A.java
A.java:5: error: [return] incompatible types in return.
    return new B<>(this);
           ^
  type of expression: @Initialized @NonNull B<@Initialized @NonNull Object, V extends @Initialized @NonNull Object>
  method return type: @Initialized @NonNull I<V extends @Initialized @Nullable Object>
A.java:5: error: [argument] incompatible argument for parameter a of B.
    return new B<>(this);
                   ^
  found   : @Initialized @NonNull A<V extends @Initialized @Nullable Object>
  required: @Initialized @NonNull A<V extends @Initialized @NonNull Object>
2 errors

The code compiles without error if extends @Nullable Object is removed.

diff A.java B.java
3c3
< class A<V extends @Nullable Object> {
---
> class A<V> {
$ ./checker-framework-3.21.3/checker/bin/javac -processor nullness B.java

cushon avatar Mar 07 '22 16:03 cushon

Yes, this a bug. For some reason, the code that infers the type arguments for the diamond is ignoring the explicit annotation on the type variable. (The errors disappear with new B<Object, V>(this);)

smillst avatar Mar 07 '22 18:03 smillst

Thanks @smillst for taking a look!

Here's one more example that seems closely related, where adding an explicit type argument doesn't seem to help:

import org.checkerframework.checker.nullness.qual.Nullable;

class C<V extends @Nullable Object> {
  I<V> c(N n) {
    return h(n.i());
  }

  abstract class N {
    abstract I<V> i();
  }

  static <V> I<V> h(I<V> i) {
    return i;
  }
}

interface I<V> {}
./checker-framework-3.21.3/checker/bin/javac -processor nullness C.java
C.java:5: error: [return] incompatible types in return.
    return h(n.i());
            ^
  type of expression: @Initialized @NonNull I<V extends @Initialized @NonNull Object>
  method return type: @Initialized @NonNull I<V extends @Initialized @Nullable Object>
1 error

The same diagnostic is reported after adding an explicit type argument:

diff C.java D.java
5c5
<     return h(n.i());
---
>     return C.<V>h(n.i());
./checker-framework-3.21.3/checker/bin/javac -processor nullness D.java
D.java:5: error: [argument] incompatible argument for parameter i of h.
    return C.<V>h(n.i());
                     ^
  found   : @Initialized @NonNull I<V extends @Initialized @NonNull Object>
  required: @Initialized @NonNull I<V extends @Initialized @Nullable Object>
1 error

cushon avatar Mar 07 '22 20:03 cushon