java.lang.IllegalArgumentException
at org.arend.core.elimtree.ElimBody.computeRefinedPatterns(ElimBody.java:75)
at org.arend.core.elimtree.ElimBody.computeRefinedPatterns(ElimBody.java:91)
at org.arend.core.elimtree.ElimBody.computeRefinedPatterns(ElimBody.java:50)
at org.arend.lib.meta.MatchingCasesMeta.lambda$invokeMeta$0(MatchingCasesMeta.java:325)
at org.arend.typechecking.visitor.FindSubexpressionVisitor.visitDefCall(FindSubexpressionVisitor.java:22)
at org.arend.typechecking.visitor.FindSubexpressionVisitor.visitDefCall(FindSubexpressionVisitor.java:8)
at org.arend.core.expr.visitor.BaseExpressionVisitor.visitFunCall(BaseExpressionVisitor.java:10)
at org.arend.core.expr.FunCallExpression.accept(FunCallExpression.java:70)
at org.arend.typechecking.visitor.SearchVisitor.lambda$visitDefCall$0(SearchVisitor.java:20)
at java.base/java.util.stream.MatchOps$1MatchSink.accept(MatchOps.java:90)
at java.base/java.util.ArrayList$ArrayListSpliterator.tryAdvance(ArrayList.java:1631)
at java.base/java.util.stream.ReferencePipeline.forEachWithCancel(ReferencePipeline.java:127)
at java.base/java.util.stream.AbstractPipeline.copyIntoWithCancel(AbstractPipeline.java:502)
at java.base/java.util.stream.AbstractPipeline.copyInto(AbstractPipeline.java:488)
at java.base/java.util.stream.AbstractPipeline.wrapAndCopyInto(AbstractPipeline.java:474)
at java.base/java.util.stream.MatchOps$MatchOp.evaluateSequential(MatchOps.java:230)
at java.base/java.util.stream.MatchOps$MatchOp.evaluateSequential(MatchOps.java:196)
at java.base/java.util.stream.AbstractPipeline.evaluate(AbstractPipeline.java:234)
at java.base/java.util.stream.ReferencePipeline.anyMatch(ReferencePipeline.java:528)
at org.arend.typechecking.visitor.SearchVisitor.visitDefCall(SearchVisitor.java:20)
at org.arend.typechecking.visitor.FindSubexpressionVisitor.visitDefCall(FindSubexpressionVisitor.java:25)
at org.arend.typechecking.visitor.FindSubexpressionVisitor.visitDefCall(FindSubexpressionVisitor.java:8)
at org.arend.core.expr.visitor.BaseExpressionVisitor.visitFunCall(BaseExpressionVisitor.java:10)
at org.arend.core.expr.FunCallExpression.accept(FunCallExpression.java:70)
at org.arend.typechecking.visitor.SearchVisitor.lambda$visitDefCall$0(SearchVisitor.java:20)
at java.base/java.util.stream.MatchOps$1MatchSink.accept(MatchOps.java:90)
at java.base/java.util.ArrayList$ArrayListSpliterator.tryAdvance(ArrayList.java:1631)
at java.base/java.util.stream.ReferencePipeline.forEachWithCancel(ReferencePipeline.java:127)
at java.base/java.util.stream.AbstractPipeline.copyIntoWithCancel(AbstractPipeline.java:502)
at java.base/java.util.stream.AbstractPipeline.copyInto(AbstractPipeline.java:488)
at java.base/java.util.stream.AbstractPipeline.wrapAndCopyInto(AbstractPipeline.java:474)
at java.base/java.util.stream.MatchOps$MatchOp.evaluateSequential(MatchOps.java:230)
at java.base/java.util.stream.MatchOps$MatchOp.evaluateSequential(MatchOps.java:196)
at java.base/java.util.stream.AbstractPipeline.evaluate(AbstractPipeline.java:234)
at java.base/java.util.stream.ReferencePipeline.anyMatch(ReferencePipeline.java:528)
at org.arend.typechecking.visitor.SearchVisitor.visitDefCall(SearchVisitor.java:20)
at org.arend.typechecking.visitor.FindSubexpressionVisitor.visitDefCall(FindSubexpressionVisitor.java:25)
at org.arend.typechecking.visitor.FindSubexpressionVisitor.visitDefCall(FindSubexpressionVisitor.java:8)
at org.arend.core.expr.visitor.BaseExpressionVisitor.visitFunCall(BaseExpressionVisitor.java:10)
at org.arend.core.expr.FunCallExpression.accept(FunCallExpression.java:70)
at org.arend.core.expr.Expression.processSubexpression(Expression.java:244)
at org.arend.lib.meta.MatchingCasesMeta.invokeMeta(MatchingCasesMeta.java:182)
at org.arend.typechecking.visitor.CheckTypeVisitor.invokeMeta(CheckTypeVisitor.java:2211)
at org.arend.typechecking.visitor.CheckTypeVisitor.checkMeta(CheckTypeVisitor.java:2234)
at org.arend.typechecking.visitor.CheckTypeVisitor.visitApp(CheckTypeVisitor.java:2384)
at org.arend.typechecking.visitor.CheckTypeVisitor.visitApp(CheckTypeVisitor.java:92)
at org.arend.term.concrete.Concrete$AppExpression.accept(Concrete.java:368)
at org.arend.typechecking.visitor.CheckTypeVisitor.checkExpr(CheckTypeVisitor.java:603)
at org.arend.typechecking.visitor.DefinitionTypechecker.typecheckFunctionBody(DefinitionTypechecker.java:1068)
at org.arend.typechecking.visitor.DefinitionTypechecker.visitFunction(DefinitionTypechecker.java:158)
at org.arend.typechecking.visitor.DefinitionTypechecker.visitFunction(DefinitionTypechecker.java:64)
at org.arend.term.concrete.Concrete$BaseFunctionDefinition.accept(Concrete.java:2086)
at org.arend.typechecking.order.listener.TypecheckingOrderingListener.unitFound(TypecheckingOrderingListener.java:222)
at org.arend.typechecking.order.listener.CollectingOrderingListener$MyUnit.feedTo(CollectingOrderingListener.java:49)
at org.arend.typechecking.BackgroundTypechecker$typecheckDefinition$ok$1$1.get(BackgroundTypechecker.kt:86)
at org.arend.typechecking.BackgroundTypechecker$typecheckDefinition$ok$1$1.get(BackgroundTypechecker.kt:20)
at org.arend.typechecking.computation.ComputationRunner.run(ComputationRunner.java:37)
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:20)
at org.arend.typechecking.DefinitionBlacklistService.runTimed(DefinitionBlacklistService.kt:25)
at org.arend.typechecking.BackgroundTypechecker.typecheckDefinition(BackgroundTypechecker.kt:84)
at org.arend.typechecking.BackgroundTypechecker.runTypechecker(BackgroundTypechecker.kt:53)
at org.arend.highlight.ArendHighlightingPass$applyInformationWithProgress$2.invoke(ArendHighlightingPass.kt:201)
at org.arend.highlight.ArendHighlightingPass$applyInformationWithProgress$2.invoke(ArendHighlightingPass.kt:34)
at org.arend.typechecking.TypecheckingTaskQueue$addTask$2.run(TypecheckingTaskQueue.kt:43)
at com.intellij.util.RunnableCallable.call(RunnableCallable.java:20)
at com.intellij.util.RunnableCallable.call(RunnableCallable.java:11)
at com.intellij.openapi.application.impl.ApplicationImpl$1.call(ApplicationImpl.java:268)
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:834)
Code for repro:
\func TorusSphereTorus (a : \Sigma Sphere1 Sphere1) : TorusSphere (SphereTorus a) = a => mcases
{SphereTorus} \with { | base1 => idp | loop i => idp }
Code for repro:
In Torus.ard