unnecessary cycle during instance synthesization

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

Using instances with forall can cause instance synthesization to add an unnecessary cycle.

Context

This occurred while testing with a LawfulBEq => DecidableEq instance.

Steps to Reproduce

class Foo (α : Type) where
  value : α → α → Bool

class Bar (x y : α) where
  value : Bool

instance : Bar x y := ⟨false⟩
instance [Foo α] : ∀ x y : α, Bar x y := fun x y => ⟨Foo.value x y⟩
instance [∀ x y : α, Bar x y] : Foo α := ⟨fun x y => Bar.value x y⟩

variable (α : Type) (x y : α)
set_option pp.explicit true in
/--
info: @instBarOfFoo α (@instFooOfBar α (@instBar α)) x y
-/
#guard_msgs in
#synth Bar x y
-- expected: @instBar α x y

Versions

4.20.0-nightly-2025-04-08

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start with the minimal self-contained Lean reproducer in the issue and inspect how instance synthesis handles forall instances and cycle detection. Done means #synth Bar x y selects the direct instance without adding the unnecessary instBarOfFoo/instFooOfBar cycle.