typetools / checker-framework

Pluggable type-checking for Java
http://checkerframework.org/
Other
990 stars 347 forks source link

Field with @RequiresNonNull + @MonotonicNonNull is treated as nullable inside lambda #6595

Open cushon opened 2 weeks ago

cushon commented 2 weeks ago
import org.checkerframework.checker.nullness.qual.MonotonicNonNull;
import org.checkerframework.checker.nullness.qual.RequiresNonNull;

class Require {
  @MonotonicNonNull String s;

  @RequiresNonNull("s")
  Supplier<String> s() {
    return () -> s;
  }

  interface Supplier<T> {
    T get();
  }
}

Actual:

$ ./checker-framework-3.43.0/checker/bin/javac -processor nullness Require.java
Require.java:9: error: [return] incompatible types in return.
    return () -> s;
                 ^
  type of expression: @Initialized @MonotonicNonNull String
  method return type: @Initialized @NonNull String
1 error

Expected:

No error: Even though the lambda may run later, s is not only known to be non-null initially but is also known to remain so because of @MonotonicNonNull.