False positive in the Optional Checker

[jyoo980]

Overview

The updated (to-be-released) Optional Checker has increased precision in its analysis of Optional values resulting from operations on container types. For example, it is able to deduce that the terminal .get() operation below is safe (i.e., will not throw a NoSuchElementException):

@NonEmpty Stream<Integer> lens = List.of("foo").stream()
    .map(String::length);
// Calling `Stream.max` on a non-empty container will always yield a present `Optional`
lens.max(Integer::compare).get();

Issue

The updated Optional Checker suffers false positives when the Optional-resulting operation depends on the type of the earliest leftmost receiver whose type is @PolyNonEmpty.

For example, the following minimal example (also attached as Main.java) should cleanly type-check:

import java.util.Optional;
import java.util.List;

import org.checkerframework.checker.nonempty.qual.*;

class Main {

  class Container {

    @NonEmpty List<String> getStrs() {
      throw new Error();
    }
  }

  void foo() {
    Container container = new Container();
    container.getStrs().stream().findAny().get();
  }
}

But it fails with the error message:

Main.java:17: error: [method.invocation] call to get() not allowed on the given receiver.
    container.getStrs().stream().findAny().get();
                                              ^
  found   : @MaybePresent Optional<@MaybePresent String>
  required: @Present Optional<@MaybePresent String>
1 error

Steps to Reproduce

Execute the test case with the following command:

javacheck -processor nonempty -ArunAsOptionalChecker -AassumePure Main.java

Expected Behavior: Main.java should cleanly type-check.

Actual Behavior: Main.java does not cleanly type-check.