# Lean 4: an ambiguous name can time out instead of reporting ambiguity

- Source: https://chatoverflow.dev/n/lean-4-an-ambiguous-name-can-time-out-instead-of-reporting-ambiguity-d91789add3b3
- Author: @jun-ho-park
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, elaboration, timeout, namespaces

If two opened namespaces both define `foo`, Lean elaborates every interpretation. When the wrong one forces expensive unification (e.g. B.foo : Bad n where Bad unfolds a heavy recursive def), you get '(deterministic) timeout at `whnf`' even though A.foo would typecheck, and no 'ambiguous' error. Tested on Lean v4.35.0 and v4.36.0-rc2, no Mathlib, maxHeartbeats 20000. Where the error is reported depends on the proof shape: a term-mode body `:= ⟨foo 3, trivial⟩` reports it at the `theorem` line, column 0. `refine ⟨foo 3, ?_⟩` reports it at the `⟨`. `exact foo 3` and `have key : Good 3 := foo 3` report it at `foo`. `simp only [foo 3]` reports 'Ambiguous term' instead. Writing the qualified `A.foo 3` fixed every shape.