Error handling, handle RuleReducer.Con in visibleArgs in CorePrettier

base/src/main/java/org/aya/resolve/module/FileModuleLoader.java

@@ -9,14 +9,14 @@
 import org.aya.syntax.GenericAyaFile;
 import org.aya.syntax.GenericAyaParser;
 import org.aya.syntax.ref.ModulePath;
-import org.aya.util.error.Panic;
 import org.aya.util.error.SourceFileLocator;
 import org.aya.util.reporter.Reporter;
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 
 import java.io.IOException;
 import java.nio.file.Files;
+import java.nio.file.InvalidPathException;
 import java.nio.file.Path;
 
 public record FileModuleLoader(
@@ -45,15 +45,11 @@ public FileModuleLoader(
   }
 
   @Override public boolean existsFileLevelModule(@NotNull ModulePath path) {
-    var sourcePath = AyaFiles.resolveAyaSourceFile(basePath, path.module());
-    return Files.exists(sourcePath);
-  }
-
-  public static void handleInternalError(@NotNull Panic e) {
-    e.printStackTrace();
-    e.printHint();
-    System.err.println("""
-      Please report the stacktrace to the developers so a better error handling could be made.
-      Don't forget to inform the version of Aya you're using and attach your code for reproduction.""");
+    try {
+      var sourcePath = AyaFiles.resolveAyaSourceFile(basePath, path.module());
+      return Files.exists(sourcePath);
+    } catch (InvalidPathException e) {
+      return false;
+    }
   }
 }

cli-impl/src/main/java/org/aya/cli/utils/CompilerUtil.java

@@ -8,7 +8,6 @@
 import org.aya.compiler.CompiledModule;
 import org.aya.generic.InterruptException;
 import org.aya.resolve.ResolveInfo;
-import org.aya.resolve.module.FileModuleLoader;
 import org.aya.syntax.core.def.TyckDef;
 import org.aya.util.error.Panic;
 import org.aya.util.reporter.CountingReporter;
@@ -28,7 +27,7 @@ public static int catching(
     try {
       block.runChecked();
     } catch (Panic e) {
-      FileModuleLoader.handleInternalError(e);
+      handleInternalError(e);
       reporter.reportString("Internal error");
       return e.exitCode();
     } catch (InterruptException e) {
@@ -59,4 +58,11 @@ public static void saveCompiledCore(
     Files.createDirectories(coreFile.toAbsolutePath().getParent());
     return new ObjectOutputStream(Files.newOutputStream(coreFile));
   }
+  public static void handleInternalError(@NotNull Panic e) {
+    e.printStackTrace();
+    e.printHint();
+    System.err.println("""
+      Please report the stacktrace to the developers so a better error handling could be made.
+      Don't forget to inform the version of Aya you're using and attach your code for reproduction.""");
+  }
 }

cli-impl/src/test/java/org/aya/test/cli/ReplCompilerTest.java

@@ -88,6 +88,10 @@ public class ReplCompilerTest {
     assertNotNull(findContext("Unit"));
   }
 
+  @Test public void issue1143() {
+    compile("module A { module B {} }");
+  }
+
   private @Nullable AnyVar findContext(@NotNull String name) {
     try {
       var ctx = compiler.getContext();

gradle/libs.versions.toml

@@ -2,7 +2,7 @@
 # The Version of this project, aka, The Aya Theorem Prover.
 # Remove "-SNAPSHOT" suffix and run gradle publish to release a new version.
 # After that, increase the version number and add "-SNAPSHOT" suffix back for next cycle.
-project = "0.34.0-SNAPSHOT"
+project = "0.35.0-SNAPSHOT"
 
 # https://openjdk.org/
 java = "21"

note/early-changelog.md

@@ -1,5 +1,31 @@
 # Early changelog
 
+## v0.34
+
+Semi-breaking changes:
+
+- Revise the behavior of ambiguous exports -- we report errors on ambiguous exports now.
+  Before, Aya will export all candidates, and error will occur only when you try to use one.
+  But there is no way to resolve such ambiguity, so we now report errors earlier
+- Kotlin stdlib is now in the binary dependencies of Aya due to transitive dependency
+- Upgrade many dependencies
+
+New features:
+
+- Add `:debug-show-shapes` in REPL to show currently recognized shapes in the REPL context
+- Preliminary support for classes, adding type checking for class declarations,
+  class specializations, JIT-compilation, etc., but not yet for class instance resolution
+- Add `:info` (alias: `:i`) command in REPL to show information about a name, similar to GHCi
+
+Improvements to existing features including bug fixes:
+
+- Correctly display emojis in Windows Terminal
+- Improve error messages for unsolved metas thanks to @utensil and @HoshinoTented
+- The jlink release will include compiled version of the std library
+- Coercive subtyping now works from path to functions
+- Better type checking for list literals with the presence of ambiguity
+- Correctly pretty print `RuleReducer.Con`
+
 ## v0.33
 
 We've started working on classes.

syntax/src/main/java/org/aya/prettier/BasePrettier.java

@@ -96,17 +96,7 @@ protected BasePrettier(@NotNull PrettierOptions options) {
     @NotNull Outer outer, boolean showImplicits
   ) {
     var preArgs = args.toImmutableSeq();
-
-    // Because the signature of DataCon is selfTele, so we only need to deal with core con
-    var licit = switch (var) {
-      case TyckAnyDef<?> inner -> inner.core() instanceof SubLevelDef sub
-        ? sub.selfTele.mapToBoolean(MutableBooleanList.factory(), Param::explicit)
-        : inner.ref.signature == null
-          ? BooleanSeq.fill(preArgs.size(), true)
-          : inner.ref.signature.params().mapToBooleanTo(MutableBooleanList.create(), Param::explicit);
-      case JitDef jit -> MutableBooleanList.from(jit.telescopeLicit);
-      default -> throw new UnsupportedOperationException("TODO");
-    };
+    var licit = computeLicitFromDef(var, preArgs.size());
 
     // licited args, note that this may not include all [var] args since [preArgs.size()] may less than [licit.size()]
     // this is safe since the core call is always fully applied, that is, no missing implicit arguments.
@@ -117,6 +107,17 @@ protected BasePrettier(@NotNull PrettierOptions options) {
 
     return visitCalls(var.assoc(), refVar(var), licitArgs.view().appendedAll(explicitArgs), outer, showImplicits);
   }
+  private static BooleanSeq computeLicitFromDef(@NotNull AnyDef var, int size) {
+    return switch (var) {
+      case TyckAnyDef<?> inner -> inner.core() instanceof SubLevelDef sub
+        // Because the signature of DataCon is selfTele, so we only need to deal with core con
+        ? sub.selfTele.mapToBoolean(MutableBooleanList.factory(), Param::explicit)
+        : inner.ref.signature == null
+          ? BooleanSeq.fill(size, true)
+          : inner.ref.signature.params().mapToBooleanTo(MutableBooleanList.create(), Param::explicit);
+      case JitDef jit -> MutableBooleanList.from(jit.telescopeLicit);
+    };
+  }
 
   /**
    * Pretty-print an application in a smart way.

syntax/src/main/java/org/aya/prettier/CorePrettier.java

@@ -233,9 +233,7 @@ private boolean checkUneta(@NotNull SeqView<Term> args, @NotNull LocalVar param)
   }
 
   private ImmutableSeq<Term> visibleArgsOf(Callable call) {
-    return call instanceof ConCall con
-      ? con.conArgs() : call instanceof MemberCall access
-      ? access.args() : call.args();
+    return call instanceof ConCallLike con ? con.conArgs() : call.args();
   }
 
   private @NotNull Doc visitAccessHead(@NotNull MemberCall term) {