An attempt to redo #1226

base/src/main/java/org/aya/resolve/ResolvingStmt.java

@@ -1,9 +1,10 @@
-// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2025 Tesla (Yinsen) Zhang.
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.resolve;
 
 import kala.collection.immutable.ImmutableSeq;
 import org.aya.resolve.context.Context;
+import org.aya.resolve.context.ModuleContext;
 import org.aya.syntax.concrete.stmt.Generalize;
 import org.aya.syntax.concrete.stmt.Stmt;
 import org.aya.syntax.concrete.stmt.decl.Decl;
@@ -38,6 +39,6 @@ sealed interface ResolvingDecl extends ResolvingStmt { }
 
   record TopDecl(@NotNull Decl stmt, @NotNull Context context) implements ResolvingDecl { }
   record MiscDecl(@NotNull Decl stmt) implements ResolvingDecl { }
-  record GenStmt(@NotNull Generalize stmt) implements ResolvingStmt { }
+  record GenStmt(@NotNull Generalize stmt, @NotNull ModuleContext context) implements ResolvingStmt { }
   record ModStmt(@NotNull ImmutableSeq<@NotNull ResolvingStmt> resolved) implements ResolvingStmt { }
 }

base/src/main/java/org/aya/resolve/error/CyclicDependencyError.java

@@ -0,0 +1,27 @@
+// Copyright (c) 2020-2025 Tesla (Yinsen) Zhang.
+// Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
+package org.aya.resolve.error;
+
+import org.aya.prettier.BasePrettier;
+import org.aya.pretty.doc.Doc;
+import org.aya.util.prettier.PrettierOptions;
+import org.aya.util.reporter.Problem;
+import org.aya.syntax.ref.GeneralizedVar;
+import org.aya.util.error.SourcePos;
+import org.jetbrains.annotations.NotNull;
+import kala.collection.immutable.ImmutableSeq;
+
+public record CyclicDependencyError(
+  @NotNull SourcePos sourcePos,
+  @NotNull GeneralizedVar var,
+  @NotNull ImmutableSeq<GeneralizedVar> cyclePath
+) implements Problem {
+  @Override public @NotNull Severity level() { return Severity.ERROR; }
+  @Override public @NotNull Stage stage() { return Stage.RESOLVE; }
+  @Override public @NotNull Doc describe(@NotNull PrettierOptions options) {
+    return Doc.vcat(
+      Doc.english("Cyclic dependency detected in variable declarations:"),
+      Doc.join(Doc.spaced(Doc.symbol("->")), cyclePath.map(BasePrettier::varDoc))
+    );
+  }
+}

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

@@ -136,12 +136,10 @@ public ExprResolver(@NotNull Context ctx, boolean allowGeneralizing) {
           case GeneralizedVar generalized -> {
             // a "resolved" GeneralizedVar is not in [allowedGeneralizes]
             if (allowGeneralizing) {
-              // Ordered set semantics. Do not expect too many generalized vars.
-              var owner = generalized.owner;
-              assert owner != null : "Sanity check";
-              var param = owner.toExpr(false, generalized.toLocal());
+              var param = generalized.toParam(false);
+              // Now introduce the variable itself
               allowedGeneralizes.put(generalized, param);
-              addReference(owner);
+              addReference(generalized.owner);
               yield param.ref();
             } else {
               yield ctx.reportAndThrow(new GeneralizedNotAvailableError(pos, generalized));
@@ -216,9 +214,7 @@ private void addReference(@NotNull TyckUnit unit) {
     }
   }
 
-  private void addReference(@NotNull DefVar<?, ?> defVar) {
-    addReference(defVar.concrete);
-  }
+  private void addReference(@NotNull DefVar<?, ?> defVar) { addReference(defVar.concrete); }
 
   public @NotNull Pattern.Clause clause(@NotNull ImmutableSeq<LocalVar> telescope, @NotNull Pattern.Clause clause) {
     var mCtx = MutableValue.create(ctx);

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

@@ -0,0 +1,47 @@
+// Copyright (c) 2020-2025 Tesla (Yinsen) Zhang.
+// Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
+package org.aya.resolve.visitor;
+
+import kala.collection.mutable.MutableList;
+import org.aya.resolve.context.Context;
+import org.aya.resolve.error.CyclicDependencyError;
+import org.aya.syntax.concrete.Expr;
+import org.aya.syntax.ref.GeneralizedVar;
+import org.jetbrains.annotations.NotNull;
+
+/// Collects dependency information for generalized variables using DFS on their types.
+///
+/// 1. A variable's type may reference other generalized variables; we record those as dependencies.
+/// 2. If we revisit a variable already on the DFS stack [#currentPath], that indicates
+///    a cyclic dependency, and we report an error.
+/// 3. Once a variable is fully processed, it goes into the [#introduceDependency] method; future registrations
+///    of the same variable skip repeated traversal using [#contains].
+public abstract class OverGeneralizer {
+  private final @NotNull Context reporter;
+  public final @NotNull MutableList<GeneralizedVar> currentPath = MutableList.create();
+
+  public OverGeneralizer(@NotNull Context reporter) { this.reporter = reporter; }
+  protected abstract boolean contains(@NotNull GeneralizedVar var);
+  protected abstract void introduceDependency(@NotNull GeneralizedVar var, @NotNull Expr.Param param);
+
+  public final void introduceDependencies(@NotNull GeneralizedVar var, @NotNull Expr.Param param) {
+    if (contains(var)) return;
+
+    // If var is already being visited in current DFS path, we found a cycle
+    if (currentPath.contains(var)) {
+      // Find cycle start index
+      var cycleStart = currentPath.indexOf(var);
+      if (cycleStart < 0) cycleStart = 0;
+      var cyclePath = currentPath.view().drop(cycleStart).appended(var);
+      reporter.reportAndThrow(new CyclicDependencyError(var.sourcePos(), var, cyclePath.toImmutableSeq()));
+    }
+
+    currentPath.append(var);
+    // Introduce dependencies first
+    var.owner.dependencies.forEach(this::introduceDependencies);
+
+    // Now introduce the variable itself
+    introduceDependency(var, param);
+    currentPath.removeLast();
+  }
+}

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

@@ -99,7 +99,7 @@ public ImmutableSeq<ResolvingStmt> resolveStmt(@NotNull ImmutableSeq<Stmt> stmts
       case Generalize variables -> {
         for (var variable : variables.variables)
           context.defineSymbol(variable, Stmt.Accessibility.Private, variable.sourcePos);
-        yield new ResolvingStmt.GenStmt(variables);
+        yield new ResolvingStmt.GenStmt(variables, context);
       }
     };
   }

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

@@ -1,9 +1,13 @@
-// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2025 Tesla (Yinsen) Zhang.
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.resolve.visitor;
 
 import kala.collection.SeqView;
+import kala.collection.immutable.ImmutableMap;
 import kala.collection.immutable.ImmutableSeq;
+import kala.collection.mutable.MutableLinkedHashMap;
+import kala.collection.mutable.MutableMap;
+import kala.control.Option;
 import kala.value.MutableValue;
 import org.aya.generic.stmt.TyckOrder;
 import org.aya.generic.stmt.TyckUnit;
@@ -12,45 +16,96 @@
 import org.aya.resolve.context.Context;
 import org.aya.resolve.error.NameProblem;
 import org.aya.resolve.visitor.ExprResolver.Where;
+import org.aya.syntax.concrete.Expr;
+import org.aya.syntax.concrete.stmt.Generalize;
 import org.aya.syntax.concrete.stmt.QualifiedID;
+import org.aya.syntax.concrete.stmt.Stmt;
 import org.aya.syntax.concrete.stmt.decl.*;
+import org.aya.syntax.ref.GeneralizedVar;
 import org.aya.syntax.ref.LocalVar;
 import org.aya.tyck.error.TyckOrderError;
 import org.aya.util.error.Panic;
+import org.aya.util.error.PosedUnaryOperator;
 import org.jetbrains.annotations.NotNull;
 
-/**
- * Resolves expressions inside stmts, after {@link StmtPreResolver}
- *
- * @author re-xyr, ice1000, kiva
- * @see StmtPreResolver
- * @see ExprResolver
- */
+/// Resolves expressions inside stmts, after [StmtPreResolver]
+///
+/// @author re-xyr, ice1000, kiva
+/// @see StmtPreResolver
+/// @see ExprResolver
 public interface StmtResolver {
   static void resolveStmt(@NotNull ImmutableSeq<ResolvingStmt> stmt, @NotNull ResolveInfo info) {
-    stmt.forEach(s -> resolveStmt(s, info));
+    var todos = stmt.flatMap(s -> resolveStmt(s, info));
+    class OvergrownGeneralizer extends OverGeneralizer {
+      final MutableMap<GeneralizedVar, Expr.Param> dependencyGeneralizes = MutableLinkedHashMap.of();
+      final ResolveStmt task;
+      // MutableList<Generalize> deps = MutableList.create();
+      public OvergrownGeneralizer(@NotNull ResolveStmt task) {
+        super(info.thisModule());
+        this.task = task;
+      }
+      @Override protected boolean contains(@NotNull GeneralizedVar var) {
+        return dependencyGeneralizes.containsKey(var) || task.generalizes.containsKey(var);
+      }
+      @Override protected void introduceDependency(@NotNull GeneralizedVar var, Expr.@NotNull Param param) {
+        var owner = var.owner;
+        assert owner != null : "GeneralizedVar owner should not be null";
+        dependencyGeneralizes.put(var, param);
+        // deps.append(owner);
+      }
+    }
+
+    todos.forEach(task -> {
+      if (task.stmt instanceof Generalize gen) {
+        var generalizer = new OvergrownGeneralizer(task);
+        generalizer.currentPath.appendAll(gen.variables);
+        // Check loops
+        task.generalizes.forEach((depGen, _) -> {
+          generalizer.currentPath.append(depGen);
+          depGen.owner.dependencies.forEach(generalizer::introduceDependencies);
+          generalizer.currentPath.removeLast();
+        });
+      }
+    });
+    todos.forEach(task -> {
+      if (task.stmt instanceof TeleDecl decl) {
+        var generalizer = new OvergrownGeneralizer(task);
+        task.generalizes.forEach((gen, _) -> gen.owner.dependencies.forEach(generalizer::introduceDependencies));
+        insertGeneralizedVars(decl, task.generalizes);
+        insertGeneralizedVars(decl, generalizer.dependencyGeneralizes);
+        // addReferences(info, new TyckOrder.Head(gen), generalizer.deps.view().map(TyckOrder.Head::new));
+      }
+    });
   }
 
-  /** @apiNote Note that this function MUTATES the stmt if it's a Decl. */
-  static void resolveStmt(@NotNull ResolvingStmt stmt, @NotNull ResolveInfo info) {
-    switch (stmt) {
+  /// @param generalizes the directly referred generalized variables
+  record ResolveStmt(Stmt stmt, MutableMap<GeneralizedVar, Expr.Param> generalizes) { }
+
+  /// @return the "TO-DO" for the rest of the resolving, see [ResolveStmt]
+  /// @apiNote Note that this function MUTATES the stmt if it's a Decl.
+  static Option<ResolveStmt> resolveStmt(@NotNull ResolvingStmt stmt, @NotNull ResolveInfo info) {
+    return switch (stmt) {
       case ResolvingStmt.ResolvingDecl decl -> resolveDecl(decl, info);
-      case ResolvingStmt.ModStmt(var stmts) -> resolveStmt(stmts, info);
-      case ResolvingStmt.GenStmt(var variables) -> {
-        var resolver = new ExprResolver(info.thisModule(), false);
+      case ResolvingStmt.ModStmt(var stmts) -> {
+        resolveStmt(stmts, info);
+        yield Option.none();
+      }
+      case ResolvingStmt.GenStmt(var variables, var context) -> {
+        var resolver = new ExprResolver(context, true);
         resolver.enter(Where.Head);
-        variables.descentInPlace(resolver, (_, p) -> p);
+        variables.descentInPlace(resolver, PosedUnaryOperator.identity());
+        variables.dependencies = ImmutableMap.from(resolver.allowedGeneralizes().view());
         addReferences(info, new TyckOrder.Head(variables), resolver);
+        yield Option.some(new ResolveStmt(variables, resolver.allowedGeneralizes()));
       }
-    }
+    };
   }
 
-  /**
-   * Resolve {@param predecl}, where {@code predecl.ctx()} is the context of the body of {@param predecl}
-   *
-   * @apiNote Note that this function MUTATES the decl
-   */
-  private static void resolveDecl(@NotNull ResolvingStmt.ResolvingDecl predecl, @NotNull ResolveInfo info) {
+  /// Resolve {@param predecl}, where `predecl.ctx()` is the context of the body of {@param predecl}
+  ///
+  /// @apiNote Note that this function MUTATES the decl
+  private static Option<ResolveStmt>
+  resolveDecl(@NotNull ResolvingStmt.ResolvingDecl predecl, @NotNull ResolveInfo info) {
     switch (predecl) {
       case ResolvingStmt.TopDecl(FnDecl decl, var ctx) -> {
         var where = decl.body instanceof FnBody.BlockBody ? Where.Head : Where.FnSimple;
@@ -59,8 +114,7 @@ private static void resolveDecl(@NotNull ResolvingStmt.ResolvingDecl predecl, @N
         switch (decl.body) {
           case FnBody.BlockBody body -> {
             assert body.elims() == null;
-            // introducing generalized variable is not allowed in clauses, hence we insert them before body resolving
-            insertGeneralizedVars(decl, resolver);
+            // insertGeneralizedVars(decl, resolver);
             resolveElim(resolver, body.inner());
             var clausesResolver = resolver.deriveRestrictive();
             clausesResolver.reference().append(new TyckOrder.Head(decl));
@@ -69,15 +123,17 @@ private static void resolveDecl(@NotNull ResolvingStmt.ResolvingDecl predecl, @N
           }
           case FnBody.ExprBody(var expr) -> {
             var body = expr.descent(resolver);
-            insertGeneralizedVars(decl, resolver);
+            // insertGeneralizedVars(decl, resolver);
             decl.body = new FnBody.ExprBody(body);
             addReferences(info, new TyckOrder.Head(decl), resolver);
           }
         }
+        if (resolver.allowedGeneralizes().isNotEmpty())
+          return Option.some(new ResolveStmt(decl, resolver.allowedGeneralizes()));
       }
       case ResolvingStmt.TopDecl(DataDecl data, var ctx) -> {
         var resolver = resolveDeclSignature(info, new ExprResolver(ctx, true), data, Where.Head);
-        insertGeneralizedVars(data, resolver);
+        // insertGeneralizedVars(data, resolver);
         resolveElim(resolver, data.body);
         data.body.forEach(con -> {
           var bodyResolver = resolver.deriveRestrictive();
@@ -95,6 +151,8 @@ private static void resolveDecl(@NotNull ResolvingStmt.ResolvingDecl predecl, @N
 
         addReferences(info, new TyckOrder.Body(data), resolver.reference().view()
           .concat(data.body.clauses.map(TyckOrder.Body::new)));
+        if (resolver.allowedGeneralizes().isNotEmpty())
+          return Option.some(new ResolveStmt(data, resolver.allowedGeneralizes()));
       }
       case ResolvingStmt.TopDecl(ClassDecl decl, var ctx) -> {
         var resolver = new ExprResolver(ctx, false);
@@ -121,6 +179,7 @@ private static void resolveDecl(@NotNull ResolvingStmt.ResolvingDecl predecl, @N
       // handled in DataDecl and ClassDecl
       case ResolvingStmt.MiscDecl _ -> Panic.unreachable();
     }
+    return Option.none();
   }
   private static void
   resolveMemberSignature(TeleDecl con, ExprResolver bodyResolver, MutableValue<@NotNull Context> mCtx) {
@@ -143,7 +202,7 @@ private static void addReferences(@NotNull ResolveInfo info, TyckOrder decl, Seq
       .filter(unit -> TyckUnit.needTyck(unit, info.modulePath())));
   }
 
-  /** @param decl is unmodified */
+  /// @param decl is unmodified
   private static void addReferences(@NotNull ResolveInfo info, TyckOrder decl, ExprResolver resolver) {
     addReferences(info, decl, resolver.reference().view());
   }
@@ -164,8 +223,8 @@ private static void addReferences(@NotNull ResolveInfo info, TyckOrder decl, Exp
     return newResolver;
   }
 
-  private static void insertGeneralizedVars(@NotNull TeleDecl decl, @NotNull ExprResolver resolver) {
-    decl.telescope = decl.telescope.prependedAll(resolver.allowedGeneralizes().valuesView());
+  private static void insertGeneralizedVars(@NotNull TeleDecl decl, MutableMap<GeneralizedVar, Expr.Param> generalizes) {
+    decl.telescope = decl.telescope.prependedAll(generalizes.valuesView());
   }
 
   private static <Cls> void resolveElim(@NotNull ExprResolver resolver, @NotNull MatchBody<Cls> body) {