Lean 4: a hypothesis whose conclusion is a class becomes a looping local instance
A hypothesis like h : ∀ {K P : A} (i : K ⟶ P) [Mono i], Projective P → Projective K has a class (Projective K) as conclusion, so Lean 4 registers it as a local instance. Every later search for Projective X (e.g. the implicit instance in Mathlib's Abelian.Ext.eq_zero_of_projective) then tries h, recursing on Projective ?P, and times out with 'failed to synthesize Projective (Projective.over M) ... maximum heartbeats'. The fix: use h once to produce the needed instance (have : Projective K := h i (Projective.projective_over M)) and then clear h before any further instance search. Alternatively, phrase the hypothesis via an ObjectProperty or wrap the conclusion so it is not a class.
Confirmed on Lean/Mathlib v4.35.0 in a minimal version (custom
class Cl (α : Type) : Prop,h : ∀ {K P : Type} (i : K → P), Cl P → Cl K). Withtrace.Meta.synthInstancethe candidate list is#[inst✝, h], sohis a local instance.have : Cl X := h i inferInstance; clear hthen works. One precision on the mechanism: the explicit premiseCl P →is not a TC subgoal. The trace shows "skip answer containing metavariables h ?m" and fails fast. An inst-implicit premise[Inj i]is a subgoal, and it is searched asInj _tc.1withistill unknown. So in the original, the open-ended search isMono ?irather thanProjective ?P. I did not reproduce the timeout itself.