Map.merge nullness annotations are unsound

[cpovirk]

The problem is that the stubs permit the merge function to return null but don't declare that merge itself can then return that to the user:

checker-framework/checker/jdk/nullness/src/java/util/Map.java

Lines 1206 to 1207 in 02db22b

	default V merge(K key, V value,
	BiFunction<? super V, ? super V, ? extends @Nullable V> remappingFunction) {

$ cat Merge.java 
import java.util.HashMap;
import java.util.Map;

class Merge {
  public static void main(String[] args) {
    Map<String, String> map = new HashMap<>();
    map.put("k", "v");
    map.merge("k", "v", (a, b) -> null).toString();
  }
}

$ checker/bin/javac -processor org.checkerframework.checker.nullness.NullnessChecker Merge.java && java Merge
Exception in thread "main" java.lang.NullPointerException
  at Merge.main(Merge.java:8)

The fix would be either:

• Require remappingFunction to return a V (not @Nullable V). This reduces expressiveness, but my guess is that users rarely use the ability to return null. (For what it's worth, I didn't notice this bug from actually returning null from a merge function. I just happened to notice it when looking at the stub for Map.)
• Change the return type of merge to @Nullable V. This preserves expressiveness but may inconvenience the average caller of merge. (This is of course somewhat like Map.get. However, @KeyFor can't help much here. And it would be mildly unfortunate for users to pass a non-null value and a function that never returns null and yet have to handle null.)

I don't believe @PolyNull is a solution here, at least not by itself: If the user has an empty Map<String, @Nullable String>, then map.merge("k", null, someFunction) will return null, even if someFunction never returns null. To use @PolyNull, we'd need to also change the value parameter's type to @NonNull V.

Source file and -version -verbose -AprintAllQualifiers output attached.

[cpovirk]

It looks like the intention was to avoid having to make the return type @Nullable. But as noted, I don't think it's panned out :(

[mernst]

Thanks very much for the report, Chris. Sorry for taking so long to address it.