Typeclass instance problem stuck for fields of class dependent on class with `outParam`

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

In a class Y [X n] dependent on another class X with an output parameter n, the automatically determined signatures of fields contain X n as implicit parameter, even if there is no way other than typeclass inference to synthesize this parameter. As a consequence when applying a field of such a class, typeclass synthesis frequently gets stuck.

Steps to Reproduce

Run this:

class X (n : outParam Nat) where

class Y [X n] where
  field : Vector Nat n

instance : X 0 where

instance : Y where
  field := #v[]

-- Note that `X n` is an implicit parameter.
/-- info: Y.field {n : Nat} {inst✝ : X n} [self : Y] : Vector Nat n -/
#guard_msgs in
#check Y.field

def Y.field' {n : Nat} [X n] [self : Y] : Vector Nat n :=
  Y.field

/-! The auto-generated field projection is problematic: -/

/--
error: typeclass instance problem is stuck, it is often due to metavariables
  Y
-/
#guard_msgs in
example : Y.field = 0 := by
  rfl

/-! With our manually defined projection, it works: -/

-- Succeeds with manual definition where `[X n]` is an instance parameter
example : Y.field' = 0 := by
  rfl

Expected behavior:

In the signature of the projection Y.field, sufficiently many parameters are explicit or instance parameters so that type inference does not get stuck.

In particular, the parameter of type X n should be an instance parameter, not an implicit parameter.

Actual behavior:

Y.field has an implicit parameter of type X n, causing Lean to fail synthesizing Y.

Versions

Lean 4.24.0-nightly-2025-08-21
Target: x86_64-unknown-linux-gnu

Context

For the polymorphic range library, I'm trying out to define the SupportsLowerBound class using an outParam:

/--
This typeclass provides decidable lower bound checks of the given shape.

Instances are automatically provided in the following cases:

* `shape` is `open` and there is an `LT α` instance
* `shape` is `closed` and there is an `LE α` instance
* `shape` is `.unbounded`
-/
class SupportsLowerBound (shape : BoundShape) (α : Type u) (P : outParam (Bound shape α → α → Prop)) where
  decidable : DecidableRel P := by infer_instance

Previously, P was a field of the class and it was tedious and annoying to unfold SupportsLowerBound.IsSatisfied everywhere, because usually one knows that it's induced by LE or LT. Using an outParam makes this class more convenient to use -- in theory. In practice, I also have this typeclass:

/--
This typeclass ensures that ranges with the given shape of upper bounds are always finite.
This is a prerequisite for many functions and instances, such as `PRange.toList` or `ForIn'`.
-/
class HasFiniteRanges (shape α) {P} [UpwardEnumerable α] [SupportsUpperBound shape α P] : Prop where
  finite : (init : α) → (u : Bound shape α) → ∃ n, (UpwardEnumerable.succMany? n init).elim True (¬ P u ·)

But with this new signature of SupportsUpperBound, finite's signature contains SupportsLowerBound as an implicit parameter instead of an instance parameter. When simply using HasFiniteRanges.finite init u, Lean is is unable to assign the metavariable for this implicit parameter.

A workaround is to define HasFiniteRanges directly as an inductive type and to define the finite by hand, choosing SupportsUpperBound to be an instance parameter. But this is very annoying and there are more classes where I would need to do this.

Impact

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

Start by running the linked Lean nightly reproducer and inspect the generated signature of Y.field alongside the manually defined Y.field'. Confirm that the projection's X n parameter is treated as an instance parameter and that the Y.field example no longer gets stuck during typeclass synthesis.