`lean.synthInstanceFailed`

Failed to synthesize instance of type class

Severity: ErrorSince: 4.26.0

Type classes are the mechanism that Lean and many other programming languages use to handle overloaded operations. The code that handles a particular overloaded operation is an instance of a typeclass; deciding which instance to use for a given overloaded operation is called synthesizing an instance.

As an example, when Lean encounters an expression x + y where x and y both have type Int, it is necessary to look up how it should add two integers and also look up what the resulting type will be. This is described as synthesizing an instance of the type class HAdd Int Int t for some type t.

Many failures to synthesize an instance of a type class are the result of using the wrong binary operation. Both success and failure are not always straightforward, because some instances are defined in terms of other instances, and Lean must recursively search to find appropriate instances. It's possible to inspect Lean's instance synthesis](https://lean-lang.org/doc/reference/latest/find/?domain=Verso.Genre.Manual.section&name=instance-search), and this can be helpful for diagnosing tricky failures of type class instance synthesis.

Examples

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"

The binary operation + is associated with the HAdd type class, and there's no way to add two strings. The binary operation ++, associated with the HAppend type class, is the correct way to append strings.

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 does not allow integers and strings to be added directly. The function ToString.toString uses type class overloading to convert values to strings; by successfully searching for an instance of ToString Int, the second example will succeed.

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: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.

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 class synthesis can fail because an instance of the type class simply needs to be provided. This commonly happens for type classes like Repr, BEq, ToJson and Inhabited. Lean can often automatically generate instances of the type class with the deriving keyword, either when the type is defined or with the stand-alone deriving command.