Lean 语言参考手册

关于：synthInstanceFailed🔗

Error code: lean.synthInstanceFailed

Failed to synthesize instance of type class.

Severity: ErrorSince: 4.26.0

类型类 是 Lean 及许多其他编程语言用来处理重载操作的机制。处理特定 重载操作的代码是类型类的一个 实例；为给定重载操作决定使用哪个实例的过程称为实例合成。

例如，当 Lean 遇到表达式 x + y，且 x 和 y 都具有 Int 类型时，既需要查找两个整数的相加方式，也需要确定结果类型。这一过程就是合成类型类 HAdd Int Int t 的实例，其中 t 是某种类型。

许多实例合成失败都是由错误的二元运算导致的。成功和失败并不总是显而易见，因为有些实例 是根据其他实例定义的，Lean 必须递归搜索才能找到合适的实例。可以 检查 Lean 的实例合成过程，这有助于诊断棘手的实例合成失败。

示例🔗

使用错误的二元运算
#eval failed to synthesize instance of type class HAdd String String ?m.4 Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command."A" + "3" 
failed to synthesize instance of type class
  HAdd String String ?m.4

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
"A3"#eval "A" ++ "3"

二元运算 + 与 HAdd 类型类相关联，而字符串不支持加法。二元运算 ++ 与 HAppend 类型类相关联，是拼接字符串的正确方式。

参数类型错误
def x : Int := 3 #eval failed to synthesize instance of type class HAppend Int String ?m.4 Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.x ++ "meters" 
failed to synthesize instance of type class
  HAppend Int String ?m.4

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
def x : Int := 3 "3meters"#eval ToString.toString x ++ "meters"

Lean 不允许直接将整数和字符串相加。函数 ToString.toString 使用类型类重载将值转换为 字符串；第二个示例之所以成功，是因为找到了 ToString Int 的实例。

缺少类型类实例
inductive MyColor where | chartreuse | sienna | thistle def forceColor (oc : Option MyColor) := failed to synthesize instance of type class Inhabited MyColor Hint: Adding the command `deriving instance Inhabited for MyColor` may allow Lean to derive the missing instance.oc.get! 
failed to synthesize instance of type class
  Inhabited MyColor

Hint: Adding the command `deriving instance Inhabited for MyColor` may allow Lean to derive the missing instance.
inductive MyColor where | chartreuse | sienna | thistle deriving Inhabited def forceColor (oc : Option MyColor) := oc.get!
inductive MyColor where | chartreuse | sienna | thistle deriving instance Inhabited for MyColor def forceColor (oc : Option MyColor) := oc.get!
inductive MyColor where | chartreuse | sienna | thistle instance : Inhabited MyColor where default := .sienna def forceColor (oc : Option MyColor) := oc.get!

实例合成可能失败，仅仅是因为尚未提供该类型类的实例。这通常发生在 Repr、BEq、 ToJson 和 Inhabited 等类型类上。Lean 通常可以在定义类型时，或使用独立的 Lean.Parser.Command.deriving : commandderiving 命令，通过 deriving 关键字 自动生成类型类的实例。