fix: prevent deriving handlers from generating ambiguous identifiers (#9371)

This PR fixes an issue that caused some `deriving` handlers to fail when
the name of the type being declared matched that of a declaration in an
open namespace.

Closes #9366

src/Lean/Elab/Deriving/BEq.lean

@@ -124,7 +124,7 @@ private def mkBEqInstanceCmds (declName : Name) : TermElabM (Array Syntax) := do
 private def mkBEqEnumFun (ctx : Context) (name : Name) : TermElabM Syntax := do
   let auxFunName := ctx.auxFunNames[0]!
   let privTk? := ctx.mkPrivateTokenFromTypes?
-  `(@[expose] $[private%$privTk?]? def $(mkIdent auxFunName):ident  (x y : $(mkIdent name)) : Bool := x.toCtorIdx == y.toCtorIdx)
+  `(@[expose] $[private%$privTk?]? def $(mkIdent auxFunName):ident  (x y : $(mkCIdent name)) : Bool := x.toCtorIdx == y.toCtorIdx)
 
 private def mkBEqEnumCmd (name : Name): TermElabM (Array Syntax) := do
   let ctx ← mkContext "beq" name

src/Lean/Elab/Deriving/DecEq.lean

@@ -184,7 +184,7 @@ def mkDecEqEnum (declName : Name) : CommandElabM Unit := do
   let ofNatIdent  := mkIdent (Name.mkStr declName "ofNat")
   let auxThmIdent := mkIdent (Name.mkStr declName "ofNat_toCtorIdx")
   let cmd ← `(
-    instance : DecidableEq $(mkIdent declName) :=
+    instance : DecidableEq $(mkCIdent declName) :=
       fun x y =>
         if h : x.toCtorIdx = y.toCtorIdx then
           -- We use `rfl` in the following proof because the first script fails for unit-like datatypes due to etaStruct.

src/Lean/Elab/Deriving/Inhabited.lean

@@ -71,7 +71,7 @@ where
       if assumingParamIdxs.contains i then
         let binder ← `(bracketedBinderF| [Inhabited $arg:ident ])
         binders := binders.push binder
-    let type ← `(Inhabited (@$(mkIdent inductiveTypeName):ident $indArgs:ident*))
+    let type ← `(Inhabited (@$(mkCIdent inductiveTypeName):ident $indArgs:ident*))
     let mut ctorArgs := #[]
     for _ in *...ctorVal.numParams do
       ctorArgs := ctorArgs.push (← `(_))

src/Lean/Server/Rpc/Deriving.lean

@@ -89,7 +89,7 @@ private def deriveInductiveInstance (indVal : InductiveVal) (params : Array Expr
 
   -- helpers for type name syntax
   let paramIds ← params.mapM fun p => return mkIdent (← getFVarLocalDecl p).userName
-  let typeId ← `(@$(mkIdent indVal.name) $paramIds*)
+  let typeId ← `(@$(mkCIdent indVal.name) $paramIds*)
 
   `(inductive RpcEncodablePacket where
       $[$ctors:ctor]*

tests/lean/run/9366.lean

@@ -0,0 +1,75 @@
+import Lean.Meta.Basic
+import Lean.Elab.Deriving.Basic
+
+/-!
+# `deriving` handlers for structures matching names in open namespaces
+
+This test ensures that `deriving` handlers do not fail when added to a declaration whose name
+matches one from an open namespace.
+
+Note that the general strategy to resolve this error is to use `mkCIdent` rather than `mkIdent` when
+referring to the declaration in deriving handlers.
+-/
+
+structure A.B where
+structure A.C where
+structure A.D where
+
+open A
+
+/-
+The following tests simulate, for each class `Cls` with a registered deriving handler, the three
+following declarations:
+
+```
+structure B where
+  deriving Cls
+
+structure C where
+  x : Nat
+  deriving Cls
+
+inductive D where
+  | mk₁ : Bool → D
+  | mk₂ : Bool → D
+  deriving Cls
+```
+
+The purpose of the three distinct declarations is to account for the fact that many deriving
+handlers have different logic for structures, singletons, and/or sums. If a class cannot be derived
+for one or more of these declarations, add it to the `exclusions` map below, indicating the tests
+from which it should be excluded.
+-/
+
+inductive ExclusionKind
+  | singleton | struct | sum
+  deriving BEq, Hashable
+
+def exclusions : Std.HashMap Lean.Name (Std.HashSet ExclusionKind) := .ofList [
+  (``SizeOf, { .singleton, .struct, .sum })
+]
+
+open Lean Meta Elab Command in
+set_option hygiene false in
+#eval show CommandElabM Unit from do
+  let go : StateRefT (Array (Name × PersistentArray Message)) CommandElabM Unit := do
+    let derivingHandlers ← derivingHandlersRef.get
+    let derivingHandlers := derivingHandlers.filter (fun nm _ => nm != ``SizeOf)
+    for (cls, _) in derivingHandlers do
+      withoutModifyingEnv do
+        let hasExcl (kind : ExclusionKind) := (·.contains kind) <$> exclusions[cls]? |>.getD false
+        let s ← getThe Command.State
+        unless hasExcl .singleton do
+          Command.elabCommand (← `(structure B where deriving $(mkIdent cls):ident))
+        unless hasExcl .struct do
+          Command.elabCommand (← `(structure C where x : Nat deriving $(mkIdent cls):ident))
+        unless hasExcl .sum do
+          Command.elabCommand (← `(inductive D where | mk₁ : Bool → D | mk₂ : Bool → D deriving $(mkIdent cls):ident))
+        let msgs := (← getThe Command.State).messages.unreported
+        set s
+        if msgs.any (·.severity == .error) then
+          modify fun s => s.push (cls, msgs)
+  let (_, failures) ← go.run #[]
+  for (cls, msgs) in failures do
+    let msgs := MessageData.joinSep (msgs.map (·.data)).toList "\n\n"
+    logError m!"Handler for class `{cls}` failed with errors:\n{msgs}"