diff --git a/base/src/main/java/org/aya/tyck/ExprTycker.java b/base/src/main/java/org/aya/tyck/ExprTycker.java
index a3e6f296c..ed489f0f1 100644
--- a/base/src/main/java/org/aya/tyck/ExprTycker.java
+++ b/base/src/main/java/org/aya/tyck/ExprTycker.java
@@ -47,6 +47,7 @@
 import org.jetbrains.annotations.Nullable;
 
 import java.util.Comparator;
+import java.util.function.BiFunction;
 import java.util.function.Function;
 import java.util.function.Supplier;
 
@@ -134,6 +135,11 @@ case PiTerm(var dom, var cod) -> {
     };
   }
 
+  /**
+   * @param type   expected type
+   * @param result wellTyped + actual type from synthesize
+   * @param expr   original expr, used for error reporting
+   */
   private @NotNull Jdg inheritFallbackUnify(@NotNull Term type, @NotNull Jdg result, @NotNull WithPos<Expr> expr) {
     type = whnf(type);
     var resultType = result.type();
@@ -155,6 +161,22 @@ case PiTerm(var dom, var cod) -> {
         return new Jdg.Default(new LamTerm(closure), eq);
       }
     }
+    // Try coercive subtyping between classes
+    if (type instanceof ClassCall clazz) {
+      // Try coercive subtyping for `SomeClass (foo := 114514)` into `SomeClass`
+      resultType = whnf(resultType);
+      if (resultType instanceof ClassCall resultClazz) {
+        // TODO: check whether resultClazz <: clazz
+        if (true) {
+          // No need to coerce
+          if (clazz.args().size() == resultClazz.args().size()) return result;
+          var forget = resultClazz.args().drop(clazz.args().size());
+          return new Jdg.Default(new ClassCastTerm(clazz.ref(), result.wellTyped(), clazz.args(), forget), type);
+        } else {
+          return makeErrorResult(type, result);
+        }
+      }
+    }
     if (unifyTyReported(type, resultType, expr)) return result;
     return makeErrorResult(type, result);
   }
@@ -315,6 +337,19 @@ yield subscoped(param.ref(), wellParam, () ->
         var type = new DataCall(def, 0, ImmutableSeq.of(elementTy));
         yield new Jdg.Default(new ListTerm(results, match.recog(), type), type);
       }
+      case Expr.New(var classCall) -> {
+        var wellTyped = synthesize(classCall);
+        if (!(wellTyped.wellTyped() instanceof ClassCall call)) {
+          yield fail(expr.data(), new ClassError.NotClassCall(classCall));
+        }
+
+        // check whether the call is fully applied
+        if (call.args().size() != call.ref().members().size()) {
+          yield fail(expr.data(), new ClassError.NotFullyApplied(classCall));
+        }
+
+        yield new Jdg.Default(new NewTerm(call), call);
+      }
       case Expr.Unresolved _ -> Panic.unreachable();
       default -> fail(expr.data(), new NoRuleError(expr, null));
     };
@@ -342,9 +377,9 @@ yield subscoped(param.ref(), wellParam, () ->
       case LocalVar ref when localLet.contains(ref) -> generateApplication(args, localLet.get(ref)).lift(lift);
       case LocalVar lVar -> generateApplication(args,
         new Jdg.Default(new FreeTerm(lVar), localCtx().get(lVar))).lift(lift);
-      case CompiledVar(var content) -> new AppTycker<>(state, sourcePos, args.size(), lift, (params, k) ->
+      case CompiledVar(var content) -> new AppTycker<>(this, sourcePos, args.size(), lift, (params, k) ->
         computeArgs(sourcePos, args, params, k)).checkCompiledApplication(content);
-      case DefVar<?, ?> defVar -> new AppTycker<>(state, sourcePos, args.size(), lift, (params, k) ->
+      case DefVar<?, ?> defVar -> new AppTycker<>(this, sourcePos, args.size(), lift, (params, k) ->
         computeArgs(sourcePos, args, params, k)).checkDefApplication(defVar);
       default -> throw new UnsupportedOperationException("TODO");
     };
@@ -359,10 +394,11 @@ case CompiledVar(var content) -> new AppTycker<>(state, sourcePos, args.size(),
 
   private Jdg computeArgs(
     @NotNull SourcePos pos, @NotNull ImmutableSeq<Expr.NamedArg> args,
-    @NotNull AbstractTele params, @NotNull Function<Term[], Jdg> k
+    @NotNull AbstractTele params, @NotNull BiFunction<Term[], Term, Jdg> k
   ) throws NotPi {
     int argIx = 0, paramIx = 0;
     var result = new Term[params.telescopeSize()];
+    Term firstType = null;
     while (argIx < args.size() && paramIx < params.telescopeSize()) {
       var arg = args.get(argIx);
       var param = params.telescopeRich(paramIx, result);
@@ -373,33 +409,39 @@ private Jdg computeArgs(
           break;
         } else if (arg.name() == null) {
           // here, arg.explicit() == true and param.explicit() == false
+          if (paramIx == 0) firstType = param.type();
           result[paramIx++] = insertImplicit(param, arg.sourcePos());
           continue;
         }
       }
       if (arg.name() != null && !param.nameEq(arg.name())) {
+        if (paramIx == 0) firstType = param.type();
         result[paramIx++] = insertImplicit(param, arg.sourcePos());
         continue;
       }
-      result[paramIx++] = inherit(arg.arg(), param.type()).wellTyped();
+      var what = inherit(arg.arg(), param.type());
+      if (paramIx == 0) firstType = param.type();
+      result[paramIx++] = what.wellTyped();
       argIx++;
     }
     // Trailing implicits
     while (paramIx < params.telescopeSize()) {
       if (params.telescopeLicit(paramIx)) break;
       var param = params.telescopeRich(paramIx, result);
+      if (paramIx == 0) firstType = param.type();
       result[paramIx++] = insertImplicit(param, pos);
     }
     var extraParams = MutableStack.<Pair<LocalVar, Term>>create();
     if (argIx < args.size()) {
-      return generateApplication(args.drop(argIx), k.apply(result));
+      return generateApplication(args.drop(argIx), k.apply(result, firstType));
     } else while (paramIx < params.telescopeSize()) {
       var param = params.telescopeRich(paramIx, result);
       var atarashiVar = LocalVar.generate(param.name());
       extraParams.push(new Pair<>(atarashiVar, param.type()));
+      if (paramIx == 0) firstType = param.type();
       result[paramIx++] = new FreeTerm(atarashiVar);
     }
-    var generated = k.apply(result);
+    var generated = k.apply(result, firstType);
     while (extraParams.isNotEmpty()) {
       var pair = extraParams.pop();
       generated = new Jdg.Default(
diff --git a/base/src/main/java/org/aya/tyck/StmtTycker.java b/base/src/main/java/org/aya/tyck/StmtTycker.java
index a5daf3b66..d8a40b635 100644
--- a/base/src/main/java/org/aya/tyck/StmtTycker.java
+++ b/base/src/main/java/org/aya/tyck/StmtTycker.java
@@ -173,7 +173,7 @@ private void checkMember(@NotNull ClassMember member, @NotNull ExprTycker tycker
         new Param("self", classCall, false),
         classRef.concrete.sourcePos()
       );
-    new MemberDef(classRef, member.ref, signature.params(), signature.result());
+    new MemberDef(classRef, member.ref, classRef.concrete.members.indexOf(member), signature.params(), signature.result());
     member.ref.signature = signature;
   }
 
diff --git a/base/src/main/java/org/aya/tyck/error/ClassError.java b/base/src/main/java/org/aya/tyck/error/ClassError.java
new file mode 100644
index 000000000..bc6954a8a
--- /dev/null
+++ b/base/src/main/java/org/aya/tyck/error/ClassError.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.tyck.error;
+
+import org.aya.pretty.doc.Doc;
+import org.aya.syntax.concrete.Expr;
+import org.aya.util.error.SourcePos;
+import org.aya.util.error.WithPos;
+import org.aya.util.prettier.PrettierOptions;
+import org.jetbrains.annotations.NotNull;
+
+public interface ClassError extends TyckError {
+  @NotNull WithPos<Expr> problemExpr();
+
+  @Override default @NotNull SourcePos sourcePos() { return problemExpr().sourcePos(); }
+
+  record NotClassCall(@Override @NotNull WithPos<Expr> problemExpr) implements ClassError {
+    @Override public @NotNull Doc describe(@NotNull PrettierOptions options) {
+      return Doc.sep(Doc.english("Unable to new a non-class type:"), Doc.code(problemExpr.data().toDoc(options)));
+    }
+  }
+
+  record NotFullyApplied(@Override @NotNull WithPos<Expr> problemExpr) implements ClassError {
+    @Override public @NotNull Doc describe(@NotNull PrettierOptions options) {
+      return Doc.sep(Doc.english("Unable to new an incomplete class type:"), Doc.code(problemExpr.data().toDoc(options)));
+    }
+  }
+}
diff --git a/base/src/main/java/org/aya/tyck/tycker/AppTycker.java b/base/src/main/java/org/aya/tyck/tycker/AppTycker.java
index 9a192e8a9..53b6b0240 100644
--- a/base/src/main/java/org/aya/tyck/tycker/AppTycker.java
+++ b/base/src/main/java/org/aya/tyck/tycker/AppTycker.java
@@ -5,6 +5,7 @@
 import kala.collection.Seq;
 import kala.collection.SeqView;
 import kala.collection.immutable.ImmutableArray;
+import kala.collection.immutable.ImmutableSeq;
 import kala.function.CheckedBiFunction;
 import org.aya.generic.stmt.Shaped;
 import org.aya.syntax.compile.JitCon;
@@ -12,27 +13,31 @@
 import org.aya.syntax.compile.JitFn;
 import org.aya.syntax.compile.JitPrim;
 import org.aya.syntax.concrete.stmt.decl.*;
+import org.aya.syntax.core.Closure;
 import org.aya.syntax.core.def.*;
 import org.aya.syntax.core.repr.AyaShape;
-import org.aya.syntax.core.term.FreeTerm;
-import org.aya.syntax.core.term.Term;
+import org.aya.syntax.core.term.*;
 import org.aya.syntax.core.term.call.*;
 import org.aya.syntax.ref.DefVar;
 import org.aya.syntax.ref.LocalVar;
 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;
 import org.jetbrains.annotations.Nullable;
 
-import java.util.function.Function;
+import java.util.function.BiFunction;
 
 public record AppTycker<Ex extends Exception>(
-  @NotNull TyckState state, @NotNull SourcePos pos,
-  int argsCount, int lift, @NotNull Factory<Ex> makeArgs
-) {
+  @Override @NotNull TyckState state,
+  @NotNull AbstractTycker tycker,
+  @NotNull SourcePos pos,
+  int argsCount, int lift,
+  @NotNull Factory<Ex> makeArgs
+) implements Stateful {
   /**
    * <pre>
    * Signature (0th param) --------> Argument Parser (this interface)
@@ -45,7 +50,14 @@ public record AppTycker<Ex extends Exception>(
    */
   @FunctionalInterface
   public interface Factory<Ex extends Exception> extends
-    CheckedBiFunction<AbstractTele, Function<Term[], Jdg>, Jdg, Ex> {
+    CheckedBiFunction<AbstractTele, BiFunction<Term[], Term, Jdg>, Jdg, Ex> {
+  }
+
+  public AppTycker(
+    @NotNull AbstractTycker tycker, @NotNull SourcePos pos,
+    int argsCount, int lift, @NotNull Factory<Ex> makeArgs
+  ) {
+    this(tycker.state, tycker, pos, argsCount, lift, makeArgs);
   }
 
   public @NotNull Jdg checkCompiledApplication(@NotNull AbstractTele def) throws Ex {
@@ -93,7 +105,7 @@ public interface Factory<Ex extends Exception> extends
     // ownerTele + selfTele
     var fullSignature = conVar.signature().lift(lift);
 
-    return makeArgs.applyChecked(fullSignature, args -> {
+    return makeArgs.applyChecked(fullSignature, (args, _) -> {
       var realArgs = ImmutableArray.from(args);
       var ownerArgs = realArgs.take(conVar.ownerTeleSize());
       var conArgs = realArgs.drop(conVar.ownerTeleSize());
@@ -109,14 +121,14 @@ public interface Factory<Ex extends Exception> extends
   }
   private @NotNull Jdg checkPrimCall(@NotNull PrimDefLike primVar) throws Ex {
     var signature = primVar.signature().lift(lift);
-    return makeArgs.applyChecked(signature, args -> new Jdg.Default(
+    return makeArgs.applyChecked(signature, (args, _) -> new Jdg.Default(
       state.primFactory.unfold(new PrimCall(primVar, 0, ImmutableArray.from(args)), state),
       signature.result(args)
     ));
   }
   private @NotNull Jdg checkDataCall(@NotNull DataDefLike data) throws Ex {
     var signature = data.signature().lift(lift);
-    return makeArgs.applyChecked(signature, args -> new Jdg.Default(
+    return makeArgs.applyChecked(signature, (args, _) -> new Jdg.Default(
       new DataCall(data, 0, ImmutableArray.from(args)),
       signature.result(args)
     ));
@@ -125,7 +137,7 @@ public interface Factory<Ex extends Exception> extends
     @NotNull FnDefLike fnDef, @Nullable Shaped.Applicable<FnDefLike> operator
   ) throws Ex {
     var signature = fnDef.signature().lift(lift);
-    return makeArgs.applyChecked(signature, args -> {
+    return makeArgs.applyChecked(signature, (args, _) -> {
       var argsSeq = ImmutableArray.from(args);
       var result = signature.result(args);
       if (operator != null) {
@@ -137,10 +149,10 @@ public interface Factory<Ex extends Exception> extends
   }
 
   private @NotNull Jdg checkClassCall(@NotNull ClassDefLike clazz) throws Ex {
-    var appliedParams = ofClassMembers(clazz, argsCount).lift(lift);
     var self = LocalVar.generate("self");
+    var appliedParams = ofClassMembers(self, clazz, argsCount).lift(lift);
     state.classThis.push(self);
-    var result = makeArgs.applyChecked(appliedParams, args -> new Jdg.Default(
+    var result = makeArgs.applyChecked(appliedParams, (args, _) -> new Jdg.Default(
       new ClassCall(clazz, 0, ImmutableArray.from(args).map(x -> x.bind(self))),
       appliedParams.result(args)
     ));
@@ -150,23 +162,29 @@ public interface Factory<Ex extends Exception> extends
 
   private @NotNull Jdg checkProjCall(@NotNull MemberDefLike member) throws Ex {
     var signature = member.signature().lift(lift);
-    return makeArgs.applyChecked(signature, args -> {
+    return makeArgs.applyChecked(signature, (args, fstTy) -> {
       assert args.length >= 1;
+      var ofTy = whnf(fstTy);
+      if (!(ofTy instanceof ClassCall classTy)) throw new UnsupportedOperationException("report");   // TODO
       var fieldArgs = ImmutableArray.fill(args.length - 1, i -> args[i + 1]);
       return new Jdg.Default(
-        new MemberCall(args[0], member, 0, fieldArgs),
+        MemberCall.make(classTy, args[0], member, 0, fieldArgs),
         signature.result(args)
       );
     });
   }
 
-  static @NotNull AbstractTele ofClassMembers(@NotNull ClassDefLike def, int memberCount) {
+  private @NotNull AbstractTele ofClassMembers(@NotNull LocalVar self, @NotNull ClassDefLike def, int memberCount) {
+    var synthesizer = new Synthesizer(tycker);
     return switch (def) {
-      case ClassDef.Delegate delegate -> new TakeMembers(delegate.core(), memberCount);
+      case ClassDef.Delegate delegate -> new TakeMembers(self, delegate.core(), memberCount, synthesizer);
     };
   }
 
-  record TakeMembers(@NotNull ClassDef clazz, @Override int telescopeSize) implements AbstractTele {
+  record TakeMembers(
+    @NotNull LocalVar self, @NotNull ClassDef clazz,
+    @Override int telescopeSize, @NotNull Synthesizer synthesizer
+  ) implements AbstractTele {
     @Override public boolean telescopeLicit(int i) { return true; }
     @Override public @NotNull String telescopeName(int i) {
       assert i < telescopeSize;
@@ -175,18 +193,26 @@ record TakeMembers(@NotNull ClassDef clazz, @Override int telescopeSize) impleme
 
     // class Foo
     // | foo : A
-    // | + : A -> A -> A
+    // | infix + : A -> A -> A
     // | bar : Fn (x : Foo A) -> (x.foo) self.+ (self.foo)
     //                  instantiate these!   ^       ^
     @Override public @NotNull Term telescope(int i, Seq<Term> teleArgs) {
       // teleArgs are former members
       assert i < telescopeSize;
       var member = clazz.members().get(i);
-      return TyckDef.defSignature(member.ref()).makePi(Seq.of(new FreeTerm(clazz.ref().concrete.self)));
+      return TyckDef.defSignature(member.ref()).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());
     }
+
     @Override public @NotNull Term result(Seq<Term> teleArgs) {
-      // Use SigmaTerm::lub
-      throw new UnsupportedOperationException("TODO");
+      return clazz.members().view()
+        .drop(telescopeSize)
+        .map(member -> TyckDef.defSignature(member.ref()).inst(ImmutableSeq.of(new FreeTerm(self))).makePi(Seq.empty()))
+        .map(ty -> (SortTerm) synthesizer.synth(ty))
+        .foldLeft(SortTerm.Type0, SigmaTerm::lub);
     }
     @Override public @NotNull SeqView<String> namesView() {
       return clazz.members().sliceView(0, telescopeSize).map(i -> i.ref().name());
diff --git a/base/src/main/java/org/aya/unify/Synthesizer.java b/base/src/main/java/org/aya/unify/Synthesizer.java
index f2cde38dc..39c29fc89 100644
--- a/base/src/main/java/org/aya/unify/Synthesizer.java
+++ b/base/src/main/java/org/aya/unify/Synthesizer.java
@@ -136,6 +136,8 @@ case MetaCall(var ref, var args) when ref.req() instanceof MetaVar.OfType(var ty
       case MetaLitTerm mlt -> mlt.type();
       case StringTerm str -> state().primFactory.getCall(PrimDef.ID.STRING);
       case ClassCall classCall -> throw new UnsupportedOperationException("TODO");
+      case NewTerm newTerm -> newTerm.inner();
+      case ClassCastTerm castTerm -> new ClassCall(castTerm.ref(), 0, castTerm.remember());
     };
   }
 
diff --git a/base/src/main/java/org/aya/unify/TermComparator.java b/base/src/main/java/org/aya/unify/TermComparator.java
index 084ab5571..1cf54e1a7 100644
--- a/base/src/main/java/org/aya/unify/TermComparator.java
+++ b/base/src/main/java/org/aya/unify/TermComparator.java
@@ -145,14 +145,32 @@ public boolean compare(@NotNull Term preLhs, @NotNull Term preRhs, @Nullable Ter
     // ^ Beware of the order!!
     if (lhs instanceof MetaCall lMeta) {
       return solveMeta(lMeta, rhs, type) != null;
-    } else if (type == null) {
-      return compareUntyped(lhs, rhs) != null;
     }
 
-    var result = doCompareTyped(lhs, rhs, type);
+    if (rhs instanceof MemberCall && !(lhs instanceof MemberCall)) {
+      return swapped(() -> doCompare(rhs, lhs, type));
+    }
+
+    return doCompare(lhs, rhs, type);
+  }
+
+  /**
+   * Do compare {@param lhs} and {@param rhs} against type {@param type} (if not null),
+   * with assumption on a good {@param lhs}, see below.
+   *
+   * @param lhs is {@link MemberCall} if rhs is not;
+   *            if there is a {@link MetaCall} then it must be lhs.
+   *            Reason: we case on lhs.
+   */
+  private boolean doCompare(Term lhs, Term rhs, @Nullable Term type) {
+    var result = type == null
+      ? compareUntyped(lhs, rhs) != null
+      : doCompareTyped(lhs, rhs, type);
+
     if (!result) fail(lhs, rhs);
     return result;
   }
+
   private boolean checkApproxResult(@Nullable Term type, Term approxResult) {
     if (approxResult != null) {
       if (type != null) compare(approxResult, type, null);
@@ -168,9 +186,20 @@ private boolean checkApproxResult(@Nullable Term type, Term approxResult) {
    */
   private boolean doCompareTyped(@NotNull Term lhs, @NotNull Term rhs, @NotNull Term type) {
     return switch (whnf(type)) {
-      // TODO: ClassCall
       case LamTerm _, ConCallLike _, TupTerm _ -> Panic.unreachable();
       case ErrorTerm _ -> true;
+      case ClassCall classCall -> {
+        if (classCall.args().size() == classCall.ref().members().size()) yield true;
+        // TODO: skip comparing fields that already have impl specified in the type
+        yield classCall.ref().members().allMatch(member -> {
+          // loop invariant: first [i] members are the "same". ([i] is the loop counter, count from 0)
+          // Note that member can only refer to first [i] members, so it is safe that we supply [lhs] or [rhs]
+          var ty = member.signature().inst(ImmutableSeq.of(lhs));
+          var lproj = MemberCall.make(classCall, lhs, member, 0, ImmutableSeq.empty());
+          var rproj = MemberCall.make(classCall, rhs, member, 0, ImmutableSeq.empty());
+          return compare(lproj, rproj, ty.makePi(ImmutableSeq.empty()));
+        });
+      }
       case PiTerm pi -> switch (new Pair<>(lhs, rhs)) {
         case Pair(LamTerm(var lbody), LamTerm(var rbody)) -> subscoped(pi.param(), var ->
           compare(
@@ -206,9 +235,9 @@ case SigmaTerm(var paramSeq) -> {
   }
 
   /**
-   * Compare whnfed {@param preLhs} and whnfed {@param preRhs} without type information.
+   * Compare head-normalized {@param preLhs} and whnfed {@param preRhs} without type information.
    *
-   * @return the whnfed type of {@param preLhs} and {@param preRhs} if they are 'the same', null otherwise.
+   * @return the head-normalized type of {@param preLhs} and {@param preRhs} if they are 'the same', null otherwise.
    */
   private @Nullable Term compareUntyped(@NotNull Term preLhs, @NotNull Term preRhs) {
     {
@@ -225,9 +254,11 @@ case SigmaTerm(var paramSeq) -> {
     }
 
     Term result;
-    if (rhs instanceof MetaCall || rhs instanceof MetaLitTerm)
+    if (rhs instanceof MetaCall || rhs instanceof MetaLitTerm || rhs instanceof MemberCall) {
       result = swapped(() -> doCompareUntyped(rhs, lhs));
-    else result = doCompareUntyped(lhs, rhs);
+    } else {
+      result = doCompareUntyped(lhs, rhs);
+    }
     if (result != null) return whnf(result);
     fail(lhs, rhs);
     return null;
@@ -299,10 +330,20 @@ case ProjTerm(var lof, var ldx) -> {
         case MetaLitTerm mrt -> compareMetaLitWithLit(mlt, mrt.repr(), mrt.type());
         default -> null;
       };
+      case MemberCall memberCall -> {
+        // it is impossible that memberCall.of() is a cast term, since it is whnfed.
+        assert !(memberCall.of() instanceof ClassCastTerm);
+        if (rhs instanceof MemberCall memberCarr) {
+          assert !(memberCarr.of() instanceof ClassCastTerm);
+          yield compareUntyped(memberCall.of(), memberCarr.of());
+        } else {
+          yield null;
+        }
+      }
       // We already compare arguments in compareApprox, if we arrive here,
       // it means their arguments don't match (even the ref don't match),
       // so we are unable to do more if we can't normalize them.
-      case FnCall _, MemberCall _ -> null;
+      case FnCall _ -> null;
 
       default -> throw noRules(lhs);
     };
diff --git a/base/src/test/java/org/aya/tyck/TyckTest.java b/base/src/test/java/org/aya/tyck/TyckTest.java
index bc92b2188..1e74c5624 100644
--- a/base/src/test/java/org/aya/tyck/TyckTest.java
+++ b/base/src/test/java/org/aya/tyck/TyckTest.java
@@ -154,10 +154,11 @@ open inductive Phantom Nat Nat (A : Type) | mk A
       def infix = (a b : A) => Path (\\i => A) a b
       
       class Monoid
-      | carrier : Type
+      | classifying carrier : Type
       | unit : carrier
-      | op : carrier -> carrier -> carrier
-      | idl (x : carrier) : op unit x = x
+      | infix * : carrier -> carrier -> carrier
+        tighter =
+      | idl (x : carrier) : unit * x = x
       """).defs.isNotEmpty());
   }
 
diff --git a/cli-impl/src/main/java/org/aya/cli/literate/SyntaxHighlight.java b/cli-impl/src/main/java/org/aya/cli/literate/SyntaxHighlight.java
index 78fc1e562..26f6756d9 100644
--- a/cli-impl/src/main/java/org/aya/cli/literate/SyntaxHighlight.java
+++ b/cli-impl/src/main/java/org/aya/cli/literate/SyntaxHighlight.java
@@ -22,14 +22,7 @@
 import org.aya.syntax.concrete.stmt.ModuleName;
 import org.aya.syntax.concrete.stmt.Stmt;
 import org.aya.syntax.concrete.stmt.StmtVisitor;
-import org.aya.syntax.concrete.stmt.decl.DataCon;
-import org.aya.syntax.concrete.stmt.decl.DataDecl;
-import org.aya.syntax.concrete.stmt.decl.FnDecl;
-import org.aya.syntax.concrete.stmt.decl.PrimDecl;
-import org.aya.syntax.core.def.ConDef;
-import org.aya.syntax.core.def.DataDef;
-import org.aya.syntax.core.def.FnDef;
-import org.aya.syntax.core.def.PrimDef;
+import org.aya.syntax.concrete.stmt.decl.*;
 import org.aya.syntax.core.term.Term;
 import org.aya.syntax.ref.*;
 import org.aya.util.error.Panic;
@@ -144,21 +137,15 @@ else if (SPECIAL_SYMBOL.contains(tokenType))
   public static @NotNull DefKind kindOf(@NotNull AnyVar var) {
     return switch (var) {
       case GeneralizedVar _ -> DefKind.Generalized;
-      case DefVar<?, ?> defVar -> {
-        if (defVar.concrete instanceof FnDecl || defVar.core instanceof FnDef)
-          yield DefKind.Fn;
-//        else if (defVar.concrete instanceof TeleDecl.ClassMember || defVar.core instanceof MemberDef)
-//          yield DefKind.Member;
-        else if (defVar.concrete instanceof DataDecl || defVar.core instanceof DataDef)
-          yield DefKind.Data;
-        else if (defVar.concrete instanceof DataCon || defVar.core instanceof ConDef)
-          yield DefKind.Con;
-        else if (defVar.concrete instanceof PrimDecl || defVar.core instanceof PrimDef)
-          yield DefKind.Prim;
-//        else if (defVar.concrete instanceof ClassDecl || defVar.core instanceof ClassDef)
-//          yield DefKind.Clazz;
-        else throw new Panic(STR."unknown def type: \{defVar}");
-      }
+      case DefVar<?, ?> defVar -> switch (defVar.concrete) {
+        case FnDecl _ -> DefKind.Fn;
+        case ClassMember _ -> DefKind.Member;
+        case DataDecl _ -> DefKind.Data;
+        case DataCon _ -> DefKind.Con;
+        case PrimDecl _ -> DefKind.Prim;
+        case ClassDecl _ -> DefKind.Clazz;
+        default -> throw new Panic(STR."unknown def type: \{defVar}");
+      };
       case LocalVar(_, _, GenerateKind.Generalized(_)) -> DefKind.Generalized;
       case LocalVar _ -> DefKind.LocalVar;
       default -> DefKind.Unknown;
diff --git a/cli-impl/src/test/java/org/aya/test/TestRunner.java b/cli-impl/src/test/java/org/aya/test/TestRunner.java
index 7c2cbb9f9..ded56d246 100644
--- a/cli-impl/src/test/java/org/aya/test/TestRunner.java
+++ b/cli-impl/src/test/java/org/aya/test/TestRunner.java
@@ -43,7 +43,8 @@ public class TestRunner {
       PatTyckError.class,
       OperatorError.class,
       TerckError.class,
-      PatCohError.class
+      PatCohError.class,
+      ClassError.class
     ).forEachChecked(TestRunner::expectFixture);
     Files.deleteIfExists(TMP_FILE);
   }
diff --git a/cli-impl/src/test/java/org/aya/test/fixtures/ClassError.java b/cli-impl/src/test/java/org/aya/test/fixtures/ClassError.java
new file mode 100644
index 000000000..18afca89c
--- /dev/null
+++ b/cli-impl/src/test/java/org/aya/test/fixtures/ClassError.java
@@ -0,0 +1,19 @@
+// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
+// Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
+package org.aya.test.fixtures;
+
+import org.intellij.lang.annotations.Language;
+
+public interface ClassError {
+  @Language("Aya") String testNotClassCall = """
+    def what (A : Type) : A => new A
+    """;
+
+  @Language("Aya") String testNotFullyApplied = """
+    inductive Nat | O | S Nat
+    class Kontainer
+    | walue : Nat
+
+    def what : Kontainer => new Kontainer
+    """;
+}
diff --git a/cli-impl/src/test/resources/negative/ClassError.txt b/cli-impl/src/test/resources/negative/ClassError.txt
new file mode 100644
index 000000000..8f3427395
--- /dev/null
+++ b/cli-impl/src/test/resources/negative/ClassError.txt
@@ -0,0 +1,24 @@
+NotClassCall:
+In file $FILE:1:31 ->
+
+  1 │   def what (A : Type) : A => new A
+    │                                  ╰╯
+
+Error: Unable to new a non-class type: `A`
+
+1 error(s), 0 warning(s).
+Let's learn from that.
+
+NotFullyApplied:
+In file $FILE:5:28 ->
+
+  3 │   | walue : Nat
+  4 │   
+  5 │   def what : Kontainer => new Kontainer
+    │                               ╰───────╯
+
+Error: Unable to new an incomplete class type: `Kontainer`
+
+1 error(s), 0 warning(s).
+Let's learn from that.
+
diff --git a/cli-impl/src/test/resources/success/src/Classes.aya b/cli-impl/src/test/resources/success/src/Classes.aya
new file mode 100644
index 000000000..8df70f758
--- /dev/null
+++ b/cli-impl/src/test/resources/success/src/Classes.aya
@@ -0,0 +1,9 @@
+open import prelude
+
+class Kontainer
+| Taipe : Type
+| walue : Taipe
+
+def tyck0 : Nat => Kontainer::walue {new Kontainer Nat 0}
+
+ def norm0 : Kontainer::walue {new Kontainer Nat 0} = 0 => refl
diff --git a/jit-compiler/src/main/java/org/aya/compiler/ModuleSerializer.java b/jit-compiler/src/main/java/org/aya/compiler/ModuleSerializer.java
index 178213eb4..c4ccc6adf 100644
--- a/jit-compiler/src/main/java/org/aya/compiler/ModuleSerializer.java
+++ b/jit-compiler/src/main/java/org/aya/compiler/ModuleSerializer.java
@@ -45,10 +45,10 @@ private void doSerialize(@NotNull TyckDef unit) {
       case PrimDef primDef -> new PrimSerializer(this)
         .serialize(primDef);
       case ClassDef classDef -> {
-        throw new UnsupportedOperationException("ClassDef");
+        // throw new UnsupportedOperationException("ClassDef");
       }
       case MemberDef memberDef -> {
-        throw new UnsupportedOperationException("MemberDef");
+        // throw new UnsupportedOperationException("MemberDef");
       }
     }
   }
diff --git a/jit-compiler/src/main/java/org/aya/compiler/TermExprializer.java b/jit-compiler/src/main/java/org/aya/compiler/TermExprializer.java
index bbbe5b03a..331d60e05 100644
--- a/jit-compiler/src/main/java/org/aya/compiler/TermExprializer.java
+++ b/jit-compiler/src/main/java/org/aya/compiler/TermExprializer.java
@@ -46,6 +46,8 @@ public class TermExprializer extends AbstractExprializer<Term> {
   public static final String CLASS_RULEREDUCER = ExprializeUtils.getJavaReference(RuleReducer.class);
   public static final String CLASS_RULE_CON = ExprializeUtils.makeSub(CLASS_RULEREDUCER, ExprializeUtils.getJavaReference(RuleReducer.Con.class));
   public static final String CLASS_RULE_FN = ExprializeUtils.makeSub(CLASS_RULEREDUCER, ExprializeUtils.getJavaReference(RuleReducer.Fn.class));
+  public static final String CLASS_NEW = ExprializeUtils.getJavaReference(NewTerm.class);
+  public static final String CLASS_MEMCALL = ExprializeUtils.getJavaReference(MemberCall.class);
 
   /**
    * Terms that should be instantiated
@@ -72,15 +74,15 @@ public TermExprializer(@NotNull NameGenerator nameGen, @NotNull ImmutableSeq<Str
   private @NotNull String serializeApplicable(@NotNull Shaped.Applicable<?> applicable) {
     return switch (applicable) {
       case IntegerOps.ConRule conRule ->
-        ExprializeUtils.makeNew(CLASS_INT_CONRULE, ExprializeUtils.getInstance(NameSerializer.getClassReference(conRule.ref())),
+        ExprializeUtils.makeNew(CLASS_INT_CONRULE, ExprializeUtils.getInstance(getClassReference(conRule.ref())),
           doSerialize(conRule.zero())
         );
       case IntegerOps.FnRule fnRule -> ExprializeUtils.makeNew(CLASS_INT_FNRULE,
-        ExprializeUtils.getInstance(NameSerializer.getClassReference(fnRule.ref())),
+        ExprializeUtils.getInstance(getClassReference(fnRule.ref())),
         ExprializeUtils.makeSub(CLASS_FNRULE_KIND, fnRule.kind().toString())
       );
       case ListOps.ConRule conRule -> ExprializeUtils.makeNew(CLASS_LIST_CONRULE,
-        ExprializeUtils.getInstance(NameSerializer.getClassReference(conRule.ref())),
+        ExprializeUtils.getInstance(getClassReference(conRule.ref())),
         doSerialize(conRule.empty())
       );
       default -> Panic.unreachable();
@@ -134,33 +136,37 @@ case FreeTerm(var bind) -> {
       }
       case TyckInternal i -> throw new Panic(i.getClass().toString());
       case Callable.SharableCall call when call.ulift() == 0 && call.args().isEmpty() ->
-        ExprializeUtils.getEmptyCallTerm(NameSerializer.getClassReference(call.ref()));
+        ExprializeUtils.getEmptyCallTerm(getClassReference(call.ref()));
       case ClassCall classCall -> throw new UnsupportedOperationException("TODO");
-      case MemberCall memberCall -> throw new UnsupportedOperationException("TODO");
+      case MemberCall(var of, var ref, var ulift, var args) -> ExprializeUtils.makeNew(CLASS_MEMCALL,
+        doSerialize(of),
+        ExprializeUtils.getInstance(getClassReference(ref)),
+        Integer.toString(ulift),
+        serializeToImmutableSeq(CLASS_TERM, args)
+      );
       case AppTerm appTerm -> makeAppNew(CLASS_APPTERM, appTerm.fun(), appTerm.arg());
       case LocalTerm _ when !allowLocalTerm -> throw new Panic("LocalTerm");
       case LocalTerm(var index) -> ExprializeUtils.makeNew(CLASS_LOCALTERM, Integer.toString(index));
       case LamTerm lamTerm -> ExprializeUtils.makeNew(CLASS_LAMTERM, serializeClosure(lamTerm.body()));
       case DataCall(var ref, var ulift, var args) -> ExprializeUtils.makeNew(CLASS_DATACALL,
-        ExprializeUtils.getInstance(NameSerializer.getClassReference(ref)),
+        ExprializeUtils.getInstance(getClassReference(ref)),
         Integer.toString(ulift),
         serializeToImmutableSeq(CLASS_TERM, args)
       );
       case ConCall(var head, var args) -> ExprializeUtils.makeNew(CLASS_CONCALL,
-        ExprializeUtils.getInstance(NameSerializer.getClassReference(head.ref())),
+        ExprializeUtils.getInstance(getClassReference(head.ref())),
         serializeToImmutableSeq(CLASS_TERM, head.ownerArgs()),
         Integer.toString(head.ulift()),
         serializeToImmutableSeq(CLASS_TERM, args)
       );
       case FnCall call -> {
         var ref = switch (call.ref()) {
-          case JitFn jit -> ExprializeUtils.getInstance(NameSerializer.getClassReference(jit));
+          case JitFn jit -> ExprializeUtils.getInstance(getClassReference(jit));
           case FnDef.Delegate def -> ExprializeUtils.getInstance(getClassReference(def.ref));
         };
 
-        var ulift = call.ulift();
         var args = call.args();
-        yield buildReducibleCall(ref, CLASS_FNCALL, ulift, ImmutableSeq.of(args), true);
+        yield buildReducibleCall(ref, CLASS_FNCALL, call.ulift(), ImmutableSeq.of(args), true);
       }
       case RuleReducer.Con conRuler -> buildReducibleCall(
         serializeApplicable(conRuler.rule()),
@@ -208,24 +214,26 @@ case TupTerm(var items) -> ExprializeUtils.makeNew(ExprializeUtils.getJavaRefere
       );
       case SigmaTerm sigmaTerm -> throw new UnsupportedOperationException("TODO");
       case PrimCall(var ref, var ulift, var args) -> ExprializeUtils.makeNew(CLASS_PRIMCALL,
-        ExprializeUtils.getInstance(NameSerializer.getClassReference(ref)),
+        ExprializeUtils.getInstance(getClassReference(ref)),
         Integer.toString(ulift),
         serializeToImmutableSeq(CLASS_TERM, args)
       );
       case IntegerTerm(var repr, var zero, var suc, var type) -> ExprializeUtils.makeNew(CLASS_INTEGER,
         Integer.toString(repr),
-        ExprializeUtils.getInstance(NameSerializer.getClassReference(zero)),
-        ExprializeUtils.getInstance(NameSerializer.getClassReference(suc)),
+        ExprializeUtils.getInstance(getClassReference(zero)),
+        ExprializeUtils.getInstance(getClassReference(suc)),
         doSerialize(type)
       );
       case ListTerm(var repr, var nil, var cons, var type) -> ExprializeUtils.makeNew(CLASS_LIST,
         ExprializeUtils.makeImmutableSeq(CLASS_TERM, repr.map(this::doSerialize), CLASS_PIMMSEQ),
-        ExprializeUtils.getInstance(NameSerializer.getClassReference(nil)),
-        ExprializeUtils.getInstance(NameSerializer.getClassReference(cons)),
+        ExprializeUtils.getInstance(getClassReference(nil)),
+        ExprializeUtils.getInstance(getClassReference(cons)),
         doSerialize(type)
       );
-      case StringTerm stringTerm ->
-        ExprializeUtils.makeNew(CLASS_STRING, ExprializeUtils.makeString(StringUtil.escapeStringCharacters(stringTerm.string())));
+      case StringTerm stringTerm -> ExprializeUtils.makeNew(CLASS_STRING,
+        ExprializeUtils.makeString(StringUtil.escapeStringCharacters(stringTerm.string())));
+      case ClassCastTerm classCastTerm -> throw new UnsupportedOperationException("TODO");
+      case NewTerm(var classCall) -> ExprializeUtils.makeNew(CLASS_NEW, doSerialize(classCall));
     };
   }
 
diff --git a/syntax/src/main/java/org/aya/prettier/BasePrettier.java b/syntax/src/main/java/org/aya/prettier/BasePrettier.java
index f93547369..3a2cf4d45 100644
--- a/syntax/src/main/java/org/aya/prettier/BasePrettier.java
+++ b/syntax/src/main/java/org/aya/prettier/BasePrettier.java
@@ -7,6 +7,7 @@
 import kala.collection.SeqView;
 import kala.collection.mutable.MutableList;
 import kala.collection.mutable.primitive.MutableBooleanList;
+import kala.collection.primitive.BooleanSeq;
 import org.aya.generic.AyaDocile;
 import org.aya.generic.term.ParamLike;
 import org.aya.pretty.doc.Doc;
@@ -98,10 +99,11 @@ protected BasePrettier(@NotNull PrettierOptions options) {
 
     // Because the signature of DataCon is selfTele, so we only need to deal with core con
     var licit = switch (var) {
-      case TyckAnyDef<?> inner -> inner.core() instanceof SubLevelDef sub ?
-        sub.selfTele.mapToBoolean(MutableBooleanList.factory(), Param::explicit) :
-        Objects.requireNonNull(inner.ref.signature).params()
-          .mapToBooleanTo(MutableBooleanList.create(), Param::explicit);
+      case TyckAnyDef<?> inner -> inner.core() instanceof SubLevelDef sub
+        ? sub.selfTele.mapToBoolean(MutableBooleanList.factory(), Param::explicit)
+        : inner.ref.signature == null
+          ? BooleanSeq.fill(preArgs.size(), true)
+          : inner.ref.signature.params().mapToBooleanTo(MutableBooleanList.create(), Param::explicit);
       case JitDef jit -> MutableBooleanList.from(jit.telescopeLicit);
       default -> throw new UnsupportedOperationException("TODO");
     };
diff --git a/syntax/src/main/java/org/aya/prettier/CorePrettier.java b/syntax/src/main/java/org/aya/prettier/CorePrettier.java
index e9c539e60..2e6865e74 100644
--- a/syntax/src/main/java/org/aya/prettier/CorePrettier.java
+++ b/syntax/src/main/java/org/aya/prettier/CorePrettier.java
@@ -199,6 +199,7 @@ case ErrorTerm(var desc, var isReallyError) -> {
       }
       case ClassCall classCall ->
         visitCoreCalls(classCall.ref(), classCall.args().map(x -> x.apply(SELF)), outer, true);
+      case NewTerm newTerm -> Doc.sep(KW_NEW, term(Outer.Free, newTerm.inner()));
       case DataCall dataCall -> visitCoreCalls(dataCall.ref(), dataCall.args(), outer, optionImplicit());
       case StringTerm(var str) -> Doc.plain("\"" + StringUtil.escapeStringCharacters(str) + "\"");
       case PAppTerm app -> visitCalls(null, term(Outer.AppHead, app.fun()),
@@ -218,6 +219,7 @@ case EqTerm(var _, var a, var b) -> {
         yield checkParen(outer, doc, Outer.BinOp);
       }
       case RuleReducer.Fn fn -> term(outer, fn.toFnCall());
+      case ClassCastTerm classCastTerm -> term(outer, classCastTerm.subterm());
     };
   }
 
diff --git a/syntax/src/main/java/org/aya/syntax/concrete/Expr.java b/syntax/src/main/java/org/aya/syntax/concrete/Expr.java
index cda6060ea..5a6916a97 100644
--- a/syntax/src/main/java/org/aya/syntax/concrete/Expr.java
+++ b/syntax/src/main/java/org/aya/syntax/concrete/Expr.java
@@ -318,9 +318,7 @@ record LitString(@NotNull String string) implements Expr {
     @Override public void forEach(@NotNull PosedConsumer<Expr> f) { }
   }
 
-  record New(
-    @NotNull WithPos<Expr> classCall
-  ) implements Expr {
+  record New(@NotNull WithPos<Expr> classCall) implements Expr {
     public @NotNull Expr.New update(@NotNull WithPos<Expr> classCall) {
       return classCall == classCall() ? this : new New(classCall);
     }
@@ -329,10 +327,7 @@ record New(
       return update(classCall.descent(f));
     }
 
-    @Override
-    public void forEach(@NotNull PosedConsumer<@NotNull Expr> f) {
-      f.accept(classCall);
-    }
+    @Override public void forEach(@NotNull PosedConsumer<@NotNull Expr> f) { f.accept(classCall); }
   }
 
   record Idiom(
diff --git a/syntax/src/main/java/org/aya/syntax/core/def/MemberDef.java b/syntax/src/main/java/org/aya/syntax/core/def/MemberDef.java
index 9db5eefba..b52b1b39c 100644
--- a/syntax/src/main/java/org/aya/syntax/core/def/MemberDef.java
+++ b/syntax/src/main/java/org/aya/syntax/core/def/MemberDef.java
@@ -12,19 +12,30 @@
 
 /**
  * A class field definition.
+ *
  * @param telescope it is bound with the `self` pointer, so whenever you need to make sense of this type,
  *                  you need to inst its elements with `self` first.
  */
 public record MemberDef(
   @NotNull DefVar<ClassDef, ClassDecl> classRef,
   @Override @NotNull DefVar<MemberDef, ClassMember> ref,
+  int index,
   @Override ImmutableSeq<Param> telescope,
   @Override @NotNull Term result
 ) implements TyckDef {
-  public MemberDef { ref.initialize(this); }
+  public MemberDef {
+    assert index >= 0;
+    ref.initialize(this);
+  }
+
   public static final class Delegate extends TyckAnyDef<MemberDef> implements MemberDefLike {
     public Delegate(@NotNull DefVar<MemberDef, ?> ref) { super(ref); }
 
+    /**
+     * this implementation prevents invocation of {@link ClassDef.Delegate#members()} while tycking {@link ClassDef}
+     */
+    @Override public int index() { return ref.core.index; }
+
     @Override public @NotNull ClassDefLike classRef() {
       return new ClassDef.Delegate(core().classRef());
     }
diff --git a/syntax/src/main/java/org/aya/syntax/core/def/MemberDefLike.java b/syntax/src/main/java/org/aya/syntax/core/def/MemberDefLike.java
index f698d85fa..f1c97084d 100644
--- a/syntax/src/main/java/org/aya/syntax/core/def/MemberDefLike.java
+++ b/syntax/src/main/java/org/aya/syntax/core/def/MemberDefLike.java
@@ -6,4 +6,10 @@
 
 public sealed interface MemberDefLike extends AnyDef permits MemberDef.Delegate {
   @NotNull ClassDefLike classRef();
+
+  default int index() {
+    var idx = classRef().members().indexOf(this);
+    assert idx >= 0;
+    return idx;
+  }
 }
diff --git a/syntax/src/main/java/org/aya/syntax/core/term/ClassCastTerm.java b/syntax/src/main/java/org/aya/syntax/core/term/ClassCastTerm.java
new file mode 100644
index 000000000..cfa77cdd0
--- /dev/null
+++ b/syntax/src/main/java/org/aya/syntax/core/term/ClassCastTerm.java
@@ -0,0 +1,55 @@
+// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
+// Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
+package org.aya.syntax.core.term;
+
+import kala.collection.immutable.ImmutableSeq;
+import kala.function.IndexedFunction;
+import org.aya.syntax.core.Closure;
+import org.aya.syntax.core.def.ClassDefLike;
+import org.aya.syntax.core.def.MemberDefLike;
+import org.aya.syntax.core.term.marker.StableWHNF;
+import org.jetbrains.annotations.NotNull;
+import org.jetbrains.annotations.Nullable;
+
+/**
+ * This term is used for subtyping of class, a term {@code x : SomeClass (foo := 114514)} is treated an
+ * instance of {@code SomeClass} in user side. In core side, we use {@code cast x [] [(foo := 114514)] : SomeClass}
+ * to make {@code x} an instance of {@code SomeClass}, it also store the type information in expression
+ * so that the {@link org.aya.syntax.core.term.call.MemberCall} can access them without synthesizing.
+ */
+public record ClassCastTerm(
+  @NotNull ClassDefLike ref,
+  @NotNull Term subterm,
+  @NotNull ImmutableSeq<Closure> remember,
+  @NotNull ImmutableSeq<Closure> forget
+) implements StableWHNF, Term {
+  public ClassCastTerm {
+    assert forget.isNotEmpty();
+  }
+
+  public @NotNull ClassCastTerm update(
+    @NotNull Term subterm,
+    @NotNull ImmutableSeq<Closure> remember,
+    @NotNull ImmutableSeq<Closure> forget
+  ) {
+    return this.subterm == subterm
+      && this.remember.sameElements(remember, true)
+      && this.forget.sameElements(forget, true)
+      ? this
+      : new ClassCastTerm(ref, subterm, remember, forget);
+  }
+
+  @Override
+  public @NotNull Term descent(@NotNull IndexedFunction<Term, Term> f) {
+    return update(f.apply(0, subterm), remember.map(x -> x.descent(f)), forget.map(x -> x.descent(f)));
+  }
+
+  public @Nullable Closure get(@NotNull MemberDefLike member) {
+    assert ref.equals(member.classRef());
+    var idx = member.index();
+    if (idx < remember.size()) return remember.get(idx);
+    idx = idx - remember.size();
+    if (idx < forget.size()) return forget.get(idx);
+    return null;
+  }
+}
diff --git a/syntax/src/main/java/org/aya/syntax/core/term/NewTerm.java b/syntax/src/main/java/org/aya/syntax/core/term/NewTerm.java
new file mode 100644
index 000000000..15165ebb1
--- /dev/null
+++ b/syntax/src/main/java/org/aya/syntax/core/term/NewTerm.java
@@ -0,0 +1,30 @@
+// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
+// Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
+package org.aya.syntax.core.term;
+
+import kala.function.IndexedFunction;
+import org.aya.syntax.core.term.call.ClassCall;
+import org.aya.syntax.core.term.marker.StableWHNF;
+import org.jetbrains.annotations.NotNull;
+
+/**
+ * Term that constructs an instance of some {@link ClassCall}.
+ * NewTerm has the same structure as a fully applied {@link ClassCall},
+ * as it has only one instance.
+ */
+public record NewTerm(@NotNull ClassCall inner) implements StableWHNF {
+  public NewTerm {
+    assert inner.args().size() == inner.ref().members().size();
+  }
+
+  public @NotNull NewTerm update(@NotNull ClassCall classCall) {
+    if (classCall == inner) return this;
+    return new NewTerm(classCall);
+  }
+
+  @Override
+  public @NotNull Term descent(@NotNull IndexedFunction<Term, Term> f) {
+    // not `f.apply(0, inner)`, since the `ClassCall` is considered to be flatten
+    return inner.descent(f);
+  }
+}
diff --git a/syntax/src/main/java/org/aya/syntax/core/term/Term.java b/syntax/src/main/java/org/aya/syntax/core/term/Term.java
index 0b703235e..af05cf992 100644
--- a/syntax/src/main/java/org/aya/syntax/core/term/Term.java
+++ b/syntax/src/main/java/org/aya/syntax/core/term/Term.java
@@ -28,7 +28,7 @@
 import java.util.function.UnaryOperator;
 
 public sealed interface Term extends Serializable, AyaDocile
-  permits BetaRedex, Formation, LocalTerm, StableWHNF, TyckInternal, Callable, CoeTerm {
+  permits ClassCastTerm, LocalTerm, Callable, BetaRedex, Formation, StableWHNF, TyckInternal, CoeTerm {
 
   @Override default @NotNull Doc toDoc(@NotNull PrettierOptions options) {
     return new CorePrettier(options).term(BasePrettier.Outer.Free, this);
diff --git a/syntax/src/main/java/org/aya/syntax/core/term/call/ClassCall.java b/syntax/src/main/java/org/aya/syntax/core/term/call/ClassCall.java
index 27035517e..0c8427833 100644
--- a/syntax/src/main/java/org/aya/syntax/core/term/call/ClassCall.java
+++ b/syntax/src/main/java/org/aya/syntax/core/term/call/ClassCall.java
@@ -5,11 +5,15 @@
 import kala.collection.immutable.ImmutableSeq;
 import kala.function.IndexedFunction;
 import org.aya.syntax.core.Closure;
+import org.aya.syntax.core.def.AnyDef;
 import org.aya.syntax.core.def.ClassDefLike;
+import org.aya.syntax.core.def.MemberDefLike;
+import org.aya.syntax.core.term.NewTerm;
 import org.aya.syntax.core.term.Term;
 import org.aya.syntax.core.term.marker.Formation;
 import org.aya.syntax.core.term.marker.StableWHNF;
 import org.jetbrains.annotations.NotNull;
+import org.jetbrains.annotations.Nullable;
 
 /**
  * ClassCall is a very special construction in Aya.
@@ -44,6 +48,11 @@ public record ClassCall(
     return update(args.map(t -> t.descent(f)));
   }
 
+  public @Nullable Closure get(@NotNull MemberDefLike member) {
+    assert ref.equals(member.classRef());
+    return args.getOrNull(member.index());
+  }
+
   @Override public @NotNull Term doElevate(int level) {
     return new ClassCall(ref, ulift + level, args);
   }
diff --git a/syntax/src/main/java/org/aya/syntax/core/term/call/MemberCall.java b/syntax/src/main/java/org/aya/syntax/core/term/call/MemberCall.java
index 01d92ddef..d5d9dcdc1 100644
--- a/syntax/src/main/java/org/aya/syntax/core/term/call/MemberCall.java
+++ b/syntax/src/main/java/org/aya/syntax/core/term/call/MemberCall.java
@@ -5,7 +5,10 @@
 import kala.collection.immutable.ImmutableSeq;
 import kala.function.IndexedFunction;
 import org.aya.syntax.core.def.MemberDefLike;
+import org.aya.syntax.core.term.ClassCastTerm;
+import org.aya.syntax.core.term.NewTerm;
 import org.aya.syntax.core.term.Term;
+import org.aya.syntax.core.term.marker.BetaRedex;
 import org.jetbrains.annotations.NotNull;
 
 public record MemberCall(
@@ -13,7 +16,7 @@ public record MemberCall(
   @Override @NotNull MemberDefLike ref,
   @Override int ulift,
   @Override @NotNull ImmutableSeq<@NotNull Term> args
-) implements Callable.Tele {
+) implements Callable.Tele, BetaRedex {
   private MemberCall update(Term clazz, ImmutableSeq<Term> newArgs) {
     return clazz == of && newArgs.sameElements(args, true) ? this
       : new MemberCall(clazz, ref, ulift, newArgs);
@@ -22,4 +25,33 @@ private MemberCall update(Term clazz, ImmutableSeq<Term> newArgs) {
   @Override public @NotNull Term descent(@NotNull IndexedFunction<Term, Term> f) {
     return update(f.apply(0, of), Callable.descent(args, f));
   }
+
+  public static @NotNull Term make(
+    @NotNull ClassCall typeOfOf,
+    @NotNull Term of,
+    @NotNull MemberDefLike ref,
+    int ulift,
+    @NotNull ImmutableSeq<@NotNull Term> args
+  ) {
+    var impl = typeOfOf.get(ref);
+    if (impl != null) return impl.apply(of);
+    return new MemberCall(of, ref, ulift, args).make();
+  }
+
+  @Override public @NotNull Term make() {
+    return switch (of()) {
+      case NewTerm neu -> {
+        var impl = neu.inner().get(ref);
+        assert impl != null;    // NewTerm is always fully applied
+        yield impl.apply(neu);
+      }
+      case ClassCastTerm cast -> {
+        var impl = cast.get(ref);
+        if (impl != null) yield impl.apply(cast);
+        // no impl, try inner
+        yield update(cast.subterm(), args);
+      }
+      default -> this;
+    };
+  }
 }
diff --git a/syntax/src/main/java/org/aya/syntax/core/term/marker/BetaRedex.java b/syntax/src/main/java/org/aya/syntax/core/term/marker/BetaRedex.java
index 167352e3d..71a911869 100644
--- a/syntax/src/main/java/org/aya/syntax/core/term/marker/BetaRedex.java
+++ b/syntax/src/main/java/org/aya/syntax/core/term/marker/BetaRedex.java
@@ -5,9 +5,10 @@
 import org.aya.syntax.core.term.AppTerm;
 import org.aya.syntax.core.term.ProjTerm;
 import org.aya.syntax.core.term.Term;
+import org.aya.syntax.core.term.call.MemberCall;
 import org.aya.syntax.core.term.xtt.PAppTerm;
 import org.jetbrains.annotations.NotNull;
 
-public sealed interface BetaRedex extends Term permits AppTerm, PAppTerm, ProjTerm {
+public sealed interface BetaRedex extends Term permits AppTerm, ProjTerm, MemberCall, PAppTerm {
   @NotNull Term make();
 }
diff --git a/syntax/src/main/java/org/aya/syntax/core/term/marker/StableWHNF.java b/syntax/src/main/java/org/aya/syntax/core/term/marker/StableWHNF.java
index 2069082f5..b0a408ab2 100644
--- a/syntax/src/main/java/org/aya/syntax/core/term/marker/StableWHNF.java
+++ b/syntax/src/main/java/org/aya/syntax/core/term/marker/StableWHNF.java
@@ -16,5 +16,5 @@
  * after a substitution (this usually happens under face restrictions (aka cofibrations)).
  */
 public sealed interface StableWHNF extends Term
-  permits ErrorTerm, LamTerm, PiTerm, SigmaTerm, SortTerm, TupTerm, ClassCall, DataCall, IntegerTerm, ListTerm, StringTerm, DimTerm, EqTerm {
+  permits ClassCastTerm, ErrorTerm, LamTerm, NewTerm, PiTerm, SigmaTerm, SortTerm, TupTerm, ClassCall, DataCall, IntegerTerm, ListTerm, StringTerm, DimTerm, EqTerm {
 }
diff --git a/tools/src/main/java/org/aya/util/MapUtil.java b/tools/src/main/java/org/aya/util/MapUtil.java
new file mode 100644
index 000000000..b8047c50e
--- /dev/null
+++ b/tools/src/main/java/org/aya/util/MapUtil.java
@@ -0,0 +1,21 @@
+// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
+// Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
+package org.aya.util;
+
+import kala.collection.immutable.ImmutableMap;
+import org.jetbrains.annotations.NotNull;
+
+public interface MapUtil {
+  static <K, V> boolean sameElements(@NotNull ImmutableMap<K, V> lhs, @NotNull ImmutableMap<K, V> rhs) {
+    if (lhs.size() != rhs.size()) return false;
+
+    var it = lhs.iterator();
+    while (it.hasNext()) {
+      var pair = it.next();
+      if (!rhs.containsKey(pair.component1())) return false;
+      if (pair.component2() != rhs.get(pair.component1())) return false;
+    }
+
+    return true;
+  }
+}