1.21 Error Messages and Debugging

Lean’s error messages report failed constraints during elaboration. Each message corresponds to a precise mismatch between what is required and what is available. Effective debugging means isolating the failing constraint, inspecting the local context, and adjusting types, arguments, or structure until the constraint is satisfied.

Problem

You encounter type errors, failed tactic steps, or unresolved instances, and you want a systematic method to diagnose and fix them.

Solution

Reduce the problem to a small expression, inspect types with #check, expose implicit arguments, and control rewriting or inference locally.

Reading a Type Mismatch

A common error is a type mismatch.

def bad (n : Nat) : Nat :=
  n + true

Lean reports that true has type Bool while + expects Nat. The fix is to correct the argument type.

def good (n : Nat) : Nat :=
  n + 1

When the message is longer, focus on the final lines that show:

• the expected type
• the actual type

Isolating the Failing Subexpression

Break a complex expression into parts.

#check subexpr

If the whole term fails, check its components one by one.

#check Nat.add
#check (2 : Nat)
#check (3 : Nat)

Then rebuild the expression.

Using Type Ascriptions

Force Lean to interpret an expression with a specific type.

#check (0 : Nat)
#check (0 : Int)

If a polymorphic expression is ambiguous:

def emptyList {α : Type} : List α :=
  []

Guide Lean:

#check (emptyList : List Nat)

Inspecting Implicit Arguments

Expose implicit parameters with @.

#check @List.map

This reveals all arguments and often explains why a call fails.

If a function application behaves unexpectedly:

#check f
#check @f

Compare the inferred and explicit forms.

Debugging Tactic Failures

When a tactic fails, inspect the goal.

theorem ex (P : Prop) (h : P) : P := by
  _

Check:

• the goal
• the context

Then choose a tactic that matches the goal.

If exact t fails, check:

#check t

The type must match the goal exactly.

Common Tactic Errors

apply creates unexpected goals

apply f

Lean replaces the goal with the premises of f. Inspect:

#check f

Understand its type before applying it.

rw does nothing

The pattern does not match.

rw [h]

Check the goal and the equality shape. Try reversing:

rw [← h]

simp fails or is too aggressive

If simp does not simplify:

• the needed lemma may not be registered

If simp changes too much:

• replace it with explicit rw steps

Instance Resolution Errors

Lean may report:

failed to synthesize instance

This means a typeclass argument in square brackets could not be found.

Example:

def showDefault {α : Type} [Inhabited α] : α :=
  default

Use:

#check (showDefault : Nat)

If no instance exists, either:

• provide one
• change the type

Unification Failures

Lean sometimes cannot match two types.

Example:

theorem bad_eq (n : Nat) : n = n + 0 := by
  rfl

This fails because n is not definitionally equal to n + 0.

Fix:

theorem good_eq (n : Nat) : n = n + 0 := by
  simp

Understand whether equality is:

• definitional (handled by rfl)
• propositional (requires lemmas like simp)

Using Holes for Debugging

Replace a failing term with _.

theorem debug (P : Prop) (h : P) : P := by
  _

Inspect the goal, then rebuild the proof step by step.

Checking Intermediate Results

Use have to isolate steps.

theorem chain (P Q R : Prop)
    (hpq : P -> Q) (hqr : Q -> R) (hp : P) : R := by
  have hq : Q := hpq hp
  have hr : R := hqr hq
  exact hr

If something fails, inspect each have.

Minimizing the Example

Reduce the failing code to a minimal case.

Bad:

-- large proof with many dependencies

Better:

-- smallest expression that still fails

This isolates the real issue and avoids noise.

Recipe: Systematic Debugging

1. Inspect the goal with a hole
2. Check subexpressions with #check
3. Add type annotations
4. Expose implicit arguments with @
5. Replace automation with explicit steps
6. Reduce to a minimal example

Common Pitfalls

If an error message is long, read the last lines first.

If types look unfamiliar, use #check on each part.

If inference fails, add explicit arguments.

If rewriting fails, verify the exact shape of the goal.

If instance search fails, check required typeclasses.

Takeaway

Lean errors report precise mismatches in types or inference. Effective debugging reduces the problem, inspects types explicitly, and rebuilds the expression step by step. Tools such as #check, holes, and explicit arguments turn debugging into a structured process rather than trial and error.