Missing type arguments on enclosing types

[wmdietl]

Take this example

import org.checkerframework.checker.nullness.qual.Nullable;

class Min<XXX extends @Nullable Object> {
  abstract class Super {
    abstract void accept(Entry<XXX> entry);
  }

  abstract class Sub extends Min<XXX>.Super {
    @Override
    abstract void accept(Entry<XXX> entry);
  }

  interface Entry<ZZZ extends @Nullable Object> {}
}

Add some instrumentation to see what types are determined:

diff --git a/framework/src/main/java/org/checkerframework/framework/type/SupertypeFinder.java b/framework/src/main/java/org/checkerframework/framework/type/SupertypeFinder.java
index 0fc1867cf..62b1ddb8d 100644
--- a/framework/src/main/java/org/checkerframework/framework/type/SupertypeFinder.java
+++ b/framework/src/main/java/org/checkerframework/framework/type/SupertypeFinder.java
@@ -62,6 +62,7 @@ final class SupertypeFinder {
         List<AnnotatedDeclaredType> supertypes =
                 supertypeFindingVisitor.visitDeclared(type.asUse(), null);
         type.atypeFactory.postDirectSuperTypes(type, supertypes);
+        System.out.println("1 type: " + type + " supertypes: " + supertypes);
         return supertypes;
     }

@@ -79,6 +80,7 @@ final class SupertypeFinder {
                 new SupertypeFindingVisitor(type.atypeFactory);
         List<? extends AnnotatedTypeMirror> supertypes = supertypeFindingVisitor.visit(type, null);
         type.atypeFactory.postDirectSuperTypes(type, supertypes);
+        System.out.println("2 type: " + type + " supertypes: " + supertypes);
         return supertypes;
     }

@@ -381,6 +383,7 @@ final class SupertypeFinder {
                     adt.setIsUnderlyingTypeRaw();
                 }
             }
+            System.out.println("3 type: " + type + " supertypes: " + supertypes);
             return supertypes;
         }

When executing ./checker/bin/javac -processor nullness -AassumeKeyFor -AassumeInitialized -AprintAllQualifiers Min.java > log 2>&1 and looking for the supertypes of Sub you'll see:

3 type: @NonNull Min<XXX extends @Nullable Object>.@NonNull Sub supertypes: [@NonNull Min<XXX extends @NonNull Object>.@NonNull Super]
3 type: @NonNull Min<XXX extends @Nullable Object> supertypes: [Object]
1 type: @NonNull Min<XXX extends @Nullable Object> supertypes: [@NonNull Object]
1 type: @NonNull Object supertypes: []
1 type: /*DECL*/ /*DECL*/ @NonNull Min<XXX/*DECL*/  extends @Nullable Object>.@NonNull Sub supertypes: [@NonNull Min<XXX extends @Nullable Object>.@NonNull Super]

Note the @NonNull upper bound for XXX initially. That upper bound is changed to @Nullable by the TypeVariableSubstitutor, but the incorrect type is a problem for type systems with stricter substitution.

One odd thing is that the output for "3" is different when we use XXX instead of the, supposedly equal, XXX extends @Nullable Object.

When we use class Sub extends Min<XXX>.Super the following change to framework/src/main/java/org/checkerframework/framework/type/TypeFromTypeTreeVisitor.java improves the situation:

     @Override
     public AnnotatedTypeMirror visitMemberSelect(MemberSelectTree tree, AnnotatedTypeFactory f) {
-
         AnnotatedTypeMirror type = f.type(tree);

         if (type.getKind() == TypeKind.TYPEVAR) {
             return getTypeVariableFromDeclaration((AnnotatedTypeVariable) type, f);
         }
-
+        if (type.getKind() == TypeKind.DECLARED
+                && ((AnnotatedDeclaredType) type).getEnclosingType() != null) {
+            AnnotatedTypeMirror encl = f.getAnnotatedTypeFromTypeTree(tree.getExpression());
+            if (encl.getKind() == TypeKind.DECLARED) {
+                clearAllTopLevelAnnotations((AnnotatedDeclaredType) encl);
+                ((AnnotatedDeclaredType) type).setEnclosingType((AnnotatedDeclaredType) encl);
+            }
+        }
         return type;
     }

+    private static void clearAllTopLevelAnnotations(AnnotatedTypeMirror type) {
+        while (type != null) {
+            type.clearAnnotations();
+            if (type.getKind() == TypeKind.DECLARED) {
+                type = ((AnnotatedDeclaredType) type).getEnclosingType();
+            } else {
+                type = null;
+            }
+        }
+    }

However, when we use the equal class Sub extends Super, a similar change to visitIdentifier is harder to come by. Maybe TypeFromTypeTreeVisitor is the wrong place to fix this issue.

One can also observe this problem when looking at the extends and implements clauses in the BaseTypeVisitor. Invalid types are not rejected, e.g. when XXX requires a nullable argument, by @Nullable XXX extends @Nullable Object, the supertype in class Sub extends Min<@NonNull String>.Super is not rejected. This should be investigated a bit more. I tried to get a false negative out of this mismatch, but in the end never managed to produce one.