NPE in typechecking
- Dominant language
- Java
- Stars
- 756
- Forks
- 31
- PR merge metrics
- No merged PRs in 30d
Description
I was writing a proof, and at some point plugin stoped showing goals although I had a hole:

As you can see `<-trans` is shown as proven, but this is not true. The log have the following NPE:
```
2021-05-02 14:34:10,472 [68609791] INFO - .deployment.AsyncDevicesGetter - adb not found
2021-05-02 14:34:10,602 [68609921] ERROR - pechecking.TypeCheckingService - null
java.lang.NullPointerException
at org.arend.core.definition.DataDefinition.getTypeWithParams(DataDefinition.java:217)
at org.arend.typechecking.result.DefCallResult.makeTResult(DefCallResult.java:40)
at org.arend.typechecking.visitor.CheckTypeVisitor.typeCheckDefCall(CheckTypeVisitor.java:1495)
at org.arend.typechecking.visitor.CheckTypeVisitor.visitReference(CheckTypeVisitor.java:1532)
at org.arend.typechecking.implicitargs.StdImplicitArgsInference.infer(StdImplicitArgsInference.java:274)
at org.arend.typechecking.visitor.CheckTypeVisitor.visitApp(CheckTypeVisitor.java:2631)
at org.arend.typechecking.visitor.CheckTypeVisitor.visitApp(CheckTypeVisitor.java:93)
at org.arend.term.concrete.Concrete$AppExpression.accept(Concrete.java:392)
at org.arend.typechecking.visitor.CheckTypeVisitor.checkType(CheckTypeVisitor.java:835)
at org.arend.typechecking.visitor.CheckTypeVisitor.finalCheckType(CheckTypeVisitor.java:873)
at org.arend.typechecking.visitor.DefinitionTypechecker.typecheckParameters(DefinitionTypechecker.java:484)
at org.arend.typechecking.visitor.DefinitionTypechecker.typecheckConstructor(DefinitionTypechecker.java:1799)
at org.arend.typechecking.visitor.DefinitionTypechecker.typecheckDataBody(DefinitionTypechecker.java:1510)
at org.arend.typechecking.visitor.DefinitionTypechecker.visitData(DefinitionTypechecker.java:180)
at org.arend.typechecking.visitor.DefinitionTypechecker.visitData(DefinitionTypechecker.java:66)
at org.arend.term.concrete.Concrete$DataDefinition.accept(Concrete.java:2226)
at org.arend.typechecking.order.listener.TypecheckingOrderingListener.unitFound(TypecheckingOrderingListener.java:221)
at org.arend.typechecking.order.listener.CollectingOrderingListener$MyUnit.feedTo(CollectingOrderingListener.java:49)
at org.arend.typechecking.order.listener.CollectingOrderingListener.feed(CollectingOrderingListener.java:142)
at org.arend.typechecking.order.listener.TypecheckingOrderingListener.lambda$typecheckCollected$4(TypecheckingOrderingListener.java:126)
at org.arend.typechecking.computation.ComputationRunner.run(ComputationRunner.java:37)
at org.arend.typechecking.computation.BooleanComputationRunner.run(BooleanComputationRunner.java:8)
at org.arend.typechecking.order.listener.TypecheckingOrderingListener.typecheckCollected(TypecheckingOrderingListener.java:125)
at org.arend.typechecking.execution.TypeCheckProcessHandler$startNotify$1.run(TypeCheckProcessHandler.kt:185)
at java.base/java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1128)
at java.base/java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:628)
at java.base/java.util.concurrent.Executors$PrivilegedThreadFactory$1$1.run(Executors.java:668)
at java.base/java.util.concurrent.Executors$PrivilegedThreadFactory$1$1.run(Executors.java:665)
at java.base/java.security.AccessController.doPrivileged(Native Method)
at java.base/java.util.concurrent.Executors$PrivilegedThreadFactory$1.run(Executors.java:665)
at java.base/java.lang.Thread.run(Thread.java:834)
2021-05-02 14:34:10,602 [68609921] ERROR - pechecking.TypeCheckingService - IntelliJ IDEA 2021.1 Build #IC-211.6693.111
2021-05-02 14:34:10,603 [68609922] ERROR - pechecking.TypeCheckingService - JDK: 11.0.10; VM: Dynamic Code Evolution 64-Bit Server VM; Vendor: JetBrains s.r.o.
2021-05-02 14:34:10,603 [68609922] ERROR - pechecking.TypeCheckingService - OS: Mac OS X
2021-05-02 14:34:10,603 [68609922] ERROR - pechecking.TypeCheckingService - Plugin to blame: Arend version: 1.6.0.3
```
When I try to rerun the Typecheck, this exception appears again. The only way to fix this is to reopen the project.
I have seen this a number of times. Sometimes this bug can be very confusing as it looks like the proof is accepted, but I am not sure why (before I realize it is a bug).
Contributor guide
No contributing guide indexed for this repository
Research direction
Start with org.arend.core.definition.DataDefinition.getTypeWithParams at DataDefinition.java:217, then follow the listed typechecking calls through CheckTypeVisitor and DefinitionTypechecker. Reproduce the failure by rerunning typechecking after the proof state loses its goals, using the reported Arend 1.6.0.3 environment if possible. Done means the exception no longer occurs and an unfinished hole is not shown as proven.
Written by the indexing model from the issue text.
Assessment
- Tech stack
- java
- Domain
- compilers
- Issue type
- Bug
- Difficulty
- 4/5
- Estimated time
- 3-5 days
- Activity status
- Stale
- Clarity
- Needs clarification
- Newbie friendliness
- 32/100