Lean 4

Failed to synthesize instance (Lean 4)

Lean needed a type class instance (such as Add, Decidable, Inhabited or a Mathlib structure like Field) and could not find one for your type.

What it looks like

Main.lean:8:16: error(lean.synthInstanceFailed): failed to synthesize instance of type class
  Inhabited Point

Hint: Adding the command `deriving instance Inhabited for Point` may allow Lean to derive the missing instance.

What does "Failed to synthesize instance (Lean 4)" mean?

Type classes are how Lean finds operations and facts for a type: + needs an HAdd instance, if p then … else … needs Decidable p, default needs Inhabited. When the search fails, Lean prints the instance it was looking for. Lean 4.27 and later say failed to synthesize instance of type class (labelled error(lean.synthInstanceFailed) on the command line); Lean 4.26 and earlier say failed to synthesize. If the search runs out of time instead, the message mentions (deterministic) timeout at `typeclass`.

What causes "Failed to synthesize instance (Lean 4)"?

The type has no instance — for example a new structure without deriving Repr, DecidableEq or Inhabited.
The Mathlib import that provides the instance is missing.
The types do not line up, so Lean searches for an odd instance such as HAdd ℕ ℝ ?m.
A Decidable instance is needed for a proposition Lean cannot decide by computation.

How do I confirm the cause?

Check the types in the instance: a ?m placeholder or two different number types means the real problem is a type mismatch earlier.
Test the search on its own with #synth Inhabited Point.
Add set_option trace.Meta.synthInstance true in before the declaration to see each instance Lean tried and why it failed.

How do I fix "Failed to synthesize instance (Lean 4)"?

Read the instance in the message — the class and the type — and check that it should exist.
Add deriving Repr, DecidableEq, Inhabited (or BEq, Hashable…) to your structure or inductive type.
Add the import, or a hypothesis such as [Field K] to the theorem when the type is a variable.
For Decidable in proofs, open Classical makes every proposition decidable (noncomputably).

How do I stop it happening again?

Derive the standard instances when you define a structure or inductive type.
In general theorems, state type-class assumptions in the binders ([LinearOrder α]) rather than relying on a concrete type.

Got a different error? Paste it into the Explain This Error tool → Identifies the family and the fix — runs locally, nothing uploaded.