feat: macro scope as the single mechanism for creating fresh names

cc @Kha

src/Lean/Elab/App.lean

@@ -62,7 +62,7 @@ match arg with
   ensureArgType f val expectedType
 
 private def mkArrow (d b : Expr) : TermElabM Expr := do
-n ← mkFreshAnonymousName;
+n ← mkFreshUserName;
 pure $ Lean.mkForall n BinderInfo.default d b
 
 /-

src/Lean/Elab/Binders.lean

@@ -26,7 +26,7 @@ else
 /-- Given syntax of the form `ident <|> hole`, return `ident`. If `hole`, then we create a new anonymous name. -/
 private def expandBinderIdent (stx : Syntax) : TermElabM Syntax :=
 match_syntax stx with
-| `(_) => mkFreshAnonymousIdent stx
+| `(_) => mkFreshIdent stx
 | _    => pure stx
 
 /-- Given syntax of the form `(ident >> " : ")?`, return `ident`, or a new instance name. -/
@@ -205,7 +205,7 @@ private partial def getFunBinderIdsAux? : Bool → Syntax → Array Syntax → T
      else do
        (some acc) ← getFunBinderIdsAux? false f acc | pure none;
        getFunBinderIdsAux? true a acc
-  | `(_) => do { ident ← mkFreshAnonymousIdent stx; pure (some (acc.push ident)) }
+  | `(_) => do { ident ← mkFreshIdent stx; pure (some (acc.push ident)) }
   | `($id:ident) => pure (some (acc.push id))
   | _ => pure none
 
@@ -225,7 +225,7 @@ private partial def expandFunBindersAux (binders : Array Syntax) : Syntax → Na
     let binder := binders.get ⟨i, h⟩;
     let processAsPattern : Unit → TermElabM (Array Syntax × Syntax × Bool) := fun _ => do {
       let pattern := binder;
-      major ← mkFreshAnonymousIdent binder;
+      major ← mkFreshIdent binder;
       (binders, newBody, _) ← expandFunBindersAux body (i+1) (newBinders.push $ mkExplicitBinder major (mkHole binder));
       newBody ← `(match $major:ident with | $pattern => $newBody);
       pure (binders, newBody, true)
@@ -235,7 +235,7 @@ private partial def expandFunBindersAux (binders : Array Syntax) : Syntax → Na
     | Syntax.node `Lean.Parser.Term.instBinder _     => expandFunBindersAux body (i+1) (newBinders.push binder)
     | Syntax.node `Lean.Parser.Term.explicitBinder _ => expandFunBindersAux body (i+1) (newBinders.push binder)
     | Syntax.node `Lean.Parser.Term.hole _ => do
-      ident ← mkFreshAnonymousIdent binder;
+      ident ← mkFreshIdent binder;
       let type := binder;
       expandFunBindersAux body (i+1) (newBinders.push $ mkExplicitBinder ident type)
     | Syntax.node `Lean.Parser.Term.paren args =>

src/Lean/Elab/Match.lean

@@ -70,7 +70,7 @@ elabDiscrsWitMatchTypeAux discrStxs expectedType 0 matchType #[]
 private def mkUserNameFor (e : Expr) : TermElabM Name :=
 match e with
 | Expr.fvar fvarId _ => do localDecl ← getLocalDecl fvarId; pure localDecl.userName
-| _ => withFreshMacroScope do x ← `(x); pure x.getId
+| _ => mkFreshUserName
 
 private def elabMatchTypeAndDiscrs (discrStxs : Array Syntax) (matchOptType : Syntax) (expectedType : Expr) : TermElabM (Array Expr × Expr) :=
 let numDiscrs := discrStxs.size;
@@ -495,7 +495,8 @@ private partial def withPatternVarsAux {α} (pVars : Array PatternVar) (k : Arra
     match pVars.get ⟨i, h⟩ with
     | PatternVar.anonymousVar mvarId => do
       type ← mkFreshTypeMVar;
-      withLocalDecl ((`_x).appendIndexAfter i) BinderInfo.default type fun x =>
+      userName ← mkFreshUserName;
+      withLocalDecl userName BinderInfo.default type fun x =>
         withPatternVarsAux (i+1) (decls.push (PatternVarDecl.anonymousVar mvarId x.fvarId!))
     | PatternVar.localVar userName   => do
       type ← mkFreshTypeMVar;
@@ -585,8 +586,7 @@ match val? with
   /- HACK: `fvarId` is not in the scope of `mvarId`
      If this generates problems in the future, we should update the metavariable declarations. -/
   assignExprMVar mvarId (mkFVar fvarId);
-  -- TODO: use macro scopes for creating userName
-  let userName := (`_x).appendIndexAfter (s.localDecls.size+1);
+  userName ← liftM $ mkFreshUserName;
   let newDecl := LocalDecl.cdecl (arbitrary _) fvarId userName type BinderInfo.default;
   modify $ fun s =>
     { s with

src/Lean/Elab/Term.lean

@@ -135,8 +135,6 @@ structure State :=
 (syntheticMVars    : List SyntheticMVarDecl := [])
 (mvarErrorContexts : List MVarErrorContext := [])
 (messages          : MessageLog := {})
-(instImplicitIdx   : Nat := 1)
-(anonymousIdx      : Nat := 1)
 (nextMacroScope    : Nat := firstFrontendMacroScope + 1)
 (letRecsToLift     : List LetRecToLift := [])
 
@@ -435,28 +433,25 @@ pure e
 /--
   Auxiliary method for creating fresh binder names.
   Do not confuse with the method for creating fresh free/meta variable ids. -/
-def mkFreshAnonymousName : TermElabM Name := do
-s ← get;
-let anonymousIdx := s.anonymousIdx;
-modify $ fun s => { s with anonymousIdx := s.anonymousIdx + 1 };
-pure $ (`_a).appendIndexAfter anonymousIdx
+def mkFreshUserName : TermElabM Name :=
+withFreshMacroScope do
+  x ← `(x);
+  pure x.getId
 
 /--
   Auxiliary method for creating a `Syntax.ident` containing
   a fresh name. This method is intended for creating fresh binder names.
-  It is just a thin layer on top of `mkFreshAnonymousName`. -/
-def mkFreshAnonymousIdent (ref : Syntax) : TermElabM Syntax := do
-n ← mkFreshAnonymousName;
+  It is just a thin layer on top of `mkFreshUserName`. -/
+def mkFreshIdent (ref : Syntax) : TermElabM Syntax := do
+n ← mkFreshUserName;
 pure $ mkIdentFrom ref n
 
 /--
-  Auxiliary method for creating binder names for local instances.
-  Users expect them to be named as `_inst_<idx>`. -/
-def mkFreshInstanceName : TermElabM Name := do
-s ← get;
-let instIdx := s.instImplicitIdx;
-modify $ fun s => { s with instImplicitIdx := s.instImplicitIdx + 1 };
-pure $ (`_inst).appendIndexAfter instIdx
+  Auxiliary method for creating binder names for local instances. -/
+def mkFreshInstanceName : TermElabM Name :=
+withFreshMacroScope do
+  inst ← `(inst);
+  pure inst.getId
 
 private partial def hasCDot : Syntax → Bool
 | Syntax.node k args =>

tests/lean/PPRoundtrip.lean.expected.out

@@ -18,14 +18,14 @@ fun (a b : Nat) => a
 fun (a : Nat)(b : Bool) => a
 fun {a b : Nat} => a
 typeAs ({α : Type} → α → α) fun {α : Type}(a : α) => a
-fun {α : Type}[_inst_1 : HasToString α](a : α) => @HasToString.toString α _inst_1 a
+fun {α : Type}[inst : HasToString α](a : α) => @HasToString.toString α inst a
 (α : Type) → α
 (α β : Type) → α
 Type → Type → Type
 (α : Type) → α → α
 (α : Type) → (a : α) → Eq a a
 {α : Type} → α
-{α : Type} → [_inst_1 : HasToString α] → α
+{α : Type} → [inst : HasToString α] → α
 0
 1
 42