[dereference.of.nullable] on final field access in closure

import java.util.function.Consumer;

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

class CF {

    private final @Nullable Ref ref;

    CF(@Nullable Ref ref) {
        this.ref = ref;
    }

    void fun(CF other) {
        if (this.ref != null && other.ref != null) {
            this.ref.apply(arg -> other.ref.fun());
        }
    }

    static class Ref {
        void fun() {}
        void apply(Consumer<Void> c) { c.accept(null); }
    }
}

Running the default NullnessChecker

checker/bin/javac -processor org.checkerframework.checker.nullness.NullnessChecker CF.java

returns the following false-positive

CF.java:[15,39] error: [dereference.of.nullable] dereference of possibly-null reference other.ref

other.ref shouldn't be null at this point because nullness has been checked before and the field is final so it can't be re-assigned by any possible side-effects. I tested against checkerframework 3.17.0 and Java 8.

This issue might be related to #4872 but here, the nullness is checked directly (instead of a result of dataflow) and the access takes place in a closure rather than an inline block.

Start with the CF.java reproducer and run the listed NullnessChecker command on Java 8 to confirm the false positive. Trace how the checker handles the final other.ref field across the lambda in fun, considering the related behavior in issue #4872. Done means the example compiles without the erroneous dereference.of.nullable diagnostic while genuine nullable dereferences remain reported.