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

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.