From b10d24ecc808f87327d5542c1413cdb00f258a6b Mon Sep 17 00:00:00 2001
From: ice1000 <ice1000kotlin@foxmail.com>
Date: Wed, 19 Jun 2024 19:02:28 -0400
Subject: [PATCH 01/33] class: primitive implementation of
 `TakeMembers::result`

---
 .../main/java/org/aya/tyck/ExprTycker.java    |  4 +--
 .../java/org/aya/tyck/tycker/AppTycker.java   | 35 ++++++++++++++-----
 base/src/test/java/org/aya/tyck/TyckTest.java |  7 ++--
 3 files changed, 32 insertions(+), 14 deletions(-)

diff --git a/base/src/main/java/org/aya/tyck/ExprTycker.java b/base/src/main/java/org/aya/tyck/ExprTycker.java
index addb327ae..95836a632 100644
--- a/base/src/main/java/org/aya/tyck/ExprTycker.java
+++ b/base/src/main/java/org/aya/tyck/ExprTycker.java
@@ -324,9 +324,9 @@ yield subscoped(param.ref(), wellParam, () ->
       case LocalVar ref when localLet.contains(ref) -> generateApplication(args, localLet.get(ref)).lift(lift);
       case LocalVar lVar -> generateApplication(args,
         new Jdg.Default(new FreeTerm(lVar), localCtx().get(lVar))).lift(lift);
-      case CompiledVar(var content) -> new AppTycker<>(state, sourcePos, args.size(), lift, (params, k) ->
+      case CompiledVar(var content) -> new AppTycker<>(this, sourcePos, args.size(), lift, (params, k) ->
         computeArgs(sourcePos, args, params, k)).checkCompiledApplication(content);
-      case DefVar<?, ?> defVar -> new AppTycker<>(state, sourcePos, args.size(), lift, (params, k) ->
+      case DefVar<?, ?> defVar -> new AppTycker<>(this, sourcePos, args.size(), lift, (params, k) ->
         computeArgs(sourcePos, args, params, k)).checkDefApplication(defVar);
       default -> throw new UnsupportedOperationException("TODO");
     };
diff --git a/base/src/main/java/org/aya/tyck/tycker/AppTycker.java b/base/src/main/java/org/aya/tyck/tycker/AppTycker.java
index 9a192e8a9..65bdc2892 100644
--- a/base/src/main/java/org/aya/tyck/tycker/AppTycker.java
+++ b/base/src/main/java/org/aya/tyck/tycker/AppTycker.java
@@ -15,6 +15,8 @@
 import org.aya.syntax.core.def.*;
 import org.aya.syntax.core.repr.AyaShape;
 import org.aya.syntax.core.term.FreeTerm;
+import org.aya.syntax.core.term.SigmaTerm;
+import org.aya.syntax.core.term.SortTerm;
 import org.aya.syntax.core.term.Term;
 import org.aya.syntax.core.term.call.*;
 import org.aya.syntax.ref.DefVar;
@@ -22,6 +24,7 @@
 import org.aya.syntax.telescope.AbstractTele;
 import org.aya.tyck.Jdg;
 import org.aya.tyck.TyckState;
+import org.aya.unify.Synthesizer;
 import org.aya.util.error.Panic;
 import org.aya.util.error.SourcePos;
 import org.jetbrains.annotations.NotNull;
@@ -30,7 +33,7 @@
 import java.util.function.Function;
 
 public record AppTycker<Ex extends Exception>(
-  @NotNull TyckState state, @NotNull SourcePos pos,
+  @NotNull TyckState state, @NotNull AbstractTycker tycker, @NotNull SourcePos pos,
   int argsCount, int lift, @NotNull Factory<Ex> makeArgs
 ) {
   /**
@@ -48,6 +51,13 @@ public interface Factory<Ex extends Exception> extends
     CheckedBiFunction<AbstractTele, Function<Term[], Jdg>, Jdg, Ex> {
   }
 
+  public AppTycker(
+    @NotNull AbstractTycker tycker, @NotNull SourcePos pos,
+    int argsCount, int lift, @NotNull Factory<Ex> makeArgs
+  ) {
+    this(tycker.state, tycker, pos, argsCount, lift, makeArgs);
+  }
+
   public @NotNull Jdg checkCompiledApplication(@NotNull AbstractTele def) throws Ex {
     return switch (def) {
       case JitFn fn -> {
@@ -137,8 +147,8 @@ public interface Factory<Ex extends Exception> extends
   }
 
   private @NotNull Jdg checkClassCall(@NotNull ClassDefLike clazz) throws Ex {
-    var appliedParams = ofClassMembers(clazz, argsCount).lift(lift);
     var self = LocalVar.generate("self");
+    var appliedParams = ofClassMembers(self, clazz, argsCount).lift(lift);
     state.classThis.push(self);
     var result = makeArgs.applyChecked(appliedParams, args -> new Jdg.Default(
       new ClassCall(clazz, 0, ImmutableArray.from(args).map(x -> x.bind(self))),
@@ -160,13 +170,17 @@ public interface Factory<Ex extends Exception> extends
     });
   }
 
-  static @NotNull AbstractTele ofClassMembers(@NotNull ClassDefLike def, int memberCount) {
+  private @NotNull AbstractTele ofClassMembers(@NotNull LocalVar self, @NotNull ClassDefLike def, int memberCount) {
+    var synthesizer = new Synthesizer(tycker);
     return switch (def) {
-      case ClassDef.Delegate delegate -> new TakeMembers(delegate.core(), memberCount);
+      case ClassDef.Delegate delegate -> new TakeMembers(self, delegate.core(), memberCount, synthesizer);
     };
   }
 
-  record TakeMembers(@NotNull ClassDef clazz, @Override int telescopeSize) implements AbstractTele {
+  record TakeMembers(
+    @NotNull LocalVar self, @NotNull ClassDef clazz,
+    @Override int telescopeSize, @NotNull Synthesizer synthesizer
+  ) implements AbstractTele {
     @Override public boolean telescopeLicit(int i) { return true; }
     @Override public @NotNull String telescopeName(int i) {
       assert i < telescopeSize;
@@ -175,18 +189,21 @@ record TakeMembers(@NotNull ClassDef clazz, @Override int telescopeSize) impleme
 
     // class Foo
     // | foo : A
-    // | + : A -> A -> A
+    // | infix + : A -> A -> A
     // | bar : Fn (x : Foo A) -> (x.foo) self.+ (self.foo)
     //                  instantiate these!   ^       ^
     @Override public @NotNull Term telescope(int i, Seq<Term> teleArgs) {
       // teleArgs are former members
       assert i < telescopeSize;
       var member = clazz.members().get(i);
-      return TyckDef.defSignature(member.ref()).makePi(Seq.of(new FreeTerm(clazz.ref().concrete.self)));
+      return TyckDef.defSignature(member.ref()).makePi(Seq.of(new FreeTerm(self)));
     }
     @Override public @NotNull Term result(Seq<Term> teleArgs) {
-      // Use SigmaTerm::lub
-      throw new UnsupportedOperationException("TODO");
+      return clazz.members().view()
+        .drop(telescopeSize)
+        .map(member -> TyckDef.defSignature(member.ref()).makePi(Seq.of(new FreeTerm(self))))
+        .map(ty -> (SortTerm) synthesizer.synth(ty))
+        .reduce(SigmaTerm::lub);
     }
     @Override public @NotNull SeqView<String> namesView() {
       return clazz.members().sliceView(0, telescopeSize).map(i -> i.ref().name());
diff --git a/base/src/test/java/org/aya/tyck/TyckTest.java b/base/src/test/java/org/aya/tyck/TyckTest.java
index bc92b2188..1e74c5624 100644
--- a/base/src/test/java/org/aya/tyck/TyckTest.java
+++ b/base/src/test/java/org/aya/tyck/TyckTest.java
@@ -154,10 +154,11 @@ open inductive Phantom Nat Nat (A : Type) | mk A
       def infix = (a b : A) => Path (\\i => A) a b
       
       class Monoid
-      | carrier : Type
+      | classifying carrier : Type
       | unit : carrier
-      | op : carrier -> carrier -> carrier
-      | idl (x : carrier) : op unit x = x
+      | infix * : carrier -> carrier -> carrier
+        tighter =
+      | idl (x : carrier) : unit * x = x
       """).defs.isNotEmpty());
   }
 

From 22673c562bfe7547905de8d76ec324f8006061ba Mon Sep 17 00:00:00 2001
From: HoshinoTented <hoshinotented@qq.com>
Date: Fri, 21 Jun 2024 12:29:08 +0800
Subject: [PATCH 02/33] expr: new

---
 .../java/org/aya/syntax/concrete/Expr.java    | 42 +++++++++++++++++++
 1 file changed, 42 insertions(+)

diff --git a/syntax/src/main/java/org/aya/syntax/concrete/Expr.java b/syntax/src/main/java/org/aya/syntax/concrete/Expr.java
index f1f907660..dd80e9d3e 100644
--- a/syntax/src/main/java/org/aya/syntax/concrete/Expr.java
+++ b/syntax/src/main/java/org/aya/syntax/concrete/Expr.java
@@ -318,6 +318,48 @@ record LitString(@NotNull String string) implements Expr {
     @Override public void forEach(@NotNull PosedConsumer<Expr> f) { }
   }
 
+  record New(
+    @NotNull WithPos<Expr> struct,
+    @NotNull ImmutableSeq<Field<Expr>> fields
+  ) implements Expr {
+    public @NotNull Expr.New update(@NotNull WithPos<Expr> struct, @NotNull ImmutableSeq<Field<Expr>> fields) {
+      return struct == struct() && fields.sameElements(fields(), true) ? this : new New(struct, fields);
+    }
+
+    @Override public @NotNull Expr.New descent(@NotNull PosedUnaryOperator<@NotNull Expr> f) {
+      return update(struct.descent(f), fields.map(field -> field.descent(f)));
+    }
+
+    @Override
+    public void forEach(@NotNull PosedConsumer<@NotNull Expr> f) {
+      f.accept(struct);
+      fields.forEach(field -> field.forEach(f));
+    }
+  }
+
+  /**
+   * @param resolvedField will be modified during tycking for LSP to function properly.
+   */
+  record Field<Term extends AyaDocile>(
+    @NotNull SourcePos sourcePos,
+    @NotNull WithPos<String> name,
+    @NotNull ImmutableSeq<WithPos<LocalVar>> bindings,
+    @NotNull WithPos<Term> body,
+    @ForLSP @NotNull MutableValue<AnyVar> resolvedField
+  ) {
+    public @NotNull Field<Term> update(@NotNull WithPos<Term> body) {
+      return body == body() ? this : new Field<Term>(sourcePos, name, bindings, body, resolvedField);
+    }
+
+    public @NotNull Field<Term> descent(@NotNull PosedUnaryOperator<@NotNull Term> f) {
+      return update(body.descent(f));
+    }
+
+    public void forEach(@NotNull PosedConsumer<@NotNull Term> f) {
+      f.accept(body);
+    }
+  }
+
   record Idiom(
     @NotNull IdiomNames names,
     @NotNull ImmutableSeq<WithPos<Expr>> barredApps

From 6984db77b2b1b296f666195b55d4c171857d7e68 Mon Sep 17 00:00:00 2001
From: HoshinoTented <hoshinotented@qq.com>
Date: Fri, 21 Jun 2024 16:33:12 +0800
Subject: [PATCH 03/33] term: new, but we need to impl
 TermComparator/Synthesizer

---
 .../java/org/aya/prettier/CorePrettier.java   |  1 +
 .../main/java/org/aya/prettier/Tokens.java    |  1 +
 .../java/org/aya/syntax/concrete/Expr.java    | 82 +++++++++----------
 .../org/aya/syntax/core/term/NewTerm.java     | 30 +++++++
 .../aya/syntax/core/term/call/ClassCall.java  |  1 +
 .../syntax/core/term/marker/StableWHNF.java   |  2 +-
 6 files changed, 75 insertions(+), 42 deletions(-)
 create mode 100644 syntax/src/main/java/org/aya/syntax/core/term/NewTerm.java

diff --git a/syntax/src/main/java/org/aya/prettier/CorePrettier.java b/syntax/src/main/java/org/aya/prettier/CorePrettier.java
index e9c539e60..c40420765 100644
--- a/syntax/src/main/java/org/aya/prettier/CorePrettier.java
+++ b/syntax/src/main/java/org/aya/prettier/CorePrettier.java
@@ -199,6 +199,7 @@ case ErrorTerm(var desc, var isReallyError) -> {
       }
       case ClassCall classCall ->
         visitCoreCalls(classCall.ref(), classCall.args().map(x -> x.apply(SELF)), outer, true);
+      case NewTerm newTerm -> Doc.sep(KW_NEW, term(Outer.Free, newTerm.inner()));
       case DataCall dataCall -> visitCoreCalls(dataCall.ref(), dataCall.args(), outer, optionImplicit());
       case StringTerm(var str) -> Doc.plain("\"" + StringUtil.escapeStringCharacters(str) + "\"");
       case PAppTerm app -> visitCalls(null, term(Outer.AppHead, app.fun()),
diff --git a/syntax/src/main/java/org/aya/prettier/Tokens.java b/syntax/src/main/java/org/aya/prettier/Tokens.java
index 449a5ba08..0c0262026 100644
--- a/syntax/src/main/java/org/aya/prettier/Tokens.java
+++ b/syntax/src/main/java/org/aya/prettier/Tokens.java
@@ -39,6 +39,7 @@ private Tokens() {
   public static final Doc KW_DEF = Doc.styled(KEYWORD, "def");
   public static final Doc KW_DATA = Doc.styled(KEYWORD, "inductive");
   public static final Doc KW_CLASS = Doc.styled(KEYWORD, "class");
+  public static final Doc KW_NEW = Doc.styled(KEYWORD, "new");
   public static final Doc PAT_ABSURD = Doc.styled(KEYWORD, "()");
   public static final Doc KW_TIGHTER = Doc.styled(KEYWORD, "tighter");
   public static final Doc KW_LOOSER = Doc.styled(KEYWORD, "looser");
diff --git a/syntax/src/main/java/org/aya/syntax/concrete/Expr.java b/syntax/src/main/java/org/aya/syntax/concrete/Expr.java
index dd80e9d3e..9638549e6 100644
--- a/syntax/src/main/java/org/aya/syntax/concrete/Expr.java
+++ b/syntax/src/main/java/org/aya/syntax/concrete/Expr.java
@@ -318,47 +318,47 @@ record LitString(@NotNull String string) implements Expr {
     @Override public void forEach(@NotNull PosedConsumer<Expr> f) { }
   }
 
-  record New(
-    @NotNull WithPos<Expr> struct,
-    @NotNull ImmutableSeq<Field<Expr>> fields
-  ) implements Expr {
-    public @NotNull Expr.New update(@NotNull WithPos<Expr> struct, @NotNull ImmutableSeq<Field<Expr>> fields) {
-      return struct == struct() && fields.sameElements(fields(), true) ? this : new New(struct, fields);
-    }
-
-    @Override public @NotNull Expr.New descent(@NotNull PosedUnaryOperator<@NotNull Expr> f) {
-      return update(struct.descent(f), fields.map(field -> field.descent(f)));
-    }
-
-    @Override
-    public void forEach(@NotNull PosedConsumer<@NotNull Expr> f) {
-      f.accept(struct);
-      fields.forEach(field -> field.forEach(f));
-    }
-  }
-
-  /**
-   * @param resolvedField will be modified during tycking for LSP to function properly.
-   */
-  record Field<Term extends AyaDocile>(
-    @NotNull SourcePos sourcePos,
-    @NotNull WithPos<String> name,
-    @NotNull ImmutableSeq<WithPos<LocalVar>> bindings,
-    @NotNull WithPos<Term> body,
-    @ForLSP @NotNull MutableValue<AnyVar> resolvedField
-  ) {
-    public @NotNull Field<Term> update(@NotNull WithPos<Term> body) {
-      return body == body() ? this : new Field<Term>(sourcePos, name, bindings, body, resolvedField);
-    }
-
-    public @NotNull Field<Term> descent(@NotNull PosedUnaryOperator<@NotNull Term> f) {
-      return update(body.descent(f));
-    }
-
-    public void forEach(@NotNull PosedConsumer<@NotNull Term> f) {
-      f.accept(body);
-    }
-  }
+  // record New(
+  //   @NotNull WithPos<Expr> struct,
+  //   @NotNull ImmutableSeq<Field<Expr>> fields
+  // ) implements Expr {
+  //   public @NotNull Expr.New update(@NotNull WithPos<Expr> struct, @NotNull ImmutableSeq<Field<Expr>> fields) {
+  //     return struct == struct() && fields.sameElements(fields(), true) ? this : new New(struct, fields);
+  //   }
+  //
+  //   @Override public @NotNull Expr.New descent(@NotNull PosedUnaryOperator<@NotNull Expr> f) {
+  //     return update(struct.descent(f), fields.map(field -> field.descent(f)));
+  //   }
+  //
+  //   @Override
+  //   public void forEach(@NotNull PosedConsumer<@NotNull Expr> f) {
+  //     f.accept(struct);
+  //     fields.forEach(field -> field.forEach(f));
+  //   }
+  // }
+  //
+  // /**
+  //  * @param resolvedField will be modified during tycking for LSP to function properly.
+  //  */
+  // record Field<Term extends AyaDocile>(
+  //   @NotNull SourcePos sourcePos,
+  //   @NotNull WithPos<String> name,
+  //   @NotNull ImmutableSeq<WithPos<LocalVar>> bindings,
+  //   @NotNull WithPos<Term> body,
+  //   @ForLSP @NotNull MutableValue<AnyVar> resolvedField
+  // ) {
+  //   public @NotNull Field<Term> update(@NotNull WithPos<Term> body) {
+  //     return body == body() ? this : new Field<Term>(sourcePos, name, bindings, body, resolvedField);
+  //   }
+  //
+  //   public @NotNull Field<Term> descent(@NotNull PosedUnaryOperator<@NotNull Term> f) {
+  //     return update(body.descent(f));
+  //   }
+  //
+  //   public void forEach(@NotNull PosedConsumer<@NotNull Term> f) {
+  //     f.accept(body);
+  //   }
+  // }
 
   record Idiom(
     @NotNull IdiomNames names,
diff --git a/syntax/src/main/java/org/aya/syntax/core/term/NewTerm.java b/syntax/src/main/java/org/aya/syntax/core/term/NewTerm.java
new file mode 100644
index 000000000..15165ebb1
--- /dev/null
+++ b/syntax/src/main/java/org/aya/syntax/core/term/NewTerm.java
@@ -0,0 +1,30 @@
+// Copyright (c) 2020-2024 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.term;
+
+import kala.function.IndexedFunction;
+import org.aya.syntax.core.term.call.ClassCall;
+import org.aya.syntax.core.term.marker.StableWHNF;
+import org.jetbrains.annotations.NotNull;
+
+/**
+ * Term that constructs an instance of some {@link ClassCall}.
+ * NewTerm has the same structure as a fully applied {@link ClassCall},
+ * as it has only one instance.
+ */
+public record NewTerm(@NotNull ClassCall inner) implements StableWHNF {
+  public NewTerm {
+    assert inner.args().size() == inner.ref().members().size();
+  }
+
+  public @NotNull NewTerm update(@NotNull ClassCall classCall) {
+    if (classCall == inner) return this;
+    return new NewTerm(classCall);
+  }
+
+  @Override
+  public @NotNull Term descent(@NotNull IndexedFunction<Term, Term> f) {
+    // not `f.apply(0, inner)`, since the `ClassCall` is considered to be flatten
+    return inner.descent(f);
+  }
+}
diff --git a/syntax/src/main/java/org/aya/syntax/core/term/call/ClassCall.java b/syntax/src/main/java/org/aya/syntax/core/term/call/ClassCall.java
index 27035517e..db9ec8d36 100644
--- a/syntax/src/main/java/org/aya/syntax/core/term/call/ClassCall.java
+++ b/syntax/src/main/java/org/aya/syntax/core/term/call/ClassCall.java
@@ -6,6 +6,7 @@
 import kala.function.IndexedFunction;
 import org.aya.syntax.core.Closure;
 import org.aya.syntax.core.def.ClassDefLike;
+import org.aya.syntax.core.term.NewTerm;
 import org.aya.syntax.core.term.Term;
 import org.aya.syntax.core.term.marker.Formation;
 import org.aya.syntax.core.term.marker.StableWHNF;
diff --git a/syntax/src/main/java/org/aya/syntax/core/term/marker/StableWHNF.java b/syntax/src/main/java/org/aya/syntax/core/term/marker/StableWHNF.java
index 2069082f5..d96968e7e 100644
--- a/syntax/src/main/java/org/aya/syntax/core/term/marker/StableWHNF.java
+++ b/syntax/src/main/java/org/aya/syntax/core/term/marker/StableWHNF.java
@@ -16,5 +16,5 @@
  * after a substitution (this usually happens under face restrictions (aka cofibrations)).
  */
 public sealed interface StableWHNF extends Term
-  permits ErrorTerm, LamTerm, PiTerm, SigmaTerm, SortTerm, TupTerm, ClassCall, DataCall, IntegerTerm, ListTerm, StringTerm, DimTerm, EqTerm {
+  permits ErrorTerm, LamTerm, NewTerm, PiTerm, SigmaTerm, SortTerm, TupTerm, ClassCall, DataCall, IntegerTerm, ListTerm, StringTerm, DimTerm, EqTerm {
 }

From 2bd64aafbd6b72862c6b082cfc0afda3d7596b2b Mon Sep 17 00:00:00 2001
From: HoshinoTented <hoshinotented@qq.com>
Date: Fri, 21 Jun 2024 18:28:01 +0800
Subject: [PATCH 04/33] tyck: new

---
 .../main/java/org/aya/tyck/ExprTycker.java    | 14 +++++
 .../main/java/org/aya/unify/Synthesizer.java  |  1 +
 .../java/org/aya/syntax/concrete/Expr.java    | 57 ++++++-------------
 3 files changed, 31 insertions(+), 41 deletions(-)

diff --git a/base/src/main/java/org/aya/tyck/ExprTycker.java b/base/src/main/java/org/aya/tyck/ExprTycker.java
index 95836a632..dc439ca2c 100644
--- a/base/src/main/java/org/aya/tyck/ExprTycker.java
+++ b/base/src/main/java/org/aya/tyck/ExprTycker.java
@@ -297,6 +297,20 @@ yield subscoped(param.ref(), wellParam, () ->
         var type = new DataCall(def, 0, ImmutableSeq.of(elementTy));
         yield new Jdg.Default(new ListTerm(results, match.recog(), type), type);
       }
+      case Expr.New neutron -> {
+        var wellTyped = synthesize(neutron.classCall());
+        if (!(wellTyped.wellTyped() instanceof ClassCall call)) {
+          // TODO
+          throw new UnsupportedOperationException("TODO");
+        }
+
+        // check whether the call is fully applied
+        if (call.args().size() != call.ref().members().size()) {
+          throw new UnsupportedOperationException("TODO");
+        }
+
+        yield new Jdg.Default(new NewTerm(call), call);
+      }
       case Expr.Unresolved _ -> Panic.unreachable();
       default -> fail(expr.data(), new NoRuleError(expr, null));
     };
diff --git a/base/src/main/java/org/aya/unify/Synthesizer.java b/base/src/main/java/org/aya/unify/Synthesizer.java
index f2cde38dc..c72ca92b5 100644
--- a/base/src/main/java/org/aya/unify/Synthesizer.java
+++ b/base/src/main/java/org/aya/unify/Synthesizer.java
@@ -136,6 +136,7 @@ case MetaCall(var ref, var args) when ref.req() instanceof MetaVar.OfType(var ty
       case MetaLitTerm mlt -> mlt.type();
       case StringTerm str -> state().primFactory.getCall(PrimDef.ID.STRING);
       case ClassCall classCall -> throw new UnsupportedOperationException("TODO");
+      case NewTerm newTerm -> newTerm.inner();
     };
   }
 
diff --git a/syntax/src/main/java/org/aya/syntax/concrete/Expr.java b/syntax/src/main/java/org/aya/syntax/concrete/Expr.java
index 9638549e6..cda6060ea 100644
--- a/syntax/src/main/java/org/aya/syntax/concrete/Expr.java
+++ b/syntax/src/main/java/org/aya/syntax/concrete/Expr.java
@@ -318,47 +318,22 @@ record LitString(@NotNull String string) implements Expr {
     @Override public void forEach(@NotNull PosedConsumer<Expr> f) { }
   }
 
-  // record New(
-  //   @NotNull WithPos<Expr> struct,
-  //   @NotNull ImmutableSeq<Field<Expr>> fields
-  // ) implements Expr {
-  //   public @NotNull Expr.New update(@NotNull WithPos<Expr> struct, @NotNull ImmutableSeq<Field<Expr>> fields) {
-  //     return struct == struct() && fields.sameElements(fields(), true) ? this : new New(struct, fields);
-  //   }
-  //
-  //   @Override public @NotNull Expr.New descent(@NotNull PosedUnaryOperator<@NotNull Expr> f) {
-  //     return update(struct.descent(f), fields.map(field -> field.descent(f)));
-  //   }
-  //
-  //   @Override
-  //   public void forEach(@NotNull PosedConsumer<@NotNull Expr> f) {
-  //     f.accept(struct);
-  //     fields.forEach(field -> field.forEach(f));
-  //   }
-  // }
-  //
-  // /**
-  //  * @param resolvedField will be modified during tycking for LSP to function properly.
-  //  */
-  // record Field<Term extends AyaDocile>(
-  //   @NotNull SourcePos sourcePos,
-  //   @NotNull WithPos<String> name,
-  //   @NotNull ImmutableSeq<WithPos<LocalVar>> bindings,
-  //   @NotNull WithPos<Term> body,
-  //   @ForLSP @NotNull MutableValue<AnyVar> resolvedField
-  // ) {
-  //   public @NotNull Field<Term> update(@NotNull WithPos<Term> body) {
-  //     return body == body() ? this : new Field<Term>(sourcePos, name, bindings, body, resolvedField);
-  //   }
-  //
-  //   public @NotNull Field<Term> descent(@NotNull PosedUnaryOperator<@NotNull Term> f) {
-  //     return update(body.descent(f));
-  //   }
-  //
-  //   public void forEach(@NotNull PosedConsumer<@NotNull Term> f) {
-  //     f.accept(body);
-  //   }
-  // }
+  record New(
+    @NotNull WithPos<Expr> classCall
+  ) implements Expr {
+    public @NotNull Expr.New update(@NotNull WithPos<Expr> classCall) {
+      return classCall == classCall() ? this : new New(classCall);
+    }
+
+    @Override public @NotNull Expr.New descent(@NotNull PosedUnaryOperator<@NotNull Expr> f) {
+      return update(classCall.descent(f));
+    }
+
+    @Override
+    public void forEach(@NotNull PosedConsumer<@NotNull Expr> f) {
+      f.accept(classCall);
+    }
+  }
 
   record Idiom(
     @NotNull IdiomNames names,

From 7cc7e35c1e6432a75116aaecc06c3760bbcc93e6 Mon Sep 17 00:00:00 2001
From: HoshinoTented <hoshinotented@qq.com>
Date: Sun, 30 Jun 2024 19:26:31 +0800
Subject: [PATCH 05/33] class: try this

---
 .../main/java/org/aya/tyck/ExprTycker.java    | 25 +++++++++++--
 .../aya/syntax/core/term/ClassCastTerm.java   | 36 +++++++++++++++++++
 .../java/org/aya/syntax/core/term/Term.java   |  2 +-
 tools/src/main/java/org/aya/util/MapUtil.java | 21 +++++++++++
 4 files changed, 81 insertions(+), 3 deletions(-)
 create mode 100644 syntax/src/main/java/org/aya/syntax/core/term/ClassCastTerm.java
 create mode 100644 tools/src/main/java/org/aya/util/MapUtil.java

diff --git a/base/src/main/java/org/aya/tyck/ExprTycker.java b/base/src/main/java/org/aya/tyck/ExprTycker.java
index dc439ca2c..7215e7d3c 100644
--- a/base/src/main/java/org/aya/tyck/ExprTycker.java
+++ b/base/src/main/java/org/aya/tyck/ExprTycker.java
@@ -2,9 +2,11 @@
 // 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.immutable.ImmutableMap;
 import kala.collection.immutable.ImmutableSeq;
 import kala.collection.immutable.ImmutableTreeSeq;
 import kala.collection.mutable.MutableList;
+import kala.collection.mutable.MutableMap;
 import kala.collection.mutable.MutableStack;
 import kala.collection.mutable.MutableTreeSet;
 import kala.control.Result;
@@ -13,6 +15,7 @@
 import org.aya.syntax.concrete.Expr;
 import org.aya.syntax.core.Closure;
 import org.aya.syntax.core.def.DataDefLike;
+import org.aya.syntax.core.def.MemberDefLike;
 import org.aya.syntax.core.def.PrimDef;
 import org.aya.syntax.core.repr.AyaShape;
 import org.aya.syntax.core.term.*;
@@ -132,6 +135,11 @@ case PiTerm(var dom, var cod) -> {
     };
   }
 
+  /**
+   * @param type   expected type
+   * @param result wellTyped + actual type from synthesize
+   * @param expr   original expr, used for error reporting
+   */
   private @NotNull Jdg inheritFallbackUnify(@NotNull Term type, @NotNull Jdg result, @NotNull WithPos<Expr> expr) {
     type = whnf(type);
     var resultType = result.type();
@@ -152,8 +160,21 @@ case PiTerm(var dom, var cod) -> {
           addWithTerm(with, expr.sourcePos(), eq);
         return new Jdg.Default(new LamTerm(closure), eq);
       }
-    }
-    if (unifyTyReported(type, resultType, expr)) return result;
+    } else if (type instanceof ClassCall clazz) {
+      resultType = whnf(resultType);
+      if (resultType instanceof ClassCall resultClazz) {
+        if (unifyTyReported(clazz, resultClazz, expr)) {
+          var restr = resultClazz.args()
+            .drop(clazz.args().size());
+          var fields = clazz.ref().members()
+            .sliceView(clazz.args().size(), resultClazz.args().size());
+          ;
+          var extra = ImmutableMap.from(fields.zipView(restr));
+          return new Jdg.Default(new ClassCastTerm(result.wellTyped(), extra), type);
+        }
+      }
+    } else if (unifyTyReported(type, resultType, expr)) return result;
+
     return new Jdg.Default(new ErrorTerm(result.wellTyped()), type);
   }
 
diff --git a/syntax/src/main/java/org/aya/syntax/core/term/ClassCastTerm.java b/syntax/src/main/java/org/aya/syntax/core/term/ClassCastTerm.java
new file mode 100644
index 000000000..0ce953c5e
--- /dev/null
+++ b/syntax/src/main/java/org/aya/syntax/core/term/ClassCastTerm.java
@@ -0,0 +1,36 @@
+// Copyright (c) 2020-2024 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.term;
+
+import kala.collection.immutable.ImmutableMap;
+import kala.collection.mutable.MutableMap;
+import kala.function.IndexedFunction;
+import org.aya.syntax.core.Closure;
+import org.aya.syntax.core.def.MemberDefLike;
+import org.aya.util.MapUtil;
+import org.jetbrains.annotations.NotNull;
+
+/**
+ * This term is used for subtyping of class, a term {@code x : SomeClass (foo := 114514)} is treated an
+ * instance of {@code SomeClass} in user side. In core side, we use {@code cast x (foo := 114514) : SomeClass}
+ * to make {@code x} an instance of {@code SomeClass}, it also store the type information in expression
+ * so that the {@link org.aya.syntax.core.term.call.MemberCall} can access them without synthesizing.
+ */
+public record ClassCastTerm(
+  @NotNull Term subterm,
+  @NotNull ImmutableMap<MemberDefLike, Closure> restriction
+) implements Term {
+  public @NotNull ClassCastTerm update(@NotNull Term subterm, @NotNull ImmutableMap<MemberDefLike, Closure> restriction) {
+    return this.subterm == subterm
+      && MapUtil.sameElements(this.restriction, restriction)
+      ? this
+      : new ClassCastTerm(subterm, restriction);
+  }
+
+  @Override
+  public @NotNull Term descent(@NotNull IndexedFunction<Term, Term> f) {
+    return update(f.apply(0, subterm), ImmutableMap.from(MutableMap.from(restriction).edit()
+      .replaceAll((_, v) -> v.descent(f))
+      .done()));
+  }
+}
diff --git a/syntax/src/main/java/org/aya/syntax/core/term/Term.java b/syntax/src/main/java/org/aya/syntax/core/term/Term.java
index 0b703235e..af05cf992 100644
--- a/syntax/src/main/java/org/aya/syntax/core/term/Term.java
+++ b/syntax/src/main/java/org/aya/syntax/core/term/Term.java
@@ -28,7 +28,7 @@
 import java.util.function.UnaryOperator;
 
 public sealed interface Term extends Serializable, AyaDocile
-  permits BetaRedex, Formation, LocalTerm, StableWHNF, TyckInternal, Callable, CoeTerm {
+  permits ClassCastTerm, LocalTerm, Callable, BetaRedex, Formation, StableWHNF, TyckInternal, CoeTerm {
 
   @Override default @NotNull Doc toDoc(@NotNull PrettierOptions options) {
     return new CorePrettier(options).term(BasePrettier.Outer.Free, this);
diff --git a/tools/src/main/java/org/aya/util/MapUtil.java b/tools/src/main/java/org/aya/util/MapUtil.java
new file mode 100644
index 000000000..b8047c50e
--- /dev/null
+++ b/tools/src/main/java/org/aya/util/MapUtil.java
@@ -0,0 +1,21 @@
+// Copyright (c) 2020-2024 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;
+
+import kala.collection.immutable.ImmutableMap;
+import org.jetbrains.annotations.NotNull;
+
+public interface MapUtil {
+  static <K, V> boolean sameElements(@NotNull ImmutableMap<K, V> lhs, @NotNull ImmutableMap<K, V> rhs) {
+    if (lhs.size() != rhs.size()) return false;
+
+    var it = lhs.iterator();
+    while (it.hasNext()) {
+      var pair = it.next();
+      if (!rhs.containsKey(pair.component1())) return false;
+      if (pair.component2() != rhs.get(pair.component1())) return false;
+    }
+
+    return true;
+  }
+}

From 7a71be1f19caf702e99ca45632473b4953db4415 Mon Sep 17 00:00:00 2001
From: HoshinoTented <hoshinotented@qq.com>
Date: Sun, 30 Jun 2024 20:30:10 +0800
Subject: [PATCH 06/33] member: normalizer

---
 .../java/org/aya/normalize/Normalizer.java    |  5 ++++
 .../main/java/org/aya/tyck/ExprTycker.java    |  2 +-
 .../aya/syntax/core/term/call/ClassCall.java  |  7 +++++
 .../aya/syntax/core/term/call/MemberCall.java | 28 +++++++++++++++++++
 4 files changed, 41 insertions(+), 1 deletion(-)

diff --git a/base/src/main/java/org/aya/normalize/Normalizer.java b/base/src/main/java/org/aya/normalize/Normalizer.java
index a44418619..dd93b9e3c 100644
--- a/base/src/main/java/org/aya/normalize/Normalizer.java
+++ b/base/src/main/java/org/aya/normalize/Normalizer.java
@@ -81,6 +81,11 @@ case FnCall(var fn, int ulift, var args) -> switch (fn) {
           ? apply(fnRule.toFnCall())
           : reduceRule;
       }
+      case MemberCall memberCall -> {
+        var result = MemberCall.make(memberCall);
+        if (result != memberCall) yield apply(result);
+        yield defaultValue;
+      }
       case ConCall(var head, _) when !head.ref().hasEq() -> defaultValue;
       case ConCall call when call.conArgs().getLast() instanceof DimTerm dim ->
         call.head().ref().equality(call.args(), dim == DimTerm.I0);
diff --git a/base/src/main/java/org/aya/tyck/ExprTycker.java b/base/src/main/java/org/aya/tyck/ExprTycker.java
index 7215e7d3c..acb375462 100644
--- a/base/src/main/java/org/aya/tyck/ExprTycker.java
+++ b/base/src/main/java/org/aya/tyck/ExprTycker.java
@@ -161,6 +161,7 @@ case PiTerm(var dom, var cod) -> {
         return new Jdg.Default(new LamTerm(closure), eq);
       }
     } else if (type instanceof ClassCall clazz) {
+      // Try coercive subtyping for `SomeClass (foo := 114514)` into `SomeClass`
       resultType = whnf(resultType);
       if (resultType instanceof ClassCall resultClazz) {
         if (unifyTyReported(clazz, resultClazz, expr)) {
@@ -168,7 +169,6 @@ case PiTerm(var dom, var cod) -> {
             .drop(clazz.args().size());
           var fields = clazz.ref().members()
             .sliceView(clazz.args().size(), resultClazz.args().size());
-          ;
           var extra = ImmutableMap.from(fields.zipView(restr));
           return new Jdg.Default(new ClassCastTerm(result.wellTyped(), extra), type);
         }
diff --git a/syntax/src/main/java/org/aya/syntax/core/term/call/ClassCall.java b/syntax/src/main/java/org/aya/syntax/core/term/call/ClassCall.java
index db9ec8d36..2c2cbd9e2 100644
--- a/syntax/src/main/java/org/aya/syntax/core/term/call/ClassCall.java
+++ b/syntax/src/main/java/org/aya/syntax/core/term/call/ClassCall.java
@@ -6,11 +6,13 @@
 import kala.function.IndexedFunction;
 import org.aya.syntax.core.Closure;
 import org.aya.syntax.core.def.ClassDefLike;
+import org.aya.syntax.core.def.MemberDefLike;
 import org.aya.syntax.core.term.NewTerm;
 import org.aya.syntax.core.term.Term;
 import org.aya.syntax.core.term.marker.Formation;
 import org.aya.syntax.core.term.marker.StableWHNF;
 import org.jetbrains.annotations.NotNull;
+import org.jetbrains.annotations.Nullable;
 
 /**
  * ClassCall is a very special construction in Aya.
@@ -45,6 +47,11 @@ public record ClassCall(
     return update(args.map(t -> t.descent(f)));
   }
 
+  public @Nullable Closure get(@NotNull MemberDefLike member) {
+    assert member.classRef() == ref;
+    return args.getOrNull(ref.members().indexOf(member));
+  }
+
   @Override public @NotNull Term doElevate(int level) {
     return new ClassCall(ref, ulift + level, args);
   }
diff --git a/syntax/src/main/java/org/aya/syntax/core/term/call/MemberCall.java b/syntax/src/main/java/org/aya/syntax/core/term/call/MemberCall.java
index 01d92ddef..64ca68d29 100644
--- a/syntax/src/main/java/org/aya/syntax/core/term/call/MemberCall.java
+++ b/syntax/src/main/java/org/aya/syntax/core/term/call/MemberCall.java
@@ -5,6 +5,8 @@
 import kala.collection.immutable.ImmutableSeq;
 import kala.function.IndexedFunction;
 import org.aya.syntax.core.def.MemberDefLike;
+import org.aya.syntax.core.term.ClassCastTerm;
+import org.aya.syntax.core.term.NewTerm;
 import org.aya.syntax.core.term.Term;
 import org.jetbrains.annotations.NotNull;
 
@@ -22,4 +24,30 @@ private MemberCall update(Term clazz, ImmutableSeq<Term> newArgs) {
   @Override public @NotNull Term descent(@NotNull IndexedFunction<Term, Term> f) {
     return update(f.apply(0, of), Callable.descent(args, f));
   }
+
+  public static @NotNull Term make(
+    @NotNull Term of,
+    @NotNull MemberDefLike ref,
+    int ulift,
+    @NotNull ImmutableSeq<@NotNull Term> args
+  ) {
+    return make(new MemberCall(of, ref, ulift, args));
+  }
+
+  public static @NotNull Term make(@NotNull MemberCall call) {
+    return switch (call.of()) {
+      case NewTerm neu -> {
+        var impl = neu.inner().get(call.ref);
+        assert impl != null;    // NewTerm is always fully applied
+        yield impl.apply(neu);
+      }
+      case ClassCastTerm cast -> {
+        var impl = cast.restriction().getOrNull(call.ref());
+        if (impl != null) yield impl.apply(cast);
+        // delegate to inner
+        yield make(call.update(cast.subterm(), call.args));
+      }
+      default -> call;
+    };
+  }
 }

From 86bd9379da416b2a4b3b14ff6d990058173102a6 Mon Sep 17 00:00:00 2001
From: HoshinoTented <hoshinotented@qq.com>
Date: Mon, 1 Jul 2024 17:24:48 +0800
Subject: [PATCH 07/33] cast: more information

---
 .../main/java/org/aya/tyck/ExprTycker.java    | 13 +++--
 .../java/org/aya/unify/TermComparator.java    | 47 ++++++++++++++++--
 .../aya/syntax/core/def/MemberDefLike.java    |  6 +++
 .../aya/syntax/core/term/ClassCastTerm.java   | 48 +++++++++++++++----
 .../aya/syntax/core/term/call/ClassCall.java  |  2 +-
 .../aya/syntax/core/term/call/MemberCall.java |  6 +--
 6 files changed, 98 insertions(+), 24 deletions(-)

diff --git a/base/src/main/java/org/aya/tyck/ExprTycker.java b/base/src/main/java/org/aya/tyck/ExprTycker.java
index 9f1eeb6b5..3a8e17c96 100644
--- a/base/src/main/java/org/aya/tyck/ExprTycker.java
+++ b/base/src/main/java/org/aya/tyck/ExprTycker.java
@@ -165,13 +165,12 @@ case PiTerm(var dom, var cod) -> {
       // Try coercive subtyping for `SomeClass (foo := 114514)` into `SomeClass`
       resultType = whnf(resultType);
       if (resultType instanceof ClassCall resultClazz) {
-        if (unifyTyReported(clazz, resultClazz, expr)) {
-          var restr = resultClazz.args()
-            .drop(clazz.args().size());
-          var fields = clazz.ref().members()
-            .sliceView(clazz.args().size(), resultClazz.args().size());
-          var extra = ImmutableMap.from(fields.zipView(restr));
-          return new Jdg.Default(new ClassCastTerm(result.wellTyped(), extra), type);
+        // TODO: check whether resultClazz <: clazz
+        if (true) {
+          // No need to coerce
+          if (clazz.args().size() == resultClazz.args().size()) return result;
+          var forget = resultClazz.args().drop(clazz.args().size());
+          return new Jdg.Default(new ClassCastTerm(clazz.ref(), result.wellTyped(), clazz.args(), forget), type);
         }
       }
     } else if (unifyTyReported(type, resultType, expr)) return result;
diff --git a/base/src/main/java/org/aya/unify/TermComparator.java b/base/src/main/java/org/aya/unify/TermComparator.java
index 084ab5571..435b1fe59 100644
--- a/base/src/main/java/org/aya/unify/TermComparator.java
+++ b/base/src/main/java/org/aya/unify/TermComparator.java
@@ -33,6 +33,7 @@
 import org.jetbrains.annotations.Nullable;
 
 import java.util.Objects;
+import java.util.function.BiFunction;
 import java.util.function.Function;
 import java.util.function.Supplier;
 import java.util.function.UnaryOperator;
@@ -120,6 +121,13 @@ private <R> R swapped(@NotNull Supplier<R> callback) {
     return result;
   }
 
+  private <L, R, T> T swapped(@NotNull L lhs, @NotNull R rhs, @NotNull BiFunction<R, L, T> callback) {
+    cmp = cmp.invert();
+    var result = callback.apply(rhs, lhs);
+    cmp = cmp.invert();
+    return result;
+  }
+
   /**
    * Compare two terms with the given {@param type} (if not null)
    *
@@ -140,12 +148,20 @@ public boolean compare(@NotNull Term preLhs, @NotNull Term preRhs, @Nullable Ter
       // prefer solving the IsType one as the OfType one.
       if (lhs instanceof MetaCall lMeta && lMeta.ref().req() == MetaVar.Misc.IsType)
         return solveMeta(lMeta, rMeta, type) != null;
-      return swapped(() -> solveMeta(rMeta, lhs, type)) != null;
+      return swapped(lhs, rMeta, (r, l) -> solveMeta(r, l, type)) != null;
     }
     // ^ Beware of the order!!
     if (lhs instanceof MetaCall lMeta) {
       return solveMeta(lMeta, rhs, type) != null;
-    } else if (type == null) {
+    }
+
+    if (rhs instanceof MemberCall && !(lhs instanceof MemberCall)) {
+      var tmp = lhs;
+      lhs = rhs;
+      rhs = tmp;
+    }
+
+    if (type == null) {
       return compareUntyped(lhs, rhs) != null;
     }
 
@@ -171,6 +187,10 @@ private boolean doCompareTyped(@NotNull Term lhs, @NotNull Term rhs, @NotNull Te
       // TODO: ClassCall
       case LamTerm _, ConCallLike _, TupTerm _ -> Panic.unreachable();
       case ErrorTerm _ -> true;
+      case ClassCall classCall -> {
+        if (classCall.args().size() == classCall.ref().members().size()) yield true;
+        // otherwise, lhs and rhs will finally
+      }
       case PiTerm pi -> switch (new Pair<>(lhs, rhs)) {
         case Pair(LamTerm(var lbody), LamTerm(var rbody)) -> subscoped(pi.param(), var ->
           compare(
@@ -226,8 +246,16 @@ case SigmaTerm(var paramSeq) -> {
 
     Term result;
     if (rhs instanceof MetaCall || rhs instanceof MetaLitTerm)
-      result = swapped(() -> doCompareUntyped(rhs, lhs));
-    else result = doCompareUntyped(lhs, rhs);
+      result = swapped(lhs, rhs, this::doCompareUntyped);
+    else {
+      if (rhs instanceof MemberCall && !(lhs instanceof MemberCall)) {
+        var tmp = lhs;
+        lhs = rhs;
+        rhs = tmp;
+      }
+
+      result = doCompareUntyped(lhs, rhs);
+    }
     if (result != null) return whnf(result);
     fail(lhs, rhs);
     return null;
@@ -299,10 +327,19 @@ case ProjTerm(var lof, var ldx) -> {
         case MetaLitTerm mrt -> compareMetaLitWithLit(mlt, mrt.repr(), mrt.type());
         default -> null;
       };
+      case MemberCall memberCall -> {
+        var lof = memberCall.of() instanceof ClassCastTerm cast ? cast.unwrap(this::whnf) : memberCall.of();
+        if (rhs instanceof MemberCall memberCarr) {
+          var rof = memberCarr.of() instanceof ClassCastTerm cast ? cast.unwrap(this::whnf) : memberCarr.of();
+          yield compareUntyped(lof, rof);
+        } else {
+          yield null;
+        }
+      }
       // We already compare arguments in compareApprox, if we arrive here,
       // it means their arguments don't match (even the ref don't match),
       // so we are unable to do more if we can't normalize them.
-      case FnCall _, MemberCall _ -> null;
+      case FnCall _ -> null;
 
       default -> throw noRules(lhs);
     };
diff --git a/syntax/src/main/java/org/aya/syntax/core/def/MemberDefLike.java b/syntax/src/main/java/org/aya/syntax/core/def/MemberDefLike.java
index f698d85fa..f1c97084d 100644
--- a/syntax/src/main/java/org/aya/syntax/core/def/MemberDefLike.java
+++ b/syntax/src/main/java/org/aya/syntax/core/def/MemberDefLike.java
@@ -6,4 +6,10 @@
 
 public sealed interface MemberDefLike extends AnyDef permits MemberDef.Delegate {
   @NotNull ClassDefLike classRef();
+
+  default int index() {
+    var idx = classRef().members().indexOf(this);
+    assert idx >= 0;
+    return idx;
+  }
 }
diff --git a/syntax/src/main/java/org/aya/syntax/core/term/ClassCastTerm.java b/syntax/src/main/java/org/aya/syntax/core/term/ClassCastTerm.java
index 0ce953c5e..80f136015 100644
--- a/syntax/src/main/java/org/aya/syntax/core/term/ClassCastTerm.java
+++ b/syntax/src/main/java/org/aya/syntax/core/term/ClassCastTerm.java
@@ -3,34 +3,66 @@
 package org.aya.syntax.core.term;
 
 import kala.collection.immutable.ImmutableMap;
+import kala.collection.immutable.ImmutableSeq;
 import kala.collection.mutable.MutableMap;
 import kala.function.IndexedFunction;
 import org.aya.syntax.core.Closure;
+import org.aya.syntax.core.def.ClassDefLike;
 import org.aya.syntax.core.def.MemberDefLike;
 import org.aya.util.MapUtil;
 import org.jetbrains.annotations.NotNull;
+import org.jetbrains.annotations.Nullable;
+
+import java.util.function.UnaryOperator;
 
 /**
  * This term is used for subtyping of class, a term {@code x : SomeClass (foo := 114514)} is treated an
- * instance of {@code SomeClass} in user side. In core side, we use {@code cast x (foo := 114514) : SomeClass}
+ * instance of {@code SomeClass} in user side. In core side, we use {@code cast x [] [(foo := 114514)] : SomeClass}
  * to make {@code x} an instance of {@code SomeClass}, it also store the type information in expression
  * so that the {@link org.aya.syntax.core.term.call.MemberCall} can access them without synthesizing.
  */
 public record ClassCastTerm(
+  @NotNull ClassDefLike ref,
   @NotNull Term subterm,
-  @NotNull ImmutableMap<MemberDefLike, Closure> restriction
+  @NotNull ImmutableSeq<Closure> remember,
+  @NotNull ImmutableSeq<Closure> forget
 ) implements Term {
-  public @NotNull ClassCastTerm update(@NotNull Term subterm, @NotNull ImmutableMap<MemberDefLike, Closure> restriction) {
+  public ClassCastTerm {
+    assert forget.isNotEmpty();
+  }
+
+  public @NotNull ClassCastTerm update(
+    @NotNull Term subterm,
+    @NotNull ImmutableSeq<Closure> remember,
+    @NotNull ImmutableSeq<Closure> forget
+  ) {
     return this.subterm == subterm
-      && MapUtil.sameElements(this.restriction, restriction)
+      && this.remember.sameElements(remember, true)
+      && this.forget.sameElements(forget, true)
       ? this
-      : new ClassCastTerm(subterm, restriction);
+      : new ClassCastTerm(ref, subterm, remember, forget);
   }
 
   @Override
   public @NotNull Term descent(@NotNull IndexedFunction<Term, Term> f) {
-    return update(f.apply(0, subterm), ImmutableMap.from(MutableMap.from(restriction).edit()
-      .replaceAll((_, v) -> v.descent(f))
-      .done()));
+    return update(f.apply(0, subterm), remember.map(x -> x.descent(f)), forget.map(x -> x.descent(f)));
+  }
+
+  public @Nullable Closure get(@NotNull MemberDefLike member) {
+    assert ref == member.classRef();
+    var idx = member.index();
+    if (idx < remember.size()) return remember.get(idx);
+    idx = idx - remember.size();
+    if (idx < forget.size()) return forget.get(idx);
+    return null;
+  }
+
+  public @NotNull Term unwrap(@NotNull UnaryOperator<Term> pre) {
+    Term term = this;
+    while (term instanceof ClassCastTerm cast) {
+      term = pre.apply(cast.subterm);
+    }
+
+    return term;
   }
 }
diff --git a/syntax/src/main/java/org/aya/syntax/core/term/call/ClassCall.java b/syntax/src/main/java/org/aya/syntax/core/term/call/ClassCall.java
index 2c2cbd9e2..715c94579 100644
--- a/syntax/src/main/java/org/aya/syntax/core/term/call/ClassCall.java
+++ b/syntax/src/main/java/org/aya/syntax/core/term/call/ClassCall.java
@@ -49,7 +49,7 @@ public record ClassCall(
 
   public @Nullable Closure get(@NotNull MemberDefLike member) {
     assert member.classRef() == ref;
-    return args.getOrNull(ref.members().indexOf(member));
+    return args.getOrNull(member.index());
   }
 
   @Override public @NotNull Term doElevate(int level) {
diff --git a/syntax/src/main/java/org/aya/syntax/core/term/call/MemberCall.java b/syntax/src/main/java/org/aya/syntax/core/term/call/MemberCall.java
index 64ca68d29..39e60eb46 100644
--- a/syntax/src/main/java/org/aya/syntax/core/term/call/MemberCall.java
+++ b/syntax/src/main/java/org/aya/syntax/core/term/call/MemberCall.java
@@ -42,10 +42,10 @@ private MemberCall update(Term clazz, ImmutableSeq<Term> newArgs) {
         yield impl.apply(neu);
       }
       case ClassCastTerm cast -> {
-        var impl = cast.restriction().getOrNull(call.ref());
+        var impl = cast.get(call.ref);
         if (impl != null) yield impl.apply(cast);
-        // delegate to inner
-        yield make(call.update(cast.subterm(), call.args));
+        // no impl
+        yield call;
       }
       default -> call;
     };

From 7dcc4aa1588f088024917776663b335c63f9d632 Mon Sep 17 00:00:00 2001
From: HoshinoTented <hoshinotented@qq.com>
Date: Mon, 1 Jul 2024 23:09:01 +0800
Subject: [PATCH 08/33] member: safe way

---
 .../org/aya/syntax/core/term/call/MemberCall.java    | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/syntax/src/main/java/org/aya/syntax/core/term/call/MemberCall.java b/syntax/src/main/java/org/aya/syntax/core/term/call/MemberCall.java
index 39e60eb46..1856793c7 100644
--- a/syntax/src/main/java/org/aya/syntax/core/term/call/MemberCall.java
+++ b/syntax/src/main/java/org/aya/syntax/core/term/call/MemberCall.java
@@ -25,6 +25,18 @@ private MemberCall update(Term clazz, ImmutableSeq<Term> newArgs) {
     return update(f.apply(0, of), Callable.descent(args, f));
   }
 
+  public static @NotNull Term make(
+    @NotNull ClassCall typeOfOf,
+    @NotNull Term of,
+    @NotNull MemberDefLike ref,
+    int ulift,
+    @NotNull ImmutableSeq<@NotNull Term> args
+  ) {
+    var impl = typeOfOf.get(ref);
+    if (impl != null) return impl.apply(of);
+    return make(new MemberCall(of, ref, ulift, args));
+  }
+
   public static @NotNull Term make(
     @NotNull Term of,
     @NotNull MemberDefLike ref,

From 1302fd37499132f4f791984a9f0e4bb889ccff78 Mon Sep 17 00:00:00 2001
From: HoshinoTented <hoshinotented@qq.com>
Date: Tue, 2 Jul 2024 00:09:43 +0800
Subject: [PATCH 09/33] normalize: fix something

---
 base/src/main/java/org/aya/unify/TermComparator.java       | 7 ++++---
 .../java/org/aya/syntax/core/term/call/MemberCall.java     | 4 ++--
 2 files changed, 6 insertions(+), 5 deletions(-)

diff --git a/base/src/main/java/org/aya/unify/TermComparator.java b/base/src/main/java/org/aya/unify/TermComparator.java
index 435b1fe59..b1154fe5f 100644
--- a/base/src/main/java/org/aya/unify/TermComparator.java
+++ b/base/src/main/java/org/aya/unify/TermComparator.java
@@ -328,10 +328,11 @@ case ProjTerm(var lof, var ldx) -> {
         default -> null;
       };
       case MemberCall memberCall -> {
-        var lof = memberCall.of() instanceof ClassCastTerm cast ? cast.unwrap(this::whnf) : memberCall.of();
+        // it is impossible that memberCall.of() is an cast term, cause it is whnfed.
+        assert !(memberCall.of() instanceof ClassCastTerm);
         if (rhs instanceof MemberCall memberCarr) {
-          var rof = memberCarr.of() instanceof ClassCastTerm cast ? cast.unwrap(this::whnf) : memberCarr.of();
-          yield compareUntyped(lof, rof);
+          assert !(memberCarr.of() instanceof ClassCastTerm);
+          yield compareUntyped(memberCall.of(), memberCarr.of());
         } else {
           yield null;
         }
diff --git a/syntax/src/main/java/org/aya/syntax/core/term/call/MemberCall.java b/syntax/src/main/java/org/aya/syntax/core/term/call/MemberCall.java
index 1856793c7..f141fb88f 100644
--- a/syntax/src/main/java/org/aya/syntax/core/term/call/MemberCall.java
+++ b/syntax/src/main/java/org/aya/syntax/core/term/call/MemberCall.java
@@ -56,8 +56,8 @@ private MemberCall update(Term clazz, ImmutableSeq<Term> newArgs) {
       case ClassCastTerm cast -> {
         var impl = cast.get(call.ref);
         if (impl != null) yield impl.apply(cast);
-        // no impl
-        yield call;
+        // no impl, try inner
+        yield call.update(cast.subterm(), call.args);
       }
       default -> call;
     };

From 050c950044b874040de5fdfa1b914d04a51ac614 Mon Sep 17 00:00:00 2001
From: HoshinoTented <hoshinotented@qq.com>
Date: Tue, 2 Jul 2024 00:11:37 +0800
Subject: [PATCH 10/33] cast: StableWHNF

---
 .../src/main/java/org/aya/syntax/core/term/ClassCastTerm.java  | 3 ++-
 .../main/java/org/aya/syntax/core/term/marker/StableWHNF.java  | 2 +-
 2 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/syntax/src/main/java/org/aya/syntax/core/term/ClassCastTerm.java b/syntax/src/main/java/org/aya/syntax/core/term/ClassCastTerm.java
index 80f136015..238eeb7b5 100644
--- a/syntax/src/main/java/org/aya/syntax/core/term/ClassCastTerm.java
+++ b/syntax/src/main/java/org/aya/syntax/core/term/ClassCastTerm.java
@@ -9,6 +9,7 @@
 import org.aya.syntax.core.Closure;
 import org.aya.syntax.core.def.ClassDefLike;
 import org.aya.syntax.core.def.MemberDefLike;
+import org.aya.syntax.core.term.marker.StableWHNF;
 import org.aya.util.MapUtil;
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
@@ -26,7 +27,7 @@ public record ClassCastTerm(
   @NotNull Term subterm,
   @NotNull ImmutableSeq<Closure> remember,
   @NotNull ImmutableSeq<Closure> forget
-) implements Term {
+) implements StableWHNF, Term {
   public ClassCastTerm {
     assert forget.isNotEmpty();
   }
diff --git a/syntax/src/main/java/org/aya/syntax/core/term/marker/StableWHNF.java b/syntax/src/main/java/org/aya/syntax/core/term/marker/StableWHNF.java
index d96968e7e..b0a408ab2 100644
--- a/syntax/src/main/java/org/aya/syntax/core/term/marker/StableWHNF.java
+++ b/syntax/src/main/java/org/aya/syntax/core/term/marker/StableWHNF.java
@@ -16,5 +16,5 @@
  * after a substitution (this usually happens under face restrictions (aka cofibrations)).
  */
 public sealed interface StableWHNF extends Term
-  permits ErrorTerm, LamTerm, NewTerm, PiTerm, SigmaTerm, SortTerm, TupTerm, ClassCall, DataCall, IntegerTerm, ListTerm, StringTerm, DimTerm, EqTerm {
+  permits ClassCastTerm, ErrorTerm, LamTerm, NewTerm, PiTerm, SigmaTerm, SortTerm, TupTerm, ClassCall, DataCall, IntegerTerm, ListTerm, StringTerm, DimTerm, EqTerm {
 }

From daf583d0b6ac3392c699776c65ad9e4d41bebb5f Mon Sep 17 00:00:00 2001
From: HoshinoTented <hoshinotented@qq.com>
Date: Wed, 3 Jul 2024 18:19:26 +0800
Subject: [PATCH 11/33] conversion: is it right?

---
 base/src/main/java/org/aya/unify/TermComparator.java | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

diff --git a/base/src/main/java/org/aya/unify/TermComparator.java b/base/src/main/java/org/aya/unify/TermComparator.java
index b1154fe5f..a6877a82e 100644
--- a/base/src/main/java/org/aya/unify/TermComparator.java
+++ b/base/src/main/java/org/aya/unify/TermComparator.java
@@ -189,7 +189,15 @@ private boolean doCompareTyped(@NotNull Term lhs, @NotNull Term rhs, @NotNull Te
       case ErrorTerm _ -> true;
       case ClassCall classCall -> {
         if (classCall.args().size() == classCall.ref().members().size()) yield true;
-        // otherwise, lhs and rhs will finally
+        // TODO: should we compare fields that have impl?
+        yield classCall.ref().members().allMatch(member -> {
+          // loop invariant: first [i] members are the "same". ([i] is the loop counter)
+          // Note that member can only refer to first [i - 1] members, so it is safe that we supply [lhs] or [rhs]
+          var ty = member.signature().inst(ImmutableSeq.of(lhs));
+          var lproj = MemberCall.make(classCall, lhs, member, 0, ImmutableSeq.empty());
+          var rproj = MemberCall.make(classCall, rhs, member, 0, ImmutableSeq.empty());
+          return compare(lproj, rproj, ty.makePi(ImmutableSeq.empty()));
+        });
       }
       case PiTerm pi -> switch (new Pair<>(lhs, rhs)) {
         case Pair(LamTerm(var lbody), LamTerm(var rbody)) -> subscoped(pi.param(), var ->

From 95a150cec779c3fc83f129195211cb7536e7e74d Mon Sep 17 00:00:00 2001
From: HoshinoTented <hoshinotented@qq.com>
Date: Wed, 3 Jul 2024 18:27:12 +0800
Subject: [PATCH 12/33] misc: oops

---
 base/src/main/java/org/aya/unify/TermComparator.java | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/base/src/main/java/org/aya/unify/TermComparator.java b/base/src/main/java/org/aya/unify/TermComparator.java
index a6877a82e..761c2db19 100644
--- a/base/src/main/java/org/aya/unify/TermComparator.java
+++ b/base/src/main/java/org/aya/unify/TermComparator.java
@@ -191,8 +191,8 @@ private boolean doCompareTyped(@NotNull Term lhs, @NotNull Term rhs, @NotNull Te
         if (classCall.args().size() == classCall.ref().members().size()) yield true;
         // TODO: should we compare fields that have impl?
         yield classCall.ref().members().allMatch(member -> {
-          // loop invariant: first [i] members are the "same". ([i] is the loop counter)
-          // Note that member can only refer to first [i - 1] members, so it is safe that we supply [lhs] or [rhs]
+          // loop invariant: first [i] members are the "same". ([i] is the loop counter, count from 0)
+          // Note that member can only refer to first [i] members, so it is safe that we supply [lhs] or [rhs]
           var ty = member.signature().inst(ImmutableSeq.of(lhs));
           var lproj = MemberCall.make(classCall, lhs, member, 0, ImmutableSeq.empty());
           var rproj = MemberCall.make(classCall, rhs, member, 0, ImmutableSeq.empty());

From 81813e3414a5e7c4ee2ae66415a4040e87543b7c Mon Sep 17 00:00:00 2001
From: HoshinoTented <hoshinotented@qq.com>
Date: Wed, 3 Jul 2024 19:24:58 +0800
Subject: [PATCH 13/33] class: maybe I should run some tests

---
 base/src/main/java/org/aya/unify/Synthesizer.java           | 1 +
 syntax/src/main/java/org/aya/prettier/ConcretePrettier.java | 1 +
 syntax/src/main/java/org/aya/prettier/CorePrettier.java     | 1 +
 3 files changed, 3 insertions(+)

diff --git a/base/src/main/java/org/aya/unify/Synthesizer.java b/base/src/main/java/org/aya/unify/Synthesizer.java
index c72ca92b5..39c29fc89 100644
--- a/base/src/main/java/org/aya/unify/Synthesizer.java
+++ b/base/src/main/java/org/aya/unify/Synthesizer.java
@@ -137,6 +137,7 @@ case MetaCall(var ref, var args) when ref.req() instanceof MetaVar.OfType(var ty
       case StringTerm str -> state().primFactory.getCall(PrimDef.ID.STRING);
       case ClassCall classCall -> throw new UnsupportedOperationException("TODO");
       case NewTerm newTerm -> newTerm.inner();
+      case ClassCastTerm castTerm -> new ClassCall(castTerm.ref(), 0, castTerm.remember());
     };
   }
 
diff --git a/syntax/src/main/java/org/aya/prettier/ConcretePrettier.java b/syntax/src/main/java/org/aya/prettier/ConcretePrettier.java
index 73d665df2..017f3ea31 100644
--- a/syntax/src/main/java/org/aya/prettier/ConcretePrettier.java
+++ b/syntax/src/main/java/org/aya/prettier/ConcretePrettier.java
@@ -235,6 +235,7 @@ yield visitCalls(null, fn, (_, l) -> l.toDoc(options), outer,
         Doc.sep(Doc.styled(KEYWORD, "let"), stmt(letOpen.openCmd()), Doc.styled(KEYWORD, "in")),
         Doc.indent(2, term(Outer.Free, letOpen.body()))
       );
+      case Expr.New neu -> throw new UnsupportedOperationException("TODO");
     };
   }
 
diff --git a/syntax/src/main/java/org/aya/prettier/CorePrettier.java b/syntax/src/main/java/org/aya/prettier/CorePrettier.java
index c40420765..2e6865e74 100644
--- a/syntax/src/main/java/org/aya/prettier/CorePrettier.java
+++ b/syntax/src/main/java/org/aya/prettier/CorePrettier.java
@@ -219,6 +219,7 @@ case EqTerm(var _, var a, var b) -> {
         yield checkParen(outer, doc, Outer.BinOp);
       }
       case RuleReducer.Fn fn -> term(outer, fn.toFnCall());
+      case ClassCastTerm classCastTerm -> term(outer, classCastTerm.subterm());
     };
   }
 

From faad9e0c1ef349853881674f197f11cf1460e52c Mon Sep 17 00:00:00 2001
From: HoshinoTented <hoshinotented@qq.com>
Date: Wed, 3 Jul 2024 19:51:02 +0800
Subject: [PATCH 14/33] prettier: new

---
 syntax/src/main/java/org/aya/prettier/ConcretePrettier.java | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/syntax/src/main/java/org/aya/prettier/ConcretePrettier.java b/syntax/src/main/java/org/aya/prettier/ConcretePrettier.java
index 017f3ea31..721eaf09e 100644
--- a/syntax/src/main/java/org/aya/prettier/ConcretePrettier.java
+++ b/syntax/src/main/java/org/aya/prettier/ConcretePrettier.java
@@ -235,7 +235,7 @@ yield visitCalls(null, fn, (_, l) -> l.toDoc(options), outer,
         Doc.sep(Doc.styled(KEYWORD, "let"), stmt(letOpen.openCmd()), Doc.styled(KEYWORD, "in")),
         Doc.indent(2, term(Outer.Free, letOpen.body()))
       );
-      case Expr.New neu -> throw new UnsupportedOperationException("TODO");
+      case Expr.New neu -> Doc.sep(KW_NEW, term(Outer.Free, neu.classCall()));
     };
   }
 

From bb67d5b4d4737a7b67c07ca0e9e8f0b7cee9a8fc Mon Sep 17 00:00:00 2001
From: HoshinoTented <hoshinotented@qq.com>
Date: Thu, 4 Jul 2024 20:23:32 +0800
Subject: [PATCH 15/33] class: omg

---
 .../main/java/org/aya/tyck/ExprTycker.java    | 24 ++++++++++-----
 .../main/java/org/aya/tyck/StmtTycker.java    |  2 +-
 .../java/org/aya/tyck/tycker/AppTycker.java   | 29 ++++++++++++-------
 .../java/org/aya/syntax/core/def/AnyDef.java  |  9 ++++++
 .../org/aya/syntax/core/def/MemberDef.java    | 12 +++++++-
 .../aya/syntax/core/term/call/ClassCall.java  |  3 +-
 6 files changed, 57 insertions(+), 22 deletions(-)

diff --git a/base/src/main/java/org/aya/tyck/ExprTycker.java b/base/src/main/java/org/aya/tyck/ExprTycker.java
index 3a8e17c96..fab419997 100644
--- a/base/src/main/java/org/aya/tyck/ExprTycker.java
+++ b/base/src/main/java/org/aya/tyck/ExprTycker.java
@@ -49,6 +49,7 @@
 import org.jetbrains.annotations.NotNull;
 
 import java.util.Comparator;
+import java.util.function.BiFunction;
 import java.util.function.Function;
 import java.util.function.Supplier;
 
@@ -376,10 +377,11 @@ case CompiledVar(var content) -> new AppTycker<>(this, sourcePos, args.size(), l
 
   private Jdg computeArgs(
     @NotNull SourcePos pos, @NotNull ImmutableSeq<Expr.NamedArg> args,
-    @NotNull AbstractTele params, @NotNull Function<Term[], Jdg> k
+    @NotNull AbstractTele params, @NotNull BiFunction<Term[], Term[], Jdg> k
   ) throws NotPi {
     int argIx = 0, paramIx = 0;
     var result = new Term[params.telescopeSize()];
+    var types = new Term[params.telescopeSize()];
     while (argIx < args.size() && paramIx < params.telescopeSize()) {
       var arg = args.get(argIx);
       var param = params.telescopeRich(paramIx, result);
@@ -390,33 +392,39 @@ private Jdg computeArgs(
           break;
         } else if (arg.name() == null) {
           // here, arg.explicit() == true and param.explicit() == false
-          result[paramIx++] = insertImplicit(param, arg.sourcePos());
+          result[paramIx] = insertImplicit(param, arg.sourcePos());
+          types[paramIx++] = param.type();
           continue;
         }
       }
       if (arg.name() != null && !param.nameEq(arg.name())) {
-        result[paramIx++] = insertImplicit(param, arg.sourcePos());
+        result[paramIx] = insertImplicit(param, arg.sourcePos());
+        types[paramIx++] = param.type();
         continue;
       }
-      result[paramIx++] = inherit(arg.arg(), param.type()).wellTyped();
+      var what = inherit(arg.arg(), param.type());
+      result[paramIx] = what.wellTyped();
+      types[paramIx++] = what.type();
       argIx++;
     }
     // Trailing implicits
     while (paramIx < params.telescopeSize()) {
       if (params.telescopeLicit(paramIx)) break;
       var param = params.telescopeRich(paramIx, result);
-      result[paramIx++] = insertImplicit(param, pos);
+      result[paramIx] = insertImplicit(param, pos);
+      types[paramIx++] = param.type();
     }
     var extraParams = MutableStack.<Pair<LocalVar, Term>>create();
     if (argIx < args.size()) {
-      return generateApplication(args.drop(argIx), k.apply(result));
+      return generateApplication(args.drop(argIx), k.apply(result, types));
     } else while (paramIx < params.telescopeSize()) {
       var param = params.telescopeRich(paramIx, result);
       var atarashiVar = LocalVar.generate(param.name());
       extraParams.push(new Pair<>(atarashiVar, param.type()));
-      result[paramIx++] = new FreeTerm(atarashiVar);
+      result[paramIx] = new FreeTerm(atarashiVar);
+      types[paramIx++] = param.type();
     }
-    var generated = k.apply(result);
+    var generated = k.apply(result, types);
     while (extraParams.isNotEmpty()) {
       var pair = extraParams.pop();
       generated = new Jdg.Default(
diff --git a/base/src/main/java/org/aya/tyck/StmtTycker.java b/base/src/main/java/org/aya/tyck/StmtTycker.java
index a5daf3b66..d8a40b635 100644
--- a/base/src/main/java/org/aya/tyck/StmtTycker.java
+++ b/base/src/main/java/org/aya/tyck/StmtTycker.java
@@ -173,7 +173,7 @@ private void checkMember(@NotNull ClassMember member, @NotNull ExprTycker tycker
         new Param("self", classCall, false),
         classRef.concrete.sourcePos()
       );
-    new MemberDef(classRef, member.ref, signature.params(), signature.result());
+    new MemberDef(classRef, member.ref, classRef.concrete.members.indexOf(member), signature.params(), signature.result());
     member.ref.signature = signature;
   }
 
diff --git a/base/src/main/java/org/aya/tyck/tycker/AppTycker.java b/base/src/main/java/org/aya/tyck/tycker/AppTycker.java
index 65bdc2892..d2434597a 100644
--- a/base/src/main/java/org/aya/tyck/tycker/AppTycker.java
+++ b/base/src/main/java/org/aya/tyck/tycker/AppTycker.java
@@ -30,12 +30,17 @@
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 
+import java.util.function.BiFunction;
 import java.util.function.Function;
 
 public record AppTycker<Ex extends Exception>(
-  @NotNull TyckState state, @NotNull AbstractTycker tycker, @NotNull SourcePos pos,
-  int argsCount, int lift, @NotNull Factory<Ex> makeArgs
-) {
+  @Override @NotNull TyckState state,
+  @NotNull AbstractTycker tycker,
+  @NotNull SourcePos pos,
+  int argsCount,
+  int lift,
+  @NotNull Factory<Ex> makeArgs
+) implements Stateful {
   /**
    * <pre>
    * Signature (0th param) --------> Argument Parser (this interface)
@@ -48,7 +53,7 @@ public record AppTycker<Ex extends Exception>(
    */
   @FunctionalInterface
   public interface Factory<Ex extends Exception> extends
-    CheckedBiFunction<AbstractTele, Function<Term[], Jdg>, Jdg, Ex> {
+    CheckedBiFunction<AbstractTele, BiFunction<Term[], Term[], Jdg>, Jdg, Ex> {
   }
 
   public AppTycker(
@@ -103,7 +108,7 @@ public AppTycker(
     // ownerTele + selfTele
     var fullSignature = conVar.signature().lift(lift);
 
-    return makeArgs.applyChecked(fullSignature, args -> {
+    return makeArgs.applyChecked(fullSignature, (args, _) -> {
       var realArgs = ImmutableArray.from(args);
       var ownerArgs = realArgs.take(conVar.ownerTeleSize());
       var conArgs = realArgs.drop(conVar.ownerTeleSize());
@@ -119,14 +124,14 @@ public AppTycker(
   }
   private @NotNull Jdg checkPrimCall(@NotNull PrimDefLike primVar) throws Ex {
     var signature = primVar.signature().lift(lift);
-    return makeArgs.applyChecked(signature, args -> new Jdg.Default(
+    return makeArgs.applyChecked(signature, (args, _) -> new Jdg.Default(
       state.primFactory.unfold(new PrimCall(primVar, 0, ImmutableArray.from(args)), state),
       signature.result(args)
     ));
   }
   private @NotNull Jdg checkDataCall(@NotNull DataDefLike data) throws Ex {
     var signature = data.signature().lift(lift);
-    return makeArgs.applyChecked(signature, args -> new Jdg.Default(
+    return makeArgs.applyChecked(signature, (args, _) -> new Jdg.Default(
       new DataCall(data, 0, ImmutableArray.from(args)),
       signature.result(args)
     ));
@@ -135,7 +140,7 @@ public AppTycker(
     @NotNull FnDefLike fnDef, @Nullable Shaped.Applicable<FnDefLike> operator
   ) throws Ex {
     var signature = fnDef.signature().lift(lift);
-    return makeArgs.applyChecked(signature, args -> {
+    return makeArgs.applyChecked(signature, (args, _) -> {
       var argsSeq = ImmutableArray.from(args);
       var result = signature.result(args);
       if (operator != null) {
@@ -150,7 +155,7 @@ public AppTycker(
     var self = LocalVar.generate("self");
     var appliedParams = ofClassMembers(self, clazz, argsCount).lift(lift);
     state.classThis.push(self);
-    var result = makeArgs.applyChecked(appliedParams, args -> new Jdg.Default(
+    var result = makeArgs.applyChecked(appliedParams, (args, _) -> new Jdg.Default(
       new ClassCall(clazz, 0, ImmutableArray.from(args).map(x -> x.bind(self))),
       appliedParams.result(args)
     ));
@@ -160,11 +165,13 @@ public AppTycker(
 
   private @NotNull Jdg checkProjCall(@NotNull MemberDefLike member) throws Ex {
     var signature = member.signature().lift(lift);
-    return makeArgs.applyChecked(signature, args -> {
+    return makeArgs.applyChecked(signature, (args, ty) -> {
       assert args.length >= 1;
+      var ofTy = whnf(ty[0]);
+      if (!(ofTy instanceof ClassCall classTy)) throw new UnsupportedOperationException("report");   // TODO
       var fieldArgs = ImmutableArray.fill(args.length - 1, i -> args[i + 1]);
       return new Jdg.Default(
-        new MemberCall(args[0], member, 0, fieldArgs),
+        MemberCall.make(classTy, args[0], member, 0, fieldArgs),
         signature.result(args)
       );
     });
diff --git a/syntax/src/main/java/org/aya/syntax/core/def/AnyDef.java b/syntax/src/main/java/org/aya/syntax/core/def/AnyDef.java
index bd8a95141..bf03af561 100644
--- a/syntax/src/main/java/org/aya/syntax/core/def/AnyDef.java
+++ b/syntax/src/main/java/org/aya/syntax/core/def/AnyDef.java
@@ -6,6 +6,7 @@
 import org.aya.syntax.compile.JitDef;
 import org.aya.syntax.ref.*;
 import org.aya.syntax.telescope.AbstractTele;
+import org.aya.util.Pair;
 import org.aya.util.binop.Assoc;
 import org.aya.util.binop.OpDecl;
 import org.jetbrains.annotations.NotNull;
@@ -60,5 +61,13 @@ public sealed interface AnyDef extends OpDecl permits JitDef, ClassDefLike, ConD
     };
   }
 
+  static @NotNull boolean equals(@NotNull AnyDef lhs, @NotNull AnyDef rhs) {
+    return switch (new Pair<>(lhs, rhs)) {
+      case Pair(JitDef jlhs, JitDef jrhs) -> jlhs == jrhs;
+      case Pair(TyckAnyDef<?> tlhs, TyckAnyDef<?> trhs) -> tlhs.ref == trhs.ref;
+      default -> throw new UnsupportedOperationException("TODO");
+    };
+  }
+
   @NotNull AbstractTele signature();
 }
diff --git a/syntax/src/main/java/org/aya/syntax/core/def/MemberDef.java b/syntax/src/main/java/org/aya/syntax/core/def/MemberDef.java
index 9db5eefba..ab1db7d38 100644
--- a/syntax/src/main/java/org/aya/syntax/core/def/MemberDef.java
+++ b/syntax/src/main/java/org/aya/syntax/core/def/MemberDef.java
@@ -18,13 +18,23 @@
 public record MemberDef(
   @NotNull DefVar<ClassDef, ClassDecl> classRef,
   @Override @NotNull DefVar<MemberDef, ClassMember> ref,
+  int index,
   @Override ImmutableSeq<Param> telescope,
   @Override @NotNull Term result
 ) implements TyckDef {
-  public MemberDef { ref.initialize(this); }
+  public MemberDef {
+    assert index >= 0;
+    ref.initialize(this);
+  }
+
   public static final class Delegate extends TyckAnyDef<MemberDef> implements MemberDefLike {
     public Delegate(@NotNull DefVar<MemberDef, ?> ref) { super(ref); }
 
+    @Override
+    public int index() {
+      return ref.core.index;
+    }
+
     @Override public @NotNull ClassDefLike classRef() {
       return new ClassDef.Delegate(core().classRef());
     }
diff --git a/syntax/src/main/java/org/aya/syntax/core/term/call/ClassCall.java b/syntax/src/main/java/org/aya/syntax/core/term/call/ClassCall.java
index 715c94579..5fd711721 100644
--- a/syntax/src/main/java/org/aya/syntax/core/term/call/ClassCall.java
+++ b/syntax/src/main/java/org/aya/syntax/core/term/call/ClassCall.java
@@ -5,6 +5,7 @@
 import kala.collection.immutable.ImmutableSeq;
 import kala.function.IndexedFunction;
 import org.aya.syntax.core.Closure;
+import org.aya.syntax.core.def.AnyDef;
 import org.aya.syntax.core.def.ClassDefLike;
 import org.aya.syntax.core.def.MemberDefLike;
 import org.aya.syntax.core.term.NewTerm;
@@ -48,7 +49,7 @@ public record ClassCall(
   }
 
   public @Nullable Closure get(@NotNull MemberDefLike member) {
-    assert member.classRef() == ref;
+    assert AnyDef.equals(ref, member.classRef());
     return args.getOrNull(member.index());
   }
 

From c0d256908a83fe27d2ff12397288bea07a87100c Mon Sep 17 00:00:00 2001
From: HoshinoTented <hoshinotented@qq.com>
Date: Thu, 4 Jul 2024 21:52:22 +0800
Subject: [PATCH 16/33] misc: docs

---
 syntax/src/main/java/org/aya/syntax/core/def/MemberDef.java | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/syntax/src/main/java/org/aya/syntax/core/def/MemberDef.java b/syntax/src/main/java/org/aya/syntax/core/def/MemberDef.java
index ab1db7d38..d1020a751 100644
--- a/syntax/src/main/java/org/aya/syntax/core/def/MemberDef.java
+++ b/syntax/src/main/java/org/aya/syntax/core/def/MemberDef.java
@@ -12,6 +12,7 @@
 
 /**
  * A class field definition.
+ *
  * @param telescope it is bound with the `self` pointer, so whenever you need to make sense of this type,
  *                  you need to inst its elements with `self` first.
  */
@@ -30,6 +31,9 @@ public record MemberDef(
   public static final class Delegate extends TyckAnyDef<MemberDef> implements MemberDefLike {
     public Delegate(@NotNull DefVar<MemberDef, ?> ref) { super(ref); }
 
+    /**
+     * this implementation prevents invocation of {@link ClassDef.Delegate#members()} while tycking {@link ClassDef}
+     */
     @Override
     public int index() {
       return ref.core.index;

From 1cd73f74431c384053b71975e85be451db37e44c Mon Sep 17 00:00:00 2001
From: HoshinoTented <hoshinotented@qq.com>
Date: Fri, 5 Jul 2024 01:19:50 +0800
Subject: [PATCH 17/33] misc: use equals

---
 .../src/main/java/org/aya/syntax/core/term/call/ClassCall.java  | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/syntax/src/main/java/org/aya/syntax/core/term/call/ClassCall.java b/syntax/src/main/java/org/aya/syntax/core/term/call/ClassCall.java
index 5fd711721..0c8427833 100644
--- a/syntax/src/main/java/org/aya/syntax/core/term/call/ClassCall.java
+++ b/syntax/src/main/java/org/aya/syntax/core/term/call/ClassCall.java
@@ -49,7 +49,7 @@ public record ClassCall(
   }
 
   public @Nullable Closure get(@NotNull MemberDefLike member) {
-    assert AnyDef.equals(ref, member.classRef());
+    assert ref.equals(member.classRef());
     return args.getOrNull(member.index());
   }
 

From f4d403603221e6020ef9460ea42cacc7d129a374 Mon Sep 17 00:00:00 2001
From: HoshinoTented <hoshinotented@qq.com>
Date: Sun, 7 Jul 2024 09:16:12 +0800
Subject: [PATCH 18/33] class: add test, but why failed on "shared"?

---
 .../test/resources/success/src/Classes.aya    |  7 +++++
 .../org/aya/compiler/TermExprializer.java     | 26 ++++++++++---------
 .../main/gen/org/aya/parser/AyaPsiParser.java |  8 ------
 parser/src/main/grammar/AyaPsiParser.bnf      |  2 +-
 .../java/org/aya/producer/AyaProducer.java    |  4 +++
 .../java/org/aya/syntax/core/def/AnyDef.java  |  8 ------
 .../aya/syntax/core/term/call/MemberCall.java |  9 -------
 7 files changed, 26 insertions(+), 38 deletions(-)
 create mode 100644 cli-impl/src/test/resources/success/src/Classes.aya

diff --git a/cli-impl/src/test/resources/success/src/Classes.aya b/cli-impl/src/test/resources/success/src/Classes.aya
new file mode 100644
index 000000000..3eadcfc08
--- /dev/null
+++ b/cli-impl/src/test/resources/success/src/Classes.aya
@@ -0,0 +1,7 @@
+open import prelude
+
+class Kontainer
+| Taipe : Type
+| walue : Taipe
+
+def norm0 : walue (new Kontainer Nat 0) = 0 => idp
diff --git a/jit-compiler/src/main/java/org/aya/compiler/TermExprializer.java b/jit-compiler/src/main/java/org/aya/compiler/TermExprializer.java
index bbbe5b03a..13fbcbf43 100644
--- a/jit-compiler/src/main/java/org/aya/compiler/TermExprializer.java
+++ b/jit-compiler/src/main/java/org/aya/compiler/TermExprializer.java
@@ -72,15 +72,15 @@ public TermExprializer(@NotNull NameGenerator nameGen, @NotNull ImmutableSeq<Str
   private @NotNull String serializeApplicable(@NotNull Shaped.Applicable<?> applicable) {
     return switch (applicable) {
       case IntegerOps.ConRule conRule ->
-        ExprializeUtils.makeNew(CLASS_INT_CONRULE, ExprializeUtils.getInstance(NameSerializer.getClassReference(conRule.ref())),
+        ExprializeUtils.makeNew(CLASS_INT_CONRULE, ExprializeUtils.getInstance(getClassReference(conRule.ref())),
           doSerialize(conRule.zero())
         );
       case IntegerOps.FnRule fnRule -> ExprializeUtils.makeNew(CLASS_INT_FNRULE,
-        ExprializeUtils.getInstance(NameSerializer.getClassReference(fnRule.ref())),
+        ExprializeUtils.getInstance(getClassReference(fnRule.ref())),
         ExprializeUtils.makeSub(CLASS_FNRULE_KIND, fnRule.kind().toString())
       );
       case ListOps.ConRule conRule -> ExprializeUtils.makeNew(CLASS_LIST_CONRULE,
-        ExprializeUtils.getInstance(NameSerializer.getClassReference(conRule.ref())),
+        ExprializeUtils.getInstance(getClassReference(conRule.ref())),
         doSerialize(conRule.empty())
       );
       default -> Panic.unreachable();
@@ -134,7 +134,7 @@ case FreeTerm(var bind) -> {
       }
       case TyckInternal i -> throw new Panic(i.getClass().toString());
       case Callable.SharableCall call when call.ulift() == 0 && call.args().isEmpty() ->
-        ExprializeUtils.getEmptyCallTerm(NameSerializer.getClassReference(call.ref()));
+        ExprializeUtils.getEmptyCallTerm(getClassReference(call.ref()));
       case ClassCall classCall -> throw new UnsupportedOperationException("TODO");
       case MemberCall memberCall -> throw new UnsupportedOperationException("TODO");
       case AppTerm appTerm -> makeAppNew(CLASS_APPTERM, appTerm.fun(), appTerm.arg());
@@ -142,19 +142,19 @@ case FreeTerm(var bind) -> {
       case LocalTerm(var index) -> ExprializeUtils.makeNew(CLASS_LOCALTERM, Integer.toString(index));
       case LamTerm lamTerm -> ExprializeUtils.makeNew(CLASS_LAMTERM, serializeClosure(lamTerm.body()));
       case DataCall(var ref, var ulift, var args) -> ExprializeUtils.makeNew(CLASS_DATACALL,
-        ExprializeUtils.getInstance(NameSerializer.getClassReference(ref)),
+        ExprializeUtils.getInstance(getClassReference(ref)),
         Integer.toString(ulift),
         serializeToImmutableSeq(CLASS_TERM, args)
       );
       case ConCall(var head, var args) -> ExprializeUtils.makeNew(CLASS_CONCALL,
-        ExprializeUtils.getInstance(NameSerializer.getClassReference(head.ref())),
+        ExprializeUtils.getInstance(getClassReference(head.ref())),
         serializeToImmutableSeq(CLASS_TERM, head.ownerArgs()),
         Integer.toString(head.ulift()),
         serializeToImmutableSeq(CLASS_TERM, args)
       );
       case FnCall call -> {
         var ref = switch (call.ref()) {
-          case JitFn jit -> ExprializeUtils.getInstance(NameSerializer.getClassReference(jit));
+          case JitFn jit -> ExprializeUtils.getInstance(getClassReference(jit));
           case FnDef.Delegate def -> ExprializeUtils.getInstance(getClassReference(def.ref));
         };
 
@@ -208,24 +208,26 @@ case TupTerm(var items) -> ExprializeUtils.makeNew(ExprializeUtils.getJavaRefere
       );
       case SigmaTerm sigmaTerm -> throw new UnsupportedOperationException("TODO");
       case PrimCall(var ref, var ulift, var args) -> ExprializeUtils.makeNew(CLASS_PRIMCALL,
-        ExprializeUtils.getInstance(NameSerializer.getClassReference(ref)),
+        ExprializeUtils.getInstance(getClassReference(ref)),
         Integer.toString(ulift),
         serializeToImmutableSeq(CLASS_TERM, args)
       );
       case IntegerTerm(var repr, var zero, var suc, var type) -> ExprializeUtils.makeNew(CLASS_INTEGER,
         Integer.toString(repr),
-        ExprializeUtils.getInstance(NameSerializer.getClassReference(zero)),
-        ExprializeUtils.getInstance(NameSerializer.getClassReference(suc)),
+        ExprializeUtils.getInstance(getClassReference(zero)),
+        ExprializeUtils.getInstance(getClassReference(suc)),
         doSerialize(type)
       );
       case ListTerm(var repr, var nil, var cons, var type) -> ExprializeUtils.makeNew(CLASS_LIST,
         ExprializeUtils.makeImmutableSeq(CLASS_TERM, repr.map(this::doSerialize), CLASS_PIMMSEQ),
-        ExprializeUtils.getInstance(NameSerializer.getClassReference(nil)),
-        ExprializeUtils.getInstance(NameSerializer.getClassReference(cons)),
+        ExprializeUtils.getInstance(getClassReference(nil)),
+        ExprializeUtils.getInstance(getClassReference(cons)),
         doSerialize(type)
       );
       case StringTerm stringTerm ->
         ExprializeUtils.makeNew(CLASS_STRING, ExprializeUtils.makeString(StringUtil.escapeStringCharacters(stringTerm.string())));
+      case ClassCastTerm classCastTerm -> throw new UnsupportedOperationException("TODO");
+      case NewTerm newTerm -> throw new UnsupportedOperationException("TODO");
     };
   }
 
diff --git a/parser/src/main/gen/org/aya/parser/AyaPsiParser.java b/parser/src/main/gen/org/aya/parser/AyaPsiParser.java
index 43b59979b..0eaa72218 100644
--- a/parser/src/main/gen/org/aya/parser/AyaPsiParser.java
+++ b/parser/src/main/gen/org/aya/parser/AyaPsiParser.java
@@ -2261,18 +2261,10 @@ public static boolean newExpr(PsiBuilder b, int l) {
     r = consumeTokenSmart(b, KW_NEW);
     p = r;
     r = p && expr(b, l, 0);
-    r = p && report_error_(b, newExpr_1(b, l + 1)) && r;
     exit_section_(b, l, m, NEW_EXPR, r, p, null);
     return r || p;
   }
 
-  // newBody?
-  private static boolean newExpr_1(PsiBuilder b, int l) {
-    if (!recursion_guard_(b, l, "newExpr_1")) return false;
-    newBody(b, l + 1);
-    return true;
-  }
-
   public static boolean piExpr(PsiBuilder b, int l) {
     if (!recursion_guard_(b, l, "piExpr")) return false;
     if (!nextTokenIsSmart(b, KW_PI)) return false;
diff --git a/parser/src/main/grammar/AyaPsiParser.bnf b/parser/src/main/grammar/AyaPsiParser.bnf
index 4c7de8e9c..ef6621bb5 100644
--- a/parser/src/main/grammar/AyaPsiParser.bnf
+++ b/parser/src/main/grammar/AyaPsiParser.bnf
@@ -279,7 +279,7 @@ arrayCompBlock ::= expr BAR <<commaSep doBinding>>
 arrayElementsBlock ::= exprList
 idiomBlock ::= barred* expr
 
-newExpr ::= KW_NEW expr newBody?
+newExpr ::= KW_NEW expr // newBody?
 appExpr ::= expr argument+
 arrowExpr ::= expr TO expr { rightAssociative = true }
 projExpr ::= expr projFix
diff --git a/producer/src/main/java/org/aya/producer/AyaProducer.java b/producer/src/main/java/org/aya/producer/AyaProducer.java
index 291611324..577e42c39 100644
--- a/producer/src/main/java/org/aya/producer/AyaProducer.java
+++ b/producer/src/main/java/org/aya/producer/AyaProducer.java
@@ -563,6 +563,10 @@ private record DeclNameOrInfix(@NotNull WithPos<String> name, @Nullable OpDecl.O
       var param = new Expr.Param(paramPos, Constants.randomlyNamed(paramPos), expr(expr0), true);
       return new WithPos<>(pos, new Expr.Pi(param, to));
     }
+    if (node.is(NEW_EXPR)) {
+      var classCall = expr(node.child(EXPR));
+      return new WithPos<>(pos, new Expr.New(classCall));
+    }
     // if (node.is(NEW_EXPR)) {
     //   var struct = expr(node.child(EXPR));
     //   var newBody = node.peekChild(NEW_BODY);
diff --git a/syntax/src/main/java/org/aya/syntax/core/def/AnyDef.java b/syntax/src/main/java/org/aya/syntax/core/def/AnyDef.java
index bf03af561..0a2ab30e0 100644
--- a/syntax/src/main/java/org/aya/syntax/core/def/AnyDef.java
+++ b/syntax/src/main/java/org/aya/syntax/core/def/AnyDef.java
@@ -61,13 +61,5 @@ public sealed interface AnyDef extends OpDecl permits JitDef, ClassDefLike, ConD
     };
   }
 
-  static @NotNull boolean equals(@NotNull AnyDef lhs, @NotNull AnyDef rhs) {
-    return switch (new Pair<>(lhs, rhs)) {
-      case Pair(JitDef jlhs, JitDef jrhs) -> jlhs == jrhs;
-      case Pair(TyckAnyDef<?> tlhs, TyckAnyDef<?> trhs) -> tlhs.ref == trhs.ref;
-      default -> throw new UnsupportedOperationException("TODO");
-    };
-  }
-
   @NotNull AbstractTele signature();
 }
diff --git a/syntax/src/main/java/org/aya/syntax/core/term/call/MemberCall.java b/syntax/src/main/java/org/aya/syntax/core/term/call/MemberCall.java
index f141fb88f..b3bfabb71 100644
--- a/syntax/src/main/java/org/aya/syntax/core/term/call/MemberCall.java
+++ b/syntax/src/main/java/org/aya/syntax/core/term/call/MemberCall.java
@@ -37,15 +37,6 @@ private MemberCall update(Term clazz, ImmutableSeq<Term> newArgs) {
     return make(new MemberCall(of, ref, ulift, args));
   }
 
-  public static @NotNull Term make(
-    @NotNull Term of,
-    @NotNull MemberDefLike ref,
-    int ulift,
-    @NotNull ImmutableSeq<@NotNull Term> args
-  ) {
-    return make(new MemberCall(of, ref, ulift, args));
-  }
-
   public static @NotNull Term make(@NotNull MemberCall call) {
     return switch (call.of()) {
       case NewTerm neu -> {

From b5c1938f943882f605d7756a56a33b1e60b01206 Mon Sep 17 00:00:00 2001
From: HoshinoTented <hoshinotented@qq.com>
Date: Sun, 7 Jul 2024 09:24:28 +0800
Subject: [PATCH 19/33] conversion: remove something

---
 .../java/org/aya/unify/TermComparator.java     | 18 +++++++-----------
 1 file changed, 7 insertions(+), 11 deletions(-)

diff --git a/base/src/main/java/org/aya/unify/TermComparator.java b/base/src/main/java/org/aya/unify/TermComparator.java
index 761c2db19..df9eaac6f 100644
--- a/base/src/main/java/org/aya/unify/TermComparator.java
+++ b/base/src/main/java/org/aya/unify/TermComparator.java
@@ -121,13 +121,6 @@ private <R> R swapped(@NotNull Supplier<R> callback) {
     return result;
   }
 
-  private <L, R, T> T swapped(@NotNull L lhs, @NotNull R rhs, @NotNull BiFunction<R, L, T> callback) {
-    cmp = cmp.invert();
-    var result = callback.apply(rhs, lhs);
-    cmp = cmp.invert();
-    return result;
-  }
-
   /**
    * Compare two terms with the given {@param type} (if not null)
    *
@@ -148,7 +141,8 @@ public boolean compare(@NotNull Term preLhs, @NotNull Term preRhs, @Nullable Ter
       // prefer solving the IsType one as the OfType one.
       if (lhs instanceof MetaCall lMeta && lMeta.ref().req() == MetaVar.Misc.IsType)
         return solveMeta(lMeta, rMeta, type) != null;
-      return swapped(lhs, rMeta, (r, l) -> solveMeta(r, l, type)) != null;
+      var llhs = lhs;
+      return swapped(() -> solveMeta(rMeta, llhs, type)) != null;
     }
     // ^ Beware of the order!!
     if (lhs instanceof MetaCall lMeta) {
@@ -253,9 +247,11 @@ case SigmaTerm(var paramSeq) -> {
     }
 
     Term result;
-    if (rhs instanceof MetaCall || rhs instanceof MetaLitTerm)
-      result = swapped(lhs, rhs, this::doCompareUntyped);
-    else {
+    if (rhs instanceof MetaCall || rhs instanceof MetaLitTerm) {
+      var llhs = lhs;
+      var rrhs = rhs;
+      result = swapped(() -> doCompareUntyped(rrhs, llhs));
+    } else {
       if (rhs instanceof MemberCall && !(lhs instanceof MemberCall)) {
         var tmp = lhs;
         lhs = rhs;

From 06da7d8012a5f5b6e5484553229d7f25c92e07b6 Mon Sep 17 00:00:00 2001
From: HoshinoTented <hoshinotented@qq.com>
Date: Sun, 7 Jul 2024 09:29:04 +0800
Subject: [PATCH 20/33] misc: fix unresolved meta

---
 base/src/main/java/org/aya/tyck/ExprTycker.java     | 6 +++++-
 cli-impl/src/test/resources/success/src/Classes.aya | 2 +-
 2 files changed, 6 insertions(+), 2 deletions(-)

diff --git a/base/src/main/java/org/aya/tyck/ExprTycker.java b/base/src/main/java/org/aya/tyck/ExprTycker.java
index fab419997..dc59efa53 100644
--- a/base/src/main/java/org/aya/tyck/ExprTycker.java
+++ b/base/src/main/java/org/aya/tyck/ExprTycker.java
@@ -172,9 +172,13 @@ case PiTerm(var dom, var cod) -> {
           if (clazz.args().size() == resultClazz.args().size()) return result;
           var forget = resultClazz.args().drop(clazz.args().size());
           return new Jdg.Default(new ClassCastTerm(clazz.ref(), result.wellTyped(), clazz.args(), forget), type);
+        } else {
+          // TODO: skip unifyTyReported below
         }
       }
-    } else if (unifyTyReported(type, resultType, expr)) return result;
+    }
+
+    if (unifyTyReported(type, resultType, expr)) return result;
 
     return new Jdg.Default(new ErrorTerm(result.wellTyped()), type);
   }
diff --git a/cli-impl/src/test/resources/success/src/Classes.aya b/cli-impl/src/test/resources/success/src/Classes.aya
index 3eadcfc08..c2695a522 100644
--- a/cli-impl/src/test/resources/success/src/Classes.aya
+++ b/cli-impl/src/test/resources/success/src/Classes.aya
@@ -4,4 +4,4 @@ class Kontainer
 | Taipe : Type
 | walue : Taipe
 
-def norm0 : walue (new Kontainer Nat 0) = 0 => idp
+def norm0 : Kontainer::walue (new Kontainer Nat 0) = 0 => refl

From 3218d252882c568fcd68598e6e7458a556c8164b Mon Sep 17 00:00:00 2001
From: HoshinoTented <hoshinotented@qq.com>
Date: Sun, 7 Jul 2024 21:43:13 +0800
Subject: [PATCH 21/33] class: omg, it passes

---
 .../main/java/org/aya/tyck/tycker/AppTycker.java | 16 ++++++++++------
 .../src/test/resources/success/src/Classes.aya   |  4 +++-
 .../org/aya/syntax/core/term/ClassCastTerm.java  |  2 +-
 3 files changed, 14 insertions(+), 8 deletions(-)

diff --git a/base/src/main/java/org/aya/tyck/tycker/AppTycker.java b/base/src/main/java/org/aya/tyck/tycker/AppTycker.java
index d2434597a..ec3a8a74e 100644
--- a/base/src/main/java/org/aya/tyck/tycker/AppTycker.java
+++ b/base/src/main/java/org/aya/tyck/tycker/AppTycker.java
@@ -5,6 +5,7 @@
 import kala.collection.Seq;
 import kala.collection.SeqView;
 import kala.collection.immutable.ImmutableArray;
+import kala.collection.immutable.ImmutableSeq;
 import kala.function.CheckedBiFunction;
 import org.aya.generic.stmt.Shaped;
 import org.aya.syntax.compile.JitCon;
@@ -12,12 +13,10 @@
 import org.aya.syntax.compile.JitFn;
 import org.aya.syntax.compile.JitPrim;
 import org.aya.syntax.concrete.stmt.decl.*;
+import org.aya.syntax.core.Closure;
 import org.aya.syntax.core.def.*;
 import org.aya.syntax.core.repr.AyaShape;
-import org.aya.syntax.core.term.FreeTerm;
-import org.aya.syntax.core.term.SigmaTerm;
-import org.aya.syntax.core.term.SortTerm;
-import org.aya.syntax.core.term.Term;
+import org.aya.syntax.core.term.*;
 import org.aya.syntax.core.term.call.*;
 import org.aya.syntax.ref.DefVar;
 import org.aya.syntax.ref.LocalVar;
@@ -203,14 +202,19 @@ record TakeMembers(
       // teleArgs are former members
       assert i < telescopeSize;
       var member = clazz.members().get(i);
-      return TyckDef.defSignature(member.ref()).makePi(Seq.of(new FreeTerm(self)));
+      return TyckDef.defSignature(member.ref()).inst(ImmutableSeq.of(new NewTerm(
+        new ClassCall(new ClassDef.Delegate(clazz.ref()), 0,
+          ImmutableSeq.fill(clazz.members().size(), idx -> Closure.mkConst(idx < teleArgs.size() ? teleArgs.get(idx) : ErrorTerm.DUMMY))
+        )
+      ))).makePi(Seq.empty());
     }
+
     @Override public @NotNull Term result(Seq<Term> teleArgs) {
       return clazz.members().view()
         .drop(telescopeSize)
         .map(member -> TyckDef.defSignature(member.ref()).makePi(Seq.of(new FreeTerm(self))))
         .map(ty -> (SortTerm) synthesizer.synth(ty))
-        .reduce(SigmaTerm::lub);
+        .foldLeft(SortTerm.Type0, SigmaTerm::lub);
     }
     @Override public @NotNull SeqView<String> namesView() {
       return clazz.members().sliceView(0, telescopeSize).map(i -> i.ref().name());
diff --git a/cli-impl/src/test/resources/success/src/Classes.aya b/cli-impl/src/test/resources/success/src/Classes.aya
index c2695a522..47c4b7df1 100644
--- a/cli-impl/src/test/resources/success/src/Classes.aya
+++ b/cli-impl/src/test/resources/success/src/Classes.aya
@@ -4,4 +4,6 @@ class Kontainer
 | Taipe : Type
 | walue : Taipe
 
-def norm0 : Kontainer::walue (new Kontainer Nat 0) = 0 => refl
+def tyck0 : Nat => Kontainer::walue {new Kontainer Nat 0}
+
+// def norm0 : Kontainer::walue {new Kontainer Nat 0} = 0 => refl
diff --git a/syntax/src/main/java/org/aya/syntax/core/term/ClassCastTerm.java b/syntax/src/main/java/org/aya/syntax/core/term/ClassCastTerm.java
index 238eeb7b5..8ef9541ec 100644
--- a/syntax/src/main/java/org/aya/syntax/core/term/ClassCastTerm.java
+++ b/syntax/src/main/java/org/aya/syntax/core/term/ClassCastTerm.java
@@ -50,7 +50,7 @@ public record ClassCastTerm(
   }
 
   public @Nullable Closure get(@NotNull MemberDefLike member) {
-    assert ref == member.classRef();
+    assert ref.equals(member.classRef());
     var idx = member.index();
     if (idx < remember.size()) return remember.get(idx);
     idx = idx - remember.size();

From 8e33f0ca34cbf5dadb8a46b14c9e54ae8ba39ee9 Mon Sep 17 00:00:00 2001
From: HoshinoTented <hoshinotented@qq.com>
Date: Sun, 7 Jul 2024 21:43:44 +0800
Subject: [PATCH 22/33] class: add more test

---
 cli-impl/src/test/resources/success/src/Classes.aya | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/cli-impl/src/test/resources/success/src/Classes.aya b/cli-impl/src/test/resources/success/src/Classes.aya
index 47c4b7df1..8df70f758 100644
--- a/cli-impl/src/test/resources/success/src/Classes.aya
+++ b/cli-impl/src/test/resources/success/src/Classes.aya
@@ -6,4 +6,4 @@ class Kontainer
 
 def tyck0 : Nat => Kontainer::walue {new Kontainer Nat 0}
 
-// def norm0 : Kontainer::walue {new Kontainer Nat 0} = 0 => refl
+ def norm0 : Kontainer::walue {new Kontainer Nat 0} = 0 => refl

From a1247a726532b2c1458bac98cf1137090ac7d2db Mon Sep 17 00:00:00 2001
From: ice1000 <ice1000kotlin@foxmail.com>
Date: Mon, 8 Jul 2024 13:03:42 -0400
Subject: [PATCH 23/33] normalize: `MemberCall` extends `BetaRedex`

---
 .../main/java/org/aya/normalize/Normalizer.java |  5 -----
 .../aya/syntax/core/term/call/MemberCall.java   | 17 +++++++++--------
 .../aya/syntax/core/term/marker/BetaRedex.java  |  3 ++-
 3 files changed, 11 insertions(+), 14 deletions(-)

diff --git a/base/src/main/java/org/aya/normalize/Normalizer.java b/base/src/main/java/org/aya/normalize/Normalizer.java
index fd5048a16..f2f5226fa 100644
--- a/base/src/main/java/org/aya/normalize/Normalizer.java
+++ b/base/src/main/java/org/aya/normalize/Normalizer.java
@@ -82,11 +82,6 @@ case FnCall(var fn, int ulift, var args) -> switch (fn) {
           ? apply(fnRule.toFnCall())
           : reduceRule;
       }
-      case MemberCall memberCall -> {
-        var result = MemberCall.make(memberCall);
-        if (result != memberCall) yield apply(result);
-        yield defaultValue;
-      }
       case ConCall(var head, _) when !head.ref().hasEq() -> defaultValue;
       case ConCall call when call.conArgs().getLast() instanceof DimTerm dim ->
         call.head().ref().equality(call.args(), dim == DimTerm.I0);
diff --git a/syntax/src/main/java/org/aya/syntax/core/term/call/MemberCall.java b/syntax/src/main/java/org/aya/syntax/core/term/call/MemberCall.java
index b3bfabb71..484737918 100644
--- a/syntax/src/main/java/org/aya/syntax/core/term/call/MemberCall.java
+++ b/syntax/src/main/java/org/aya/syntax/core/term/call/MemberCall.java
@@ -8,6 +8,7 @@
 import org.aya.syntax.core.term.ClassCastTerm;
 import org.aya.syntax.core.term.NewTerm;
 import org.aya.syntax.core.term.Term;
+import org.aya.syntax.core.term.marker.BetaRedex;
 import org.jetbrains.annotations.NotNull;
 
 public record MemberCall(
@@ -15,7 +16,7 @@ public record MemberCall(
   @Override @NotNull MemberDefLike ref,
   @Override int ulift,
   @Override @NotNull ImmutableSeq<@NotNull Term> args
-) implements Callable.Tele {
+) implements Callable.Tele, BetaRedex {
   private MemberCall update(Term clazz, ImmutableSeq<Term> newArgs) {
     return clazz == of && newArgs.sameElements(args, true) ? this
       : new MemberCall(clazz, ref, ulift, newArgs);
@@ -34,23 +35,23 @@ private MemberCall update(Term clazz, ImmutableSeq<Term> newArgs) {
   ) {
     var impl = typeOfOf.get(ref);
     if (impl != null) return impl.apply(of);
-    return make(new MemberCall(of, ref, ulift, args));
+    return new MemberCall(of, ref, ulift, args).make();
   }
 
-  public static @NotNull Term make(@NotNull MemberCall call) {
-    return switch (call.of()) {
+  public @NotNull Term make() {
+    return switch (of()) {
       case NewTerm neu -> {
-        var impl = neu.inner().get(call.ref);
+        var impl = neu.inner().get(ref);
         assert impl != null;    // NewTerm is always fully applied
         yield impl.apply(neu);
       }
       case ClassCastTerm cast -> {
-        var impl = cast.get(call.ref);
+        var impl = cast.get(ref);
         if (impl != null) yield impl.apply(cast);
         // no impl, try inner
-        yield call.update(cast.subterm(), call.args);
+        yield update(cast.subterm(), args);
       }
-      default -> call;
+      default -> this;
     };
   }
 }
diff --git a/syntax/src/main/java/org/aya/syntax/core/term/marker/BetaRedex.java b/syntax/src/main/java/org/aya/syntax/core/term/marker/BetaRedex.java
index 167352e3d..71a911869 100644
--- a/syntax/src/main/java/org/aya/syntax/core/term/marker/BetaRedex.java
+++ b/syntax/src/main/java/org/aya/syntax/core/term/marker/BetaRedex.java
@@ -5,9 +5,10 @@
 import org.aya.syntax.core.term.AppTerm;
 import org.aya.syntax.core.term.ProjTerm;
 import org.aya.syntax.core.term.Term;
+import org.aya.syntax.core.term.call.MemberCall;
 import org.aya.syntax.core.term.xtt.PAppTerm;
 import org.jetbrains.annotations.NotNull;
 
-public sealed interface BetaRedex extends Term permits AppTerm, PAppTerm, ProjTerm {
+public sealed interface BetaRedex extends Term permits AppTerm, ProjTerm, MemberCall, PAppTerm {
   @NotNull Term make();
 }

From 2fb4b5a4a2a0c9ed762886d5f317e19913362404 Mon Sep 17 00:00:00 2001
From: ice1000 <ice1000kotlin@foxmail.com>
Date: Mon, 8 Jul 2024 13:10:02 -0400
Subject: [PATCH 24/33] class: code review

---
 .../main/java/org/aya/producer/AyaProducer.java   | 15 ---------------
 .../main/java/org/aya/syntax/core/def/AnyDef.java |  1 -
 .../java/org/aya/syntax/core/def/MemberDef.java   |  5 +----
 3 files changed, 1 insertion(+), 20 deletions(-)

diff --git a/producer/src/main/java/org/aya/producer/AyaProducer.java b/producer/src/main/java/org/aya/producer/AyaProducer.java
index 577e42c39..561faa0ca 100644
--- a/producer/src/main/java/org/aya/producer/AyaProducer.java
+++ b/producer/src/main/java/org/aya/producer/AyaProducer.java
@@ -567,21 +567,6 @@ private record DeclNameOrInfix(@NotNull WithPos<String> name, @Nullable OpDecl.O
       var classCall = expr(node.child(EXPR));
       return new WithPos<>(pos, new Expr.New(classCall));
     }
-    // if (node.is(NEW_EXPR)) {
-    //   var struct = expr(node.child(EXPR));
-    //   var newBody = node.peekChild(NEW_BODY);
-    //   return new WithPos<>(pos, new Expr.New(pos, struct,
-    //     newBody == null
-    //       ? ImmutableSeq.empty()
-    //       : newBody.childrenOfType(NEW_ARG).map(arg -> {
-    //         var id = newArgField(arg.child(NEW_ARG_FIELD));
-    //         var bindings = arg.childrenOfType(TELE_PARAM_NAME).map(this::teleParamName)
-    //           .map(b -> b.map(_ -> LocalVar.from(b)))
-    //           .toImmutableSeq();
-    //         var body = expr(arg.child(EXPR));
-    //         return new WithPos<>(pos, new Expr.Field<>(sourcePosOf(arg), id, bindings, body, MutableValue.create()));
-    //       }).toImmutableSeq()));
-    // }
     if (node.is(PI_EXPR)) return Expr.buildPi(pos,
       telescope(node.childrenOfType(TELE)).view(),
       expr(node.child(EXPR)));
diff --git a/syntax/src/main/java/org/aya/syntax/core/def/AnyDef.java b/syntax/src/main/java/org/aya/syntax/core/def/AnyDef.java
index 0a2ab30e0..bd8a95141 100644
--- a/syntax/src/main/java/org/aya/syntax/core/def/AnyDef.java
+++ b/syntax/src/main/java/org/aya/syntax/core/def/AnyDef.java
@@ -6,7 +6,6 @@
 import org.aya.syntax.compile.JitDef;
 import org.aya.syntax.ref.*;
 import org.aya.syntax.telescope.AbstractTele;
-import org.aya.util.Pair;
 import org.aya.util.binop.Assoc;
 import org.aya.util.binop.OpDecl;
 import org.jetbrains.annotations.NotNull;
diff --git a/syntax/src/main/java/org/aya/syntax/core/def/MemberDef.java b/syntax/src/main/java/org/aya/syntax/core/def/MemberDef.java
index d1020a751..b52b1b39c 100644
--- a/syntax/src/main/java/org/aya/syntax/core/def/MemberDef.java
+++ b/syntax/src/main/java/org/aya/syntax/core/def/MemberDef.java
@@ -34,10 +34,7 @@ public static final class Delegate extends TyckAnyDef<MemberDef> implements Memb
     /**
      * this implementation prevents invocation of {@link ClassDef.Delegate#members()} while tycking {@link ClassDef}
      */
-    @Override
-    public int index() {
-      return ref.core.index;
-    }
+    @Override public int index() { return ref.core.index; }
 
     @Override public @NotNull ClassDefLike classRef() {
       return new ClassDef.Delegate(core().classRef());

From a0459b7cedc50d7690feaee2d8bb36ea5382c983 Mon Sep 17 00:00:00 2001
From: HoshinoTented <hoshinotented@qq.com>
Date: Tue, 9 Jul 2024 10:29:01 +0800
Subject: [PATCH 25/33] member: beta redux

---
 .../main/java/org/aya/syntax/core/term/call/MemberCall.java  | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/syntax/src/main/java/org/aya/syntax/core/term/call/MemberCall.java b/syntax/src/main/java/org/aya/syntax/core/term/call/MemberCall.java
index 484737918..e436a47b5 100644
--- a/syntax/src/main/java/org/aya/syntax/core/term/call/MemberCall.java
+++ b/syntax/src/main/java/org/aya/syntax/core/term/call/MemberCall.java
@@ -26,6 +26,11 @@ private MemberCall update(Term clazz, ImmutableSeq<Term> newArgs) {
     return update(f.apply(0, of), Callable.descent(args, f));
   }
 
+  @Override
+  public @NotNull Term make() {
+    return make(this);
+  }
+
   public static @NotNull Term make(
     @NotNull ClassCall typeOfOf,
     @NotNull Term of,

From bd870c4f41f018b96e12e4118bb1cb4b77e9b7db Mon Sep 17 00:00:00 2001
From: ice1000 <ice1000kotlin@foxmail.com>
Date: Tue, 9 Jul 2024 18:49:46 -0400
Subject: [PATCH 26/33] revert: previous commit

---
 .../java/org/aya/syntax/core/term/call/MemberCall.java     | 7 +------
 1 file changed, 1 insertion(+), 6 deletions(-)

diff --git a/syntax/src/main/java/org/aya/syntax/core/term/call/MemberCall.java b/syntax/src/main/java/org/aya/syntax/core/term/call/MemberCall.java
index e436a47b5..d5d9dcdc1 100644
--- a/syntax/src/main/java/org/aya/syntax/core/term/call/MemberCall.java
+++ b/syntax/src/main/java/org/aya/syntax/core/term/call/MemberCall.java
@@ -26,11 +26,6 @@ private MemberCall update(Term clazz, ImmutableSeq<Term> newArgs) {
     return update(f.apply(0, of), Callable.descent(args, f));
   }
 
-  @Override
-  public @NotNull Term make() {
-    return make(this);
-  }
-
   public static @NotNull Term make(
     @NotNull ClassCall typeOfOf,
     @NotNull Term of,
@@ -43,7 +38,7 @@ private MemberCall update(Term clazz, ImmutableSeq<Term> newArgs) {
     return new MemberCall(of, ref, ulift, args).make();
   }
 
-  public @NotNull Term make() {
+  @Override public @NotNull Term make() {
     return switch (of()) {
       case NewTerm neu -> {
         var impl = neu.inner().get(ref);

From 3442d051968cf22729bc614402bd55f0a8ad7878 Mon Sep 17 00:00:00 2001
From: HoshinoTented <hoshinotented@qq.com>
Date: Thu, 11 Jul 2024 20:03:22 +0800
Subject: [PATCH 27/33] class: error

---
 .../main/java/org/aya/tyck/ExprTycker.java    |  5 ++-
 .../java/org/aya/tyck/error/ClassError.java   | 33 +++++++++++++++++++
 .../java/org/aya/tyck/tycker/AppTycker.java   |  2 +-
 .../java/org/aya/unify/TermComparator.java    |  2 +-
 .../test/java/org/aya/test/TestRunner.java    |  3 +-
 .../org/aya/test/fixtures/ClassError.java     | 19 +++++++++++
 6 files changed, 58 insertions(+), 6 deletions(-)
 create mode 100644 base/src/main/java/org/aya/tyck/error/ClassError.java
 create mode 100644 cli-impl/src/test/java/org/aya/test/fixtures/ClassError.java

diff --git a/base/src/main/java/org/aya/tyck/ExprTycker.java b/base/src/main/java/org/aya/tyck/ExprTycker.java
index 47a261da1..41e2855ac 100644
--- a/base/src/main/java/org/aya/tyck/ExprTycker.java
+++ b/base/src/main/java/org/aya/tyck/ExprTycker.java
@@ -343,13 +343,12 @@ yield subscoped(param.ref(), wellParam, () ->
       case Expr.New neutron -> {
         var wellTyped = synthesize(neutron.classCall());
         if (!(wellTyped.wellTyped() instanceof ClassCall call)) {
-          // TODO
-          throw new UnsupportedOperationException("TODO");
+          yield fail(expr.data(), new ClassError.NotClassCall(neutron.classCall()));
         }
 
         // check whether the call is fully applied
         if (call.args().size() != call.ref().members().size()) {
-          throw new UnsupportedOperationException("TODO");
+          yield fail(expr.data(), new ClassError.NotFullyApplied(neutron.classCall()));
         }
 
         yield new Jdg.Default(new NewTerm(call), call);
diff --git a/base/src/main/java/org/aya/tyck/error/ClassError.java b/base/src/main/java/org/aya/tyck/error/ClassError.java
new file mode 100644
index 000000000..9074af807
--- /dev/null
+++ b/base/src/main/java/org/aya/tyck/error/ClassError.java
@@ -0,0 +1,33 @@
+// Copyright (c) 2020-2024 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.error;
+
+import org.aya.pretty.doc.Doc;
+import org.aya.syntax.concrete.Expr;
+import org.aya.util.error.SourcePos;
+import org.aya.util.error.WithPos;
+import org.aya.util.prettier.PrettierOptions;
+import org.jetbrains.annotations.NotNull;
+
+public interface ClassError extends TyckError {
+  @NotNull WithPos<Expr> problemExpr();
+
+  @Override
+  default @NotNull SourcePos sourcePos() {
+    return problemExpr().sourcePos();
+  }
+
+  record NotClassCall(@Override @NotNull WithPos<Expr> problemExpr) implements ClassError {
+    @Override
+    public @NotNull Doc describe(@NotNull PrettierOptions options) {
+      return Doc.sep(Doc.english("Unable to new a non-class type:"), Doc.code(problemExpr.data().toDoc(options)));
+    }
+  }
+
+  record NotFullyApplied(@Override @NotNull WithPos<Expr> problemExpr) implements ClassError {
+    @Override
+    public @NotNull Doc describe(@NotNull PrettierOptions options) {
+      return Doc.sep(Doc.english("Unable to new an incomplete class type:"), Doc.code(problemExpr.data().toDoc(options)));
+    }
+  }
+}
diff --git a/base/src/main/java/org/aya/tyck/tycker/AppTycker.java b/base/src/main/java/org/aya/tyck/tycker/AppTycker.java
index ec3a8a74e..7e5a206dd 100644
--- a/base/src/main/java/org/aya/tyck/tycker/AppTycker.java
+++ b/base/src/main/java/org/aya/tyck/tycker/AppTycker.java
@@ -212,7 +212,7 @@ record TakeMembers(
     @Override public @NotNull Term result(Seq<Term> teleArgs) {
       return clazz.members().view()
         .drop(telescopeSize)
-        .map(member -> TyckDef.defSignature(member.ref()).makePi(Seq.of(new FreeTerm(self))))
+        .map(member -> TyckDef.defSignature(member.ref()).inst(ImmutableSeq.of(new FreeTerm(self))).makePi(Seq.empty()))
         .map(ty -> (SortTerm) synthesizer.synth(ty))
         .foldLeft(SortTerm.Type0, SigmaTerm::lub);
     }
diff --git a/base/src/main/java/org/aya/unify/TermComparator.java b/base/src/main/java/org/aya/unify/TermComparator.java
index df9eaac6f..71dd1b2b9 100644
--- a/base/src/main/java/org/aya/unify/TermComparator.java
+++ b/base/src/main/java/org/aya/unify/TermComparator.java
@@ -332,7 +332,7 @@ case ProjTerm(var lof, var ldx) -> {
         default -> null;
       };
       case MemberCall memberCall -> {
-        // it is impossible that memberCall.of() is an cast term, cause it is whnfed.
+        // it is impossible that memberCall.of() is a cast term, since it is whnfed.
         assert !(memberCall.of() instanceof ClassCastTerm);
         if (rhs instanceof MemberCall memberCarr) {
           assert !(memberCarr.of() instanceof ClassCastTerm);
diff --git a/cli-impl/src/test/java/org/aya/test/TestRunner.java b/cli-impl/src/test/java/org/aya/test/TestRunner.java
index 7c2cbb9f9..ded56d246 100644
--- a/cli-impl/src/test/java/org/aya/test/TestRunner.java
+++ b/cli-impl/src/test/java/org/aya/test/TestRunner.java
@@ -43,7 +43,8 @@ public class TestRunner {
       PatTyckError.class,
       OperatorError.class,
       TerckError.class,
-      PatCohError.class
+      PatCohError.class,
+      ClassError.class
     ).forEachChecked(TestRunner::expectFixture);
     Files.deleteIfExists(TMP_FILE);
   }
diff --git a/cli-impl/src/test/java/org/aya/test/fixtures/ClassError.java b/cli-impl/src/test/java/org/aya/test/fixtures/ClassError.java
new file mode 100644
index 000000000..18afca89c
--- /dev/null
+++ b/cli-impl/src/test/java/org/aya/test/fixtures/ClassError.java
@@ -0,0 +1,19 @@
+// Copyright (c) 2020-2024 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.test.fixtures;
+
+import org.intellij.lang.annotations.Language;
+
+public interface ClassError {
+  @Language("Aya") String testNotClassCall = """
+    def what (A : Type) : A => new A
+    """;
+
+  @Language("Aya") String testNotFullyApplied = """
+    inductive Nat | O | S Nat
+    class Kontainer
+    | walue : Nat
+
+    def what : Kontainer => new Kontainer
+    """;
+}

From 397a6f6fcbf3601e4d447bdad632e2ede74dcf2c Mon Sep 17 00:00:00 2001
From: HoshinoTented <hoshinotented@qq.com>
Date: Thu, 11 Jul 2024 20:03:58 +0800
Subject: [PATCH 28/33] test: missing

---
 .../test/resources/negative/ClassError.txt    | 24 +++++++++++++++++++
 1 file changed, 24 insertions(+)
 create mode 100644 cli-impl/src/test/resources/negative/ClassError.txt

diff --git a/cli-impl/src/test/resources/negative/ClassError.txt b/cli-impl/src/test/resources/negative/ClassError.txt
new file mode 100644
index 000000000..8f3427395
--- /dev/null
+++ b/cli-impl/src/test/resources/negative/ClassError.txt
@@ -0,0 +1,24 @@
+NotClassCall:
+In file $FILE:1:31 ->
+
+  1 │   def what (A : Type) : A => new A
+    │                                  ╰╯
+
+Error: Unable to new a non-class type: `A`
+
+1 error(s), 0 warning(s).
+Let's learn from that.
+
+NotFullyApplied:
+In file $FILE:5:28 ->
+
+  3 │   | walue : Nat
+  4 │   
+  5 │   def what : Kontainer => new Kontainer
+    │                               ╰───────╯
+
+Error: Unable to new an incomplete class type: `Kontainer`
+
+1 error(s), 0 warning(s).
+Let's learn from that.
+

From a6e9a4f3389deb2ad1579702f86ac209049f68d8 Mon Sep 17 00:00:00 2001
From: ice1000 <ice1000kotlin@foxmail.com>
Date: Fri, 12 Jul 2024 13:11:09 -0400
Subject: [PATCH 29/33] class: code review, do not compute all the types

---
 .../main/java/org/aya/tyck/ExprTycker.java    | 41 +++++++++----------
 .../java/org/aya/tyck/error/ClassError.java   | 11 ++---
 .../java/org/aya/tyck/tycker/AppTycker.java   | 10 ++---
 .../java/org/aya/unify/TermComparator.java    |  4 +-
 .../java/org/aya/syntax/concrete/Expr.java    |  9 +---
 5 files changed, 29 insertions(+), 46 deletions(-)

diff --git a/base/src/main/java/org/aya/tyck/ExprTycker.java b/base/src/main/java/org/aya/tyck/ExprTycker.java
index 41e2855ac..ed489f0f1 100644
--- a/base/src/main/java/org/aya/tyck/ExprTycker.java
+++ b/base/src/main/java/org/aya/tyck/ExprTycker.java
@@ -2,11 +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;
 
-import kala.collection.immutable.ImmutableMap;
 import kala.collection.immutable.ImmutableSeq;
 import kala.collection.immutable.ImmutableTreeSeq;
 import kala.collection.mutable.MutableList;
-import kala.collection.mutable.MutableMap;
 import kala.collection.mutable.MutableStack;
 import kala.collection.mutable.MutableTreeSet;
 import kala.control.Result;
@@ -15,7 +13,6 @@
 import org.aya.syntax.concrete.Expr;
 import org.aya.syntax.core.Closure;
 import org.aya.syntax.core.def.DataDefLike;
-import org.aya.syntax.core.def.MemberDefLike;
 import org.aya.syntax.core.def.PrimDef;
 import org.aya.syntax.core.repr.AyaShape;
 import org.aya.syntax.core.term.*;
@@ -176,7 +173,7 @@ case PiTerm(var dom, var cod) -> {
           var forget = resultClazz.args().drop(clazz.args().size());
           return new Jdg.Default(new ClassCastTerm(clazz.ref(), result.wellTyped(), clazz.args(), forget), type);
         } else {
-          // TODO: skip unifyTyReported below
+          return makeErrorResult(type, result);
         }
       }
     }
@@ -340,15 +337,15 @@ yield subscoped(param.ref(), wellParam, () ->
         var type = new DataCall(def, 0, ImmutableSeq.of(elementTy));
         yield new Jdg.Default(new ListTerm(results, match.recog(), type), type);
       }
-      case Expr.New neutron -> {
-        var wellTyped = synthesize(neutron.classCall());
+      case Expr.New(var classCall) -> {
+        var wellTyped = synthesize(classCall);
         if (!(wellTyped.wellTyped() instanceof ClassCall call)) {
-          yield fail(expr.data(), new ClassError.NotClassCall(neutron.classCall()));
+          yield fail(expr.data(), new ClassError.NotClassCall(classCall));
         }
 
         // check whether the call is fully applied
         if (call.args().size() != call.ref().members().size()) {
-          yield fail(expr.data(), new ClassError.NotFullyApplied(neutron.classCall()));
+          yield fail(expr.data(), new ClassError.NotFullyApplied(classCall));
         }
 
         yield new Jdg.Default(new NewTerm(call), call);
@@ -397,11 +394,11 @@ case CompiledVar(var content) -> new AppTycker<>(this, sourcePos, args.size(), l
 
   private Jdg computeArgs(
     @NotNull SourcePos pos, @NotNull ImmutableSeq<Expr.NamedArg> args,
-    @NotNull AbstractTele params, @NotNull BiFunction<Term[], Term[], Jdg> k
+    @NotNull AbstractTele params, @NotNull BiFunction<Term[], Term, Jdg> k
   ) throws NotPi {
     int argIx = 0, paramIx = 0;
     var result = new Term[params.telescopeSize()];
-    var types = new Term[params.telescopeSize()];
+    Term firstType = null;
     while (argIx < args.size() && paramIx < params.telescopeSize()) {
       var arg = args.get(argIx);
       var param = params.telescopeRich(paramIx, result);
@@ -412,39 +409,39 @@ private Jdg computeArgs(
           break;
         } else if (arg.name() == null) {
           // here, arg.explicit() == true and param.explicit() == false
-          result[paramIx] = insertImplicit(param, arg.sourcePos());
-          types[paramIx++] = param.type();
+          if (paramIx == 0) firstType = param.type();
+          result[paramIx++] = insertImplicit(param, arg.sourcePos());
           continue;
         }
       }
       if (arg.name() != null && !param.nameEq(arg.name())) {
-        result[paramIx] = insertImplicit(param, arg.sourcePos());
-        types[paramIx++] = param.type();
+        if (paramIx == 0) firstType = param.type();
+        result[paramIx++] = insertImplicit(param, arg.sourcePos());
         continue;
       }
       var what = inherit(arg.arg(), param.type());
-      result[paramIx] = what.wellTyped();
-      types[paramIx++] = what.type();
+      if (paramIx == 0) firstType = param.type();
+      result[paramIx++] = what.wellTyped();
       argIx++;
     }
     // Trailing implicits
     while (paramIx < params.telescopeSize()) {
       if (params.telescopeLicit(paramIx)) break;
       var param = params.telescopeRich(paramIx, result);
-      result[paramIx] = insertImplicit(param, pos);
-      types[paramIx++] = param.type();
+      if (paramIx == 0) firstType = param.type();
+      result[paramIx++] = insertImplicit(param, pos);
     }
     var extraParams = MutableStack.<Pair<LocalVar, Term>>create();
     if (argIx < args.size()) {
-      return generateApplication(args.drop(argIx), k.apply(result, types));
+      return generateApplication(args.drop(argIx), k.apply(result, firstType));
     } else while (paramIx < params.telescopeSize()) {
       var param = params.telescopeRich(paramIx, result);
       var atarashiVar = LocalVar.generate(param.name());
       extraParams.push(new Pair<>(atarashiVar, param.type()));
-      result[paramIx] = new FreeTerm(atarashiVar);
-      types[paramIx++] = param.type();
+      if (paramIx == 0) firstType = param.type();
+      result[paramIx++] = new FreeTerm(atarashiVar);
     }
-    var generated = k.apply(result, types);
+    var generated = k.apply(result, firstType);
     while (extraParams.isNotEmpty()) {
       var pair = extraParams.pop();
       generated = new Jdg.Default(
diff --git a/base/src/main/java/org/aya/tyck/error/ClassError.java b/base/src/main/java/org/aya/tyck/error/ClassError.java
index 9074af807..bc6954a8a 100644
--- a/base/src/main/java/org/aya/tyck/error/ClassError.java
+++ b/base/src/main/java/org/aya/tyck/error/ClassError.java
@@ -12,21 +12,16 @@
 public interface ClassError extends TyckError {
   @NotNull WithPos<Expr> problemExpr();
 
-  @Override
-  default @NotNull SourcePos sourcePos() {
-    return problemExpr().sourcePos();
-  }
+  @Override default @NotNull SourcePos sourcePos() { return problemExpr().sourcePos(); }
 
   record NotClassCall(@Override @NotNull WithPos<Expr> problemExpr) implements ClassError {
-    @Override
-    public @NotNull Doc describe(@NotNull PrettierOptions options) {
+    @Override public @NotNull Doc describe(@NotNull PrettierOptions options) {
       return Doc.sep(Doc.english("Unable to new a non-class type:"), Doc.code(problemExpr.data().toDoc(options)));
     }
   }
 
   record NotFullyApplied(@Override @NotNull WithPos<Expr> problemExpr) implements ClassError {
-    @Override
-    public @NotNull Doc describe(@NotNull PrettierOptions options) {
+    @Override public @NotNull Doc describe(@NotNull PrettierOptions options) {
       return Doc.sep(Doc.english("Unable to new an incomplete class type:"), Doc.code(problemExpr.data().toDoc(options)));
     }
   }
diff --git a/base/src/main/java/org/aya/tyck/tycker/AppTycker.java b/base/src/main/java/org/aya/tyck/tycker/AppTycker.java
index 7e5a206dd..cb0d6b96b 100644
--- a/base/src/main/java/org/aya/tyck/tycker/AppTycker.java
+++ b/base/src/main/java/org/aya/tyck/tycker/AppTycker.java
@@ -30,14 +30,12 @@
 import org.jetbrains.annotations.Nullable;
 
 import java.util.function.BiFunction;
-import java.util.function.Function;
 
 public record AppTycker<Ex extends Exception>(
   @Override @NotNull TyckState state,
   @NotNull AbstractTycker tycker,
   @NotNull SourcePos pos,
-  int argsCount,
-  int lift,
+  int argsCount, int lift,
   @NotNull Factory<Ex> makeArgs
 ) implements Stateful {
   /**
@@ -52,7 +50,7 @@ public record AppTycker<Ex extends Exception>(
    */
   @FunctionalInterface
   public interface Factory<Ex extends Exception> extends
-    CheckedBiFunction<AbstractTele, BiFunction<Term[], Term[], Jdg>, Jdg, Ex> {
+    CheckedBiFunction<AbstractTele, BiFunction<Term[], Term, Jdg>, Jdg, Ex> {
   }
 
   public AppTycker(
@@ -164,9 +162,9 @@ public AppTycker(
 
   private @NotNull Jdg checkProjCall(@NotNull MemberDefLike member) throws Ex {
     var signature = member.signature().lift(lift);
-    return makeArgs.applyChecked(signature, (args, ty) -> {
+    return makeArgs.applyChecked(signature, (args, fstTy) -> {
       assert args.length >= 1;
-      var ofTy = whnf(ty[0]);
+      var ofTy = whnf(fstTy);
       if (!(ofTy instanceof ClassCall classTy)) throw new UnsupportedOperationException("report");   // TODO
       var fieldArgs = ImmutableArray.fill(args.length - 1, i -> args[i + 1]);
       return new Jdg.Default(
diff --git a/base/src/main/java/org/aya/unify/TermComparator.java b/base/src/main/java/org/aya/unify/TermComparator.java
index 71dd1b2b9..045d4295c 100644
--- a/base/src/main/java/org/aya/unify/TermComparator.java
+++ b/base/src/main/java/org/aya/unify/TermComparator.java
@@ -33,7 +33,6 @@
 import org.jetbrains.annotations.Nullable;
 
 import java.util.Objects;
-import java.util.function.BiFunction;
 import java.util.function.Function;
 import java.util.function.Supplier;
 import java.util.function.UnaryOperator;
@@ -178,12 +177,11 @@ private boolean checkApproxResult(@Nullable Term type, Term approxResult) {
    */
   private boolean doCompareTyped(@NotNull Term lhs, @NotNull Term rhs, @NotNull Term type) {
     return switch (whnf(type)) {
-      // TODO: ClassCall
       case LamTerm _, ConCallLike _, TupTerm _ -> Panic.unreachable();
       case ErrorTerm _ -> true;
       case ClassCall classCall -> {
         if (classCall.args().size() == classCall.ref().members().size()) yield true;
-        // TODO: should we compare fields that have impl?
+        // TODO: skip comparing fields that already have impl specified in the type
         yield classCall.ref().members().allMatch(member -> {
           // loop invariant: first [i] members are the "same". ([i] is the loop counter, count from 0)
           // Note that member can only refer to first [i] members, so it is safe that we supply [lhs] or [rhs]
diff --git a/syntax/src/main/java/org/aya/syntax/concrete/Expr.java b/syntax/src/main/java/org/aya/syntax/concrete/Expr.java
index cda6060ea..5a6916a97 100644
--- a/syntax/src/main/java/org/aya/syntax/concrete/Expr.java
+++ b/syntax/src/main/java/org/aya/syntax/concrete/Expr.java
@@ -318,9 +318,7 @@ record LitString(@NotNull String string) implements Expr {
     @Override public void forEach(@NotNull PosedConsumer<Expr> f) { }
   }
 
-  record New(
-    @NotNull WithPos<Expr> classCall
-  ) implements Expr {
+  record New(@NotNull WithPos<Expr> classCall) implements Expr {
     public @NotNull Expr.New update(@NotNull WithPos<Expr> classCall) {
       return classCall == classCall() ? this : new New(classCall);
     }
@@ -329,10 +327,7 @@ record New(
       return update(classCall.descent(f));
     }
 
-    @Override
-    public void forEach(@NotNull PosedConsumer<@NotNull Expr> f) {
-      f.accept(classCall);
-    }
+    @Override public void forEach(@NotNull PosedConsumer<@NotNull Expr> f) { f.accept(classCall); }
   }
 
   record Idiom(

From 4b3843fe2cd9686ab5024261358fad85c4e82fc5 Mon Sep 17 00:00:00 2001
From: ice1000 <ice1000kotlin@foxmail.com>
Date: Fri, 12 Jul 2024 13:29:29 -0400
Subject: [PATCH 30/33] class: done code review, remove some unnecessary stuff

Co-authored-by: HoshinoTented <hoshinotented@qq.com>
---
 .../java/org/aya/unify/TermComparator.java    | 43 ++++++++++---------
 .../aya/syntax/core/term/ClassCastTerm.java   | 14 ------
 2 files changed, 22 insertions(+), 35 deletions(-)

diff --git a/base/src/main/java/org/aya/unify/TermComparator.java b/base/src/main/java/org/aya/unify/TermComparator.java
index 045d4295c..1cf54e1a7 100644
--- a/base/src/main/java/org/aya/unify/TermComparator.java
+++ b/base/src/main/java/org/aya/unify/TermComparator.java
@@ -140,8 +140,7 @@ public boolean compare(@NotNull Term preLhs, @NotNull Term preRhs, @Nullable Ter
       // prefer solving the IsType one as the OfType one.
       if (lhs instanceof MetaCall lMeta && lMeta.ref().req() == MetaVar.Misc.IsType)
         return solveMeta(lMeta, rMeta, type) != null;
-      var llhs = lhs;
-      return swapped(() -> solveMeta(rMeta, llhs, type)) != null;
+      return swapped(() -> solveMeta(rMeta, lhs, type)) != null;
     }
     // ^ Beware of the order!!
     if (lhs instanceof MetaCall lMeta) {
@@ -149,19 +148,29 @@ public boolean compare(@NotNull Term preLhs, @NotNull Term preRhs, @Nullable Ter
     }
 
     if (rhs instanceof MemberCall && !(lhs instanceof MemberCall)) {
-      var tmp = lhs;
-      lhs = rhs;
-      rhs = tmp;
+      return swapped(() -> doCompare(rhs, lhs, type));
     }
 
-    if (type == null) {
-      return compareUntyped(lhs, rhs) != null;
-    }
+    return doCompare(lhs, rhs, type);
+  }
+
+  /**
+   * Do compare {@param lhs} and {@param rhs} against type {@param type} (if not null),
+   * with assumption on a good {@param lhs}, see below.
+   *
+   * @param lhs is {@link MemberCall} if rhs is not;
+   *            if there is a {@link MetaCall} then it must be lhs.
+   *            Reason: we case on lhs.
+   */
+  private boolean doCompare(Term lhs, Term rhs, @Nullable Term type) {
+    var result = type == null
+      ? compareUntyped(lhs, rhs) != null
+      : doCompareTyped(lhs, rhs, type);
 
-    var result = doCompareTyped(lhs, rhs, type);
     if (!result) fail(lhs, rhs);
     return result;
   }
+
   private boolean checkApproxResult(@Nullable Term type, Term approxResult) {
     if (approxResult != null) {
       if (type != null) compare(approxResult, type, null);
@@ -226,9 +235,9 @@ case SigmaTerm(var paramSeq) -> {
   }
 
   /**
-   * Compare whnfed {@param preLhs} and whnfed {@param preRhs} without type information.
+   * Compare head-normalized {@param preLhs} and whnfed {@param preRhs} without type information.
    *
-   * @return the whnfed type of {@param preLhs} and {@param preRhs} if they are 'the same', null otherwise.
+   * @return the head-normalized type of {@param preLhs} and {@param preRhs} if they are 'the same', null otherwise.
    */
   private @Nullable Term compareUntyped(@NotNull Term preLhs, @NotNull Term preRhs) {
     {
@@ -245,17 +254,9 @@ case SigmaTerm(var paramSeq) -> {
     }
 
     Term result;
-    if (rhs instanceof MetaCall || rhs instanceof MetaLitTerm) {
-      var llhs = lhs;
-      var rrhs = rhs;
-      result = swapped(() -> doCompareUntyped(rrhs, llhs));
+    if (rhs instanceof MetaCall || rhs instanceof MetaLitTerm || rhs instanceof MemberCall) {
+      result = swapped(() -> doCompareUntyped(rhs, lhs));
     } else {
-      if (rhs instanceof MemberCall && !(lhs instanceof MemberCall)) {
-        var tmp = lhs;
-        lhs = rhs;
-        rhs = tmp;
-      }
-
       result = doCompareUntyped(lhs, rhs);
     }
     if (result != null) return whnf(result);
diff --git a/syntax/src/main/java/org/aya/syntax/core/term/ClassCastTerm.java b/syntax/src/main/java/org/aya/syntax/core/term/ClassCastTerm.java
index 8ef9541ec..cfa77cdd0 100644
--- a/syntax/src/main/java/org/aya/syntax/core/term/ClassCastTerm.java
+++ b/syntax/src/main/java/org/aya/syntax/core/term/ClassCastTerm.java
@@ -2,20 +2,15 @@
 // 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.term;
 
-import kala.collection.immutable.ImmutableMap;
 import kala.collection.immutable.ImmutableSeq;
-import kala.collection.mutable.MutableMap;
 import kala.function.IndexedFunction;
 import org.aya.syntax.core.Closure;
 import org.aya.syntax.core.def.ClassDefLike;
 import org.aya.syntax.core.def.MemberDefLike;
 import org.aya.syntax.core.term.marker.StableWHNF;
-import org.aya.util.MapUtil;
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 
-import java.util.function.UnaryOperator;
-
 /**
  * This term is used for subtyping of class, a term {@code x : SomeClass (foo := 114514)} is treated an
  * instance of {@code SomeClass} in user side. In core side, we use {@code cast x [] [(foo := 114514)] : SomeClass}
@@ -57,13 +52,4 @@ public record ClassCastTerm(
     if (idx < forget.size()) return forget.get(idx);
     return null;
   }
-
-  public @NotNull Term unwrap(@NotNull UnaryOperator<Term> pre) {
-    Term term = this;
-    while (term instanceof ClassCastTerm cast) {
-      term = pre.apply(cast.subterm);
-    }
-
-    return term;
-  }
 }

From 6f6b9edcc742261003ca5cf4c167c3a74f59cdda Mon Sep 17 00:00:00 2001
From: ice1000 <ice1000kotlin@foxmail.com>
Date: Fri, 12 Jul 2024 13:36:12 -0400
Subject: [PATCH 31/33] class: serialize memcall and new, need classcast and
 classcall

---
 .../java/org/aya/compiler/TermExprializer.java | 18 ++++++++++++------
 1 file changed, 12 insertions(+), 6 deletions(-)

diff --git a/jit-compiler/src/main/java/org/aya/compiler/TermExprializer.java b/jit-compiler/src/main/java/org/aya/compiler/TermExprializer.java
index 13fbcbf43..331d60e05 100644
--- a/jit-compiler/src/main/java/org/aya/compiler/TermExprializer.java
+++ b/jit-compiler/src/main/java/org/aya/compiler/TermExprializer.java
@@ -46,6 +46,8 @@ public class TermExprializer extends AbstractExprializer<Term> {
   public static final String CLASS_RULEREDUCER = ExprializeUtils.getJavaReference(RuleReducer.class);
   public static final String CLASS_RULE_CON = ExprializeUtils.makeSub(CLASS_RULEREDUCER, ExprializeUtils.getJavaReference(RuleReducer.Con.class));
   public static final String CLASS_RULE_FN = ExprializeUtils.makeSub(CLASS_RULEREDUCER, ExprializeUtils.getJavaReference(RuleReducer.Fn.class));
+  public static final String CLASS_NEW = ExprializeUtils.getJavaReference(NewTerm.class);
+  public static final String CLASS_MEMCALL = ExprializeUtils.getJavaReference(MemberCall.class);
 
   /**
    * Terms that should be instantiated
@@ -136,7 +138,12 @@ case FreeTerm(var bind) -> {
       case Callable.SharableCall call when call.ulift() == 0 && call.args().isEmpty() ->
         ExprializeUtils.getEmptyCallTerm(getClassReference(call.ref()));
       case ClassCall classCall -> throw new UnsupportedOperationException("TODO");
-      case MemberCall memberCall -> throw new UnsupportedOperationException("TODO");
+      case MemberCall(var of, var ref, var ulift, var args) -> ExprializeUtils.makeNew(CLASS_MEMCALL,
+        doSerialize(of),
+        ExprializeUtils.getInstance(getClassReference(ref)),
+        Integer.toString(ulift),
+        serializeToImmutableSeq(CLASS_TERM, args)
+      );
       case AppTerm appTerm -> makeAppNew(CLASS_APPTERM, appTerm.fun(), appTerm.arg());
       case LocalTerm _ when !allowLocalTerm -> throw new Panic("LocalTerm");
       case LocalTerm(var index) -> ExprializeUtils.makeNew(CLASS_LOCALTERM, Integer.toString(index));
@@ -158,9 +165,8 @@ case ConCall(var head, var args) -> ExprializeUtils.makeNew(CLASS_CONCALL,
           case FnDef.Delegate def -> ExprializeUtils.getInstance(getClassReference(def.ref));
         };
 
-        var ulift = call.ulift();
         var args = call.args();
-        yield buildReducibleCall(ref, CLASS_FNCALL, ulift, ImmutableSeq.of(args), true);
+        yield buildReducibleCall(ref, CLASS_FNCALL, call.ulift(), ImmutableSeq.of(args), true);
       }
       case RuleReducer.Con conRuler -> buildReducibleCall(
         serializeApplicable(conRuler.rule()),
@@ -224,10 +230,10 @@ case ListTerm(var repr, var nil, var cons, var type) -> ExprializeUtils.makeNew(
         ExprializeUtils.getInstance(getClassReference(cons)),
         doSerialize(type)
       );
-      case StringTerm stringTerm ->
-        ExprializeUtils.makeNew(CLASS_STRING, ExprializeUtils.makeString(StringUtil.escapeStringCharacters(stringTerm.string())));
+      case StringTerm stringTerm -> ExprializeUtils.makeNew(CLASS_STRING,
+        ExprializeUtils.makeString(StringUtil.escapeStringCharacters(stringTerm.string())));
       case ClassCastTerm classCastTerm -> throw new UnsupportedOperationException("TODO");
-      case NewTerm newTerm -> throw new UnsupportedOperationException("TODO");
+      case NewTerm(var classCall) -> ExprializeUtils.makeNew(CLASS_NEW, doSerialize(classCall));
     };
   }
 

From 309bc3f518cc090b43cee41e8ef0fefcc2814bbf Mon Sep 17 00:00:00 2001
From: ice1000 <ice1000kotlin@foxmail.com>
Date: Fri, 12 Jul 2024 13:37:38 -0400
Subject: [PATCH 32/33] todo: do not panic

---
 .../src/main/java/org/aya/compiler/ModuleSerializer.java      | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/jit-compiler/src/main/java/org/aya/compiler/ModuleSerializer.java b/jit-compiler/src/main/java/org/aya/compiler/ModuleSerializer.java
index 178213eb4..c4ccc6adf 100644
--- a/jit-compiler/src/main/java/org/aya/compiler/ModuleSerializer.java
+++ b/jit-compiler/src/main/java/org/aya/compiler/ModuleSerializer.java
@@ -45,10 +45,10 @@ private void doSerialize(@NotNull TyckDef unit) {
       case PrimDef primDef -> new PrimSerializer(this)
         .serialize(primDef);
       case ClassDef classDef -> {
-        throw new UnsupportedOperationException("ClassDef");
+        // throw new UnsupportedOperationException("ClassDef");
       }
       case MemberDef memberDef -> {
-        throw new UnsupportedOperationException("MemberDef");
+        // throw new UnsupportedOperationException("MemberDef");
       }
     }
   }

From 8f52aab36e4b9426e2253f02673c4f7146fe45eb Mon Sep 17 00:00:00 2001
From: ice1000 <ice1000kotlin@foxmail.com>
Date: Fri, 12 Jul 2024 13:58:01 -0400
Subject: [PATCH 33/33] pretty: explicitize when signature is null

---
 .../java/org/aya/tyck/tycker/AppTycker.java   |  2 +-
 .../org/aya/cli/literate/SyntaxHighlight.java | 33 ++++++-------------
 .../java/org/aya/prettier/BasePrettier.java   | 10 +++---
 3 files changed, 17 insertions(+), 28 deletions(-)

diff --git a/base/src/main/java/org/aya/tyck/tycker/AppTycker.java b/base/src/main/java/org/aya/tyck/tycker/AppTycker.java
index cb0d6b96b..53b6b0240 100644
--- a/base/src/main/java/org/aya/tyck/tycker/AppTycker.java
+++ b/base/src/main/java/org/aya/tyck/tycker/AppTycker.java
@@ -202,7 +202,7 @@ record TakeMembers(
       var member = clazz.members().get(i);
       return TyckDef.defSignature(member.ref()).inst(ImmutableSeq.of(new NewTerm(
         new ClassCall(new ClassDef.Delegate(clazz.ref()), 0,
-          ImmutableSeq.fill(clazz.members().size(), idx -> Closure.mkConst(idx < teleArgs.size() ? teleArgs.get(idx) : ErrorTerm.DUMMY))
+          ImmutableSeq.fill(clazz.members().size(), idx -> Closure.mkConst(idx < i ? teleArgs.get(idx) : ErrorTerm.DUMMY))
         )
       ))).makePi(Seq.empty());
     }
diff --git a/cli-impl/src/main/java/org/aya/cli/literate/SyntaxHighlight.java b/cli-impl/src/main/java/org/aya/cli/literate/SyntaxHighlight.java
index 78fc1e562..26f6756d9 100644
--- a/cli-impl/src/main/java/org/aya/cli/literate/SyntaxHighlight.java
+++ b/cli-impl/src/main/java/org/aya/cli/literate/SyntaxHighlight.java
@@ -22,14 +22,7 @@
 import org.aya.syntax.concrete.stmt.ModuleName;
 import org.aya.syntax.concrete.stmt.Stmt;
 import org.aya.syntax.concrete.stmt.StmtVisitor;
-import org.aya.syntax.concrete.stmt.decl.DataCon;
-import org.aya.syntax.concrete.stmt.decl.DataDecl;
-import org.aya.syntax.concrete.stmt.decl.FnDecl;
-import org.aya.syntax.concrete.stmt.decl.PrimDecl;
-import org.aya.syntax.core.def.ConDef;
-import org.aya.syntax.core.def.DataDef;
-import org.aya.syntax.core.def.FnDef;
-import org.aya.syntax.core.def.PrimDef;
+import org.aya.syntax.concrete.stmt.decl.*;
 import org.aya.syntax.core.term.Term;
 import org.aya.syntax.ref.*;
 import org.aya.util.error.Panic;
@@ -144,21 +137,15 @@ else if (SPECIAL_SYMBOL.contains(tokenType))
   public static @NotNull DefKind kindOf(@NotNull AnyVar var) {
     return switch (var) {
       case GeneralizedVar _ -> DefKind.Generalized;
-      case DefVar<?, ?> defVar -> {
-        if (defVar.concrete instanceof FnDecl || defVar.core instanceof FnDef)
-          yield DefKind.Fn;
-//        else if (defVar.concrete instanceof TeleDecl.ClassMember || defVar.core instanceof MemberDef)
-//          yield DefKind.Member;
-        else if (defVar.concrete instanceof DataDecl || defVar.core instanceof DataDef)
-          yield DefKind.Data;
-        else if (defVar.concrete instanceof DataCon || defVar.core instanceof ConDef)
-          yield DefKind.Con;
-        else if (defVar.concrete instanceof PrimDecl || defVar.core instanceof PrimDef)
-          yield DefKind.Prim;
-//        else if (defVar.concrete instanceof ClassDecl || defVar.core instanceof ClassDef)
-//          yield DefKind.Clazz;
-        else throw new Panic(STR."unknown def type: \{defVar}");
-      }
+      case DefVar<?, ?> defVar -> switch (defVar.concrete) {
+        case FnDecl _ -> DefKind.Fn;
+        case ClassMember _ -> DefKind.Member;
+        case DataDecl _ -> DefKind.Data;
+        case DataCon _ -> DefKind.Con;
+        case PrimDecl _ -> DefKind.Prim;
+        case ClassDecl _ -> DefKind.Clazz;
+        default -> throw new Panic(STR."unknown def type: \{defVar}");
+      };
       case LocalVar(_, _, GenerateKind.Generalized(_)) -> DefKind.Generalized;
       case LocalVar _ -> DefKind.LocalVar;
       default -> DefKind.Unknown;
diff --git a/syntax/src/main/java/org/aya/prettier/BasePrettier.java b/syntax/src/main/java/org/aya/prettier/BasePrettier.java
index f93547369..3a2cf4d45 100644
--- a/syntax/src/main/java/org/aya/prettier/BasePrettier.java
+++ b/syntax/src/main/java/org/aya/prettier/BasePrettier.java
@@ -7,6 +7,7 @@
 import kala.collection.SeqView;
 import kala.collection.mutable.MutableList;
 import kala.collection.mutable.primitive.MutableBooleanList;
+import kala.collection.primitive.BooleanSeq;
 import org.aya.generic.AyaDocile;
 import org.aya.generic.term.ParamLike;
 import org.aya.pretty.doc.Doc;
@@ -98,10 +99,11 @@ protected BasePrettier(@NotNull PrettierOptions options) {
 
     // Because the signature of DataCon is selfTele, so we only need to deal with core con
     var licit = switch (var) {
-      case TyckAnyDef<?> inner -> inner.core() instanceof SubLevelDef sub ?
-        sub.selfTele.mapToBoolean(MutableBooleanList.factory(), Param::explicit) :
-        Objects.requireNonNull(inner.ref.signature).params()
-          .mapToBooleanTo(MutableBooleanList.create(), Param::explicit);
+      case TyckAnyDef<?> inner -> inner.core() instanceof SubLevelDef sub
+        ? sub.selfTele.mapToBoolean(MutableBooleanList.factory(), Param::explicit)
+        : inner.ref.signature == null
+          ? BooleanSeq.fill(preArgs.size(), true)
+          : inner.ref.signature.params().mapToBooleanTo(MutableBooleanList.create(), Param::explicit);
       case JitDef jit -> MutableBooleanList.from(jit.telescopeLicit);
       default -> throw new UnsupportedOperationException("TODO");
     };