From b097376d2877d31d4168a7f8308dc746bc53ad3a Mon Sep 17 00:00:00 2001
From: ice1000 <ice1000kotlin@foxmail.com>
Date: Fri, 15 Nov 2024 11:26:57 -0500
Subject: [PATCH 01/16] deps: upgrade badass jpms plugin

---
 gradle/libs.versions.toml | 6 +++---
 ide-lsp/build.gradle.kts  | 7 +++----
 2 files changed, 6 insertions(+), 7 deletions(-)

diff --git a/gradle/libs.versions.toml b/gradle/libs.versions.toml
index aff121d77..47506beaa 100644
--- a/gradle/libs.versions.toml
+++ b/gradle/libs.versions.toml
@@ -14,7 +14,7 @@ kala = "0.74.0"
 picocli = "4.7.6"
 build-util = "0.0.28"
 # https://github.com/jline/jline3
-jline = "3.26.3"
+jline = "3.27.1"
 # https://github.com/commonmark/commonmark-java
 commonmark = "0.24.0"
 # https://junit.org/junit5
@@ -23,11 +23,11 @@ hamcrest = "2.2"
 # https://github.com/google/gson
 gson = "2.11.0"
 # https://github.com/beryx/badass-jlink-plugin
-jlink = "3.0.1"
+jlink = "3.1.0"
 # https://github.com/jacoco/jacoco
 jacoco = "0.8.12"
 # https://github.com/manifold-systems/manifold/tree/master/manifold-deps-parent/manifold-delegation
-manifold = "2024.1.39"
+manifold = "2024.1.41"
 
 [plugins]
 jlink = { id = "org.beryx.jlink", version.ref = "jlink" }
diff --git a/ide-lsp/build.gradle.kts b/ide-lsp/build.gradle.kts
index e8c5d31f4..1a93250cd 100644
--- a/ide-lsp/build.gradle.kts
+++ b/ide-lsp/build.gradle.kts
@@ -57,16 +57,15 @@ jlink {
     requires("java.logging")
   }
   launcher {
-    mainClass.set(Constants.mainClassQName)
+    mainClass = Constants.mainClassQName
     name = "aya-lsp"
     jvmArgs = mutableListOf("--enable-preview")
   }
   secondaryLauncher {
+    moduleName = "aya.cli.console"
+    mainClass = "org.aya.cli.console.Main"
     name = "aya"
     jvmArgs = mutableListOf("--enable-preview")
-    this as org.beryx.jlink.data.SecondaryLauncherData
-    mainClass = "org.aya.cli.console.Main"
-    moduleName = "aya.cli.console"
   }
   supportedPlatforms.forEach { platform ->
     targetPlatform(platform) {

From 70a9f9337ffc15a57843da209d19645393acb89e Mon Sep 17 00:00:00 2001
From: HoshinoTented <hoshinotented@qq.com>
Date: Fri, 12 Jul 2024 08:51:51 +0800
Subject: [PATCH 02/16] jit: primitive class

---
 .../org/aya/compiler/ClassSerializer.java     | 52 +++++++++++
 .../org/aya/compiler/JitDefSerializer.java    | 86 +++++++++++++++++++
 .../org/aya/compiler/JitTeleSerializer.java   | 71 +--------------
 .../java/org/aya/syntax/compile/JitClass.java | 37 ++++++++
 .../java/org/aya/syntax/compile/JitDef.java   |  2 +-
 .../org/aya/syntax/compile/JitMember.java     | 30 +++++++
 .../org/aya/syntax/core/def/ClassDefLike.java |  3 +-
 .../aya/syntax/core/def/MemberDefLike.java    |  3 +-
 8 files changed, 213 insertions(+), 71 deletions(-)
 create mode 100644 jit-compiler/src/main/java/org/aya/compiler/ClassSerializer.java
 create mode 100644 jit-compiler/src/main/java/org/aya/compiler/JitDefSerializer.java
 create mode 100644 syntax/src/main/java/org/aya/syntax/compile/JitClass.java
 create mode 100644 syntax/src/main/java/org/aya/syntax/compile/JitMember.java

diff --git a/jit-compiler/src/main/java/org/aya/compiler/ClassSerializer.java b/jit-compiler/src/main/java/org/aya/compiler/ClassSerializer.java
new file mode 100644
index 000000000..4720029af
--- /dev/null
+++ b/jit-compiler/src/main/java/org/aya/compiler/ClassSerializer.java
@@ -0,0 +1,52 @@
+// 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.compiler;
+
+import kala.collection.immutable.ImmutableSeq;
+import org.aya.syntax.compile.JitClass;
+import org.aya.syntax.compile.JitMember;
+import org.aya.syntax.core.def.ClassDef;
+import org.aya.syntax.core.term.call.ClassCall;
+import org.jetbrains.annotations.NotNull;
+
+import static org.aya.compiler.AyaSerializer.CLASS_IMMSEQ;
+import static org.aya.compiler.NameSerializer.getClassReference;
+
+public final class ClassSerializer extends JitTeleSerializer<ClassDef> {
+  public static final String CLASS_JITMEMBERS = ExprializeUtils.getJavaReference(JitMember.class);
+  public static final String FIELD_MEMBERS = "members";
+  public static final String METHOD_MEMBARS = "membars";
+
+  public ClassSerializer(@NotNull SourceBuilder builder) {
+    super(builder, JitClass.class);
+  }
+
+  @Override
+  protected @NotNull String callClass() {
+    // TODO: return Class<?>
+    return ClassCall.class.getSimpleName();
+  }
+
+  @Override
+  protected void buildConstructor(ClassDef unit) {
+    buildSuperCall(ImmutableSeq.empty());
+  }
+
+  private void buildMembers(ClassDef unit) {
+    buildIf(STR."\{FIELD_MEMBERS} == null", () ->
+      buildUpdate(FIELD_MEMBERS, ExprializeUtils.makeArrayFrom(CLASS_JITMEMBERS, unit.members().map(mem ->
+        ExprializeUtils.getInstance(getClassReference(mem.ref())))
+      )));
+
+    buildReturn(FIELD_MEMBERS);
+  }
+
+  @Override
+  public AbstractSerializer<ClassDef> serialize(ClassDef unit) {
+    buildFramework(unit, () ->
+      buildMethod(METHOD_MEMBARS, ImmutableSeq.empty(), STR."\{CLASS_IMMSEQ}<\{CLASS_JITMEMBERS}>", true,
+        () -> buildMembers(unit)));
+
+    return null;
+  }
+}
diff --git a/jit-compiler/src/main/java/org/aya/compiler/JitDefSerializer.java b/jit-compiler/src/main/java/org/aya/compiler/JitDefSerializer.java
new file mode 100644
index 000000000..2c0794ed8
--- /dev/null
+++ b/jit-compiler/src/main/java/org/aya/compiler/JitDefSerializer.java
@@ -0,0 +1,86 @@
+// 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.compiler;
+
+import kala.collection.immutable.ImmutableSeq;
+import org.aya.syntax.compile.CompiledAya;
+import org.aya.syntax.core.def.TyckDef;
+import org.jetbrains.annotations.NotNull;
+
+import static org.aya.compiler.AyaSerializer.*;
+import static org.aya.compiler.NameSerializer.javifyClassName;
+
+public abstract class JitDefSerializer<T extends TyckDef> extends AbstractSerializer<T> {
+  public static final String CLASS_METADATA = ExprializeUtils.getJavaReference(CompiledAya.class);
+
+  protected final @NotNull Class<?> superClass;
+
+  protected JitDefSerializer(@NotNull SourceBuilder builder, @NotNull Class<?> superClass) {
+    super(builder);
+    this.superClass = superClass;
+  }
+
+  /**
+   * @see CompiledAya
+   */
+  protected void buildMetadata(@NotNull T unit) {
+    var ref = unit.ref();
+    var module = ref.module;
+    var assoc = ref.assoc();
+    var assocIdx = assoc == null ? -1 : assoc.ordinal();
+    assert module != null;
+    appendLine(STR."@\{CLASS_METADATA}(");
+    var modPath = module.module().module();
+    appendMetadataRecord("module", ExprializeUtils.makeHalfArrayFrom(modPath.view().map(ExprializeUtils::makeString)), true);
+    // Assumption: module.take(fileModule.size).equals(fileModule)
+    appendMetadataRecord("fileModuleSize", Integer.toString(module.fileModuleSize()), false);
+    appendMetadataRecord("name", ExprializeUtils.makeString(ref.name()), false);
+    appendMetadataRecord("assoc", Integer.toString(assocIdx), false);
+    buildShape(unit);
+
+    appendLine(")");
+  }
+
+  protected void buildShape(T unit) {
+    appendMetadataRecord("shape", "-1", false);
+    appendMetadataRecord("recognition", ExprializeUtils.makeHalfArrayFrom(ImmutableSeq.empty()), false);
+  }
+
+  protected void appendMetadataRecord(@NotNull String name, @NotNull String value, boolean isFirst) {
+    var prepend = isFirst ? "" : ", ";
+    appendLine(STR."\{prepend}\{name} = \{value}");
+  }
+
+  public void buildInstance(@NotNull String className) {
+    buildConstantField(className, STATIC_FIELD_INSTANCE, ExprializeUtils.makeNew(className));
+  }
+
+  public void buildSuperCall(@NotNull ImmutableSeq<String> args) {
+    appendLine(STR."super(\{args.joinToString(", ")});");
+  }
+
+  protected void buildFramework(@NotNull T unit, @NotNull Runnable continuation) {
+    var className = javifyClassName(unit.ref());
+    buildMetadata(unit);
+    buildInnerClass(className, superClass, () -> {
+      buildInstance(className);
+      appendLine();
+      // empty return type for constructor
+      buildMethod(className, ImmutableSeq.empty(), "/*constructor*/", false, () -> buildConstructor(unit));
+      appendLine();
+      if (unit.telescope().isEmpty()) {
+        buildConstantField(callClass(), FIELD_EMPTYCALL, ExprializeUtils.makeNew(
+          callClass(), ExprializeUtils.getInstance(className)));
+      }
+      appendLine();
+      continuation.run();
+    });
+  }
+
+  protected abstract @NotNull String callClass();
+
+  /**
+   * @see org.aya.syntax.compile.JitDef
+   */
+  protected abstract void buildConstructor(T unit);
+}
diff --git a/jit-compiler/src/main/java/org/aya/compiler/JitTeleSerializer.java b/jit-compiler/src/main/java/org/aya/compiler/JitTeleSerializer.java
index 4e6bb16be..5ea9daf9d 100644
--- a/jit-compiler/src/main/java/org/aya/compiler/JitTeleSerializer.java
+++ b/jit-compiler/src/main/java/org/aya/compiler/JitTeleSerializer.java
@@ -4,7 +4,6 @@
 
 import kala.collection.immutable.ImmutableSeq;
 import kala.range.primitive.IntRange;
-import org.aya.syntax.compile.CompiledAya;
 import org.aya.syntax.compile.JitCon;
 import org.aya.syntax.core.def.TyckDef;
 import org.aya.syntax.core.repr.CodeShape;
@@ -16,37 +15,22 @@
 import static org.aya.compiler.AyaSerializer.*;
 import static org.aya.compiler.NameSerializer.javifyClassName;
 
-public abstract class JitTeleSerializer<T extends TyckDef> extends AbstractSerializer<T> {
-  public static final String CLASS_METADATA = ExprializeUtils.getJavaReference(CompiledAya.class);
+public abstract class JitTeleSerializer<T extends TyckDef> extends JitDefSerializer<T> {
   public static final String CLASS_JITCON = ExprializeUtils.getJavaReference(JitCon.class);
   public static final String CLASS_GLOBALID = ExprializeUtils.makeSub(ExprializeUtils.getJavaReference(CodeShape.class), ExprializeUtils.getJavaReference(CodeShape.GlobalId.class));
   public static final String METHOD_TELESCOPE = "telescope";
   public static final String METHOD_RESULT = "result";
   public static final String TYPE_TERMSEQ = STR."\{CLASS_SEQ}<\{CLASS_TERM}>";
 
-  protected final @NotNull Class<?> superClass;
-
   protected JitTeleSerializer(
     @NotNull SourceBuilder builder,
     @NotNull Class<?> superClass
   ) {
-    super(builder);
-    this.superClass = superClass;
+    super(builder, superClass);
   }
 
   protected void buildFramework(@NotNull T unit, @NotNull Runnable continuation) {
-    var className = getClassName(unit);
-    buildMetadata(unit);
-    buildInnerClass(className, superClass, () -> {
-      buildInstance(className);
-      appendLine();
-      // empty return type for constructor
-      buildMethod(className, ImmutableSeq.empty(), "/*constructor*/", false, () -> buildConstructor(unit));
-      appendLine();
-      if (unit.telescope().isEmpty()) {
-        buildConstantField(callClass(), FIELD_EMPTYCALL, ExprializeUtils.makeNew(
-          callClass(), ExprializeUtils.getInstance(className)));
-      }
+    super.buildFramework(unit, () -> {
       var iTerm = "i";
       var teleArgsTerm = "teleArgs";
       buildMethod(METHOD_TELESCOPE, ImmutableSeq.of(
@@ -62,51 +46,6 @@ protected void buildFramework(@NotNull T unit, @NotNull Runnable continuation) {
     });
   }
 
-  protected abstract @NotNull String callClass();
-  private @NotNull String getClassName(@NotNull T unit) {
-    return javifyClassName(unit.ref());
-  }
-
-  public void buildInstance(@NotNull String className) {
-    buildConstantField(className, STATIC_FIELD_INSTANCE, ExprializeUtils.makeNew(className));
-  }
-
-  protected void appendMetadataRecord(@NotNull String name, @NotNull String value, boolean isFirst) {
-    var prepend = isFirst ? "" : ", ";
-    appendLine(STR."\{prepend}\{name} = \{value}");
-  }
-
-  /**
-   * @see CompiledAya
-   */
-  protected void buildMetadata(@NotNull T unit) {
-    var ref = unit.ref();
-    var module = ref.module;
-    var assoc = ref.assoc();
-    var assocIdx = assoc == null ? -1 : assoc.ordinal();
-    assert module != null;
-    appendLine(STR."@\{CLASS_METADATA}(");
-    var modPath = module.module().module();
-    appendMetadataRecord("module", ExprializeUtils.makeHalfArrayFrom(modPath.view().map(ExprializeUtils::makeString)), true);
-    // Assumption: module.take(fileModule.size).equals(fileModule)
-    appendMetadataRecord("fileModuleSize", Integer.toString(module.fileModuleSize()), false);
-    appendMetadataRecord("name", ExprializeUtils.makeString(ref.name()), false);
-    appendMetadataRecord("assoc", Integer.toString(assocIdx), false);
-    buildShape(unit);
-
-    appendLine(")");
-  }
-
-  protected void buildShape(T unit) {
-    appendMetadataRecord("shape", "-1", false);
-    appendMetadataRecord("recognition", ExprializeUtils.makeHalfArrayFrom(ImmutableSeq.empty()), false);
-  }
-
-  /**
-   * @see org.aya.syntax.compile.JitDef
-   */
-  protected abstract void buildConstructor(T unit);
-
   protected void buildConstructor(@NotNull T def, @NotNull ImmutableSeq<String> ext) {
     var tele = def.telescope();
     var size = tele.size();
@@ -135,8 +74,4 @@ protected void buildTelescope(@NotNull T unit, @NotNull String iTerm, @NotNull S
   protected void buildResult(@NotNull T unit, @NotNull String teleArgsTerm) {
     buildReturn(serializeTermUnderTele(unit.result(), teleArgsTerm, unit.telescope().size()));
   }
-
-  public void buildSuperCall(@NotNull ImmutableSeq<String> args) {
-    appendLine(STR."super(\{args.joinToString(", ")});");
-  }
 }
diff --git a/syntax/src/main/java/org/aya/syntax/compile/JitClass.java b/syntax/src/main/java/org/aya/syntax/compile/JitClass.java
new file mode 100644
index 000000000..5daf8c79d
--- /dev/null
+++ b/syntax/src/main/java/org/aya/syntax/compile/JitClass.java
@@ -0,0 +1,37 @@
+// 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.compile;
+
+import kala.collection.Seq;
+import kala.collection.immutable.ImmutableArray;
+import kala.collection.immutable.ImmutableSeq;
+import org.aya.syntax.core.def.ClassDefLike;
+import org.aya.syntax.core.def.MemberDefLike;
+import org.aya.syntax.core.term.SortTerm;
+import org.aya.syntax.core.term.Term;
+import org.jetbrains.annotations.NotNull;
+
+public abstract non-sealed class JitClass extends JitDef implements ClassDefLike {
+  private JitMember[] members = null;
+
+  protected JitClass() {
+    super(0, new boolean[0], new String[0]);
+  }
+
+  public abstract @NotNull JitMember[] membars();
+
+  @Override
+  public final @NotNull ImmutableSeq<MemberDefLike> members() {
+    return ImmutableArray.Unsafe.wrap(membars());
+  }
+
+  @Override
+  public @NotNull Term telescope(int i, Seq<Term> teleArgs) {
+    throw new UnsupportedOperationException("Unreachable");
+  }
+
+  @Override
+  public @NotNull Term result(Seq<Term> teleArgs) {
+    return SortTerm.Type0;
+  }
+}
diff --git a/syntax/src/main/java/org/aya/syntax/compile/JitDef.java b/syntax/src/main/java/org/aya/syntax/compile/JitDef.java
index a6e08d4bd..f38eddbcc 100644
--- a/syntax/src/main/java/org/aya/syntax/compile/JitDef.java
+++ b/syntax/src/main/java/org/aya/syntax/compile/JitDef.java
@@ -18,7 +18,7 @@
  *
  * @implNote every definition should be annotated by {@link CompiledAya}
  */
-public abstract sealed class JitDef extends JitTele implements AnyDef permits JitCon, JitData, JitFn, JitPrim {
+public abstract sealed class JitDef extends JitTele implements AnyDef permits JitClass, JitCon, JitData, JitFn, JitMember, JitPrim {
   private CompiledAya metadata;
 
   protected JitDef(int telescopeSize, boolean[] telescopeLicit, String[] telescopeNames) {
diff --git a/syntax/src/main/java/org/aya/syntax/compile/JitMember.java b/syntax/src/main/java/org/aya/syntax/compile/JitMember.java
new file mode 100644
index 000000000..77aa64608
--- /dev/null
+++ b/syntax/src/main/java/org/aya/syntax/compile/JitMember.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.compile;
+
+import org.aya.syntax.core.def.ClassDefLike;
+import org.aya.syntax.core.def.MemberDefLike;
+import org.jetbrains.annotations.NotNull;
+
+public abstract non-sealed class JitMember extends JitDef implements MemberDefLike {
+  public final @NotNull JitClass classRef;
+  public final @NotNull int index;
+
+  protected JitMember(
+    int telescopeSize, boolean[] telescopeLicit, String[] telescopeNames,
+    JitClass classRef, int index) {
+    super(telescopeSize, telescopeLicit, telescopeNames);
+    this.classRef = classRef;
+    this.index = index;
+  }
+
+  @Override
+  public @NotNull ClassDefLike classRef() {
+    return classRef;
+  }
+
+  @Override
+  public int index() {
+    return index;
+  }
+}
diff --git a/syntax/src/main/java/org/aya/syntax/core/def/ClassDefLike.java b/syntax/src/main/java/org/aya/syntax/core/def/ClassDefLike.java
index 3b4ffead2..a5d578fc6 100644
--- a/syntax/src/main/java/org/aya/syntax/core/def/ClassDefLike.java
+++ b/syntax/src/main/java/org/aya/syntax/core/def/ClassDefLike.java
@@ -3,8 +3,9 @@
 package org.aya.syntax.core.def;
 
 import kala.collection.immutable.ImmutableSeq;
+import org.aya.syntax.compile.JitClass;
 import org.jetbrains.annotations.NotNull;
 
-public sealed interface ClassDefLike extends AnyDef permits ClassDef.Delegate {
+public sealed interface ClassDefLike extends AnyDef permits JitClass, ClassDef.Delegate {
   @NotNull ImmutableSeq<MemberDefLike> members();
 }
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 f1c97084d..d4b639ffa 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
@@ -2,9 +2,10 @@
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.syntax.core.def;
 
+import org.aya.syntax.compile.JitMember;
 import org.jetbrains.annotations.NotNull;
 
-public sealed interface MemberDefLike extends AnyDef permits MemberDef.Delegate {
+public sealed interface MemberDefLike extends AnyDef permits JitMember, MemberDef.Delegate {
   @NotNull ClassDefLike classRef();
 
   default int index() {

From 333f1b918cca04eab1d17a1e86e7309f58218db7 Mon Sep 17 00:00:00 2001
From: HoshinoTented <hoshinotented@qq.com>
Date: Sat, 13 Jul 2024 05:57:04 +0800
Subject: [PATCH 03/16] jit: trying to make thing work

---
 .../org/aya/compiler/ClassSerializer.java     |  7 ++--
 .../org/aya/compiler/MemberSerializer.java    | 34 +++++++++++++++++++
 .../org/aya/compiler/PatternExprializer.java  |  2 +-
 .../java/org/aya/compiler/PrimSerializer.java |  2 +-
 .../org/aya/compiler/TermExprializer.java     | 24 ++++++++++---
 .../java/org/aya/syntax/compile/JitClass.java |  7 ++--
 .../org/aya/syntax/compile/JitMember.java     |  2 +-
 7 files changed, 65 insertions(+), 13 deletions(-)
 create mode 100644 jit-compiler/src/main/java/org/aya/compiler/MemberSerializer.java

diff --git a/jit-compiler/src/main/java/org/aya/compiler/ClassSerializer.java b/jit-compiler/src/main/java/org/aya/compiler/ClassSerializer.java
index 4720029af..04db7aab3 100644
--- a/jit-compiler/src/main/java/org/aya/compiler/ClassSerializer.java
+++ b/jit-compiler/src/main/java/org/aya/compiler/ClassSerializer.java
@@ -10,10 +10,12 @@
 import org.jetbrains.annotations.NotNull;
 
 import static org.aya.compiler.AyaSerializer.CLASS_IMMSEQ;
+import static org.aya.compiler.ExprializeUtils.getJavaReference;
 import static org.aya.compiler.NameSerializer.getClassReference;
 
 public final class ClassSerializer extends JitTeleSerializer<ClassDef> {
-  public static final String CLASS_JITMEMBERS = ExprializeUtils.getJavaReference(JitMember.class);
+  public static final String CLASS_JITMEMBERS = getJavaReference(JitMember.class);
+  public static final String CLASS_CLASSCALL = getJavaReference(ClassCall.class);
   public static final String FIELD_MEMBERS = "members";
   public static final String METHOD_MEMBARS = "membars";
 
@@ -23,8 +25,7 @@ public ClassSerializer(@NotNull SourceBuilder builder) {
 
   @Override
   protected @NotNull String callClass() {
-    // TODO: return Class<?>
-    return ClassCall.class.getSimpleName();
+    return CLASS_CLASSCALL;
   }
 
   @Override
diff --git a/jit-compiler/src/main/java/org/aya/compiler/MemberSerializer.java b/jit-compiler/src/main/java/org/aya/compiler/MemberSerializer.java
new file mode 100644
index 000000000..2a8a392b3
--- /dev/null
+++ b/jit-compiler/src/main/java/org/aya/compiler/MemberSerializer.java
@@ -0,0 +1,34 @@
+// 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.compiler;
+
+import kala.collection.immutable.ImmutableSeq;
+import org.aya.syntax.compile.JitMember;
+import org.aya.syntax.core.def.MemberDef;
+import org.jetbrains.annotations.NotNull;
+
+import static org.aya.compiler.NameSerializer.getClassReference;
+
+public final class MemberSerializer extends JitTeleSerializer<MemberDef> {
+  public MemberSerializer(@NotNull SourceBuilder builder) {
+    super(builder, JitMember.class);
+  }
+
+  @Override
+  protected @NotNull String callClass() {
+    return TermExprializer.CLASS_MEMCALL;
+  }
+
+  @Override
+  protected void buildConstructor(MemberDef unit) {
+    buildConstructor(unit, ImmutableSeq.of(
+      ExprializeUtils.getInstance(getClassReference(unit.classRef())),
+      Integer.toString(unit.index())
+    ));
+  }
+
+  @Override
+  public AbstractSerializer<MemberDef> serialize(MemberDef unit) {
+    return null;
+  }
+}
diff --git a/jit-compiler/src/main/java/org/aya/compiler/PatternExprializer.java b/jit-compiler/src/main/java/org/aya/compiler/PatternExprializer.java
index 46e4421e2..a7e527e50 100644
--- a/jit-compiler/src/main/java/org/aya/compiler/PatternExprializer.java
+++ b/jit-compiler/src/main/java/org/aya/compiler/PatternExprializer.java
@@ -13,7 +13,7 @@
 import static org.aya.compiler.AyaSerializer.CLASS_PAT;
 import static org.aya.compiler.AyaSerializer.CLASS_TERM;
 
-public class PatternExprializer extends AbstractExprializer<Pat> {
+public final class PatternExprializer extends AbstractExprializer<Pat> {
   public static final @NotNull String CLASS_PAT_ABSURD = ExprializeUtils.makeSub(CLASS_PAT, ExprializeUtils.getJavaReference(Pat.Absurd.class));
   public static final @NotNull String CLASS_PAT_BIND = ExprializeUtils.makeSub(CLASS_PAT, ExprializeUtils.getJavaReference(Pat.Bind.class));
   public static final @NotNull String CLASS_PAT_CON = ExprializeUtils.makeSub(CLASS_PAT, ExprializeUtils.getJavaReference(Pat.Con.class));
diff --git a/jit-compiler/src/main/java/org/aya/compiler/PrimSerializer.java b/jit-compiler/src/main/java/org/aya/compiler/PrimSerializer.java
index 9498a218b..cc1310342 100644
--- a/jit-compiler/src/main/java/org/aya/compiler/PrimSerializer.java
+++ b/jit-compiler/src/main/java/org/aya/compiler/PrimSerializer.java
@@ -9,7 +9,7 @@
 
 import static org.aya.compiler.AyaSerializer.CLASS_PRIMCALL;
 
-public class PrimSerializer extends JitTeleSerializer<PrimDef> {
+public final class PrimSerializer extends JitTeleSerializer<PrimDef> {
   public PrimSerializer(@NotNull AbstractSerializer<?> parent) {
     super(parent, JitPrim.class);
   }
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 331d60e05..3c6b8e9fc 100644
--- a/jit-compiler/src/main/java/org/aya/compiler/TermExprializer.java
+++ b/jit-compiler/src/main/java/org/aya/compiler/TermExprializer.java
@@ -22,13 +22,13 @@
 import java.util.function.Function;
 
 import static org.aya.compiler.AyaSerializer.*;
-import static org.aya.compiler.ExprializeUtils.makeThunk;
+import static org.aya.compiler.ExprializeUtils.*;
 import static org.aya.compiler.NameSerializer.getClassReference;
 
 /**
  * Build the "constructor form" of {@link Term}, but in Java.
  */
-public class TermExprializer extends AbstractExprializer<Term> {
+public final class TermExprializer extends AbstractExprializer<Term> {
   public static final String CLASS_LAMTERM = ExprializeUtils.getJavaReference(LamTerm.class);
   public static final String CLASS_JITLAMTERM = ExprializeUtils.getJavaReference(Closure.Jit.class);
   public static final String CLASS_APPTERM = ExprializeUtils.getJavaReference(AppTerm.class);
@@ -48,6 +48,9 @@ public class TermExprializer extends AbstractExprializer<Term> {
   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);
+  public static final String CLASS_CASTTERM = ExprializeUtils.getJavaReference(ClassCastTerm.class);
+  public static final String CLASS_CLSCALL = ExprializeUtils.getJavaReference(ClassCall.class);
+  public static final String CLASS_CLOSURE = ExprializeUtils.getJavaReference(Closure.class);
 
   /**
    * Terms that should be instantiated
@@ -137,7 +140,11 @@ 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(getClassReference(call.ref()));
-      case ClassCall classCall -> throw new UnsupportedOperationException("TODO");
+      case ClassCall(var ref, var ulift, var args) -> ExprializeUtils.makeNew(CLASS_CLSCALL,
+        getInstance(getClassReference(ref)),
+        Integer.toString(ulift),
+        serializeClosureToImmutableSeq(args)
+      );
       case MemberCall(var of, var ref, var ulift, var args) -> ExprializeUtils.makeNew(CLASS_MEMCALL,
         doSerialize(of),
         ExprializeUtils.getInstance(getClassReference(ref)),
@@ -232,7 +239,12 @@ case ListTerm(var repr, var nil, var cons, var type) -> ExprializeUtils.makeNew(
       );
       case StringTerm stringTerm -> ExprializeUtils.makeNew(CLASS_STRING,
         ExprializeUtils.makeString(StringUtil.escapeStringCharacters(stringTerm.string())));
-      case ClassCastTerm classCastTerm -> throw new UnsupportedOperationException("TODO");
+      case ClassCastTerm(var classRef, var subterm, var rember, var forgor) -> makeNew(CLASS_CASTTERM,
+        getInstance(getClassReference(classRef)),
+        serialize(subterm),
+        serializeClosureToImmutableSeq(rember),
+        serializeClosureToImmutableSeq(forgor)
+      );
       case NewTerm(var classCall) -> ExprializeUtils.makeNew(CLASS_NEW, doSerialize(classCall));
     };
   }
@@ -249,6 +261,10 @@ case ListTerm(var repr, var nil, var cons, var type) -> ExprializeUtils.makeNew(
     return result;
   }
 
+  private @NotNull String serializeClosureToImmutableSeq(@NotNull ImmutableSeq<Closure> cls) {
+    return makeImmutableSeq(CLASS_CLOSURE, cls.map(this::serializeClosure));
+  }
+
   private @NotNull String serializeClosure(@NotNull Closure body) {
     return serializeClosure(nameGen.nextName(), body);
   }
diff --git a/syntax/src/main/java/org/aya/syntax/compile/JitClass.java b/syntax/src/main/java/org/aya/syntax/compile/JitClass.java
index 5daf8c79d..df4c00209 100644
--- a/syntax/src/main/java/org/aya/syntax/compile/JitClass.java
+++ b/syntax/src/main/java/org/aya/syntax/compile/JitClass.java
@@ -10,9 +10,10 @@
 import org.aya.syntax.core.term.SortTerm;
 import org.aya.syntax.core.term.Term;
 import org.jetbrains.annotations.NotNull;
+import org.jetbrains.annotations.Nullable;
 
 public abstract non-sealed class JitClass extends JitDef implements ClassDefLike {
-  private JitMember[] members = null;
+  private JitMember @Nullable [] members = null;
 
   protected JitClass() {
     super(0, new boolean[0], new String[0]);
@@ -26,12 +27,12 @@ protected JitClass() {
   }
 
   @Override
-  public @NotNull Term telescope(int i, Seq<Term> teleArgs) {
+  public final @NotNull Term telescope(int i, Seq<Term> teleArgs) {
     throw new UnsupportedOperationException("Unreachable");
   }
 
   @Override
-  public @NotNull Term result(Seq<Term> teleArgs) {
+  public final @NotNull Term result(Seq<Term> teleArgs) {
     return SortTerm.Type0;
   }
 }
diff --git a/syntax/src/main/java/org/aya/syntax/compile/JitMember.java b/syntax/src/main/java/org/aya/syntax/compile/JitMember.java
index 77aa64608..6da6c0e12 100644
--- a/syntax/src/main/java/org/aya/syntax/compile/JitMember.java
+++ b/syntax/src/main/java/org/aya/syntax/compile/JitMember.java
@@ -8,7 +8,7 @@
 
 public abstract non-sealed class JitMember extends JitDef implements MemberDefLike {
   public final @NotNull JitClass classRef;
-  public final @NotNull int index;
+  public final int index;
 
   protected JitMember(
     int telescopeSize, boolean[] telescopeLicit, String[] telescopeNames,

From b145c44f21c7d2fc1f0b2b66e428e2d9788991c6 Mon Sep 17 00:00:00 2001
From: HoshinoTented <hoshinotented@qq.com>
Date: Sat, 13 Jul 2024 06:02:01 +0800
Subject: [PATCH 04/16] jit: trying to make more thing work

---
 .../java/org/aya/compiler/ClassSerializer.java     |  2 +-
 .../java/org/aya/compiler/MemberSerializer.java    |  3 ++-
 .../java/org/aya/compiler/ModuleSerializer.java    | 14 ++++++++++----
 3 files changed, 13 insertions(+), 6 deletions(-)

diff --git a/jit-compiler/src/main/java/org/aya/compiler/ClassSerializer.java b/jit-compiler/src/main/java/org/aya/compiler/ClassSerializer.java
index 04db7aab3..25e6cb0df 100644
--- a/jit-compiler/src/main/java/org/aya/compiler/ClassSerializer.java
+++ b/jit-compiler/src/main/java/org/aya/compiler/ClassSerializer.java
@@ -48,6 +48,6 @@ public AbstractSerializer<ClassDef> serialize(ClassDef unit) {
       buildMethod(METHOD_MEMBARS, ImmutableSeq.empty(), STR."\{CLASS_IMMSEQ}<\{CLASS_JITMEMBERS}>", true,
         () -> buildMembers(unit)));
 
-    return null;
+    return this;
   }
 }
diff --git a/jit-compiler/src/main/java/org/aya/compiler/MemberSerializer.java b/jit-compiler/src/main/java/org/aya/compiler/MemberSerializer.java
index 2a8a392b3..2d9c3e46e 100644
--- a/jit-compiler/src/main/java/org/aya/compiler/MemberSerializer.java
+++ b/jit-compiler/src/main/java/org/aya/compiler/MemberSerializer.java
@@ -29,6 +29,7 @@ protected void buildConstructor(MemberDef unit) {
 
   @Override
   public AbstractSerializer<MemberDef> serialize(MemberDef unit) {
-    return null;
+    buildFramework(unit, () -> { });
+    return this;
   }
 }
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 c4ccc6adf..8624b7868 100644
--- a/jit-compiler/src/main/java/org/aya/compiler/ModuleSerializer.java
+++ b/jit-compiler/src/main/java/org/aya/compiler/ModuleSerializer.java
@@ -32,6 +32,11 @@ private void serializeCons(@NotNull DataDef dataDef, @NotNull SourceBuilder seri
     IterableUtil.forEach(dataDef.body, ser::appendLine, ser::serialize);
   }
 
+  private void serializeMems(@NotNull ClassDef classDef, @NotNull SourceBuilder serializer) {
+    var ser = new MemberSerializer(serializer);
+    IterableUtil.forEach(classDef.members(), ser::appendLine, ser::serialize);
+  }
+
   private void doSerialize(@NotNull TyckDef unit) {
     switch (unit) {
       case FnDef teleDef -> new FnSerializer(this, shapeFactory)
@@ -45,11 +50,12 @@ private void doSerialize(@NotNull TyckDef unit) {
       case PrimDef primDef -> new PrimSerializer(this)
         .serialize(primDef);
       case ClassDef classDef -> {
-        // throw new UnsupportedOperationException("ClassDef");
-      }
-      case MemberDef memberDef -> {
-        // throw new UnsupportedOperationException("MemberDef");
+        new ClassSerializer(this)
+          .serialize(classDef);
+        serializeMems(classDef, this);
       }
+      case MemberDef memberDef -> new MemberSerializer(this)
+        .serialize(memberDef);
     }
   }
 

From 50f773276e39f380f288814e297cc923b9e265cf Mon Sep 17 00:00:00 2001
From: ice1000 <ice1000kotlin@foxmail.com>
Date: Sat, 13 Jul 2024 16:58:33 -0400
Subject: [PATCH 05/16] misc: fewer lines of code

---
 .../org/aya/compiler/ClassSerializer.java     | 19 ++++---------------
 .../org/aya/compiler/MemberSerializer.java    | 16 ++++------------
 2 files changed, 8 insertions(+), 27 deletions(-)

diff --git a/jit-compiler/src/main/java/org/aya/compiler/ClassSerializer.java b/jit-compiler/src/main/java/org/aya/compiler/ClassSerializer.java
index 25e6cb0df..8a6910f7f 100644
--- a/jit-compiler/src/main/java/org/aya/compiler/ClassSerializer.java
+++ b/jit-compiler/src/main/java/org/aya/compiler/ClassSerializer.java
@@ -19,19 +19,9 @@ public final class ClassSerializer extends JitTeleSerializer<ClassDef> {
   public static final String FIELD_MEMBERS = "members";
   public static final String METHOD_MEMBARS = "membars";
 
-  public ClassSerializer(@NotNull SourceBuilder builder) {
-    super(builder, JitClass.class);
-  }
-
-  @Override
-  protected @NotNull String callClass() {
-    return CLASS_CLASSCALL;
-  }
-
-  @Override
-  protected void buildConstructor(ClassDef unit) {
-    buildSuperCall(ImmutableSeq.empty());
-  }
+  public ClassSerializer(@NotNull SourceBuilder builder) { super(builder, JitClass.class); }
+  @Override protected @NotNull String callClass() { return CLASS_CLASSCALL; }
+  @Override protected void buildConstructor(ClassDef unit) { buildSuperCall(ImmutableSeq.empty()); }
 
   private void buildMembers(ClassDef unit) {
     buildIf(STR."\{FIELD_MEMBERS} == null", () ->
@@ -42,8 +32,7 @@ private void buildMembers(ClassDef unit) {
     buildReturn(FIELD_MEMBERS);
   }
 
-  @Override
-  public AbstractSerializer<ClassDef> serialize(ClassDef unit) {
+  @Override public AbstractSerializer<ClassDef> serialize(ClassDef unit) {
     buildFramework(unit, () ->
       buildMethod(METHOD_MEMBARS, ImmutableSeq.empty(), STR."\{CLASS_IMMSEQ}<\{CLASS_JITMEMBERS}>", true,
         () -> buildMembers(unit)));
diff --git a/jit-compiler/src/main/java/org/aya/compiler/MemberSerializer.java b/jit-compiler/src/main/java/org/aya/compiler/MemberSerializer.java
index 2d9c3e46e..65f5c4c65 100644
--- a/jit-compiler/src/main/java/org/aya/compiler/MemberSerializer.java
+++ b/jit-compiler/src/main/java/org/aya/compiler/MemberSerializer.java
@@ -10,25 +10,17 @@
 import static org.aya.compiler.NameSerializer.getClassReference;
 
 public final class MemberSerializer extends JitTeleSerializer<MemberDef> {
-  public MemberSerializer(@NotNull SourceBuilder builder) {
-    super(builder, JitMember.class);
-  }
-
-  @Override
-  protected @NotNull String callClass() {
-    return TermExprializer.CLASS_MEMCALL;
-  }
+  public MemberSerializer(@NotNull SourceBuilder builder) { super(builder, JitMember.class); }
+  @Override protected @NotNull String callClass() { return TermExprializer.CLASS_MEMCALL; }
 
-  @Override
-  protected void buildConstructor(MemberDef unit) {
+  @Override protected void buildConstructor(MemberDef unit) {
     buildConstructor(unit, ImmutableSeq.of(
       ExprializeUtils.getInstance(getClassReference(unit.classRef())),
       Integer.toString(unit.index())
     ));
   }
 
-  @Override
-  public AbstractSerializer<MemberDef> serialize(MemberDef unit) {
+  @Override public AbstractSerializer<MemberDef> serialize(MemberDef unit) {
     buildFramework(unit, () -> { });
     return this;
   }

From 5e6310483d9a889f11727e4a7103865d43ce66d9 Mon Sep 17 00:00:00 2001
From: HoshinoTented <hoshinotented@qq.com>
Date: Sun, 14 Jul 2024 05:40:54 +0800
Subject: [PATCH 06/16] member: cache type

---
 base/src/main/java/org/aya/tyck/StmtTycker.java     | 13 +++++++++++--
 .../main/java/org/aya/tyck/tycker/AppTycker.java    |  6 ++----
 .../java/org/aya/compiler/AbstractSerializer.java   |  4 ++++
 .../java/org/aya/compiler/MemberSerializer.java     |  3 ++-
 .../main/java/org/aya/syntax/compile/JitMember.java |  7 ++++++-
 .../java/org/aya/syntax/core/def/MemberDef.java     |  7 ++++++-
 .../java/org/aya/syntax/core/def/MemberDefLike.java |  8 +++-----
 .../java/org/aya/syntax/telescope/AbstractTele.java |  4 ++++
 8 files changed, 38 insertions(+), 14 deletions(-)

diff --git a/base/src/main/java/org/aya/tyck/StmtTycker.java b/base/src/main/java/org/aya/tyck/StmtTycker.java
index d8a40b635..b495147d5 100644
--- a/base/src/main/java/org/aya/tyck/StmtTycker.java
+++ b/base/src/main/java/org/aya/tyck/StmtTycker.java
@@ -32,6 +32,8 @@
 import org.aya.tyck.pat.YouTrack;
 import org.aya.tyck.tycker.Problematic;
 import org.aya.tyck.tycker.TeleTycker;
+import org.aya.unify.Synthesizer;
+import org.aya.util.error.Panic;
 import org.aya.util.error.WithPos;
 import org.aya.util.reporter.Reporter;
 import org.jetbrains.annotations.NotNull;
@@ -173,8 +175,15 @@ private void checkMember(@NotNull ClassMember member, @NotNull ExprTycker tycker
         new Param("self", classCall, false),
         classRef.concrete.sourcePos()
       );
-    new MemberDef(classRef, member.ref, classRef.concrete.members.indexOf(member), signature.params(), signature.result());
-    member.ref.signature = signature;
+
+    // self is still in the context
+    var type = new Synthesizer(tycker).synth(signature.telescope().inst(ImmutableSeq.of(new FreeTerm(self))).makePi());
+    if (!(type instanceof SortTerm sortType)) {
+      Panic.unreachable();
+    } else {
+      new MemberDef(classRef, member.ref, classRef.concrete.members.indexOf(member), signature.params(), signature.result(), sortType);
+      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 53b6b0240..65590331e 100644
--- a/base/src/main/java/org/aya/tyck/tycker/AppTycker.java
+++ b/base/src/main/java/org/aya/tyck/tycker/AppTycker.java
@@ -8,10 +8,7 @@
 import kala.collection.immutable.ImmutableSeq;
 import kala.function.CheckedBiFunction;
 import org.aya.generic.stmt.Shaped;
-import org.aya.syntax.compile.JitCon;
-import org.aya.syntax.compile.JitData;
-import org.aya.syntax.compile.JitFn;
-import org.aya.syntax.compile.JitPrim;
+import org.aya.syntax.compile.*;
 import org.aya.syntax.concrete.stmt.decl.*;
 import org.aya.syntax.core.Closure;
 import org.aya.syntax.core.def.*;
@@ -177,6 +174,7 @@ public AppTycker(
   private @NotNull AbstractTele ofClassMembers(@NotNull LocalVar self, @NotNull ClassDefLike def, int memberCount) {
     var synthesizer = new Synthesizer(tycker);
     return switch (def) {
+      case JitClass jit -> throw new UnsupportedOperationException("TODO");
       case ClassDef.Delegate delegate -> new TakeMembers(self, delegate.core(), memberCount, synthesizer);
     };
   }
diff --git a/jit-compiler/src/main/java/org/aya/compiler/AbstractSerializer.java b/jit-compiler/src/main/java/org/aya/compiler/AbstractSerializer.java
index ebe94036d..e6f743050 100644
--- a/jit-compiler/src/main/java/org/aya/compiler/AbstractSerializer.java
+++ b/jit-compiler/src/main/java/org/aya/compiler/AbstractSerializer.java
@@ -40,4 +40,8 @@ protected AbstractSerializer(@NotNull SourceBuilder builder) {
     return new TermExprializer(sourceBuilder.nameGen(), argTerms)
       .serialize(term);
   }
+
+  protected @NotNull String serializeTerm(@NotNull Term term) {
+    return serializeTermUnderTele(term, ImmutableSeq.empty());
+  }
 }
diff --git a/jit-compiler/src/main/java/org/aya/compiler/MemberSerializer.java b/jit-compiler/src/main/java/org/aya/compiler/MemberSerializer.java
index 65f5c4c65..d4fc55931 100644
--- a/jit-compiler/src/main/java/org/aya/compiler/MemberSerializer.java
+++ b/jit-compiler/src/main/java/org/aya/compiler/MemberSerializer.java
@@ -16,7 +16,8 @@ public final class MemberSerializer extends JitTeleSerializer<MemberDef> {
   @Override protected void buildConstructor(MemberDef unit) {
     buildConstructor(unit, ImmutableSeq.of(
       ExprializeUtils.getInstance(getClassReference(unit.classRef())),
-      Integer.toString(unit.index())
+      Integer.toString(unit.index()),
+      serializeTerm(unit.type())
     ));
   }
 
diff --git a/syntax/src/main/java/org/aya/syntax/compile/JitMember.java b/syntax/src/main/java/org/aya/syntax/compile/JitMember.java
index 6da6c0e12..7823cfc51 100644
--- a/syntax/src/main/java/org/aya/syntax/compile/JitMember.java
+++ b/syntax/src/main/java/org/aya/syntax/compile/JitMember.java
@@ -4,18 +4,21 @@
 
 import org.aya.syntax.core.def.ClassDefLike;
 import org.aya.syntax.core.def.MemberDefLike;
+import org.aya.syntax.core.term.SortTerm;
 import org.jetbrains.annotations.NotNull;
 
 public abstract non-sealed class JitMember extends JitDef implements MemberDefLike {
   public final @NotNull JitClass classRef;
   public final int index;
+  public final @NotNull SortTerm type;
 
   protected JitMember(
     int telescopeSize, boolean[] telescopeLicit, String[] telescopeNames,
-    JitClass classRef, int index) {
+    JitClass classRef, int index, @NotNull SortTerm type) {
     super(telescopeSize, telescopeLicit, telescopeNames);
     this.classRef = classRef;
     this.index = index;
+    this.type = type;
   }
 
   @Override
@@ -23,6 +26,8 @@ protected JitMember(
     return classRef;
   }
 
+  @Override
+  public @NotNull SortTerm type() { return type; }
   @Override
   public int index() {
     return index;
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 b52b1b39c..51d324a4c 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
@@ -6,6 +6,7 @@
 import org.aya.syntax.concrete.stmt.decl.ClassDecl;
 import org.aya.syntax.concrete.stmt.decl.ClassMember;
 import org.aya.syntax.core.term.Param;
+import org.aya.syntax.core.term.SortTerm;
 import org.aya.syntax.core.term.Term;
 import org.aya.syntax.ref.DefVar;
 import org.jetbrains.annotations.NotNull;
@@ -15,13 +16,15 @@
  *
  * @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.
+ * @param type the type of the signature of this member (exclude {@code self : ClassCall})
  */
 public record MemberDef(
   @NotNull DefVar<ClassDef, ClassDecl> classRef,
   @Override @NotNull DefVar<MemberDef, ClassMember> ref,
   int index,
   @Override ImmutableSeq<Param> telescope,
-  @Override @NotNull Term result
+  @Override @NotNull Term result,
+  @NotNull SortTerm type
 ) implements TyckDef {
   public MemberDef {
     assert index >= 0;
@@ -36,6 +39,8 @@ public static final class Delegate extends TyckAnyDef<MemberDef> implements Memb
      */
     @Override public int index() { return ref.core.index; }
 
+    @Override public @NotNull SortTerm type() { return ref.core.type; }
+
     @Override public @NotNull ClassDefLike classRef() {
       return new ClassDef.Delegate(core().classRef());
     }
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 d4b639ffa..f5ec6e27f 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
@@ -3,14 +3,12 @@
 package org.aya.syntax.core.def;
 
 import org.aya.syntax.compile.JitMember;
+import org.aya.syntax.core.term.SortTerm;
 import org.jetbrains.annotations.NotNull;
 
 public sealed interface MemberDefLike extends AnyDef permits JitMember, MemberDef.Delegate {
   @NotNull ClassDefLike classRef();
+  @NotNull SortTerm type();
 
-  default int index() {
-    var idx = classRef().members().indexOf(this);
-    assert idx >= 0;
-    return idx;
-  }
+  int index();
 }
diff --git a/syntax/src/main/java/org/aya/syntax/telescope/AbstractTele.java b/syntax/src/main/java/org/aya/syntax/telescope/AbstractTele.java
index 58cb2619f..cea4a3263 100644
--- a/syntax/src/main/java/org/aya/syntax/telescope/AbstractTele.java
+++ b/syntax/src/main/java/org/aya/syntax/telescope/AbstractTele.java
@@ -79,6 +79,10 @@ public interface AbstractTele {
       .view().mapToObj(this::telescopeName);
   }
 
+  default @NotNull Term makePi() {
+    return makePi(Seq.empty());
+  }
+
   default @NotNull Term makePi(@NotNull Seq<Term> initialArgs) {
     return new PiBuilder(this).make(0, initialArgs);
   }

From 66d16b80fa815d79687c762bc4c5abfc29bc3626 Mon Sep 17 00:00:00 2001
From: HoshinoTented <hoshinotented@qq.com>
Date: Sun, 14 Jul 2024 05:41:54 +0800
Subject: [PATCH 07/16] tycker: remove duplicated

---
 base/src/main/java/org/aya/tyck/tycker/AppTycker.java | 3 +--
 1 file changed, 1 insertion(+), 2 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 65590331e..316b6e4b2 100644
--- a/base/src/main/java/org/aya/tyck/tycker/AppTycker.java
+++ b/base/src/main/java/org/aya/tyck/tycker/AppTycker.java
@@ -208,8 +208,7 @@ record TakeMembers(
     @Override public @NotNull Term result(Seq<Term> teleArgs) {
       return clazz.members().view()
         .drop(telescopeSize)
-        .map(member -> TyckDef.defSignature(member.ref()).inst(ImmutableSeq.of(new FreeTerm(self))).makePi(Seq.empty()))
-        .map(ty -> (SortTerm) synthesizer.synth(ty))
+        .map(MemberDef::type)
         .foldLeft(SortTerm.Type0, SigmaTerm::lub);
     }
     @Override public @NotNull SeqView<String> namesView() {

From 0345edfea0335f6c76311ab2b836969a3739cb5e Mon Sep 17 00:00:00 2001
From: HoshinoTented <hoshinotented@qq.com>
Date: Sun, 14 Jul 2024 09:22:33 +0800
Subject: [PATCH 08/16] tycker: generialize

---
 .../java/org/aya/tyck/tycker/AppTycker.java   | 20 ++++++++-----------
 base/src/test/java/org/aya/tyck/TyckTest.java | 15 +++++++++++---
 2 files changed, 20 insertions(+), 15 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 316b6e4b2..a90665f1c 100644
--- a/base/src/main/java/org/aya/tyck/tycker/AppTycker.java
+++ b/base/src/main/java/org/aya/tyck/tycker/AppTycker.java
@@ -172,21 +172,17 @@ public AppTycker(
   }
 
   private @NotNull AbstractTele ofClassMembers(@NotNull LocalVar self, @NotNull ClassDefLike def, int memberCount) {
-    var synthesizer = new Synthesizer(tycker);
-    return switch (def) {
-      case JitClass jit -> throw new UnsupportedOperationException("TODO");
-      case ClassDef.Delegate delegate -> new TakeMembers(self, delegate.core(), memberCount, synthesizer);
-    };
+    return new TakeMembers(self, def, memberCount);
   }
 
   record TakeMembers(
-    @NotNull LocalVar self, @NotNull ClassDef clazz,
-    @Override int telescopeSize, @NotNull Synthesizer synthesizer
+    @NotNull LocalVar self, @NotNull ClassDefLike clazz,
+    @Override int telescopeSize
   ) implements AbstractTele {
     @Override public boolean telescopeLicit(int i) { return true; }
     @Override public @NotNull String telescopeName(int i) {
       assert i < telescopeSize;
-      return clazz.members().get(i).ref().name();
+      return clazz.members().get(i).name();
     }
 
     // class Foo
@@ -198,8 +194,8 @@ record TakeMembers(
       // teleArgs are former members
       assert i < telescopeSize;
       var member = clazz.members().get(i);
-      return TyckDef.defSignature(member.ref()).inst(ImmutableSeq.of(new NewTerm(
-        new ClassCall(new ClassDef.Delegate(clazz.ref()), 0,
+      return member.signature().inst(ImmutableSeq.of(new NewTerm(
+        new ClassCall(clazz, 0,
           ImmutableSeq.fill(clazz.members().size(), idx -> Closure.mkConst(idx < i ? teleArgs.get(idx) : ErrorTerm.DUMMY))
         )
       ))).makePi(Seq.empty());
@@ -208,11 +204,11 @@ record TakeMembers(
     @Override public @NotNull Term result(Seq<Term> teleArgs) {
       return clazz.members().view()
         .drop(telescopeSize)
-        .map(MemberDef::type)
+        .map(MemberDefLike::type)
         .foldLeft(SortTerm.Type0, SigmaTerm::lub);
     }
     @Override public @NotNull SeqView<String> namesView() {
-      return clazz.members().sliceView(0, telescopeSize).map(i -> i.ref().name());
+      return clazz.members().sliceView(0, telescopeSize).map(AnyDef::name);
     }
   }
 }
diff --git a/base/src/test/java/org/aya/tyck/TyckTest.java b/base/src/test/java/org/aya/tyck/TyckTest.java
index 1e74c5624..ad1335392 100644
--- a/base/src/test/java/org/aya/tyck/TyckTest.java
+++ b/base/src/test/java/org/aya/tyck/TyckTest.java
@@ -37,7 +37,7 @@ public class TyckTest {
     var result = tyck("""
       inductive Nat | O | S Nat
       inductive FreeMonoid (A : Type) | e | cons A (FreeMonoid A)
-      
+            
       def id {A : Type} (a : A) => a
       def lam (A : Type) : Fn (a : A) -> Type => fn a => A
       def tup (A : Type) (B : A -> Type) (a : A) (b : Fn (a : A) -> B a)
@@ -66,7 +66,7 @@ def letExample (A : Type) (B : A -> Type) (f : Fn (a : A) -> B a) (a : A) : B a
       prim I : ISet
       prim Path (A : I -> Type) (a : A 0) (b : A 1) : Type
       prim coe (r s : I) (A : I -> Type) : A r -> A s
-      
+            
       def transp (A : I -> Type) (a : A 0) : A 1 => coe 0 1 A a
       def transpInv (A : I -> Type) (a : A 1) : A 0 => coe 1 0 A a
       def coeFill0 (A : I -> Type) (u : A 0) : Path A u (transp A u) => \\i => coe 0 i A u
@@ -152,7 +152,7 @@ open inductive Phantom Nat Nat (A : Type) | mk A
       prim I prim Path prim coe
       variable A : Type
       def infix = (a b : A) => Path (\\i => A) a b
-      
+            
       class Monoid
       | classifying carrier : Type
       | unit : carrier
@@ -162,6 +162,15 @@ class Monoid
       """).defs.isNotEmpty());
   }
 
+  @Test
+  public void what() {
+    assertTrue(tyck("""
+      class Kontainer
+      | Taipe : Type
+      | walue : Taipe
+      """).defs.isNotEmpty());
+  }
+
   @SuppressWarnings("unchecked") private static <T extends AnyDef> T
   getDef(@NotNull ImmutableSeq<TyckDef> defs, @NotNull String name) {
     return (T) TyckAnyDef.make(defs.find(x -> x.ref().name().equals(name)).get());

From a1bd3a05c0b75cf16ab1019c181e52500fdeb4d1 Mon Sep 17 00:00:00 2001
From: HoshinoTented <hoshinotented@qq.com>
Date: Sun, 14 Jul 2024 13:41:17 +0800
Subject: [PATCH 09/16] tycker: generalize more

---
 base/src/main/java/org/aya/tyck/tycker/AppTycker.java | 11 ++++-------
 1 file changed, 4 insertions(+), 7 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 a90665f1c..c2c1d0fa9 100644
--- a/base/src/main/java/org/aya/tyck/tycker/AppTycker.java
+++ b/base/src/main/java/org/aya/tyck/tycker/AppTycker.java
@@ -147,7 +147,7 @@ public AppTycker(
 
   private @NotNull Jdg checkClassCall(@NotNull ClassDefLike clazz) throws Ex {
     var self = LocalVar.generate("self");
-    var appliedParams = ofClassMembers(self, clazz, argsCount).lift(lift);
+    var appliedParams = ofClassMembers(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))),
@@ -171,14 +171,11 @@ public AppTycker(
     });
   }
 
-  private @NotNull AbstractTele ofClassMembers(@NotNull LocalVar self, @NotNull ClassDefLike def, int memberCount) {
-    return new TakeMembers(self, def, memberCount);
+  private @NotNull AbstractTele ofClassMembers(@NotNull ClassDefLike def, int memberCount) {
+    return new TakeMembers(def, memberCount);
   }
 
-  record TakeMembers(
-    @NotNull LocalVar self, @NotNull ClassDefLike clazz,
-    @Override int telescopeSize
-  ) implements AbstractTele {
+  record TakeMembers(@NotNull ClassDefLike clazz, @Override int telescopeSize) implements AbstractTele {
     @Override public boolean telescopeLicit(int i) { return true; }
     @Override public @NotNull String telescopeName(int i) {
       assert i < telescopeSize;

From 9dea402b4f1bf80f8bd031e6f7b4a5265b6a3137 Mon Sep 17 00:00:00 2001
From: HoshinoTented <hoshinotented@qq.com>
Date: Mon, 15 Jul 2024 07:24:21 +0800
Subject: [PATCH 10/16] test: add more class test

---
 cli-impl/src/test/resources/success/src/Classes.aya | 6 +++++-
 1 file changed, 5 insertions(+), 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 8df70f758..bf0c13ccb 100644
--- a/cli-impl/src/test/resources/success/src/Classes.aya
+++ b/cli-impl/src/test/resources/success/src/Classes.aya
@@ -6,4 +6,8 @@ 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
+
+def subtype : Kontainer Nat => new Kontainer Nat 0
+
+def norm1 : Kontainer::walue {subtype} = 0 => refl

From 1f1437a047e0438966f1f302695a683a9d792beb Mon Sep 17 00:00:00 2001
From: HoshinoTented <hoshinotented@qq.com>
Date: Mon, 15 Jul 2024 07:27:12 +0800
Subject: [PATCH 11/16] class: move the computation of result to ClassDefLike

---
 .../src/main/java/org/aya/tyck/tycker/AppTycker.java |  5 +----
 .../java/org/aya/syntax/core/def/ClassDefLike.java   | 12 ++++++++++++
 2 files changed, 13 insertions(+), 4 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 c2c1d0fa9..38be7f925 100644
--- a/base/src/main/java/org/aya/tyck/tycker/AppTycker.java
+++ b/base/src/main/java/org/aya/tyck/tycker/AppTycker.java
@@ -199,10 +199,7 @@ record TakeMembers(@NotNull ClassDefLike clazz, @Override int telescopeSize) imp
     }
 
     @Override public @NotNull Term result(Seq<Term> teleArgs) {
-      return clazz.members().view()
-        .drop(telescopeSize)
-        .map(MemberDefLike::type)
-        .foldLeft(SortTerm.Type0, SigmaTerm::lub);
+      return clazz.result(telescopeSize);
     }
     @Override public @NotNull SeqView<String> namesView() {
       return clazz.members().sliceView(0, telescopeSize).map(AnyDef::name);
diff --git a/syntax/src/main/java/org/aya/syntax/core/def/ClassDefLike.java b/syntax/src/main/java/org/aya/syntax/core/def/ClassDefLike.java
index a5d578fc6..66fdd8684 100644
--- a/syntax/src/main/java/org/aya/syntax/core/def/ClassDefLike.java
+++ b/syntax/src/main/java/org/aya/syntax/core/def/ClassDefLike.java
@@ -4,8 +4,20 @@
 
 import kala.collection.immutable.ImmutableSeq;
 import org.aya.syntax.compile.JitClass;
+import org.aya.syntax.core.term.SigmaTerm;
+import org.aya.syntax.core.term.SortTerm;
 import org.jetbrains.annotations.NotNull;
 
 public sealed interface ClassDefLike extends AnyDef permits JitClass, ClassDef.Delegate {
   @NotNull ImmutableSeq<MemberDefLike> members();
+
+  default @NotNull SortTerm result(int implSize) {
+    var members = members();
+    assert implSize < members.size();
+
+    return members.view()
+      .drop(implSize)
+      .map(MemberDefLike::type)
+      .foldLeft(SortTerm.Type0, SigmaTerm::lub);
+  }
 }

From 4930159ff5ee46b993421059d0b27ca07df116b3 Mon Sep 17 00:00:00 2001
From: HoshinoTented <hoshinotented@qq.com>
Date: Mon, 15 Jul 2024 07:29:28 +0800
Subject: [PATCH 12/16] misc: comment

---
 cli-impl/src/test/resources/success/src/Classes.aya | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/cli-impl/src/test/resources/success/src/Classes.aya b/cli-impl/src/test/resources/success/src/Classes.aya
index bf0c13ccb..338cf98d2 100644
--- a/cli-impl/src/test/resources/success/src/Classes.aya
+++ b/cli-impl/src/test/resources/success/src/Classes.aya
@@ -9,5 +9,10 @@ def tyck0 : Nat => Kontainer::walue {new Kontainer Nat 0}
 def norm0 : Kontainer::walue {new Kontainer Nat 0} = 0 => refl
 
 def subtype : Kontainer Nat => new Kontainer Nat 0
+// In core:
+// def subtype : Kontainer Nat => cast [Taipe := Nat] [walue := 0] (new Kontainer Nat 0)
 
 def norm1 : Kontainer::walue {subtype} = 0 => refl
+// In core:
+// (cast [Taipe := Nat] [walue := 0] (new Kontainer Nat 0)) .walue
+// -> 0 (it is recorded in the ClassCastTerm!)

From 42e82f0a45eb73e69ae219d61548e959e4b517a3 Mon Sep 17 00:00:00 2001
From: HoshinoTented <hoshinotented@qq.com>
Date: Wed, 17 Jul 2024 06:44:00 +0800
Subject: [PATCH 13/16] jit: fix compilation

---
 cli-impl/src/test/java/org/aya/test/LibraryTest.java      | 8 ++++++++
 .../src/main/java/org/aya/compiler/ClassSerializer.java   | 7 ++++++-
 .../src/main/java/org/aya/compiler/JitDefSerializer.java  | 4 +++-
 .../src/main/java/org/aya/compiler/JitTeleSerializer.java | 4 ++++
 .../main/java/org/aya/syntax/core/def/ClassDefLike.java   | 2 +-
 5 files changed, 22 insertions(+), 3 deletions(-)

diff --git a/cli-impl/src/test/java/org/aya/test/LibraryTest.java b/cli-impl/src/test/java/org/aya/test/LibraryTest.java
index 0f4d80e71..959b33718 100644
--- a/cli-impl/src/test/java/org/aya/test/LibraryTest.java
+++ b/cli-impl/src/test/java/org/aya/test/LibraryTest.java
@@ -34,6 +34,13 @@
 
 import static org.junit.jupiter.api.Assertions.assertEquals;
 
+/**
+ * LibraryTest testing the compilation of a library and its dependencies
+ *
+ * @see #testOnDisk
+ * @see #testLiterate
+ * @see #testInMemoryAndPrim
+ */
 public class LibraryTest {
   public static final ThrowingReporter REPORTER = new ThrowingReporter(AyaPrettierOptions.pretty());
   @ParameterizedTest
@@ -51,6 +58,7 @@ public void testOnDisk(@NotNull String libName) throws IOException {
     assertEquals(0, compile(libRoot));
   }
 
+  // Use this test for additional compilation
   @Test public void fastTestOnDisk() throws IOException {
     FileUtil.deleteRecursively(DIR.resolve("build"));
     assertEquals(0, compile(DIR));
diff --git a/jit-compiler/src/main/java/org/aya/compiler/ClassSerializer.java b/jit-compiler/src/main/java/org/aya/compiler/ClassSerializer.java
index 8a6910f7f..3a66935ba 100644
--- a/jit-compiler/src/main/java/org/aya/compiler/ClassSerializer.java
+++ b/jit-compiler/src/main/java/org/aya/compiler/ClassSerializer.java
@@ -13,7 +13,7 @@
 import static org.aya.compiler.ExprializeUtils.getJavaReference;
 import static org.aya.compiler.NameSerializer.getClassReference;
 
-public final class ClassSerializer extends JitTeleSerializer<ClassDef> {
+public final class ClassSerializer extends JitDefSerializer<ClassDef> {
   public static final String CLASS_JITMEMBERS = getJavaReference(JitMember.class);
   public static final String CLASS_CLASSCALL = getJavaReference(ClassCall.class);
   public static final String FIELD_MEMBERS = "members";
@@ -23,6 +23,11 @@ public final class ClassSerializer extends JitTeleSerializer<ClassDef> {
   @Override protected @NotNull String callClass() { return CLASS_CLASSCALL; }
   @Override protected void buildConstructor(ClassDef unit) { buildSuperCall(ImmutableSeq.empty()); }
 
+  @Override
+  protected boolean shouldBuildEmptyCall(@NotNull ClassDef unit) {
+    return true;
+  }
+
   private void buildMembers(ClassDef unit) {
     buildIf(STR."\{FIELD_MEMBERS} == null", () ->
       buildUpdate(FIELD_MEMBERS, ExprializeUtils.makeArrayFrom(CLASS_JITMEMBERS, unit.members().map(mem ->
diff --git a/jit-compiler/src/main/java/org/aya/compiler/JitDefSerializer.java b/jit-compiler/src/main/java/org/aya/compiler/JitDefSerializer.java
index 2c0794ed8..b2576b9d8 100644
--- a/jit-compiler/src/main/java/org/aya/compiler/JitDefSerializer.java
+++ b/jit-compiler/src/main/java/org/aya/compiler/JitDefSerializer.java
@@ -59,6 +59,8 @@ public void buildSuperCall(@NotNull ImmutableSeq<String> args) {
     appendLine(STR."super(\{args.joinToString(", ")});");
   }
 
+  protected abstract boolean shouldBuildEmptyCall(@NotNull T unit);
+
   protected void buildFramework(@NotNull T unit, @NotNull Runnable continuation) {
     var className = javifyClassName(unit.ref());
     buildMetadata(unit);
@@ -68,7 +70,7 @@ protected void buildFramework(@NotNull T unit, @NotNull Runnable continuation) {
       // empty return type for constructor
       buildMethod(className, ImmutableSeq.empty(), "/*constructor*/", false, () -> buildConstructor(unit));
       appendLine();
-      if (unit.telescope().isEmpty()) {
+      if (shouldBuildEmptyCall(unit)) {
         buildConstantField(callClass(), FIELD_EMPTYCALL, ExprializeUtils.makeNew(
           callClass(), ExprializeUtils.getInstance(className)));
       }
diff --git a/jit-compiler/src/main/java/org/aya/compiler/JitTeleSerializer.java b/jit-compiler/src/main/java/org/aya/compiler/JitTeleSerializer.java
index 5ea9daf9d..75a4a7aed 100644
--- a/jit-compiler/src/main/java/org/aya/compiler/JitTeleSerializer.java
+++ b/jit-compiler/src/main/java/org/aya/compiler/JitTeleSerializer.java
@@ -46,6 +46,10 @@ protected void buildFramework(@NotNull T unit, @NotNull Runnable continuation) {
     });
   }
 
+  @Override
+  protected boolean shouldBuildEmptyCall(@NotNull T unit) {
+    return unit.telescope().isEmpty();
+  }
   protected void buildConstructor(@NotNull T def, @NotNull ImmutableSeq<String> ext) {
     var tele = def.telescope();
     var size = tele.size();
diff --git a/syntax/src/main/java/org/aya/syntax/core/def/ClassDefLike.java b/syntax/src/main/java/org/aya/syntax/core/def/ClassDefLike.java
index 66fdd8684..d2ebd480f 100644
--- a/syntax/src/main/java/org/aya/syntax/core/def/ClassDefLike.java
+++ b/syntax/src/main/java/org/aya/syntax/core/def/ClassDefLike.java
@@ -13,7 +13,7 @@ public sealed interface ClassDefLike extends AnyDef permits JitClass, ClassDef.D
 
   default @NotNull SortTerm result(int implSize) {
     var members = members();
-    assert implSize < members.size();
+    assert implSize <= members.size();
 
     return members.view()
       .drop(implSize)

From 6b671fe7a025708c8dddf94c216847fb9b0583e7 Mon Sep 17 00:00:00 2001
From: HoshinoTented <hoshinotented@qq.com>
Date: Tue, 27 Aug 2024 11:30:10 +0800
Subject: [PATCH 14/16] class: make thing better

---
 .../java/org/aya/syntax/compile/JitClass.java   |  6 +++---
 .../java/org/aya/syntax/compile/JitMember.java  |  6 +++++-
 .../org/aya/syntax/core/def/ClassDefLike.java   | 17 +++++++++++++++--
 3 files changed, 23 insertions(+), 6 deletions(-)

diff --git a/syntax/src/main/java/org/aya/syntax/compile/JitClass.java b/syntax/src/main/java/org/aya/syntax/compile/JitClass.java
index df4c00209..ebee5c53e 100644
--- a/syntax/src/main/java/org/aya/syntax/compile/JitClass.java
+++ b/syntax/src/main/java/org/aya/syntax/compile/JitClass.java
@@ -27,12 +27,12 @@ protected JitClass() {
   }
 
   @Override
-  public final @NotNull Term telescope(int i, Seq<Term> teleArgs) {
-    throw new UnsupportedOperationException("Unreachable");
+  public final @NotNull Term telescope(int i, @NotNull Seq<Term> teleArgs) {
+    return ClassDefLike.super.telescope(i, teleArgs);
   }
 
   @Override
   public final @NotNull Term result(Seq<Term> teleArgs) {
-    return SortTerm.Type0;
+    return result(teleArgs.size());
   }
 }
diff --git a/syntax/src/main/java/org/aya/syntax/compile/JitMember.java b/syntax/src/main/java/org/aya/syntax/compile/JitMember.java
index 7823cfc51..2093e4992 100644
--- a/syntax/src/main/java/org/aya/syntax/compile/JitMember.java
+++ b/syntax/src/main/java/org/aya/syntax/compile/JitMember.java
@@ -10,11 +10,15 @@
 public abstract non-sealed class JitMember extends JitDef implements MemberDefLike {
   public final @NotNull JitClass classRef;
   public final int index;
+
+  /**
+   * the type of the type/telescope (exclude self-parameter) of this member
+   */
   public final @NotNull SortTerm type;
 
   protected JitMember(
     int telescopeSize, boolean[] telescopeLicit, String[] telescopeNames,
-    JitClass classRef, int index, @NotNull SortTerm type) {
+    @NotNull JitClass classRef, int index, @NotNull SortTerm type) {
     super(telescopeSize, telescopeLicit, telescopeNames);
     this.classRef = classRef;
     this.index = index;
diff --git a/syntax/src/main/java/org/aya/syntax/core/def/ClassDefLike.java b/syntax/src/main/java/org/aya/syntax/core/def/ClassDefLike.java
index d2ebd480f..738b819a0 100644
--- a/syntax/src/main/java/org/aya/syntax/core/def/ClassDefLike.java
+++ b/syntax/src/main/java/org/aya/syntax/core/def/ClassDefLike.java
@@ -2,15 +2,28 @@
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.syntax.core.def;
 
+import kala.collection.Seq;
 import kala.collection.immutable.ImmutableSeq;
 import org.aya.syntax.compile.JitClass;
-import org.aya.syntax.core.term.SigmaTerm;
-import org.aya.syntax.core.term.SortTerm;
+import org.aya.syntax.core.Closure;
+import org.aya.syntax.core.term.*;
+import org.aya.syntax.core.term.call.ClassCall;
 import org.jetbrains.annotations.NotNull;
 
 public sealed interface ClassDefLike extends AnyDef permits JitClass, ClassDef.Delegate {
   @NotNull ImmutableSeq<MemberDefLike> members();
 
+  default @NotNull Term telescope(int i, @NotNull Seq<Term> restriction) {
+    var member = members().get(i);
+    // Our code should not refer the subterm of self, the only meaningful part is [self.forget()]
+    // Also, we don't use NewTerm, cause the type of the self-parameter is a class call without any restriction.
+    var self = new ClassCastTerm(this, ErrorTerm.DUMMY, ImmutableSeq.empty(),
+      restriction.map(Closure::mkConst)
+    );
+
+    return member.signature().inst(ImmutableSeq.of(self)).makePi(Seq.empty());
+  }
+
   default @NotNull SortTerm result(int implSize) {
     var members = members();
     assert implSize <= members.size();

From 9852c4f30e26561d0428af72fd561c12abff1ed1 Mon Sep 17 00:00:00 2001
From: HoshinoTented <hoshinotented@qq.com>
Date: Tue, 27 Aug 2024 11:31:06 +0800
Subject: [PATCH 15/16] class: unify some code

---
 base/src/main/java/org/aya/tyck/tycker/AppTycker.java | 7 +------
 1 file changed, 1 insertion(+), 6 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 38be7f925..0888bb613 100644
--- a/base/src/main/java/org/aya/tyck/tycker/AppTycker.java
+++ b/base/src/main/java/org/aya/tyck/tycker/AppTycker.java
@@ -190,12 +190,7 @@ record TakeMembers(@NotNull ClassDefLike clazz, @Override int telescopeSize) imp
     @Override public @NotNull Term telescope(int i, Seq<Term> teleArgs) {
       // teleArgs are former members
       assert i < telescopeSize;
-      var member = clazz.members().get(i);
-      return member.signature().inst(ImmutableSeq.of(new NewTerm(
-        new ClassCall(clazz, 0,
-          ImmutableSeq.fill(clazz.members().size(), idx -> Closure.mkConst(idx < i ? teleArgs.get(idx) : ErrorTerm.DUMMY))
-        )
-      ))).makePi(Seq.empty());
+      return clazz.telescope(i, teleArgs);
     }
 
     @Override public @NotNull Term result(Seq<Term> teleArgs) {

From 26555c7c59c4531e33bb9e947f3dce53588a64cf Mon Sep 17 00:00:00 2001
From: ice1000 <ice1000kotlin@foxmail.com>
Date: Fri, 15 Nov 2024 11:35:40 -0500
Subject: [PATCH 16/16] deps: looks like 3.1.0 is not yet published

---
 base/src/main/java/org/aya/tyck/tycker/AppTycker.java | 10 +++++-----
 gradle/libs.versions.toml                             |  2 +-
 2 files changed, 6 insertions(+), 6 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 0888bb613..12c37f321 100644
--- a/base/src/main/java/org/aya/tyck/tycker/AppTycker.java
+++ b/base/src/main/java/org/aya/tyck/tycker/AppTycker.java
@@ -5,22 +5,22 @@
 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.*;
+import org.aya.syntax.compile.JitCon;
+import org.aya.syntax.compile.JitData;
+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.*;
+import org.aya.syntax.core.term.Term;
 import org.aya.syntax.core.term.call.*;
 import org.aya.syntax.ref.DefVar;
 import org.aya.syntax.ref.LocalVar;
 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;
diff --git a/gradle/libs.versions.toml b/gradle/libs.versions.toml
index 47506beaa..ce6166fd9 100644
--- a/gradle/libs.versions.toml
+++ b/gradle/libs.versions.toml
@@ -23,7 +23,7 @@ hamcrest = "2.2"
 # https://github.com/google/gson
 gson = "2.11.0"
 # https://github.com/beryx/badass-jlink-plugin
-jlink = "3.1.0"
+jlink = "3.1.0-rc-1"
 # https://github.com/jacoco/jacoco
 jacoco = "0.8.12"
 # https://github.com/manifold-systems/manifold/tree/master/manifold-deps-parent/manifold-delegation