Typeclass search loops with `outParam` and inheritance

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

In the attached example, typeclass search repeatedly tries to apply an instance which is unrelated to the goal, causing a loop. This is the output of trace.Meta.synthInstance:

[Meta.synthInstance] 💥️ BotHomClass (SupHom α) α ▼
  [] new goal BotHomClass (SupHom α) _tc.0 ▶
  [] ✅️ apply @SupBotHomClass.toBotHomClass to BotHomClass (SupHom α) ?m.4 ▶
  [] ✅️ apply @BoundedLatticeHomClass.toSupBotHomClass to SupBotHomClass (SupHom α) ?m.7 ▶
  [] ✅️ apply @Pi.instLattice to Lattice ((i : ?m.10) → ?m.11 i) ▶
  [] ✅️ apply @Pi.instLattice to (i : ?m.10) → Lattice ((i_1 : ?m.13 i) → ?m.14 i i_1) ▶
  [] ✅️ apply @Pi.instLattice to (i : ?m.10) → (i_1 : ?m.13 i) → Lattice ((i_2 : ?m.16 i i_1) → ?m.17 i i_1 i_2) ▶
  [] ✅️ apply @Pi.instLattice to (i : ?m.10) →
        (i_1 : ?m.13 i) → (i_2 : ?m.16 i i_1) → Lattice ((i_3 : ?m.19 i i_1 i_2) → ?m.20 i i_1 i_2 i_3) ▶
  ...

Context

I was trying to redefine BoundedOrderHomClass using inheritance, but a simp timed out when it tried to rewrite using BotHomClass.map_bot.

Steps to Reproduce

class Lattice (α : Type) : Type where

instance Pi.instLattice {ι : Type} {α' : ι → Type} [∀ i, Lattice (α' i)] :
    Lattice (∀ i, α' i) where

class BotHomClass (F : Type) (α : outParam Type) : Prop where
  map_bot : True

class SupHomClass (F α : Type) : Prop where
  map_sup : True

class SupBotHomClass (F α : Type) : Prop
  extends SupHomClass F α, BotHomClass F α where

class BoundedLatticeHomClass (F α : Type) [Lattice α]  : Prop
  extends SupHomClass F α, SupBotHomClass F α where

structure SupHom (α : Type) where

instance (priority := low) SupHom.instBotHomClass {α : Type} : BotHomClass (SupHom α) α where
  map_bot := trivial

variable {α : Type}

/--
error: failed to synthesize
  BotHomClass (SupHom α) ?_
(deterministic) timeout at `typeclass`, maximum number of heartbeats (20000) has been reached

Note: Use `set_option synthInstance.maxHeartbeats <num>` to set the limit.

Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.

Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
-/
#guard_msgs in
set_option pp.mvars false in
#synth BotHomClass (SupHom α) α

Expected behavior: The synthesis should succeed.

Actual behavior: The loop causes a timeout, preventing the low-priority instance from applying.

Versions

Lean 4.29.0-rc6
Target: x86_64-unknown-linux-gnu

Additional Information

[Additional information, configuration or data that might be necessary to reproduce the issue]

Impact

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

Start with the self-contained reproduction and the trace.Meta.synthInstance output, then run the #synth BotHomClass (SupHom α) α case with the stated heartbeat limit. Trace why the inherited instances and Pi.instLattice recur despite the low-priority instance; done means synthesis succeeds without timing out and the reproduction's expected behavior holds.