Dealing with @Nullable in FunctionalInterface lambda

Question

How should I deal with lambda functions using checker-framework typed annotations?

For example,

private void dispatch(Progress progress, Load request, @Nullable Layer layer)
    {
        if (layer == null) return;

        Utils.log("DISPATCHING " + layer.name);
        JThread.run(() -> runDispatch(progress, request, layer));
    }

Checker will issue a argument.type.incompatible warning on the runDispatch line call, even though layer is being checked beforehand. I understand that the lambda function is inside a different context, and therefore Checker can't correctly assess that. What is the best way to deal with it?

Extra info

Full warning:

error: [argument.type.incompatible] incompatible types in argument.
[ERROR] found   : @Initialized @Nullable Layer<? extends @Initialized @NonNull Item, ? extends @Initialized @NonNull Deliver, ? extends @Initialized @NonNull Recipient>
[ERROR] 
[ERROR] required: @Initialized @NonNull Layer<? extends @Initialized @NonNull Item, ? extends @Initialized @NonNull Deliver, ? extends @Initialized @NonNull Recipient>

runDispatchis declared on the same class, signature private void runDispatch(Progress progress, Load request, Layer layer)

Another example: Elsewhere in my code I have a similar situation, but involving method behavior:

on Item.class:

    @EnsuresNonNullIf(expression="extraAction", result=true)
    public final boolean hasExtraAction() {
        return extraAction != null;
    }

on a separate class:

    @RequiresNonNull("#2.extraAction")
    private void buildExtraActionRunnable(Layer layer, Item item, Deliver deliver) {
    ....
    }



    ...
    } else if (item.hasExtraAction()) {
            Runnable r = () -> buildExtraActionRunnable(layer, item, deliver);

Here, at the Runnable line I get error: [contracts.precondition.not.satisfied] the called method 'buildExtraActionRunnable(layer, item, deliver)' has a precondition 'item.extraAction' that is not satisfied

Answer 1

I agree that this is a bug in the Nullness Checker. In this part of your code:

    Utils.log("DISPATCHING " + layer.name);
    JThread.run(() -> runDispatch(progress, request, layer));

the Nullness Checker knows at the call of Utils.log that layer is non-null, but it doesn't know that fact at the call to runDispatch within the method body. Within the method body, it is using the declared type of layer rather than a refined type computed via dataflow analysis.

Your question was how to work around the Checker Framework bug. One way to do so is to introduce a new variable:

    Utils.log("DISPATCHING " + layer.name);
    Layer layer2 = layer;  // work around CF issue #1248
    JThread.run(() -> runDispatch(progress, request, layer2));

The above code typechecks correctly.

I can't give a detailed answer for your second example, because you didn't give a compilable MWE. But whenever there is an error of the form error: [KEY] ..., you can always suppress it by adding @SuppressWarnings("KEY"). It your case, this would be @SuppressWarnings("contracts.precondition.not.satisfied").