TYCK: subst concall properly

Author: ice1000

base/src/main/java/org/aya/core/def/DataDef.java

@@ -57,5 +57,13 @@ public record CtorTelescopes(
         sortTele,
         conTele.map(Term.Param::toArg));
     }
+
+    public @NotNull CtorTelescopes rename() {
+      return new CtorTelescopes(dataTele.map(Term.Param::rename), sortTele, conTele.map(Term.Param::rename));
+    }
+
+    public @NotNull ImmutableSeq<Term.Param> params() {
+      return dataTele.concat(conTele);
+    }
   }
 }

base/src/main/java/org/aya/tyck/ExprTycker.java

@@ -499,11 +499,11 @@ private static boolean needImplicitParamIns(@NotNull Expr expr, @NotNull FormTer
     } else if (var.core instanceof CtorDef || var.concrete instanceof Decl.DataDecl.DataCtor) {
       var conVar = (DefVar<CtorDef, Decl.DataDecl.DataCtor>) var;
       var level = levelStuffs(pos, conVar);
-      var telescopes = CtorDef.telescopes(conVar, level._2);
       var tele = Term.Param.subst(Def.defTele(conVar), level._1);
       var type = FormTerm.Pi.make(tele, Def.defResult(conVar).subst(Substituter.TermSubst.EMPTY, level._1));
+      var telescopes = CtorDef.telescopes(conVar, level._2).rename();
       var body = telescopes.toConCall(conVar).subst(Substituter.TermSubst.EMPTY, level._1);
-      return new Result(IntroTerm.Lambda.make(tele, body), type);
+      return new Result(IntroTerm.Lambda.make(telescopes.params(), body), type);
     } else if (var.core instanceof FieldDef || var.concrete instanceof Decl.StructField) {
       // the code runs to here because we are tycking a StructField in a StructDecl
       // there should be two-stage check for this case:

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

@@ -16,8 +16,7 @@
 import org.aya.core.def.DataDef;
 import org.aya.core.def.Def;
 import org.aya.core.def.FnDef;
-import org.aya.core.pat.Pat;
-import org.aya.core.term.RefTerm;
+import org.aya.core.term.CallTerm;
 import org.aya.test.ThrowingReporter;
 import org.intellij.lang.annotations.Language;
 import org.jetbrains.annotations.NonNls;
@@ -48,17 +47,16 @@ private FnDef successTyckFn(@NotNull @NonNls @Language("TEXT") String code) {
       def xyr (zero : Nat) : Nat
         | zero => zero
         | suc n => zero""");
+    // ^ the latter `zero` refers to the `zero` parameter, and will be substituted as `suc n`
     var nat = (DataDef) defs.get(0);
     var xyr = (FnDef) defs.get(1);
-      var ctors = nat.body;
+    var ctors = nat.body;
     assertEquals(2, ctors.size());
     var clauses = xyr.body.getRightValue();
-    var zeroToZero = clauses.get(0);
-    var zeroCtor = ctors.get(0);
-    assertEquals(0, zeroCtor.selfTele.size());
-    var zeroParam = xyr.telescope().get(0);
-    assertEquals(((RefTerm) zeroToZero.body()).var(), zeroParam.ref());
-    assertEquals(zeroCtor.ref(), ((Pat.Ctor) zeroToZero.patterns().get(0)).ref());
+    var sucToZero = clauses.get(1);
+    var sucCtor = ctors.get(1);
+    assertEquals(1, sucCtor.selfTele.size());
+    assertEquals(((CallTerm.Con) sucToZero.body()).ref(), sucCtor.ref);
   }
 
   public static @NotNull ImmutableSeq<Stmt> successDesugarDecls(@Language("TEXT") @NonNls @NotNull String text) {