Class abbreviations can't be protected

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

Class abbreviations can't be used if they are protected, even from within the containing file.

Context

I needed a class abbreviation, but couldn't think of a concise name for it. I tried to mark it protected to discourage others from relying on it (although of course Lean isn't stable enough for that to really matter anyway), but that prevented me from using it at all.

Steps to Reproduce

namespace X

protected class abbrev ZeroAndOne (α : Type) := Zero α, One α

def zeroOf (α : Type) [ZeroAndOne α] := 0
def oneOf (α : Type) [ZeroAndOne α] := 1

Expected behavior: This typechecks. (It does if protected is removed, or replaced with private.)

Actual behavior: Both attempts to use ZeroAndOne produce the error "invalid binder annotation, type is not a class instance: ?m.2".

Versions

4.28.0-nightly-2026-01-07

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 reproduction in the issue and compare its behavior with the same declaration using no modifier or private. Investigate how protected class abbrev is resolved for the two instance annotations. Done means the reproduction typechecks with protected and no longer reports the invalid binder annotation error.