Fix problem with type var in a method reference

framework/src/main/java/org/checkerframework/framework/util/element/ElementAnnotationUtil.java

@@ -327,7 +327,7 @@ private static void addWildcardToBoundMap(
    * Returns true if the typeCompound is a primary annotation for the type it targets (or lower
    * bound if this is a type variable or wildcard ). If you think of a type as a tree-like structure
    * then a nested type any type that is not the root. E.g. {@code @T List< @N String>}, @T is on a
-   * top-level NON-nested type where as the annotation @N is on a nested type.
+   * top-level NON-nested type whereas the annotation @N is on a nested type.
    *
    * @param typeCompound the type compound to inspect
    * @return true if typeCompound is placed on a nested type, false otherwise

framework/src/main/java/org/checkerframework/framework/util/typeinference8/DefaultTypeArgumentInference.java

@@ -45,7 +45,7 @@ public DefaultTypeArgumentInference() {}
   public InferenceResult inferTypeArgs(
       AnnotatedTypeFactory typeFactory,
       ExpressionTree expressionTree,
-      AnnotatedExecutableType methodType) {
+      AnnotatedExecutableType executableType) {
     TreePath pathToExpression = typeFactory.getPath(expressionTree);
 
     // In order to find the type arguments for expressionTree, type arguments for outer method
@@ -94,7 +94,7 @@ public InferenceResult inferTypeArgs(
             "Unexpected kind of outer expression to infer type arguments: %s", outerTree.getKind());
       }
     } else {
-      outerMethodType = methodType;
+      outerMethodType = executableType;
     }
     if (java8Inference != null) {
       java8InferenceStack.push(java8Inference);
@@ -110,7 +110,7 @@ public InferenceResult inferTypeArgs(
           java8Inference.context.pathToExpression = typeFactory.getPath(expressionTree);
           return java8Inference.infer(mrt2);
         }
-        return result.swapTypeVariables(methodType, expressionTree);
+        return result.swapTypeVariables(executableType, expressionTree);
       }
     } catch (Exception ex) {
       if (typeFactory

framework/src/main/java/org/checkerframework/framework/util/typeinference8/InferenceResult.java

@@ -171,17 +171,17 @@ public String getErrorMsg() {
 
   /**
    * Switch the {@link TypeVariable}s in {@code results} with the {@code TypeVariable}s in {@code
-   * methodType} so that the {@code TypeVariable}s in the result are {@code .equals}. {@link
+   * executableType} so that the {@code TypeVariable}s in the result are {@code .equals}. {@link
    * TypesUtils#areSame(TypeVariable, TypeVariable)} is used to decide which type variables to swap.
    *
-   * @param methodType annotated method type
+   * @param executableType annotated method type
    * @param tree method invocation tree
    * @return this
    */
   /* package-private */ InferenceResult swapTypeVariables(
-      AnnotatedExecutableType methodType, ExpressionTree tree) {
+      AnnotatedExecutableType executableType, ExpressionTree tree) {
     Map<TypeVariable, AnnotatedTypeMirror> map = results.get(tree);
-    for (AnnotatedTypeVariable tv : methodType.getTypeVariables()) {
+    for (AnnotatedTypeVariable tv : executableType.getTypeVariables()) {
       TypeVariable typeVariable = tv.getUnderlyingType();
       for (TypeVariable t : new HashSet<>(map.keySet())) {
         if (TypesUtils.areSame(t, typeVariable)) {

framework/src/main/java/org/checkerframework/framework/util/typeinference8/InvocationTypeInference.java

@@ -27,9 +27,11 @@
 import org.checkerframework.framework.util.typeinference8.constraint.Expression;
 import org.checkerframework.framework.util.typeinference8.constraint.TypeConstraint;
 import org.checkerframework.framework.util.typeinference8.constraint.Typing;
+import org.checkerframework.framework.util.typeinference8.types.AbstractExecutableType;
+import org.checkerframework.framework.util.typeinference8.types.AbstractInvocationType;
 import org.checkerframework.framework.util.typeinference8.types.AbstractType;
+import org.checkerframework.framework.util.typeinference8.types.CompileTimeDeclarationType;
 import org.checkerframework.framework.util.typeinference8.types.InferenceType;
-import org.checkerframework.framework.util.typeinference8.types.InvocationType;
 import org.checkerframework.framework.util.typeinference8.types.ProperType;
 import org.checkerframework.framework.util.typeinference8.types.UseOfVariable;
 import org.checkerframework.framework.util.typeinference8.types.Variable;
@@ -141,14 +143,15 @@ public Tree getInferenceExpression() {
    * 18.5.2</a>.
    *
    * @param invocation invocation which needs inference
-   * @param methodType type of the method invocation
+   * @param executableType type of the method invocation
    * @return the result of inference
    * @throws FalseBoundException if inference fails because of the java types
    */
-  public InferenceResult infer(ExpressionTree invocation, AnnotatedExecutableType methodType)
+  public InferenceResult infer(ExpressionTree invocation, AnnotatedExecutableType executableType)
       throws FalseBoundException {
-    ExecutableType e = methodType.getUnderlyingType();
-    InvocationType invocationType = new InvocationType(methodType, e, invocation, context);
+    ExecutableType e = executableType.getUnderlyingType();
+    AbstractExecutableType inferenceExectuableType =
+        new AbstractInvocationType(executableType, e, invocation, context);
     ProperType target = context.inferenceTypeFactory.getTargetType();
     List<? extends ExpressionTree> args;
     if (invocation instanceof MethodInvocationTree mit) {
@@ -158,15 +161,16 @@ public InferenceResult infer(ExpressionTree invocation, AnnotatedExecutableType
     }
 
     Theta map =
-        context.inferenceTypeFactory.createThetaForInvocation(invocation, invocationType, context);
-    BoundSet b2 = createB2(invocationType, args, map);
+        context.inferenceTypeFactory.createThetaForInvocation(
+            invocation, inferenceExectuableType, context);
+    BoundSet b2 = createB2(inferenceExectuableType, args, map);
     BoundSet b3;
     if (target != null && TreeUtils.isPolyExpression(invocation)) {
-      b3 = createB3(b2, invocation, invocationType, target, map);
+      b3 = createB3(b2, invocation, inferenceExectuableType, target, map);
     } else {
       b3 = b2;
     }
-    ConstraintSet c = createC(invocationType, args, map);
+    ConstraintSet c = createC(inferenceExectuableType, args, map);
 
     BoundSet b4 = getB4(b3, c);
     b4.resolve();
@@ -200,7 +204,7 @@ public InferenceResult infer(MemberReferenceTree invocation) throws FalseBoundEx
       throw new BugInCF("Target of method reference should not be null: %s", invocation);
     }
 
-    InvocationType compileTimeDecl =
+    CompileTimeDeclarationType compileTimeDecl =
         context.inferenceTypeFactory.compileTimeDeclarationType(invocation);
     Theta map =
         context.inferenceTypeFactory.createThetaForMethodReference(
@@ -230,7 +234,7 @@ public InferenceResult infer(MemberReferenceTree invocation) throws FalseBoundEx
    * <ol>
    *   <li value="1">Creating the inference variables and initializing their bounds based on the
    *       type parameter declaration.
-   *   <li value="2">Adding any bounds implied by the throws clause of {@code methodType}.
+   *   <li value="2">Adding any bounds implied by the throws clause of {@code executableType}.
    *   <li value="3">Constructing constraints between formal parameters and arguments that are
    *       "pertinent to applicability" (See <a
    *       href="https://docs.oracle.com/javase/specs/jls/se11/html/jls-15.html#jls-15.12.2.2">JLS
@@ -240,27 +244,27 @@ public InferenceResult infer(MemberReferenceTree invocation) throws FalseBoundEx
    *   <li value="4">Reducing and incorporating those constraints which finally produces B2.
    * </ol>
    *
-   * @param methodType the type of the method or constructor invoked
+   * @param executableType the type of the method or constructor invoked
    * @param args argument expression tress
    * @param map map of type variables to (inference) variables
    * @return bound set used to determine whether a method is applicable
    */
   public BoundSet createB2(
-      InvocationType methodType, List<? extends ExpressionTree> args, Theta map) {
+      AbstractExecutableType executableType, List<? extends ExpressionTree> args, Theta map) {
     BoundSet b0 = BoundSet.initialBounds(map, context);
 
     // For all i (1 <= i <= p), if Pi appears in the throws clause of m, then the bound throws
     // alphai is implied. These bounds, if any, are incorporated with B0 to produce a new bound
     // set, B1.
-    for (AbstractType thrownType : methodType.getThrownTypes(map)) {
+    for (AbstractType thrownType : executableType.getThrownTypes(map)) {
       if (thrownType.isUseOfVariable()) {
         ((UseOfVariable) thrownType).setHasThrowsBound(true);
       }
     }
 
     BoundSet b1 = b0;
     ConstraintSet c = new ConstraintSet();
-    List<AbstractType> formals = methodType.getParameterTypes(map, args.size());
+    List<AbstractType> formals = executableType.getParameterTypes(map, args.size());
 
     for (int i = 0; i < formals.size(); i++) {
       ExpressionTree ei = args.get(i);
@@ -279,31 +283,32 @@ public BoundSet createB2(
   }
 
   /**
-   * Same as {@link #createB2(InvocationType, List, Theta)}, but for method references. A list of
-   * types is used instead of a list of arguments. These types are the types of the formal
+   * Same as {@link #createB2(AbstractExecutableType, List, Theta)}, but for method references. A
+   * list of types is used instead of a list of arguments. These types are the types of the formal
    * parameters of function type of target type of the method reference.
    *
-   * @param methodType the type of the method or constructor invoked
+   * @param executableType the type of the method or constructor invoked
    * @param args types to use as arguments
    * @param map map of type variables to (inference) variables
    * @return bound set used to determine whether a method is applicable
    */
-  public BoundSet createB2MethodRef(InvocationType methodType, List<AbstractType> args, Theta map) {
+  public BoundSet createB2MethodRef(
+      CompileTimeDeclarationType executableType, List<AbstractType> args, Theta map) {
     BoundSet b0 = BoundSet.initialBounds(map, context);
 
     // For all i (1 <= i <= p), if Pi appears in the throws clause of m, then the bound throws
     // alphai is implied. These bounds, if any, are incorporated with B0 to produce a new bound
     // set, B1.
-    for (AbstractType thrownType : methodType.getThrownTypes(map)) {
+    for (AbstractType thrownType : executableType.getThrownTypes(map)) {
       if (thrownType.isUseOfVariable()) {
         ((UseOfVariable) thrownType).setHasThrowsBound(true);
       }
     }
 
     BoundSet b1 = b0;
     ConstraintSet c = new ConstraintSet();
-    List<AbstractType> formals = methodType.getParameterTypes(map, args.size());
-    if (TreeUtils.isLikeDiamondMemberReference(methodType.getInvocation())) {
+    List<AbstractType> formals = executableType.getParameterTypes(map, args.size());
+    if (TreeUtils.isLikeDiamondMemberReference(executableType.getMethodRef())) {
       // https://docs.oracle.com/javase/specs/jls/se19/html/jls-15.html#jls-15.13.1
       //  If ReferenceType is a raw type, and there exists a parameterization of this type,
       // G<...>, that is a supertype of P1, the type to search is the result of capture
@@ -320,7 +325,7 @@ public BoundSet createB2MethodRef(InvocationType methodType, List<AbstractType>
       String source =
           String.format(
               "Method reference: %s, constraint against arguments, index %s.",
-              methodType.getInvocation(), i);
+              executableType.getMethodRef(), i);
       c.add(new Typing(source, ei, fi, Kind.TYPE_COMPATIBILITY));
     }
 
@@ -337,20 +342,20 @@ public BoundSet createB2MethodRef(InvocationType methodType, List<AbstractType>
    * href="https://docs.oracle.com/javase/specs/jls/se11/html/jls-18.html#jls-18.5.2.1">JLS
    * 18.5.2.1</a>.)
    *
-   * @param b2 BoundSet created by {@link #createB2(InvocationType, List, Theta)}
+   * @param b2 BoundSet created by {@link #createB2(AbstractExecutableType, List, Theta)}
    * @param invocation a method or constructor invocation
-   * @param methodType the type of the method or constructor invoked by expression
+   * @param executableType the type of the method or constructor invoked by expression
    * @param target target type of the invocation
    * @param map map of type variables to (inference) variables
    * @return bound set created by constraints against the target type of the invocation
    */
   public BoundSet createB3(
       BoundSet b2,
       ExpressionTree invocation,
-      InvocationType methodType,
+      AbstractExecutableType executableType,
       AbstractType target,
       Theta map) {
-    AbstractType r = methodType.getReturnType(map);
+    AbstractType r = executableType.getReturnType(map);
     if (b2.isUncheckedConversion()) {
       // If unchecked conversion was necessary for the method to be applicable during
       // constraint set reduction in 18.5.1, the constraint formula <|R| -> T> is reduced and
@@ -443,16 +448,16 @@ public BoundSet createB3(
    * href="https://docs.oracle.com/javase/specs/jls/se11/html/jls-18.html#jls-18.5.2.2">JLS
    * 18.5.2.2</a>.)
    *
-   * @param methodType type of method invoked
+   * @param executableType type of method invoked
    * @param args argument expression trees
    * @param map map from type variable to inference variable
    * @return the constraints between the formal parameters and arguments that are not pertinent to
    *     applicability
    */
   public ConstraintSet createC(
-      InvocationType methodType, List<? extends ExpressionTree> args, Theta map) {
+      AbstractExecutableType executableType, List<? extends ExpressionTree> args, Theta map) {
     ConstraintSet c = new ConstraintSet();
-    List<AbstractType> formals = methodType.getParameterTypes(map, args.size());
+    List<AbstractType> formals = executableType.getParameterTypes(map, args.size());
 
     for (int i = 0; i < formals.size(); i++) {
       ExpressionTree ei = args.get(i);
@@ -475,7 +480,7 @@ public ConstraintSet createC(
 
   /**
    * Adds argument constraints for the argument {@code ei} and its subexpressions. These are in
-   * addition to the constraints added in {@link #createC(InvocationType, List, Theta)}.
+   * addition to the constraints added in {@link #createC(AbstractExecutableType, List, Theta)}.
    *
    * <p>It does this by traversing {@code ei} if it is a method reference, lambda, method
    * invocation, new class tree, conditional expression, switch expression, or parenthesized

framework/src/main/java/org/checkerframework/framework/util/typeinference8/TypeArgumentInference.java

@@ -32,15 +32,15 @@ public interface TypeArgumentInference {
   /**
    * Infer the type arguments for the method or constructor invocation given by invocation.
    *
-   * @param typeFactory the type factory used to create methodType
+   * @param typeFactory the type factory used to create executableType
    * @param invocation a tree representing the method or constructor invocation for which we are
    *     inferring type arguments
-   * @param methodType the declaration type of method elem
+   * @param executableType the declaration type of method elem
    * @return the result which includes the inferred type arguments or an error message if they were
    *     not inferred
    */
   InferenceResult inferTypeArgs(
       AnnotatedTypeFactory typeFactory,
       ExpressionTree invocation,
-      AnnotatedExecutableType methodType);
+      AnnotatedExecutableType executableType);
 }

framework/src/main/java/org/checkerframework/framework/util/typeinference8/constraint/AdditionalArgument.java

@@ -3,8 +3,7 @@
 import com.sun.source.tree.ExpressionTree;
 import com.sun.source.tree.MethodInvocationTree;
 import com.sun.source.tree.NewClassTree;
-import com.sun.source.tree.Tree.Kind;
-import org.checkerframework.framework.util.typeinference8.types.InvocationType;
+import org.checkerframework.framework.util.typeinference8.types.AbstractExecutableType;
 import org.checkerframework.framework.util.typeinference8.util.Java8InferenceContext;
 import org.checkerframework.framework.util.typeinference8.util.Theta;
 
@@ -39,24 +38,25 @@ public Kind getKind() {
   @Override
   public ConstraintSet reduce(Java8InferenceContext context) {
     if (methodOrConstructorInvocation instanceof MethodInvocationTree methodInvocation) {
-      InvocationType methodType =
+      AbstractExecutableType executableType =
           context.inferenceTypeFactory.getTypeOfMethodAdaptedToUse(methodInvocation);
       Theta newMap =
           context.inferenceTypeFactory.createThetaForInvocation(
-              methodInvocation, methodType, context);
+              methodInvocation, executableType, context);
       ConstraintSet set =
-          context.inference.createC(methodType, methodInvocation.getArguments(), newMap);
+          context.inference.createC(executableType, methodInvocation.getArguments(), newMap);
       set.applyInstantiations();
       return set;
     } else {
       NewClassTree newClassTree = (NewClassTree) methodOrConstructorInvocation;
-      InvocationType methodType =
+      AbstractExecutableType executableType =
           context.inferenceTypeFactory.getTypeOfMethodAdaptedToUse(newClassTree);
 
       Theta newMap =
-          context.inferenceTypeFactory.createThetaForInvocation(newClassTree, methodType, context);
+          context.inferenceTypeFactory.createThetaForInvocation(
+              newClassTree, executableType, context);
       ConstraintSet set =
-          context.inference.createC(methodType, newClassTree.getArguments(), newMap);
+          context.inference.createC(executableType, newClassTree.getArguments(), newMap);
       set.applyInstantiations();
       return set;
     }

framework/src/main/java/org/checkerframework/framework/util/typeinference8/constraint/Expression.java

@@ -14,9 +14,10 @@
 import javax.lang.model.type.TypeKind;
 import org.checkerframework.framework.type.AnnotatedTypeMirror;
 import org.checkerframework.framework.util.typeinference8.bound.BoundSet;
+import org.checkerframework.framework.util.typeinference8.types.AbstractExecutableType;
 import org.checkerframework.framework.util.typeinference8.types.AbstractType;
+import org.checkerframework.framework.util.typeinference8.types.CompileTimeDeclarationType;
 import org.checkerframework.framework.util.typeinference8.types.InferenceType;
-import org.checkerframework.framework.util.typeinference8.types.InvocationType;
 import org.checkerframework.framework.util.typeinference8.types.ProperType;
 import org.checkerframework.framework.util.typeinference8.types.Variable;
 import org.checkerframework.framework.util.typeinference8.util.Java8InferenceContext;
@@ -172,12 +173,13 @@ private BoundSet reduceMethodInvocation(Java8InferenceContext context) {
       args = methodInvocationTree.getArguments();
     }
 
-    InvocationType methodType =
+    AbstractExecutableType executableType =
         context.inferenceTypeFactory.getTypeOfMethodAdaptedToUse(expressionTree);
     Theta map =
-        context.inferenceTypeFactory.createThetaForInvocation(expressionTree, methodType, context);
-    BoundSet b2 = context.inference.createB2(methodType, args, map);
-    return context.inference.createB3(b2, expressionTree, methodType, T, map);
+        context.inferenceTypeFactory.createThetaForInvocation(
+            expressionTree, executableType, context);
+    BoundSet b2 = context.inference.createB2(executableType, args, map);
+    return context.inference.createB3(b2, expressionTree, executableType, T, map);
   }
 
   /**
@@ -190,7 +192,7 @@ private BoundSet reduceMethodInvocation(Java8InferenceContext context) {
   private ReductionResult reduceMethodRef(Java8InferenceContext context) {
     MemberReferenceTree memRef = (MemberReferenceTree) expression;
     if (TreeUtils.isExactMethodReference(memRef)) {
-      InvocationType typeOfPoAppMethod =
+      CompileTimeDeclarationType typeOfPoAppMethod =
           context.inferenceTypeFactory.compileTimeDeclarationType(memRef);
 
       ConstraintSet constraintSet = new ConstraintSet();
@@ -229,7 +231,7 @@ private ReductionResult reduceMethodRef(Java8InferenceContext context) {
     // else the method reference is inexact.
 
     // Compile-time declaration of the member reference expression
-    InvocationType compileTimeDecl =
+    CompileTimeDeclarationType compileTimeDecl =
         context.inferenceTypeFactory.compileTimeDeclarationType(memRef);
     if (compileTimeDecl.isVoid()) {
       return ConstraintSet.TRUE;