From e9d65dd2de58648feeab49beba8ca643e1e8fcf3 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 17 Sep 2020 08:57:54 -0700
Subject: [PATCH] chore: improve `sanitizeNames` superscripts

cc @Kha
---
 src/Lean/LocalContext.lean          |  7 +++++--
 tests/lean/shadow.lean              |  2 +-
 tests/lean/shadow.lean.expected.out | 20 ++++++++++----------
 3 files changed, 16 insertions(+), 13 deletions(-)

diff --git a/src/Lean/LocalContext.lean b/src/Lean/LocalContext.lean
index a26ba3a528..0eb2a48f8b 100644
--- a/src/Lean/LocalContext.lean
+++ b/src/Lean/LocalContext.lean
@@ -373,7 +373,10 @@ Id.run $ lctx.allM p
 
 private def mkInaccessibleUserNameAux (unicode : Bool) (name : Name) (idx : Nat) : Name :=
 if unicode then
-  name.appendAfter ("✝" ++ idx.toSuperscriptString)
+  if idx == 0 then
+    name.appendAfter "✝"
+  else
+    name.appendAfter ("✝" ++ idx.toSuperscriptString)
 else
   name ++ mkNameNum "_inaccessible" idx
 
@@ -420,7 +423,7 @@ let (lctx, _, _) := lctx.decls.size.foldRev
       let userName := decl.userName;
       if userName.hasMacroScopes || usedNames.contains userName then
         let userName := userName.eraseMacroScopes;
-        let idx      := (usedName2Idx.find? userName).getD 1;
+        let idx      := (usedName2Idx.find? userName).getD 0;
         let (userNameNew, usedName2Idx) := mkFreshInaccessibleUserName unicode usedName2Idx userName idx;
         let lctx := lctx.setUserName decl.fvarId userNameNew;
         (lctx, usedNames, usedName2Idx)
diff --git a/tests/lean/shadow.lean b/tests/lean/shadow.lean
index 3ce6b26f2d..3628625f88 100644
--- a/tests/lean/shadow.lean
+++ b/tests/lean/shadow.lean
@@ -16,5 +16,5 @@ set_option pp.sanitizeNames false in
 def foo2 {α} [Inhabited α] (inst inst : α) : {β δ : Type} → α → β → δ → α × β × δ :=
 _
 
-def foo3 {α β} (inst : α) (b : β) (inst : α) [Inhabited α] : {β δ : Type} → α → β → δ → α × β × δ :=
+def foo3 {α β} (inst : α) (inst : β) (b : β) (inst : α) [Inhabited α] : {β δ : Type} → α → β → δ → α × β × δ :=
 _
diff --git a/tests/lean/shadow.lean.expected.out b/tests/lean/shadow.lean.expected.out
index c40ab4fffc..cfeba3d40e 100644
--- a/tests/lean/shadow.lean.expected.out
+++ b/tests/lean/shadow.lean.expected.out
@@ -1,11 +1,11 @@
 shadow.lean:6:0: error: type mismatch
   h
 has type
-  x✝¹ = x✝¹
+  x✝ = x✝
 but it is expected to have type
   x = x
 failed to synthesize instance
-  CoeT (x✝¹ = x✝¹) h (x = x)
+  CoeT (x✝ = x✝) h (x = x)
 shadow.lean:10:0: error: type mismatch
   h
 has type
@@ -17,10 +17,10 @@ failed to synthesize instance
 shadow.lean:13:0: error: don't know how to synthesize placeholder
 context:
 α : Type u_1
-inst✝² : Inhabited α
-inst✝¹ inst : α
-β✝¹ δ✝¹ : Type
-⊢ α → β✝¹ → δ✝¹ → α × β✝¹ × δ✝¹
+inst✝¹ : Inhabited α
+inst✝ inst : α
+β✝ δ✝ : Type
+⊢ α → β✝ → δ✝ → α × β✝ × δ✝
 shadow.lean:17:0: error: don't know how to synthesize placeholder
 context:
 α : Type u_1
@@ -33,8 +33,8 @@ context:
 α : Type u_1
 β : Sort u_2
 inst✝² : α
-b : β
+inst✝¹ b : β
 inst : α
-inst✝¹ : Inhabited α
-β✝¹ δ✝¹ : Type
-⊢ α → β✝¹ → δ✝¹ → α × β✝¹ × δ✝¹
+inst✝ : Inhabited α
+β✝ δ✝ : Type
+⊢ α → β✝ → δ✝ → α × β✝ × δ✝