intellij-arend icon indicating copy to clipboard operation
intellij-arend copied to clipboard

NPE in CheckTypeVisitor

Open sxhya opened this issue 3 years ago • 0 comments

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

sxhya avatar Jan 24 '22 09:01 sxhya