Support dependent types in variable

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

@@ -0,0 +1,28 @@
+// Copyright (c) 2020-2024 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.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.plain("Cyclic dependency detected in variable declarations:"),
+      Doc.plain(String.join(" -> ", cyclePath.view()
+        .map(GeneralizedVar::name)
+        .toImmutableSeq()))
+    );
+  }
+}

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

@@ -47,7 +47,8 @@
   boolean allowGeneralizing,
   @NotNull MutableMap<GeneralizedVar, Expr.Param> allowedGeneralizes,
   @NotNull MutableList<TyckOrder> reference,
-  @NotNull MutableStack<Where> where
+  @NotNull MutableStack<Where> where,
+  @NotNull VariableDependencyCollector collector
 ) implements PosedUnaryOperator<Expr> {
   public record LiterateResolved(
     ImmutableSeq<Expr.Param> params,
@@ -71,23 +72,24 @@
   }
 
   public ExprResolver(@NotNull Context ctx, boolean allowGeneralizing) {
-    this(ctx, allowGeneralizing, MutableLinkedHashMap.of(), MutableList.create(), MutableStack.create());
+    this(ctx, allowGeneralizing, MutableLinkedHashMap.of(), MutableList.create(), MutableStack.create(),
+      new VariableDependencyCollector(ctx.reporter()));
   }
 
   public void resetRefs() { reference.clear(); }
   public void enter(Where loc) { where.push(loc); }
   public void exit() { where.pop(); }
 
   public @NotNull ExprResolver enter(Context ctx) {
-    return ctx == ctx() ? this : new ExprResolver(ctx, allowGeneralizing, allowedGeneralizes, reference, where);
+    return ctx == ctx() ? this : new ExprResolver(ctx, allowGeneralizing, allowedGeneralizes, reference, where, collector);
   }
 
   /**
    * The intended usage is to create an {@link ExprResolver}
    * that resolves the body/bodies of something.
    */
   public @NotNull ExprResolver deriveRestrictive() {
-    return new ExprResolver(ctx, false, allowedGeneralizes, reference, where);
+    return new ExprResolver(ctx, false, allowedGeneralizes, reference, where, collector);
   }
 
   public @NotNull Expr pre(@NotNull Expr expr) {
@@ -258,20 +260,41 @@
     });
   }
 
+  private void introduceDependencies(@NotNull GeneralizedVar var) {
+    if (allowedGeneralizes.containsKey(var)) return;
+
+    // Introduce dependencies first
+    var dependencies = collector.getDependencies(var);
+    for (var dep : dependencies) {
+      introduceDependencies(dep);
+    }
+
+    // Now introduce the variable itself
+    var owner = var.owner;
+    assert owner != null : "GeneralizedVar owner should not be null";
+    var param = owner.toExpr(false, var.toLocal());
+    allowedGeneralizes.put(var, param);
+    addReference(owner);
+  }
+
   public @NotNull AnyVar resolve(@NotNull QualifiedID name) {
     var result = ctx.get(name);
     if (result instanceof GeneralizedVar gvar) {
       var gened = allowedGeneralizes.getOrNull(gvar);
       if (gened != null) return gened.ref();
+      if (!allowGeneralizing) {
+        ctx.reporter().report(new GeneralizedNotAvailableError(name.sourcePos(), gvar));
+        throw new Context.ResolvingInterruptedException();
+      }
+      introduceDependencies(gvar);
     }
-
     return result;
   }
 
   public @NotNull ExprResolver member(@NotNull TyckUnit decl, Where initial) {
     var resolver = new ExprResolver(ctx, false, allowedGeneralizes,
       MutableList.of(new TyckOrder.Head(decl)),
-      MutableStack.create());
+      MutableStack.create(), collector);
     resolver.enter(initial);
     return resolver;
   }

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

@@ -4,6 +4,7 @@
 
 import kala.collection.SeqView;
 import kala.collection.immutable.ImmutableSeq;
+import kala.collection.mutable.MutableList;
 import kala.value.MutableValue;
 import org.aya.generic.stmt.TyckOrder;
 import org.aya.generic.stmt.TyckUnit;
@@ -37,10 +38,57 @@
       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);
+        // Create resolver with allowGeneralizing=true for variable declarations
+        var resolver = new ExprResolver(info.thisModule(), true);
         resolver.enter(Where.Head);
+
+        // First pass: register all variables to detect cycles
+        for (var variable : variables.variables) {
+          resolver.collector().registerVariable(variable);
+        }
+
+        // Second pass: handle dependencies and references
+        var ownerRefs = MutableList.<TyckOrder>create();
+        for (var variable : variables.variables) {
+          var owner = variable.owner;
+          assert owner != null : "GeneralizedVar owner should not be null";
+
+          // Add to allowedGeneralizes
+          var param = owner.toExpr(false, variable.toLocal());
+          resolver.allowedGeneralizes().put(variable, param);
+
+          // Collect owner reference if it's a TyckUnit
+          if (owner instanceof TyckUnit unit) {
+            var ref = new TyckOrder.Head(unit);
+            if (!ownerRefs.contains(ref)) ownerRefs.append(ref);
+          }
+
+          // Handle dependencies
+          var deps = resolver.collector().getDependencies(variable);
+          for (var dep : deps) {
+            if (!resolver.allowedGeneralizes().containsKey(dep)) {
+              var depOwner = dep.owner;
+              assert depOwner != null : "GeneralizedVar owner should not be null";
+              var depParam = depOwner.toExpr(false, dep.toLocal());
+              resolver.allowedGeneralizes().put(dep, depParam);
+            }
+
+            // Add dependency owner reference if it's a TyckUnit
+            if (dep.owner instanceof TyckUnit depUnit) {
+              var ref = new TyckOrder.Head(depUnit);
+              if (!ownerRefs.contains(ref)) ownerRefs.append(ref);
+            }
+          }
+        }
+
+        // Add collected references to resolver
+        ownerRefs.forEach(resolver.reference()::append);
+
+        // Process the statement itself
         variables.descentInPlace(resolver, (_, p) -> p);
-        addReferences(info, new TyckOrder.Head(variables), resolver);
+
+        // Do not add the GenStmt itself to TyckOrder as it's not a TyckUnit
+        // So we skip calling addReferences for the GenStmt
       }
     }
   }

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

@@ -0,0 +1,98 @@
+// Copyright (c) 2020-2024 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.immutable.ImmutableSeq;
+import kala.collection.mutable.MutableList;
+import kala.collection.mutable.MutableSet;
+import org.aya.util.error.PosedUnaryOperator;
+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.aya.util.error.SourcePos;
+import org.aya.util.reporter.Reporter;
+import org.jetbrains.annotations.NotNull;
+
+import java.util.HashMap;
+import java.util.Map;
+
+/**
+ * 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 ("visiting" set), that indicates
+ *    a cyclic dependency, and we report an error.
+ * 3. Once a variable is fully processed, it goes into the "visited" set; future registrations
+ *    of the same variable skip repeated traversal.
+ *
+ * Pitfalls & Notes:
+ *   - A single variable (e.g. “A”) should be registered once, to avoid duplication.
+ *   - Attempting to re-scan or re-introduce “A” in another variable’s context can cause
+ *     confusion or potential cycles. So we do all dependency scans here, at declaration time.
+ *   - Any reference to a variable out of scope is handled as an error in the resolver
+ *     if it’s not in the allowedGeneralizes map.
+ */
+public final class VariableDependencyCollector {
+  private final Reporter reporter;
+  private final MutableSet<GeneralizedVar> visiting = MutableSet.create();
+  private final MutableSet<GeneralizedVar> visited = MutableSet.create();
+  private final MutableList<GeneralizedVar> currentPath = MutableList.create();
+
+  public VariableDependencyCollector(Reporter reporter) {
+    this.reporter = reporter;
+  }
+
+  public void registerVariable(GeneralizedVar var) {
+    if (visited.contains(var)) return;
+
+    // If var is already being visited in current DFS path, we found a cycle
+    if (!visiting.add(var)) {
+      // Find cycle start index
+      var cycleStart = currentPath.indexOf(var);
+      var cyclePath = currentPath.view().drop(cycleStart).appended(var);
+      reporter.report(new CyclicDependencyError(var.sourcePos(), var, cyclePath.toImmutableSeq()));
+      throw new Context.ResolvingInterruptedException();
+    }
+
+    currentPath.append(var);
+    var deps = collectReferences(var);
+    var.setDependencies(deps);
+
+    // Recursively register dependencies
+    for (var dep : deps) {
+      registerVariable(dep);
+    }
+
+    currentPath.removeLast();
+    visiting.remove(var);
+    visited.add(var);
+  }
+
+  public ImmutableSeq<GeneralizedVar> getDependencies(GeneralizedVar var) {
+    return var.getDependencies();
+  }
+
+  private ImmutableSeq<GeneralizedVar> collectReferences(GeneralizedVar var) {
+    var type = var.owner.type;
+    var collector = new StaticGeneralizedVarCollector();
+    type.descent(collector);
+    return collector.getCollected();
+  }
+
+  private static class StaticGeneralizedVarCollector implements PosedUnaryOperator<Expr> {
+    private final MutableList<GeneralizedVar> collected = MutableList.create();
+
+    @Override
+    public @NotNull Expr apply(@NotNull SourcePos pos, @NotNull Expr expr) {
+      if (expr instanceof Expr.Ref ref && ref.var() instanceof GeneralizedVar gvar) {
+        collected.append(gvar);
+      }
+      return expr.descent(this);
+    }
+
+    public ImmutableSeq<GeneralizedVar> getCollected() {
+      return collected.toImmutableSeq();
+    }
+  }
+}

base/src/test/java/org/aya/tyck/TyckTest.java

@@ -168,6 +168,26 @@ class Kontainer
       """).defs.isNotEmpty());
   }
 
+  @Test
+  public void testVariableDefinition() {
+    var result = tyck("""
+      prim I prim Path
+      variable A : Type
+      variable a : A
+      open inductive K | kk
+      open inductive G (k : K) | gg
+      open inductive F (A : Type) (k : K) (n : G k) | ff
+      open inductive N (b : A) (c : A) | nn
+      variable k : K
+      variable n : G k
+      variable xs : F A k n
+      variable b c : A
+      variable d : N b c
+      def infix = (a b : A) => Path (\\i => A) a b
+    """).defs;
+    assertTrue(result.isNotEmpty());
+  }
+
   @SuppressWarnings("unchecked") private static <T extends AnyDef> T
   getDef(@NotNull ImmutableSeq<TyckDef> defs, @NotNull String name) {
     return (T) TyckAnyDef.make(defs.find(x -> x.ref().name().equals(name)).get());

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

@@ -103,4 +103,8 @@ def test (A : Type) (a : A) : A =>
           | x : A := a
       in x
     """;
+  @Language("Aya") String testCyclicDependency = """
+    variable A : B
+    variable B : A
+  """;
 }

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

@@ -318,3 +318,6 @@ That looks right!
 LocalShadowSuppress:
 That looks right!
 
+CyclicDependency:
+That looks right!
+

syntax/src/main/java/org/aya/syntax/ref/GeneralizedVar.java

@@ -6,17 +6,27 @@
 import org.aya.util.error.SourceNode;
 import org.aya.util.error.SourcePos;
 import org.jetbrains.annotations.NotNull;
+import kala.collection.immutable.ImmutableSeq;
 
 public final class GeneralizedVar implements AnyVar, SourceNode {
   public final @NotNull String name;
   public final @NotNull SourcePos sourcePos;
   public Generalize owner;
+  private @NotNull ImmutableSeq<GeneralizedVar> dependencies = ImmutableSeq.empty();
 
   public GeneralizedVar(@NotNull String name, @NotNull SourcePos sourcePos) {
     this.name = name;
     this.sourcePos = sourcePos;
   }
 
+  public void setDependencies(@NotNull ImmutableSeq<GeneralizedVar> deps) {
+    this.dependencies = deps;
+  }
+
+  public @NotNull ImmutableSeq<GeneralizedVar> getDependencies() {
+    return dependencies;
+  }
+
   public @NotNull LocalVar toLocal() {
     return new LocalVar(name, sourcePos, new GenerateKind.Generalized(this));
   }