Correct the way explicit annotations are handled in type argument inference

Author: smillst

checker/tests/nullness/Issue6740.java

@@ -0,0 +1,20 @@
+package open.falsepos;
+
+import java.util.Optional;
+import org.checkerframework.checker.nullness.qual.NonNull;
+import org.checkerframework.checker.nullness.qual.Nullable;
+
+public class Issue6740 {
+
+  static <A> Optional<@NonNull A> ofNullable(@Nullable A value) {
+    throw new RuntimeException();
+  }
+
+  <B> @Nullable B getNullable(Class<B> type) {
+    throw new RuntimeException();
+  }
+
+  <C> Optional<@NonNull C> getOpt(int index, Class<C> type) {
+    return ofNullable(getNullable(type));
+  }
+}

checker/tests/nullness/flow/TestNullnessUtil.java

@@ -23,7 +23,7 @@ void testArr1(@Nullable Object @NonNull [] a) {
     // one way to use as a cast:
     @NonNull Object[] l2 = NullnessUtil.castNonNullDeep(a);
     // Careful, the non-deep version only casts the main modifier.
-    // :: error: (type.arguments.not.inferred) :: error: (assignment)
+    // :: error: (assignment)
     @NonNull Object[] l2b = NullnessUtil.castNonNull(a);
     // OK
     @Nullable Object[] l2c = NullnessUtil.castNonNull(a);
@@ -33,7 +33,7 @@ void testArr1b(@Nullable Object @Nullable [] a) {
     // one way to use as a cast:
     @NonNull Object[] l2 = NullnessUtil.castNonNullDeep(a);
     // Careful, the non-deep version only casts the main modifier.
-    // :: error: (type.arguments.not.inferred) :: error: (assignment)
+    // :: error: (assignment)
     @NonNull Object[] l2b = NullnessUtil.castNonNull(a);
     // OK
     @Nullable Object[] l2c = NullnessUtil.castNonNull(a);

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

@@ -91,7 +91,7 @@ public ReductionResult reduce(Java8InferenceContext context) {
         s = new ProperType(expression, context);
       } else {
         AnnotatedTypeMirror atm = context.typeFactory.getAnnotatedType(expression);
-        s = getT().create(atm, atm.getUnderlyingType());
+        s = getT().create(atm, atm.getUnderlyingType(), false);
       }
       return new Typing(this, s, T, TypeConstraint.Kind.TYPE_COMPATIBILITY);
     }
@@ -200,7 +200,7 @@ private ReductionResult reduceMethodRef(Java8InferenceContext context) {
         AbstractType referenceType;
         if (context.isLambdaParam(preColonTree)) {
           AnnotatedTypeMirror atm = context.typeFactory.getAnnotatedType(preColonTree);
-          referenceType = T.create(atm, atm.getUnderlyingType());
+          referenceType = T.create(atm, atm.getUnderlyingType(), false);
         } else {
           if (MemberReferenceKind.getMemberReferenceKind(memRef).isUnbound()) {
             AnnotatedTypeMirror atm =

framework/src/main/java/org/checkerframework/framework/util/typeinference8/types/AbstractType.java

@@ -68,14 +68,19 @@ public enum Kind {
   /** The {@link AnnotatedTypeFactory}. */
   protected final AnnotatedTypeFactory typeFactory;
 
+  /** Whether the annotations on this type should be ignored. */
+  public final boolean ignoreAnnotations;
+
   /**
    * Creates an {@link AbstractType}.
    *
    * @param context the context object
+   * @param ignoreAnnotations whether the annotations on this type should be ignored
    */
-  protected AbstractType(Java8InferenceContext context) {
+  protected AbstractType(Java8InferenceContext context, boolean ignoreAnnotations) {
     this.context = context;
     this.typeFactory = context.typeFactory;
+    this.ignoreAnnotations = ignoreAnnotations;
   }
 
   /**
@@ -126,9 +131,11 @@ public final TypeKind getTypeKind() {
    *
    * @param atm annotated type mirror
    * @param type type mirror
+   * @param ignoreAnnotations whether the annotations on this type should be ignored
    * @return the new type
    */
-  public abstract AbstractType create(AnnotatedTypeMirror atm, TypeMirror type);
+  public abstract AbstractType create(
+      AnnotatedTypeMirror atm, TypeMirror type, boolean ignoreAnnotations);
 
   /**
    * Return the underlying Java type without inference variables.
@@ -183,7 +190,9 @@ public List<ProperType> getTypeParameterBounds() {
 
     for (AnnotatedTypeParameterBounds bound : typeVars) {
       TypeVariable typeVariable = (TypeVariable) javaEle.next().asType();
-      bounds.add(new ProperType(bound.getUpperBound(), typeVariable.getUpperBound(), context));
+      bounds.add(
+          new ProperType(
+              bound.getUpperBound(), typeVariable.getUpperBound(), context, ignoreAnnotations));
     }
     return bounds;
   }
@@ -197,7 +206,7 @@ public List<ProperType> getTypeParameterBounds() {
   public AbstractType capture(Java8InferenceContext context) {
     AnnotatedTypeMirror capturedType =
         context.typeFactory.applyCaptureConversion(getAnnotatedType());
-    return create(capturedType, capturedType.getUnderlyingType());
+    return create(capturedType, capturedType.getUnderlyingType(), ignoreAnnotations);
   }
 
   /**
@@ -228,7 +237,7 @@ public AbstractType asSuper(TypeMirror superType) {
         AnnotatedTypeMirror.createType(superType, typeFactory, type.isDeclaration());
     typeFactory.initializeAtm(superAnnotatedType);
     AnnotatedTypeMirror asSuper = AnnotatedTypes.asSuper(typeFactory, type, superAnnotatedType);
-    return create(asSuper, asSuper.getUnderlyingType());
+    return create(asSuper, asSuper.getUnderlyingType(), ignoreAnnotations);
   }
 
   /**
@@ -277,7 +286,7 @@ public AbstractType getFunctionTypeReturnType() {
       if (returnType.getKind() == TypeKind.VOID) {
         return null;
       }
-      return create(returnType, returnTypeJava);
+      return create(returnType, returnTypeJava, ignoreAnnotations);
     } else {
       return null;
     }
@@ -297,7 +306,7 @@ public List<AbstractType> getFunctionTypeParameterTypes() {
       List<AbstractType> params = new ArrayList<>();
       Iterator<? extends TypeMirror> iter = paramsTypeMirror.iterator();
       for (AnnotatedTypeMirror param : pair.first.getParameterTypes()) {
-        params.add(create(param, iter.next()));
+        params.add(create(param, iter.next(), ignoreAnnotations));
       }
       return params;
     } else {
@@ -385,7 +394,7 @@ public AbstractType replaceTypeArgs(List<AbstractType> args) {
     }
     newType.setTypeArguments(argTypes);
     newType.replaceAnnotations(getAnnotatedType().getPrimaryAnnotations());
-    return create(newType, newTypeJava);
+    return create(newType, newTypeJava, ignoreAnnotations);
   }
 
   /**
@@ -416,7 +425,7 @@ public AbstractType getMostSpecificArrayType() {
       TypeMirror typeMirror =
           TypesUtils.getMostSpecificArrayType(getJavaType(), context.modelTypes);
       if (msat != null) {
-        return create(msat, typeMirror);
+        return create(msat, typeMirror, ignoreAnnotations);
       }
       return null;
     }
@@ -466,7 +475,7 @@ public List<AbstractType> getIntersectionBounds() {
     List<AbstractType> bounds = new ArrayList<>();
     for (AnnotatedTypeMirror bound :
         ((AnnotatedIntersectionType) getAnnotatedType()).directSupertypes()) {
-      bounds.add(create(bound, iter.next()));
+      bounds.add(create(bound, iter.next(), ignoreAnnotations));
     }
     return bounds;
   }
@@ -478,7 +487,10 @@ public List<AbstractType> getIntersectionBounds() {
    */
   public AbstractType getTypeVarUpperBound() {
     TypeMirror javaUpperBound = ((TypeVariable) getJavaType()).getUpperBound();
-    return create(((AnnotatedTypeVariable) getAnnotatedType()).getUpperBound(), javaUpperBound);
+    return create(
+        ((AnnotatedTypeVariable) getAnnotatedType()).getUpperBound(),
+        javaUpperBound,
+        ignoreAnnotations);
   }
 
   /**
@@ -490,7 +502,10 @@ public AbstractType getTypeVarUpperBound() {
    */
   public AbstractType getTypeVarLowerBound() {
     TypeMirror lowerBound = ((TypeVariable) getJavaType()).getLowerBound();
-    return create(((AnnotatedTypeVariable) getAnnotatedType()).getLowerBound(), lowerBound);
+    return create(
+        ((AnnotatedTypeVariable) getAnnotatedType()).getLowerBound(),
+        lowerBound,
+        ignoreAnnotations);
   }
 
   /**
@@ -530,7 +545,7 @@ public List<AbstractType> getTypeArguments() {
     List<AbstractType> list = new ArrayList<>();
     for (AnnotatedTypeMirror typeArg :
         ((AnnotatedDeclaredType) getAnnotatedType()).getTypeArguments()) {
-      list.add(create(typeArg, iter.next()));
+      list.add(create(typeArg, iter.next(), ignoreAnnotations));
     }
     return list;
   }
@@ -571,7 +586,9 @@ public AbstractType getWildcardLowerBound() {
     if (getJavaType().getKind() == TypeKind.WILDCARD) {
       WildcardType wild = (WildcardType) getJavaType();
       return create(
-          ((AnnotatedWildcardType) getAnnotatedType()).getSuperBound(), wild.getSuperBound());
+          ((AnnotatedWildcardType) getAnnotatedType()).getSuperBound(),
+          wild.getSuperBound(),
+          ignoreAnnotations);
     }
     return null;
   }
@@ -587,7 +604,10 @@ public AbstractType getWildcardUpperBound() {
       if (upperBoundJava == null) {
         upperBoundJava = context.object.getJavaType();
       }
-      return create(((AnnotatedWildcardType) getAnnotatedType()).getExtendsBound(), upperBoundJava);
+      return create(
+          ((AnnotatedWildcardType) getAnnotatedType()).getExtendsBound(),
+          upperBoundJava,
+          ignoreAnnotations);
     } else {
       return null;
     }
@@ -600,7 +620,7 @@ public AbstractType getWildcardUpperBound() {
    */
   public AbstractType getErased() {
     TypeMirror typeMirror = context.env.getTypeUtils().erasure(getJavaType());
-    return create(getAnnotatedType().getErased(), typeMirror);
+    return create(getAnnotatedType().getErased(), typeMirror, ignoreAnnotations);
   }
 
   /**
@@ -611,7 +631,10 @@ public AbstractType getErased() {
   public final AbstractType getComponentType() {
     if (getJavaType().getKind() == TypeKind.ARRAY) {
       TypeMirror javaType = ((ArrayType) getJavaType()).getComponentType();
-      return create(((AnnotatedArrayType) getAnnotatedType()).getComponentType(), javaType);
+      return create(
+          ((AnnotatedArrayType) getAnnotatedType()).getComponentType(),
+          javaType,
+          ignoreAnnotations);
     } else {
       return null;
     }
@@ -634,6 +657,9 @@ public boolean equals(Object o) {
     }
 
     AbstractType that = (AbstractType) o;
+    if (ignoreAnnotations != that.ignoreAnnotations) {
+      return false;
+    }
 
     if (!context.equals(that.context)) {
       return false;

framework/src/main/java/org/checkerframework/framework/util/typeinference8/types/InferenceFactory.java

@@ -871,20 +871,33 @@ public ProperType lub(Set<ProperType> properTypes) {
     if (properTypes.isEmpty()) {
       return null;
     }
-    TypeMirror tiTypeMirror = null;
-    AnnotatedTypeMirror ti = null;
-    for (ProperType liProperType : properTypes) {
-      AnnotatedTypeMirror li = liProperType.getAnnotatedType();
-      TypeMirror liTypeMirror = liProperType.getJavaType();
-      if (ti == null) {
-        ti = li;
-        tiTypeMirror = liTypeMirror;
+
+    TypeMirror lubTM = null;
+    AnnotatedTypeMirror lubATM = null;
+    boolean ignoreAnnotations = false;
+    for (ProperType properType : properTypes) {
+      AnnotatedTypeMirror atm = properType.getAnnotatedType();
+      TypeMirror tm = properType.getJavaType();
+      if (lubATM == null) {
+        lubATM = atm;
+        lubTM = tm;
+        ignoreAnnotations = properType.ignoreAnnotations;
       } else {
-        tiTypeMirror = lub(context.env, tiTypeMirror, liTypeMirror);
-        ti = AnnotatedTypes.leastUpperBound(typeFactory, ti, li, tiTypeMirror);
+        lubTM = lub(context.env, lubTM, tm);
+        if (properType.ignoreAnnotations == ignoreAnnotations) {
+          lubATM = AnnotatedTypes.leastUpperBound(typeFactory, lubATM, atm, lubTM);
+        } else if (properType.ignoreAnnotations) {
+          lubATM =
+              AnnotatedTypes.asSuper(
+                  typeFactory, lubATM, AnnotatedTypeMirror.createType(lubTM, typeFactory, false));
+        } else {
+          lubATM =
+              AnnotatedTypes.asSuper(
+                  typeFactory, atm, AnnotatedTypeMirror.createType(lubTM, typeFactory, false));
+        }
       }
     }
-    return new ProperType(ti, tiTypeMirror, context);
+    return new ProperType(lubATM, lubTM, context, ignoreAnnotations);
   }
 
   /**
@@ -921,22 +934,29 @@ public AbstractType glb(AbstractType a, AbstractType b) {
     AnnotatedTypeMirror aAtm = a.getAnnotatedType();
     AnnotatedTypeMirror bAtm = b.getAnnotatedType();
     AnnotatedTypeMirror glbATM = AnnotatedTypes.annotatedGLB(typeFactory, aAtm, bAtm);
+    if (a.ignoreAnnotations != b.ignoreAnnotations) {
+      if (a.ignoreAnnotations) {
+        glbATM.replaceAnnotations(bAtm.getPrimaryAnnotations());
+      } else {
+        glbATM.replaceAnnotations(aAtm.getPrimaryAnnotations());
+      }
+    }
     if (context.types.isSameType(aJavaType, (Type) glb)) {
-      return a.create(glbATM, glb);
+      return a.create(glbATM, glb, false);
     }
 
     if (context.types.isSameType(bJavaType, (Type) glb)) {
-      return b.create(glbATM, glb);
+      return b.create(glbATM, glb, false);
     }
 
     if (a.isInferenceType()) {
-      return a.create(glbATM, glb);
+      return a.create(glbATM, glb, false);
     } else if (b.isInferenceType()) {
-      return b.create(glbATM, glb);
+      return b.create(glbATM, glb, false);
     }
 
     assert a.isProper() && b.isProper();
-    return new ProperType(glbATM, glb, context);
+    return new ProperType(glbATM, glb, context, a.ignoreAnnotations && b.ignoreAnnotations);
   }
 
   /**
@@ -1104,7 +1124,7 @@ public AbstractType createFreshTypeVariable(
     }
     context.typeFactory.capturedTypeVarSubstitutor.substitute(
         typeVariable, Collections.singletonMap(typeVariable.getUnderlyingType(), typeVariable));
-    return upperBound.create(typeVariable, freshTypeVariable);
+    return upperBound.create(typeVariable, freshTypeVariable, false);
   }
 
   /**