pat: insert pats before classifier, add comments

base/src/main/java/org/aya/tyck/pat/ClauseTycker.java

@@ -41,10 +41,7 @@ public final class ClauseTycker implements Problematic, Stateful {
   private final Finalizer.Zonk<ClauseTycker> zonker = new Finalizer.Zonk<>(this);
   public ClauseTycker(@NotNull ExprTycker exprTycker) { this.exprTycker = exprTycker; }
 
-  public record TyckResult(
-    @NotNull ImmutableSeq<Pat.Preclause<Term>> clauses,
-    boolean hasLhsError
-  ) {
+  public record TyckResult(@NotNull ImmutableSeq<Pat.Preclause<Term>> clauses, boolean hasLhsError) {
     public @NotNull ImmutableSeq<WithPos<Term.Matching>> wellTyped() {
       return clauses.flatMap(Pat.Preclause::lift);
     }
@@ -54,12 +51,16 @@ public record TyckResult(
    * @param unpiedResult the result according to the pattern tycking, the
    *                     {@link DepTypeTerm.Unpi#params} is always empty if the signature result is
    *                     {@link org.aya.tyck.pat.iter.Pusheenable.Const}
-   * @param paramSubst   substitution for parameter, in the same order as parameter.
-   *                     See {@link PatternTycker#paramSubst}
+   * @param paramSubst   substitution for parameter, in the same ordeer as parameter.
+   *                     See {@link PatternTycker#paramSubst}.
    * @param freePats     a free version of the patterns.
    *                     In most cases you want to use {@code clause.pats} instead
    * @param allBinds     all binders in the patterns
    * @param asSubst      substitution of the {@code as} patterns
+   * @implNote If there are fewer pats than parameters, there will be some pats inserted,
+   * but this will not affect {@code paramSubst}, and the inserted pat are "ignored" in tycking
+   * of the body, because we check the body against to {@link #unpiedResult}.
+   * Then we apply the inserted pats to the body to complete it.
    */
   public record LhsResult(
     @NotNull LocalCtx localCtx,
@@ -76,6 +77,10 @@ public record LhsResult(
         freePats.map(f), paramSubst, asSubst, clause, hasError);
     }
 
+    public @NotNull SeqView<Pat> unpiPats() {
+      return clause.pats().view().takeLast(unpiedResult.params().size());
+    }
+
     /// Returns the instantiated result type of this clause
     public @NotNull Term instResult() {
       // We need not to inline this term even we did before. The [paramSubst] is already inlined.
@@ -104,7 +109,6 @@ public record Worker(
       if (lhs.noneMatch(r -> r.hasError)) {
         var classes = PatClassifier.classify(
           lhs.view().map(LhsResult::clause),
-          // TODO: max(lhs.signature.telescope by size)
           telescope.view().concat(unpi.params()), parent.exprTycker, overallPos);
         if (clauses.isNotEmpty()) {
           var usages = PatClassifier.firstMatchDomination(clauses, parent, classes);
@@ -222,12 +226,7 @@ else if (result.hasError) {
         wellBody = zonker.zonk(wellBody);
 
         // fill missing patterns and eta body
-        var unpiPat = result.unpiedResult.params().mapIndexed((idx, x) ->
-          // It would be nice if we have a SourcePos for the LocalVar
-          new Pat.Bind(new LocalVar("unpi" + idx), x.type()));
-
-        var fullPats = result.clause.pats().view().concat(unpiPat);
-        wellBody = AppTerm.make(wellBody, unpiPat.view().map(PatToTerm::visit));
+        wellBody = AppTerm.make(wellBody, result.unpiPats().map(PatToTerm::visit));
 
         // bind all pat bindings
         var patBindTele = Pat.collectVariables(result.clause.pats().view()).component1();

base/src/main/java/org/aya/tyck/pat/PatternTycker.java

@@ -236,7 +236,6 @@ public enum Kind {
         // too many implicit
         try (var _ = instCurrentParam()) {
           assert pattern != null;
-          // FIXME: I am not sure if we should consume the parameter even we found a critical error.
           foundError(new PatternProblem.TooManyImplicitPattern(pattern, currentParam));
         }
 
@@ -282,10 +281,9 @@ public enum Kind {
 
       // find the next appropriate parameter
       var fnp = findNextParam(currentPat.term(), p ->
-          p.explicit() == currentPat.explicit()
-        // || telescope.isFromPusheen() == patterns.isFromPusheen()
-        // ^this check implies the first one
-      );
+        p.explicit() == currentPat.explicit());
+      // || telescope.isFromPusheen() == patterns.isFromPusheen()
+      // ^this check implies the first one
 
       ImmutableSeq<Pat> generated = null;
 
@@ -326,10 +324,8 @@ public enum Kind {
 
     // is there any explicit parameters?
     var generated = findNextParam(null, p ->
-        p.explicit()
-          || telescope.isFromPusheen()
-      // ^this check implies the first one
-    );
+      p.explicit() || telescope.isFromPusheen());
+    // ^this check implies the first one
 
     // what kind of parameter you found?
     if (generated.kind == FindNextParam.Kind.Success && !telescope.isFromPusheen()) {
@@ -420,8 +416,7 @@ private void addAsSubst(@NotNull LocalVar as, @NotNull Pat pattern, @NotNull Ter
   }
 
   private @NotNull TyckResult done(@NotNull MutableList<Pat> wellTyped) {
-    var paramSubst = this.paramSubst.toImmutableSeq();
-    return new TyckResult(wellTyped.toImmutableSeq(), paramSubst, asSubst, hasError);
+    return new TyckResult(wellTyped.toImmutableSeq(), paramSubst.toImmutableSeq(), asSubst, hasError);
   }
 
   private record Selection(

tools-kala/src/main/java/org/aya/util/tyck/pat/ClassifierUtil.java

@@ -30,7 +30,8 @@ public interface ClassifierUtil<Subst, Term, Param, Pat> {
       ImmutableSeq.empty(), Indexed.indices(clauses)));
     var first = telescope.getFirst();
     var cls = classify1(subst, subst(subst, first),
-      clauses.mapIndexed((ix, it) -> new Indexed<>(normalize(it.pat().getFirst()), ix)), fuel);
+      clauses.mapIndexed((ix, it) ->
+        new Indexed<>(normalize(it.pat().getFirst()), ix)), fuel);
     return cls.flatMap(subclauses ->
       classifyN(add(subst, subclauses.term()),
         // Drop heads of both