Optional checker: possible erroneous report of an incompatible method receiver for `Optional#get` in a `Stream#map`

[jyoo980]

trafficstars

Summary

Running the Optional checker on code that contains a call to Optional#get within a call to .map on a Java stream produces an error reporting to an incompatible method receiver.

Commands executed

Using the latest commit on the master branch of the Checker Framework, where javacheck is an alias for javac included in the Checker Framework's binary distribution.

javacheck -processor optional Main.java

Input

This is a minimal test case that should be able to trigger this issue

import java.util.List;
import java.util.Optional;
import java.util.stream.Collectors;

public class Main {

  public List<Integer> getOnlyPresentInts(List<Optional<Integer>> optInts) {
    return optInts.stream()
      .map(Optional::get)
      .collect(Collectors.toList());
  }
}

Actual output

Main.java:9: warning: [optional.as.element.type] Don't use Optional as the element type in a collection.
  public List<Integer> getOnlyPresentInts(List<Optional<Integer>> optInts) {
                                                                  ^
Main.java:11: error: [methodref.receiver] Incompatible receiver type
      .map(Optional::get)
           ^
  found   : @Present Optional<@MaybePresent Integer>
  required: @MaybePresent Optional<@MaybePresent Integer>
  Consequence: method in @MaybePresent Optional<@MaybePresent Integer>
    @MaybePresent Integer get(@Present Optional<@MaybePresent Integer> this)
  is not a valid method reference for method in @MaybePresent Function<@MaybePresent Optional<@MaybePresent Integer>, @MaybePresent Integer>
    @MaybePresent Integer apply(@MaybePresent Function<@MaybePresent Optional<@MaybePresent Integer>, @MaybePresent Integer> this, @MaybePresent Optional<@MaybePresent Integer> p0)
1 error
1 warning

Expected output

There should technically be no error about an incompatible method receiver, as calling .stream() on an object of type List<Optional<Integer>> should evaluate to an object of type Stream<Optional<Integer>>.

Additionally, the error line

Main.java:11: error: [methodref.receiver] Incompatible receiver type
      .map(Optional::get)
           ^
  found   : @Present Optional<@MaybePresent Integer>
  required: @MaybePresent Optional<@MaybePresent Integer>

Is confusing to me, shouldn't the found type be annotated with @MaybePresent? Since the manual states

@MaybePresent The annotated Optional container may or may not contain a value. This is the default type, so programmers do not have to write it.

However, this might be a misunderstanding of the Optional checker's type system on my part.

[smillst]

This is a true positive warning that is trying to prevent the following crash:

import java.util.ArrayList;
import java.util.List;
import java.util.Optional;
import java.util.stream.Collectors;

public class Main {

  public static List<Integer> getOnlyPresentInts(List<Optional<Integer>> optInts) {
    return optInts.stream()
        .map(Optional::get)
        .collect(Collectors.toList());
  }

  public static void main(String[] args) {
    List<Optional<Integer>> list = new ArrayList<>();
    list.add(Optional.empty());
    getOnlyPresentInts(list);
  }
}

Which if you run this test gives the following exception:

Exception in thread "main" java.util.NoSuchElementException: No value present
	at java.base/java.util.Optional.get(Optional.java:143)
	at java.base/java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:197)
	at java.base/java.util.ArrayList$ArrayListSpliterator.forEachRemaining(ArrayList.java:1708)
	at java.base/java.util.stream.AbstractPipeline.copyInto(AbstractPipeline.java:509)
	at java.base/java.util.stream.AbstractPipeline.wrapAndCopyInto(AbstractPipeline.java:499)
	at java.base/java.util.stream.ReduceOps$ReduceOp.evaluateSequential(ReduceOps.java:921)
	at java.base/java.util.stream.AbstractPipeline.evaluate(AbstractPipeline.java:234)
	at java.base/java.util.stream.ReferencePipeline.collect(ReferencePipeline.java:682)
	at Main.getOnlyPresentInts(Main.java:11)
	at Main.main(Main.java:17)

If you annotate the type of optInts like this: List<@Present Optional<Integer>>, then the methodref.receiver warning goes away. (Then there are new errors at the call to getOnlyPresentInts).

[jyoo980]

Thanks for looking into this, Suzanne.

This is interesting, the test case I provided was a reduction of an error that Mike and I observed in a project for which the annotations were inferred via WPI, I wonder if this means there's a limitation to the types being inferred or if this is another issue altogether (or not one at all)

[smillst]

I bet the full example included a call to filter:

optInts.stream().filter(Optional::isPresent)
        .map(Optional::get)
        .collect(Collectors.toList());

In that case, the code should type check (even without @Present on the type of optInts), but won't because of https://github.com/typetools/checker-framework/issues/1345.

[jyoo980]

You're right, here's the block of code in question that failed to type-check

if (userDTO.getAuthorities() != null) {
    Set<Authority> authorities = userDTO.getAuthorities().stream()
      .map(authorityRepository::findById
      .filter(Optional::isPresent)                   // a .filter
      .map(Optional::get)
      .collect(Collectors.toSet());
    user.setAuthorities(authorities);
}

So it looks like this is just a trigger for a known issue (#1345). Thanks.

@mernst, do you have any thoughts on how we should be handling this in our analysis of the typecheck results from WPI? We could ignore them for now, and look at the other types of errors that might surface, as you suggested.

That said, I think this is something worth fixing, as the pattern of filtering for present and mapping is definitely something I've seen in a bunch of codebases while working.

[mernst]

I suggest that we should focus on other issues when examining Optional Checker output, and we should prioritize #1345. @smillst is the latter something you could do?