依赖类型 elaboration

表面语言允许人省略显然信息，核心语言要求机器把每个依赖关系写清。Elaborator 就像排版前的技术编辑：根据上下文补上宇宙层、隐式类型参数和强制运输，把模式子句重排成核心消去；最后由独立内核检查成稿，而不是要求用户信任编辑过程没有猜错。

依赖类型让这种补全具有反馈回路。选择一个隐式实参会改变后续参数的类型，后续显式实参又可能反过来确定先前的 metavariable。双向方向标记限制信息流，约束队列保存尚未确定的部分；二者共同把全局猜测缩小成可管理的局部求解，却不能消灭固有歧义。

设核心恒等函数为

表面项 id true 没写隐式 $A$。elaborator 先输出候选 $\mathsf{id}\{?A\}\mathsf{true}$，再由 $\mathsf{true}:\mathsf{Bool}$ 产生约束 $?A\equiv \mathsf{Bool}$，求解后得到核心项

若期望类型已经是 $\mathsf{Bool}$，checking 方向可更早传播该信息。对

调用 append xs ys 会从两个向量的类型恢复 $m,n$，再把结果类型实例化；这不是运行时读取长度，而是解 typing constraints。

边界例子是 λx. x 处在 synthesis 位置且没有注解：$x$ 的类型无来源，系统可拒绝或要求 annotation，不能凭“显然是恒等函数”选择某一个宇宙与类型。另一个边界是方程 $?Fx\equiv t$ 的高阶求解；若允许任意 metavariable 函数，可能有多个不可比较解或进入不可判定搜索。实现常采用 pattern unification、occurs check、冻结约束与用户交互，这些是有意限定的完备范围，不应包装成一般依赖类型推断。

Elaboration 把丰富语法与小可信内核分离。notation、type class、coercion、record projection 和 tactic 可以在不扩张核心证明规则的情况下加入，只要最终生成的项通过检查。这种架构还改善错误定位：约束记录了哪一个隐式选择导致类型冲突，编辑器可展示尚未解决洞的局部语境与目标。

分离也明确了信任边界。Elaborator 有 bug 时可能拒绝合法程序或生成错误项，但健全内核会拦下后者；若编译器绕过重检、让未解 metavariable 成为任意常量，可靠性便失效。性能优化如缓存规范形、增量约束求解和启发式实例搜索都必须保持最终 core judgment 不变。