diff --git a/RELEASES.md b/RELEASES.md
index 2e03f7e51e9d..cb62720247e4 100644
--- a/RELEASES.md
+++ b/RELEASES.md
@@ -57,6 +57,15 @@ v4.8.0 (development in progress)
   ```
   is recognized without having to say `termination_by arr.size - i`.
 
+* Shorter instances names. There is a new algorithm for generating names for anonymous instances.
+  Across Std and Mathlib, the median ratio between lengths of new names and of old names is about 72%.
+  With the old algorithm, the longest name was 1660 characters, and now the longest name is 202 characters.
+  The new algorithm's 95th percentile name length is 67 characters, versus 278 for the old algorithm.
+  While the new algorithm produces names that are 1.2% less unique,
+  it avoids cross-project collisions by adding a module-based suffix
+  when it does not refer to declarations from the same "project" (modules that share the same root).
+  PR [#3089](https://github.com/leanprover/lean4/pull/3089).
+
 * Attribute `@[pp_using_anonymous_constructor]` to make structures pretty print like `⟨x, y, z⟩`
   rather than `{a := x, b := y, c := z}`.
   This attribute is applied to `Sigma`, `PSigma`, `PProd`, `Subtype`, `And`, and `Fin`.
@@ -121,6 +130,8 @@ fact.def :
 
 * The `Subarray` fields `as`, `h₁` and `h₂` have been renamed to `array`, `start_le_stop`, and `stop_le_array_size`, respectively. This more closely follows standard Lean conventions. Deprecated aliases for the field projections were added; these will be removed in a future release.
 
+* The change to the instance name algorithm (described above) can break projects that made use of the auto-generated names.
+
 v4.7.0
 ---------
 
diff --git a/src/Init/Control/Lawful/Instances.lean b/src/Init/Control/Lawful/Instances.lean
index 80a0710892c1..f662c4c55f3a 100644
--- a/src/Init/Control/Lawful/Instances.lean
+++ b/src/Init/Control/Lawful/Instances.lean
@@ -235,13 +235,13 @@ end StateT
 
 instance : LawfulMonad (EStateM ε σ) := .mk'
   (id_map := fun x => funext <| fun s => by
-    dsimp only [EStateM.instMonadEStateM, EStateM.map]
+    dsimp only [EStateM.instMonad, EStateM.map]
     match x s with
     | .ok _ _ => rfl
     | .error _ _ => rfl)
   (pure_bind := fun _ _ => rfl)
   (bind_assoc := fun x _ _ => funext <| fun s => by
-    dsimp only [EStateM.instMonadEStateM, EStateM.bind]
+    dsimp only [EStateM.instMonad, EStateM.bind]
     match x s with
     | .ok _ _ => rfl
     | .error _ _ => rfl)
diff --git a/src/Init/Data/Int/Basic.lean b/src/Init/Data/Int/Basic.lean
index 390a646594bd..ba8d16de2966 100644
--- a/src/Init/Data/Int/Basic.lean
+++ b/src/Init/Data/Int/Basic.lean
@@ -100,7 +100,7 @@ protected def neg (n : @& Int) : Int :=
   ```
 -/
 @[default_instance mid]
-instance : Neg Int where
+instance instNegInt : Neg Int where
   neg := Int.neg
 
 /-- Subtraction of two natural numbers. -/
@@ -173,13 +173,13 @@ inductive NonNeg : Int → Prop where
 /-- Definition of `a ≤ b`, encoded as `b - a ≥ 0`. -/
 protected def le (a b : Int) : Prop := NonNeg (b - a)
 
-instance : LE Int where
+instance instLEInt : LE Int where
   le := Int.le
 
 /-- Definition of `a < b`, encoded as `a + 1 ≤ b`. -/
 protected def lt (a b : Int) : Prop := (a + 1) ≤ b
 
-instance : LT Int where
+instance instLTInt : LT Int where
   lt := Int.lt
 
 set_option bootstrap.genMatcherCode false in
diff --git a/src/Init/Data/Nat/Div.lean b/src/Init/Data/Nat/Div.lean
index 9407c4284507..8bd98b8d5215 100644
--- a/src/Init/Data/Nat/Div.lean
+++ b/src/Init/Data/Nat/Div.lean
@@ -28,7 +28,7 @@ protected def div (x y : @& Nat) : Nat :=
     0
 decreasing_by apply div_rec_lemma; assumption
 
-instance : Div Nat := ⟨Nat.div⟩
+instance instDiv : Div Nat := ⟨Nat.div⟩
 
 theorem div_eq (x y : Nat) : x / y = if 0 < y ∧ y ≤ x then (x - y) / y + 1 else 0 := by
   show Nat.div x y = _
@@ -90,7 +90,7 @@ protected def mod : @& Nat → @& Nat → Nat
   | 0, _ => 0
   | x@(_ + 1), y => Nat.modCore x y
 
-instance : Mod Nat := ⟨Nat.mod⟩
+instance instMod : Mod Nat := ⟨Nat.mod⟩
 
 protected theorem modCore_eq_mod (x y : Nat) : Nat.modCore x y = x % y := by
   cases x with
diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index 9dd83028f3f8..8d3354fc0338 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -1098,7 +1098,7 @@ class OfNat (α : Type u) (_ : Nat) where
   ofNat : α
 
 @[default_instance 100] /- low prio -/
-instance (n : Nat) : OfNat Nat n where
+instance instOfNatNat (n : Nat) : OfNat Nat n where
   ofNat := n
 
 /-- `LE α` is the typeclass which supports the notation `x ≤ y` where `x y : α`.-/
@@ -1432,31 +1432,31 @@ class ShiftRight (α : Type u) where
   shiftRight : α → α → α
 
 @[default_instance]
-instance [Add α] : HAdd α α α where
+instance instHAdd [Add α] : HAdd α α α where
   hAdd a b := Add.add a b
 
 @[default_instance]
-instance [Sub α] : HSub α α α where
+instance instHSub [Sub α] : HSub α α α where
   hSub a b := Sub.sub a b
 
 @[default_instance]
-instance [Mul α] : HMul α α α where
+instance instHMul [Mul α] : HMul α α α where
   hMul a b := Mul.mul a b
 
 @[default_instance]
-instance [Div α] : HDiv α α α where
+instance instHDiv [Div α] : HDiv α α α where
   hDiv a b := Div.div a b
 
 @[default_instance]
-instance [Mod α] : HMod α α α where
+instance instHMod [Mod α] : HMod α α α where
   hMod a b := Mod.mod a b
 
 @[default_instance]
-instance [Pow α β] : HPow α β α where
+instance instHPow [Pow α β] : HPow α β α where
   hPow a b := Pow.pow a b
 
 @[default_instance]
-instance [NatPow α] : Pow α Nat where
+instance instPowNat [NatPow α] : Pow α Nat where
   pow a n := NatPow.pow a n
 
 @[default_instance]
@@ -1523,7 +1523,7 @@ protected def Nat.add : (@& Nat) → (@& Nat) → Nat
   | a, Nat.zero   => a
   | a, Nat.succ b => Nat.succ (Nat.add a b)
 
-instance : Add Nat where
+instance instAddNat : Add Nat where
   add := Nat.add
 
 /- We mark the following definitions as pattern to make sure they can be used in recursive equations,
@@ -1543,7 +1543,7 @@ protected def Nat.mul : (@& Nat) → (@& Nat) → Nat
   | _, 0          => 0
   | a, Nat.succ b => Nat.add (Nat.mul a b) a
 
-instance : Mul Nat where
+instance instMulNat : Mul Nat where
   mul := Nat.mul
 
 set_option bootstrap.genMatcherCode false in
@@ -1559,7 +1559,7 @@ protected def Nat.pow (m : @& Nat) : (@& Nat) → Nat
   | 0      => 1
   | succ n => Nat.mul (Nat.pow m n) m
 
-instance : NatPow Nat := ⟨Nat.pow⟩
+instance instNatPowNat : NatPow Nat := ⟨Nat.pow⟩
 
 set_option bootstrap.genMatcherCode false in
 /--
@@ -1636,14 +1636,14 @@ protected inductive Nat.le (n : Nat) : Nat → Prop
   /-- If `n ≤ m`, then `n ≤ m + 1`. -/
   | step {m} : Nat.le n m → Nat.le n (succ m)
 
-instance : LE Nat where
+instance instLENat : LE Nat where
   le := Nat.le
 
 /-- The strict less than relation on natural numbers is defined as `n < m := n + 1 ≤ m`. -/
 protected def Nat.lt (n m : Nat) : Prop :=
   Nat.le (succ n) m
 
-instance : LT Nat where
+instance instLTNat : LT Nat where
   lt := Nat.lt
 
 theorem Nat.not_succ_le_zero : ∀ (n : Nat), LE.le (succ n) 0 → False
@@ -1795,7 +1795,7 @@ protected def Nat.sub : (@& Nat) → (@& Nat) → Nat
   | a, 0      => a
   | a, succ b => pred (Nat.sub a b)
 
-instance : Sub Nat where
+instance instSubNat : Sub Nat where
   sub := Nat.sub
 
 /--
@@ -3361,7 +3361,7 @@ protected def seqRight (x : EStateM ε σ α) (y : Unit → EStateM ε σ β) :
   | Result.error e s => Result.error e s
 
 @[always_inline]
-instance : Monad (EStateM ε σ) where
+instance instMonad : Monad (EStateM ε σ) where
   bind     := EStateM.bind
   pure     := EStateM.pure
   map      := EStateM.map
diff --git a/src/Init/System/IO.lean b/src/Init/System/IO.lean
index bad54a3f4dbd..4a3d0c5bce8b 100644
--- a/src/Init/System/IO.lean
+++ b/src/Init/System/IO.lean
@@ -802,7 +802,7 @@ class Eval (α : Type u) where
   -- We take `Unit → α` instead of `α` because ‵α` may contain effectful debugging primitives (e.g., `dbg_trace`)
   eval : (Unit → α) → (hideUnit : Bool := true) → IO Unit
 
-instance [ToString α] : Eval α where
+instance instEval [ToString α] : Eval α where
   eval a _ := IO.println (toString (a ()))
 
 instance [Repr α] : Eval α where
diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index cebd8e4c00a5..d0071714ac0c 100644
--- a/src/Lean/Elab/Command.lean
+++ b/src/Lean/Elab/Command.lean
@@ -30,7 +30,6 @@ structure State where
   scopes         : List Scope := [{ header := "" }]
   nextMacroScope : Nat := firstFrontendMacroScope + 1
   maxRecDepth    : Nat
-  nextInstIdx    : Nat := 1 -- for generating anonymous instance names
   ngen           : NameGenerator := {}
   infoState      : InfoState := {}
   traceState     : TraceState := {}
diff --git a/src/Lean/Elab/DeclNameGen.lean b/src/Lean/Elab/DeclNameGen.lean
new file mode 100644
index 000000000000..8d94e6435323
--- /dev/null
+++ b/src/Lean/Elab/DeclNameGen.lean
@@ -0,0 +1,254 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kyle Miller
+-/
+prelude
+import Lean.Elab.Command
+
+/-!
+# Name generator for declarations
+
+This module provides functionality to generate a name for a declaration using its binders and its type.
+This is used to generate names for anonymous instances.
+
+It uses heuristics to generate an informative but terse name given its namespace, supplied binders, and type.
+It tries to make these relatively unique,
+and it uses suffixes derived from the module to ensure cross-project uniqueness
+when the instance doesn't refer to anything defined in the current project.
+
+The name generator can be thought of as a kind of pretty printer, rendering an expression in textual form.
+The general structure of this generator is
+1. `Lean.Elab.Command.NameGen.winnowExpr` takes an expression and re-uses `Expr` as a data structure
+   to record the "Syntax"-like structure.
+2. `Lean.Elab.Command.NameGen.mkBaseNameCore` formats the result of that as a string.
+   It actually does a bit more computation than that, since it further removes duplicate expressions,
+   reporting only the first occurrence of each subexpression.
+-/
+
+namespace Lean.Elab.Command
+
+open Meta
+
+namespace NameGen
+
+/--
+If `e` is an application of a projection to a parent structure, returns the term being projected.
+-/
+private def getParentProjArg (e : Expr) : MetaM (Option Expr) := do
+  let .const c@(.str _ field) _ := e.getAppFn | return none
+  let env ← getEnv
+  let some info := env.getProjectionFnInfo? c | return none
+  unless e.getAppNumArgs == info.numParams + 1 do return none
+  let some (.ctorInfo cVal) := env.find? info.ctorName | return none
+  if isSubobjectField? env cVal.induct (Name.mkSimple field) |>.isNone then return none
+  return e.appArg!
+
+/--
+Strips out universes and arguments we decide are unnecessary for naming.
+The resulting expression can have loose fvars and be mangled in other ways.
+Expressions can also be replaced by `.bvar 0` if they shouldn't be mentioned.
+-/
+private partial def winnowExpr (e : Expr) : MetaM Expr := do
+  let rec visit (e : Expr) : MonadCacheT Expr Expr MetaM Expr := checkCache e fun _ => do
+    match e with
+    | .app .. =>
+      if let some e' ← getParentProjArg e then
+        return (← visit e')
+      e.withApp fun f args => do
+        -- Visit only the explicit arguments to `f` and also its type (and type family) arguments.
+        -- The reason we visit type arguments is so that, for example, `Decidable (_ < _)` has
+        -- a chance to insert type information. Type families are for reporting things such as type constructors and monads.
+        let mut fty ← inferType f
+        let mut j := 0
+        let mut e' ← visit f
+        for i in [0:args.size] do
+          unless fty.isForall do
+            fty ← withTransparency .all <| whnf <| fty.instantiateRevRange j i args
+            j := i
+          let .forallE _ _ fty' bi := fty | failure
+          fty := fty'
+          let arg := args[i]!
+          if ← pure bi.isExplicit <||> (pure !arg.isSort <&&> isTypeFormer arg) then
+            unless (← isProof arg) do
+              e' := .app e' (← visit arg)
+        return e'
+    | .forallE n ty body bi =>
+      withLocalDecl n bi ty fun arg => do
+        -- In a dependent forall the body implies `ty`, so we won't mention it.
+        let ty' ← if body.hasLooseBVars then pure (.bvar 0) else visit ty
+        return .forallE n ty' (← visit (body.instantiate1 arg)) bi
+    | .lam n ty body bi =>
+      if let some e := Expr.etaExpandedStrict? e then
+        visit e
+      else
+        withLocalDecl n bi ty fun arg => do
+          -- Don't record the `.lam` since `ty` should be recorded elsewhere in the expression.
+          visit (body.instantiate1 arg)
+    | .letE _n _t v b _ => visit (b.instantiate1 v)
+    | .sort .. =>
+      if e.isProp then return .sort levelZero
+      else if e.isType then return .sort levelOne
+      else return .sort (.param `u)
+    | .const name .. => return .const name []
+    | .mdata _ e' => visit e'
+    | _ => return .bvar 0
+  visit e |>.run
+
+/--
+State for name generation.
+-/
+private structure MkNameState where
+  /-- Keeps track of expressions already visited so that we do not include them again. -/
+  seen : ExprSet := {}
+  /-- Keeps track of constants that appear in the generated name. -/
+  consts : NameSet := {}
+
+/--
+Monad for name generation.
+-/
+private abbrev MkNameM := StateRefT MkNameState MetaM
+
+/--
+Core algorithm for generating a name. The provided expression should be a winnowed expression.
+
+- `omitTopForall` if true causes "Forall" to not be included if the binding type results in an empty string.
+-/
+private def mkBaseNameCore (e : Expr) (omitTopForall : Bool := false) : MkNameM String :=
+  visit e omitTopForall
+where
+  visit (e : Expr) (omitTopForall : Bool := false) : MkNameM String := do
+    if (← get).seen.contains e then
+      return ""
+    else
+      let s ← visit' e omitTopForall
+      modify fun st => {st with seen := st.seen.insert e}
+      return s
+  visit' (e : Expr) (omitTopForall : Bool) : MkNameM String := do
+    match e with
+    | .const name .. =>
+      modify (fun st => {st with consts := st.consts.insert name})
+      return match name.eraseMacroScopes with
+              | .str _ str => str.capitalize
+              | _ => ""
+    | .app f x => (· ++ ·) <$> visit f <*> visit x
+    | .forallE _ ty body _ =>
+      let sty ← visit ty
+      if omitTopForall && sty == "" then
+        visit body true
+      else
+        ("Forall" ++ sty ++ ·) <$> visit body
+    | .sort .zero => return "Prop"
+    | .sort (.succ _) => return "Type"
+    | .sort _ => return "Sort"
+    | _ => return ""
+
+/--
+Generate a name, while naming the top-level foralls using "Of".
+The provided expression should be a winnowed expression.
+-/
+private partial def mkBaseNameAux (e : Expr) : MkNameM String := do
+  let (foralls, sb) ← visit e
+  return sb ++ String.join foralls
+where
+  visit (e : Expr) : MkNameM (List String × String) := do
+    match e with
+    | .forallE _ ty body _ =>
+      let (foralls, sb) ← visit body
+      let st ← mkBaseNameCore ty (omitTopForall := true)
+      if st == "" then
+        return (foralls, sb)
+      else
+        return (("Of" ++ st) :: foralls, sb)
+    | _ => return ([], ← mkBaseNameCore e)
+
+/--
+Adds all prefixes of `ns` as seen constants.
+-/
+private def visitNamespace (ns : Name) : MkNameM Unit := do
+  match ns with
+  | .anonymous => pure ()
+  | .num ns' _ => visitNamespace ns'
+  | .str ns' _ =>
+    let env ← getEnv
+    if env.contains ns then
+      modify fun st => {st with seen := st.seen.insert (.const ns []), consts := st.consts.insert ns}
+    visitNamespace ns'
+
+/--
+Given an expression, generates a "base name" for a declaration.
+The top-level foralls in `e` are treated as being binders, so use the `...Of...` naming convention.
+The current namespace is used to seed the seen expressions with each prefix of the namespace that's a global constant.
+
+Collects all constants that contribute to the name in the `MkInstM` state.
+This can be used to decide whether to further transform the generated name;
+in particular, this enables checking whether the generated name mentions declarations
+from the current module or project.
+-/
+def mkBaseName (e : Expr) : MkNameM String := do
+  let e ← instantiateMVars e
+  visitNamespace (← getCurrNamespace)
+  mkBaseNameAux (← winnowExpr e)
+
+/--
+Converts a module name into a suffix. Includes a leading `_`,
+so for example `Lean.Elab.DefView` becomes `_lean_elab_defView`.
+-/
+private def moduleToSuffix : Name → String
+  | .anonymous => ""
+  | .num n _ => moduleToSuffix n
+  | .str n s => moduleToSuffix n ++ "_" ++ s.decapitalize
+
+/--
+Uses heuristics to generate an informative but terse base name for a term of the given type, using `mkBaseName`.
+Makes use of the current namespace.
+It tries to make these names relatively unique ecosystem-wide,
+and it adds suffixes using the current module if the resulting name doesn't refer to anything defined in this module.
+-/
+def mkBaseNameWithSuffix (pre : String) (type : Expr) : MetaM String := do
+  let (name, st) ← mkBaseName type |>.run {}
+  let name := pre ++ name
+  let project := (← getMainModule).getRoot
+  -- Collect the modules for each constant that appeared.
+  let modules ← st.consts.foldM (init := Array.mkEmpty st.consts.size) fun mods name => return mods.push (← findModuleOf? name)
+  -- We can avoid adding the suffix if the instance refers to module-local names.
+  let isModuleLocal := modules.any Option.isNone
+  -- We can also avoid adding the full module suffix if the instance refers to "project"-local names.
+  let isProjectLocal := isModuleLocal || modules.any fun mod? => mod?.map (·.getRoot) == project
+  if !isProjectLocal then
+    return s!"{name}{moduleToSuffix project}"
+  else
+    return name
+
+/--
+Elaborates the binders and type and then uses `mkBaseNameWithSuffix` to generate a name.
+Furthermore, uses `mkUnusedBaseName` on the result.
+-/
+def mkBaseNameWithSuffix' (pre : String) (binders : Array Syntax) (type : Syntax) : TermElabM Name := do
+  let name ←
+    try
+      Term.withAutoBoundImplicit <| Term.elabBinders binders fun binds => Term.withoutErrToSorry do
+        let ty ← mkForallFVars binds (← Term.elabType type)
+        mkBaseNameWithSuffix pre ty
+    catch _ =>
+      pure pre
+  liftMacroM <| mkUnusedBaseName <| Name.mkSimple name
+
+end NameGen
+
+/--
+Generates an instance name for a declaration that has the given binders and type.
+It tries to make these names relatively unique ecosystem-wide.
+
+Note that this elaborates the binders and the type.
+This means that when elaborating an instance declaration, we elaborate these twice.
+-/
+def mkInstanceName (binders : Array Syntax) (type : Syntax) : CommandElabM Name := do
+  let savedState ← get
+  try
+    -- Unfortunately we can't include any of the binders from `runTermElabM` since, without
+    -- elaborating the body of the instance, we have no idea which of these binders are
+    -- actually used.
+    runTermElabM fun _ => NameGen.mkBaseNameWithSuffix' "inst" binders type
+  finally
+    set savedState
diff --git a/src/Lean/Elab/DeclUtil.lean b/src/Lean/Elab/DeclUtil.lean
index 9b5025ad41e3..e62d3513bcc2 100644
--- a/src/Lean/Elab/DeclUtil.lean
+++ b/src/Lean/Elab/DeclUtil.lean
@@ -54,14 +54,6 @@ def expandDeclSig (stx : Syntax) : Syntax × Syntax :=
   let typeSpec := stx[1]
   (binders, typeSpec[1])
 
-def mkFreshInstanceName (env : Environment) (nextIdx : Nat) : Name :=
-  (env.mainModule ++ `_instance).appendIndexAfter nextIdx
-
-def isFreshInstanceName (name : Name) : Bool :=
-  match name with
-  | .str _ s => "_instance".isPrefixOf s
-  | _        => false
-
 /--
   Sort the given list of `usedParams` using the following order:
   - If it is an explicit level `allUserParams`, then use user given order.
diff --git a/src/Lean/Elab/DefView.lean b/src/Lean/Elab/DefView.lean
index 1ac40b2bfd3f..091e3a3f3c74 100644
--- a/src/Lean/Elab/DefView.lean
+++ b/src/Lean/Elab/DefView.lean
@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Sebastian Ullrich
 -/
 prelude
-import Lean.Meta.ForEachExpr
 import Lean.Elab.Command
+import Lean.Elab.DeclNameGen
 import Lean.Elab.DeclUtil
 
 namespace Lean.Elab
@@ -66,41 +66,6 @@ def mkDefViewOfTheorem (modifiers : Modifiers) (stx : Syntax) : DefView :=
   { ref := stx, kind := DefKind.theorem, modifiers,
     declId := stx[1], binders, type? := some type, value := stx[3] }
 
-def mkFreshInstanceName : CommandElabM Name := do
-  let s ← get
-  let idx := s.nextInstIdx
-  modify fun s => { s with nextInstIdx := s.nextInstIdx + 1 }
-  return Lean.Elab.mkFreshInstanceName s.env idx
-
-/--
-  Generate a name for an instance with the given type.
-  Note that we elaborate the type twice. Once for producing the name, and another when elaborating the declaration. -/
-def mkInstanceName (binders : Array Syntax) (type : Syntax) : CommandElabM Name := do
-  let savedState ← get
-  try
-    let result ← runTermElabM fun _ => Term.withAutoBoundImplicit <| Term.elabBinders binders fun _ => Term.withoutErrToSorry do
-      let type ← instantiateMVars (← Term.elabType type)
-      let ref ← IO.mkRef ""
-      Meta.forEachExpr type fun e => do
-        if e.isForall then ref.modify (· ++ "ForAll")
-        else if e.isProp then ref.modify (· ++ "Prop")
-        else if e.isType then ref.modify (· ++ "Type")
-        else if e.isSort then ref.modify (· ++ "Sort")
-        else if e.isConst then
-          match e.constName!.eraseMacroScopes with
-          | .str _ str =>
-              if str.front.isLower then
-                ref.modify (· ++ str.capitalize)
-              else
-                ref.modify (· ++ str)
-          | _ => pure ()
-      ref.get
-    set savedState
-    liftMacroM <| mkUnusedBaseName <| Name.mkSimple ("inst" ++ result)
-  catch _ =>
-    set savedState
-    mkFreshInstanceName
-
 def mkDefViewOfInstance (modifiers : Modifiers) (stx : Syntax) : CommandElabM DefView := do
   -- leading_parser Term.attrKind >> "instance " >> optNamedPrio >> optional declId >> declSig >> declVal
   let attrKind        ← liftMacroM <| toAttributeKind stx[0]
@@ -109,9 +74,14 @@ def mkDefViewOfInstance (modifiers : Modifiers) (stx : Syntax) : CommandElabM De
   let (binders, type) := expandDeclSig stx[4]
   let modifiers       := modifiers.addAttribute { kind := attrKind, name := `instance, stx := attrStx }
   let declId ← match stx[3].getOptional? with
-    | some declId => pure declId
+    | some declId =>
+      if ← isTracingEnabledFor `Elab.instance.mkInstanceName then
+        let id ← mkInstanceName binders.getArgs type
+        trace[Elab.instance.mkInstanceName] "generated {(← getCurrNamespace) ++ id} for {declId}"
+      pure declId
     | none        =>
       let id ← mkInstanceName binders.getArgs type
+      trace[Elab.instance.mkInstanceName] "generated {(← getCurrNamespace) ++ id}"
       pure <| mkNode ``Parser.Command.declId #[mkIdentFrom stx id, mkNullNode]
   return {
     ref := stx, kind := DefKind.def, modifiers := modifiers,
@@ -166,6 +136,7 @@ def mkDefView (modifiers : Modifiers) (stx : Syntax) : CommandElabM DefView :=
     throwError "unexpected kind of definition"
 
 builtin_initialize registerTraceClass `Elab.definition
+builtin_initialize registerTraceClass `Elab.instance.mkInstanceName
 
 end Command
 end Lean.Elab
diff --git a/src/Lean/Elab/PreDefinition/Basic.lean b/src/Lean/Elab/PreDefinition/Basic.lean
index 7e86071fa255..0963d017d455 100644
--- a/src/Lean/Elab/PreDefinition/Basic.lean
+++ b/src/Lean/Elab/PreDefinition/Basic.lean
@@ -7,6 +7,7 @@ prelude
 import Lean.Compiler.NoncomputableAttr
 import Lean.Util.CollectLevelParams
 import Lean.Meta.AbstractNestedProofs
+import Lean.Meta.ForEachExpr
 import Lean.Elab.RecAppSyntax
 import Lean.Elab.DefView
 import Lean.Elab.PreDefinition.WF.TerminationHint
diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean
index 96e610de3a1a..c2dd647c6d2a 100644
--- a/src/Lean/Expr.lean
+++ b/src/Lean/Expr.lean
@@ -2025,43 +2025,43 @@ def mkIff (p q : Expr) : Expr := mkApp2 (mkConst ``Iff) p q
 /-! Constants for Nat typeclasses. -/
 namespace Nat
 
-def natType : Expr := mkConst ``Nat
+protected def mkType : Expr := mkConst ``Nat
 
-def instAdd : Expr := mkConst ``instAddNat
-def instHAdd : Expr := mkApp2 (mkConst ``instHAdd [levelZero]) natType instAdd
+def mkInstAdd : Expr := mkConst ``instAddNat
+def mkInstHAdd : Expr := mkApp2 (mkConst ``instHAdd [levelZero]) Nat.mkType mkInstAdd
 
-def instSub : Expr := mkConst ``instSubNat
-def instHSub : Expr := mkApp2 (mkConst ``instHSub [levelZero]) natType instSub
+def mkInstSub : Expr := mkConst ``instSubNat
+def mkInstHSub : Expr := mkApp2 (mkConst ``instHSub [levelZero]) Nat.mkType mkInstSub
 
-def instMul : Expr := mkConst ``instMulNat
-def instHMul : Expr := mkApp2 (mkConst ``instHMul [levelZero]) natType instMul
+def mkInstMul : Expr := mkConst ``instMulNat
+def mkInstHMul : Expr := mkApp2 (mkConst ``instHMul [levelZero]) Nat.mkType mkInstMul
 
-def instDiv : Expr := mkConst ``Nat.instDivNat
-def instHDiv : Expr := mkApp2 (mkConst ``instHDiv [levelZero]) natType instDiv
+def mkInstDiv : Expr := mkConst ``Nat.instDiv
+def mkInstHDiv : Expr := mkApp2 (mkConst ``instHDiv [levelZero]) Nat.mkType mkInstDiv
 
-def instMod : Expr := mkConst ``Nat.instModNat
-def instHMod : Expr := mkApp2 (mkConst ``instHMod [levelZero]) natType instMod
+def mkInstMod : Expr := mkConst ``Nat.instMod
+def mkInstHMod : Expr := mkApp2 (mkConst ``instHMod [levelZero]) Nat.mkType mkInstMod
 
-def instNatPow : Expr := mkConst ``instNatPowNat
-def instPow  : Expr := mkApp2 (mkConst ``instPowNat [levelZero]) natType instNatPow
-def instHPow : Expr := mkApp3 (mkConst ``instHPow [levelZero, levelZero]) natType natType instPow
+def mkInstNatPow : Expr := mkConst ``instNatPowNat
+def mkInstPow  : Expr := mkApp2 (mkConst ``instPowNat [levelZero]) Nat.mkType mkInstNatPow
+def mkInstHPow : Expr := mkApp3 (mkConst ``instHPow [levelZero, levelZero]) Nat.mkType Nat.mkType mkInstPow
 
-def instLT : Expr := mkConst ``instLTNat
-def instLE : Expr := mkConst ``instLENat
+def mkInstLT : Expr := mkConst ``instLTNat
+def mkInstLE : Expr := mkConst ``instLENat
 
 end Nat
 
 private def natAddFn : Expr :=
   let nat := mkConst ``Nat
-  mkApp4 (mkConst ``HAdd.hAdd [0, 0, 0]) nat nat nat Nat.instHAdd
+  mkApp4 (mkConst ``HAdd.hAdd [0, 0, 0]) nat nat nat Nat.mkInstHAdd
 
 private def natSubFn : Expr :=
   let nat := mkConst ``Nat
-  mkApp4 (mkConst ``HSub.hSub [0, 0, 0]) nat nat nat Nat.instHSub
+  mkApp4 (mkConst ``HSub.hSub [0, 0, 0]) nat nat nat Nat.mkInstHSub
 
 private def natMulFn : Expr :=
   let nat := mkConst ``Nat
-  mkApp4 (mkConst ``HMul.hMul [0, 0, 0]) nat nat nat Nat.instHMul
+  mkApp4 (mkConst ``HMul.hMul [0, 0, 0]) nat nat nat Nat.mkInstHMul
 
 /-- Given `a : Nat`, returns `Nat.succ a` -/
 def mkNatSucc (a : Expr) : Expr :=
@@ -2080,7 +2080,7 @@ def mkNatMul (a b : Expr) : Expr :=
   mkApp2 natMulFn a b
 
 private def natLEPred : Expr :=
-  mkApp2 (mkConst ``LE.le [0]) (mkConst ``Nat) Nat.instLE
+  mkApp2 (mkConst ``LE.le [0]) (mkConst ``Nat) Nat.mkInstLE
 
 /-- Given `a b : Nat`, return `a ≤ b` -/
 def mkNatLE (a b : Expr) : Expr :=
diff --git a/src/Lean/Meta/NatInstTesters.lean b/src/Lean/Meta/NatInstTesters.lean
index ee4b81d3c459..028894bb3fb2 100644
--- a/src/Lean/Meta/NatInstTesters.lean
+++ b/src/Lean/Meta/NatInstTesters.lean
@@ -24,10 +24,10 @@ def isInstMulNat (e : Expr) : MetaM Bool := do
   let_expr instMulNat ← e | return false
   return true
 def isInstDivNat (e : Expr) : MetaM Bool := do
-  let_expr Nat.instDivNat ← e | return false
+  let_expr Nat.instDiv ← e | return false
   return true
 def isInstModNat (e : Expr) : MetaM Bool := do
-  let_expr Nat.instModNat ← e | return false
+  let_expr Nat.instMod ← e | return false
   return true
 def isInstNatPowNat (e : Expr) : MetaM Bool := do
   let_expr instNatPowNat ← e | return false
diff --git a/src/Lean/Meta/Offset.lean b/src/Lean/Meta/Offset.lean
index 9b125a1a1488..a4940982227f 100644
--- a/src/Lean/Meta/Offset.lean
+++ b/src/Lean/Meta/Offset.lean
@@ -87,8 +87,8 @@ partial def isOffset? (e : Expr) : OptionT MetaM (Expr × Nat) := do
     let (s, k) ← getOffset a
     return (s, k+1)
   | Nat.add a b => add a b
-  | Add.add _ i a b => guard (← matchesInstance i Nat.instAdd); add a b
-  | HAdd.hAdd _ _ _ i a b => guard (← matchesInstance i Nat.instHAdd); add a b
+  | Add.add _ i a b => guard (← matchesInstance i Nat.mkInstAdd); add a b
+  | HAdd.hAdd _ _ _ i a b => guard (← matchesInstance i Nat.mkInstHAdd); add a b
   | _ => failure
 
 end
diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean
index 27cef9d94ef6..f9f2c077768d 100644
--- a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean
+++ b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean
@@ -76,14 +76,14 @@ private inductive NatOffset where
 private partial def NatOffset.asOffset (e : Expr) : Meta.SimpM (Option (Expr × Nat)) := do
   if e.isAppOfArity ``HAdd.hAdd 6 then
     let inst := e.appFn!.appFn!.appArg!
-    unless ← matchesInstance inst Nat.instHAdd do return none
+    unless ← matchesInstance inst Nat.mkInstHAdd do return none
     let b := e.appFn!.appArg!
     let o := e.appArg!
     let some n ← Nat.fromExpr? o | return none
     pure (some (b, n))
   else if e.isAppOfArity ``Add.add 4 then
     let inst := e.appFn!.appFn!.appArg!
-    unless ← matchesInstance inst Nat.instAdd do return none
+    unless ← matchesInstance inst Nat.mkInstAdd do return none
     let b := e.appFn!.appArg!
     let some n ← Nat.fromExpr? e.appArg! | return none
     pure (some (b, n))
diff --git a/tests/lean/621.lean b/tests/lean/621.lean
index 40b9a4f411b3..1152cdf048a9 100644
--- a/tests/lean/621.lean
+++ b/tests/lean/621.lean
@@ -1,4 +1,4 @@
-instance (ϕ : α → Prop) : CoeSort (Subtype ϕ) α where
+instance inst621 (ϕ : α → Prop) : CoeSort (Subtype ϕ) α where
   coe := fun x => x.val
 
 example (ϕ : α → Prop) (xs : Subtype ϕ) (x : xs) : True := trivial
diff --git a/tests/lean/621.lean.expected.out b/tests/lean/621.lean.expected.out
index 9711895ddaff..837ce9d9f1f9 100644
--- a/tests/lean/621.lean.expected.out
+++ b/tests/lean/621.lean.expected.out
@@ -3,4 +3,4 @@
 to a type, after applying `CoeSort.coe`, result is still not a type
   xs.val
 this is often due to incorrect `CoeSort` instances, the synthesized instance was
-  instCoeSortSubtype ϕ
+  inst621 ϕ
diff --git a/tests/lean/755.lean.expected.out b/tests/lean/755.lean.expected.out
index 1124e5f70ae8..e36765b8705c 100644
--- a/tests/lean/755.lean.expected.out
+++ b/tests/lean/755.lean.expected.out
@@ -3,13 +3,13 @@
 has type
   0 = @OfNat.ofNat Nat 0 (instOfNatNat 0) : Prop
 but is expected to have type
-  0 = @OfNat.ofNat (Additive Nat) 0 instOfNatAdditive : Prop
+  0 = @OfNat.ofNat (Additive Nat) 0 instOfNatAdditiveOfOfNatNat : Prop
 755.lean:24:2-24:5: error: type mismatch
   rfl
 has type
   2 * 3 = @HMul.hMul Nat Nat Nat instHMul 2 3 : Prop
 but is expected to have type
-  2 * 3 = @HMul.hMul (Foo Nat) (Foo Nat) (Foo Nat) instHMulFoo 2 3 : Prop
+  2 * 3 = @HMul.hMul (Foo Nat) (Foo Nat) (Foo Nat) instHMulFooOfHAdd 2 3 : Prop
 755.lean:27:2-27:5: error: type mismatch
   rfl
 has type
@@ -21,4 +21,4 @@ but is expected to have type
 has type
   2 - 3 = @HSub.hSub Nat Nat Nat instHSub 2 3 : Prop
 but is expected to have type
-  2 - 3 = @HSub.hSub (Foo Nat) (Foo Nat) (Foo Nat) instHSubFoo 2 3 : Prop
+  2 - 3 = @HSub.hSub (Foo Nat) (Foo Nat) (Foo Nat) instHSubFooOfHAdd 2 3 : Prop
diff --git a/tests/lean/951.lean b/tests/lean/951.lean
index b107b0c87db5..37b3cc5a0deb 100644
--- a/tests/lean/951.lean
+++ b/tests/lean/951.lean
@@ -1,3 +1,7 @@
+/-!
+# Names of inferred instances clash (issue 951)
+-/
+
 inductive ThingA where
 | mkA
 deriving Ord
@@ -5,8 +9,7 @@ instance : LE ThingA where
   le a b := (compare a b).isLE
 
 instance (t₁ t₂ : ThingA) : Decidable (t₁ <= t₂) := inferInstance
--- TODO: we may want to suppress the name of nested instances
-#check instDecidableLeThingAInstLEThingA
+#check instDecidableLeThingA
 
 inductive ThingB where
 | mkB
@@ -14,4 +17,4 @@ deriving Ord
 instance : LE ThingB where
   le a b := (compare a b).isLE
 instance (t₁ t₂ : ThingB) : Decidable (t₁ <= t₂) := inferInstance
-#check instDecidableLeThingBInstLEThingB
+#check instDecidableLeThingB
diff --git a/tests/lean/951.lean.expected.out b/tests/lean/951.lean.expected.out
index 44c6d7ad2431..79fe685950c7 100644
--- a/tests/lean/951.lean.expected.out
+++ b/tests/lean/951.lean.expected.out
@@ -1,2 +1,2 @@
-instDecidableLeThingAInstLEThingA (t₁ t₂ : ThingA) : Decidable (t₁ ≤ t₂)
-instDecidableLeThingBInstLEThingB (t₁ t₂ : ThingB) : Decidable (t₁ ≤ t₂)
+instDecidableLeThingA (t₁ t₂ : ThingA) : Decidable (t₁ ≤ t₂)
+instDecidableLeThingB (t₁ t₂ : ThingB) : Decidable (t₁ ≤ t₂)
diff --git a/tests/lean/run/lcnf1.lean b/tests/lean/run/lcnf1.lean
index e487ca8c4f07..219f13acccb9 100644
--- a/tests/lean/run/lcnf1.lean
+++ b/tests/lean/run/lcnf1.lean
@@ -104,4 +104,4 @@ def gebner2 (x : UInt64) := x &&& ((1 : UInt64) <<< 5 : UInt64)
 #eval Compiler.compile #[``Lean.Core.instMonadCoreM]
 #eval Compiler.compile #[``instMonadEIO]
 -- set_option pp.explicit true in
-#eval Compiler.compile #[``EStateM.instMonadEStateM]
+#eval Compiler.compile #[``EStateM.instMonad]
diff --git a/tests/lean/run/regressions3210.lean b/tests/lean/run/regressions3210.lean
index 4ed0930f3bff..591c88d4f4b9 100644
--- a/tests/lean/run/regressions3210.lean
+++ b/tests/lean/run/regressions3210.lean
@@ -15,7 +15,7 @@ instance One.ofOfNat1 {α} [OfNat α (nat_lit 1)] : One α where
 
 example : Not
   (@Eq.{1} Nat
-    (@HMod.hMod.{0, 0, 0} Nat Nat Nat (@instHMod.{0} Nat Nat.instModNat)
+    (@HMod.hMod.{0, 0, 0} Nat Nat Nat (@instHMod.{0} Nat Nat.instMod)
       (@OfNat.ofNat.{0} Nat (nat_lit 1) (@One.toOfNat1.{0} Nat (@One.ofOfNat1.{0} Nat (instOfNatNat (nat_lit 1)))))
       (@OfNat.ofNat.{0} Nat (nat_lit 2) (instOfNatNat (nat_lit 2))))
     (@OfNat.ofNat.{0} Nat (nat_lit 0) (instOfNatNat (nat_lit 0)))) := by
@@ -23,7 +23,7 @@ example : Not
 
 example : Not
   (@Eq.{1} Nat
-    (@HMod.hMod.{0, 0, 0} Nat Nat Nat (@instHMod.{0} Nat Nat.instModNat)
+    (@HMod.hMod.{0, 0, 0} Nat Nat Nat (@instHMod.{0} Nat Nat.instMod)
       (@OfNat.ofNat.{0} Nat 1 (@One.toOfNat1.{0} Nat (@One.ofOfNat1.{0} Nat (instOfNatNat 1))))
       (@OfNat.ofNat.{0} Nat 2 (instOfNatNat 2)))
     (@OfNat.ofNat.{0} Nat 0 (instOfNatNat 0))) := by
diff --git a/tests/lean/run/structWithAlgTCSynth.lean b/tests/lean/run/structWithAlgTCSynth.lean
index 128e851f563c..df43eab4b6dd 100644
--- a/tests/lean/run/structWithAlgTCSynth.lean
+++ b/tests/lean/run/structWithAlgTCSynth.lean
@@ -1311,7 +1311,7 @@ instance : Semiring (Quot_r R M) :=
   RingQuot.instSemiring _
 
 instance {S : Type w} [CommRing S] : CommRing (Quot_r S M) :=
-  RingQuot.instCommRingRingQuotToSemiringToCommSemiring _
+  RingQuot.instCommRing _
 
 instance instAlgebra
     {R A M} [CommSemiring R] [CommRing A] [Algebra R A] :
diff --git a/tests/lean/synthorder.lean.expected.out b/tests/lean/synthorder.lean.expected.out
index d891c4ec711e..707c333edea2 100644
--- a/tests/lean/synthorder.lean.expected.out
+++ b/tests/lean/synthorder.lean.expected.out
@@ -18,7 +18,7 @@ all remaining arguments have metavariables:
       Four α β
       One β
       TwoHalf β
-[Meta.synthOrder] synthesizing the arguments of @instFour in the order [4, 2, 3]:
+[Meta.synthOrder] synthesizing the arguments of @instFourOfThree in the order [4, 2, 3]:
       Three α β
       One β
       TwoHalf β