merge: Fix 1135 (#1167)

as title

base/src/main/java/org/aya/resolve/visitor/StmtBinder.java

@@ -49,8 +49,9 @@ public void bind(@NotNull Context ctx, @NotNull BindBlock bindBlock, OpDecl self
     }
 
     // make compiler happy 😥
-    throw StmtResolver.resolvingInterrupt(info.opSet().reporter,
+    info.opSet().reporter.report(
       new NameProblem.OperatorNameNotFound(id.sourcePos(), id.join()));
+    throw new Context.ResolvingInterruptedException();
   }
 
   public void resolveBind(@NotNull SeqLike<ResolvingStmt> contents) {

base/src/main/java/org/aya/resolve/visitor/StmtResolver.java

@@ -15,10 +15,8 @@
 import org.aya.syntax.concrete.stmt.QualifiedID;
 import org.aya.syntax.concrete.stmt.decl.*;
 import org.aya.syntax.ref.LocalVar;
+import org.aya.tyck.error.TyckOrderError;
 import org.aya.util.error.Panic;
-import org.aya.util.reporter.Problem;
-import org.aya.util.reporter.Reporter;
-import org.jetbrains.annotations.Contract;
 import org.jetbrains.annotations.NotNull;
 
 /**
@@ -140,6 +138,12 @@ private static void resolveDecl(@NotNull ResolvingStmt.ResolvingDecl predecl, @N
   }
 
   private static void addReferences(@NotNull ResolveInfo info, TyckOrder decl, SeqView<TyckOrder> refs) {
+    // check self-reference
+    if (decl instanceof TyckOrder.Head head && refs.contains(head)) {
+      info.opSet().reporter.report(new TyckOrderError.SelfReference(head.unit()));
+      throw new Context.ResolvingInterruptedException();
+    }
+
     info.depGraph().sucMut(decl).appendAll(refs
       .filter(unit -> TyckUnit.needTyck(unit, info.thisModule().modulePath())));
   }
@@ -165,15 +169,7 @@ private static void addReferences(@NotNull ResolveInfo info, TyckOrder decl, Exp
     return newResolver;
   }
 
-  private static void insertGeneralizedVars(
-    @NotNull TeleDecl decl, @NotNull ExprResolver resolver
-  ) {
+  private static void insertGeneralizedVars(@NotNull TeleDecl decl, @NotNull ExprResolver resolver) {
     decl.telescope = decl.telescope.prependedAll(resolver.allowedGeneralizes().valuesView());
   }
-
-  @Contract("_, _ -> fail")
-  static Context.ResolvingInterruptedException resolvingInterrupt(Reporter reporter, Problem problem) {
-    reporter.report(problem);
-    throw new Context.ResolvingInterruptedException();
-  }
 }

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

@@ -73,7 +73,7 @@ private static void checkOutput(Path expectedOutFile, String hookOut) {
       var output = Strings.convertLineSeparators(hookOut);
       var expected = instantiateVars(Strings.convertLineSeparators(
         Files.readString(expectedOutFile, StandardCharsets.UTF_8)));
-      assertEquals(expected, output, TMP_FILE.getFileName().toString());
+      assertEquals(expected, output, expectedOutFile.getFileName().toString());
     } catch (IOException e) {
       fail("error reading file " + expectedOutFile.toAbsolutePath());
     }

cli-impl/src/test/java/org/aya/test/fixtures/OperatorError.java

@@ -40,7 +40,7 @@ def NonEmpty (A : Type) => ¬ ¬ A
     """;
 
   @Language("Aya") String testSelfBind = """
-    def infix + : Type => +
+    def infix + : Type 1 => Type
       looser +
     """;
 

cli-impl/src/test/java/org/aya/test/fixtures/ScopeError.java

@@ -43,7 +43,6 @@ open A hiding (bar)
     def foo => false
     open A
     """;
-  @Language("Aya") String testInfRec = "def undefined => undefined";
   @Language("Aya") String testIssue247 = """
     inductive Z : Type
     | zero

cli-impl/src/test/java/org/aya/test/fixtures/TerckError.java

@@ -35,4 +35,14 @@ def swapAdd (a b : Nat) : Nat elim a
     partial def f Nat : Nat
     | a => f a
     """;
+
+  @Language("Aya") String testSelfData = "inductive SelfData (A : SelfData)";
+
+  @Language("Aya") String testSelfCon = "inductive SelfData | SelfCon SelfCon";
+
+  @Language("Aya") String testSelfFn = """
+    open import arith::nat::base
+    def crazyAdd (a : Nat) : crazyAdd a
+    | x => x
+    """;
 }

cli-impl/src/test/resources/negative/OperatorError.txt

@@ -66,7 +66,7 @@ Let's learn from that.
 SelfBind:
 In file $FILE:2:9 ->
 
-  1 │   def infix + : Type => +
+  1 │   def infix + : Type 1 => Type
   2 │     looser +
     │            ╰╯
 

cli-impl/src/test/resources/negative/ScopeError.txt

@@ -133,17 +133,6 @@ Warning: The name `foo` introduces ambiguity and can only be accessed through a
 
 That looks right!
 
-InfRec:
-In file $FILE:1:4 ->
-
-  1 │   def undefined => undefined
-    │       ╰───────╯
-
-Error: The recursive definition `undefined` is not structurally recursive
-
-1 error(s), 0 warning(s).
-Let's learn from that.
-
 Issue247:
 In file $FILE:3:2 ->
 

cli-impl/src/test/resources/negative/TerckError.txt

@@ -38,3 +38,41 @@ That looks right!
 PartialDef:
 That looks right!
 
+SelfData:
+In file $FILE:1:10 ->
+
+  1 │   inductive SelfData (A : SelfData)
+    │             ╰──────╯
+
+Error: Self-reference found in the signature of SelfData
+
+Resolving interrupted due to:
+1 error(s), 0 warning(s).
+Let's learn from that.
+
+SelfCon:
+In file $FILE:1:21 ->
+
+  1 │   inductive SelfData | SelfCon SelfCon
+    │                        ╰─────╯
+
+Error: Self-reference found in the signature of SelfCon
+
+Resolving interrupted due to:
+1 error(s), 0 warning(s).
+Let's learn from that.
+
+SelfFn:
+In file $FILE:2:4 ->
+
+  1 │   open import arith::nat::base
+  2 │   def crazyAdd (a : Nat) : crazyAdd a
+    │       ╰──────╯
+  3 │   | x => x
+
+Error: Self-reference found in the signature of crazyAdd
+
+Resolving interrupted due to:
+1 error(s), 0 warning(s).
+Let's learn from that.
+

cli-impl/src/test/resources/shared/src/data/unit.aya

@@ -0,0 +1 @@
+public open import data::unit::base

cli-impl/src/test/resources/shared/src/data/unit/base.aya

@@ -0,0 +1,6 @@
+open import relation::binary::path
+
+open inductive Unit | tt
+
+def Unit-isContr (u : Unit) : u = tt
+| tt => refl