From 0803f1e77e486a4ea7603b394789e05cebcd94f5 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Tue, 26 Aug 2025 15:00:10 +0200
Subject: [PATCH] perf: ctorIdx for single-constructor inductives: no casesOn,
 macro_inline (#10135)

This PR lets the `ctorIdx` definition for single constructor inductives
avoid the pointless `.casesOn`, and uses `macro_inline` to avoid
compiling the function and wasting symbols.
---
 src/Lean/Meta/Constructions/CtorIdx.lean | 43 +++++++++++++++---------
 tests/lean/run/ctorIdx.lean              | 21 +++++++++++-
 2 files changed, 47 insertions(+), 17 deletions(-)

diff --git a/src/Lean/Meta/Constructions/CtorIdx.lean b/src/Lean/Meta/Constructions/CtorIdx.lean
index a44e522220..3a32ca6ead 100644
--- a/src/Lean/Meta/Constructions/CtorIdx.lean
+++ b/src/Lean/Meta/Constructions/CtorIdx.lean
@@ -55,26 +55,34 @@ public def mkCtorIdx (indName : Name) : MetaM Unit := do
       let declType ← mkArrow indType natType
       let declType ← mkForallFVars xs declType
       let declValue ← withLocalDeclD `x indType fun x => do
-        let motive ← mkLambdaFVars (indices.push x) natType
-        let mut value := mkConst casesOnName (levelOne::us)
-        value := mkAppN value params
-        value := mkApp value motive
-        value := mkAppN value indices
-        value := mkApp value x
-        for c in info.ctors do
-          let cInfo ← getConstInfoCtor c
-          let cType ← instantiateForall cInfo.type params
-          let alt ← forallBoundedTelescope cType cInfo.numFields fun ys _ =>
-            mkLambdaFVars ys <| mkRawNatLit cInfo.cidx
-          value := mkApp value alt
+        let value ← if info.numCtors = 1 then
+          pure (mkRawNatLit 0)
+        else
+          let motive ← mkLambdaFVars (indices.push x) natType
+          let mut value := mkConst casesOnName (levelOne::us)
+          value := mkAppN value params
+          value := mkApp value motive
+          value := mkAppN value indices
+          value := mkApp value x
+          for c in info.ctors do
+            let cInfo ← getConstInfoCtor c
+            let cType ← instantiateForall cInfo.type params
+            let alt ← forallBoundedTelescope cType cInfo.numFields fun ys _ =>
+              mkLambdaFVars ys <| mkRawNatLit cInfo.cidx
+            value := mkApp value alt
+          pure value
         mkLambdaFVars (xs.push x) value
-      addAndCompile (.defnDecl (← mkDefinitionValInferringUnsafe
+      let decl := .defnDecl (← mkDefinitionValInferringUnsafe
         (name        := declName)
         (levelParams := info.levelParams)
         (type        := declType)
         (value       := declValue)
         (hints       := ReducibilityHints.abbrev)
-      ))
+      )
+      addDecl decl
+      if info.numCtors = 1 then
+        setInlineAttribute declName .macroInline
+      compileDecl decl
       modifyEnv fun env => addToCompletionBlackList env declName
       modifyEnv fun env => addProtected env declName
       setReducibleAttribute declName
@@ -82,13 +90,16 @@ public def mkCtorIdx (indName : Name) : MetaM Unit := do
       -- Deprecated alias for enumeration types (which used to have `toCtorIdx`)
       if (← isEnumType indName) then
         let aliasName := mkToCtorIdxName indName
-        addAndCompile (.defnDecl (← mkDefinitionValInferringUnsafe
+        let decl := .defnDecl (← mkDefinitionValInferringUnsafe
           (name        := aliasName)
           (levelParams := info.levelParams)
           (type        := declType)
           (value       := mkConst declName us)
           (hints       := ReducibilityHints.abbrev)
-        ))
+        )
+        addDecl decl
+        setInlineAttribute aliasName .macroInline
+        compileDecl decl
         modifyEnv fun env => addToCompletionBlackList env aliasName
         modifyEnv fun env => addProtected env aliasName
         setReducibleAttribute aliasName
diff --git a/tests/lean/run/ctorIdx.lean b/tests/lean/run/ctorIdx.lean
index dd5afede2f..a753fca995 100644
--- a/tests/lean/run/ctorIdx.lean
+++ b/tests/lean/run/ctorIdx.lean
@@ -54,11 +54,30 @@ fun {m a} x => x.casesOn (fun {n} a => 0) (fun {n} a => 1) 2
 #guard_msgs in
 #print B.ctorIdx
 
+-- Single constructor inductives do not use casesOn
+
+inductive Single where | only (n : Nat)
+/--
+info: @[reducible] protected def Single.ctorIdx : Single → Nat :=
+fun x => 0
+-/
+#guard_msgs in #print Single.ctorIdx
+
+structure Struct where
+  field1 : Nat
+  field2 : Bool
+/--
+info: @[reducible] protected def Struct.ctorIdx : Struct → Nat :=
+fun x => 0
+-/
+#guard_msgs in #print Struct.ctorIdx
+
+-- Unsafe inductives do get a definition
 
 unsafe inductive U : Type | mk : (U → U) → U
 /--
 info: @[reducible] unsafe protected def U.ctorIdx : U → Nat :=
-fun x => U.casesOn x fun a => 0
+fun x => 0
 -/
 #guard_msgs in
 #print U.ctorIdx