From 30f41fe5426c50e2126dbb760ade0534159065ff Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Mon, 6 Oct 2025 13:46:46 +0200
Subject: [PATCH] fix: instance name for deriving ToExpr (#10682)

This PR changes the instance name for `deriving ToExpr` to be consistent
with other derived instance since #10271. Fixes #10678.
---
 src/Lean/Elab/Deriving/Inhabited.lean |  2 +-
 src/Lean/Elab/Deriving/ToExpr.lean    | 18 ++++----
 tests/lean/run/issue10678.lean        | 65 +++++++++++++++++++++++++++
 3 files changed, 75 insertions(+), 10 deletions(-)
 create mode 100644 tests/lean/run/issue10678.lean

diff --git a/src/Lean/Elab/Deriving/Inhabited.lean b/src/Lean/Elab/Deriving/Inhabited.lean
index a8244b9a68..d6dd279567 100644
--- a/src/Lean/Elab/Deriving/Inhabited.lean
+++ b/src/Lean/Elab/Deriving/Inhabited.lean
@@ -84,7 +84,7 @@ where
     let ctx ← mkContext ``Inhabited "default" inductiveTypeName
     let auxFunName := ctx.auxFunNames[0]!
     `(def $(mkIdent auxFunName):ident $binders:bracketedBinder* : $type := $val
-      instance $binders:bracketedBinder* : Inhabited $type := ⟨$(mkIdent auxFunName)⟩)
+      instance $(mkIdent ctx.instName):ident $binders:bracketedBinder* : Inhabited $type := ⟨$(mkIdent auxFunName)⟩)
 
 
   mkInstanceCmd? : TermElabM (Option Syntax) := do
diff --git a/src/Lean/Elab/Deriving/ToExpr.lean b/src/Lean/Elab/Deriving/ToExpr.lean
index 9fe1341ed3..8d10477e65 100644
--- a/src/Lean/Elab/Deriving/ToExpr.lean
+++ b/src/Lean/Elab/Deriving/ToExpr.lean
@@ -6,13 +6,11 @@ Authors: Kyle Miller
 module
 
 prelude
-public import Lean.Meta.Transform
-public import Lean.Elab.Deriving.Basic
-public import Lean.Elab.Deriving.Util
-public import Lean.ToLevel
-public import Lean.ToExpr
-
-public section
+import Lean.Meta.Transform
+import Lean.Elab.Deriving.Basic
+import Lean.Elab.Deriving.Util
+import Lean.ToLevel
+import Lean.ToExpr
 
 /-!
 # `ToExpr` deriving handler
@@ -190,7 +188,8 @@ open TSyntax.Compat in
 /--
 Assuming all of the auxiliary definitions exist,
 creates all the `instance` commands for the `ToExpr` instances for the (mutual) inductive type(s).
-This is a modified copy of `Lean.Elab.Deriving.mkInstanceCmds` to account for `ToLevel` instances.
+This is a modified copy of `Lean.Elab.Deriving.mkInstanceCmds` to account for `ToLevel` instances
+parameters.
 -/
 def mkInstanceCmds (ctx : Deriving.Context) (typeNames : Array Name) :
     TermElabM (Array Command) := do
@@ -206,7 +205,8 @@ def mkInstanceCmds (ctx : Deriving.Context) (typeNames : Array Name) :
       let binders      := binders ++ levelBinders
       let indType      ← updateIndType indVal (← mkInductiveApp indVal argNames)
       let toTypeExpr   ← mkToTypeExpr indVal argNames
-      let instCmd ← `(instance $binders:implicitBinder* : ToExpr $indType where
+      let instName     ← mkInstName ``ToExpr indVal.name
+      let instCmd ← `(instance $(mkIdent instName):ident $binders:implicitBinder* : ToExpr $indType where
                         toExpr := $(mkIdent auxFunName) $toLevelInsts*
                         toTypeExpr := $toTypeExpr)
       instances := instances.push instCmd
diff --git a/tests/lean/run/issue10678.lean b/tests/lean/run/issue10678.lean
new file mode 100644
index 0000000000..6d77e3bd64
--- /dev/null
+++ b/tests/lean/run/issue10678.lean
@@ -0,0 +1,65 @@
+import Lean
+
+namespace A
+
+structure A (α : Type u) where
+  a : α
+deriving Lean.ToExpr, Inhabited
+
+-- same namespace for instance and aux decls
+
+/--
+info: def A.instToExprA.{u} : {α : Type u} → [Lean.ToExpr α] → [Lean.ToLevel] → Lean.ToExpr (A α) :=
+fun {α} [Lean.ToExpr α] [inst_1 : Lean.ToLevel] =>
+  { toExpr := instToExprA.toExpr inst_1, toTypeExpr := (Lean.Expr.const `A.A [Lean.toLevel]).app (Lean.toTypeExpr α) }
+-/
+#guard_msgs in #print A.instToExprA
+
+
+/--
+info: def A.instInhabitedA.{u_1} : {a : Type u_1} → [Inhabited a] → Inhabited (A a) :=
+fun {a} [Inhabited a] => { default := instInhabitedA.default }
+-/
+#guard_msgs in #print A.instInhabitedA
+
+end A
+
+mutual
+inductive B (α : Type u) : Type _ where
+  | leaf
+  | mk (a : C α)
+deriving Lean.ToExpr, Inhabited
+inductive C (α : Type u) : Type _ where
+  | mk (b : B α)
+deriving Lean.ToExpr, Inhabited
+end
+
+/--
+info: def instToExprB.{u} : {α : Type u} → [Lean.ToExpr α] → [Lean.ToLevel] → Lean.ToExpr (B α) :=
+fun {α} [Lean.ToExpr α] [inst_1 : Lean.ToLevel] =>
+  { toExpr := instToExprB.toExpr_1 inst_1, toTypeExpr := (Lean.Expr.const `B [Lean.toLevel]).app (Lean.toTypeExpr α) }
+-/
+#guard_msgs in
+#print instToExprB
+/--
+info: def instToExprC.{u} : {α : Type u} → [Lean.ToExpr α] → [Lean.ToLevel] → Lean.ToExpr (C α) :=
+fun {α} [Lean.ToExpr α] [inst_1 : Lean.ToLevel] =>
+  { toExpr := instToExprB.toExpr_2 inst_1, toTypeExpr := (Lean.Expr.const `C [Lean.toLevel]).app (Lean.toTypeExpr α) }
+-/
+#guard_msgs in
+#print instToExprC
+
+
+/--
+info: def instInhabitedB.{u_1} : {a : Type u_1} → Inhabited (B a) :=
+fun {a} => { default := instInhabitedB.default_1 }
+-/
+#guard_msgs in
+#print instInhabitedB
+
+/--
+info: def instInhabitedC.{u_1} : {a : Type u_1} → Inhabited (C a) :=
+fun {a} => { default := instInhabitedC.default_1 }
+-/
+#guard_msgs in
+#print instInhabitedC