关于：`synthInstanceFailed`🔗

Error code: lean.synthInstanceFailed

Failed to synthesize instance of type class.

Severity: ErrorSince: 4.26.0

Type 类是 Lean 和许多其他编程语言用于处理重载操作。处理特定的代码重载操作是一个类型类的instance；决定对于给定的情况使用哪个实例重载操作称为合成实例。

例如，当 Lean 遇到表达式 x + y 时，其中 x 和 y 都有类型 Int，有必要查找它应该如何添加两个整数并查找结果类型是什么。这被描述为合成类型类的实例 HAdd Int Int t 对于某些类型 t。

许多合成类型类实例失败的原因是使用了错误的二进制文件操作。成功和失败并不总是那么简单，因为有些情况是根据其他实例定义，并且 Lean 必须递归搜索以找到适当的实例。可以检查 Lean 的实例合成，并且这个有助于诊断类型类实例合成的棘手故障。

示例🔗

Using the Wrong Binary Operation

#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 类型类关联的二元运算 ++ 是附加字符串的正确方法。

Arguments Have the Wrong Type

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 的实例，第二个示例将成功。

Missing Type Class Instance

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!

Type 类综合可能会失败，因为只需要提供类型类的实例。对于 Repr、BEq、ToJson 等类型类，通常会发生这种情况 Inhabited。 Lean 通常可以自动生成带有 deriving 关键字的类型类在定义类型时或使用独立类型时 Lean.Parser.Command.deriving : commandderiving 命令。

关于：synthInstanceFailed🔗

示例🔗

关于：`synthInstanceFailed`🔗