The return type of filter should reflect the predicate's postconditions

When calling Stream.filter(), Opt.filter(), and (in Java 8) Optional.filter(), the return type should take account of the postconditions on the predicate.

Here is a test case, which is committed as checker/tests/nullness/flow/Issue1345.java but currently disabled:

// Test case for issue #1345:
// https://github.com/typetools/checker-framework/issues/1345
// @below-java8-jdk-skip-test

// @skip-test until the issue is resolved

import java.math.BigDecimal;
import java.util.stream.Stream;
import org.checkerframework.checker.nullness.Opt;
import org.checkerframework.checker.nullness.qual.*;

public class Issue1345 {

    @EnsuresNonNullIf(expression = "#1", result = true)
    static boolean isNonNull(@Nullable Object o) {
        return o != null;
    }

    void filterPresent_Optional(Stream<@Nullable BigDecimal> s) {
        Stream<@NonNull BigDecimal> filtered = s.<BigDecimal>filter(Issue1345::isNonNull);
    }

    void filterPresent_Opt(@Nullable Object p) {
        @NonNull Object o = Opt.filter(p, Opt::isPresent);
    }
}

Here is the Nullness Checker output:

Issue1345.java:20: error: [assignment.type.incompatible] incompatible types in assignment.
        Stream<@NonNull BigDecimal> filtered = s.<BigDecimal>filter(TestFilter::isNonNull);
                                                                   ^
  found   : @Initialized @NonNull Stream<@Initialized @Nullable BigDecimal>
  required: @UnknownInitialization @Nullable Stream<@Initialized @NonNull BigDecimal>
Issue1345.java:24: error: [assignment.type.incompatible] incompatible types in assignment.
        @NonNull Object o = Opt.filter(p, Opt::isPresent);
                                      ^
  found   : @Initialized @Nullable Object
  required: @UnknownInitialization @NonNull Object
2 errors

I am interested in a different checker than the Nullness Checker, but it is convenient to show the test case for the Nullness Checker.

Start with the disabled test in checker/tests/nullness/flow/Issue1345.java and review the examples for Stream.filter(), Opt.filter(), and Optional.filter() in the issue. Run the test to reproduce the two assignment errors. Done means the test passes with filtered values recognized according to the predicate's postconditions.