From b15d6d41b87ea2a976eab0e53467be28f35c3ef6 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Mon, 24 Jul 2023 15:50:38 +0200
Subject: [PATCH] fix: missing `mkCIdent`s in Lean.Elab.Deriving.Util

---
 src/Lean/Elab/Deriving/Util.lean | 12 +++++++-----
 tests/lean/run/2344.lean         | 17 +++++++++++++++++
 2 files changed, 24 insertions(+), 5 deletions(-)
 create mode 100644 tests/lean/run/2344.lean

diff --git a/src/Lean/Elab/Deriving/Util.lean b/src/Lean/Elab/Deriving/Util.lean
index 0f8642271c..009dd21404 100644
--- a/src/Lean/Elab/Deriving/Util.lean
+++ b/src/Lean/Elab/Deriving/Util.lean
@@ -27,7 +27,7 @@ def mkInductArgNames (indVal : InductiveVal) : TermElabM (Array Name) := do
 
 /-- Return the inductive declaration's type applied to the arguments in `argNames`. -/
 def mkInductiveApp (indVal : InductiveVal) (argNames : Array Name) : TermElabM Term :=
-  let f    := mkIdent indVal.name
+  let f    := mkCIdent indVal.name
   let args := argNames.map mkIdent
   `(@$f $args*)
 
@@ -54,7 +54,7 @@ def mkInstImplicitBinders (className : Name) (indVal : InductiveVal) (argNames :
         let c ← mkAppM className #[x]
         if (← isTypeCorrect c) then
           let argName := argNames[i]!
-          let binder : Syntax ← `(instBinderF| [ $(mkIdent className):ident $(mkIdent argName):ident ])
+          let binder : Syntax ← `(instBinderF| [ $(mkCIdent className):ident $(mkIdent argName):ident ])
           binders := binders.push binder
       catch _ =>
         pure ()
@@ -94,7 +94,7 @@ def mkLocalInstanceLetDecls (ctx : Context) (className : Name) (argNames : Array
     let binders      ← mkImplicitBinders currIndices
     let argNamesNew  := argNames[:numParams] ++ currIndices
     let indType      ← mkInductiveApp indVal argNamesNew
-    let type         ← `($(mkIdent className) $indType)
+    let type         ← `($(mkCIdent className) $indType)
     let val          ← `(⟨$(mkIdent auxFunName)⟩)
     let instName     ← mkFreshUserName `localinst
     let letDecl      ← `(Parser.Term.letDecl| $(mkIdent instName):ident $binders:implicitBinder* : $type := $val)
@@ -116,8 +116,10 @@ def mkInstanceCmds (ctx : Context) (className : Name) (typeNames : Array Name) (
       let binders      ← mkImplicitBinders argNames
       let binders      := binders ++ (← mkInstImplicitBinders className indVal argNames)
       let indType      ← mkInductiveApp indVal argNames
-      let type         ← `($(mkIdent className) $indType)
-      let val          ← if useAnonCtor then `(⟨$(mkIdent auxFunName)⟩) else pure <| mkIdent auxFunName
+      let type         ← `($(mkCIdent className) $indType)
+      let mut val      := mkIdent auxFunName
+      if useAnonCtor then
+        val ← `(⟨$val⟩)
       let instCmd ← `(instance $binders:implicitBinder* : $type := $val)
       instances := instances.push instCmd
   return instances
diff --git a/tests/lean/run/2344.lean b/tests/lean/run/2344.lean
new file mode 100644
index 0000000000..20cd775ed2
--- /dev/null
+++ b/tests/lean/run/2344.lean
@@ -0,0 +1,17 @@
+namespace Value
+
+inductive Primitive where
+  | Bool (b : Bool)
+  | Int (i : Int)
+  | String (s : String)
+
+deriving instance DecidableEq for Primitive -- Works
+
+inductive Value where
+  | Primitive (p : Primitive)
+
+deriving instance DecidableEq for Primitive -- (no longer) fails
+deriving instance DecidableEq for _root_.Value.Primitive -- (no longer) fails
+
+deriving instance Repr for Primitive
+deriving instance Repr for _root_.Value.Primitive