[Nullness] false positive for BasicMultimap

[alexvas]

Inputs

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

import java.util.ArrayList;
import java.util.HashMap;
import java.util.List;
import java.util.Map;

interface BasicMultimap<K, V> {
    @Nullable List<V> get(K key);

    void put(K key, V value);
}

class BasicMultimapImpl<K, V> implements BasicMultimap<K, V> {

    private final Map<K, List<V>> delegate = new HashMap<>();

    public void put(K key, V value) {
        delegate.computeIfAbsent(key, ignored -> new ArrayList<>()).add(value);
    }

    public @Nullable List<V> get(K key) {
        return delegate.get(key);
    }
}

Live demo of the example

Output

An error at line 23, column 29:

Error: [argument.type.incompatible] incompatible argument for parameter arg0 of get.   
     found   : K extends @Initialized @Nullable Object
     required: @Initialized @NonNull Object

Expectation

One expects no error here.

It is not quite clear where to add what annotation (@NonNull, whatever ?) except @SuppressWarnings("nullness") above the line 23 to get rid of the error.

[wmdietl]

Thanks for the report! This is actually desired behavior, caused by our goal of being sound and preventing all possible NPEs.

Note that the parameter to Map#get is non-null.
This is because there are implementations of Map that forbid null keys. E.g. if you replace new HashMap<>(); with new Hashtable<>(); and then called get(null), you should get an NPE.

As you note, you could add a SuppressWarnings on your implementation of get, reasoning that you don't use a null-hostile map.

Another way to relax this constraint is to use the stub file at: https://github.com/eisop/checker-framework/blob/master/checker/src/main/java/org/checkerframework/checker/nullness/collection-object-parameters-may-be-null.astub

Also see:
https://eisop.github.io/cf/manual/manual.html#nullness-collection-arguments

[cpovirk]

Another alternative (which would be somewhat against typical Java style, though I like it :)) would be to declare your field type as HashMap<K, List<V>>. Then the checker would use the stub for HashMap.get, which (unlike the stub for Map.get) has a @Nullable annotation on the parameter.

[alexvas]

Thank you for your answers.

Here is fixed (proof) initial example that pass nullness check:

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

import java.util.ArrayList;
import java.util.HashMap;
import java.util.List;
import java.util.Map;

interface BasicMultimap<K extends @NonNull Object, V extends @NonNull Object> {
    @Nullable List<V> get(K key);

    void put(K key, V value);
}

class BasicMultimapImpl<K extends @NonNull Object, V extends @NonNull Object> implements BasicMultimap<K, V> {

    private final Map<K, List<V>> delegate = new HashMap<>();

    public void put(K key, V value) {
        delegate.computeIfAbsent(key, ignored -> new ArrayList<>()).add(value);
    }

    public @Nullable List<V> get(K key) {
        return delegate.get(key);
    }
}

A couple of newcomer questions:

1. Why explicit K extends @NonNull Object is required? It seems from documentation that @NonNull is always a default qualifier. It might worth to especially mention opposite for type parameters if this is the case.
2. The Map does not suffer from this verbosity, because get's argument is a non-generic Object, is it correct?

[wmdietl]

Re 1: The @NonNull in the type parameter bounds is not necessary, but the explicit upper bound is necessary.
Just <K> is interpreted as <K extends @Nullable Object>, whereas <K extends Object> is defaulted to <K extends @NonNull Object>.
So the defaulting rules are consistent - explicit types are defaulted to @NonNull (except a few places, e.g. local variables).
In the current Nullness Checker, there is a difference between <K> and <K extends Object>, which can be convenient, but surprising.
Note that in JSpecify we made a different choice: <K> is equivalent to <K extends @NonNull Object> and one needs to explicitly write <K extends @Nullable Object> to get an nullable upper bound. This is described here.
In @NullMarked code, the CF Nullness Checker uses the same defaults as JSpecify. At some point, we might switch to use the same type parameter bounds behavior for both.

Re 2: I'm not sure what you mean with "suffer from this verbosity"... the get signature in your example doesn't need any annotations. Can you expand?

Welcome to static null checking! Feel free to open issues or post a discussion and we'll try to help.

[alexvas]

Thank you for such detailed comment.

1. First of all let me state that CF has an excellent and comprehensive documentation. It's shortcoming is a sequel of it's virtue. When a one is trying to estimate whether the framework would fit his or her needs or not, it's easy to overlook the difference between defaults for method argument and defaults for type parameter. Hope my little MR (or a few other words that way) will help the next newcomer to catch the difference sooner.

2. I mean, from a view of newcomer: where to find example of correctly annotated class that is most close to Multimap? It is probably a Map, right? It turns out the Map annotations are quite different from correct annotations for Multimap. Map has no <K extends @NonNull Object>. And this is for the reason, yes. Yet the reason is not self-evident at first.

Another my very biased point is, for historical perspective we have a paradigm shift. From "Everything might be null by default" in Good Old Java to "Every argument is @NonNull by default, yet not a type parameter" in CF (or e.g. Kotlin) and further into "Everything is @NonNull by default, even a type parameter" in JSpecify. This is taking aside Algebraic Data Types with Pattern Matching removing nulls away in some modern languages (e.g. Rust). So this is about a shift in mindset.

Every casual user of the CF lives somewhere in between Good Old Java approach and Rust approach. A user might think: "Whatever default your excellent framework has, I would like to have an option to override them for this or that particular module of my project." It would be nice to have a command-line flag to say "All type parameters here are non-null by default" or even "Both arguments and type parameters are null by default". In my particular case the former option would reduce verbosity, as just <K> would be enough to mean <K extends @NonNull Object>.