Implement Java 8 type argument inference

[smillst]

The Checker Framework should implement Java 8 type inference for method type arguments, new class trees that use diamonds, and raw types. (Currently, the Checker Framework implements Java 7 type inference.)
This involves completely replacing/rewriting the implementation in the framework.utils.typeinference package. Also, the code that adds type arguments to raw types (AnnotatedDeclaredType#getTypeArguments) and the code that infers type arguments for diamonds (AnnotatedTypeFactory#fromNewClass) should be changed to use type argument inference.

The Java 8 algorithm specified in the JLS cannot be used as is. It must be adapted to use with annotated types. In particular, annotated types complicate the JLS algorithm in following ways.

1. In the JLS, if there is a subtyping constraint against a null type, the constraint is reduced to "true".[JLS #18.2.3] However, if null isn't annotation with the bottom qualifier, then the constraint should be reduced to new constraint where the primary annotation of the type must be a subtype of the annotation on null.

2. If a use of a type variable has a primary annotation, then constraints against that use should not include that annotation. In other words, that constraint should be against the Java type rather than the annotated type. But if the type system has a multigraph qualifier hierarchy, then there should still be a constraint against an annotated type for some of the hierarchies. (See examples in checker/tests/nullness/generics/MethodTypeVars7.java.)

3. A class can be marked with @Covariant to signify that one or more of its type parameters can be treated covariantly. Covariant type parameters should generate subtyping constraints rather than equality constraints.

4. Method postconditions. See The return type of filter should reflect the predicate's postconditions #1345.

Also, once Java 8 inference is implemented, the field AnnotatedWildcardType#uninferredTypeArgument should be removed and the -AconservativeUninferredTypeArguments option should also be removed.
In the meanwhile, if you are concerned that the Checker Framework is suffering false negatives due to this issue, use -AconservativeUninferredTypeArguments. A user reported that this required editing 0.5% of the lines of code in his project.

The following issues were closed in favor of this issue: #402, #404, #531, #953, #980, #1032. The test cases from those issues are now in framework/tests/all-systems/java8inferrence/ and checker/tests/nullness/java8inferrence/.

[wmdietlGC]

As people are adopting Stream-based APIs, I'm running into this issue very frequently.

I have a patch that instead of raising errors like:

Issue404.java:17: error: [return.type.incompatible] incompatible types in return.
        return strings.stream().map(String::trim).collect(Collectors.toSet());
                                                         ^
  found   : @Initialized @NonNull Set<? extends @Initialized @Nullable Object>
  required: @Initialized @NonNull Set<@Initialized @NonNull String>

allows uninferred wildcards as subtypes. The Nullness Checker then successfully compiles all examples in tests/all-systems/java8inference.
This is unsound, but there is currently no test case that would require an error. We should add one to highlight the problem.

The current error message isn't useful and very frustrating.
I would suggest making the default behavior unsound (it hurts me to say that...) and adding an option to use the current conservative behavior.

Let me know what you think.

[smillst]

#979 (comment) was implemented via bfeee16.

[wmdietlGC]

The following code:

import org.checkerframework.checker.nullness.qual.Nullable;
import java.util.function.BiFunction;
import java.util.function.Function;
import java.util.stream.Collector;
import java.util.Map;

class Demo {
  static <T, R, A> void use(@Nullable Collector<? super T, A, R> collector) { }

  static <T, K, V> @Nullable Collector<T, ?, Map<K,V>> calc(Function<? super T, ? extends K> keyFunction,
    Function<? super T, ? extends V> valueFunction,
    BiFunction<V, V, V> mergeFunction) { return null; }

  void foo(Function<Long, Float> f) {
    // No error when using a lambda
    use(calc(f, f, (a, b) -> Math.max(a, b)));
    // Error when using a method reference
    use(calc(f, f, Math::max));
  }
}

gives the following errors with the Nullness Checker:

Demo.java:18: error: [methodref.param.invalid] Incompatible parameter type for a
    use(calc(f, f, Math::max));
                   ^
  Method
    @Initialized @NonNull float max(@Initialized @NonNull float p0, @Initialized @NonNull float p1) in java.lang.Math
  is not a valid method reference for
    /*INFERENCE FAILED for:*/ ? extends @Initialized @Nullable Object apply(@Initialized @NonNull BiFunction</*INFERENCE FAILED for:*/ ? extends @Initialized @Nullable Object, /*INFERENCE FAILED for:*/ ? extends @Initialized @Nullable Object, /*INFERENCE FAILED for:*/ ? extends @Initialized @Nullable Object> this, /*INFERENCE FAILED for:*/ ? extends @Initialized @Nullable Object p0, /*INFERENCE FAILED for:*/ ? extends @Initialized @Nullable Object p1) in java.util.function.BiFunction
  found   : @Initialized @NonNull float
  required: /*INFERENCE FAILED for:*/ ? extends @Initialized @Nullable Object
Demo.java:18: error: [methodref.param.invalid] Incompatible parameter type for b
    use(calc(f, f, Math::max));
                   ^
  Method
    @Initialized @NonNull float max(@Initialized @NonNull float p0, @Initialized @NonNull float p1) in java.lang.Math
  is not a valid method reference for
    /*INFERENCE FAILED for:*/ ? extends @Initialized @Nullable Object apply(@Initialized @NonNull BiFunction</*INFERENCE FAILED for:*/ ? extends @Initialized @Nullable Object, /*INFERENCE FAILED for:*/ ? extends @Initialized @Nullable Object, /*INFERENCE FAILED for:*/ ? extends @Initialized @Nullable Object> this, /*INFERENCE FAILED for:*/ ? extends @Initialized @Nullable Object p0, /*INFERENCE FAILED for:*/ ? extends @Initialized @Nullable Object p1) in java.util.function.BiFunction
  found   : @Initialized @NonNull float
  required: /*INFERENCE FAILED for:*/ ? extends @Initialized @Nullable Object
2 errors

Note how the equivalent, but more verbose, lambda expression works without errors.

I would have expected these errors to be suppressed by default, because the types contain INFERENCE FAILED. Maybe that suppression is implemented for lambdas but not for method references?
Maybe this can be fixed independently of the larger fix for #979?

[msridhar]

@wmdietlGC #3044 was the previous attempt to suppress these types of warnings by default, I think. #3568 shows another example where errors are still reported with INFERENCE FAILED. Maybe open a new issue for the case above? IMO all such errors should be suppressed by default.

[wmdietlGC]

@msridhar Thanks for the cross-references! I've opened #3764.