From aa0cf78d9376818476f2d802eb7928f70e906566 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Tue, 26 Aug 2025 10:33:37 +0200
Subject: [PATCH] chore: create `.toCtorIdx` alias only for enumeration types
 (#10130)

This PR creates the deprecated `.toCtorIdx` alias only for enumeration
types, which are the types that used to have this function. No need
generating an alias for types that never had it. Should reduce the
number of symbols in the standard library.
---
 src/Lean/Meta/Constructions/CtorIdx.lean      | 28 +++++++++----------
 .../lean/computedFieldsCode.lean.expected.out |  8 ------
 tests/lean/run/ctorIdx.lean                   | 11 ++++++++
 3 files changed, 25 insertions(+), 22 deletions(-)

diff --git a/src/Lean/Meta/Constructions/CtorIdx.lean b/src/Lean/Meta/Constructions/CtorIdx.lean
index 8e66200962..a44e522220 100644
--- a/src/Lean/Meta/Constructions/CtorIdx.lean
+++ b/src/Lean/Meta/Constructions/CtorIdx.lean
@@ -79,17 +79,17 @@ public def mkCtorIdx (indName : Name) : MetaM Unit := do
       modifyEnv fun env => addProtected env declName
       setReducibleAttribute declName
 
-      -- Deprecated alias
-      -- (Add deprecation attribute after stage0 update)
-      let aliasName := mkToCtorIdxName indName
-      addAndCompile (.defnDecl (← mkDefinitionValInferringUnsafe
-        (name        := aliasName)
-        (levelParams := info.levelParams)
-        (type        := declType)
-        (value       := mkConst declName us)
-        (hints       := ReducibilityHints.abbrev)
-      ))
-      modifyEnv fun env => addToCompletionBlackList env aliasName
-      modifyEnv fun env => addProtected env aliasName
-      setReducibleAttribute aliasName
-      Lean.Linter.setDeprecated aliasName { newName? := some declName, since? := "2025-08-25" }
+      -- Deprecated alias for enumeration types (which used to have `toCtorIdx`)
+      if (← isEnumType indName) then
+        let aliasName := mkToCtorIdxName indName
+        addAndCompile (.defnDecl (← mkDefinitionValInferringUnsafe
+          (name        := aliasName)
+          (levelParams := info.levelParams)
+          (type        := declType)
+          (value       := mkConst declName us)
+          (hints       := ReducibilityHints.abbrev)
+        ))
+        modifyEnv fun env => addToCompletionBlackList env aliasName
+        modifyEnv fun env => addProtected env aliasName
+        setReducibleAttribute aliasName
+        Lean.Linter.setDeprecated aliasName { newName? := some declName, since? := "2025-08-25" }
diff --git a/tests/lean/computedFieldsCode.lean.expected.out b/tests/lean/computedFieldsCode.lean.expected.out
index 12f77c85b6..8bfb81fad1 100644
--- a/tests/lean/computedFieldsCode.lean.expected.out
+++ b/tests/lean/computedFieldsCode.lean.expected.out
@@ -26,14 +26,6 @@
       let x_2 : tobj := Exp.ctorIdx x_1;
       dec x_1;
       ret x_2
-[Compiler.IR] [result]
-    def Exp.toCtorIdx (x_1 : @& tobj) : tobj :=
-      let x_2 : tobj := Exp.ctorIdx x_1;
-      ret x_2
-    def Exp.toCtorIdx._boxed (x_1 : tobj) : tobj :=
-      let x_2 : tobj := Exp.toCtorIdx x_1;
-      dec x_1;
-      ret x_2
 [Compiler.IR] [result]
     def Exp.casesOn._override._redArg (x_1 : tobj) (x_2 : tobj) (x_3 : tobj) (x_4 : @& tobj) (x_5 : @& tobj) (x_6 : @& tobj) (x_7 : @& tobj) (x_8 : @& tobj) : tobj :=
       case x_1 : tobj of
diff --git a/tests/lean/run/ctorIdx.lean b/tests/lean/run/ctorIdx.lean
index edafffdb71..dd5afede2f 100644
--- a/tests/lean/run/ctorIdx.lean
+++ b/tests/lean/run/ctorIdx.lean
@@ -69,3 +69,14 @@ inductive Eq' : α → α → Prop where | refl (a : α) : Eq' a a
 /-- error: Unknown constant `Eq'.ctorIdx` -/
 #guard_msgs in
 #print Eq'.ctorIdx
+
+
+set_option linter.deprecated true
+
+-- Enumeration types get a deprecated alias, other types dont
+/-- info: Enum.toCtorIdx : Enum → Nat -/
+#guard_msgs in #check Enum.toCtorIdx
+/-- warning: `Enum.toCtorIdx` has been deprecated: Use `Enum.ctorIdx` instead -/
+#guard_msgs in example := Enum.toCtorIdx
+/-- error: Unknown identifier `Nonrec.toCtorIdx` -/
+#guard_msgs in #check Nonrec.toCtorIdx