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..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,7 +5,6 @@
 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;
@@ -13,17 +12,15 @@
 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;
@@ -150,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))),
@@ -174,21 +171,15 @@ public AppTycker(
     });
   }
 
-  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(self, delegate.core(), memberCount, synthesizer);
-    };
+  private @NotNull AbstractTele ofClassMembers(@NotNull ClassDefLike def, int memberCount) {
+    return new TakeMembers(def, memberCount);
   }
 
-  record TakeMembers(
-    @NotNull LocalVar self, @NotNull ClassDef clazz,
-    @Override int telescopeSize, @NotNull Synthesizer synthesizer
-  ) 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;
-      return clazz.members().get(i).ref().name();
+      return clazz.members().get(i).name();
     }
 
     // class Foo
@@ -199,23 +190,14 @@ record TakeMembers(
     @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()).inst(ImmutableSeq.of(new NewTerm(
-        new ClassCall(new ClassDef.Delegate(clazz.ref()), 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) {
-      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))
-        .foldLeft(SortTerm.Type0, SigmaTerm::lub);
+      return clazz.result(telescopeSize);
     }
     @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());
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/cli-impl/src/test/resources/success/src/Classes.aya b/cli-impl/src/test/resources/success/src/Classes.aya
index 8df70f758..338cf98d2 100644
--- a/cli-impl/src/test/resources/success/src/Classes.aya
+++ b/cli-impl/src/test/resources/success/src/Classes.aya
@@ -6,4 +6,13 @@ 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
+// 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!)
diff --git a/gradle/libs.versions.toml b/gradle/libs.versions.toml
index aff121d77..ce6166fd9 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-rc-1"
 # 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) {
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/ClassSerializer.java b/jit-compiler/src/main/java/org/aya/compiler/ClassSerializer.java
new file mode 100644
index 000000000..3a66935ba
--- /dev/null
+++ b/jit-compiler/src/main/java/org/aya/compiler/ClassSerializer.java
@@ -0,0 +1,47 @@
+// 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.ExprializeUtils.getJavaReference;
+import static org.aya.compiler.NameSerializer.getClassReference;
+
+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";
+  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()); }
+
+  @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 ->
+        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 this;
+  }
+}
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..b2576b9d8
--- /dev/null
+++ b/jit-compiler/src/main/java/org/aya/compiler/JitDefSerializer.java
@@ -0,0 +1,88 @@
+// 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 abstract boolean shouldBuildEmptyCall(@NotNull T unit);
+
+  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 (shouldBuildEmptyCall(unit)) {
+        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..75a4a7aed 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,10 @@ 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);
+  @Override
+  protected boolean shouldBuildEmptyCall(@NotNull T unit) {
+    return unit.telescope().isEmpty();
   }
-
-  /**
-   * @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 +78,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/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..d4fc55931
--- /dev/null
+++ b/jit-compiler/src/main/java/org/aya/compiler/MemberSerializer.java
@@ -0,0 +1,28 @@
+// 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()),
+      serializeTerm(unit.type())
+    ));
+  }
+
+  @Override public AbstractSerializer<MemberDef> serialize(MemberDef unit) {
+    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);
     }
   }
 
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
new file mode 100644
index 000000000..ebee5c53e
--- /dev/null
+++ b/syntax/src/main/java/org/aya/syntax/compile/JitClass.java
@@ -0,0 +1,38 @@
+// 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;
+import org.jetbrains.annotations.Nullable;
+
+public abstract non-sealed class JitClass extends JitDef implements ClassDefLike {
+  private JitMember @Nullable [] 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 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 result(teleArgs.size());
+  }
+}
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..2093e4992
--- /dev/null
+++ b/syntax/src/main/java/org/aya/syntax/compile/JitMember.java
@@ -0,0 +1,39 @@
+// 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.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;
+
+  /**
+   * 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,
+    @NotNull JitClass classRef, int index, @NotNull SortTerm type) {
+    super(telescopeSize, telescopeLicit, telescopeNames);
+    this.classRef = classRef;
+    this.index = index;
+    this.type = type;
+  }
+
+  @Override
+  public @NotNull ClassDefLike classRef() {
+    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/ClassDefLike.java b/syntax/src/main/java/org/aya/syntax/core/def/ClassDefLike.java
index 3b4ffead2..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,9 +2,35 @@
 // 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.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 ClassDef.Delegate {
+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();
+
+    return members.view()
+      .drop(implSize)
+      .map(MemberDefLike::type)
+      .foldLeft(SortTerm.Type0, SigmaTerm::lub);
+  }
 }
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 f1c97084d..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
@@ -2,14 +2,13 @@
 // 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.aya.syntax.core.term.SortTerm;
 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();
+  @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);
   }