diff --git a/base/src/main/java/org/aya/normalize/Normalizer.java b/base/src/main/java/org/aya/normalize/Normalizer.java
index 0f397257d5..2f5e5e872c 100644
--- a/base/src/main/java/org/aya/normalize/Normalizer.java
+++ b/base/src/main/java/org/aya/normalize/Normalizer.java
@@ -45,13 +45,14 @@ public final class Normalizer implements UnaryOperator<Term> {
     // ConCall for point constructors are always in WHNF
     if (term instanceof ConCall con && !con.ref().hasEq()) return con;
     var postTerm = term.descent(this);
+    // descent may change the java type of term, i.e. beta reduce
     var defaultValue = usePostTerm ? postTerm : term;
 
     return switch (postTerm) {
       case StableWHNF _, FreeTerm _ -> postTerm;
       case BetaRedex app -> {
         var result = app.make();
-        yield result == app ? result : apply(result);
+        yield result == app ? defaultValue : apply(result);
       }
       case FnCall(var fn, int ulift, var args) -> switch (fn) {
         case JitFn instance -> {
@@ -78,11 +79,12 @@ case FnCall(var fn, int ulift, var args) -> switch (fn) {
         var result = reduceRule.rule().apply(reduceRule.args());
         if (result != null) yield apply(result);
         // We can't handle it, try to delegate to FnCall
-        yield reduceRule instanceof RuleReducer.Fn fnRule
-          ? apply(fnRule.toFnCall())
-          : reduceRule;
+        yield switch (reduceRule) {
+          case RuleReducer.Fn fn -> apply(fn.toFnCall());
+          case RuleReducer.Con _ -> postTerm;
+        };
       }
-      case ConCall(var head, _) when !head.ref().hasEq() -> defaultValue;
+      case ConCall(var head, _) when !head.ref().hasEq() -> postTerm;
       case ConCall call when call.conArgs().getLast() instanceof DimTerm dim ->
         call.head().ref().equality(call.args(), dim == DimTerm.I0);
       case PrimCall prim -> state.primFactory.unfold(prim, state);
diff --git a/base/src/main/java/org/aya/resolve/ResolveInfo.java b/base/src/main/java/org/aya/resolve/ResolveInfo.java
index 8c4a1d8bc8..014548a7d1 100644
--- a/base/src/main/java/org/aya/resolve/ResolveInfo.java
+++ b/base/src/main/java/org/aya/resolve/ResolveInfo.java
@@ -36,7 +36,7 @@
  * @param opRename     open/import renames with operators
  * @param depGraph     local to this module
  * @param imports      importing information, it only contains the modules that is explicitly imported, 
- *                     should not be confused with the {@code import} in {@link ModuleContext#importModule}
+ *                     should not be confused with the {@code import} in {@link ModuleContext#importModuleContext}
  * @param reExports    re-exporting module, it is {@link ModuleName.Qualified} rather than {@link String}
  *                     cause we can re-export a module inside another module without import it.
  */
diff --git a/base/src/main/java/org/aya/resolve/context/Candidate.java b/base/src/main/java/org/aya/resolve/context/Candidate.java
index b4215e55d2..a1d6113523 100644
--- a/base/src/main/java/org/aya/resolve/context/Candidate.java
+++ b/base/src/main/java/org/aya/resolve/context/Candidate.java
@@ -6,12 +6,19 @@
 import kala.collection.immutable.ImmutableSeq;
 import kala.collection.mutable.MutableMap;
 import org.aya.syntax.concrete.stmt.ModuleName;
+import org.aya.util.error.Panic;
 import org.jetbrains.annotations.NotNull;
 
 /**
  * Candidate represents a list of candidate of symbol resolving
  */
 public sealed interface Candidate<T> {
+  /**
+   * Merge two candidate.
+   *
+   * @implSpec If conflict happens, {@param candy} will overwrite {@code this},
+   * the user should check all possible conflicts before merge.
+   */
   @NotNull Candidate<T> merge(@NotNull Candidate<T> candy);
   boolean isAmbiguous();
   boolean isEmpty();
@@ -52,7 +59,6 @@ record Defined<T>(T symbol) implements Candidate<T> {
    *
    * @param symbols key: the module that the symbol comes from<br/>
    *                value: the symbol
-   * @param <T>
    */
   record Imported<T>(@NotNull ImmutableMap<ModuleName.Qualified, T> symbols) implements Candidate<T> {
     public static <T> @NotNull Candidate<T> empty() {
@@ -70,6 +76,8 @@ record Imported<T>(@NotNull ImmutableMap<ModuleName.Qualified, T> symbols) imple
     @Override public boolean isEmpty() { return symbols.isEmpty(); }
 
     @Override public T get() {
+      var view = symbols.valuesView().distinct();
+      if (view.sizeGreaterThan(1)) Panic.unreachable();
       //noinspection OptionalGetWithoutIsPresent
       return symbols.valuesView().stream().findFirst().get();
     }
@@ -82,6 +90,7 @@ record Imported<T>(@NotNull ImmutableMap<ModuleName.Qualified, T> symbols) imple
     @Override public boolean contains(@NotNull ModuleName modName) {
       return modName instanceof ModuleName.Qualified qmod && symbols.containsKey(qmod);
     }
+
     @Override public @NotNull Candidate<T> merge(@NotNull Candidate<T> candy) {
       return switch (candy) {
         case Candidate.Defined<T> v -> v;
diff --git a/base/src/main/java/org/aya/resolve/context/ModuleContext.java b/base/src/main/java/org/aya/resolve/context/ModuleContext.java
index b7a02953ae..ce1699b1ce 100644
--- a/base/src/main/java/org/aya/resolve/context/ModuleContext.java
+++ b/base/src/main/java/org/aya/resolve/context/ModuleContext.java
@@ -88,9 +88,12 @@ public sealed interface ModuleContext extends Context permits NoExportContext, P
   }
 
   /**
+   * Import modules from {@param module}, this method also import modules
+   * that inside {@param module}.
+   *
    * @see ModuleContext#importModule(ModuleName.Qualified, ModuleExport, Stmt.Accessibility, SourcePos)
    */
-  default void importModule(
+  default void importModuleContext(
     @NotNull ModuleName.Qualified modName,
     @NotNull ModuleContext module,
     @NotNull Stmt.Accessibility accessibility,
@@ -198,6 +201,8 @@ default void importSymbol(
         fail(new NameProblem.ShadowingWarn(name, sourcePos));
       }
     } else if (candidates.from().contains(fromModule)) {
+      // this case happens when the user is trying to open a module in twice (even the symbol are equal)
+      // or define two symbols with same name ([fromModule == ModuleName.This])
       reportAndThrow(new NameProblem.DuplicateNameError(name, ref, sourcePos));
     } else if (candidates.isAmbiguous() || candidates.get() != ref) {
       fail(new NameProblem.AmbiguousNameWarn(name, sourcePos));
@@ -209,13 +214,13 @@ default void importSymbol(
     if (ref instanceof AnyDefVar defVar && acc == Stmt.Accessibility.Public) {
       var success = exportSymbol(name, defVar);
       if (!success) {
-        reportAndThrow(new NameProblem.DuplicateExportError(name, sourcePos));    // TODO: use a more appropriate error
+        reportAndThrow(new NameProblem.DuplicateExportError(name, sourcePos));
       }
     }
   }
 
   /**
-   * Exporting an {@link AnyVar} with qualified id {@code {modName}::{name}}
+   * Exporting an {@link AnyDefVar}.
    *
    * @return true if exported successfully, otherwise (when there already exist a symbol with the same name) false.
    */
diff --git a/base/src/main/java/org/aya/resolve/context/ModuleExport.java b/base/src/main/java/org/aya/resolve/context/ModuleExport.java
index c4b766c80c..62b9ba2a17 100644
--- a/base/src/main/java/org/aya/resolve/context/ModuleExport.java
+++ b/base/src/main/java/org/aya/resolve/context/ModuleExport.java
@@ -110,7 +110,7 @@ public ModuleExport(@NotNull ModuleExport that) {
           }
         }
 
-        thing.forEach(x -> newExport.export(to, x), x -> newExport.export(new ModuleName.Qualified(to), x));
+        thing.forEach(x -> newExport.export(to, x), x -> newExport.export(ModuleName.of(to), x));
       } else {
         badNames.append(pair.data().name());
       }
diff --git a/base/src/main/java/org/aya/resolve/visitor/StmtPreResolver.java b/base/src/main/java/org/aya/resolve/visitor/StmtPreResolver.java
index e6efd25d7e..16453d5c6a 100644
--- a/base/src/main/java/org/aya/resolve/visitor/StmtPreResolver.java
+++ b/base/src/main/java/org/aya/resolve/visitor/StmtPreResolver.java
@@ -51,7 +51,7 @@ public ImmutableSeq<ResolvingStmt> resolveStmt(@NotNull ImmutableSeq<Stmt> stmts
         }
         var newCtx = context.derive(mod.name());
         var children = resolveStmt(mod.contents(), newCtx);
-        context.importModule(ModuleName.This.resolve(mod.name()), newCtx, mod.accessibility(), mod.sourcePos());
+        context.importModuleContext(ModuleName.This.resolve(mod.name()), newCtx, mod.accessibility(), mod.sourcePos());
         yield new ResolvingStmt.ModStmt(children);
       }
       case Command.Import cmd -> {
@@ -62,7 +62,7 @@ public ImmutableSeq<ResolvingStmt> resolveStmt(@NotNull ImmutableSeq<Stmt> stmts
         var mod = success.thisModule();
         var as = cmd.asName();
         var importedName = as != null ? ModuleName.This.resolve(as) : modulePath.asName();
-        context.importModule(importedName, mod, cmd.accessibility(), cmd.sourcePos());
+        context.importModuleContext(importedName, mod, cmd.accessibility(), cmd.sourcePos());
         var importInfo = new ResolveInfo.ImportInfo(success, cmd.accessibility() == Stmt.Accessibility.Public);
         resolveInfo.imports().put(importedName, importInfo);
         yield null;
diff --git a/base/src/main/java/org/aya/tyck/tycker/Stateful.java b/base/src/main/java/org/aya/tyck/tycker/Stateful.java
index e07052238e..dc887fe12d 100644
--- a/base/src/main/java/org/aya/tyck/tycker/Stateful.java
+++ b/base/src/main/java/org/aya/tyck/tycker/Stateful.java
@@ -13,7 +13,7 @@
 
 /**
  * Indicating something is {@link TyckState}ful,
- * therefore we can perform weak-head normalizing and <b>Ice Spell 「 Perfect Freeze 」</b>
+ * therefore we can perform weak-head normalizing and <b>Freeze Spell 「 Perfect Freeze 」</b>
  *
  * @see #state()
  * @see #whnf(Term)
diff --git a/cli-console/src/main/java/org/aya/cli/repl/jline/AyaCompleters.java b/cli-console/src/main/java/org/aya/cli/repl/jline/AyaCompleters.java
index ef1ee903e1..e366dde06f 100644
--- a/cli-console/src/main/java/org/aya/cli/repl/jline/AyaCompleters.java
+++ b/cli-console/src/main/java/org/aya/cli/repl/jline/AyaCompleters.java
@@ -80,6 +80,7 @@ record FixWord(@NotNull ImmutableSeq<String> moduleName, boolean fixed) { }
       var word = line.word();
       var fixed = fixWord(word, line.wordIndex(), (ImmutableSeq<FlexLexer.Token>) line.rawTokens(), line.line());
       var context = repl.replCompiler.getContext();
+      // Keep these for debugging, they are hard to type.
       // System.out.println(word + " ∈ " + line.words() + ", [idx, cursor, wordCursor]: "
       //   + line.wordIndex() + ", " + line.cursor() + ", " + line.wordCursor());
       context.giveMeHint(fixed.moduleName).forEach(candidate -> {
diff --git a/cli-impl/src/main/java/org/aya/cli/interactive/ReplCompiler.java b/cli-impl/src/main/java/org/aya/cli/interactive/ReplCompiler.java
index 95f8c65752..839c828d4f 100644
--- a/cli-impl/src/main/java/org/aya/cli/interactive/ReplCompiler.java
+++ b/cli-impl/src/main/java/org/aya/cli/interactive/ReplCompiler.java
@@ -114,7 +114,7 @@ private void importModule(@NotNull LibraryOwner owner) {
     owner.librarySources()
       .map(src -> src.resolveInfo().get().thisModule())
       .filterIsInstance(PhysicalModuleContext.class)
-      .forEach(mod -> context.importModule(mod.modulePath().asName(), mod, Stmt.Accessibility.Public, SourcePos.NONE));
+      .forEach(mod -> context.importModuleContext(mod.modulePath().asName(), mod, Stmt.Accessibility.Public, SourcePos.NONE));
     owner.libraryDeps().forEach(this::importModule);
   }
 
diff --git a/cli-impl/src/main/java/org/aya/cli/interactive/ReplContext.java b/cli-impl/src/main/java/org/aya/cli/interactive/ReplContext.java
index d36936b8bf..a8f9cdb95d 100644
--- a/cli-impl/src/main/java/org/aya/cli/interactive/ReplContext.java
+++ b/cli-impl/src/main/java/org/aya/cli/interactive/ReplContext.java
@@ -170,13 +170,19 @@ public record ModuleTrie(@NotNull ImmutableMap<String, ModuleTrie> children, boo
    */
   private @NotNull ImmutableMap<String, ModuleTrie>
   buildModuleTree(@NotNull Seq<SeqView<String>> moduleNames) {
+    if (moduleNames.isEmpty()) {
+      return ImmutableMap.empty();
+    }
+
     var indexed = MutableMap.<String, MutableList<SeqView<String>>>create();
     var inhabited = MutableSet.<String>create();
 
+    // merge module names those have the same 1-length prefix
+    // also mark 1-length name as inhabited
     for (var name : moduleNames) {
       var head = name.getFirst();
       var tail = name.drop(1);
-      // we always create a record even [tail] is empty
+      // we always create a record even [tail] is empty, it is used to trigger the creation of ModuleTrie.
       var root = indexed.getOrPut(head, MutableList::create);
       if (tail.isNotEmpty()) {
         root.append(tail);
diff --git a/ide-lsp/src/test/resources/lsp-test-lib/README.md b/ide-lsp/src/test/resources/lsp-test-lib/README.md
new file mode 100644
index 0000000000..b444c40d9f
--- /dev/null
+++ b/ide-lsp/src/test/resources/lsp-test-lib/README.md
@@ -0,0 +1,7 @@
+# lsp-test-lib
+
+This is the test resource for ids-lsp,
+some tests may highly depend on the content of certain file,
+you may need to fix those test after modifying test resource.
+In order to minimize the troubles, please append (rather than insert)
+code to the end of file.
diff --git a/jit-compiler/src/main/java/org/aya/compiler/CompiledModule.java b/jit-compiler/src/main/java/org/aya/compiler/CompiledModule.java
index cdcb487d5e..1456e31118 100644
--- a/jit-compiler/src/main/java/org/aya/compiler/CompiledModule.java
+++ b/jit-compiler/src/main/java/org/aya/compiler/CompiledModule.java
@@ -188,7 +188,7 @@ private void loadModule(
           for (var constructor : data.constructors()) {
             innerCtx.defineSymbol(new CompiledVar(constructor), Stmt.Accessibility.Public, SourcePos.SER);
           }
-          context.importModule(
+          context.importModuleContext(
             ModuleName.This.resolve(data.name()),
             innerCtx, Stmt.Accessibility.Public, SourcePos.SER);
           if (metadata.shape() != -1) {
@@ -223,7 +223,7 @@ private void shallowResolve(@NotNull ModuleLoader loader, @NotNull ResolveInfo t
         thisResolve.thisModule().reportAndThrow(new NameProblem.ModNotFoundError(modName, SourcePos.SER));
       thisResolve.imports().put(modRename, new ResolveInfo.ImportInfo(success, isPublic));
       var mod = success.thisModule();
-      thisResolve.thisModule().importModule(modRename, mod, isPublic ? Stmt.Accessibility.Public : Stmt.Accessibility.Private, SourcePos.SER);
+      thisResolve.thisModule().importModuleContext(modRename, mod, isPublic ? Stmt.Accessibility.Public : Stmt.Accessibility.Private, SourcePos.SER);
       reExports.getOption(modName).forEach(useHide -> thisResolve.thisModule().openModule(modRename,
         Stmt.Accessibility.Public,
         useHide.names().map(x -> new QualifiedID(SourcePos.SER, x)),
diff --git a/note/module.md b/note/module.md
index ed007b497d..21ef42998f 100644
--- a/note/module.md
+++ b/note/module.md
@@ -1,31 +1,63 @@
 # Aya 的 Module 设计
 
-## Module 的名称
+## ModulePath
 
-Module 的名称是一个满足 `weakId(::weakId)*` 的字符串，双冒号并不意味着嵌套关系。
+ModulePath 是一个模块的绝对路径，它通常是以某个库为根到特定模块的物理路径。使用双冒号分隔每个路径的组成部分。
 
-## Module 的嵌套
+```aya
+// 导入 arith/nat.aya 模块
+import arith::nat
+```
 
-Module 名称中的双冒号（在编译器内部）并不总是意味着嵌套关系。
-实际上，如果我们声明了一个名字为 `A` 的 module，并且在 `A` 中声明了一个名字为 `B` 的 module。
-当我们导入 `A` 时（实际上已经自动导入了），我们其实导入了：
+## ModuleName
 
-* 名字为 `A` 的 module
-* 名字为 `A::B` 的 module
+尽管 ModuleName 和 ModulePath 有完全相同的表达式（用双冒号分隔），但 ModuleName 指的是在特定模块中，对某个模块的赋予的名字。
+要注意的是，在这种情况下，双冒号不总是表达包含关系（尽管在正常的使用过程中，用户绝不可能构造出没有包含关系的 ModuleName）。
 
-理论上（至少在 module 的设计上），我们完全可以直接定义一个名字为 `A::B` 而不需要去在 `A` module 中定义 `B`
-module（不过就无法在 `B` 中享受 `A` 的作用域了，但这并不是重点）
+```aya
+// 以默认名称 arith::nat 导入 arith/nat.aya 模块
+import arith::nat
+// 导入 arith::nat 模块中的所有符号和模块。
+open arith::nat
+```
 
-## Module 的导入
+## 上下文
 
-当我们导入一个 module 时，我们同时也会导入这个 module 所导出的所有 module。
-正如上一节所示，我们导入 `A` module 时，同时也以名字 `A::B` 导入了它（自动）导出的 `B` module。
-如果一个名字为 `A::B` 的 module 导出了名字为 `C::D` 的 module：当我们导入 `A::B` 时，同时也会以名字 `A::B::C::D`
-导入 `C::D`；
-而到底是 `A::B::C` 中的 `D` 模块还是 `A` 中的 `B::C::D` 模块或是其他的，我们完全不关心。
+由于 aya 的 tyck 具有顺序，因此我们不能在没有导入某个模块的情况下使用其内部的符号或模块。
 
-## Module 的歧义
+## 歧义
 
-当我们（直接或间接）导入的 module 所使用的名称与现有的 module 冲突，便发生了歧义。
-如果这两个 Module 是同一个 Module，那么歧义便失去了它的意义，因此 Aya 不会为此困扰。
-反之，Aya 会报告一个错误。
+在使用 `open` 时，通常会遇到歧义：`open` 的多个模块中有相同名字的符号，或者是当前模块中定义的符号与 `open` 导入的符号有相同的名字。
+为了更简单地解决这个问题，我们要求模块不能导出歧义的符号（但只要不导出，模块中是可以有相同名字的符号的）。
+
+```aya
+// 假设 foo 和 bar 都定义了符号 baz
+public open import arith::nat::foo
+// public open import arith::nat::bar      // 报错：名字 baz 不能再被导出
+open import arith::nat::bar                // 没有问题
+
+// def = baz                               // 报错：我们不清楚要用哪个 baz
+def = arith::nat::foo::baz                 // 没有问题
+```
+
+为了通过提供模块名来解决符号的歧义问题，我们需要模块名不能歧义
+（也许我们可以通过其他方式来解决模块名的歧义，但那样得不偿失，我们通常不会有歧义的模块名，即使有，也可以通过重命名解决）
+
+> 如果涉及歧义的所有符号名都指向同一个符号，就不会有报错
+
+## 导入与开放
+
+在导入/开放时，我们可以提供一些参数来影响它们的行为。
+
+```aya
+// 以名称 nat 导入 arith/nat.aya 模块 
+import arith::nat as nat
+
+// 将 nat 中除了 + 外的所有符号和模块导入当前模块
+open nat hiding (+)
+
+// 将 nat 中的 + 符号以名字 plus 导入当前模块
+open nat using (+ as plus)
+```
+
+一般来说，用户是可以重复 `open` 同一个模块的。
diff --git a/producer/src/main/java/org/aya/producer/AyaProducer.java b/producer/src/main/java/org/aya/producer/AyaProducer.java
index 8d55da58f6..bf26e793dc 100644
--- a/producer/src/main/java/org/aya/producer/AyaProducer.java
+++ b/producer/src/main/java/org/aya/producer/AyaProducer.java
@@ -322,7 +322,7 @@ private void giveMeOpen(@NotNull ModifierParser.Modifiers modiSet, @NotNull Decl
     additional.append(new Command.Open(
       keyword,
       modiSet.accessibility().data(),
-      new ModuleName.Qualified(decl.ref().name()),
+      ModuleName.of(decl.ref().name()),
       UseHide.EMPTY,
       modiSet.isExample(),
       true
diff --git a/syntax/src/main/java/org/aya/syntax/concrete/stmt/ModuleName.java b/syntax/src/main/java/org/aya/syntax/concrete/stmt/ModuleName.java
index bb64c04a58..b1fe589f49 100644
--- a/syntax/src/main/java/org/aya/syntax/concrete/stmt/ModuleName.java
+++ b/syntax/src/main/java/org/aya/syntax/concrete/stmt/ModuleName.java
@@ -3,6 +3,8 @@
 package org.aya.syntax.concrete.stmt;
 
 import kala.collection.SeqLike;
+import kala.collection.SeqView;
+import kala.collection.immutable.ImmutableArray;
 import kala.collection.immutable.ImmutableSeq;
 import org.aya.util.error.Panic;
 import org.jetbrains.annotations.NotNull;
@@ -28,7 +30,6 @@ enum ThisRef implements ModuleName {
   }
 
   record Qualified(@NotNull ImmutableSeq<String> ids) implements ModuleName {
-    public Qualified(@NotNull String @NotNull ... ids) { this(ImmutableSeq.of(ids)); }
     public Qualified {
       assert ids.isNotEmpty() : "Otherwise please use `This`";
     }
@@ -57,6 +58,14 @@ record Qualified(@NotNull ImmutableSeq<String> ids) implements ModuleName {
     return new Qualified(ids.toImmutableSeq());
   }
 
+  static @NotNull ModuleName.ThisRef of() {
+    return ModuleName.This;
+  }
+
+  static @NotNull ModuleName.Qualified of(@NotNull String first, @NotNull String @NotNull ... tail) {
+    return new Qualified(ImmutableSeq.from(SeqView.of(first).concat(ImmutableArray.Unsafe.wrap(tail))));
+  }
+
   /**
    * Construct a qualified module path from a not empty id sequence.
    *
diff --git a/syntax/src/main/java/org/aya/syntax/concrete/stmt/StmtVisitor.java b/syntax/src/main/java/org/aya/syntax/concrete/stmt/StmtVisitor.java
index 0f84d13897..52635eb531 100644
--- a/syntax/src/main/java/org/aya/syntax/concrete/stmt/StmtVisitor.java
+++ b/syntax/src/main/java/org/aya/syntax/concrete/stmt/StmtVisitor.java
@@ -64,12 +64,12 @@ default void visit(@NotNull BindBlock bb) {
   private void visitVars(@NotNull Stmt stmt) {
     switch (stmt) {
       case Generalize g -> g.variables.forEach(v -> visitVarDecl(v.sourcePos, v, noType));
-      case Command.Module m -> visitModuleDecl(m.sourcePos(), new ModuleName.Qualified(m.name()));
+      case Command.Module m -> visitModuleDecl(m.sourcePos(), ModuleName.of(m.name()));
       case Command.Import i -> {
         var isAlsoDef = i.asName() == null;
         visitModuleRef(i.sourcePos(), i.path());
         if (!isAlsoDef) {
-          visitModuleDecl(i.sourcePos(), new ModuleName.Qualified(i.asName()));
+          visitModuleDecl(i.sourcePos(), ModuleName.of(i.asName()));
         } else {
           // TODO: visitModuleDecl on the last element of i.path
         }
diff --git a/syntax/src/main/java/org/aya/syntax/core/pat/BindEater.java b/syntax/src/main/java/org/aya/syntax/core/pat/BindEater.java
index 4662df0f4e..6e5911918a 100644
--- a/syntax/src/main/java/org/aya/syntax/core/pat/BindEater.java
+++ b/syntax/src/main/java/org/aya/syntax/core/pat/BindEater.java
@@ -30,7 +30,6 @@ public record BindEater(
       // which should not contain meta pattern
       case Pat.Meta _ -> throw new Panic("I don't like holes :(");
       case Pat.Bind bind -> {
-        // TODO: also eat reference to bind in bind.type()
         var realType = bind.type().instantiateTele(inst());
         var meta = new Pat.Meta(MutableValue.create(), bind.bind().name(), realType, bind.bind().definition());
         // yummy yummy
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 d5d9dcdc1c..9d70f762e3 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
@@ -38,6 +38,19 @@ private MemberCall update(Term clazz, ImmutableSeq<Term> newArgs) {
     return new MemberCall(of, ref, ulift, args).make();
   }
 
+  /**
+   * Trying to normalize this {@link MemberCall}:
+   * <ul>
+   *   <li>If it calls on a {@link NewTerm}, we just pick the corresponding term.</li>
+   *   <li>
+   *     If it calls on a {@link ClassCastTerm}, we will try to obtain the restriction information from it (see {@link ClassCastTerm#get(MemberDefLike)}).
+   *     If failed, we look inside. Note that nested {@link ClassCastTerm} is possible,
+   *     we also return {@code mostInnerTerm .someField} when we are unable to normalize it anymore, it looks like we normalized
+   *     the arguments of a function call but we still unable to unfold it.
+   *   </li>
+   *   <li>Otherwise, we just return the {@link MemberCall} itself</li>
+   * </ul>
+   */
   @Override public @NotNull Term make() {
     return switch (of()) {
       case NewTerm neu -> {
diff --git a/syntax/src/main/java/org/aya/syntax/ref/LocalCtx.java b/syntax/src/main/java/org/aya/syntax/ref/LocalCtx.java
index cca48a32e7..f61b1b1fa6 100644
--- a/syntax/src/main/java/org/aya/syntax/ref/LocalCtx.java
+++ b/syntax/src/main/java/org/aya/syntax/ref/LocalCtx.java
@@ -13,7 +13,7 @@
 
 import java.util.function.UnaryOperator;
 
-public interface LocalCtx extends Scoped<LocalVar, Term, LocalCtx> {
+public sealed interface LocalCtx extends Scoped<LocalVar, Term, LocalCtx> permits SeqLocalCtx, MapLocalCtx {
   boolean isEmpty();
   int size();
   @Contract(value = "_ -> new", pure = true)
diff --git a/tools/src/main/java/org/aya/util/Scoped.java b/tools/src/main/java/org/aya/util/Scoped.java
index d9476d84cd..32bb229489 100644
--- a/tools/src/main/java/org/aya/util/Scoped.java
+++ b/tools/src/main/java/org/aya/util/Scoped.java
@@ -12,10 +12,10 @@
 import java.util.function.BiFunction;
 
 /**
- * A container that has scope structure,
- * this is designed to growable, but not shrinkable or modify existing record.
+ * A map-like container that has a scope structure,
+ * this is designed to be growable, but not shrinkable or modify existing record.
  *
- * @param <This> the <b>final</b> type that implemented this interface
+ * @param <This> the <b>final</b>(at least, final for user) type that implemented this interface
  */
 public interface Scoped<K, V, This extends Scoped<K, V, This>> {
   @Contract(pure = true) @Nullable This parent();