fix: when constructing instance names, avoid private names (#11385)

This PR lets implicit instance names avoid name clashes with private
declarations. This fixes #10329.

Author: nomeata

src/Lean/Elab/Util.lean

@@ -186,7 +186,11 @@ def liftMacroM [Monad m] [MonadMacroAdapter m] [MonadEnv m] [MonadRecDepth m] [M
       match (← expandMacroImpl? env stx) with
       | some (_, stx?) => liftExcept stx?
       | none           => return none
-    hasDecl          := fun declName => return env.contains declName
+    hasDecl          := fun declName => do
+      -- this is used (by mkUnusedBaseName) to find available names, so check
+      -- for both private and public names
+      let env := env.setExporting false
+      return env.contains (mkPrivateName env declName) || env.contains (privateToUserName declName)
     getCurrNamespace := return currNamespace
     resolveNamespace := fun n => return ResolveName.resolveNamespace env currNamespace openDecls n
     resolveGlobalName := fun n => return ResolveName.resolveGlobalName env opts currNamespace openDecls n

tests/lean/run/issue10329.lean

@@ -0,0 +1,48 @@
+module
+
+set_option warn.sorry false
+
+public class X
+instance : X := sorry
+public instance : X := sorry
+instance : X := sorry
+
+namespace InNamespace
+public class Y
+instance : Y := sorry
+public instance : Y := sorry
+instance : Y := sorry
+end InNamespace
+
+
+inductive Day where
+  | mo | tu | we
+deriving Repr
+
+def Day.succ? : Day → Option Day
+  | mo => some tu
+  | tu => some we
+  | we => none
+
+instance : Std.PRange.UpwardEnumerable Day where
+  succ? := Day.succ?
+
+def Day.toNat : Day → Nat
+  | mo => 0
+  | tu => 1
+  | we => 2
+
+instance : LT Day where
+  lt _ _ := True
+
+instance : LE Day where
+  le _ _ := True
+
+instance : Std.Rxo.IsAlwaysFinite Day where
+  finite init hi := ⟨3, by sorry⟩
+
+instance : Std.Rxi.IsAlwaysFinite Day where
+  finite init := ⟨3, by sorry⟩
+
+instance : Std.Rxc.IsAlwaysFinite Day where
+  finite init hi := ⟨3, by sorry⟩