实例合成是一种递归搜索过程：它要么为给定的类型类找到实例，要么失败。 换言之，给定一个注册为类型类的类型，实例合成会尝试构造一个具有该类型的项。 它遵循可约性：半可约或不可约定义不会被展开，因此，除非某个定义是可约的，否则该定义的实例不会自动被视为其展开结果的实例。 一个给定的类可能有多个可用实例；此时依次以声明的优先级和声明顺序打破平局，同一优先级下，较新的实例优先于较早的实例。
该搜索过程在存在菱形时仍然高效，遇到循环时也不会无限循环。 当到达同一目标的路径不止一条时，就会出现菱形；而循环则是两个实例各自在另一个实例得到解决后便可解决的情形。 实践中，用类型类编码数学概念时经常会出现菱形，而 Lean 的强制类型转换功能 会自然地产生循环，例如有限集合与有限多重集合之间的循环。
可以使用 Lean.Parser.Command.synth : command#synth 命令测试实例合成。
此外，可以在需要实例本身的位置使用 inferInstance 和 inferInstanceAs 合成实例。
带类型标注的 inferInstance 与 inferInstanceAs 并不等价；inferInstanceAs 会预处理合成出的实例，以防实现细节无意间泄漏到接口中。
inferInstance 通过类型类推断（实例合成）合成任意目标类型的值。此函数与恒等函数具有相同的类型签名，
但参数 [i : α] 上的方括号表示 Lean 将尝试通过类型类推断构造该参数。
（如果 α 不是一个类型类，此过程将失败。）例如：
#check (inferInstance : Inhabited Nat) -- Inhabited Nat
@[instance_reducible]
def foo : Inhabited (Nat × Nat) :=
inferInstance
example : foo.default = (default, default) :=
rfl
inferInstanceAs α 合成一个类型为 α 的实例，然后调整它以符合预期类型 β；
β 必须能够从上下文中推断出来。
例如：
def D := Nat
instance : Inhabited D := inferInstanceAs (Inhabited Nat)
这种调整会确保所得实例在低于 semireducible 的透明度下归约时，不会“泄漏”右侧的
Nat；在这些透明度下，D 本来也不会被展开。这样可以防止“滥用定义相等”。
更具体地说，给定“源类型”（参数）和“目标类型”（预期类型），inferInstanceAs
先为源类型合成实例，再按需展开并重新包装实例的组成部分（字段、嵌套实例），使其与
目标类型兼容。各个步骤由下列选项控制；它们默认都启用，并且可以在移植代码时禁用：
backward.inferInstanceAs.wrap：实例调整的总开关，同时作用于 inferInstanceAs
和默认派生处理器（deriving）；
backward.inferInstanceAs.wrap.reuseSubInstances：对子实例字段复用目标类型已有的实例，
以避免菱形中的实例不是定义相等的；
backward.inferInstanceAs.wrap.instances：将不可约实例包装在辅助定义中；
backward.inferInstanceAs.wrap.data：将数据字段包装在辅助定义中（证明字段总会被包装）。
如果只需合成实例而不必在类型之间进行迁移，请改用 inferInstance；必要时可为预期类型
添加类型标注。
一般而言，实例合成是一种可能任意回溯的递归搜索过程。 合成可能以一个实例项成功；若找不到这样的项，则会失败；若信息不足，则会卡住。 Selsam, Ullrich, and de Moura (2020)Daniel Selsam, Sebastian Ullrich, and Leonardo de Moura, 2020. “Tabled typeclass resolution”. arXiv:2001.04301 中给出了实例合成算法的详细说明。 实例搜索问题由应用于具体参数的类型类给出；这些参数值可能已知，也可能未知。 实例搜索会按优先级和定义顺序，尝试每个类型为类的局部绑定变量以及每个已注册实例。 当候选实例本身带有实例隐式参数时，它们会引入更多合成任务。
只有当类型类的所有输入参数均已知时，才会尝试解决问题。 若某个问题尚不能尝试，该分支便会卡住；其他子问题取得进展后，这个问题可能变得可解。 实例搜索开始时，输出参数或半输出参数既可以已知，也可以未知。 检查实例是否匹配问题时会忽略输出参数，但会考虑半输出参数。
给定问题的每个候选解都会保存在表中；这既能防止循环导致无限递归，也能避免菱形（即存在多条路径可达成同一目标）造成指数级搜索开销。 出现以下任一情况时，搜索分支失败：
所有潜在实例均已尝试，搜索空间已耗尽。
达到选项 synthInstance.maxSize 指定的实例大小上限。
输出参数的合成值与搜索问题中指定的值不匹配。 失败的分支不会重试。
若搜索原本会失败或卡住，搜索过程会按优先级尝试使用匹配的默认实例。 对于默认实例，输入参数不必完全已知，可以用该实例的参数值进行实例化。 默认实例可以接受实例隐式参数，这会引发进一步的递归搜索。
若成功分支中的问题已完全确定（即不存在未解决的元变量），该分支便会被剪枝，并且不再尝试其他可能成功的实例，因为后续实例不可能使先前已成功的分支转为失败。
实例搜索发生在函数应用（参数个数可能为零）的精译过程中。 某些隐式参数的值会由其他参数强制确定；例如，可以利用稍后显式提供的值参数的类型来解决一个隐式类型参数。 隐式参数也可以利用程序中该处的预期类型信息来解决。 搜索实例隐式参数时，可以利用已找到的隐式参数值，也可能顺带解决其他隐式参数。
实例合成从实例隐式参数的类型开始。 该类型必须是类型类对零个或多个参数的应用；搜索开始时，这些参数值可能已知，也可能未知。 若类的某个参数未知，搜索过程不会将其实例化，除非对应形参被标记为输出参数，从而明确成为实例合成过程的输出。
搜索可能成功、失败或卡住；如果某个未知参数值变为已知后可能推动搜索进展，搜索就可能卡住。 当精译器确定了某个先前未知的隐式参数时，可能会重新调用卡住的搜索。 若未发生这种情况，卡住的搜索就会转为失败。
将 trace.Meta.synthInstance 选项设为 true，会让 Lean 输出合成类型类实例的过程跟踪。
该跟踪可用于理解实例合成如何成功以及为何失败。
这里可以看到 Lean 为得出类型 (Nat ⊕ Empty) 存在元素（具体而言是元素 Sum.inl 0）这一结论而采取的步骤：
点击 ▶ 符号会展开跟踪中的对应分支，点击 ▼ 则会折叠已展开的分支。
set_option pp.explicit true in
set_option trace.Meta.synthInstance true in
#synth Nonempty (Nat ⊕ Empty)
通过查看跟踪，可以观察 Lean 在类型类实例搜索中采用的深度优先回溯搜索。 要熟悉它可能需要一些练习！ 在上例中，Lean 依次执行以下步骤：
最初的第三、第四个候选项从未被考虑。
一旦对 Nonempty Nat 的搜索成功，Lean.Parser.Command.synth : command#synth 命令便会结束并输出解：
实例合成在搜索中同时使用局部实例和全局实例。
局部实例是局部上下文中可用的实例；它们可以是函数的参数，也可以用 let 在局部定义。
局部实例无需特别标示；任何类型为类型类的局部变量都是实例合成的候选项。
全局实例是全局环境中可用的实例；每个全局实例都是一个应用了 instance 属性的已定义名称。Lean.Parser.Command.declaration : commandinstance 声明会自动应用 instance 属性。
这里虽然已有全局实例，addPairs 仍包含一个局部定义的 Add NatPair 实例：
structure NatPair where
x : Nat
y : Nat
instance : Add NatPair where
add
| ⟨x1, y1⟩, ⟨x2, y2⟩ => ⟨x1 + x2, y1 + y2⟩
def addPairs (p1 p2 : NatPair) : NatPair :=
let _ : Add NatPair :=
⟨fun _ _ => ⟨0, 0⟩⟩
p1 + p2
最终选择的是局部实例，而非全局实例：
#eval addPairs ⟨1, 2⟩ ⟨5, 2⟩
实例的搜索过程主要由类参数支配。 类型类接受一定数量的参数；搜索期间，如果某个实例所选的参数与当前正在合成实例的类类型中的参数兼容，就会尝试该实例。
实例本身也可以接受参数，但实例的参数在实例合成中扮演的角色大不相同。 实例的参数要么表示可由实例合成实例化的变量，要么表示使用该实例前需要完成的进一步合成工作。 具体而言，实例的参数可以是显式的、隐式的或实例隐式的。 若参数是实例隐式的，就会引发进一步的递归实例搜索；而显式或隐式参数必须通过合一来解决。
虽然实例通常以隐式或实例隐式方式接受参数，但在实例合成过程中，显式参数也可以像隐式参数一样被填充。
本例中，合成过程找到 aNonemptySumInstance，并将它显式应用于 Nat，这是保证类型正确所必需的。
instance aNonemptySumInstance
(α : Type) {β : Type} [inst : Nonempty α] :
Nonempty (α ⊕ β) :=
let ⟨x⟩ := inst
⟨.inl x⟩
set_option pp.explicit true in
#synth Nonempty (Nat ⊕ Empty)
输出中，显式参数 Nat 和隐式参数 Empty 都是通过与搜索目标合一找到的，而 Nonempty Nat 实例则通过递归实例合成找到。
默认情况下，类型类的参数被视为搜索过程的输入。 如果参数未知，搜索过程就会卡住，因为选择实例要求参数值与该实例中的值匹配，而依据不完整的信息无法确定这些值。 在大多数情况下，猜测实例会使实例合成变得不可预测。
然而在某些情况下，一个参数的选择应当自动决定另一个参数。
例如，重载成员关系谓词的类型类 Membership 将数据结构中元素的类型视为输出，因此在使用位置可以由数据结构的类型确定元素类型，而无需在实例合成开始前提供足够的类型标注来同时确定两种类型。
仅凭某个元素属于 List Nat，就可以断定该元素是 Nat。
可以用 outParam 这一小工具包装类型类参数的类型，从而将参数声明为输出。
当类参数是输出参数时，实例合成不会要求它已知；事实上，任何已有值都会被完全忽略。
会选中第一个匹配输入参数的实例，并将该实例为输出参数指定的值作为其值。
如果原先已有值，则在合成完成后将其与指定值比较；二者不匹配即为错误。
用于在类型类中标记输出参数的辅助构造。
例如，Membership 类定义为：
class Membership (α : outParam (Type u)) (γ : Type v)
这表示每当出现形如 Membership ?α ?γ 的类型类目标时，Lean 会等到 ?γ 已知后再求解；
随后运行实例合成，并接受为 ?α 取任意值时找到的第一个解，由此确定 ?α 应取的值。
这表达了如下事实：在 a ∈ s 这样的项中，s 可能是 Set α、List α，或其他带有
成员关系操作的类型；无论哪种情况，都可以通过查看容器类型来确定“成员”类型 α。
这个序列化框架提供了将值转换为某种底层存储类型的方法：
class Serialize (input output : Type) where
ser : input → output
export Serialize (ser)
instance : Serialize Nat String where
ser n := toString n
instance [Serialize α γ] [Serialize β γ] [Append γ] :
Serialize (α × β) γ where
ser
| (x, y) => ser x ++ ser y
在本例中，输出类型未知。
example := ser (2, 3)
实例合成无法选择 Serialize Nat String 实例，因而也无法选择 Append String 实例，因为这要求将输出类型实例化为 String，所以搜索会卡住：
正如消息所示，一种修复方法是提供预期类型：
example : String := ser (2, 3)
另一种方法是将输出类型改为输出参数：
class Serialize (input : Type) (output : outParam Type) where
ser : input → output
export Serialize (ser)
instance : Serialize Nat String where
ser n := toString n
instance [Serialize α γ] [Serialize β γ] [Append γ] :
Serialize (α × β) γ where
ser
| (x, y) => ser x ++ ser y
现在，实例合成可以自由选择 Serialize Nat String 实例，从而解决 ser 的未知隐式参数 output：
example := ser (2, 3)
类 OneSmaller 表示一种转换方式：将某类型的非最大元素转换为元素数量少一个的类型中的元素。
有两个不同的实例都能匹配输入类型 Option Bool，但它们的输出不同：
class OneSmaller (α : Type) (β : outParam Type) where
biggest : α
shrink : (x : α) → x ≠ biggest → β
instance : OneSmaller (Option α) α where
biggest := none
shrink
| some x, _ => x
instance : OneSmaller (Option Bool) (Option Unit) where
biggest := some true
shrink
| none, _ => none
| some false, _ => some ()
instance : OneSmaller Bool Unit where
biggest := true
shrink
| false, _ => ()
由于实例合成会选择最近定义的实例，以下代码会报错：
#check OneSmaller.shrink (β := Bool) (some false) sorry
实例合成选择了 OneSmaller (Option Bool) (Option Unit) 实例，而没有考虑所提供的 β 值。
半输出参数与输出参数相似，都无需在合成开始前已知；但与输出参数不同，选择实例时会考虑半输出参数的值。
用于在类型类中标记半输出参数的辅助构造。
半输出参数会影响类型类实例各参数的处理顺序。Lean 会确定一个顺序：只有当实例参数的
所有非（半）输出参数都已确定后，才尝试合成该参数（也就是说，这些参数不能含有在
类型类合成期间创建的、可赋值的元变量）。这会排除 [Mul β] : Add α 之类的实例，
因为 β 可以是任意类型。把参数标记为半输出参数，就是承诺该类型类的实例总会为它
填入一个值。
例如，Coe 类定义为：
class Coe (α : semiOutParam (Sort u)) (β : Sort v)
这表示所有 Coe 实例都应当为 α 提供一个具体值（即不是可赋值的元变量）。
Coe Nat Int 或 Coe α (Option α) 这样的实例是合适的，但 Coe α Nat 不合适，
因为它没有为 α 提供值。
半输出参数对实例施加了一项要求：带有半输出参数的类的每个实例，都应当确定其半输出参数的值。
类 OneSmaller 表示一种转换方式：将某类型的非最大元素转换为元素数量少一个的类型中的元素。
它有两个不同的实例都能匹配输入类型 Option Bool，但输出不同：
class OneSmaller (α : Type) (β : semiOutParam Type) where
biggest : α
shrink : (x : α) → x ≠ biggest → β
instance : OneSmaller (Option α) α where
biggest := none
shrink
| some x, _ => x
instance : OneSmaller (Option Bool) (Option Unit) where
biggest := some true
shrink
| none, _ => none
| some false, _ => some ()
instance : OneSmaller Bool Unit where
biggest := true
shrink
| false, _ => ()
由于实例合成在选择实例时会考虑半输出参数，所提供的 β 值使 OneSmaller (Option Bool) (Option Unit) 实例被跳过：
#check OneSmaller.shrink (β := Bool) (some false) sorry
当实例合成没有选中实例、原本将要失败时，会按优先级尝试使用 default_instance 属性指定的默认实例。
优先级相同时，较新定义的默认实例先于较早定义的默认实例。
会选择第一个使搜索成功的默认实例。
如果默认实例本身带有实例隐式参数，就可能引发进一步的递归实例搜索。 若递归搜索失败，搜索过程就会回溯并尝试下一个默认实例。
在实例合成期间，如果目标已完全确定（即不含元变量）且搜索成功，就不会再为同一目标尝试其他实例。 换言之，如果对某个目标的搜索成功，且后续信息增加也不可能推翻这一成功，那么即便还存在其他可能可用的实例，也不会再次尝试该目标。 这一优化可以防止实例合成搜索后续分支中的失败引发虚假回溯，避免用对巨大状态空间的缓慢探索替换先前分支中的快速解。
该优化依赖于实例是实质上典范的这一假设。
即使给定类型类的重载操作存在多个潜在实现，或由于菱形而存在多种实例合成方式，也应认为任何找到的实例都与其他实例同样好。
换言之，只要保证其中一个实例可用，就无需考虑所有潜在实例。
可以用向后兼容选项 backward.synthInstance.canonInstances 禁用该优化；此选项可能会在未来版本的 Lean 中移除。
使用实例隐式参数的代码应当准备好将所有实例视为等价。 换言之，它应当能够稳健应对合成实例之间的差异。 如果代码依赖实例事实上等价，那么它要么应显式操纵实例（例如通过局部定义、将实例保存在结构字段中，或让结构继承适当的类），要么应在类型中明确体现这一依赖，使不同的实例选择产生不兼容的类型。
在 inferInstanceAs 或默认的 Lean.Parser.Command.declaration : commandderiving 处理器合成实例后，会处理实例体，以确保其实例类型和各字段类型在 instances 透明度下与预期类型匹配；该透明度只展开可约定义和隐式可约定义。
这一处理可以防止实例在低于半可约透明度下归约时泄漏其实例定义的内部细节，因为这种泄漏可能在代码库的不同部分之间引入非预期依赖。
如果预期类型是命题，实例会被包装在一个辅助定理中。
否则，合成出的实例会在 instances 透明度下归约到弱头范式。
如果结果是构造器应用，则会处理每个字段：
如果能为子实例字段的类型找到新合成的实例，就用该实例替换该字段。 这可确保该实例与客户端代码自行合成实例时找到的实例相同，避免通往实例的多条路径（称为菱形）产生彼此并非定义相等的实例。 如果合成没有找到实例，就用此过程递归包装该字段。
类型与预期类型并非定义相等的证明字段，会被包装在辅助定理中，以隐藏类型差异。
类型与预期类型不匹配的数据字段，会被包装在具有适当可约性的辅助定义中。
如果实例无法归约为构造器应用且其类型与预期类型不匹配，就会被包装在具有适当可约性的辅助定义中。
synthInstance.maxHeartbeats
默认值：20000
每个类型类实例合成问题可使用的最大心跳数。一次心跳计数表示一千次（小型）内存分配；
设为 0 表示不设上限。
synthInstance.maxSize
默认值：128
类型类实例合成过程中，用于构造一个解的实例数量上限。
backward.inferInstanceAs.wrap.reuseSubInstances
默认值：true
递归处理子实例时，复用目标类型已有的实例，而不是重新包装它们；这对于避免实例菱形中 出现并非定义相等的实例可能十分重要。