diff --git a/base/src/main/java/org/aya/core/Meta.java b/base/src/main/java/org/aya/core/Meta.java
index cffd050c21..02b059d1ae 100644
--- a/base/src/main/java/org/aya/core/Meta.java
+++ b/base/src/main/java/org/aya/core/Meta.java
@@ -67,13 +67,13 @@ private Meta(
 
   public @NotNull FormTerm.Pi asPi(
     @NotNull String domName, @NotNull String codName, boolean explicit,
-    @NotNull ImmutableSeq<Arg<Term>> contextArgs
+    int ulift, @NotNull ImmutableSeq<Arg<Term>> contextArgs
   ) {
     assert telescope.isEmpty();
     var domVar = Meta.from(contextTele, domName, result, sourcePos);
     var codVar = Meta.from(contextTele, codName, result, sourcePos);
-    var dom = new CallTerm.Hole(domVar, contextArgs, ImmutableSeq.empty());
-    var cod = new CallTerm.Hole(codVar, contextArgs, ImmutableSeq.empty());
+    var dom = new CallTerm.Hole(domVar, ulift, contextArgs, ImmutableSeq.empty());
+    var cod = new CallTerm.Hole(codVar, ulift, contextArgs, ImmutableSeq.empty());
     var domParam = new Term.Param(Constants.randomlyNamed(sourcePos), dom, explicit);
     return new FormTerm.Pi(domParam, cod);
   }
diff --git a/base/src/main/java/org/aya/core/term/CallTerm.java b/base/src/main/java/org/aya/core/term/CallTerm.java
index 2f60e71343..33cd39a00b 100644
--- a/base/src/main/java/org/aya/core/term/CallTerm.java
+++ b/base/src/main/java/org/aya/core/term/CallTerm.java
@@ -36,7 +36,7 @@ interface Factory<D extends Def, S extends Signatured> {
   make(@NotNull Term f, @NotNull Arg<Term> arg) {
     if (f instanceof Hole hole) {
       if (hole.args.sizeLessThan(hole.ref.telescope))
-        return new Hole(hole.ref, hole.contextArgs, hole.args.appended(arg));
+        return new Hole(hole.ref, hole.ulift, hole.contextArgs, hole.args.appended(arg));
     }
     if (!(f instanceof IntroTerm.Lambda lam)) return new ElimTerm.App(f, 0, arg);
     return make(lam, arg);
@@ -149,11 +149,12 @@ public Con(
    */
   record Hole(
     @NotNull Meta ref,
+    int ulift,
     @NotNull ImmutableSeq<@NotNull Arg<@NotNull Term>> contextArgs,
     @NotNull ImmutableSeq<@NotNull Arg<@NotNull Term>> args
   ) implements CallTerm {
     public @NotNull FormTerm.Pi asPi(boolean explicit) {
-      return ref.asPi(ref.name() + "dom", ref.name() + "cod", explicit, contextArgs);
+      return ref.asPi(ref.name() + "dom", ref.name() + "cod", explicit, ulift, contextArgs);
     }
 
     public @NotNull SeqView<@NotNull Arg<Term>> fullArgs() {
@@ -163,11 +164,6 @@ record Hole(
     @Override public <P, R> R doAccept(@NotNull Visitor<P, R> visitor, P p) {
       return visitor.visitHole(this, p);
     }
-
-    @Override public int ulift() {
-      // TODO[lift-meta]: we should be able to lift a meta
-      return 0;
-    }
   }
 
   /**
diff --git a/base/src/main/java/org/aya/core/visitor/TermConsumer.java b/base/src/main/java/org/aya/core/visitor/TermConsumer.java
index 856c5e4c0c..f9aa96ac7c 100644
--- a/base/src/main/java/org/aya/core/visitor/TermConsumer.java
+++ b/base/src/main/java/org/aya/core/visitor/TermConsumer.java
@@ -9,9 +9,13 @@
 import org.jetbrains.annotations.NotNull;
 
 public interface TermConsumer<P> extends Term.Visitor<P, Unit> {
+  default void visitCall(@NotNull CallTerm call, P p) {
+  }
+
   @Override default Unit visitHole(@NotNull CallTerm.Hole term, P p) {
     visitArgs(p, term.args());
     visitArgs(p, term.contextArgs());
+    visitCall(term, p);
     // TODO[ice]: is it fine? Maybe we want to visit the solutions as well?
     // var body = term.ref().body;
     // if (body != null) body.accept(this, p);
@@ -56,28 +60,33 @@ default void visitArg(@NotNull Arg<? extends Term> arg, P p) {
 
   @Override default Unit visitFnCall(@NotNull CallTerm.Fn fnCall, P p) {
     visitArgs(p, fnCall.args());
+    visitCall(fnCall, p);
     return Unit.unit();
   }
 
   @Override default Unit visitPrimCall(CallTerm.@NotNull Prim prim, P p) {
     visitArgs(p, prim.args());
+    visitCall(prim, p);
     return Unit.unit();
   }
 
 
   @Override default Unit visitDataCall(@NotNull CallTerm.Data dataCall, P p) {
     visitArgs(p, dataCall.args());
+    visitCall(dataCall, p);
     return Unit.unit();
   }
 
   @Override default Unit visitConCall(@NotNull CallTerm.Con conCall, P p) {
     visitArgs(p, conCall.head().dataArgs());
     visitArgs(p, conCall.conArgs());
+    visitCall(conCall, p);
     return Unit.unit();
   }
 
   @Override default Unit visitStructCall(@NotNull CallTerm.Struct structCall, P p) {
     visitArgs(p, structCall.args());
+    visitCall(structCall, p);
     return Unit.unit();
   }
 
@@ -110,6 +119,7 @@ default void visitArgs(P p, SeqLike<Arg<@NotNull Term>> args) {
 
   @Override default Unit visitAccess(@NotNull CallTerm.Access term, P p) {
     visitArgs(p, term.fieldArgs());
+    visitCall(term, p);
     return term.of().accept(this, p);
   }
 }
diff --git a/base/src/main/java/org/aya/core/visitor/TermFixpoint.java b/base/src/main/java/org/aya/core/visitor/TermFixpoint.java
index de1263f7de..bc60d2b2a4 100644
--- a/base/src/main/java/org/aya/core/visitor/TermFixpoint.java
+++ b/base/src/main/java/org/aya/core/visitor/TermFixpoint.java
@@ -17,9 +17,10 @@ public interface TermFixpoint<P> extends Term.Visitor<P, @NotNull Term> {
   @Override default @NotNull Term visitHole(@NotNull CallTerm.Hole term, P p) {
     var contextArgs = term.contextArgs().map(arg -> visitArg(arg, p));
     var args = term.args().map(arg -> visitArg(arg, p));
-    if (term.contextArgs().sameElements(contextArgs, true)
+    if (ulift() == 0
+      && term.contextArgs().sameElements(contextArgs, true)
       && term.args().sameElements(args, true)) return term;
-    return new CallTerm.Hole(term.ref(), contextArgs, args);
+    return new CallTerm.Hole(term.ref(), ulift() + term.ulift(), contextArgs, args);
   }
   @Override
   default @NotNull Term visitFieldRef(@NotNull RefTerm.Field term, P p) {
diff --git a/base/src/main/java/org/aya/tyck/env/LocalCtx.java b/base/src/main/java/org/aya/tyck/env/LocalCtx.java
index d4df5c554b..aabafaf993 100644
--- a/base/src/main/java/org/aya/tyck/env/LocalCtx.java
+++ b/base/src/main/java/org/aya/tyck/env/LocalCtx.java
@@ -33,7 +33,7 @@ public sealed interface LocalCtx permits MapLocalCtx, SeqLocalCtx {
   freshHole(@Nullable Term type, @NotNull String name, @NotNull SourcePos sourcePos) {
     var ctxTele = extract();
     var meta = Meta.from(ctxTele, name, type, sourcePos);
-    var hole = new CallTerm.Hole(meta, ctxTele.map(Term.Param::toArg), meta.telescope.map(Term.Param::toArg));
+    var hole = new CallTerm.Hole(meta, 0, ctxTele.map(Term.Param::toArg), meta.telescope.map(Term.Param::toArg));
     return Tuple2.of(hole, IntroTerm.Lambda.make(meta.telescope, hole));
   }
   default <T> T with(@NotNull Term.Param param, @NotNull Supplier<T> action) {
diff --git a/base/src/main/java/org/aya/tyck/unify/DefEq.java b/base/src/main/java/org/aya/tyck/unify/DefEq.java
index 0eb9088fc6..39afc625ec 100644
--- a/base/src/main/java/org/aya/tyck/unify/DefEq.java
+++ b/base/src/main/java/org/aya/tyck/unify/DefEq.java
@@ -380,75 +380,83 @@ yield checkParam(lhs.param(), rhs.param(), null, lr, rl, () -> null, () -> {
         if (lhs.ref() != rhs.ref()) yield null;
         yield Def.defResult(lhs.ref());
       }
-      case CallTerm.Hole lhs -> {
-        var meta = lhs.ref();
-        if (preRhs instanceof CallTerm.Hole rcall && lhs.ref() == rcall.ref()) {
-          // If we do not know the type, then we do not perform the comparison
-          if (meta.result == null) yield null;
-          var holeTy = FormTerm.Pi.make(meta.telescope, meta.result);
-          for (var arg : lhs.args().view().zip(rcall.args())) {
-            if (!(holeTy instanceof FormTerm.Pi holePi))
-              throw new IllegalStateException("meta arg size larger than param size. this should not happen");
-            if (!compare(arg._1.term(), arg._2.term(), lr, rl, holePi.param().type())) yield null;
-            holeTy = holePi.substBody(arg._1.term());
-          }
-          yield holeTy;
-        }
-        // Long time ago I wrote this to generate more unification equations,
-        // which solves more universe levels. However, with latest version Aya (0.13),
-        // removing this does not break anything.
-        // Update: this is still needed, see #327 last task (`coe'`)
-        var resultTy = preRhs.computeType(state, ctx);
-        if (meta.result != null) compareUntyped(resultTy, meta.result, rl, lr);
-        var argSubst = extract(lhs, preRhs, meta);
-        if (argSubst == null) {
-          reporter.report(new HoleProblem.BadSpineError(lhs, pos));
-          yield null;
-        }
-        var subst = Unfolder.buildSubst(meta.contextTele, lhs.contextArgs());
-        // In this case, the solution may not be unique (see #608),
-        // so we may delay its resolution to the end of the tycking when we disallow vague unification.
-        if (!allowVague && subst.overlap(argSubst).anyMatch(var -> preRhs.findUsages(var) > 0)) {
-          state.addEqn(createEqn(lhs, preRhs, lr, rl));
-          // Skip the unification and scope check
-          yield meta.result;
-        }
-        subst.add(argSubst);
-        // TODO
-        // TODO: what's the TODO above? I don't know what's TODO? ????
-        rl.map.forEach(subst::add);
-        assert !state.metas().containsKey(meta);
-        var solved = preRhs.freezeHoles(state).subst(subst);
-        var allowedVars = meta.fullTelescope().map(Term.Param::ref).toImmutableSeq();
-        var scopeCheck = solved.scopeCheck(allowedVars);
-        if (scopeCheck.invalid.isNotEmpty()) {
-          // Normalization may remove the usages of certain variables
-          solved = solved.normalize(state, NormalizeMode.NF);
-          scopeCheck = solved.scopeCheck(allowedVars);
-        }
-        if (scopeCheck.invalid.isNotEmpty()) {
-          reporter.report(new HoleProblem.BadlyScopedError(lhs, solved, scopeCheck.invalid, pos));
-          yield new ErrorTerm(solved);
-        }
-        if (scopeCheck.confused.isNotEmpty()) {
-          if (allowConfused) state.addEqn(createEqn(lhs, solved, lr, rl));
-          else {
-            reporter.report(new HoleProblem.BadlyScopedError(lhs, solved, scopeCheck.confused, pos));
-            yield new ErrorTerm(solved);
-          }
-        }
-        if (!meta.solve(state, solved)) {
-          reporter.report(new HoleProblem.RecursionError(lhs, solved, pos));
-          yield new ErrorTerm(solved);
-        }
-        tracing(builder -> builder.append(new Trace.LabelT(pos, "Hole solved!")));
-        yield resultTy;
-      }
+      case CallTerm.Hole lhs -> solveMeta(preRhs, lr, rl, lhs);
     };
     traceExit();
     return ret;
   }
 
+  private @Nullable Term solveMeta(@NotNull Term preRhs, Sub lr, Sub rl, CallTerm.Hole lhs) {
+    var meta = lhs.ref();
+    if (preRhs instanceof CallTerm.Hole rcall && lhs.ref() == rcall.ref()) {
+      // If we do not know the type, then we do not perform the comparison
+      if (meta.result == null) return null;
+      // Is this going to produce a readable error message?
+      compareLevel(lhs.ulift(), rcall.ulift());
+      var holeTy = FormTerm.Pi.make(meta.telescope, meta.result);
+      for (var arg : lhs.args().view().zip(rcall.args())) {
+        if (!(holeTy instanceof FormTerm.Pi holePi))
+          throw new IllegalStateException("meta arg size larger than param size. this should not happen");
+        if (!compare(arg._1.term(), arg._2.term(), lr, rl, holePi.param().type())) return null;
+        holeTy = holePi.substBody(arg._1.term());
+      }
+      return holeTy.subst(Substituter.TermSubst.EMPTY, lhs.ulift());
+    }
+    // Long time ago I wrote this to generate more unification equations,
+    // which solves more universe levels. However, with latest version Aya (0.13),
+    // removing this does not break anything.
+    // Update: this is still needed, see #327 last task (`coe'`)
+    var resultTy = preRhs.computeType(state, ctx);
+    if (meta.result != null) {
+      var liftedType = meta.result.subst(Substituter.TermSubst.EMPTY, lhs.ulift());
+      compareUntyped(resultTy, liftedType, rl, lr);
+    }
+    var argSubst = extract(lhs, preRhs, meta);
+    if (argSubst == null) {
+      reporter.report(new HoleProblem.BadSpineError(lhs, pos));
+      return null;
+    }
+    var subst = Unfolder.buildSubst(meta.contextTele, lhs.contextArgs());
+    // In this case, the solution may not be unique (see #608),
+    // so we may delay its resolution to the end of the tycking when we disallow vague unification.
+    if (!allowVague && subst.overlap(argSubst).anyMatch(var -> preRhs.findUsages(var) > 0)) {
+      state.addEqn(createEqn(lhs, preRhs, lr, rl));
+      // Skip the unification and scope check
+      return resultTy;
+    }
+    subst.add(argSubst);
+    // TODO
+    // TODO: what's the TODO above? I don't know what's TODO? ????
+    rl.map.forEach(subst::add);
+    assert !state.metas().containsKey(meta);
+    // TODO: report error if unlifting makes < 0 levels
+    var solved = preRhs.freezeHoles(state).subst(subst, -lhs.ulift());
+    var allowedVars = meta.fullTelescope().map(Term.Param::ref).toImmutableSeq();
+    var scopeCheck = solved.scopeCheck(allowedVars);
+    if (scopeCheck.invalid.isNotEmpty()) {
+      // Normalization may remove the usages of certain variables
+      solved = solved.normalize(state, NormalizeMode.NF);
+      scopeCheck = solved.scopeCheck(allowedVars);
+    }
+    if (scopeCheck.invalid.isNotEmpty()) {
+      reporter.report(new HoleProblem.BadlyScopedError(lhs, solved, scopeCheck.invalid, pos));
+      return new ErrorTerm(solved);
+    }
+    if (scopeCheck.confused.isNotEmpty()) {
+      if (allowConfused) state.addEqn(createEqn(lhs, solved, lr, rl));
+      else {
+        reporter.report(new HoleProblem.BadlyScopedError(lhs, solved, scopeCheck.confused, pos));
+        return new ErrorTerm(solved);
+      }
+    }
+    if (!meta.solve(state, solved)) {
+      reporter.report(new HoleProblem.RecursionError(lhs, solved, pos));
+      return new ErrorTerm(solved);
+    }
+    tracing(builder -> builder.append(new Trace.LabelT(pos, "Hole solved!")));
+    return resultTy;
+  }
+
   private boolean compareLevel(int l, int r) {
     switch (cmp) {
       case Eq: