The case which is leading to "error: AsSuperVisitor: type is not an erased subtype of supertype." #6891
Description
Hi there
Thank you for The Checker Framework.
I've noticed the following case.
If I run:
javac \
-J--add-exports=jdk.compiler/com.sun.tools.javac.api=ALL-UNNAMED \
-J--add-exports=jdk.compiler/com.sun.tools.javac.code=ALL-UNNAMED \
-J--add-exports=jdk.compiler/com.sun.tools.javac.file=ALL-UNNAMED \
-J--add-exports=jdk.compiler/com.sun.tools.javac.main=ALL-UNNAMED \
-J--add-exports=jdk.compiler/com.sun.tools.javac.model=ALL-UNNAMED \
-J--add-exports=jdk.compiler/com.sun.tools.javac.processing=ALL-UNNAMED \
-J--add-exports=jdk.compiler/com.sun.tools.javac.tree=ALL-UNNAMED \
-J--add-exports=jdk.compiler/com.sun.tools.javac.util=ALL-UNNAMED \
-J--add-opens=jdk.compiler/com.sun.tools.javac.comp=ALL-UNNAMED -processor org.checkerframework.checker.nullness.NullnessChecker -cp ~/Downloads/checker-framework-3.48.2/checker/dist/checker.jar Reproduction.java
for the following code:
private Map<String, String> func(Set<Entity> entities) {
return Optional.ofNullable(entities)
.map(t -> t.stream().collect(Collectors.toMap(Entity::getName, Entity::getId))
).orElse(Collections.emptyMap());
}
The Checker framework crashes in this way:
error: AsSuperVisitor: type is not an erased subtype of supertype.
type: Object
superType: Map<String, String>
; The Checker Framework crashed. Please report the crash. Version: Checker Framework 3.48.2.
Compilation unit: Reproduction.java
Last visited tree at line 11 column 5:
return Optional.ofNullable(entities)
Exception: java.lang.Throwable; java.lang.Throwable
at org.checkerframework.javacutil.BugInCF.<init>(BugInCF.java:38)
at org.checkerframework.framework.type.AsSuperVisitor.errorTypeNotErasedSubtypeOfSuperType(AsSuperVisitor.java:148)
at org.checkerframework.framework.type.AsSuperVisitor.visitDeclared_Declared(AsSuperVisitor.java:338)
at org.checkerframework.framework.type.AsSuperVisitor.visitDeclared_Declared(AsSuperVisitor.java:30)
at org.checkerframework.framework.util.AtmCombo.accept(AtmCombo.java:313)
at org.checkerframework.framework.type.visitor.AbstractAtmComboVisitor.visit(AbstractAtmComboVisitor.java:34)
at org.checkerframework.framework.type.AsSuperVisitor.visit(AsSuperVisitor.java:107)
at org.checkerframework.framework.type.AsSuperVisitor.asSuper(AsSuperVisitor.java:88)
at org.checkerframework.framework.util.AnnotatedTypes.asSuper(AnnotatedTypes.java:118)
at org.checkerframework.framework.util.AnnotatedTypes.castedAsSuper(AnnotatedTypes.java:154)
at org.checkerframework.framework.type.DefaultTypeHierarchy.visitTypeArgs(DefaultTypeHierarchy.java:583)
at org.checkerframework.framework.type.DefaultTypeHierarchy.visitDeclared_Declared(DefaultTypeHierarchy.java:555)
at org.checkerframework.framework.type.DefaultTypeHierarchy.visitDeclared_Declared(DefaultTypeHierarchy.java:49)
at org.checkerframework.framework.util.AtmCombo.accept(AtmCombo.java:313)
at org.checkerframework.framework.type.DefaultTypeHierarchy.isSubtype(DefaultTypeHierarchy.java:259)
at org.checkerframework.framework.type.DefaultTypeHierarchy.isSubtype(DefaultTypeHierarchy.java:137)
at org.checkerframework.common.basetype.BaseTypeVisitor.commonAssignmentCheck(BaseTypeVisitor.java:3137)
at org.checkerframework.common.basetype.BaseTypeVisitor.commonAssignmentCheck(BaseTypeVisitor.java:3112)
at org.checkerframework.common.basetype.BaseTypeVisitor.visitReturn(BaseTypeVisitor.java:2277)
at org.checkerframework.common.basetype.BaseTypeVisitor.visitReturn(BaseTypeVisitor.java:189)
at jdk.compiler/com.sun.tools.javac.tree.JCTree$JCReturn.accept(JCTree.java:1717)
at jdk.compiler/com.sun.source.util.TreePathScanner.scan(TreePathScanner.java:86)
at org.checkerframework.framework.source.SourceVisitor.scan(SourceVisitor.java:92)
at org.checkerframework.common.basetype.BaseTypeVisitor.scan(BaseTypeVisitor.java:408)
at org.checkerframework.common.basetype.BaseTypeVisitor.scan(BaseTypeVisitor.java:189)
at jdk.compiler/com.sun.source.util.TreeScanner.scan(TreeScanner.java:111)
at jdk.compiler/com.sun.source.util.TreeScanner.visitBlock(TreeScanner.java:272)
at jdk.compiler/com.sun.tools.javac.tree.JCTree$JCBlock.accept(JCTree.java:1103)
at jdk.compiler/com.sun.source.util.TreePathScanner.scan(TreePathScanner.java:86)
at org.checkerframework.framework.source.SourceVisitor.scan(SourceVisitor.java:92)
at org.checkerframework.common.basetype.BaseTypeVisitor.scan(BaseTypeVisitor.java:408)
at org.checkerframework.common.basetype.BaseTypeVisitor.scan(BaseTypeVisitor.java:189)
at jdk.compiler/com.sun.source.util.TreeScanner.scanAndReduce(TreeScanner.java:96)
at jdk.compiler/com.sun.source.util.TreeScanner.visitMethod(TreeScanner.java:224)
at org.checkerframework.framework.source.SourceVisitor.visitMethod(SourceVisitor.java:110)
at org.checkerframework.common.basetype.BaseTypeVisitor.processMethodTree(BaseTypeVisitor.java:1058)
at org.checkerframework.common.basetype.BaseTypeVisitor.visitMethod(BaseTypeVisitor.java:954)
at org.checkerframework.common.basetype.BaseTypeVisitor.visitMethod(BaseTypeVisitor.java:189)
at jdk.compiler/com.sun.tools.javac.tree.JCTree$JCMethodDecl.accept(JCTree.java:953)
at jdk.compiler/com.sun.source.util.TreePathScanner.scan(TreePathScanner.java:86)
at org.checkerframework.framework.source.SourceVisitor.scan(SourceVisitor.java:92)
at org.checkerframework.common.basetype.BaseTypeVisitor.scan(BaseTypeVisitor.java:408)
at org.checkerframework.common.basetype.BaseTypeVisitor.scan(BaseTypeVisitor.java:189)
at jdk.compiler/com.sun.source.util.TreeScanner.scanAndReduce(TreeScanner.java:96)
at jdk.compiler/com.sun.source.util.TreeScanner.scan(TreeScanner.java:111)
at jdk.compiler/com.sun.source.util.TreeScanner.scanAndReduce(TreeScanner.java:119)
at jdk.compiler/com.sun.source.util.TreeScanner.visitClass(TreeScanner.java:203)
at org.checkerframework.framework.source.SourceVisitor.visitClass(SourceVisitor.java:98)
at org.checkerframework.common.basetype.BaseTypeVisitor.processClassTree(BaseTypeVisitor.java:603)
at org.checkerframework.common.basetype.BaseTypeVisitor.visitClass(BaseTypeVisitor.java:558)
at org.checkerframework.common.basetype.BaseTypeVisitor.visitClass(BaseTypeVisitor.java:189)
at jdk.compiler/com.sun.tools.javac.tree.JCTree$JCClassDecl.accept(JCTree.java:860)
at jdk.compiler/com.sun.source.util.TreePathScanner.scan(TreePathScanner.java:60)
at org.checkerframework.framework.source.SourceVisitor.visit(SourceVisitor.java:86)
at org.checkerframework.framework.source.SourceChecker.typeProcess(SourceChecker.java:1347)
at org.checkerframework.framework.source.SourceChecker.typeProcess(SourceChecker.java:1268)
at org.checkerframework.javacutil.AbstractTypeProcessor$AttributionTaskListener.finished(AbstractTypeProcessor.java:188)
at jdk.compiler/com.sun.tools.javac.api.ClientCodeWrapper$WrappedTaskListener.finished(ClientCodeWrapper.java:854)
at jdk.compiler/com.sun.tools.javac.api.MultiTaskListener.finished(MultiTaskListener.java:132)
at jdk.compiler/com.sun.tools.javac.main.JavaCompiler.flow(JavaCompiler.java:1394)
at jdk.compiler/com.sun.tools.javac.main.JavaCompiler.flow(JavaCompiler.java:1351)
at jdk.compiler/com.sun.tools.javac.main.JavaCompiler.compile(JavaCompiler.java:946)
at jdk.compiler/com.sun.tools.javac.main.Main.compile(Main.java:317)
at jdk.compiler/com.sun.tools.javac.main.Main.compile(Main.java:176)
at jdk.compiler/com.sun.tools.javac.Main.compile(Main.java:64)
at jdk.compiler/com.sun.tools.javac.Main.main(Main.java:50)
It works correctly if I clarify types for Collectors call:
Collectors.<Entity, String, String>toMap(Entity::getName, Entity::getId)
I've attached the full version of this file: Reproduction.zip