feat: safer mkCIdentFrom

cc @Kha

src/Init/Lean/Elab/Command.lean

@@ -30,7 +30,7 @@ structure State :=
 (env            : Environment)
 (messages       : MessageLog := {})
 (scopes         : List Scope := [{ kind := "root", header := "" }])
-(nextMacroScope : Nat := 1)
+(nextMacroScope : Nat := firstFrontendMacroScope + 1)
 (maxRecDepth    : Nat)
 
 instance State.inhabited : Inhabited State := ⟨{ env := arbitrary _, maxRecDepth := 0 }⟩
@@ -45,7 +45,7 @@ structure Context :=
 (currRecDepth   : Nat := 0)
 (cmdPos         : String.Pos := 0)
 (macroStack     : MacroStack := [])
-(currMacroScope : MacroScope := 0)
+(currMacroScope : MacroScope := firstFrontendMacroScope)
 
 instance Exception.inhabited : Inhabited Exception := ⟨Exception.error $ arbitrary _⟩
 

src/Init/Lean/Elab/Term.lean

@@ -27,7 +27,7 @@ structure Context extends Meta.Context :=
 (levelNames      : List Name       := [])
 (openDecls       : List OpenDecl   := [])
 (macroStack      : MacroStack      := [])
-(currMacroScope  : MacroScope      := 0)
+(currMacroScope  : MacroScope      := firstFrontendMacroScope)
 /- When `mayPostpone == true`, an elaboration function may interrupt its execution by throwing `Exception.postpone`.
    The function `elabTerm` catches this exception and creates fresh synthetic metavariable `?m`, stores `?m` in
    the list of pending synthetic metavariables, and returns `?m`. -/
@@ -53,7 +53,7 @@ structure State extends Meta.State :=
 (messages        : MessageLog := {})
 (instImplicitIdx : Nat := 1)
 (anonymousIdx    : Nat := 1)
-(nextMacroScope  : Nat := 1)
+(nextMacroScope  : Nat := firstFrontendMacroScope + 1)
 
 instance State.inhabited : Inhabited State := ⟨{ env := arbitrary _ }⟩
 

src/Init/Lean/Hygiene.lean

@@ -33,7 +33,7 @@ instance MonadQuotation : MonadQuotation Unhygienic := {
     fresh ← modifyGet (fun n => (n, n + 1));
     adaptReader (fun _ => fresh) x
 }
-protected def run {α : Type} (x : Unhygienic α) : α := run x 0 1
+protected def run {α : Type} (x : Unhygienic α) : α := run x firstFrontendMacroScope (firstFrontendMacroScope+1)
 end Unhygienic
 
 instance monadQuotationTrans {m n : Type → Type} [MonadQuotation m] [HasMonadLift m n] [MonadFunctorT m m n n] : MonadQuotation n :=

src/Init/LeanInit.lean

@@ -247,6 +247,10 @@ paper soon.
 -/
 
 abbrev MacroScope := Nat
+/-- Macro scope used internally. It is not available for our frontend. -/
+def reservedMacroScope := 0
+/-- First macro scope available for our frontend -/
+def firstFrontendMacroScope := reservedMacroScope + 1
 
 /-- A monad that supports syntax quotations. Syntax quotations (in term
     position) are monadic values that when executed retrieve the current "macro
@@ -423,7 +427,9 @@ Syntax.ident info (toString val).toSubstring val []
   be captured. -/
 def mkCIdentFrom (src : Syntax) (c : Name) : Syntax :=
 let info := src.getHeadInfo;
-Syntax.ident info (toString c).toSubstring (`_root_ ++ c) [(c, [])]
+-- Remark: We use the reserved macro scope to make sure there are no accidental collision with our frontend
+let id   := addMacroScope `_internal c reservedMacroScope;
+Syntax.ident info (toString id).toSubstring id [(c, [])]
 
 def mkAtomFrom (src : Syntax) (val : String) : Syntax :=
 let info := src.getHeadInfo;