Fix JIT of matchy calls #582
GitHub Actions / junit-tests
failed
Dec 17, 2024 in 0s
53 tests run, 49 passed, 0 skipped, 4 failed.
Annotations
Check failure on line 88 in cli-impl/src/test/java/org/aya/test/LibraryTest.java
github-actions / junit-tests
LibraryTest.testInMemoryAndPrim()
java.lang.AssertionError: Failed with `class org.aya.tyck.error.MetaVarError$BadlyScopedError`: In file data/vec/properties.aya:13:8 ->
11 | (xs ++ (ys ++ zs))
12 | ((xs ++ ys) ++ zs) elim xs
13 | | [] => refl
| ^--^
Error: The solution
Vec (+-assoc i) A
is not well-scoped
Only the variables below are allowed: `A`, `m`, `o`, `ys`, `zs`
at (373-376) [13:8-13:11]Raw output
java.lang.AssertionError: Failed with `class org.aya.tyck.error.MetaVarError$BadlyScopedError`: In file data/vec/properties.aya:13:8 ->
11 | (xs ++ (ys ++ zs))
12 | ((xs ++ ys) ++ zs) elim xs
13 | | [] => refl
| ^--^
Error: The solution
Vec (+-assoc i) A
is not well-scoped
Only the variables below are allowed: `A`, `m`, `o`, `ys`, `zs`
at (373-376) [13:8-13:11]
at org.aya.util.reporter.ThrowingReporter.report(ThrowingReporter.java:15)
at org.aya.util.reporter.CountingReporter$Delegated.report(CountingReporter.java:63)
at org.aya.util.reporter.CountingReporter$Delegated.report(CountingReporter.java:63)
at kala.collection.IndexedSeqLike.forEach(IndexedSeqLike.java:803)
at org.aya.util.reporter.DelayedReporter.reportNow(DelayedReporter.java:21)
at org.aya.util.reporter.DelayedReporter.close(DelayedReporter.java:26)
at org.aya.resolve.module.ModuleLoader.tyckModule(ModuleLoader.java:43)
at org.aya.cli.library.LibraryModuleLoader.load(LibraryModuleLoader.java:77)
at org.aya.resolve.module.CachedModuleLoader.lambda$load$0(CachedModuleLoader.java:26)
at kala.collection.mutable.MutableTreeMap.getOrPut(MutableTreeMap.java:483)
at org.aya.resolve.module.CachedModuleLoader.load(CachedModuleLoader.java:26)
at org.aya.resolve.module.ModuleLoader.load(ModuleLoader.java:89)
at org.aya.cli.library.LibraryCompiler$LibrarySccTycker.tyckOne(LibraryCompiler.java:376)
at org.aya.cli.library.LibraryCompiler$LibrarySccTycker.tyckSCC(LibraryCompiler.java:362)
at org.aya.util.tyck.OrgaTycker.tyckSCC(OrgaTycker.java:25)
at kala.function.CheckedConsumer.accept(CheckedConsumer.java:36)
at kala.collection.immutable.ImmutableVectors$Vector1.forEach(ImmutableVectors.java:460)
at kala.collection.base.Traversable.forEachChecked(Traversable.java:976)
at org.aya.cli.library.LibraryCompiler.make(LibraryCompiler.java:262)
at org.aya.cli.library.LibraryCompiler.make(LibraryCompiler.java:231)
at org.aya.cli.library.LibraryCompiler.make(LibraryCompiler.java:210)
at org.aya.cli.utils.CompilerUtil.catching(CompilerUtil.java:28)
at org.aya.cli.library.LibraryCompiler.start(LibraryCompiler.java:152)
at org.aya.test.LibraryTest.compile(LibraryTest.java:153)
at org.aya.test.LibraryTest.testInMemoryAndPrim(LibraryTest.java:88)
at java.base/jdk.internal.reflect.DirectMethodHandleAccessor.invoke(DirectMethodHandleAccessor.java:103)
at java.base/java.lang.reflect.Method.invoke(Method.java:580)
at org.junit.platform.commons.util.ReflectionUtils.invokeMethod(ReflectionUtils.java:767)
at org.junit.jupiter.engine.execution.MethodInvocation.proceed(MethodInvocation.java:60)
at org.junit.jupiter.engine.execution.InvocationInterceptorChain$ValidatingInvocation.proceed(InvocationInterceptorChain.java:131)
at org.junit.jupiter.engine.extension.TimeoutExtension.intercept(TimeoutExtension.java:156)
at org.junit.jupiter.engine.extension.TimeoutExtension.interceptTestableMethod(TimeoutExtension.java:147)
at org.junit.jupiter.engine.extension.TimeoutExtension.interceptTestMethod(TimeoutExtension.java:86)
at org.junit.jupiter.engine.execution.InterceptingExecutableInvoker$ReflectiveInterceptorCall.lambda$ofVoidMethod$0(InterceptingExecutableInvoker.java:103)
at org.junit.jupiter.engine.execution.InterceptingExecutableInvoker.lambda$invoke$0(InterceptingExecutableInvoker.java:93)
at org.junit.jupiter.engine.execution.InvocationInterceptorChain$InterceptedInvocation.proceed(InvocationInterceptorChain.java:106)
at org.junit.jupiter.engine.execution.InvocationInterceptorChain.proceed(InvocationInterceptorChain.java:64)
at org.junit.jupiter.engine.execution.InvocationInterceptorChain.chainAndInvoke(InvocationInterceptorChain.java:45)
at org.junit.jupiter.engine.execution.InvocationInterceptorChain.invoke(InvocationInterceptorChain.java:37)
at org.junit.jupiter.engine.execution.InterceptingExecutableInvoker.invoke(InterceptingExecutableInvoker.java:92)
at org.junit.jupiter.engine.execution.InterceptingExecutableInvoker.invoke(InterceptingExecutableInvoker.java:86)
at org.junit.jupiter.engine.descriptor.TestMethodTestDescriptor.lambda$invokeTestMethod$8(TestMethodTestDescriptor.java:217)
at org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
at org.junit.jupiter.engine.descriptor.TestMethodTestDescriptor.invokeTestMethod(TestMethodTestDescriptor.java:213)
at org.junit.jupiter.engine.descriptor.TestMethodTestDescriptor.execute(TestMethodTestDescriptor.java:138)
at org.junit.jupiter.engine.descriptor.TestMethodTestDescriptor.execute(TestMethodTestDescriptor.java:68)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$6(NodeTestTask.java:156)
at org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$8(NodeTestTask.java:146)
at org.junit.platform.engine.support.hierarchical.Node.around(Node.java:137)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$9(NodeTestTask.java:144)
at org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.executeRecursively(NodeTestTask.java:143)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.execute(NodeTestTask.java:100)
at java.base/java.util.ArrayList.forEach(ArrayList.java:1596)
at org.junit.platform.engine.support.hierarchical.SameThreadHierarchicalTestExecutorService.invokeAll(SameThreadHierarchicalTestExecutorService.java:41)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$6(NodeTestTask.java:160)
at org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$8(NodeTestTask.java:146)
at org.junit.platform.engine.support.hierarchical.Node.around(Node.java:137)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$9(NodeTestTask.java:144)
at org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.executeRecursively(NodeTestTask.java:143)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.execute(NodeTestTask.java:100)
at java.base/java.util.ArrayList.forEach(ArrayList.java:1596)
at org.junit.platform.engine.support.hierarchical.SameThreadHierarchicalTestExecutorService.invokeAll(SameThreadHierarchicalTestExecutorService.java:41)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$6(NodeTestTask.java:160)
at org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$8(NodeTestTask.java:146)
at org.junit.platform.engine.support.hierarchical.Node.around(Node.java:137)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$9(NodeTestTask.java:144)
at org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.executeRecursively(NodeTestTask.java:143)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.execute(NodeTestTask.java:100)
at org.junit.platform.engine.support.hierarchical.SameThreadHierarchicalTestExecutorService.submit(SameThreadHierarchicalTestExecutorService.java:35)
at org.junit.platform.engine.support.hierarchical.HierarchicalTestExecutor.execute(HierarchicalTestExecutor.java:57)
at org.junit.platform.engine.support.hierarchical.HierarchicalTestEngine.execute(HierarchicalTestEngine.java:54)
at org.junit.platform.launcher.core.EngineExecutionOrchestrator.execute(EngineExecutionOrchestrator.java:107)
at org.junit.platform.launcher.core.EngineExecutionOrchestrator.execute(EngineExecutionOrchestrator.java:88)
at org.junit.platform.launcher.core.EngineExecutionOrchestrator.lambda$execute$0(EngineExecutionOrchestrator.java:54)
at org.junit.platform.launcher.core.EngineExecutionOrchestrator.withInterceptedStreams(EngineExecutionOrchestrator.java:67)
at org.junit.platform.launcher.core.EngineExecutionOrchestrator.execute(EngineExecutionOrchestrator.java:52)
at org.junit.platform.launcher.core.DefaultLauncher.execute(DefaultLauncher.java:114)
at org.junit.platform.launcher.core.DefaultLauncher.execute(DefaultLauncher.java:86)
at org.junit.platform.launcher.core.DefaultLauncherSession$DelegatingLauncher.execute(DefaultLauncherSession.java:86)
at org.gradle.api.internal.tasks.testing.junitplatform.JUnitPlatformTestClassProcessor$CollectAllTestClassesExecutor.processAllTestClasses(JUnitPlatformTestClassProcessor.java:124)
at org.gradle.api.internal.tasks.testing.junitplatform.JUnitPlatformTestClassProcessor$CollectAllTestClassesExecutor.access$000(JUnitPlatformTestClassProcessor.java:99)
at org.gradle.api.internal.tasks.testing.junitplatform.JUnitPlatformTestClassProcessor.stop(JUnitPlatformTestClassProcessor.java:94)
at org.gradle.api.internal.tasks.testing.SuiteTestClassProcessor.stop(SuiteTestClassProcessor.java:63)
at java.base/jdk.internal.reflect.DirectMethodHandleAccessor.invoke(DirectMethodHandleAccessor.java:103)
at java.base/java.lang.reflect.Method.invoke(Method.java:580)
at org.gradle.internal.dispatch.ReflectionDispatch.dispatch(ReflectionDispatch.java:36)
at org.gradle.internal.dispatch.ReflectionDispatch.dispatch(ReflectionDispatch.java:24)
at org.gradle.internal.dispatch.ContextClassLoaderDispatch.dispatch(ContextClassLoaderDispatch.java:33)
at org.gradle.internal.dispatch.ProxyDispatchAdapter$DispatchingInvocationHandler.invoke(ProxyDispatchAdapter.java:92)
at jdk.proxy2/jdk.proxy2.$Proxy6.stop(Unknown Source)
at org.gradle.api.internal.tasks.testing.worker.TestWorker$3.run(TestWorker.java:200)
at org.gradle.api.internal.tasks.testing.worker.TestWorker.executeAndMaintainThreadName(TestWorker.java:132)
at org.gradle.api.internal.tasks.testing.worker.TestWorker.execute(TestWorker.java:103)
at org.gradle.api.internal.tasks.testing.worker.TestWorker.execute(TestWorker.java:63)
at org.gradle.process.internal.worker.child.ActionExecutionWorker.execute(ActionExecutionWorker.java:56)
at org.gradle.process.internal.worker.child.SystemApplicationClassLoaderWorker.call(SystemApplicationClassLoaderWorker.java:121)
at org.gradle.process.internal.worker.child.SystemApplicationClassLoaderWorker.call(SystemApplicationClassLoaderWorker.java:71)
at worker.org.gradle.process.internal.worker.GradleWorkerMain.run(GradleWorkerMain.java:69)
at worker.org.gradle.process.internal.worker.GradleWorkerMain.main(GradleWorkerMain.java:74)
Check failure on line 53 in cli-impl/src/test/java/org/aya/test/LibraryTest.java
github-actions / junit-tests
LibraryTest.[1] success
java.lang.AssertionError: Failed with `class org.aya.tyck.error.MetaVarError$BadlyScopedError`: In file data/vec/properties.aya:13:8 ->
11 | (xs ++ (ys ++ zs))
12 | ((xs ++ ys) ++ zs) elim xs
13 | | [] => refl
| ^--^
Error: The solution
Vec (+-assoc i) A
is not well-scoped
Only the variables below are allowed: `A`, `m`, `o`, `ys`, `zs`
at (373-376) [13:8-13:11]Raw output
java.lang.AssertionError: Failed with `class org.aya.tyck.error.MetaVarError$BadlyScopedError`: In file data/vec/properties.aya:13:8 ->
11 | (xs ++ (ys ++ zs))
12 | ((xs ++ ys) ++ zs) elim xs
13 | | [] => refl
| ^--^
Error: The solution
Vec (+-assoc i) A
is not well-scoped
Only the variables below are allowed: `A`, `m`, `o`, `ys`, `zs`
at (373-376) [13:8-13:11]
at org.aya.util.reporter.ThrowingReporter.report(ThrowingReporter.java:15)
at org.aya.util.reporter.CountingReporter$Delegated.report(CountingReporter.java:63)
at org.aya.util.reporter.CountingReporter$Delegated.report(CountingReporter.java:63)
at kala.collection.IndexedSeqLike.forEach(IndexedSeqLike.java:803)
at org.aya.util.reporter.DelayedReporter.reportNow(DelayedReporter.java:21)
at org.aya.util.reporter.DelayedReporter.close(DelayedReporter.java:26)
at org.aya.resolve.module.ModuleLoader.tyckModule(ModuleLoader.java:43)
at org.aya.cli.library.LibraryModuleLoader.load(LibraryModuleLoader.java:77)
at org.aya.resolve.module.CachedModuleLoader.lambda$load$0(CachedModuleLoader.java:26)
at kala.collection.mutable.MutableTreeMap.getOrPut(MutableTreeMap.java:483)
at org.aya.resolve.module.CachedModuleLoader.load(CachedModuleLoader.java:26)
at org.aya.resolve.module.ModuleLoader.load(ModuleLoader.java:89)
at org.aya.cli.library.LibraryCompiler$LibrarySccTycker.tyckOne(LibraryCompiler.java:376)
at org.aya.cli.library.LibraryCompiler$LibrarySccTycker.tyckSCC(LibraryCompiler.java:362)
at org.aya.util.tyck.OrgaTycker.tyckSCC(OrgaTycker.java:25)
at kala.function.CheckedConsumer.accept(CheckedConsumer.java:36)
at kala.collection.immutable.ImmutableVectors$Vector1.forEach(ImmutableVectors.java:460)
at kala.collection.base.Traversable.forEachChecked(Traversable.java:976)
at org.aya.cli.library.LibraryCompiler.make(LibraryCompiler.java:262)
at org.aya.cli.library.LibraryCompiler.make(LibraryCompiler.java:231)
at org.aya.cli.library.LibraryCompiler.make(LibraryCompiler.java:210)
at org.aya.cli.utils.CompilerUtil.catching(CompilerUtil.java:28)
at org.aya.cli.library.LibraryCompiler.start(LibraryCompiler.java:152)
at org.aya.cli.library.LibraryCompiler.compile(LibraryCompiler.java:95)
at org.aya.test.LibraryTest.compile(LibraryTest.java:149)
at org.aya.test.LibraryTest.compile(LibraryTest.java:145)
at org.aya.test.LibraryTest.testOnDisk(LibraryTest.java:53)
at java.base/jdk.internal.reflect.DirectMethodHandleAccessor.invoke(DirectMethodHandleAccessor.java:103)
at java.base/java.lang.reflect.Method.invoke(Method.java:580)
at org.junit.platform.commons.util.ReflectionUtils.invokeMethod(ReflectionUtils.java:767)
at org.junit.jupiter.engine.execution.MethodInvocation.proceed(MethodInvocation.java:60)
at org.junit.jupiter.engine.execution.InvocationInterceptorChain$ValidatingInvocation.proceed(InvocationInterceptorChain.java:131)
at org.junit.jupiter.engine.extension.TimeoutExtension.intercept(TimeoutExtension.java:156)
at org.junit.jupiter.engine.extension.TimeoutExtension.interceptTestableMethod(TimeoutExtension.java:147)
at org.junit.jupiter.engine.extension.TimeoutExtension.interceptTestTemplateMethod(TimeoutExtension.java:94)
at org.junit.jupiter.engine.execution.InterceptingExecutableInvoker$ReflectiveInterceptorCall.lambda$ofVoidMethod$0(InterceptingExecutableInvoker.java:103)
at org.junit.jupiter.engine.execution.InterceptingExecutableInvoker.lambda$invoke$0(InterceptingExecutableInvoker.java:93)
at org.junit.jupiter.engine.execution.InvocationInterceptorChain$InterceptedInvocation.proceed(InvocationInterceptorChain.java:106)
at org.junit.jupiter.engine.execution.InvocationInterceptorChain.proceed(InvocationInterceptorChain.java:64)
at org.junit.jupiter.engine.execution.InvocationInterceptorChain.chainAndInvoke(InvocationInterceptorChain.java:45)
at org.junit.jupiter.engine.execution.InvocationInterceptorChain.invoke(InvocationInterceptorChain.java:37)
at org.junit.jupiter.engine.execution.InterceptingExecutableInvoker.invoke(InterceptingExecutableInvoker.java:92)
at org.junit.jupiter.engine.execution.InterceptingExecutableInvoker.invoke(InterceptingExecutableInvoker.java:86)
at org.junit.jupiter.engine.descriptor.TestMethodTestDescriptor.lambda$invokeTestMethod$8(TestMethodTestDescriptor.java:217)
at org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
at org.junit.jupiter.engine.descriptor.TestMethodTestDescriptor.invokeTestMethod(TestMethodTestDescriptor.java:213)
at org.junit.jupiter.engine.descriptor.TestMethodTestDescriptor.execute(TestMethodTestDescriptor.java:138)
at org.junit.jupiter.engine.descriptor.TestMethodTestDescriptor.execute(TestMethodTestDescriptor.java:68)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$6(NodeTestTask.java:156)
at org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$8(NodeTestTask.java:146)
at org.junit.platform.engine.support.hierarchical.Node.around(Node.java:137)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$9(NodeTestTask.java:144)
at org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.executeRecursively(NodeTestTask.java:143)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.execute(NodeTestTask.java:100)
at org.junit.platform.engine.support.hierarchical.SameThreadHierarchicalTestExecutorService.submit(SameThreadHierarchicalTestExecutorService.java:35)
at org.junit.platform.engine.support.hierarchical.NodeTestTask$DefaultDynamicTestExecutor.execute(NodeTestTask.java:231)
at org.junit.platform.engine.support.hierarchical.NodeTestTask$DefaultDynamicTestExecutor.execute(NodeTestTask.java:209)
at org.junit.jupiter.engine.descriptor.TestTemplateTestDescriptor.execute(TestTemplateTestDescriptor.java:141)
at org.junit.jupiter.engine.descriptor.TestTemplateTestDescriptor.lambda$execute$3(TestTemplateTestDescriptor.java:109)
at java.base/java.util.stream.ForEachOps$ForEachOp$OfRef.accept(ForEachOps.java:184)
at java.base/java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:197)
at java.base/java.util.stream.ReferencePipeline$2$1.accept(ReferencePipeline.java:179)
at java.base/java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:197)
at java.base/java.util.stream.ForEachOps$ForEachOp$OfRef.accept(ForEachOps.java:184)
at java.base/java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:197)
at java.base/java.util.stream.ForEachOps$ForEachOp$OfRef.accept(ForEachOps.java:184)
at java.base/java.util.stream.ForEachOps$ForEachOp$OfRef.accept(ForEachOps.java:184)
at java.base/java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:197)
at java.base/java.util.Spliterators$ArraySpliterator.forEachRemaining(Spliterators.java:1024)
at java.base/java.util.stream.AbstractPipeline.copyInto(AbstractPipeline.java:509)
at java.base/java.util.stream.AbstractPipeline.wrapAndCopyInto(AbstractPipeline.java:499)
at java.base/java.util.stream.ForEachOps$ForEachOp.evaluateSequential(ForEachOps.java:151)
at java.base/java.util.stream.ForEachOps$ForEachOp$OfRef.evaluateSequential(ForEachOps.java:174)
at java.base/java.util.stream.AbstractPipeline.evaluate(AbstractPipeline.java:234)
at java.base/java.util.stream.ReferencePipeline.forEach(ReferencePipeline.java:596)
at java.base/java.util.stream.ReferencePipeline$7$1.accept(ReferencePipeline.java:276)
at java.base/java.util.ArrayList$ArrayListSpliterator.forEachRemaining(ArrayList.java:1708)
at java.base/java.util.stream.AbstractPipeline.copyInto(AbstractPipeline.java:509)
at java.base/java.util.stream.AbstractPipeline.wrapAndCopyInto(AbstractPipeline.java:499)
at java.base/java.util.stream.ForEachOps$ForEachOp.evaluateSequential(ForEachOps.java:151)
at java.base/java.util.stream.ForEachOps$ForEachOp$OfRef.evaluateSequential(ForEachOps.java:174)
at java.base/java.util.stream.AbstractPipeline.evaluate(AbstractPipeline.java:234)
at java.base/java.util.stream.ReferencePipeline.forEach(ReferencePipeline.java:596)
at java.base/java.util.stream.ReferencePipeline$7$1.accept(ReferencePipeline.java:276)
at java.base/java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:197)
at java.base/java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:197)
at java.base/java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:197)
at java.base/java.util.ArrayList$ArrayListSpliterator.forEachRemaining(ArrayList.java:1708)
at java.base/java.util.stream.AbstractPipeline.copyInto(AbstractPipeline.java:509)
at java.base/java.util.stream.AbstractPipeline.wrapAndCopyInto(AbstractPipeline.java:499)
at java.base/java.util.stream.ForEachOps$ForEachOp.evaluateSequential(ForEachOps.java:151)
at java.base/java.util.stream.ForEachOps$ForEachOp$OfRef.evaluateSequential(ForEachOps.java:174)
at java.base/java.util.stream.AbstractPipeline.evaluate(AbstractPipeline.java:234)
at java.base/java.util.stream.ReferencePipeline.forEach(ReferencePipeline.java:596)
at java.base/java.util.stream.ReferencePipeline$7$1.accept(ReferencePipeline.java:276)
at java.base/java.util.ArrayList$ArrayListSpliterator.forEachRemaining(ArrayList.java:1708)
at java.base/java.util.stream.AbstractPipeline.copyInto(AbstractPipeline.java:509)
at java.base/java.util.stream.AbstractPipeline.wrapAndCopyInto(AbstractPipeline.java:499)
at java.base/java.util.stream.ForEachOps$ForEachOp.evaluateSequential(ForEachOps.java:151)
at java.base/java.util.stream.ForEachOps$ForEachOp$OfRef.evaluateSequential(ForEachOps.java:174)
at java.base/java.util.stream.AbstractPipeline.evaluate(AbstractPipeline.java:234)
at java.base/java.util.stream.ReferencePipeline.forEach(ReferencePipeline.java:596)
at org.junit.jupiter.engine.descriptor.TestTemplateTestDescriptor.execute(TestTemplateTestDescriptor.java:109)
at org.junit.jupiter.engine.descriptor.TestTemplateTestDescriptor.execute(TestTemplateTestDescriptor.java:43)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$6(NodeTestTask.java:156)
at org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$8(NodeTestTask.java:146)
at org.junit.platform.engine.support.hierarchical.Node.around(Node.java:137)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$9(NodeTestTask.java:144)
at org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.executeRecursively(NodeTestTask.java:143)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.execute(NodeTestTask.java:100)
at java.base/java.util.ArrayList.forEach(ArrayList.java:1596)
at org.junit.platform.engine.support.hierarchical.SameThreadHierarchicalTestExecutorService.invokeAll(SameThreadHierarchicalTestExecutorService.java:41)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$6(NodeTestTask.java:160)
at org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$8(NodeTestTask.java:146)
at org.junit.platform.engine.support.hierarchical.Node.around(Node.java:137)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$9(NodeTestTask.java:144)
at org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.executeRecursively(NodeTestTask.java:143)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.execute(NodeTestTask.java:100)
at java.base/java.util.ArrayList.forEach(ArrayList.java:1596)
at org.junit.platform.engine.support.hierarchical.SameThreadHierarchicalTestExecutorService.invokeAll(SameThreadHierarchicalTestExecutorService.java:41)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$6(NodeTestTask.java:160)
at org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$8(NodeTestTask.java:146)
at org.junit.platform.engine.support.hierarchical.Node.around(Node.java:137)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$9(NodeTestTask.java:144)
at org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.executeRecursively(NodeTestTask.java:143)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.execute(NodeTestTask.java:100)
at org.junit.platform.engine.support.hierarchical.SameThreadHierarchicalTestExecutorService.submit(SameThreadHierarchicalTestExecutorService.java:35)
at org.junit.platform.engine.support.hierarchical.HierarchicalTestExecutor.execute(HierarchicalTestExecutor.java:57)
at org.junit.platform.engine.support.hierarchical.HierarchicalTestEngine.execute(HierarchicalTestEngine.java:54)
at org.junit.platform.launcher.core.EngineExecutionOrchestrator.execute(EngineExecutionOrchestrator.java:107)
at org.junit.platform.launcher.core.EngineExecutionOrchestrator.execute(EngineExecutionOrchestrator.java:88)
at org.junit.platform.launcher.core.EngineExecutionOrchestrator.lambda$execute$0(EngineExecutionOrchestrator.java:54)
at org.junit.platform.launcher.core.EngineExecutionOrchestrator.withInterceptedStreams(EngineExecutionOrchestrator.java:67)
at org.junit.platform.launcher.core.EngineExecutionOrchestrator.execute(EngineExecutionOrchestrator.java:52)
at org.junit.platform.launcher.core.DefaultLauncher.execute(DefaultLauncher.java:114)
at org.junit.platform.launcher.core.DefaultLauncher.execute(DefaultLauncher.java:86)
at org.junit.platform.launcher.core.DefaultLauncherSession$DelegatingLauncher.execute(DefaultLauncherSession.java:86)
at org.gradle.api.internal.tasks.testing.junitplatform.JUnitPlatformTestClassProcessor$CollectAllTestClassesExecutor.processAllTestClasses(JUnitPlatformTestClassProcessor.java:124)
at org.gradle.api.internal.tasks.testing.junitplatform.JUnitPlatformTestClassProcessor$CollectAllTestClassesExecutor.access$000(JUnitPlatformTestClassProcessor.java:99)
at org.gradle.api.internal.tasks.testing.junitplatform.JUnitPlatformTestClassProcessor.stop(JUnitPlatformTestClassProcessor.java:94)
at org.gradle.api.internal.tasks.testing.SuiteTestClassProcessor.stop(SuiteTestClassProcessor.java:63)
at java.base/jdk.internal.reflect.DirectMethodHandleAccessor.invoke(DirectMethodHandleAccessor.java:103)
at java.base/java.lang.reflect.Method.invoke(Method.java:580)
at org.gradle.internal.dispatch.ReflectionDispatch.dispatch(ReflectionDispatch.java:36)
at org.gradle.internal.dispatch.ReflectionDispatch.dispatch(ReflectionDispatch.java:24)
at org.gradle.internal.dispatch.ContextClassLoaderDispatch.dispatch(ContextClassLoaderDispatch.java:33)
at org.gradle.internal.dispatch.ProxyDispatchAdapter$DispatchingInvocationHandler.invoke(ProxyDispatchAdapter.java:92)
at jdk.proxy2/jdk.proxy2.$Proxy6.stop(Unknown Source)
at org.gradle.api.internal.tasks.testing.worker.TestWorker$3.run(TestWorker.java:200)
at org.gradle.api.internal.tasks.testing.worker.TestWorker.executeAndMaintainThreadName(TestWorker.java:132)
at org.gradle.api.internal.tasks.testing.worker.TestWorker.execute(TestWorker.java:103)
at org.gradle.api.internal.tasks.testing.worker.TestWorker.execute(TestWorker.java:63)
at org.gradle.process.internal.worker.child.ActionExecutionWorker.execute(ActionExecutionWorker.java:56)
at org.gradle.process.internal.worker.child.SystemApplicationClassLoaderWorker.call(SystemApplicationClassLoaderWorker.java:121)
at org.gradle.process.internal.worker.child.SystemApplicationClassLoaderWorker.call(SystemApplicationClassLoaderWorker.java:71)
at worker.org.gradle.process.internal.worker.GradleWorkerMain.run(GradleWorkerMain.java:69)
at worker.org.gradle.process.internal.worker.GradleWorkerMain.main(GradleWorkerMain.java:74)
Check failure on line 74 in cli-impl/src/test/java/org/aya/test/LibraryTest.java
github-actions / junit-tests
LibraryTest.testLiterate()
java.lang.AssertionError: Failed with `class org.aya.tyck.error.MetaVarError$BadlyScopedError`: In file data/vec/properties.aya:13:8 ->
11 | (xs ++ (ys ++ zs))
12 | ((xs ++ ys) ++ zs) elim xs
13 | | [] => refl
| ^--^
Error: The solution
Vec (+-assoc i) A
is not well-scoped
Only the variables below are allowed: `A`, `m`, `o`, `ys`, `zs`
at (373-376) [13:8-13:11]Raw output
java.lang.AssertionError: Failed with `class org.aya.tyck.error.MetaVarError$BadlyScopedError`: In file data/vec/properties.aya:13:8 ->
11 | (xs ++ (ys ++ zs))
12 | ((xs ++ ys) ++ zs) elim xs
13 | | [] => refl
| ^--^
Error: The solution
Vec (+-assoc i) A
is not well-scoped
Only the variables below are allowed: `A`, `m`, `o`, `ys`, `zs`
at (373-376) [13:8-13:11]
at org.aya.util.reporter.ThrowingReporter.report(ThrowingReporter.java:15)
at org.aya.util.reporter.CountingReporter$Delegated.report(CountingReporter.java:63)
at org.aya.util.reporter.CountingReporter$Delegated.report(CountingReporter.java:63)
at kala.collection.IndexedSeqLike.forEach(IndexedSeqLike.java:803)
at org.aya.util.reporter.DelayedReporter.reportNow(DelayedReporter.java:21)
at org.aya.util.reporter.DelayedReporter.close(DelayedReporter.java:26)
at org.aya.resolve.module.ModuleLoader.tyckModule(ModuleLoader.java:43)
at org.aya.cli.library.LibraryModuleLoader.load(LibraryModuleLoader.java:77)
at org.aya.resolve.module.CachedModuleLoader.lambda$load$0(CachedModuleLoader.java:26)
at kala.collection.mutable.MutableTreeMap.getOrPut(MutableTreeMap.java:483)
at org.aya.resolve.module.CachedModuleLoader.load(CachedModuleLoader.java:26)
at org.aya.resolve.module.ModuleLoader.load(ModuleLoader.java:89)
at org.aya.cli.library.LibraryCompiler$LibrarySccTycker.tyckOne(LibraryCompiler.java:376)
at org.aya.cli.library.LibraryCompiler$LibrarySccTycker.tyckSCC(LibraryCompiler.java:362)
at org.aya.util.tyck.OrgaTycker.tyckSCC(OrgaTycker.java:25)
at kala.function.CheckedConsumer.accept(CheckedConsumer.java:36)
at kala.collection.immutable.ImmutableVectors$Vector1.forEach(ImmutableVectors.java:460)
at kala.collection.base.Traversable.forEachChecked(Traversable.java:976)
at org.aya.cli.library.LibraryCompiler.make(LibraryCompiler.java:262)
at org.aya.cli.library.LibraryCompiler.make(LibraryCompiler.java:231)
at org.aya.cli.library.LibraryCompiler.make(LibraryCompiler.java:210)
at org.aya.cli.utils.CompilerUtil.catching(CompilerUtil.java:28)
at org.aya.cli.library.LibraryCompiler.start(LibraryCompiler.java:152)
at org.aya.cli.library.LibraryCompiler.compile(LibraryCompiler.java:95)
at org.aya.test.LibraryTest.compile(LibraryTest.java:149)
at org.aya.test.LibraryTest.testLiterate(LibraryTest.java:74)
at java.base/jdk.internal.reflect.DirectMethodHandleAccessor.invoke(DirectMethodHandleAccessor.java:103)
at java.base/java.lang.reflect.Method.invoke(Method.java:580)
at org.junit.platform.commons.util.ReflectionUtils.invokeMethod(ReflectionUtils.java:767)
at org.junit.jupiter.engine.execution.MethodInvocation.proceed(MethodInvocation.java:60)
at org.junit.jupiter.engine.execution.InvocationInterceptorChain$ValidatingInvocation.proceed(InvocationInterceptorChain.java:131)
at org.junit.jupiter.engine.extension.TimeoutExtension.intercept(TimeoutExtension.java:156)
at org.junit.jupiter.engine.extension.TimeoutExtension.interceptTestableMethod(TimeoutExtension.java:147)
at org.junit.jupiter.engine.extension.TimeoutExtension.interceptTestMethod(TimeoutExtension.java:86)
at org.junit.jupiter.engine.execution.InterceptingExecutableInvoker$ReflectiveInterceptorCall.lambda$ofVoidMethod$0(InterceptingExecutableInvoker.java:103)
at org.junit.jupiter.engine.execution.InterceptingExecutableInvoker.lambda$invoke$0(InterceptingExecutableInvoker.java:93)
at org.junit.jupiter.engine.execution.InvocationInterceptorChain$InterceptedInvocation.proceed(InvocationInterceptorChain.java:106)
at org.junit.jupiter.engine.execution.InvocationInterceptorChain.proceed(InvocationInterceptorChain.java:64)
at org.junit.jupiter.engine.execution.InvocationInterceptorChain.chainAndInvoke(InvocationInterceptorChain.java:45)
at org.junit.jupiter.engine.execution.InvocationInterceptorChain.invoke(InvocationInterceptorChain.java:37)
at org.junit.jupiter.engine.execution.InterceptingExecutableInvoker.invoke(InterceptingExecutableInvoker.java:92)
at org.junit.jupiter.engine.execution.InterceptingExecutableInvoker.invoke(InterceptingExecutableInvoker.java:86)
at org.junit.jupiter.engine.descriptor.TestMethodTestDescriptor.lambda$invokeTestMethod$8(TestMethodTestDescriptor.java:217)
at org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
at org.junit.jupiter.engine.descriptor.TestMethodTestDescriptor.invokeTestMethod(TestMethodTestDescriptor.java:213)
at org.junit.jupiter.engine.descriptor.TestMethodTestDescriptor.execute(TestMethodTestDescriptor.java:138)
at org.junit.jupiter.engine.descriptor.TestMethodTestDescriptor.execute(TestMethodTestDescriptor.java:68)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$6(NodeTestTask.java:156)
at org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$8(NodeTestTask.java:146)
at org.junit.platform.engine.support.hierarchical.Node.around(Node.java:137)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$9(NodeTestTask.java:144)
at org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.executeRecursively(NodeTestTask.java:143)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.execute(NodeTestTask.java:100)
at java.base/java.util.ArrayList.forEach(ArrayList.java:1596)
at org.junit.platform.engine.support.hierarchical.SameThreadHierarchicalTestExecutorService.invokeAll(SameThreadHierarchicalTestExecutorService.java:41)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$6(NodeTestTask.java:160)
at org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$8(NodeTestTask.java:146)
at org.junit.platform.engine.support.hierarchical.Node.around(Node.java:137)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$9(NodeTestTask.java:144)
at org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.executeRecursively(NodeTestTask.java:143)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.execute(NodeTestTask.java:100)
at java.base/java.util.ArrayList.forEach(ArrayList.java:1596)
at org.junit.platform.engine.support.hierarchical.SameThreadHierarchicalTestExecutorService.invokeAll(SameThreadHierarchicalTestExecutorService.java:41)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$6(NodeTestTask.java:160)
at org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$8(NodeTestTask.java:146)
at org.junit.platform.engine.support.hierarchical.Node.around(Node.java:137)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$9(NodeTestTask.java:144)
at org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.executeRecursively(NodeTestTask.java:143)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.execute(NodeTestTask.java:100)
at org.junit.platform.engine.support.hierarchical.SameThreadHierarchicalTestExecutorService.submit(SameThreadHierarchicalTestExecutorService.java:35)
at org.junit.platform.engine.support.hierarchical.HierarchicalTestExecutor.execute(HierarchicalTestExecutor.java:57)
at org.junit.platform.engine.support.hierarchical.HierarchicalTestEngine.execute(HierarchicalTestEngine.java:54)
at org.junit.platform.launcher.core.EngineExecutionOrchestrator.execute(EngineExecutionOrchestrator.java:107)
at org.junit.platform.launcher.core.EngineExecutionOrchestrator.execute(EngineExecutionOrchestrator.java:88)
at org.junit.platform.launcher.core.EngineExecutionOrchestrator.lambda$execute$0(EngineExecutionOrchestrator.java:54)
at org.junit.platform.launcher.core.EngineExecutionOrchestrator.withInterceptedStreams(EngineExecutionOrchestrator.java:67)
at org.junit.platform.launcher.core.EngineExecutionOrchestrator.execute(EngineExecutionOrchestrator.java:52)
at org.junit.platform.launcher.core.DefaultLauncher.execute(DefaultLauncher.java:114)
at org.junit.platform.launcher.core.DefaultLauncher.execute(DefaultLauncher.java:86)
at org.junit.platform.launcher.core.DefaultLauncherSession$DelegatingLauncher.execute(DefaultLauncherSession.java:86)
at org.gradle.api.internal.tasks.testing.junitplatform.JUnitPlatformTestClassProcessor$CollectAllTestClassesExecutor.processAllTestClasses(JUnitPlatformTestClassProcessor.java:124)
at org.gradle.api.internal.tasks.testing.junitplatform.JUnitPlatformTestClassProcessor$CollectAllTestClassesExecutor.access$000(JUnitPlatformTestClassProcessor.java:99)
at org.gradle.api.internal.tasks.testing.junitplatform.JUnitPlatformTestClassProcessor.stop(JUnitPlatformTestClassProcessor.java:94)
at org.gradle.api.internal.tasks.testing.SuiteTestClassProcessor.stop(SuiteTestClassProcessor.java:63)
at java.base/jdk.internal.reflect.DirectMethodHandleAccessor.invoke(DirectMethodHandleAccessor.java:103)
at java.base/java.lang.reflect.Method.invoke(Method.java:580)
at org.gradle.internal.dispatch.ReflectionDispatch.dispatch(ReflectionDispatch.java:36)
at org.gradle.internal.dispatch.ReflectionDispatch.dispatch(ReflectionDispatch.java:24)
at org.gradle.internal.dispatch.ContextClassLoaderDispatch.dispatch(ContextClassLoaderDispatch.java:33)
at org.gradle.internal.dispatch.ProxyDispatchAdapter$DispatchingInvocationHandler.invoke(ProxyDispatchAdapter.java:92)
at jdk.proxy2/jdk.proxy2.$Proxy6.stop(Unknown Source)
at org.gradle.api.internal.tasks.testing.worker.TestWorker$3.run(TestWorker.java:200)
at org.gradle.api.internal.tasks.testing.worker.TestWorker.executeAndMaintainThreadName(TestWorker.java:132)
at org.gradle.api.internal.tasks.testing.worker.TestWorker.execute(TestWorker.java:103)
at org.gradle.api.internal.tasks.testing.worker.TestWorker.execute(TestWorker.java:63)
at org.gradle.process.internal.worker.child.ActionExecutionWorker.execute(ActionExecutionWorker.java:56)
at org.gradle.process.internal.worker.child.SystemApplicationClassLoaderWorker.call(SystemApplicationClassLoaderWorker.java:121)
at org.gradle.process.internal.worker.child.SystemApplicationClassLoaderWorker.call(SystemApplicationClassLoaderWorker.java:71)
at worker.org.gradle.process.internal.worker.GradleWorkerMain.run(GradleWorkerMain.java:69)
at worker.org.gradle.process.internal.worker.GradleWorkerMain.main(GradleWorkerMain.java:74)
Check failure on line 48 in cli-impl/src/test/java/org/aya/test/TestRunner.java
github-actions / junit-tests
TestRunner.negative()
org.opentest4j.AssertionFailedError: GoalAndMeta.txt ==> expected: <Unsolved:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:18 ->
1 │ open import arith::nat::base
2 │ def test : Nat => _
│ ╰╯
Error: Unsolved meta _
1 error(s), 0 warning(s).
Let's learn from that.
Goal:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:28 ->
1 │ open import arith::nat::base
2 │ def test (a : Nat) : Nat => {? a ?}
│ ╰─────╯
Goal: Goal of type
Nat
(Normalized: Nat)
Context:
a : Nat
You are trying:
a
It has type:
Nat
0 error(s), 0 warning(s).
Let's learn from that.
UnsolvedMetaLit:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:5:17 ->
3 │ open inductive Option (A : Type)
4 │ | some A
5 │ def test => some 114514
│ ╰────╯
Error: Unsolved meta A
in `some 114514`
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:5:17 ->
3 │ open inductive Option (A : Type)
4 │ | some A
5 │ def test => some 114514
│ ╰────╯
Error: Unable to solve the type of this literal:
114514
I'm confused about the following candidates:
`Nat`, `Nat2`
2 error(s), 0 warning(s).
Let's learn from that.
Daylily:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:5:12 ->
3 │ def wow {A : Type 1} {B : A -> Type} (a b : A) (x : B a) (y : B b) : Bool => true
4 │ example def test1 (A B : Type) (x : A) (y : B) =>
5 │ wow A B x y
│ ╰╯ ╰╯ ?B A B x y A >= A
│ ╰╯ ?B A B x y B >= B
Info: Solving equation(s) with not very general solution(s)
That looks right!
Norell:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:7:28 ->
5 │ def test
6 │ (F : Type -> Type)
7 │ (g : ∀ (X : F _) -> F (Neg X)) : Nat => g 0
│ ╰╯
Error: Cannot check the expression
X
of type
F (?_ F)
against the type
Type 0
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:7:43 ->
5 │ def test
6 │ (F : Type -> Type)
7 │ (g : ∀ (X : F _) -> F (Neg X)) : Nat => g 0
│ ╰╯
Error: Cannot check the expression
0
of type
Nat
against the type
F (?_ F)
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:7:41 ->
5 │ def test
6 │ (F : Type -> Type)
7 │ (g : ∀ (X : F _) -> F (Neg X)) : Nat => g 0
│ ╰─╯
Error: Cannot check the expression
g 0
of type
F (Neg <X>)
(Normalized: F (<X> → Empty))
against the type
Nat
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:7:15 ->
5 │ def test
6 │ (F : Type -> Type)
7 │ (g : ∀ (X : F _) -> F (Neg X)) : Nat => g 0
│ ╰╯
Error: Unsolved meta _
in `^0 (?_ ^0)`
in `^0 (?_ ^0) → ^1 (Neg <X>)`
4 error(s), 0 warning(s).
Let's learn from that.
ScopeCheck:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:5:14 ->
3 │
4 │ // https://cstheory.stackexchange.com/a/49160/50892
5 │ def test (a : _) (B : Type) (b : B) (p : a = b) : I => 0
│ ╰╯
Error: The solution
B
is not well-scoped
Only the variables below are allowed:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:5:41 ->
3 │
4 │ // https://cstheory.stackexchange.com/a/49160/50892
5 │ def test (a : _) (B : Type) (b : B) (p : a = b) : I => 0
│ ╰╯
│ ╰╯ ?_ <= ?A a B b
Error: Equations do not have solutions!
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:5:14 ->
3 │
4 │ // https://cstheory.stackexchange.com/a/49160/50892
5 │ def test (a : _) (B : Type) (b : B) (p : a = b) : I => 0
│ ╰╯
Error: Unsolved meta _
3 error(s), 0 warning(s).
Let's learn from that.
LiteralAmbiguous3:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:6:4 ->
4 │
5 │ def good : List Unit => [ ]
6 │ def bad => [ unit ]
│ ╰─╯
Error: Unsolved meta _
in `?_`
in `[unit]`
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:6:11 ->
4 │
5 │ def good : List Unit => [ ]
6 │ def bad => [ unit ]
│ ╰──────╯
Error: Unable to solve the type of this literal:
[unit]
I'm confused about the following candidates:
`List`, `List2`
2 error(s), 0 warning(s).
Let's learn from that.
NonPattern:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:9:3 ->
6 │ def ++-assoc-type (xs : Vec n A) (ys : Vec m A) (zs : Vec o A)
7 │ => Path (fn i => Vec (+-assoc i) A)
8 │ (xs ++ (ys ++ zs))
│ ╰──────────────╯ ?b n A m o xs ys zs 0 >= m, ?c n A m o xs ys zs 0 >= o,
?a n A m o xs ys zs 0 >= n
9 │ ((xs ++ ys) ++ zs)
│ ╰──────────────╯
│ ╰──────────────╯ ?a n A m o xs ys zs 1 >= n, ?b n A m o xs ys zs 1 >= m,
?c n A m o xs ys zs 1 >= o
Info: Solving equation(s) with not very general solution(s)
That looks right!
UtensilFullFile:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:9:22 ->
7 │ def ++-assoc' (xs : Vec n A) (ys : Vec m A) (zs : Vec o A)
8 │ : Path (fn i ⇒ Vec (+-assoc i) A)
9 │ (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs
│ ╰──────────────╯ ╰──────────────╯ ?b n A m o xs ys zs 0 >= m, ?c
n A m o xs ys zs 0 >= o, ?a n A
m o xs ys zs 0 >= n
│ ╰──────────────╯ ?a n A m o xs ys zs 1 >= n, ?b n
A m o xs ys zs 1 >= m, ?c n A
m o xs ys zs 1 >= o
Info: Solving equation(s) with not very general solution(s)
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:11:18 ->
9 │ (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs
10 │ | [] ⇒ refl
11 │ | x :> _ => pmap (x :>) (++-assoc' _ _ _)
│ ╰──╯
Error: The solution
Vec (+-assoc {?n A x n m o _ ys zs} {?m A x n m o _ ys zs} {?o A x n m o _
ys zs} i) (?A A x n m o _ ys zs)
is not well-scoped
Only the variables below are allowed: `A`, `x`, `n`, `m`, `o`, `_`, `ys`,
`zs`
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:11:25 ->
9 │ (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs
10 │ | [] ⇒ refl
11 │ | x :> _ => pmap (x :>) (++-assoc' _ _ _)
│ ╰─────────────╯
Error: Cannot check the expression
++-assoc' _ _ _
of type
(++) {?n A x n m o _ ys zs} {?A A x n m o _ ys zs} {?m A x n m o _ ys zs +
?o A x n m o _ ys zs} (?_ A x n m o _ ys zs) ((++) {?m A x n m o _ ys zs} {?A
A x n m o _ ys zs} {?o A x n m o _ ys zs} (?_ A x n m o _ ys zs) (?_ A x
n m o _ ys zs)) = (++) {?n A x n m o _ ys zs + ?m A x n m o _ ys zs} {?A
A x n m o _ ys zs} {?o A x n m o _ ys zs} ((++) {?n A x n m o _ ys zs} {?A
A x n m o _ ys zs} {?m A x n m o _ ys zs} (?_ A x n m o _ ys zs) (?_ A x
n m o _ ys zs)) (?_ A x n m o _ ys zs)
against the type
?a A x n m o _ ys zs = ?b A x n m o _ ys zs
In particular, we failed to unify
?A A x n m o _ ys zs
with
Vec (+-assoc {?n A x n m o _ ys zs} {?m A x n m o _ ys zs} {?o A x n m o _
ys zs} i) (?A A x n m o _ ys zs)
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:11:18 ->
9 │ (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs
10 │ | [] ⇒ refl
11 │ | x :> _ => pmap (x :>) (++-assoc' _ _ _)
│ ╰──╯
Error: The solution
Vec (suc (+-assoc {n} {m} {o} i)) A
is not well-scoped
Only the variables below are allowed: `A`, `x`, `n`, `m`, `o`, `_`, `ys`,
`zs`
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:11:12 ->
9 │ (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs
10 │ | [] ⇒ refl
11 │ | x :> _ => pmap (x :>) (++-assoc' _ _ _)
│ ╰───────────────────────────╯
Error: Cannot check the expression
pmap (\ _ ⇒ x :> _) (++-assoc' _ _ _)
of type
(=) {?B A x n m o _ ys zs} (x :> ?a A x n m o _ ys zs) (x :> ?b A x n m
o _ ys zs)
(Normalized: (x :> ?a A x n m o _ ys zs) = (x :> ?b A x n m o _ ys zs))
against the type
(++) {suc n} {A} {m + o} (x :> _) ((++) {m} {A} {o} ys zs) = (++) {suc n +
m} {A} {o} ((++) {suc n} {A} {m} (x :> _) ys) zs
(Normalized: (x :> (++) {n} {A} {m + o} _ ((++) {m} {A} {o} ys zs)) = (x :>
(++) {n + m} {A} {o} ((++) {n} {A} {m} _ ys) zs))
In particular, we failed to unify
?B A x n m o _ ys zs
with
Vec (+-assoc {suc n} {m} {o} i) A
(Normalized: Vec (suc (+-assoc {n} {m} {o} i)) A)
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:11:18 ->
9 │ (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs
10 │ | [] ⇒ refl
11 │ | x :> _ => pmap (x :>) (++-assoc' _ _ _)
│ ╰──╯
Error: The solution
Vec (?n A x n m o _ ys zs _) (?A A x n m o _ ys zs _)
is not well-scoped
Only the variables below are allowed: `A`, `x`, `n`, `m`, `o`, `_`, `ys`,
`zs`
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:11:18 ->
9 │ (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs
10 │ | [] ⇒ refl
11 │ | x :> _ => pmap (x :>) (++-assoc' _ _ _)
│ ╰──╯
Error: The solution
Vec (suc (?n A x n m o _ ys zs _)) (?A A x n m o _ ys zs _)
is not well-scoped
Only the variables below are allowed: `A`, `x`, `n`, `m`, `o`, `_`, `ys`,
`zs`
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:11:18 ->
9 │ (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs
10 │ | [] ⇒ refl
11 │ | x :> _ => pmap (x :>) (++-assoc' _ _ _)
│ ╰──╯
│ ╰──╯ ?B A x n m o _ ys zs >= Vec (suc (?n A x n m
o _ ys zs _)) (?A A x n m o _ ys zs _)
│ ╰╯ ?A A x n m o _ ys zs <= Vec (?n A x n m o _ ys
zs _) (?A A x n m o _ ys zs _)
Error: Equations do not have solutions!
7 error(s), 0 warning(s).
Let's learn from that.
> but was: <Unsolved:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:18 ->
1 │ open import arith::nat::base
2 │ def test : Nat => _
│ ╰╯
Error: Unsolved meta _
1 error(s), 0 warning(s).
Let's learn from that.
Goal:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:28 ->
1 │ open import arith::nat::base
2 │ def test (a : Nat) : Nat => {? a ?}
│ ╰─────╯
Goal: Goal of type
Nat
(Normalized: Nat)
Context:
a : Nat
You are trying:
a
It has type:
Nat
0 error(s), 0 warning(s).
Let's learn from that.
UnsolvedMetaLit:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:5:17 ->
3 │ open inductive Option (A : Type)
4 │ | some A
5 │ def test => some 114514
│ ╰────╯
Error: Unsolved meta A
in `some 114514`
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:5:17 ->
3 │ open inductive Option (A : Type)
4 │ | some A
5 │ def test => some 114514
│ ╰────╯
Error: Unable to solve the type of this literal:
114514
I'm confused about the following candidates:
`Nat`, `Nat2`
2 error(s), 0 warning(s).
Let's learn from that.
Daylily:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:5:12 ->
3 │ def wow {A : Type 1} {B : A -> Type} (a b : A) (x : B a) (y : B b) : Bool => true
4 │ example def test1 (A B : Type) (x : A) (y : B) =>
5 │ wow A B x y
│ ╰╯ ╰╯ ?B A B x y A >= A
│ ╰╯ ?B A B x y B >= B
Info: Solving equation(s) with not very general solution(s)
That looks right!
Norell:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:7:28 ->
5 │ def test
6 │ (F : Type -> Type)
7 │ (g : ∀ (X : F _) -> F (Neg X)) : Nat => g 0
│ ╰╯
Error: Cannot check the expression
X
of type
F (?_ F)
against the type
Type 0
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:7:43 ->
5 │ def test
6 │ (F : Type -> Type)
7 │ (g : ∀ (X : F _) -> F (Neg X)) : Nat => g 0
│ ╰╯
Error: Cannot check the expression
0
of type
Nat
against the type
F (?_ F)
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:7:41 ->
5 │ def test
6 │ (F : Type -> Type)
7 │ (g : ∀ (X : F _) -> F (Neg X)) : Nat => g 0
│ ╰─╯
Error: Cannot check the expression
g 0
of type
F (Neg <X>)
(Normalized: F (<X> → Empty))
against the type
Nat
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:7:15 ->
5 │ def test
6 │ (F : Type -> Type)
7 │ (g : ∀ (X : F _) -> F (Neg X)) : Nat => g 0
│ ╰╯
Error: Unsolved meta _
in `^0 (?_ ^0)`
in `^0 (?_ ^0) → ^1 (Neg <X>)`
4 error(s), 0 warning(s).
Let's learn from that.
ScopeCheck:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:5:14 ->
3 │
4 │ // https://cstheory.stackexchange.com/a/49160/50892
5 │ def test (a : _) (B : Type) (b : B) (p : a = b) : I => 0
│ ╰╯
Error: The solution
B
is not well-scoped
Only the variables below are allowed:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:5:41 ->
3 │
4 │ // https://cstheory.stackexchange.com/a/49160/50892
5 │ def test (a : _) (B : Type) (b : B) (p : a = b) : I => 0
│ ╰╯
│ ╰╯ ?_ <= ?A a B b
Error: Equations do not have solutions!
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:5:14 ->
3 │
4 │ // https://cstheory.stackexchange.com/a/49160/50892
5 │ def test (a : _) (B : Type) (b : B) (p : a = b) : I => 0
│ ╰╯
Error: Unsolved meta _
3 error(s), 0 warning(s).
Let's learn from that.
LiteralAmbiguous3:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:6:4 ->
4 │
5 │ def good : List Unit => [ ]
6 │ def bad => [ unit ]
│ ╰─╯
Error: Unsolved meta _
in `?_`
in `[unit]`
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:6:11 ->
4 │
5 │ def good : List Unit => [ ]
6 │ def bad => [ unit ]
│ ╰──────╯
Error: Unable to solve the type of this literal:
[unit]
I'm confused about the following candidates:
`List`, `List2`
2 error(s), 0 warning(s).
Let's learn from that.
NonPattern:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:9:3 ->
6 │ def ++-assoc-type (xs : Vec n A) (ys : Vec m A) (zs : Vec o A)
7 │ => Path (fn i => Vec (+-assoc i) A)
8 │ (xs ++ (ys ++ zs))
│ ╰──────────────╯ ?b n A m o xs ys zs 0 >= m, ?c n A m o xs ys zs 0 >= o,
?a n A m o xs ys zs 0 >= n
9 │ ((xs ++ ys) ++ zs)
│ ╰──────────────╯
│ ╰──────────────╯ ?a n A m o xs ys zs 1 >= n, ?b n A m o xs ys zs 1 >= m,
?c n A m o xs ys zs 1 >= o
Info: Solving equation(s) with not very general solution(s)
That looks right!
UtensilFullFile:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:9:22 ->
7 │ def ++-assoc' (xs : Vec n A) (ys : Vec m A) (zs : Vec o A)
8 │ : Path (fn i ⇒ Vec (+-assoc i) A)
9 │ (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs
│ ╰──────────────╯ ╰──────────────╯ ?b n A m o xs ys zs 0 >= m, ?c
n A m o xs ys zs 0 >= o, ?a n A
m o xs ys zs 0 >= n
│ ╰──────────────╯ ?a n A m o xs ys zs 1 >= n, ?b n
A m o xs ys zs 1 >= m, ?c n A
m o xs ys zs 1 >= o
Info: Solving equation(s) with not very general solution(s)
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:10:7 ->
8 │ : Path (fn i ⇒ Vec (+-assoc i) A)
9 │ (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs
10 │ | [] ⇒ refl
│ ╰──╯
Error: The solution
Vec (+-assoc {zero} {m} {o} i) A
is not well-scoped
Only the variables below are allowed: `A`, `m`, `o`, `ys`, `zs`
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:10:7 ->
8 │ : Path (fn i ⇒ Vec (+-assoc i) A)
9 │ (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs
10 │ | [] ⇒ refl
│ ╰──╯
Error: Cannot check the expression
refl
of type
(=) {?A A m o ys zs} (?a A m o ys zs) (?a A m o ys zs)
(Normalized: ?a A m o ys zs = ?a A m o ys zs)
against the type
(++) {zero} {A} {m + o} [] ((++) {m} {A} {o} ys zs) = (++) {zero + m} {A}
{o} ((++) {zero} {A} {m} [] ys) zs
In particular, we failed to unify
?A A m o ys zs
with
Vec (+-assoc {zero} {m} {o} i) A
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:11:18 ->
9 │ (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs
10 │ | [] ⇒ refl
11 │ | x :> _ => pmap (x :>) (++-assoc' _ _ _)
│ ╰──╯
Error: The solution
Vec (+-assoc {?n A x n m o _ ys zs} {?m A x n m o _ ys zs} {?o A x n m o _
ys zs} i) (?A A x n m o _ ys zs)
is not well-scoped
Only the variables below are allowed: `A`, `x`, `n`, `m`, `o`, `_`, `ys`,
`zs`
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:11:25 ->
9 │ (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs
10 │ | [] ⇒ refl
11 │ | x :> _ => pmap (x :>) (++-assoc' _ _ _)
│ ╰─────────────╯
Error: Cannot check the expression
++-assoc' _ _ _
of type
(++) {?n A x n m o _ ys zs} {?A A x n m o _ ys zs} {?m A x n m o _ ys zs +
?o A x n m o _ ys zs} (?_ A x n m o _ ys zs) ((++) {?m A x n m o _ ys zs} {?A
A x n m o _ ys zs} {?o A x n m o _ ys zs} (?_ A x n m o _ ys zs) (?_ A x
n m o _ ys zs)) = (++) {?n A x n m o _ ys zs + ?m A x n m o _ ys zs} {?A
A x n m o _ ys zs} {?o A x n m o _ ys zs} ((++) {?n A x n m o _ ys zs} {?A
A x n m o _ ys zs} {?m A x n m o _ ys zs} (?_ A x n m o _ ys zs) (?_ A x
n m o _ ys zs)) (?_ A x n m o _ ys zs)
against the type
?a A x n m o _ ys zs = ?b A x n m o _ ys zs
In particular, we failed to unify
?A A x n m o _ ys zs
with
Vec (+-assoc {?n A x n m o _ ys zs} {?m A x n m o _ ys zs} {?o A x n m o _
ys zs} i) (?A A x n m o _ ys zs)
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:11:18 ->
9 │ (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs
10 │ | [] ⇒ refl
11 │ | x :> _ => pmap (x :>) (++-assoc' _ _ _)
│ ╰──╯
Error: The solution
Vec (+-assoc {suc n} {m} {o} i) A
is not well-scoped
Only the variables below are allowed: `A`, `x`, `n`, `m`, `o`, `_`, `ys`,
`zs`
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:11:12 ->
9 │ (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs
10 │ | [] ⇒ refl
11 │ | x :> _ => pmap (x :>) (++-assoc' _ _ _)
│ ╰───────────────────────────╯
Error: Cannot check the expression
pmap (\ _ ⇒ x :> _) (++-assoc' _ _ _)
of type
(=) {?B A x n m o _ ys zs} (x :> ?a A x n m o _ ys zs) (x :> ?b A x n m
o _ ys zs)
(Normalized: (x :> ?a A x n m o _ ys zs) = (x :> ?b A x n m o _ ys zs))
against the type
(++) {suc n} {A} {m + o} (x :> _) ((++) {m} {A} {o} ys zs) = (++) {suc n +
m} {A} {o} ((++) {suc n} {A} {m} (x :> _) ys) zs
In particular, we failed to unify
?B A x n m o _ ys zs
with
Vec (+-assoc {suc n} {m} {o} i) A
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:11:18 ->
9 │ (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs
10 │ | [] ⇒ refl
11 │ | x :> _ => pmap (x :>) (++-assoc' _ _ _)
│ ╰──╯
Error: The solution
Vec (?n A x n m o _ ys zs _) (?A A x n m o _ ys zs _)
is not well-scoped
Only the variables below are allowed: `A`, `x`, `n`, `m`, `o`, `_`, `ys`,
`zs`
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:11:18 ->
9 │ (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs
10 │ | [] ⇒ refl
11 │ | x :> _ => pmap (x :>) (++-assoc' _ _ _)
│ ╰──╯
Error: The solution
Vec (suc (?n A x n m o _ ys zs _)) (?A A x n m o _ ys zs _)
is not well-scoped
Only the variables below are allowed: `A`, `x`, `n`, `m`, `o`, `_`, `ys`,
`zs`
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:11:18 ->
9 │ (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs
10 │ | [] ⇒ refl
11 │ | x :> _ => pmap (x :>) (++-assoc' _ _ _)
│ ╰──╯
│ ╰──╯ ?B A x n m o _ ys zs >= Vec (suc (?n A x n m
o _ ys zs _)) (?A A x n m o _ ys zs _)
│ ╰╯ ?A A x n m o _ ys zs <= Vec (?n A x n m o _ ys
zs _) (?A A x n m o _ ys zs _)
Error: Equations do not have solutions!
9 error(s), 0 warning(s).
Let's learn from that.
>Raw output
org.opentest4j.AssertionFailedError: GoalAndMeta.txt ==> expected: <Unsolved:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:18 ->
1 │ open import arith::nat::base
2 │ def test : Nat => _
│ ╰╯
Error: Unsolved meta _
1 error(s), 0 warning(s).
Let's learn from that.
Goal:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:28 ->
1 │ open import arith::nat::base
2 │ def test (a : Nat) : Nat => {? a ?}
│ ╰─────╯
Goal: Goal of type
Nat
(Normalized: Nat)
Context:
a : Nat
You are trying:
a
It has type:
Nat
0 error(s), 0 warning(s).
Let's learn from that.
UnsolvedMetaLit:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:5:17 ->
3 │ open inductive Option (A : Type)
4 │ | some A
5 │ def test => some 114514
│ ╰────╯
Error: Unsolved meta A
in `some 114514`
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:5:17 ->
3 │ open inductive Option (A : Type)
4 │ | some A
5 │ def test => some 114514
│ ╰────╯
Error: Unable to solve the type of this literal:
114514
I'm confused about the following candidates:
`Nat`, `Nat2`
2 error(s), 0 warning(s).
Let's learn from that.
Daylily:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:5:12 ->
3 │ def wow {A : Type 1} {B : A -> Type} (a b : A) (x : B a) (y : B b) : Bool => true
4 │ example def test1 (A B : Type) (x : A) (y : B) =>
5 │ wow A B x y
│ ╰╯ ╰╯ ?B A B x y A >= A
│ ╰╯ ?B A B x y B >= B
Info: Solving equation(s) with not very general solution(s)
That looks right!
Norell:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:7:28 ->
5 │ def test
6 │ (F : Type -> Type)
7 │ (g : ∀ (X : F _) -> F (Neg X)) : Nat => g 0
│ ╰╯
Error: Cannot check the expression
X
of type
F (?_ F)
against the type
Type 0
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:7:43 ->
5 │ def test
6 │ (F : Type -> Type)
7 │ (g : ∀ (X : F _) -> F (Neg X)) : Nat => g 0
│ ╰╯
Error: Cannot check the expression
0
of type
Nat
against the type
F (?_ F)
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:7:41 ->
5 │ def test
6 │ (F : Type -> Type)
7 │ (g : ∀ (X : F _) -> F (Neg X)) : Nat => g 0
│ ╰─╯
Error: Cannot check the expression
g 0
of type
F (Neg <X>)
(Normalized: F (<X> → Empty))
against the type
Nat
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:7:15 ->
5 │ def test
6 │ (F : Type -> Type)
7 │ (g : ∀ (X : F _) -> F (Neg X)) : Nat => g 0
│ ╰╯
Error: Unsolved meta _
in `^0 (?_ ^0)`
in `^0 (?_ ^0) → ^1 (Neg <X>)`
4 error(s), 0 warning(s).
Let's learn from that.
ScopeCheck:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:5:14 ->
3 │
4 │ // https://cstheory.stackexchange.com/a/49160/50892
5 │ def test (a : _) (B : Type) (b : B) (p : a = b) : I => 0
│ ╰╯
Error: The solution
B
is not well-scoped
Only the variables below are allowed:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:5:41 ->
3 │
4 │ // https://cstheory.stackexchange.com/a/49160/50892
5 │ def test (a : _) (B : Type) (b : B) (p : a = b) : I => 0
│ ╰╯
│ ╰╯ ?_ <= ?A a B b
Error: Equations do not have solutions!
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:5:14 ->
3 │
4 │ // https://cstheory.stackexchange.com/a/49160/50892
5 │ def test (a : _) (B : Type) (b : B) (p : a = b) : I => 0
│ ╰╯
Error: Unsolved meta _
3 error(s), 0 warning(s).
Let's learn from that.
LiteralAmbiguous3:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:6:4 ->
4 │
5 │ def good : List Unit => [ ]
6 │ def bad => [ unit ]
│ ╰─╯
Error: Unsolved meta _
in `?_`
in `[unit]`
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:6:11 ->
4 │
5 │ def good : List Unit => [ ]
6 │ def bad => [ unit ]
│ ╰──────╯
Error: Unable to solve the type of this literal:
[unit]
I'm confused about the following candidates:
`List`, `List2`
2 error(s), 0 warning(s).
Let's learn from that.
NonPattern:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:9:3 ->
6 │ def ++-assoc-type (xs : Vec n A) (ys : Vec m A) (zs : Vec o A)
7 │ => Path (fn i => Vec (+-assoc i) A)
8 │ (xs ++ (ys ++ zs))
│ ╰──────────────╯ ?b n A m o xs ys zs 0 >= m, ?c n A m o xs ys zs 0 >= o,
?a n A m o xs ys zs 0 >= n
9 │ ((xs ++ ys) ++ zs)
│ ╰──────────────╯
│ ╰──────────────╯ ?a n A m o xs ys zs 1 >= n, ?b n A m o xs ys zs 1 >= m,
?c n A m o xs ys zs 1 >= o
Info: Solving equation(s) with not very general solution(s)
That looks right!
UtensilFullFile:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:9:22 ->
7 │ def ++-assoc' (xs : Vec n A) (ys : Vec m A) (zs : Vec o A)
8 │ : Path (fn i ⇒ Vec (+-assoc i) A)
9 │ (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs
│ ╰──────────────╯ ╰──────────────╯ ?b n A m o xs ys zs 0 >= m, ?c
n A m o xs ys zs 0 >= o, ?a n A
m o xs ys zs 0 >= n
│ ╰──────────────╯ ?a n A m o xs ys zs 1 >= n, ?b n
A m o xs ys zs 1 >= m, ?c n A
m o xs ys zs 1 >= o
Info: Solving equation(s) with not very general solution(s)
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:11:18 ->
9 │ (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs
10 │ | [] ⇒ refl
11 │ | x :> _ => pmap (x :>) (++-assoc' _ _ _)
│ ╰──╯
Error: The solution
Vec (+-assoc {?n A x n m o _ ys zs} {?m A x n m o _ ys zs} {?o A x n m o _
ys zs} i) (?A A x n m o _ ys zs)
is not well-scoped
Only the variables below are allowed: `A`, `x`, `n`, `m`, `o`, `_`, `ys`,
`zs`
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:11:25 ->
9 │ (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs
10 │ | [] ⇒ refl
11 │ | x :> _ => pmap (x :>) (++-assoc' _ _ _)
│ ╰─────────────╯
Error: Cannot check the expression
++-assoc' _ _ _
of type
(++) {?n A x n m o _ ys zs} {?A A x n m o _ ys zs} {?m A x n m o _ ys zs +
?o A x n m o _ ys zs} (?_ A x n m o _ ys zs) ((++) {?m A x n m o _ ys zs} {?A
A x n m o _ ys zs} {?o A x n m o _ ys zs} (?_ A x n m o _ ys zs) (?_ A x
n m o _ ys zs)) = (++) {?n A x n m o _ ys zs + ?m A x n m o _ ys zs} {?A
A x n m o _ ys zs} {?o A x n m o _ ys zs} ((++) {?n A x n m o _ ys zs} {?A
A x n m o _ ys zs} {?m A x n m o _ ys zs} (?_ A x n m o _ ys zs) (?_ A x
n m o _ ys zs)) (?_ A x n m o _ ys zs)
against the type
?a A x n m o _ ys zs = ?b A x n m o _ ys zs
In particular, we failed to unify
?A A x n m o _ ys zs
with
Vec (+-assoc {?n A x n m o _ ys zs} {?m A x n m o _ ys zs} {?o A x n m o _
ys zs} i) (?A A x n m o _ ys zs)
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:11:18 ->
9 │ (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs
10 │ | [] ⇒ refl
11 │ | x :> _ => pmap (x :>) (++-assoc' _ _ _)
│ ╰──╯
Error: The solution
Vec (suc (+-assoc {n} {m} {o} i)) A
is not well-scoped
Only the variables below are allowed: `A`, `x`, `n`, `m`, `o`, `_`, `ys`,
`zs`
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:11:12 ->
9 │ (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs
10 │ | [] ⇒ refl
11 │ | x :> _ => pmap (x :>) (++-assoc' _ _ _)
│ ╰───────────────────────────╯
Error: Cannot check the expression
pmap (\ _ ⇒ x :> _) (++-assoc' _ _ _)
of type
(=) {?B A x n m o _ ys zs} (x :> ?a A x n m o _ ys zs) (x :> ?b A x n m
o _ ys zs)
(Normalized: (x :> ?a A x n m o _ ys zs) = (x :> ?b A x n m o _ ys zs))
against the type
(++) {suc n} {A} {m + o} (x :> _) ((++) {m} {A} {o} ys zs) = (++) {suc n +
m} {A} {o} ((++) {suc n} {A} {m} (x :> _) ys) zs
(Normalized: (x :> (++) {n} {A} {m + o} _ ((++) {m} {A} {o} ys zs)) = (x :>
(++) {n + m} {A} {o} ((++) {n} {A} {m} _ ys) zs))
In particular, we failed to unify
?B A x n m o _ ys zs
with
Vec (+-assoc {suc n} {m} {o} i) A
(Normalized: Vec (suc (+-assoc {n} {m} {o} i)) A)
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:11:18 ->
9 │ (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs
10 │ | [] ⇒ refl
11 │ | x :> _ => pmap (x :>) (++-assoc' _ _ _)
│ ╰──╯
Error: The solution
Vec (?n A x n m o _ ys zs _) (?A A x n m o _ ys zs _)
is not well-scoped
Only the variables below are allowed: `A`, `x`, `n`, `m`, `o`, `_`, `ys`,
`zs`
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:11:18 ->
9 │ (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs
10 │ | [] ⇒ refl
11 │ | x :> _ => pmap (x :>) (++-assoc' _ _ _)
│ ╰──╯
Error: The solution
Vec (suc (?n A x n m o _ ys zs _)) (?A A x n m o _ ys zs _)
is not well-scoped
Only the variables below are allowed: `A`, `x`, `n`, `m`, `o`, `_`, `ys`,
`zs`
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:11:18 ->
9 │ (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs
10 │ | [] ⇒ refl
11 │ | x :> _ => pmap (x :>) (++-assoc' _ _ _)
│ ╰──╯
│ ╰──╯ ?B A x n m o _ ys zs >= Vec (suc (?n A x n m
o _ ys zs _)) (?A A x n m o _ ys zs _)
│ ╰╯ ?A A x n m o _ ys zs <= Vec (?n A x n m o _ ys
zs _) (?A A x n m o _ ys zs _)
Error: Equations do not have solutions!
7 error(s), 0 warning(s).
Let's learn from that.
> but was: <Unsolved:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:18 ->
1 │ open import arith::nat::base
2 │ def test : Nat => _
│ ╰╯
Error: Unsolved meta _
1 error(s), 0 warning(s).
Let's learn from that.
Goal:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:28 ->
1 │ open import arith::nat::base
2 │ def test (a : Nat) : Nat => {? a ?}
│ ╰─────╯
Goal: Goal of type
Nat
(Normalized: Nat)
Context:
a : Nat
You are trying:
a
It has type:
Nat
0 error(s), 0 warning(s).
Let's learn from that.
UnsolvedMetaLit:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:5:17 ->
3 │ open inductive Option (A : Type)
4 │ | some A
5 │ def test => some 114514
│ ╰────╯
Error: Unsolved meta A
in `some 114514`
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:5:17 ->
3 │ open inductive Option (A : Type)
4 │ | some A
5 │ def test => some 114514
│ ╰────╯
Error: Unable to solve the type of this literal:
114514
I'm confused about the following candidates:
`Nat`, `Nat2`
2 error(s), 0 warning(s).
Let's learn from that.
Daylily:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:5:12 ->
3 │ def wow {A : Type 1} {B : A -> Type} (a b : A) (x : B a) (y : B b) : Bool => true
4 │ example def test1 (A B : Type) (x : A) (y : B) =>
5 │ wow A B x y
│ ╰╯ ╰╯ ?B A B x y A >= A
│ ╰╯ ?B A B x y B >= B
Info: Solving equation(s) with not very general solution(s)
That looks right!
Norell:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:7:28 ->
5 │ def test
6 │ (F : Type -> Type)
7 │ (g : ∀ (X : F _) -> F (Neg X)) : Nat => g 0
│ ╰╯
Error: Cannot check the expression
X
of type
F (?_ F)
against the type
Type 0
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:7:43 ->
5 │ def test
6 │ (F : Type -> Type)
7 │ (g : ∀ (X : F _) -> F (Neg X)) : Nat => g 0
│ ╰╯
Error: Cannot check the expression
0
of type
Nat
against the type
F (?_ F)
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:7:41 ->
5 │ def test
6 │ (F : Type -> Type)
7 │ (g : ∀ (X : F _) -> F (Neg X)) : Nat => g 0
│ ╰─╯
Error: Cannot check the expression
g 0
of type
F (Neg <X>)
(Normalized: F (<X> → Empty))
against the type
Nat
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:7:15 ->
5 │ def test
6 │ (F : Type -> Type)
7 │ (g : ∀ (X : F _) -> F (Neg X)) : Nat => g 0
│ ╰╯
Error: Unsolved meta _
in `^0 (?_ ^0)`
in `^0 (?_ ^0) → ^1 (Neg <X>)`
4 error(s), 0 warning(s).
Let's learn from that.
ScopeCheck:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:5:14 ->
3 │
4 │ // https://cstheory.stackexchange.com/a/49160/50892
5 │ def test (a : _) (B : Type) (b : B) (p : a = b) : I => 0
│ ╰╯
Error: The solution
B
is not well-scoped
Only the variables below are allowed:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:5:41 ->
3 │
4 │ // https://cstheory.stackexchange.com/a/49160/50892
5 │ def test (a : _) (B : Type) (b : B) (p : a = b) : I => 0
│ ╰╯
│ ╰╯ ?_ <= ?A a B b
Error: Equations do not have solutions!
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:5:14 ->
3 │
4 │ // https://cstheory.stackexchange.com/a/49160/50892
5 │ def test (a : _) (B : Type) (b : B) (p : a = b) : I => 0
│ ╰╯
Error: Unsolved meta _
3 error(s), 0 warning(s).
Let's learn from that.
LiteralAmbiguous3:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:6:4 ->
4 │
5 │ def good : List Unit => [ ]
6 │ def bad => [ unit ]
│ ╰─╯
Error: Unsolved meta _
in `?_`
in `[unit]`
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:6:11 ->
4 │
5 │ def good : List Unit => [ ]
6 │ def bad => [ unit ]
│ ╰──────╯
Error: Unable to solve the type of this literal:
[unit]
I'm confused about the following candidates:
`List`, `List2`
2 error(s), 0 warning(s).
Let's learn from that.
NonPattern:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:9:3 ->
6 │ def ++-assoc-type (xs : Vec n A) (ys : Vec m A) (zs : Vec o A)
7 │ => Path (fn i => Vec (+-assoc i) A)
8 │ (xs ++ (ys ++ zs))
│ ╰──────────────╯ ?b n A m o xs ys zs 0 >= m, ?c n A m o xs ys zs 0 >= o,
?a n A m o xs ys zs 0 >= n
9 │ ((xs ++ ys) ++ zs)
│ ╰──────────────╯
│ ╰──────────────╯ ?a n A m o xs ys zs 1 >= n, ?b n A m o xs ys zs 1 >= m,
?c n A m o xs ys zs 1 >= o
Info: Solving equation(s) with not very general solution(s)
That looks right!
UtensilFullFile:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:9:22 ->
7 │ def ++-assoc' (xs : Vec n A) (ys : Vec m A) (zs : Vec o A)
8 │ : Path (fn i ⇒ Vec (+-assoc i) A)
9 │ (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs
│ ╰──────────────╯ ╰──────────────╯ ?b n A m o xs ys zs 0 >= m, ?c
n A m o xs ys zs 0 >= o, ?a n A
m o xs ys zs 0 >= n
│ ╰──────────────╯ ?a n A m o xs ys zs 1 >= n, ?b n
A m o xs ys zs 1 >= m, ?c n A
m o xs ys zs 1 >= o
Info: Solving equation(s) with not very general solution(s)
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:10:7 ->
8 │ : Path (fn i ⇒ Vec (+-assoc i) A)
9 │ (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs
10 │ | [] ⇒ refl
│ ╰──╯
Error: The solution
Vec (+-assoc {zero} {m} {o} i) A
is not well-scoped
Only the variables below are allowed: `A`, `m`, `o`, `ys`, `zs`
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:10:7 ->
8 │ : Path (fn i ⇒ Vec (+-assoc i) A)
9 │ (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs
10 │ | [] ⇒ refl
│ ╰──╯
Error: Cannot check the expression
refl
of type
(=) {?A A m o ys zs} (?a A m o ys zs) (?a A m o ys zs)
(Normalized: ?a A m o ys zs = ?a A m o ys zs)
against the type
(++) {zero} {A} {m + o} [] ((++) {m} {A} {o} ys zs) = (++) {zero + m} {A}
{o} ((++) {zero} {A} {m} [] ys) zs
In particular, we failed to unify
?A A m o ys zs
with
Vec (+-assoc {zero} {m} {o} i) A
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:11:18 ->
9 │ (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs
10 │ | [] ⇒ refl
11 │ | x :> _ => pmap (x :>) (++-assoc' _ _ _)
│ ╰──╯
Error: The solution
Vec (+-assoc {?n A x n m o _ ys zs} {?m A x n m o _ ys zs} {?o A x n m o _
ys zs} i) (?A A x n m o _ ys zs)
is not well-scoped
Only the variables below are allowed: `A`, `x`, `n`, `m`, `o`, `_`, `ys`,
`zs`
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:11:25 ->
9 │ (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs
10 │ | [] ⇒ refl
11 │ | x :> _ => pmap (x :>) (++-assoc' _ _ _)
│ ╰─────────────╯
Error: Cannot check the expression
++-assoc' _ _ _
of type
(++) {?n A x n m o _ ys zs} {?A A x n m o _ ys zs} {?m A x n m o _ ys zs +
?o A x n m o _ ys zs} (?_ A x n m o _ ys zs) ((++) {?m A x n m o _ ys zs} {?A
A x n m o _ ys zs} {?o A x n m o _ ys zs} (?_ A x n m o _ ys zs) (?_ A x
n m o _ ys zs)) = (++) {?n A x n m o _ ys zs + ?m A x n m o _ ys zs} {?A
A x n m o _ ys zs} {?o A x n m o _ ys zs} ((++) {?n A x n m o _ ys zs} {?A
A x n m o _ ys zs} {?m A x n m o _ ys zs} (?_ A x n m o _ ys zs) (?_ A x
n m o _ ys zs)) (?_ A x n m o _ ys zs)
against the type
?a A x n m o _ ys zs = ?b A x n m o _ ys zs
In particular, we failed to unify
?A A x n m o _ ys zs
with
Vec (+-assoc {?n A x n m o _ ys zs} {?m A x n m o _ ys zs} {?o A x n m o _
ys zs} i) (?A A x n m o _ ys zs)
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:11:18 ->
9 │ (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs
10 │ | [] ⇒ refl
11 │ | x :> _ => pmap (x :>) (++-assoc' _ _ _)
│ ╰──╯
Error: The solution
Vec (+-assoc {suc n} {m} {o} i) A
is not well-scoped
Only the variables below are allowed: `A`, `x`, `n`, `m`, `o`, `_`, `ys`,
`zs`
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:11:12 ->
9 │ (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs
10 │ | [] ⇒ refl
11 │ | x :> _ => pmap (x :>) (++-assoc' _ _ _)
│ ╰───────────────────────────╯
Error: Cannot check the expression
pmap (\ _ ⇒ x :> _) (++-assoc' _ _ _)
of type
(=) {?B A x n m o _ ys zs} (x :> ?a A x n m o _ ys zs) (x :> ?b A x n m
o _ ys zs)
(Normalized: (x :> ?a A x n m o _ ys zs) = (x :> ?b A x n m o _ ys zs))
against the type
(++) {suc n} {A} {m + o} (x :> _) ((++) {m} {A} {o} ys zs) = (++) {suc n +
m} {A} {o} ((++) {suc n} {A} {m} (x :> _) ys) zs
In particular, we failed to unify
?B A x n m o _ ys zs
with
Vec (+-assoc {suc n} {m} {o} i) A
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:11:18 ->
9 │ (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs
10 │ | [] ⇒ refl
11 │ | x :> _ => pmap (x :>) (++-assoc' _ _ _)
│ ╰──╯
Error: The solution
Vec (?n A x n m o _ ys zs _) (?A A x n m o _ ys zs _)
is not well-scoped
Only the variables below are allowed: `A`, `x`, `n`, `m`, `o`, `_`, `ys`,
`zs`
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:11:18 ->
9 │ (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs
10 │ | [] ⇒ refl
11 │ | x :> _ => pmap (x :>) (++-assoc' _ _ _)
│ ╰──╯
Error: The solution
Vec (suc (?n A x n m o _ ys zs _)) (?A A x n m o _ ys zs _)
is not well-scoped
Only the variables below are allowed: `A`, `x`, `n`, `m`, `o`, `_`, `ys`,
`zs`
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:11:18 ->
9 │ (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs
10 │ | [] ⇒ refl
11 │ | x :> _ => pmap (x :>) (++-assoc' _ _ _)
│ ╰──╯
│ ╰──╯ ?B A x n m o _ ys zs >= Vec (suc (?n A x n m
o _ ys zs _)) (?A A x n m o _ ys zs _)
│ ╰╯ ?A A x n m o _ ys zs <= Vec (?n A x n m o _ ys
zs _) (?A A x n m o _ ys zs _)
Error: Equations do not have solutions!
9 error(s), 0 warning(s).
Let's learn from that.
>
at app//org.junit.jupiter.api.AssertionFailureBuilder.build(AssertionFailureBuilder.java:151)
at app//org.junit.jupiter.api.AssertionFailureBuilder.buildAndThrow(AssertionFailureBuilder.java:132)
at app//org.junit.jupiter.api.AssertEquals.failNotEqual(AssertEquals.java:197)
at app//org.junit.jupiter.api.AssertEquals.assertEquals(AssertEquals.java:182)
at app//org.junit.jupiter.api.Assertions.assertEquals(Assertions.java:1156)
at app//org.aya.test.TestRunner.checkOutput(TestRunner.java:76)
at app//org.aya.test.TestRunner.expectFixture(TestRunner.java:88)
at app//kala.function.CheckedConsumer.accept(CheckedConsumer.java:36)
at app//kala.collection.immutable.ImmutableVectors$Vector1.forEach(ImmutableVectors.java:460)
at app//kala.collection.base.Traversable.forEachChecked(Traversable.java:976)
at app//org.aya.test.TestRunner.negative(TestRunner.java:48)
at java.base@21.0.5/jdk.internal.reflect.DirectMethodHandleAccessor.invoke(DirectMethodHandleAccessor.java:103)
at java.base@21.0.5/java.lang.reflect.Method.invoke(Method.java:580)
at app//org.junit.platform.commons.util.ReflectionUtils.invokeMethod(ReflectionUtils.java:767)
at app//org.junit.jupiter.engine.execution.MethodInvocation.proceed(MethodInvocation.java:60)
at app//org.junit.jupiter.engine.execution.InvocationInterceptorChain$ValidatingInvocation.proceed(InvocationInterceptorChain.java:131)
at app//org.junit.jupiter.engine.extension.TimeoutExtension.intercept(TimeoutExtension.java:156)
at app//org.junit.jupiter.engine.extension.TimeoutExtension.interceptTestableMethod(TimeoutExtension.java:147)
at app//org.junit.jupiter.engine.extension.TimeoutExtension.interceptTestMethod(TimeoutExtension.java:86)
at app//org.junit.jupiter.engine.execution.InterceptingExecutableInvoker$ReflectiveInterceptorCall.lambda$ofVoidMethod$0(InterceptingExecutableInvoker.java:103)
at app//org.junit.jupiter.engine.execution.InterceptingExecutableInvoker.lambda$invoke$0(InterceptingExecutableInvoker.java:93)
at app//org.junit.jupiter.engine.execution.InvocationInterceptorChain$InterceptedInvocation.proceed(InvocationInterceptorChain.java:106)
at app//org.junit.jupiter.engine.execution.InvocationInterceptorChain.proceed(InvocationInterceptorChain.java:64)
at app//org.junit.jupiter.engine.execution.InvocationInterceptorChain.chainAndInvoke(InvocationInterceptorChain.java:45)
at app//org.junit.jupiter.engine.execution.InvocationInterceptorChain.invoke(InvocationInterceptorChain.java:37)
at app//org.junit.jupiter.engine.execution.InterceptingExecutableInvoker.invoke(InterceptingExecutableInvoker.java:92)
at app//org.junit.jupiter.engine.execution.InterceptingExecutableInvoker.invoke(InterceptingExecutableInvoker.java:86)
at app//org.junit.jupiter.engine.descriptor.TestMethodTestDescriptor.lambda$invokeTestMethod$8(TestMethodTestDescriptor.java:217)
at app//org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
at app//org.junit.jupiter.engine.descriptor.TestMethodTestDescriptor.invokeTestMethod(TestMethodTestDescriptor.java:213)
at app//org.junit.jupiter.engine.descriptor.TestMethodTestDescriptor.execute(TestMethodTestDescriptor.java:138)
at app//org.junit.jupiter.engine.descriptor.TestMethodTestDescriptor.execute(TestMethodTestDescriptor.java:68)
at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$6(NodeTestTask.java:156)
at app//org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$8(NodeTestTask.java:146)
at app//org.junit.platform.engine.support.hierarchical.Node.around(Node.java:137)
at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$9(NodeTestTask.java:144)
at app//org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.executeRecursively(NodeTestTask.java:143)
at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.execute(NodeTestTask.java:100)
at java.base@21.0.5/java.util.ArrayList.forEach(ArrayList.java:1596)
at app//org.junit.platform.engine.support.hierarchical.SameThreadHierarchicalTestExecutorService.invokeAll(SameThreadHierarchicalTestExecutorService.java:41)
at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$6(NodeTestTask.java:160)
at app//org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$8(NodeTestTask.java:146)
at app//org.junit.platform.engine.support.hierarchical.Node.around(Node.java:137)
at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$9(NodeTestTask.java:144)
at app//org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.executeRecursively(NodeTestTask.java:143)
at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.execute(NodeTestTask.java:100)
at java.base@21.0.5/java.util.ArrayList.forEach(ArrayList.java:1596)
at app//org.junit.platform.engine.support.hierarchical.SameThreadHierarchicalTestExecutorService.invokeAll(SameThreadHierarchicalTestExecutorService.java:41)
at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$6(NodeTestTask.java:160)
at app//org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$8(NodeTestTask.java:146)
at app//org.junit.platform.engine.support.hierarchical.Node.around(Node.java:137)
at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$9(NodeTestTask.java:144)
at app//org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.executeRecursively(NodeTestTask.java:143)
at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.execute(NodeTestTask.java:100)
at app//org.junit.platform.engine.support.hierarchical.SameThreadHierarchicalTestExecutorService.submit(SameThreadHierarchicalTestExecutorService.java:35)
at app//org.junit.platform.engine.support.hierarchical.HierarchicalTestExecutor.execute(HierarchicalTestExecutor.java:57)
at app//org.junit.platform.engine.support.hierarchical.HierarchicalTestEngine.execute(HierarchicalTestEngine.java:54)
at app//org.junit.platform.launcher.core.EngineExecutionOrchestrator.execute(EngineExecutionOrchestrator.java:107)
at app//org.junit.platform.launcher.core.EngineExecutionOrchestrator.execute(EngineExecutionOrchestrator.java:88)
at app//org.junit.platform.launcher.core.EngineExecutionOrchestrator.lambda$execute$0(EngineExecutionOrchestrator.java:54)
at app//org.junit.platform.launcher.core.EngineExecutionOrchestrator.withInterceptedStreams(EngineExecutionOrchestrator.java:67)
at app//org.junit.platform.launcher.core.EngineExecutionOrchestrator.execute(EngineExecutionOrchestrator.java:52)
at app//org.junit.platform.launcher.core.DefaultLauncher.execute(DefaultLauncher.java:114)
at app//org.junit.platform.launcher.core.DefaultLauncher.execute(DefaultLauncher.java:86)
at app//org.junit.platform.launcher.core.DefaultLauncherSession$DelegatingLauncher.execute(DefaultLauncherSession.java:86)
at org.gradle.api.internal.tasks.testing.junitplatform.JUnitPlatformTestClassProcessor$CollectAllTestClassesExecutor.processAllTestClasses(JUnitPlatformTestClassProcessor.java:124)
at org.gradle.api.internal.tasks.testing.junitplatform.JUnitPlatformTestClassProcessor$CollectAllTestClassesExecutor.access$000(JUnitPlatformTestClassProcessor.java:99)
at org.gradle.api.internal.tasks.testing.junitplatform.JUnitPlatformTestClassProcessor.stop(JUnitPlatformTestClassProcessor.java:94)
at org.gradle.api.internal.tasks.testing.SuiteTestClassProcessor.stop(SuiteTestClassProcessor.java:63)
at java.base@21.0.5/jdk.internal.reflect.DirectMethodHandleAccessor.invoke(DirectMethodHandleAccessor.java:103)
at java.base@21.0.5/java.lang.reflect.Method.invoke(Method.java:580)
at org.gradle.internal.dispatch.ReflectionDispatch.dispatch(ReflectionDispatch.java:36)
at org.gradle.internal.dispatch.ReflectionDispatch.dispatch(ReflectionDispatch.java:24)
at org.gradle.internal.dispatch.ContextClassLoaderDispatch.dispatch(ContextClassLoaderDispatch.java:33)
at org.gradle.internal.dispatch.ProxyDispatchAdapter$DispatchingInvocationHandler.invoke(ProxyDispatchAdapter.java:92)
at jdk.proxy2/jdk.proxy2.$Proxy6.stop(Unknown Source)
at org.gradle.api.internal.tasks.testing.worker.TestWorker$3.run(TestWorker.java:200)
at org.gradle.api.internal.tasks.testing.worker.TestWorker.executeAndMaintainThreadName(TestWorker.java:132)
at org.gradle.api.internal.tasks.testing.worker.TestWorker.execute(TestWorker.java:103)
at org.gradle.api.internal.tasks.testing.worker.TestWorker.execute(TestWorker.java:63)
at org.gradle.process.internal.worker.child.ActionExecutionWorker.execute(ActionExecutionWorker.java:56)
at org.gradle.process.internal.worker.child.SystemApplicationClassLoaderWorker.call(SystemApplicationClassLoaderWorker.java:121)
at org.gradle.process.internal.worker.child.SystemApplicationClassLoaderWorker.call(SystemApplicationClassLoaderWorker.java:71)
at app//worker.org.gradle.process.internal.worker.GradleWorkerMain.run(GradleWorkerMain.java:69)
at app//worker.org.gradle.process.internal.worker.GradleWorkerMain.main(GradleWorkerMain.java:74)
Loading