tele: no more fromSig

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

@@ -219,14 +219,18 @@ private void checkKitsune(@NotNull DataCon con, @NotNull ExprTycker tycker) {
 
     var teleTycker = new TeleTycker.Con(tycker, (SortTerm) dataSig.result());
     var selfTele = teleTycker.checkTele(con.telescope);
+    var selfTelePos = con.telescope.map(Expr.Param::sourcePos);
     var selfBinds = con.teleVars();
 
     var conTy = con.result;
     EqTerm boundaries = null;
     if (conTy != null) {
       var pusheenResult = PiTerm.unpi(tycker.ty(conTy), tycker::whnf);
+
       selfTele = selfTele.appendedAll(pusheenResult.params().zip(pusheenResult.names(),
-        (param, name) -> new WithPos<>(conTy.sourcePos(), new Param(name.name(), param, true))));
+        (param, name) -> new Param(name.name(), param, true)));
+      selfTelePos = selfTelePos.appendedAll(ImmutableSeq.fill(pusheenResult.params().size(), conTy.sourcePos()));
+
       selfBinds = selfBinds.appendedAll(pusheenResult.names());
       var tyResult = tycker.whnf(pusheenResult.body());
       if (tyResult instanceof EqTerm eq) {
@@ -235,8 +239,9 @@ private void checkKitsune(@NotNull DataCon con, @NotNull ExprTycker tycker) {
         tycker.unifyTermReported(eq.appA(fresh), freeDataCall, null, conTy.sourcePos(),
           cmp -> new UnifyError.ConReturn(con, cmp, new UnifyInfo(state)));
 
-        selfTele = selfTele.appended(new WithPos<>(conTy.sourcePos(),
-          new Param("i", DimTyTerm.INSTANCE, true)));
+        selfTele = selfTele.appended(new Param("i", DimTyTerm.INSTANCE, true));
+        selfTelePos = selfTelePos.appended(conTy.sourcePos());
+
         selfBinds = selfBinds.appended(fresh.name());
         boundaries = eq;
       } else {
@@ -252,7 +257,7 @@ private void checkKitsune(@NotNull DataCon con, @NotNull ExprTycker tycker) {
     var boundDataCall = (DataCall) tycker.zonk(freeDataCall).bindTele(selfBinds);
     if (boundaries != null) boundaries = (EqTerm) tycker.zonk(boundaries).bindTele(selfBinds);
     var boundariesWithDummy = boundaries != null ? boundaries : ErrorTerm.DUMMY;
-    var wholeSig = new AbstractTele.Locns(tycker.zonk(selfTele.map(WithPos::data)), new TupTerm(
+    var wholeSig = new AbstractTele.Locns(tycker.zonk(selfTele), new TupTerm(
       // This is a silly hack that allows two terms to appear in the result of a Signature
       // I considered using `AppTerm` but that is more disgraceful
       ImmutableSeq.of(boundDataCall, boundariesWithDummy)))
@@ -263,7 +268,7 @@ private void checkKitsune(@NotNull DataCon con, @NotNull ExprTycker tycker) {
 
     // The signature of con should be full (the same as [konCore.telescope()])
     ref.signature = new Signature(new AbstractTele.Locns(wholeSig.telescope(), boundDataCall),
-      ownerTelePos.appendedAll(selfTele.map(WithPos::sourcePos)));
+      ownerTelePos.appendedAll(selfTelePos));
     new ConDef(dataDef, ref, wellPats, boundaries,
       ownerTele,
       wholeSig.telescope().drop(ownerTele.size()),

base/src/main/java/org/aya/tyck/tycker/TeleTycker.java

@@ -13,6 +13,7 @@
 import org.aya.syntax.core.term.Term;
 import org.aya.syntax.ref.LocalCtx;
 import org.aya.syntax.ref.LocalVar;
+import org.aya.syntax.telescope.AbstractTele;
 import org.aya.syntax.telescope.Signature;
 import org.aya.tyck.ExprTycker;
 import org.aya.tyck.Jdg;
@@ -43,18 +44,17 @@ public sealed interface TeleTycker extends Contextful {
     var locals = cTele.view().map(Expr.Param::ref).toImmutableSeq();
     var checkedParam = checkTele(cTele);
     var checkedResult = checkType(result, true).bindTele(locals.view());
-    return Signature.fromSig(checkedParam, checkedResult);
+    return new Signature(new AbstractTele.Locns(checkedParam, checkedResult), cTele.map(Expr.Param::sourcePos));
   }
 
   /**
    * Does not zonk the result. Need <emph>you</emph> to zonk them.
    */
-  default @NotNull ImmutableSeq<WithPos<Param>> checkTele(@NotNull ImmutableSeq<Expr.Param> cTele) {
+  default @NotNull ImmutableSeq<Param> checkTele(@NotNull ImmutableSeq<Expr.Param> cTele) {
     var tele = checkTeleFree(cTele);
     var locals = cTele.view().map(Expr.Param::ref).toImmutableSeq();
     bindTele(locals, tele);
-    return tele.zip(cTele, (param, sp) -> new WithPos<>(sp.sourcePos(), param))
-      .toImmutableSeq();
+    return tele.toImmutableSeq();
   }
 
   /**

syntax/src/main/java/org/aya/syntax/telescope/Signature.java

@@ -7,18 +7,13 @@
 import org.aya.syntax.core.term.PiTerm;
 import org.aya.syntax.core.term.Term;
 import org.aya.util.error.SourcePos;
-import org.aya.util.error.WithPos;
 import org.jetbrains.annotations.NotNull;
 
 import java.util.function.UnaryOperator;
 
 public record Signature(@NotNull AbstractTele.Locns telescope, @NotNull ImmutableSeq<SourcePos> pos) {
   public Signature { assert telescope.telescopeSize() == pos.size(); }
 
-  public static @NotNull Signature fromSig(@NotNull ImmutableSeq<WithPos<Param>> param, @NotNull Term result) {
-    return new Signature(new AbstractTele.Locns(param.map(WithPos::data), result), param.map(WithPos::sourcePos));
-  }
-
   public @NotNull ImmutableSeq<Param> params() { return telescope.telescope(); }
   public @NotNull Term result() { return telescope.result(); }