class projections have the wrong binderInfo

[JovanGerb]

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

#5376 changed the binderinfo for class projections with the goal of speeding up type class search. In particular, the instance implicit parameters of the type class now get an implicit binderInfo in projections. Unfortunately, the new binderInfos are wrong. This leads to 2 problems:

1. When elaborating a type class projection, the instance implicit parameters of the type class don't get synthesized immediately. Instead they get filled in during type class search by synthPending, even though type class search uses withNewMCtxDepth (see issue synthPending doesn't respect metavariable context depth #9726). For example

class A (α : Type) where

class B (G : Type) [A G] where
  x : Nat
#check B.x -- B.x (G : Type) {inst✝ : A G} [self : B G] : Nat

variable {G : Type} [A G] [B G]
set_option pp.explicit true in
set_option trace.Meta.synthInstance true in
#check B.x (G := G)

The trace show the following

[Meta.synthInstance] ✅️ @B G inst✝¹ ▼
  [] new goal @B G ?m.560 ▶
  [] ✅️ apply inst✝ to @B G inst✝¹ ▼
    [tryResolve] ✅️ @B G inst✝¹ ≟ @B G inst✝¹ ▼
      [] ✅️ A G ▶
    [answer] ✅️ @B G inst✝¹ 
  [] result inst✝ 

You can see there that the type class search starts with @B G ?m, where ?m is a metavariable introduced by the elaborator. And we see a nested type class search goal A G, which then leads to the answer having type @B G inst✝¹. So, the metavariable is illegally filled in by synthPending. To fix this problem, B.x needs to take the argument [A G] instead of {_ : A G}.

2. When declaring a class using extends, Lean should check that the generated instance is valid. However, since fix: modify projection instance binder info #5376, this doesn't work as well anymore. This has lead to people unknowingly defining some illegal instances in batteries and mathlib. The miminized examples are as follows. In each case B.toA is a bad instance but Lean doesn't complain. And if you try to write an instance with the same type, Lean does complain.

namespace test1
class A (α : Type) where
class B (α β : Type) extends A α
#check B.toA
instance {α : Type} (β : Type) [B α β] : A α where
end test1

namespace test2
class A (α : Type) (β : semiOutParam Type) where
class B (α β : Type) extends A α β where
#check B.toA
instance {α β : Type} [B α β] : A α β where
end test2

Context

This bug needs to be fixed in order to fix #9726, and to get #lean4 > One line change gives type class search speedup of 17% to work.

Zulip discussion on this topic: #lean4 > projection instance binderinfo problem

Steps to Reproduce

namespace test1
class A (α : Type) where
class B (α β : Type) extends A α
end test1

namespace test2
class A (α : Type) (β : semiOutParam Type) where
class B (α β : Type) extends A α β where
end test2

namespace test3
class A (α : Type) where

class B (G : Type) [A G] where
  x : Nat
variable {G : Type} [A G] [B G]
set_option pp.explicit true in
set_option trace.Meta.synthInstance true in
#check B.x (G := G)
end test3

Expected behavior: test1 and test2 give an error, and test3 works without an illegal metavariable assignment.

Actual behavior: test1 and test2 don't give an error, and test3 works by doing an illegal metavariable assignment.

Versions

Lean 4.23.0-nightly-2025-08-04

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.