search

JetBrains / Arend

The Arend Proof Assistant
https://arend-lang.github.io/
Apache License 2.0
690 stars 33 forks source link

IllegalArgumentException #317

Closed knisht closed 2 years ago

knisht commented 2 years ago 
\record R {
  | X : \Set
  | A : X -> D
}

\record D { | Y : R }

\record U \extends R {
}

\func f (e : \Set) : U \cowith
  | X => e
  | A x => \new D {
    | Y => (\this : U)
  }
java.lang.IllegalArgumentException: Too many implemented fields (expected 0): D
    at org.arend.typechecking.visitor.CheckTypeVisitor.checkAllImplemented(CheckTypeVisitor.java:1638)
    at org.arend.typechecking.visitor.CheckTypeVisitor.makeNew(CheckTypeVisitor.java:1625)
    at org.arend.typechecking.visitor.CheckTypeVisitor.visitNew(CheckTypeVisitor.java:1611)
    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:903)
    at org.arend.typechecking.visitor.CheckTypeVisitor.visitLam(CheckTypeVisitor.java:2254)
    at org.arend.typechecking.visitor.CheckTypeVisitor.lambda$visitLam$1(CheckTypeVisitor.java:2274)
    at org.arend.typechecking.visitor.CheckTypeVisitor.visitLam(CheckTypeVisitor.java:2406)
    at org.arend.typechecking.visitor.CheckTypeVisitor.visitLam(CheckTypeVisitor.java:2430)
    at org.arend.typechecking.visitor.CheckTypeVisitor.visitLam(CheckTypeVisitor.java:87)
    at org.arend.term.concrete.Concrete$LamExpression.accept(Concrete.java:954)
    at org.arend.typechecking.visitor.CheckTypeVisitor.checkExpr(CheckTypeVisitor.java:903)
    at org.arend.typechecking.visitor.CheckTypeVisitor.typecheckImplementation(CheckTypeVisitor.java:1480)
    at org.arend.typechecking.visitor.CheckTypeVisitor.typecheckClassExt(CheckTypeVisitor.java:1348)
    at org.arend.typechecking.visitor.CheckTypeVisitor.visitNew(CheckTypeVisitor.java:1608)
    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:903)
    at org.arend.typechecking.visitor.CheckTypeVisitor.finalCheckExpr(CheckTypeVisitor.java:911)
    at org.arend.typechecking.visitor.DefinitionTypechecker.typecheckCoClauses(DefinitionTypechecker.java:903)
    at org.arend.typechecking.visitor.DefinitionTypechecker.typecheckFunctionBody(DefinitionTypechecker.java:1226)
    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:227)
    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:86)
    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:85)
    at org.arend.typechecking.BackgroundTypechecker$typecheckDefinition$ok$1.invoke(BackgroundTypechecker.kt:84)
    at org.arend.typechecking.DefinitionBlacklistService.runTimed(DefinitionBlacklistService.kt:24)
    at org.arend.typechecking.BackgroundTypechecker.typecheckDefinition(BackgroundTypechecker.kt:84)
    at org.arend.typechecking.BackgroundTypechecker.runTypechecker(BackgroundTypechecker.kt:64)
    at org.arend.highlight.ArendHighlightingPass$applyInformationWithProgress$2.invoke(ArendHighlightingPass.kt:202)
    at org.arend.highlight.ArendHighlightingPass$applyInformationWithProgress$2.invoke(ArendHighlightingPass.kt:201)
    at org.arend.typechecking.TypecheckingTaskQueue.addTask$lambda-1(TypecheckingTaskQueue.kt:43)
    at com.intellij.openapi.application.impl.ApplicationImpl$1.run(ApplicationImpl.java:265)
    at java.base/java.util.concurrent.Executors$RunnableAdapter.call(Executors.java:515)
    at java.base/java.util.concurrent.FutureTask.run(FutureTask.java:264)
    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:829)