6.3.1. 第一步：查缓存🔗

Lean 使用 tabled resolution（带记忆化的搜索）。之前搜索过的结果会被缓存，同一个实例可能在一次编译中被请求成千上万次，缓存避免了重复搜索。

6.3.2. 第二步：展开候选实例🔗

缓存未命中时，Lean 遍历所有 @[instance] 声明，逐一尝试 unification。

-- [伪代码] 搜索 Add (Fin n)
目标：Add (Fin n)
  ├─ 候选 instAddFin : Add (Fin n)     ← unify 成功！
  ├─ 候选 instAddNat : Add Nat         ← unify 失败（Fin n ≠ Nat）
  └─ ...

6.3.3. 第三步：递归搜索前提🔗

如果候选实例依赖其他 type class（有 [...] 参数），Lean 递归搜索这些前提。

-- [示意] 有前提的实例
instance [Add α] : Add (Option α) where
  add
- some a, some b => some (Add.add a b)：_, _ => none

搜索 Add (Option Nat) 时，Lean 发现需要先找 Add Nat，触发递归：

-- [伪代码] 递归搜索
目标：Add (Option Nat)
  └─ 候选 instAddOption : [Add α] → Add (Option α)
       ├─ unify：α := Nat
       └─ 递归目标：Add Nat  ← 成功！

6.3.4. 第四步：深度限制🔗

Lean 通过两个参数控制搜索规模：

• synthInstance.maxHeartbeats：最大计算步数（默认 20000）

• synthInstance.maxSize：搜索树最大节点数

超限后搜索终止报错，防止循环依赖导致无限搜索。

注意：Synthesis 不只搜索全局注册的 @[instance] 声明，也会考虑当前局部上下文中的实例——例如函数签名里的 [Add α] 参数、haveI 引入的实例、以及 withNewLocalInstance 临时注册的实例，都会参与搜索。

6.3.5. 优先级🔗

每个实例有一个优先级数值（@[instance N]），N 越大越优先，默认 1000。

当你对同一类型有通用实例和特化实例时，给特化实例更高优先级可以控制选择偏好。

提醒：重叠实例加优先级是为不可避免的冲突而设计的应急手段，不鼓励主动制造同头实例。优先设计不重叠的实例结构；只有在库兼容性等外部约束下无法避免时，再用优先级消歧。

6.4.1. synthInstance：失败即报错🔗

-- [示意]
synthInstance (type : Expr) : MetaM Expr

传入 type class 类型的 Expr，返回找到的实例项。搜索失败时抛异常。

-- [示意] 在 tactic 中搜索 Add Nat
elab "demo_synth" : tactic => do
  let addNatType ← mkAppM ``Add #[mkConst ``Nat]
  let inst ← synthInstance addNatType
  logInfo m!"找到实例：{inst}"

这里 mkAppM 会自动处理 universe 和隐式参数，比手动 mkApp + mkConst 更安全。

6.4.2. synthInstance?：失败返回 none🔗

-- [示意]
synthInstance? (type : Expr) : MetaM (Option Expr)

当你需要探测实例是否存在而非一定要找到它时，用这个版本。

-- [示意] 根据 Decidable 实例选择策略
elab "smart_decide" : tactic => withMainContext do
  let target ← getMainTarget
  let decType ← mkAppM ``Decidable #[target]
  match ← synthInstance? decType with
- some _ => logInfo "目标可判定，使用 decide"：none   => logInfo "目标不可判定，需要其他方法"

6.4.3. isInstance：检查声明是否是实例🔗

-- [示意]
isInstance (declName : Name) : CoreM Bool

遍历环境中的声明并筛选实例时会用到。

6.7.1. 调整搜索预算🔗

-- [示意] 临时增加搜索预算
withOptions (fun o => o.set `synthInstance.maxHeartbeats 80000) do
  let inst ← synthInstance goalType

注意：盲目增大预算不是正解。超时通常说明实例注册有问题（见 5.7 节）。

6.7.2. 临时添加局部实例🔗

-- [示意]
-- withNewLocalInstance (className : Name) (fvar : Expr) (body : MetaM α)
-- 在 body 执行期间，把 fvar 注册为 className 的临时实例

典型用途：把 hypothesis 中的 type class 约束临时注册为实例，让后续 synthesis 能找到它。

6.7.3. 用户侧控制🔗

6.8.1. 失败一：找不到实例（No Instance Found）🔗

症状：failed to synthesize instance Add MyType。

常见原因：忘记定义实例、没有 import 实例所在模块、类型参数含有未解决的 metavariable。

诊断：用 #check (inferInstance : TargetClass TargetType) 手动测试。成功则问题在 Expr 构造，失败则问题在实例注册。

6.8.2. 失败二：实例歧义 / Diamond Problem🔗

症状：找到多个实例无法决定，或多重继承路径不一致。

-- [示意] Diamond problem
class A (α : Type)
class B (α : Type) extends A α
class C (α : Type) extends A α
class D (α : Type) extends B α, C α
-- D → B → A 和 D → C → A 必须 definitionally equal

诊断：set_option trace.Meta.synthInstance true 查看完整搜索过程。

6.8.3. 失败三：循环依赖导致超时🔗

症状：maxHeartbeats 超限。

-- [示意] 循环实例——不要这样写！
instance [B α] : A α where ...
instance [A α] : B α where ...
-- A α → B α → A α → ... 无限循环

Tabled resolution 能处理某些循环（缓存命中时），但如果每步涉及新类型参数，缓存帮不上忙。

修复：打破循环——去掉一个方向的实例，或改成非 instance 的普通定义。

6.8.4. 补充陷阱：Universe 与 Out-parameter🔗

用 mkConst 时需提供 universe level 参数，遗漏会导致错误。推荐用 mkAppM 自动处理：

-- [示意] mkAppM 自动推导 universe
let type ← mkAppM ``Add #[mkConst ``Nat]

对有 out-parameter 的 type class（如 HAdd），synthesis 完成后要读取 metavariable 赋值来获取推断出的输出类型。

6.9.1. 练习 1（热身）：探测 BEq 实例🔗

编写 elab 命令 has_beq，接受一个类型名，报告该类型是否有 BEq 实例。

-- [示意] 实现后的预期调用形式
-- #has_beq Nat         →  "Nat 有 BEq 实例"
-- #has_beq (Nat → Nat) →  "Nat → Nat 没有 BEq 实例"

提示：synthInstance? + mkAppM 构造 BEq 类型。

6.9.2. 练习 2（热身）：观察搜索过程🔗

用 trace 选项观察实例搜索，回答：搜索 Add (List Nat) 触发了几次递归？

-- [可运行]
set_option trace.Meta.synthInstance true in
#check (inferInstance : Add (List Nat))

6.9.3. 练习 3（Debug）：诊断超时🔗

下面的代码会导致 synthesis 超时，解释原因并修复。

-- [示意] 超时代码
class Serialize (α : Type) where
  serialize : α → String

class Deserialize (α : Type) where
  deserialize : String → Option α

instance [Deserialize α] : Serialize α where
  serialize _ := "serialized"

instance [Serialize α] : Deserialize α where
  deserialize _ := none

-- 超时：example : Serialize Nat := inferInstance

提示：画依赖箭头找环。修复方案：可以为 Nat 提供直接的 base instance 打破循环，也可以去掉形成环的某条 instance 边（改为普通 def），根据实际需求选择。

6.9.4. 练习 4（综合）：自动交换律改写🔗

编写 tactic comm_rw：

1. 检查目标是否是等式 a op b = c op d

2. 用 synthInstance? 检查 op 是否满足 Commutative

3. 满足则用交换律改写左侧为 b op a；不满足则报错

-- [示意] 预期行为
-- example (a b : Nat) : a + b = b + a := by comm_rw; rfl

提示：结合第三章 Expr 操作、第四章目标管理、本章 synthInstance?。