review: more cosmetics changes

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

@@ -90,22 +90,23 @@ public record Worker(
     boolean isFn
   ) {
     public @NotNull TyckResult check(@NotNull SourcePos overallPos) {
-      var lhsResult = checkAllLhs();
+      var lhs = checkAllLhs();
 
-      if (lhsResult.noneMatch(r -> r.hasError)) {
-        var classes = PatClassifier.classify(lhsResult.view().map(LhsResult::clause),
-          // TODO: max(lhsResult.signature.telescope by size)
+      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);
-          // refinePatterns(lhsResults, usages, classes);
+          // refinePatterns(lhs, usages, classes);
         }
       }
 
-      lhsResult = lhsResult.map(cl -> new LhsResult(cl.localCtx, cl.newSignature, cl.allBinds,
+      lhs = lhs.map(cl -> new LhsResult(cl.localCtx, cl.newSignature, cl.allBinds,
         cl.freePats.map(TypeEraser::erase),
         cl.paramSubst, cl.asSubst, cl.clause, cl.hasError));
-      return parent.checkAllRhs(teleVars, lhsResult);
+      return parent.checkAllRhs(teleVars, lhs);
     }
 
     public @NotNull ImmutableSeq<LhsResult> checkAllLhs() {
@@ -125,10 +126,10 @@ public record Worker(
   // region tycking
 
   public @NotNull ImmutableSeq<LhsResult> checkAllLhs(
-    @NotNull Supplier<SignatureIterator> sigIter,
+    @NotNull Supplier<SignatureIterator> sigIterFactory,
     @NotNull SeqView<Pattern.Clause> clauses, boolean isFn
   ) {
-    return clauses.map(c -> checkLhs(sigIter.get(), c, isFn)).toImmutableSeq();
+    return clauses.map(c -> checkLhs(sigIterFactory.get(), c, isFn)).toImmutableSeq();
   }
 
   public @NotNull TyckResult checkAllRhs(

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

@@ -30,8 +30,8 @@
 import org.aya.tyck.TyckState;
 import org.aya.tyck.ctx.LocalLet;
 import org.aya.tyck.error.PatternProblem;
-import org.aya.tyck.pat.iter.ConstPusheen;
 import org.aya.tyck.pat.iter.PatternIterator;
+import org.aya.tyck.pat.iter.Pusheenable;
 import org.aya.tyck.pat.iter.SignatureIterator;
 import org.aya.tyck.tycker.Problematic;
 import org.aya.tyck.tycker.Stateful;
@@ -381,7 +381,7 @@ private class Closer implements AutoCloseable {
     @NotNull ImmutableSeq<Arg<WithPos<Pattern>>> patterns,
     @NotNull WithPos<Pattern> outerPattern
   ) {
-    var sub = new PatternTycker(exprTycker, new SignatureIterator(telescope, new ConstPusheen<>(ErrorTerm.DUMMY), null), asSubst, nameGen);
+    var sub = new PatternTycker(exprTycker, new SignatureIterator(telescope, new Pusheenable.Const<>(ErrorTerm.DUMMY), null), asSubst, nameGen);
     var tyckResult = sub.tyck(new PatternIterator(patterns), outerPattern);
 
     hasError = hasError || sub.hasError;

base/src/main/java/org/aya/tyck/pat/iter/PatternIterator.java

@@ -13,7 +13,7 @@
 
 public class PatternIterator extends PusheenIterator<Arg<WithPos<Pattern>>, WithPos<Expr>> {
   public static final @NotNull Pusheenable<Arg<WithPos<Pattern>>, WithPos<Expr>> DUMMY =
-    new ConstPusheen<>(WithPos.dummy(new Expr.Error(Doc.empty())));
+    new Const<>(WithPos.dummy(new Expr.Error(Doc.empty())));
 
   public PatternIterator(@NotNull ImmutableSeq<Arg<WithPos<Pattern>>> patterns) {
     super(patterns.iterator(), DUMMY);

base/src/main/java/org/aya/tyck/pat/iter/Pusheenable.java

@@ -2,6 +2,7 @@
 // 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.iter;
 
+import org.aya.util.error.Panic;
 import org.jetbrains.annotations.NotNull;
 
 import java.util.Iterator;
@@ -11,4 +12,10 @@
 public interface Pusheenable<T, R> extends Iterator<T> {
   @NotNull T peek();
   @NotNull R body();
+  record Const<T, R>(@NotNull R body) implements Pusheenable<T, R> {
+    @Override public @NotNull T peek() { return Panic.unreachable(); }
+    @Override public @NotNull R body() { return body; }
+    @Override public boolean hasNext() { return false; }
+    @Override public T next() { return Panic.unreachable(); }
+  }
 }

base/src/main/java/org/aya/tyck/pat/iter/SignatureIterator.java

@@ -19,7 +19,7 @@
 public class SignatureIterator extends PusheenIterator<Param, Term> {
   public static @NotNull Pusheenable<Param, @NotNull Term> makePusheen(@NotNull DepTypeTerm.UnpiRaw unpi) {
     if (unpi.params().isEmpty()) {
-      return new ConstPusheen<>(unpi.body());
+      return new Const<>(unpi.body());
     } else {
       return new PiPusheen(unpi);
 
@@ -40,7 +40,7 @@ public class SignatureIterator extends PusheenIterator<Param, Term> {
         .map(elims::contains)
         .collect(ImmutableBooleanSeq.factory());
 
-      return new SignatureIterator(telescope, new ConstPusheen<>(unpi.makePi()), bElims);
+      return new SignatureIterator(telescope, new Const<>(unpi.makePi()), bElims);
     }
   }
 

syntax/src/main/java/org/aya/syntax/concrete/stmt/decl/FnBody.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.syntax.concrete.stmt.decl;
 
@@ -9,6 +9,7 @@
 import org.aya.util.error.PosedConsumer;
 import org.aya.util.error.PosedUnaryOperator;
 import org.aya.util.error.WithPos;
+import org.jetbrains.annotations.Contract;
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 
@@ -35,17 +36,14 @@ public BlockBody(
       this(new MatchBody<>(clauses, rawElims));
     }
 
-    public @NotNull ImmutableSeq<Pattern.Clause> clauses() {
+    @Contract(pure = true) public @NotNull ImmutableSeq<Pattern.Clause> clauses() {
       return inner.clauses;
     }
 
-    public @Nullable ImmutableSeq<LocalVar> elims() {
+    @Contract(pure = true) public @Nullable ImmutableSeq<LocalVar> elims() {
       return inner.elims();
     }
-
-    public @NotNull ImmutableSeq<WithPos<String>> rawElims() {
-      return inner.rawElims;
-    }
+    public @NotNull ImmutableSeq<WithPos<String>> rawElims() { return inner.rawElims; }
 
     public @NotNull BlockBody map(@NotNull UnaryOperator<Pattern.Clause> f) {
       return new BlockBody(inner.descent(f));