intellij-arend
intellij-arend copied to clipboard
NPE in CheckTypeVisitor
java.lang.NullPointerException
at org.arend.typechecking.visitor.CheckTypeVisitor.addImplicitLamParams(CheckTypeVisitor.java:1503)
at org.arend.typechecking.visitor.CheckTypeVisitor.typecheckImplementation(CheckTypeVisitor.java:1485)
at org.arend.typechecking.visitor.CheckTypeVisitor.typecheckClassExt(CheckTypeVisitor.java:1356)
at org.arend.typechecking.visitor.CheckTypeVisitor.visitNew(CheckTypeVisitor.java:1616)
at org.arend.typechecking.visitor.CheckTypeVisitor.visitNew(CheckTypeVisitor.java:87)
at org.arend.term.concrete.Concrete$NewExpression.accept(Concrete.java:829)
at org.arend.typechecking.visitor.CheckTypeVisitor.checkExpr(CheckTypeVisitor.java:911)
at org.arend.typechecking.implicitargs.StdImplicitArgsInference.infer(StdImplicitArgsInference.java:544)
at org.arend.typechecking.visitor.CheckTypeVisitor.visitApp(CheckTypeVisitor.java:3100)
at org.arend.typechecking.visitor.CheckTypeVisitor.visitApp(CheckTypeVisitor.java:3045)
at org.arend.typechecking.visitor.CheckTypeVisitor.visitApp(CheckTypeVisitor.java:87)
at org.arend.term.concrete.Concrete$AppExpression.accept(Concrete.java:402)
at org.arend.typechecking.visitor.CheckTypeVisitor.checkExpr(CheckTypeVisitor.java:911)
at org.arend.typechecking.visitor.DefinitionTypechecker.typecheckFunctionBody(DefinitionTypechecker.java:1285)
at org.arend.typechecking.visitor.DefinitionTypechecker.visitFunction(DefinitionTypechecker.java:173)
at org.arend.typechecking.visitor.DefinitionTypechecker.visitFunction(DefinitionTypechecker.java:68)
at org.arend.term.concrete.Concrete$BaseFunctionDefinition.accept(Concrete.java:2285)
at org.arend.typechecking.order.listener.TypecheckingOrderingListener.unitFound(TypecheckingOrderingListener.java:228)
at org.arend.typechecking.order.listener.CollectingOrderingListener$MyUnit.feedTo(CollectingOrderingListener.java:49)
at org.arend.typechecking.BackgroundTypechecker$typecheckDefinition$ok$1.invoke$lambda-0(BackgroundTypechecker.kt:80)
at org.arend.typechecking.computation.ComputationRunner.run(ComputationRunner.java:48)
at org.arend.typechecking.computation.BooleanComputationRunner.run(BooleanComputationRunner.java:8)
at org.arend.typechecking.BackgroundTypechecker$typecheckDefinition$ok$1.invoke(BackgroundTypechecker.kt:79)
at org.arend.typechecking.BackgroundTypechecker$typecheckDefinition$ok$1.invoke(BackgroundTypechecker.kt:78)
at org.arend.typechecking.DefinitionBlacklistService.runTimed(DefinitionBlacklistService.kt:24)
at org.arend.typechecking.BackgroundTypechecker.typecheckDefinition(BackgroundTypechecker.kt:78)
at org.arend.typechecking.BackgroundTypechecker.runTypechecker(BackgroundTypechecker.kt:64)
To reproduce try to typecheck the following (incorrect) piece of code in IDE:
\record testRecord (T : \Type)
| k {A B : \Type} {a : A} (b : B) : A
\func h => \new testRecord (\Sigma Nat Nat) {
| k {a, a1} b => a
}
This issue is not reproducible in the console version of Arend