feat: shorten auto-generated instance names (#3089)

Implements a new method to generate instance names for anonymous
instances that uses a heuristic that tends to produce shorter names. A
design goal is to make them relatively unique within projects and
definitely unique across projects, while also using accessible names so
that they can be referred to as needed, both in Lean code and in
discussions.

The new method also takes into account binders provided to the instance,
and it adds project-based suffixes. Despite this, a median new name is
73% its original auto-generated length. (Compare: [old generated
names](https://gist.github.com/kmill/b72bb43f5b01dafef41eb1d2e57a8237)
and [new generated
names](https://gist.github.com/kmill/393acc82e7a8d67fc7387829f4ed547e).)

Some notes:
* The naming is sensitive to what is explicitly provided as a binder vs
what is provided via a `variable`. It does not make use of `variable`s
since, when names are generated, it is not yet known which variables are
used in the body of the instance.
* If the instance name refers to declarations in the current "project"
(given by the root module), then it does not add a suffix. Otherwise, it
adds the project name as a suffix to protect against cross-project
collisions.
* `set_option trace.Elab.instance.mkInstanceName true` can be used to
see what name the auto-generator would give, even if the instance
already has an explicit name.

There were a number of instances that were referred to explicitly in
meta code, and these have been given explicit names.

Removes the unused `Lean.Elab.mkFreshInstanceName` along with the
Command state's `nextInstIdx`.

Fixes #2343

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
 ---------
 

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)

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

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

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

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

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 := {}