pat: do insert pats before classifier

Co-authored-by: Hoshino Tented <[email protected]>
aya-prover · Jan 4, 2025 · c2bf007 · c2bf007
1 parent c4fba2c
commit c2bf007
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 3 deletions.
diff --git a/base/src/main/java/org/aya/tyck/ExprTycker.java b/base/src/main/java/org/aya/tyck/ExprTycker.java
@@ -188,7 +188,8 @@ && whnf(type) instanceof DataCall dataCall
       new ClauseTycker(this),
       telescope,
       new DepTypeTerm.Unpi(ImmutableSeq.empty(), type),
-      ImmutableSeq.fill(discriminant.size(), i -> new LocalVar("match" + i)),
+      ImmutableSeq.fill(discriminant.size(), i ->
+        new LocalVar("match" + i, discriminant.get(i).sourcePos(), GenerateKind.Basic.Tyck)),
       ImmutableSeq.empty(),
       clauses, true);
     var wellClauses = clauseTycker.check(exprPos)

diff --git a/base/src/main/java/org/aya/tyck/pat/ClauseTycker.java b/base/src/main/java/org/aya/tyck/pat/ClauseTycker.java
@@ -15,6 +15,7 @@
 import org.aya.syntax.core.pat.PatToTerm;
 import org.aya.syntax.core.pat.TypeEraser;
 import org.aya.syntax.core.term.*;
+import org.aya.syntax.ref.GenerateKind;
 import org.aya.syntax.ref.LocalCtx;
 import org.aya.syntax.ref.LocalVar;
 import org.aya.tyck.ExprTycker;
@@ -187,11 +188,18 @@ public record Worker(
       ctx = ctx.map(new TermInline());
       var patWithTypeBound = Pat.collectVariables(patResult.wellTyped().view());
 
+      var unpiBody = sigIter.unpiBody();
+      // fill missing patterns
+      var missingPats = unpiBody.params().mapIndexed((idx, x) ->
+        // It would be nice if we have a SourcePos here
+        new Pat.Bind(new LocalVar("unpi" + idx, SourcePos.NONE, GenerateKind.Basic.Tyck), x.type()));
+
       var allBinds = patWithTypeBound.component1().toImmutableSeq();
       var newClause = new Pat.Preclause<>(clause.sourcePos, patWithTypeBound.component2(),
         allBinds.size(), patIter.exprBody());
       return new LhsResult(ctx, sigIter.unpiBody(), allBinds,
-        patResult.wellTyped(), patResult.paramSubst(), patResult.asSubst(), newClause, patResult.hasError());
+        patResult.wellTyped().appendedAll(missingPats),
+        patResult.paramSubst(), patResult.asSubst(), newClause, patResult.hasError());
     }
   }
 
@@ -225,7 +233,7 @@ else if (result.hasError) {
         exprTycker.solveMetas();
         wellBody = zonker.zonk(wellBody);
 
-        // fill missing patterns and eta body
+        // eta body with inserted patterns
         wellBody = AppTerm.make(wellBody, result.unpiPats().map(PatToTerm::visit));
 
         // bind all pat bindings