From 05226aaffea64d66e45fdfb07a7c356cdccba69c Mon Sep 17 00:00:00 2001
From: ice1000 <ice1000kotlin@foxmail.com>
Date: Sat, 25 Jan 2025 05:19:34 -0500
Subject: [PATCH 1/6] core: the ability to store extra info in `FnClauseBody`

---
 .../java/org/aya/normalize/Normalizer.java    | 15 +++++++------
 .../java/org/aya/primitive/ShapeMatcher.java  | 14 ++++++------
 .../main/java/org/aya/terck/CallResolver.java |  8 +++----
 .../java/org/aya/tyck/pat/IApplyConfl.java    |  6 ++---
 .../java/org/aya/prettier/CorePrettier.java   | 22 ++++++++++---------
 .../org/aya/syntax/core/def/FnClauseBody.java | 12 ++++++++++
 .../java/org/aya/syntax/core/def/FnDef.java   | 16 ++++++--------
 7 files changed, 53 insertions(+), 40 deletions(-)
 create mode 100644 syntax/src/main/java/org/aya/syntax/core/def/FnClauseBody.java

diff --git a/base/src/main/java/org/aya/normalize/Normalizer.java b/base/src/main/java/org/aya/normalize/Normalizer.java
index aa470a718e..2099b8fcb8 100644
--- a/base/src/main/java/org/aya/normalize/Normalizer.java
+++ b/base/src/main/java/org/aya/normalize/Normalizer.java
@@ -1,7 +1,12 @@
-// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2025 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.normalize;
 
+import java.util.function.BiFunction;
+import java.util.function.UnaryOperator;
+
+import static org.aya.generic.State.Stuck;
+
 import kala.collection.SeqView;
 import kala.collection.immutable.ImmutableSeq;
 import kala.collection.immutable.ImmutableSet;
@@ -10,6 +15,7 @@
 import org.aya.generic.Modifier;
 import org.aya.syntax.compile.JitFn;
 import org.aya.syntax.compile.JitMatchy;
+import org.aya.syntax.core.def.FnClauseBody;
 import org.aya.syntax.core.def.FnDef;
 import org.aya.syntax.core.def.Matchy;
 import org.aya.syntax.core.pat.PatMatcher;
@@ -29,11 +35,6 @@
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 
-import java.util.function.BiFunction;
-import java.util.function.UnaryOperator;
-
-import static org.aya.generic.State.Stuck;
-
 /**
  * Unlike in pre-v0.30 Aya, we use only one normalizer, only doing head reduction,
  * and we merge conservative normalizer and the whnf normalizer.
@@ -92,7 +93,7 @@ case FnCall(FnDef.Delegate delegate, int ulift, var args) -> {
               term = body.instTele(args.view());
               continue;
             }
-            case Either.Right(var clauses): {
+            case Either.Right(FnClauseBody(var clauses)): {
               var result = tryUnfoldClauses(clauses.view().map(WithPos::data),
                 args, core.is(Modifier.Overlap), ulift);
               // we may get stuck
diff --git a/base/src/main/java/org/aya/primitive/ShapeMatcher.java b/base/src/main/java/org/aya/primitive/ShapeMatcher.java
index 89d9cd2701..8370e5dde1 100644
--- a/base/src/main/java/org/aya/primitive/ShapeMatcher.java
+++ b/base/src/main/java/org/aya/primitive/ShapeMatcher.java
@@ -1,7 +1,12 @@
-// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2025 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.primitive;
 
+import java.util.Objects;
+import java.util.function.BiPredicate;
+import java.util.function.BooleanSupplier;
+import java.util.function.Function;
+
 import kala.collection.SeqLike;
 import kala.collection.immutable.ImmutableMap;
 import kala.collection.immutable.ImmutableSeq;
@@ -28,11 +33,6 @@
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 
-import java.util.Objects;
-import java.util.function.BiPredicate;
-import java.util.function.BooleanSupplier;
-import java.util.function.Function;
-
 /**
  * @author kiva
  */
@@ -123,7 +123,7 @@ private boolean matchFn(@NotNull FnShape shape, @NotNull FnDef def) {
     return switch (new Pair<>(shape.body(), def.body())) {
       case Pair(Either.Left(var termShape), Either.Left(var term)) ->
         matchInside(() -> captures.put(shape.name(), def.ref()), () -> matchTerm(termShape, term));
-      case Pair(Either.Right(var clauseShapes), Either.Right(var clauses)) -> {
+      case Pair(Either.Right(var clauseShapes), Either.Right(FnClauseBody(var clauses))) -> {
         var mode = def.is(Modifier.Overlap) ? MatchMode.Sub : MatchMode.Eq;
         yield matchInside(() -> captures.put(shape.name(), def.ref()), () ->
           matchMany(mode, clauseShapes, clauses.view().map(WithPos::data), this::matchClause));
diff --git a/base/src/main/java/org/aya/terck/CallResolver.java b/base/src/main/java/org/aya/terck/CallResolver.java
index 5a2a84cf0b..cb5ad6b86b 100644
--- a/base/src/main/java/org/aya/terck/CallResolver.java
+++ b/base/src/main/java/org/aya/terck/CallResolver.java
@@ -1,7 +1,9 @@
-// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2025 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.terck;
 
+import java.util.function.Consumer;
+
 import kala.collection.Set;
 import kala.collection.immutable.ImmutableSeq;
 import kala.collection.immutable.ImmutableSet;
@@ -28,8 +30,6 @@
 import org.aya.util.terck.Relation;
 import org.jetbrains.annotations.NotNull;
 
-import java.util.function.Consumer;
-
 /**
  * Resolve calls and build call graph of recursive functions,
  * after {@link org.aya.tyck.StmtTycker}.
@@ -139,7 +139,7 @@ private Relation compareConArgs(@NotNull ImmutableSeq<Term> conArgs, @NotNull Pa
   }
 
   public void check() {
-    var clauses = caller.body().getRightValue();
+    var clauses = caller.body().getRightValue().clauses();
     clauses.view().map(WithPos::data).forEach(this);
   }
 
diff --git a/base/src/main/java/org/aya/tyck/pat/IApplyConfl.java b/base/src/main/java/org/aya/tyck/pat/IApplyConfl.java
index 1b7f1f0719..2a245b3e91 100644
--- a/base/src/main/java/org/aya/tyck/pat/IApplyConfl.java
+++ b/base/src/main/java/org/aya/tyck/pat/IApplyConfl.java
@@ -2,6 +2,8 @@
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.tyck.pat;
 
+import java.util.function.UnaryOperator;
+
 import kala.collection.immutable.ImmutableSeq;
 import org.aya.generic.Modifier;
 import org.aya.syntax.core.def.FnDef;
@@ -18,8 +20,6 @@
 import org.aya.util.error.WithPos;
 import org.jetbrains.annotations.NotNull;
 
-import java.util.function.UnaryOperator;
-
 /// This is XTT-specific confluence check, very simple: we check for all combinations.
 /// So, if we do
 /// ```
@@ -42,7 +42,7 @@ public record IApplyConfl(
   boolean orderIndep, @NotNull SourcePos sourcePos, @NotNull ExprTycker tycker
 ) {
   public IApplyConfl(@NotNull FnDef def, @NotNull ExprTycker tycker, @NotNull SourcePos pos) {
-    this(def, def.body().getRightValue(), def.is(Modifier.Overlap), pos, tycker);
+    this(def, def.body().getRightValue().clauses(), def.is(Modifier.Overlap), pos, tycker);
   }
   public void check() {
     // A matcher that does not normalize the arguments.
diff --git a/syntax/src/main/java/org/aya/prettier/CorePrettier.java b/syntax/src/main/java/org/aya/prettier/CorePrettier.java
index a25f46a1eb..f8742f794b 100644
--- a/syntax/src/main/java/org/aya/prettier/CorePrettier.java
+++ b/syntax/src/main/java/org/aya/prettier/CorePrettier.java
@@ -2,11 +2,17 @@
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.prettier;
 
+import java.util.function.Function;
+import java.util.function.UnaryOperator;
+
+import static org.aya.prettier.Tokens.*;
+
 import com.intellij.openapi.util.text.StringUtil;
 import kala.collection.SeqLike;
 import kala.collection.SeqView;
 import kala.collection.immutable.ImmutableSeq;
 import kala.collection.mutable.MutableList;
+import kala.control.Either;
 import org.aya.generic.AyaDocile;
 import org.aya.generic.Renamer;
 import org.aya.generic.term.DTKind;
@@ -35,11 +41,6 @@
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 
-import java.util.function.Function;
-import java.util.function.UnaryOperator;
-
-import static org.aya.prettier.Tokens.*;
-
 /**
  * It's the pretty printer.
  * Credit after <a href="https://github.com/jonsterling/dreamtt/blob/main/frontend/Distiller.ml">Jon Sterling</a>
@@ -205,7 +206,7 @@ case MatchCall(Matchy clauses, var discriminant, var captures) -> {
 
         yield Doc.cblock(prefix, 2, clauseDoc);
       }
-      case MatchCall(JitMatchy _, var discriminant, var captures) -> {
+      case MatchCall(JitMatchy _, var discriminant, _) -> {
         var deltaDoc = discriminant.map(x -> term(Outer.Free, x));
         var prefix = Doc.sep(KW_MATCH, Doc.commaList(deltaDoc));
         yield Doc.sep(prefix, Doc.braced(Doc.spaced(Doc.styled(COMMENT, "compiled code"))));
@@ -282,10 +283,11 @@ private ImmutableSeq<Term> visibleArgsOf(Callable call) {
           term(Outer.Free, def.result().instTeleVar(tele.view().map(ParamLike::ref)))
         });
         var line1sep = Doc.sepNonEmpty(line1);
-        yield def.body().fold(
-          term -> Doc.sep(line1sep, FN_DEFINED_AS, term(Outer.Free, term.instTele(subst))),
-          clauses -> Doc.vcat(line1sep,
-            Doc.nest(2, visitClauses(clauses.view().map(WithPos::data), tele.view().map(ParamLike::explicit)))));
+        yield switch (def.body()) {
+          case Either.Left(var term) -> Doc.sep(line1sep, FN_DEFINED_AS, term(Outer.Free, term.instTele(subst)));
+          case Either.Right(FnClauseBody(var clauses)) -> Doc.vcat(line1sep,
+            Doc.nest(2, visitClauses(clauses.view().map(WithPos::data), tele.view().map(ParamLike::explicit))));
+        };
       }
       case MemberDef field -> Doc.sepNonEmpty(Doc.symbol("|"),
         defVar(field.ref()),
diff --git a/syntax/src/main/java/org/aya/syntax/core/def/FnClauseBody.java b/syntax/src/main/java/org/aya/syntax/core/def/FnClauseBody.java
new file mode 100644
index 0000000000..59051eecc8
--- /dev/null
+++ b/syntax/src/main/java/org/aya/syntax/core/def/FnClauseBody.java
@@ -0,0 +1,12 @@
+// Copyright (c) 2020-2025 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.syntax.core.def;
+
+import kala.collection.immutable.ImmutableSeq;
+import org.aya.syntax.core.term.Term;
+import org.aya.util.error.WithPos;
+
+public record FnClauseBody(
+  ImmutableSeq<WithPos<Term.Matching>> clauses
+) {
+}
diff --git a/syntax/src/main/java/org/aya/syntax/core/def/FnDef.java b/syntax/src/main/java/org/aya/syntax/core/def/FnDef.java
index 503c2e84a9..1d4cd5980a 100644
--- a/syntax/src/main/java/org/aya/syntax/core/def/FnDef.java
+++ b/syntax/src/main/java/org/aya/syntax/core/def/FnDef.java
@@ -1,28 +1,26 @@
-// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2025 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.syntax.core.def;
 
-import kala.collection.immutable.ImmutableSeq;
+import java.util.EnumSet;
+import java.util.function.Function;
+
 import kala.control.Either;
 import org.aya.generic.Modifier;
 import org.aya.syntax.concrete.stmt.decl.FnDecl;
 import org.aya.syntax.core.term.Term;
 import org.aya.syntax.ref.DefVar;
-import org.aya.util.error.WithPos;
 import org.jetbrains.annotations.NotNull;
 
-import java.util.EnumSet;
-import java.util.function.Function;
-
 public record FnDef(
   @NotNull DefVar<FnDef, FnDecl> ref,
   @NotNull EnumSet<Modifier> modifiers,
-  @NotNull Either<Term, ImmutableSeq<WithPos<Term.Matching>>> body
+  @NotNull Either<Term, FnClauseBody> body
 ) implements TopLevelDef {
   public FnDef { ref.initialize(this); }
 
-  public static <T> Function<Either<Term, ImmutableSeq<WithPos<Term.Matching>>>, T>
-  factory(Function<Either<Term, ImmutableSeq<WithPos<Term.Matching>>>, T> function) {
+  public static <T> Function<Either<Term, FnClauseBody>, T>
+  factory(Function<Either<Term, FnClauseBody>, T> function) {
     return function;
   }
 

From 7857bc1f3abea6dfdaa15c171834ccad5a1e6609 Mon Sep 17 00:00:00 2001
From: ice1000 <ice1000kotlin@foxmail.com>
Date: Sat, 25 Jan 2025 05:27:59 -0500
Subject: [PATCH 2/6] core: construct the `coreBody`

---
 .../java/org/aya/normalize/Normalizer.java    |  5 ++---
 .../java/org/aya/primitive/ShapeMatcher.java  |  4 ++--
 .../main/java/org/aya/terck/CallResolver.java |  2 +-
 .../main/java/org/aya/tyck/StmtTycker.java    | 20 +++++++++++--------
 .../java/org/aya/tyck/pat/IApplyConfl.java    |  2 +-
 .../java/org/aya/prettier/CorePrettier.java   |  4 ++--
 .../org/aya/syntax/core/def/FnClauseBody.java |  6 +++---
 .../java/org/aya/syntax/core/def/FnDef.java   |  6 ------
 8 files changed, 23 insertions(+), 26 deletions(-)

diff --git a/base/src/main/java/org/aya/normalize/Normalizer.java b/base/src/main/java/org/aya/normalize/Normalizer.java
index 2099b8fcb8..fc12295385 100644
--- a/base/src/main/java/org/aya/normalize/Normalizer.java
+++ b/base/src/main/java/org/aya/normalize/Normalizer.java
@@ -15,7 +15,6 @@
 import org.aya.generic.Modifier;
 import org.aya.syntax.compile.JitFn;
 import org.aya.syntax.compile.JitMatchy;
-import org.aya.syntax.core.def.FnClauseBody;
 import org.aya.syntax.core.def.FnDef;
 import org.aya.syntax.core.def.Matchy;
 import org.aya.syntax.core.pat.PatMatcher;
@@ -93,8 +92,8 @@ case FnCall(FnDef.Delegate delegate, int ulift, var args) -> {
               term = body.instTele(args.view());
               continue;
             }
-            case Either.Right(FnClauseBody(var clauses)): {
-              var result = tryUnfoldClauses(clauses.view().map(WithPos::data),
+            case Either.Right(var body): {
+              var result = tryUnfoldClauses(body.clauses.view().map(WithPos::data),
                 args, core.is(Modifier.Overlap), ulift);
               // we may get stuck
               if (result == null) return defaultValue;
diff --git a/base/src/main/java/org/aya/primitive/ShapeMatcher.java b/base/src/main/java/org/aya/primitive/ShapeMatcher.java
index 8370e5dde1..4c5df43b35 100644
--- a/base/src/main/java/org/aya/primitive/ShapeMatcher.java
+++ b/base/src/main/java/org/aya/primitive/ShapeMatcher.java
@@ -123,10 +123,10 @@ private boolean matchFn(@NotNull FnShape shape, @NotNull FnDef def) {
     return switch (new Pair<>(shape.body(), def.body())) {
       case Pair(Either.Left(var termShape), Either.Left(var term)) ->
         matchInside(() -> captures.put(shape.name(), def.ref()), () -> matchTerm(termShape, term));
-      case Pair(Either.Right(var clauseShapes), Either.Right(FnClauseBody(var clauses))) -> {
+      case Pair(Either.Right(var clauseShapes), Either.Right(var body)) -> {
         var mode = def.is(Modifier.Overlap) ? MatchMode.Sub : MatchMode.Eq;
         yield matchInside(() -> captures.put(shape.name(), def.ref()), () ->
-          matchMany(mode, clauseShapes, clauses.view().map(WithPos::data), this::matchClause));
+          matchMany(mode, clauseShapes, body.clauses.view().map(WithPos::data), this::matchClause));
       }
       default -> false;
     };
diff --git a/base/src/main/java/org/aya/terck/CallResolver.java b/base/src/main/java/org/aya/terck/CallResolver.java
index cb5ad6b86b..ec2f01087a 100644
--- a/base/src/main/java/org/aya/terck/CallResolver.java
+++ b/base/src/main/java/org/aya/terck/CallResolver.java
@@ -139,7 +139,7 @@ private Relation compareConArgs(@NotNull ImmutableSeq<Term> conArgs, @NotNull Pa
   }
 
   public void check() {
-    var clauses = caller.body().getRightValue().clauses();
+    var clauses = caller.body().getRightValue().clauses;
     clauses.view().map(WithPos::data).forEach(this);
   }
 
diff --git a/base/src/main/java/org/aya/tyck/StmtTycker.java b/base/src/main/java/org/aya/tyck/StmtTycker.java
index 36f7cae696..eb4f781a0e 100644
--- a/base/src/main/java/org/aya/tyck/StmtTycker.java
+++ b/base/src/main/java/org/aya/tyck/StmtTycker.java
@@ -2,6 +2,8 @@
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.tyck;
 
+import static org.aya.tyck.tycker.TeleTycker.loadTele;
+
 import kala.collection.immutable.ImmutableSeq;
 import kala.control.Either;
 import kala.control.Option;
@@ -44,8 +46,6 @@
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 
-import static org.aya.tyck.tycker.TeleTycker.loadTele;
-
 public record StmtTycker(
   @NotNull SuppressingReporter reporter, @NotNull ModulePath fileModule,
   @NotNull ShapeFactory shapeFactory, @NotNull PrimFactory primFactory
@@ -85,8 +85,6 @@ public void suppress(@NotNull Decl decl) {
       case FnDecl fnDecl -> {
         var fnRef = fnDecl.ref;
         assert fnRef.signature != null;
-
-        var factory = FnDef.factory(body -> new FnDef(fnRef, fnDecl.modifiers, body));
         var teleVars = fnDecl.telescope.map(Expr.Param::ref);
 
         yield switch (fnDecl.body) {
@@ -100,7 +98,7 @@ yield switch (fnDecl.body) {
             var zonker = new Finalizer.Zonk<>(tycker);
             var resultTerm = zonker.zonk(result).bindTele(teleVars.view());
             fnRef.signature = fnRef.signature.descent(zonker::zonk);
-            yield factory.apply(Either.left(resultTerm));
+            yield new FnDef(fnRef, fnDecl.modifiers, Either.left(resultTerm));
           }
           case FnBody.BlockBody body -> {
             var clauses = body.clauses();
@@ -120,10 +118,12 @@ yield switch (fnDecl.body) {
             var orderIndependent = fnDecl.modifiers.contains(Modifier.Overlap);
             FnDef def;
             ClauseTycker.TyckResult patResult;
+            FnClauseBody coreBody;
             if (orderIndependent) {
               // Order-independent.
               patResult = clauseTycker.checkNoClassify();
-              def = factory.apply(Either.right(patResult.wellTyped()));
+              coreBody = new FnClauseBody(patResult.wellTyped());
+              def = new FnDef(fnRef, fnDecl.modifiers, Either.right(coreBody));
               if (!patResult.hasLhsError()) {
                 var rawParams = signature.params();
                 var confluence = new YouTrack(rawParams, tycker, fnDecl.sourcePos());
@@ -132,9 +132,13 @@ yield switch (fnDecl.body) {
               }
             } else {
               patResult = clauseTycker.check(fnDecl.entireSourcePos());
-              def = factory.apply(Either.right(patResult.wellTyped()));
+              coreBody = new FnClauseBody(patResult.wellTyped());
+              def = new FnDef(fnRef, fnDecl.modifiers, Either.right(coreBody));
+            }
+            if (!patResult.hasLhsError()) {
+              var hitConflChecker = new IApplyConfl(def, tycker, fnDecl.sourcePos());
+              hitConflChecker.check();
             }
-            if (!patResult.hasLhsError()) new IApplyConfl(def, tycker, fnDecl.sourcePos()).check();
             yield def;
           }
         };
diff --git a/base/src/main/java/org/aya/tyck/pat/IApplyConfl.java b/base/src/main/java/org/aya/tyck/pat/IApplyConfl.java
index 2a245b3e91..2288b55627 100644
--- a/base/src/main/java/org/aya/tyck/pat/IApplyConfl.java
+++ b/base/src/main/java/org/aya/tyck/pat/IApplyConfl.java
@@ -42,7 +42,7 @@ public record IApplyConfl(
   boolean orderIndep, @NotNull SourcePos sourcePos, @NotNull ExprTycker tycker
 ) {
   public IApplyConfl(@NotNull FnDef def, @NotNull ExprTycker tycker, @NotNull SourcePos pos) {
-    this(def, def.body().getRightValue().clauses(), def.is(Modifier.Overlap), pos, tycker);
+    this(def, def.body().getRightValue().clauses, def.is(Modifier.Overlap), pos, tycker);
   }
   public void check() {
     // A matcher that does not normalize the arguments.
diff --git a/syntax/src/main/java/org/aya/prettier/CorePrettier.java b/syntax/src/main/java/org/aya/prettier/CorePrettier.java
index f8742f794b..f80ee53a29 100644
--- a/syntax/src/main/java/org/aya/prettier/CorePrettier.java
+++ b/syntax/src/main/java/org/aya/prettier/CorePrettier.java
@@ -285,8 +285,8 @@ private ImmutableSeq<Term> visibleArgsOf(Callable call) {
         var line1sep = Doc.sepNonEmpty(line1);
         yield switch (def.body()) {
           case Either.Left(var term) -> Doc.sep(line1sep, FN_DEFINED_AS, term(Outer.Free, term.instTele(subst)));
-          case Either.Right(FnClauseBody(var clauses)) -> Doc.vcat(line1sep,
-            Doc.nest(2, visitClauses(clauses.view().map(WithPos::data), tele.view().map(ParamLike::explicit))));
+          case Either.Right(var body) -> Doc.vcat(line1sep,
+            Doc.nest(2, visitClauses(body.clauses.view().map(WithPos::data), tele.view().map(ParamLike::explicit))));
         };
       }
       case MemberDef field -> Doc.sepNonEmpty(Doc.symbol("|"),
diff --git a/syntax/src/main/java/org/aya/syntax/core/def/FnClauseBody.java b/syntax/src/main/java/org/aya/syntax/core/def/FnClauseBody.java
index 59051eecc8..54dd2060df 100644
--- a/syntax/src/main/java/org/aya/syntax/core/def/FnClauseBody.java
+++ b/syntax/src/main/java/org/aya/syntax/core/def/FnClauseBody.java
@@ -6,7 +6,7 @@
 import org.aya.syntax.core.term.Term;
 import org.aya.util.error.WithPos;
 
-public record FnClauseBody(
-  ImmutableSeq<WithPos<Term.Matching>> clauses
-) {
+public final class FnClauseBody {
+  public final ImmutableSeq<WithPos<Term.Matching>> clauses;
+  public FnClauseBody(ImmutableSeq<WithPos<Term.Matching>> clauses) { this.clauses = clauses; }
 }
diff --git a/syntax/src/main/java/org/aya/syntax/core/def/FnDef.java b/syntax/src/main/java/org/aya/syntax/core/def/FnDef.java
index 1d4cd5980a..00614eca9d 100644
--- a/syntax/src/main/java/org/aya/syntax/core/def/FnDef.java
+++ b/syntax/src/main/java/org/aya/syntax/core/def/FnDef.java
@@ -3,7 +3,6 @@
 package org.aya.syntax.core.def;
 
 import java.util.EnumSet;
-import java.util.function.Function;
 
 import kala.control.Either;
 import org.aya.generic.Modifier;
@@ -19,11 +18,6 @@ public record FnDef(
 ) implements TopLevelDef {
   public FnDef { ref.initialize(this); }
 
-  public static <T> Function<Either<Term, FnClauseBody>, T>
-  factory(Function<Either<Term, FnClauseBody>, T> function) {
-    return function;
-  }
-
   public boolean is(@NotNull Modifier mod) { return modifiers.contains(mod); }
   public static final class Delegate extends TyckAnyDef<FnDef> implements FnDefLike {
     public Delegate(@NotNull DefVar<FnDef, ?> ref) { super(ref); }

From 3459e769770f15f33b361970f9be5ef6b8dfa274 Mon Sep 17 00:00:00 2001
From: ice1000 <ice1000kotlin@foxmail.com>
Date: Sat, 25 Jan 2025 05:38:46 -0500
Subject: [PATCH 3/6] tyck: store classes into `coreBody`

---
 .../main/java/org/aya/tyck/ExprTycker.java    | 11 ++++-----
 .../main/java/org/aya/tyck/StmtTycker.java    | 21 ++++++++++-------
 .../java/org/aya/tyck/pat/ClauseTycker.java   | 23 +++++++++++++------
 .../org/aya/syntax/core/def/FnClauseBody.java |  2 ++
 4 files changed, 36 insertions(+), 21 deletions(-)

diff --git a/base/src/main/java/org/aya/tyck/ExprTycker.java b/base/src/main/java/org/aya/tyck/ExprTycker.java
index 2e8cabbd38..d5ca80d6ce 100644
--- a/base/src/main/java/org/aya/tyck/ExprTycker.java
+++ b/base/src/main/java/org/aya/tyck/ExprTycker.java
@@ -2,7 +2,10 @@
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.tyck;
 
-import kala.collection.AbstractSeqView;
+import java.util.Comparator;
+import java.util.function.BiFunction;
+import java.util.function.Function;
+
 import kala.collection.immutable.ImmutableSeq;
 import kala.collection.immutable.ImmutableTreeSeq;
 import kala.collection.mutable.MutableList;
@@ -51,10 +54,6 @@
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 
-import java.util.Comparator;
-import java.util.function.BiFunction;
-import java.util.function.Function;
-
 public final class ExprTycker extends AbstractTycker implements Unifiable {
   public final @NotNull MutableTreeSet<WithPos<Expr.WithTerm>> withTerms =
     MutableTreeSet.create(Comparator.comparing(SourceNode::sourcePos));
@@ -193,7 +192,7 @@ && whnf(type) instanceof DataCall dataCall
         new LocalVar("match" + i, discriminant.get(i).sourcePos(), GenerateKind.Basic.Tyck)),
       ImmutableSeq.empty(), clauses);
     var wellClauses = clauseTycker.check(exprPos)
-      .wellTyped()
+      .clauses()
       .map(WithPos::data);
 
     // Find free occurrences
diff --git a/base/src/main/java/org/aya/tyck/StmtTycker.java b/base/src/main/java/org/aya/tyck/StmtTycker.java
index eb4f781a0e..98b831972b 100644
--- a/base/src/main/java/org/aya/tyck/StmtTycker.java
+++ b/base/src/main/java/org/aya/tyck/StmtTycker.java
@@ -117,25 +117,30 @@ yield switch (fnDecl.body) {
 
             var orderIndependent = fnDecl.modifiers.contains(Modifier.Overlap);
             FnDef def;
-            ClauseTycker.TyckResult patResult;
+            boolean hasLhsError;
             FnClauseBody coreBody;
             if (orderIndependent) {
               // Order-independent.
-              patResult = clauseTycker.checkNoClassify();
+              var patResult = clauseTycker.checkNoClassify();
               coreBody = new FnClauseBody(patResult.wellTyped());
               def = new FnDef(fnRef, fnDecl.modifiers, Either.right(coreBody));
-              if (!patResult.hasLhsError()) {
+              hasLhsError = patResult.hasLhsError();
+              if (!hasLhsError) {
                 var rawParams = signature.params();
                 var confluence = new YouTrack(rawParams, tycker, fnDecl.sourcePos());
-                confluence.check(patResult, signature.result(),
-                  PatClassifier.classify(patResult.clauses().view(), rawParams.view(), tycker, fnDecl.sourcePos()));
+                var classes = PatClassifier.classify(patResult.clauses().view(),
+                  rawParams.view(), tycker, fnDecl.sourcePos());
+                coreBody.classes = classes;
+                confluence.check(patResult, signature.result(), classes);
               }
             } else {
-              patResult = clauseTycker.check(fnDecl.entireSourcePos());
-              coreBody = new FnClauseBody(patResult.wellTyped());
+              var patResult = clauseTycker.check(fnDecl.entireSourcePos());
+              coreBody = new FnClauseBody(patResult.clauses());
+              coreBody.classes = patResult.classes();
+              hasLhsError = patResult.hasLhsError();
               def = new FnDef(fnRef, fnDecl.modifiers, Either.right(coreBody));
             }
-            if (!patResult.hasLhsError()) {
+            if (!hasLhsError) {
               var hitConflChecker = new IApplyConfl(def, tycker, fnDecl.sourcePos());
               hitConflChecker.check();
             }
diff --git a/base/src/main/java/org/aya/tyck/pat/ClauseTycker.java b/base/src/main/java/org/aya/tyck/pat/ClauseTycker.java
index 943f23bab2..53a618afed 100644
--- a/base/src/main/java/org/aya/tyck/pat/ClauseTycker.java
+++ b/base/src/main/java/org/aya/tyck/pat/ClauseTycker.java
@@ -2,6 +2,9 @@
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.tyck.pat;
 
+import java.util.function.Supplier;
+import java.util.function.UnaryOperator;
+
 import kala.collection.SeqView;
 import kala.collection.immutable.ImmutableSeq;
 import kala.value.primitive.MutableBooleanValue;
@@ -31,11 +34,10 @@
 import org.aya.util.error.SourcePos;
 import org.aya.util.error.WithPos;
 import org.aya.util.reporter.Reporter;
+import org.aya.util.tyck.pat.PatClass;
 import org.jetbrains.annotations.Contract;
 import org.jetbrains.annotations.NotNull;
-
-import java.util.function.Supplier;
-import java.util.function.UnaryOperator;
+import org.jetbrains.annotations.Nullable;
 
 public final class ClauseTycker implements Problematic, Stateful {
   private final @NotNull ExprTycker exprTycker;
@@ -89,6 +91,11 @@ public void addLocalLet(@NotNull ImmutableSeq<LocalVar> teleBinds, @NotNull Expr
     }
   }
 
+  public record WorkerResult(
+    ImmutableSeq<WithPos<Term.Matching>> clauses,
+    @Nullable ImmutableSeq<PatClass<ImmutableSeq<Term>>> classes,
+    boolean hasLhsError
+  ) { }
   public record Worker(
     @NotNull ClauseTycker parent,
     @NotNull ImmutableSeq<Param> telescope,
@@ -97,11 +104,12 @@ public record Worker(
     @NotNull ImmutableSeq<LocalVar> elims,
     @NotNull ImmutableSeq<Pattern.Clause> clauses
   ) {
-    public @NotNull TyckResult check(@NotNull SourcePos overallPos) {
+    public @NotNull WorkerResult check(@NotNull SourcePos overallPos) {
       var lhs = checkAllLhs();
 
+      ImmutableSeq<PatClass<ImmutableSeq<Term>>> classes = null;
       if (lhs.noneMatch(r -> r.hasError)) {
-        var classes = PatClassifier.classify(
+        classes = PatClassifier.classify(
           lhs.view().map(LhsResult::clause),
           telescope.view().concat(unpi.params()), parent.exprTycker, overallPos);
         if (clauses.isNotEmpty()) {
@@ -110,7 +118,8 @@ public record Worker(
         }
       }
 
-      return parent.checkAllRhs(teleVars, lhs.map(cl -> cl.mapPats(new TypeEraser())));
+      var rhs = parent.checkAllRhs(teleVars, lhs.map(cl -> cl.mapPats(new TypeEraser())));
+      return new WorkerResult(rhs.wellTyped(), classes, rhs.hasLhsError);
     }
 
     public @NotNull ImmutableSeq<LhsResult> checkAllLhs() {
@@ -188,7 +197,7 @@ public record Worker(
         // 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 wellTypedPats = patResult.wellTyped().appendedAll(missingPats);
       var patWithTypeBound = Pat.collectVariables(wellTypedPats.view());
 
diff --git a/syntax/src/main/java/org/aya/syntax/core/def/FnClauseBody.java b/syntax/src/main/java/org/aya/syntax/core/def/FnClauseBody.java
index 54dd2060df..14910d8473 100644
--- a/syntax/src/main/java/org/aya/syntax/core/def/FnClauseBody.java
+++ b/syntax/src/main/java/org/aya/syntax/core/def/FnClauseBody.java
@@ -5,8 +5,10 @@
 import kala.collection.immutable.ImmutableSeq;
 import org.aya.syntax.core.term.Term;
 import org.aya.util.error.WithPos;
+import org.aya.util.tyck.pat.PatClass;
 
 public final class FnClauseBody {
   public final ImmutableSeq<WithPos<Term.Matching>> clauses;
+  public ImmutableSeq<PatClass<ImmutableSeq<Term>>> classes;
   public FnClauseBody(ImmutableSeq<WithPos<Term.Matching>> clauses) { this.clauses = clauses; }
 }

From 82ce4a9b25dba02d9d3cb18481da9a885fea5d92 Mon Sep 17 00:00:00 2001
From: ice1000 <ice1000kotlin@foxmail.com>
Date: Sat, 25 Jan 2025 06:23:53 -0500
Subject: [PATCH 4/6] tyck: reduce by the prefix array

---
 .../main/java/org/aya/tyck/ExprTycker.java    |  3 +-
 .../main/java/org/aya/tyck/StmtTycker.java    |  6 +--
 .../java/org/aya/tyck/pat/ClauseTycker.java   | 45 ++++++++++++++-----
 .../main/java/org/aya/tyck/pat/YouTrack.java  |  5 +--
 .../java/org/aya/syntax/core/def/FnDef.java   |  3 +-
 .../java/org/aya/util/tyck/pat/PatClass.java  | 12 +++--
 6 files changed, 49 insertions(+), 25 deletions(-)

diff --git a/base/src/main/java/org/aya/tyck/ExprTycker.java b/base/src/main/java/org/aya/tyck/ExprTycker.java
index d5ca80d6ce..84fd69a575 100644
--- a/base/src/main/java/org/aya/tyck/ExprTycker.java
+++ b/base/src/main/java/org/aya/tyck/ExprTycker.java
@@ -192,8 +192,7 @@ && whnf(type) instanceof DataCall dataCall
         new LocalVar("match" + i, discriminant.get(i).sourcePos(), GenerateKind.Basic.Tyck)),
       ImmutableSeq.empty(), clauses);
     var wellClauses = clauseTycker.check(exprPos)
-      .clauses()
-      .map(WithPos::data);
+      .wellTyped().clauses.map(WithPos::data);
 
     // Find free occurrences
     var usages = new FreeCollector();
diff --git a/base/src/main/java/org/aya/tyck/StmtTycker.java b/base/src/main/java/org/aya/tyck/StmtTycker.java
index 98b831972b..d02add1db1 100644
--- a/base/src/main/java/org/aya/tyck/StmtTycker.java
+++ b/base/src/main/java/org/aya/tyck/StmtTycker.java
@@ -130,13 +130,13 @@ yield switch (fnDecl.body) {
                 var confluence = new YouTrack(rawParams, tycker, fnDecl.sourcePos());
                 var classes = PatClassifier.classify(patResult.clauses().view(),
                   rawParams.view(), tycker, fnDecl.sourcePos());
-                coreBody.classes = classes;
+                var absurds = patResult.absurdPrefixCount();
+                coreBody.classes = classes.map(cls -> cls.ignoreAbsurd(absurds));
                 confluence.check(patResult, signature.result(), classes);
               }
             } else {
               var patResult = clauseTycker.check(fnDecl.entireSourcePos());
-              coreBody = new FnClauseBody(patResult.clauses());
-              coreBody.classes = patResult.classes();
+              coreBody = patResult.wellTyped();
               hasLhsError = patResult.hasLhsError();
               def = new FnDef(fnRef, fnDecl.modifiers, Either.right(coreBody));
             }
diff --git a/base/src/main/java/org/aya/tyck/pat/ClauseTycker.java b/base/src/main/java/org/aya/tyck/pat/ClauseTycker.java
index 53a618afed..5dbd0e40d1 100644
--- a/base/src/main/java/org/aya/tyck/pat/ClauseTycker.java
+++ b/base/src/main/java/org/aya/tyck/pat/ClauseTycker.java
@@ -7,6 +7,8 @@
 
 import kala.collection.SeqView;
 import kala.collection.immutable.ImmutableSeq;
+import kala.collection.immutable.primitive.ImmutableIntArray;
+import kala.collection.immutable.primitive.ImmutableIntSeq;
 import kala.value.primitive.MutableBooleanValue;
 import org.aya.generic.Renamer;
 import org.aya.normalize.Finalizer;
@@ -14,6 +16,7 @@
 import org.aya.syntax.concrete.Expr;
 import org.aya.syntax.concrete.Pattern;
 import org.aya.syntax.core.Jdg;
+import org.aya.syntax.core.def.FnClauseBody;
 import org.aya.syntax.core.pat.Pat;
 import org.aya.syntax.core.pat.PatToTerm;
 import org.aya.syntax.core.pat.TypeEraser;
@@ -48,6 +51,18 @@ public record TyckResult(@NotNull ImmutableSeq<Pat.Preclause<Term>> clauses, boo
     public @NotNull ImmutableSeq<WithPos<Term.Matching>> wellTyped() {
       return clauses.flatMap(Pat.Preclause::lift);
     }
+    /// @return null if there is no absurd pattern
+    public @Nullable ImmutableIntSeq absurdPrefixCount() {
+      var ints = new int[clauses.size()];
+      var count = 0;
+      for (int i = 0; i < clauses.size(); i++) {
+        var clause = clauses.get(i);
+        if (clause.expr() == null) count++;
+        ints[i] = count;
+      }
+      if (count == 0) return null;
+      return ImmutableIntArray.Unsafe.wrap(ints);
+    }
   }
 
   /**
@@ -91,11 +106,7 @@ public void addLocalLet(@NotNull ImmutableSeq<LocalVar> teleBinds, @NotNull Expr
     }
   }
 
-  public record WorkerResult(
-    ImmutableSeq<WithPos<Term.Matching>> clauses,
-    @Nullable ImmutableSeq<PatClass<ImmutableSeq<Term>>> classes,
-    boolean hasLhsError
-  ) { }
+  public record WorkerResult(FnClauseBody wellTyped, boolean hasLhsError) { }
   public record Worker(
     @NotNull ClauseTycker parent,
     @NotNull ImmutableSeq<Param> telescope,
@@ -107,8 +118,9 @@ public record Worker(
     public @NotNull WorkerResult check(@NotNull SourcePos overallPos) {
       var lhs = checkAllLhs();
 
-      ImmutableSeq<PatClass<ImmutableSeq<Term>>> classes = null;
-      if (lhs.noneMatch(r -> r.hasError)) {
+      ImmutableSeq<PatClass<ImmutableSeq<Term>>> classes;
+      var hasError = lhs.anyMatch(LhsResult::hasError);
+      if (!hasError) {
         classes = PatClassifier.classify(
           lhs.view().map(LhsResult::clause),
           telescope.view().concat(unpi.params()), parent.exprTycker, overallPos);
@@ -116,10 +128,18 @@ public record Worker(
           var usages = PatClassifier.firstMatchDomination(clauses, parent, classes);
           // refinePatterns(lhs, usages, classes);
         }
+      } else {
+        classes = null;
       }
 
-      var rhs = parent.checkAllRhs(teleVars, lhs.map(cl -> cl.mapPats(new TypeEraser())));
-      return new WorkerResult(rhs.wellTyped(), classes, rhs.hasLhsError);
+      var map = lhs.map(cl -> cl.mapPats(new TypeEraser()));
+      var rhs = parent.checkAllRhs(teleVars, map, hasError);
+      var wellTyped = new FnClauseBody(rhs.wellTyped());
+      if (classes != null) {
+        var absurds = rhs.absurdPrefixCount();
+        wellTyped.classes = classes.map(cl -> cl.ignoreAbsurd(absurds));
+      }
+      return new WorkerResult(wellTyped, hasError);
     }
 
     public @NotNull ImmutableSeq<LhsResult> checkAllLhs() {
@@ -129,7 +149,8 @@ public record Worker(
     }
 
     public @NotNull TyckResult checkNoClassify() {
-      return parent.checkAllRhs(teleVars, checkAllLhs());
+      var lhsResults = checkAllLhs();
+      return parent.checkAllRhs(teleVars, lhsResults, lhsResults.anyMatch(LhsResult::hasError));
     }
   }
 
@@ -147,9 +168,9 @@ public record Worker(
 
   public @NotNull TyckResult checkAllRhs(
     @NotNull ImmutableSeq<LocalVar> vars,
-    @NotNull ImmutableSeq<LhsResult> lhsResults
+    @NotNull ImmutableSeq<LhsResult> lhsResults,
+    boolean lhsError
   ) {
-    var lhsError = lhsResults.anyMatch(LhsResult::hasError);
     var rhsResult = lhsResults.map(x -> checkRhs(vars, x));
 
     // inline terms in rhsResult
diff --git a/base/src/main/java/org/aya/tyck/pat/YouTrack.java b/base/src/main/java/org/aya/tyck/pat/YouTrack.java
index ab68710168..e49205f0f9 100644
--- a/base/src/main/java/org/aya/tyck/pat/YouTrack.java
+++ b/base/src/main/java/org/aya/tyck/pat/YouTrack.java
@@ -1,4 +1,4 @@
-// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2025 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.tyck.pat;
 
@@ -76,9 +76,8 @@ public void check(
         .flatMapToObj(i -> Pat.Preclause.lift(clauses.clauses().get(i))
           .map(matching -> new Info(i, matching)));
       for (int i = 1, size = contents.size(); i < size; i++) {
-        var ix = i;
         try (var _ = tycker.subscope()) {
-          unifyClauses(type, contents.get(ix - 1), contents.get(ix), doms);
+          unifyClauses(type, contents.get(i - 1), contents.get(i), doms);
         }
       }
     });
diff --git a/syntax/src/main/java/org/aya/syntax/core/def/FnDef.java b/syntax/src/main/java/org/aya/syntax/core/def/FnDef.java
index 00614eca9d..e193db522d 100644
--- a/syntax/src/main/java/org/aya/syntax/core/def/FnDef.java
+++ b/syntax/src/main/java/org/aya/syntax/core/def/FnDef.java
@@ -21,8 +21,7 @@ public record FnDef(
   public boolean is(@NotNull Modifier mod) { return modifiers.contains(mod); }
   public static final class Delegate extends TyckAnyDef<FnDef> implements FnDefLike {
     public Delegate(@NotNull DefVar<FnDef, ?> ref) { super(ref); }
-    @Override
-    public boolean is(@NotNull Modifier mod) {
+    @Override public boolean is(@NotNull Modifier mod) {
       var core = ref.core;
       if (core != null) return core.is(mod);
       return ((FnDecl) ref.concrete).modifiers.contains(mod);
diff --git a/tools-kala/src/main/java/org/aya/util/tyck/pat/PatClass.java b/tools-kala/src/main/java/org/aya/util/tyck/pat/PatClass.java
index 41a6ee3d55..edf8f532d8 100644
--- a/tools-kala/src/main/java/org/aya/util/tyck/pat/PatClass.java
+++ b/tools-kala/src/main/java/org/aya/util/tyck/pat/PatClass.java
@@ -1,12 +1,13 @@
-// Copyright (c) 2020-2023 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2025 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.util.tyck.pat;
 
+import java.util.function.Function;
+
 import kala.collection.immutable.ImmutableSeq;
 import kala.collection.immutable.primitive.ImmutableIntSeq;
 import org.jetbrains.annotations.NotNull;
-
-import java.util.function.Function;
+import org.jetbrains.annotations.Nullable;
 
 public record PatClass<T>(@NotNull T term, @NotNull ImmutableIntSeq cls) {
   public <R> @NotNull PatClass<R> map(Function<T, R> f) {
@@ -16,4 +17,9 @@ public record PatClass<T>(@NotNull T term, @NotNull ImmutableIntSeq cls) {
   public <P> @NotNull ImmutableSeq<P> extract(@NotNull ImmutableSeq<P> seq) {
     return cls.mapToObj(seq::get);
   }
+
+  public @NotNull PatClass<T> ignoreAbsurd(@Nullable ImmutableIntSeq absurdPrefixCount) {
+    if (absurdPrefixCount == null) return this;
+    return new PatClass<>(term, cls.map(i -> i - absurdPrefixCount.get(i)));
+  }
 }

From ad5cce95c2dc34607b4eb1d064f4d80abdf246cd Mon Sep 17 00:00:00 2001
From: ice1000 <ice1000kotlin@foxmail.com>
Date: Sat, 25 Jan 2025 06:30:08 -0500
Subject: [PATCH 5/6] confl: simplify

---
 base/src/main/java/org/aya/tyck/StmtTycker.java   |  2 +-
 base/src/main/java/org/aya/tyck/pat/YouTrack.java | 14 ++++----------
 2 files changed, 5 insertions(+), 11 deletions(-)

diff --git a/base/src/main/java/org/aya/tyck/StmtTycker.java b/base/src/main/java/org/aya/tyck/StmtTycker.java
index d02add1db1..066d53fdb2 100644
--- a/base/src/main/java/org/aya/tyck/StmtTycker.java
+++ b/base/src/main/java/org/aya/tyck/StmtTycker.java
@@ -132,7 +132,7 @@ yield switch (fnDecl.body) {
                   rawParams.view(), tycker, fnDecl.sourcePos());
                 var absurds = patResult.absurdPrefixCount();
                 coreBody.classes = classes.map(cls -> cls.ignoreAbsurd(absurds));
-                confluence.check(patResult, signature.result(), classes);
+                confluence.check(coreBody, signature.result());
               }
             } else {
               var patResult = clauseTycker.check(fnDecl.entireSourcePos());
diff --git a/base/src/main/java/org/aya/tyck/pat/YouTrack.java b/base/src/main/java/org/aya/tyck/pat/YouTrack.java
index e49205f0f9..3f009a802f 100644
--- a/base/src/main/java/org/aya/tyck/pat/YouTrack.java
+++ b/base/src/main/java/org/aya/tyck/pat/YouTrack.java
@@ -7,7 +7,7 @@
 import kala.collection.mutable.MutableLinkedSet;
 import kala.collection.mutable.MutableList;
 import kala.collection.mutable.MutableSet;
-import org.aya.syntax.core.pat.Pat;
+import org.aya.syntax.core.def.FnClauseBody;
 import org.aya.syntax.core.term.FreeTerm;
 import org.aya.syntax.core.term.Param;
 import org.aya.syntax.core.term.Term;
@@ -17,7 +17,6 @@
 import org.aya.tyck.error.UnifyInfo;
 import org.aya.util.error.SourcePos;
 import org.aya.util.error.WithPos;
-import org.aya.util.tyck.pat.PatClass;
 import org.jetbrains.annotations.NotNull;
 
 /**
@@ -66,15 +65,10 @@ private void domination(
       doms.add(new ClausesProblem.Domination(lhsIx + 1, rhsIx + 1, matching.sourcePos()));
   }
 
-  public void check(
-    @NotNull ClauseTycker.TyckResult clauses, @NotNull Term type,
-    @NotNull ImmutableSeq<PatClass<ImmutableSeq<Term>>> mct
-  ) {
+  public void check(@NotNull FnClauseBody body, @NotNull Term type) {
     var doms = MutableLinkedSet.<ClausesProblem.Domination>create();
-    mct.forEach(results -> {
-      var contents = results.cls()
-        .flatMapToObj(i -> Pat.Preclause.lift(clauses.clauses().get(i))
-          .map(matching -> new Info(i, matching)));
+    body.classes.forEach(results -> {
+      var contents = results.cls().mapToObj(i -> new Info(i, body.clauses.get(i)));
       for (int i = 1, size = contents.size(); i < size; i++) {
         try (var _ = tycker.subscope()) {
           unifyClauses(type, contents.get(i - 1), contents.get(i), doms);

From cb5abcbbac6e7ac2719d55d82114240f7cb38fc5 Mon Sep 17 00:00:00 2001
From: ice1000 <ice1000kotlin@foxmail.com>
Date: Sat, 25 Jan 2025 06:36:06 -0500
Subject: [PATCH 6/6] serde: fix compile

---
 .../java/org/aya/normalize/Normalizer.java    |  3 +-
 .../java/org/aya/primitive/ShapeMatcher.java  |  3 +-
 .../main/java/org/aya/terck/CallResolver.java |  5 +--
 .../main/java/org/aya/tyck/ExprTycker.java    |  6 +--
 .../compiler/serializers/FnSerializer.java    | 39 +++++++++----------
 .../java/org/aya/prettier/CorePrettier.java   |  3 +-
 .../org/aya/syntax/core/def/FnClauseBody.java |  5 +++
 7 files changed, 31 insertions(+), 33 deletions(-)

diff --git a/base/src/main/java/org/aya/normalize/Normalizer.java b/base/src/main/java/org/aya/normalize/Normalizer.java
index fc12295385..1f47938098 100644
--- a/base/src/main/java/org/aya/normalize/Normalizer.java
+++ b/base/src/main/java/org/aya/normalize/Normalizer.java
@@ -30,7 +30,6 @@
 import org.aya.syntax.ref.LocalVar;
 import org.aya.tyck.TyckState;
 import org.aya.tyck.tycker.Stateful;
-import org.aya.util.error.WithPos;
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 
@@ -93,7 +92,7 @@ case FnCall(FnDef.Delegate delegate, int ulift, var args) -> {
               continue;
             }
             case Either.Right(var body): {
-              var result = tryUnfoldClauses(body.clauses.view().map(WithPos::data),
+              var result = tryUnfoldClauses(body.matchingsView(),
                 args, core.is(Modifier.Overlap), ulift);
               // we may get stuck
               if (result == null) return defaultValue;
diff --git a/base/src/main/java/org/aya/primitive/ShapeMatcher.java b/base/src/main/java/org/aya/primitive/ShapeMatcher.java
index 4c5df43b35..08b10da7b0 100644
--- a/base/src/main/java/org/aya/primitive/ShapeMatcher.java
+++ b/base/src/main/java/org/aya/primitive/ShapeMatcher.java
@@ -29,7 +29,6 @@
 import org.aya.util.Pair;
 import org.aya.util.RepoLike;
 import org.aya.util.error.Panic;
-import org.aya.util.error.WithPos;
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 
@@ -126,7 +125,7 @@ case Pair(Either.Left(var termShape), Either.Left(var term)) ->
       case Pair(Either.Right(var clauseShapes), Either.Right(var body)) -> {
         var mode = def.is(Modifier.Overlap) ? MatchMode.Sub : MatchMode.Eq;
         yield matchInside(() -> captures.put(shape.name(), def.ref()), () ->
-          matchMany(mode, clauseShapes, body.clauses.view().map(WithPos::data), this::matchClause));
+          matchMany(mode, clauseShapes, body.matchingsView(), this::matchClause));
       }
       default -> false;
     };
diff --git a/base/src/main/java/org/aya/terck/CallResolver.java b/base/src/main/java/org/aya/terck/CallResolver.java
index ec2f01087a..88ee70b4b8 100644
--- a/base/src/main/java/org/aya/terck/CallResolver.java
+++ b/base/src/main/java/org/aya/terck/CallResolver.java
@@ -24,7 +24,6 @@
 import org.aya.syntax.core.term.xtt.PAppTerm;
 import org.aya.tyck.TyckState;
 import org.aya.tyck.tycker.Stateful;
-import org.aya.util.error.WithPos;
 import org.aya.util.terck.CallGraph;
 import org.aya.util.terck.CallMatrix;
 import org.aya.util.terck.Relation;
@@ -139,8 +138,8 @@ private Relation compareConArgs(@NotNull ImmutableSeq<Term> conArgs, @NotNull Pa
   }
 
   public void check() {
-    var clauses = caller.body().getRightValue().clauses;
-    clauses.view().map(WithPos::data).forEach(this);
+    var clauses = caller.body().getRightValue().matchingsView();
+    clauses.forEach(this);
   }
 
   @Override public void accept(@NotNull Term.Matching matching) {
diff --git a/base/src/main/java/org/aya/tyck/ExprTycker.java b/base/src/main/java/org/aya/tyck/ExprTycker.java
index 84fd69a575..c8a28c3c08 100644
--- a/base/src/main/java/org/aya/tyck/ExprTycker.java
+++ b/base/src/main/java/org/aya/tyck/ExprTycker.java
@@ -191,8 +191,7 @@ && whnf(type) instanceof DataCall dataCall
       ImmutableSeq.fill(discriminant.size(), i ->
         new LocalVar("match" + i, discriminant.get(i).sourcePos(), GenerateKind.Basic.Tyck)),
       ImmutableSeq.empty(), clauses);
-    var wellClauses = clauseTycker.check(exprPos)
-      .wellTyped().clauses.map(WithPos::data);
+    var wellClauses = clauseTycker.check(exprPos).wellTyped().matchingsView();
 
     // Find free occurrences
     var usages = new FreeCollector();
@@ -203,7 +202,8 @@ && whnf(type) instanceof DataCall dataCall
     var captures = usages.collected();
     var lifted = new Matchy(type.bindTele(wellArgs.size(), captures.view()),
       new QName(QPath.fileLevel(fileModule), "match-" + exprPos.lineColumnString()),
-      wellClauses.map(clause -> clause.update(clause.body().bindTele(clause.bindCount(), captures.view()))));
+      wellClauses.map(clause -> clause.update(clause.body().bindTele(clause.bindCount(), captures.view())))
+        .toImmutableSeq());
 
     var wellTerms = wellArgs.map(Jdg::wellTyped);
     return new MatchCall(lifted, wellTerms, captures.map(FreeTerm::new));
diff --git a/jit-compiler/src/main/java/org/aya/compiler/serializers/FnSerializer.java b/jit-compiler/src/main/java/org/aya/compiler/serializers/FnSerializer.java
index 2d6aed76b4..ec0ef74692 100644
--- a/jit-compiler/src/main/java/org/aya/compiler/serializers/FnSerializer.java
+++ b/jit-compiler/src/main/java/org/aya/compiler/serializers/FnSerializer.java
@@ -1,29 +1,28 @@
-// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2025 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.compiler.serializers;
 
+import java.lang.constant.ClassDesc;
+import java.lang.constant.ConstantDescs;
+import java.util.EnumSet;
+import java.util.function.Consumer;
+
 import kala.collection.immutable.ImmutableSeq;
 import kala.control.Either;
 import org.aya.compiler.free.Constants;
 import org.aya.compiler.free.FreeClassBuilder;
 import org.aya.compiler.free.FreeCodeBuilder;
 import org.aya.compiler.free.FreeJavaExpr;
-import org.aya.compiler.free.data.MethodRef;
 import org.aya.compiler.free.data.LocalVariable;
+import org.aya.compiler.free.data.MethodRef;
 import org.aya.generic.Modifier;
 import org.aya.primitive.ShapeFactory;
 import org.aya.syntax.compile.JitFn;
 import org.aya.syntax.core.def.FnDef;
 import org.aya.syntax.core.def.TyckAnyDef;
 import org.aya.syntax.core.term.call.FnCall;
-import org.aya.util.error.WithPos;
 import org.jetbrains.annotations.NotNull;
 
-import java.lang.constant.ClassDesc;
-import java.lang.constant.ConstantDescs;
-import java.util.EnumSet;
-import java.util.function.Consumer;
-
 public final class FnSerializer extends JitTeleSerializer<FnDef> {
   private final @NotNull ShapeFactory shapeFactory;
 
@@ -83,19 +82,17 @@ private void buildInvoke(
       }
       case Either.Right(var clauses) -> {
         var ser = new PatternSerializer(argExprs, onStuckCon, unit.is(Modifier.Overlap));
-        ser.serialize(builder, clauses.view()
-          .map(WithPos::data)
-          .map(matching -> new PatternSerializer.Matching(
-              matching.bindCount(), matching.patterns(), (patSer, builder0, bindSize) -> {
-              var result = serializeTermUnderTele(
-                builder0,
-                matching.body(),
-                patSer.result.ref(),
-                bindSize
-              );
-              builder0.returnWith(result);
-            })
-          ).toImmutableSeq());
+        ser.serialize(builder, clauses.matchingsView().map(matching -> new PatternSerializer.Matching(
+            matching.bindCount(), matching.patterns(), (patSer, builder0, bindSize) -> {
+            var result = serializeTermUnderTele(
+              builder0,
+              matching.body(),
+              patSer.result.ref(),
+              bindSize
+            );
+            builder0.returnWith(result);
+          })
+        ).toImmutableSeq());
       }
     }
   }
diff --git a/syntax/src/main/java/org/aya/prettier/CorePrettier.java b/syntax/src/main/java/org/aya/prettier/CorePrettier.java
index f80ee53a29..b3d4b81664 100644
--- a/syntax/src/main/java/org/aya/prettier/CorePrettier.java
+++ b/syntax/src/main/java/org/aya/prettier/CorePrettier.java
@@ -36,7 +36,6 @@
 import org.aya.syntax.ref.LocalVar;
 import org.aya.util.Arg;
 import org.aya.util.error.SourcePos;
-import org.aya.util.error.WithPos;
 import org.aya.util.prettier.PrettierOptions;
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
@@ -286,7 +285,7 @@ private ImmutableSeq<Term> visibleArgsOf(Callable call) {
         yield switch (def.body()) {
           case Either.Left(var term) -> Doc.sep(line1sep, FN_DEFINED_AS, term(Outer.Free, term.instTele(subst)));
           case Either.Right(var body) -> Doc.vcat(line1sep,
-            Doc.nest(2, visitClauses(body.clauses.view().map(WithPos::data), tele.view().map(ParamLike::explicit))));
+            Doc.nest(2, visitClauses(body.matchingsView(), tele.view().map(ParamLike::explicit))));
         };
       }
       case MemberDef field -> Doc.sepNonEmpty(Doc.symbol("|"),
diff --git a/syntax/src/main/java/org/aya/syntax/core/def/FnClauseBody.java b/syntax/src/main/java/org/aya/syntax/core/def/FnClauseBody.java
index 14910d8473..f60c11e4d2 100644
--- a/syntax/src/main/java/org/aya/syntax/core/def/FnClauseBody.java
+++ b/syntax/src/main/java/org/aya/syntax/core/def/FnClauseBody.java
@@ -2,13 +2,18 @@
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.syntax.core.def;
 
+import kala.collection.SeqView;
 import kala.collection.immutable.ImmutableSeq;
 import org.aya.syntax.core.term.Term;
 import org.aya.util.error.WithPos;
 import org.aya.util.tyck.pat.PatClass;
+import org.jetbrains.annotations.NotNull;
 
 public final class FnClauseBody {
   public final ImmutableSeq<WithPos<Term.Matching>> clauses;
   public ImmutableSeq<PatClass<ImmutableSeq<Term>>> classes;
   public FnClauseBody(ImmutableSeq<WithPos<Term.Matching>> clauses) { this.clauses = clauses; }
+  public @NotNull SeqView<Term.Matching> matchingsView() {
+    return clauses.view().map(WithPos::data);
+  }
 }