JSpecify: False negative when overriding narrows `@Nullable` type variable bound

[HildingLinden]

The following code passes using NullAway 0.13.1 in JSpecify mode.

@NullMarked
interface Foo {
    <T extends @Nullable Object> void bar( T arg );
}

@NullMarked
class Baz implements Foo {
    @Override
    public <T> void bar( T arg ) {}
}

This looks like a false negative: the override narrows the method type variable bound from <T extends @Nullable Object> to <T>, even though T is used in parameter position. No diagnostic is reported.

[msridhar]

Interesting! Here is a more complete example, which throws an NPE when run:

class Test {
  interface Foo {
      <T extends @Nullable Object> void bar( T arg );
  }
  static class Baz implements Foo {
      @Override
      public <T> void bar( T arg ) { arg.hashCode(); }
  }
  public static void main(String[] args) {
    Foo f = new Baz();
    f.<@Nullable String>bar(null);
  }
}

This passes NullAway, which is unsound. It also passes the JSpecify reference checker. But it does not pass the Checker Framework / EISOP, which report an error indicating that arg.hashCode() is dereferencing a possibly-null reference. For the original version of the code without arg.hashCode(), Checker Framework / EISOP do not report an error.

@cpovirk any thoughts on whether this might be an issue in the JSpecify specification, or whether it's a bug in the reference checker implementation?

[msridhar]

FWIW, here's a roughly analogous example in Java without nullability:

class Test {
  static class Foo {
      <T> void bar( T arg ) {}
  }
  static class Baz extends Foo {
      @Override
      public <T extends String> void bar( T arg ) { arg.length(); }
  }
  public static void main(String[] args) {
    Foo f = new Baz();
    Object x = new Object();
    f.<Object>bar(x);
  }
}

Here, javac reports an error at @Override saying Baz.bar does not override any method in Foo. If you remove @Override it compiles, but there is no error at runtime since the call invokes Foo.bar rather than Baz.bar.

[HildingLinden]

I can add that IntelliJ IDEA raises a warning both examples:

[cpovirk]

Thanks!

I agree that there should be an error in the original code, both in NullAway and in the reference checker. (And we should add a sample / conformance test, too, if we don't have one already.)

I think the situation with the Checker Framework and IntelliJ is adding another layer of complexity with their handling of type-parameter declarations.

In the absence of @NullMarked in the Test example, the Checker Framework (both eisop and typetools) applies its special case for <T> read from source code, treating it as <T extends @Nullable Object>. Thus, the override is legal, but the usage of arg triggers the error that you noted.

That said, if we override the special case by providing an explicit <T extends @NonNull Object> (or probably even just <T extends Object>), then both typetools and eisop (I didn't test IntelliJ) do complain about the override itself:

Test.java:11: error: [override.param] Incompatible parameter type for arg.
      public <T extends @NonNull Object> void bar( T arg ) { arg.hashCode(); }
                                                     ^
  found   : T extends @Initialized @NonNull Object
  required: T extends @Initialized @Nullable Object
  Consequence: method in @Initialized @NonNull Baz
    <T extends @Initialized @NonNull Object> @NonNull void bar(@Initialized @NonNull Baz this, T extends @Initialized @NonNull Object p0)
  cannot override method in @Initialized @NonNull Foo
    <T extends @Initialized @Nullable Object> @NonNull void bar(@Initialized @NonNull Foo this, T extends @Initialized @Nullable Object p0)
1 error

eisop likewise complains even about a plain <T> in the override if I make Test be @NullMarked.

(As always, another potential complication is the need to run the reference checker with -Astrict in order to report all possible problems in the absence of @NullMarked. But the original code used @NullMarked, and I don't see an error, anyway. That remains true even if I (unnecessarily) do pass -Astrict.)

As for the spec: We have thus far settled with "We anticipate that tools will typically apply each part of this spec in the same cases that they (or javac) already apply the corresponding part of the Java Language Specification." So, since javac reports the analogous error that you mentioned, it would make sense for tools to do the same here. We could certainly try to do more, either in the spec (normatively or non-normatively) or in a separate document. I haven't been too excited about trying to "compete with" the JLS, but it would obviously be convenient for someone to put together some kind of list.

[msridhar]

Thanks a lot, @cpovirk! Very sorry, in my comment above I intended the Test class to have a @NullMarked annotation:

@NullMarked
class Test {
  interface Foo {
      <T extends @Nullable Object> void bar( T arg );
  }
  static class Baz implements Foo {
      @Override
      public <T> void bar( T arg ) { arg.hashCode(); }
  }
  public static void main(String[] args) {
    Foo f = new Baz();
    f.<@Nullable String>bar(null);
  }
}

Even with @NullMarked I don't see an error with NullAway or the reference checker. Good to know that eisop gives an appropriate error with @NullMarked though.

I agree this case should be covered by that phrase in the spec that you mentioned.