java.lang.Record is a super type of all records.

checker/src/test/java/org/checkerframework/checker/test/junit/ainferrunners/AinferTestCheckerJaifsGenerationTest.java

@@ -26,7 +26,7 @@ public AinferTestCheckerJaifsGenerationTest(List<File> testFiles) {
         "ainfer-testchecker/non-annotated",
         "-Ainfer=jaifs",
         // The AFU's JAIF reading/writing libraries don't support records.
-        "-AskipDefs=SimpleRecord",
+        "-AskipDefs=SimpleRecord|Issue6069",
         // Use a stub file here, even though this is a JAIF test. This test can't pass
         // without an external file that specifies that a method is pure, and there is no
         // way to directly pass a JAIF file (in a real WPI run, the JAIF file's annotations

checker/src/test/java/org/checkerframework/checker/test/junit/ainferrunners/AinferTestCheckerJaifsValidationTest.java

@@ -25,7 +25,7 @@ public AinferTestCheckerJaifsValidationTest(List<File> testFiles) {
         AinferTestCheckerJaifsGenerationTest.class,
         "-Awarns",
         // The AFU's JAIF reading/writing libraries don't support records.
-        "-AskipDefs=TestPure|SimpleRecord");
+        "-AskipDefs=TestPure|SimpleRecord|Issue6069");
   }
 
   @Parameters

framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeMirror.java

@@ -919,6 +919,20 @@ protected static AnnotatedDeclaredType createTypeOfObject(AnnotatedTypeFactory a
     return objectType;
   }
 
+  /**
+   * Create an {@link AnnotatedDeclaredType} with the underlying type of {@link java.lang.Record}.
+   * It includes any annotations placed by {@link AnnotatedTypeFactory#fromElement(Element)}.
+   *
+   * @param atypeFactory type factory to use
+   * @return AnnotatedDeclaredType for Record
+   */
+  protected static AnnotatedDeclaredType createTypeOfRecord(AnnotatedTypeFactory atypeFactory) {
+    AnnotatedDeclaredType recordType =
+        atypeFactory.fromElement(atypeFactory.elements.getTypeElement("java.lang.Record"));
+    recordType.declaration = false;
+    return recordType;
+  }
+
   /**
    * Returns the result of calling {@code underlyingType.toString().hashcode()}. This method saves
    * the result in a field so that it isn't recomputed each time.

framework/src/main/java/org/checkerframework/framework/type/SupertypeFinder.java

@@ -327,7 +327,11 @@ private List<AnnotatedDeclaredType> supertypesFromTree(
                 atypeFactory.getAnnotatedTypeFromTypeTree(classTree.getExtendsClause());
         supertypes.add(adt);
       } else if (!ElementUtils.isObject(TreeUtils.elementFromDeclaration(classTree))) {
-        supertypes.add(AnnotatedTypeMirror.createTypeOfObject(atypeFactory));
+        if (classTree.getKind().name().contentEquals("RECORD")) {
+          supertypes.add(AnnotatedTypeMirror.createTypeOfRecord(atypeFactory));
+        } else {
+          supertypes.add(AnnotatedTypeMirror.createTypeOfObject(atypeFactory));
+        }
       }
 
       for (Tree implemented : classTree.getImplementsClause()) {

framework/tests/all-systems/java17/Issue6069.java

@@ -0,0 +1,22 @@
+// @below-java17-jdk-skip-test
+package issue6069;
+
+public class Issue6069 {
+  public interface MyInterface {
+    Record foo();
+  }
+
+  public static class MyClass implements MyInterface {
+
+    public MyRecord foo() {
+      return new MyRecord(42);
+    }
+
+    record MyRecord(int bar) {}
+
+    public static void main(String[] args) {
+      MyClass f = new MyClass();
+      System.out.println(f.foo());
+    }
+  }
+}