# 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.

```lean id="t1x0z9"
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.

```lean id="0l5y9o"
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.

```lean id="r2g8z3"
#check subexpr
```

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

```lean id="x4m7kw"
#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.

```lean id="n0j2sz"
#check (0 : Nat)
#check (0 : Int)
```

If a polymorphic expression is ambiguous:

```lean id="8m1t7q"
def emptyList {α : Type} : List α :=
  []
```

Guide Lean:

```lean id="b0p9dq"
#check (emptyList : List Nat)
```
## Inspecting Implicit Arguments

Expose implicit parameters with `@`.

```lean id="y6k3pd"
#check @List.map
```

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

If a function application behaves unexpectedly:

```lean id="6k8c1v"
#check f
#check @f
```

Compare the inferred and explicit forms.
## Debugging Tactic Failures

When a tactic fails, inspect the goal.

```lean id="2r3c4v"
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:

```lean id="k5l9y2"
#check t
```

The type must match the goal exactly.
## Common Tactic Errors

### `apply` creates unexpected goals

```lean id="u1p4fz"
apply f
```

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

```lean id="z8v7wm"
#check f
```

Understand its type before applying it.
### `rw` does nothing

The pattern does not match.

```lean id="o6n3qb"
rw [h]
```

Check the goal and the equality shape. Try reversing:

```lean id="d4c7xe"
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:

```text
failed to synthesize instance
```

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

Example:

```lean id="t0f9ya"
def showDefault {α : Type} [Inhabited α] : α :=
  default
```

Use:

```lean id="v9m1el"
#check (showDefault : Nat)
```

If no instance exists, either:

* provide one
* change the type
## Unification Failures

Lean sometimes cannot match two types.

Example:

```lean id="g7d2rb"
theorem bad_eq (n : Nat) : n = n + 0 := by
  rfl
```

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

Fix:

```lean id="p2k9dw"
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 `_`.

```lean id="f3c8qs"
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.

```lean id="z5u8vk"
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:

```lean id="k8q3rt"
-- large proof with many dependencies
```

Better:

```lean id="s9j4lm"
-- 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.