loop in typeclass inference at different depths

Prerequisites

• 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

Loops are normally detected by typeclass inference. However, this is not the case if the loop happens at different depths, leading to max recursion or bad performance.

Context

This is a minimized version of a serious performance issue in Mathlib related to Riemannian geometry. Discussed at #mathlib4 > Slow Riemannian geometry @ 💬

Steps to Reproduce

class SGTop (α : Type)
class SGIsCont (α : Type) [SGTop α]
class SGNormed (α : Type) extends SGTop α

instance instIsContOfNormed {α : Type} [SGNormed α] : SGIsCont α where
instance instIsNormedOfBundle {α : Type} [SGTop α] [SGIsCont α] : SGNormed α where

variable {α : Type} [SGTop α]

set_option maxSynthPendingDepth 500

/--
error: failed to synthesize
  SGNormed α
maximum recursion depth has been reached
use `set_option maxRecDepth <num>` to increase limit
use `set_option diagnostics true` to get diagnostic information

Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
-/
#guard_msgs in
#synth SGIsCont α

Expected behavior:

To synthetize SGIsCont α, Lean tries to apply instIsContOfNormed, and then instIsNormedOfBundle. For the latter to make sense, it needs SGIsCont α. Typeclass inference should see that there is a loop, and stop there.

Actual behavior:

Typeclass inference does not detect that there is a loop (probably because it's at depth one more), tries again the same instances, and this goes on forever, resulting in a maximum recursion error. With the standard values for maxSynthPendingDepth of 2 or 3, the loop stops after a few iterations, but this has still a very bad performance impact in Mathlib real-life situation.

Versions

Lean 4.29.0-rc6

Impact

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

Start with the minimized reproduction in the issue and the typeclass inference behavior controlled by maxSynthPendingDepth. Compare the nightly result with the expected loop detection at different depths. Done means the example terminates by recognizing the recursive SGIsCont/SGNormed cycle without reaching a maximum recursion error.