refactor: avoid Name, MVarId, and FVarId confusion

src/Lean/Class.lean

@@ -69,7 +69,7 @@ def isOutParam (e : Expr) : Bool :=
 private partial def checkOutParam : Nat → Array FVarId → Expr → Except String Bool
   | i, outParams, Expr.forallE _ d b _ =>
     if isOutParam d then
-      let fvarId    := Name.mkNum `_fvar outParams.size
+      let fvarId    := { name := Name.mkNum `_fvar outParams.size }
       let outParams := outParams.push fvarId
       let fvar      := mkFVar fvarId
       let b         := b.instantiate1 fvar

src/Lean/Compiler/Util.lean

@@ -31,12 +31,12 @@ instance : AndThen Visitor where
 
 @[inline] def skip : Visitor := id
 
-@[inline] def visitFVar (x y : Name) : Visitor
+@[inline] def visitFVar (x y : FVarId) : Visitor
   | d@{result := false, ..} => d
   | {found := false, result := true} => {found := x == y, result := true}
   | {found := true,  result := true} => {found := true, result := x != y}
 
-def visit (x : Name) : Expr → Visitor
+def visit (x : FVarId) : Expr → Visitor
   | Expr.fvar y _        => visitFVar y x
   | Expr.app f a _       => visit x a >> visit x f
   | Expr.lam _ d b _     => visit x d >> visit x b
@@ -51,7 +51,7 @@ end atMostOnce
 open atMostOnce (visit) in
 /-- Return true iff the free variable with id `x` occurs at most once in `e` -/
 @[export lean_at_most_once]
-def atMostOnce (e : Expr) (x : Name) : Bool :=
+def atMostOnce (e : Expr) (x : FVarId) : Bool :=
   let {result := result, ..} := visit x e {found := false, result := true}
   result
 

src/Lean/Elab/Deriving/Inhabited.lean

@@ -10,7 +10,7 @@ open Command
 open Meta
 
 private abbrev IndexSet := Std.RBTree Nat compare
-private abbrev LocalInst2Index := NameMap Nat
+private abbrev LocalInst2Index := FVarIdMap Nat
 
 private def implicitBinderF := Parser.Term.implicitBinder
 private def instBinderF     := Parser.Term.instBinder

src/Lean/Elab/InfoTree.lean

@@ -243,7 +243,7 @@ def Info.updateContext? : Option ContextInfo → Info → Option ContextInfo
 partial def InfoTree.format (tree : InfoTree) (ctx? : Option ContextInfo := none) : IO Format := do
   match tree with
   | ofJson j    => return toString j
-  | hole id     => return toString id
+  | hole id     => return toString id.name
   | context i t => format t i
   | node i cs   => match ctx? with
     | none => return "<context-not-available>"

src/Lean/Elab/Level.lean

@@ -38,7 +38,7 @@ instance : MonadNameGenerator LevelElabM where
   setNGen ngen := modify fun s => { s with ngen := ngen }
 
 def mkFreshLevelMVar : LevelElabM Level := do
-  let mvarId ← mkFreshId
+  let mvarId ← mkFreshMVarId
   modify fun s => { s with mctx := s.mctx.addLevelMVarDecl mvarId }
   return mkLevelMVar mvarId
 

src/Lean/Elab/Match.lean

@@ -406,7 +406,7 @@ def finalizePatternDecls (patternVarDecls : Array PatternVarDecl) : TermElabM (A
       decls := decls.push decl
     | PatternVarDecl.anonymousVar mvarId fvarId =>
        let e ← instantiateMVars (mkMVar mvarId);
-       trace[Elab.match] "finalizePatternDecls: mvarId: {mvarId} := {e}, fvar: {mkFVar fvarId}"
+       trace[Elab.match] "finalizePatternDecls: mvarId: {mvarId.name} := {e}, fvar: {mkFVar fvarId}"
        match e with
        | Expr.mvar newMVarId _ =>
          /- Metavariable was not assigned, or assigned to another metavariable. So,
@@ -425,9 +425,9 @@ open Meta.Match (Pattern Pattern.var Pattern.inaccessible Pattern.ctor Pattern.a
 namespace ToDepElimPattern
 
 structure State where
-  found      : NameSet := {}
+  found      : FVarIdSet := {}
   localDecls : Array LocalDecl
-  newLocals  : NameSet := {}
+  newLocals  : FVarIdSet := {}
 
 abbrev M := StateRefT State TermElabM
 
@@ -448,7 +448,7 @@ private def mkLocalDeclFor (mvar : Expr) : M Pattern := do
   match (← getExprMVarAssignment? mvarId) with
   | some val => return Pattern.inaccessible val
   | none =>
-    let fvarId ← mkFreshId
+    let fvarId ← mkFreshFVarId
     let type   ← inferType mvar
     /- HACK: `fvarId` is not in the scope of `mvarId`
        If this generates problems in the future, we should update the metavariable declarations. -/
@@ -857,7 +857,7 @@ private def expandNonAtomicDiscrs? (matchStx : Syntax) : TermElabM (Option Synta
     else
       -- We use `foundFVars` to make sure the discriminants are distinct variables.
       -- See: code for computing "matchType" at `elabMatchTypeAndDiscrs`
-      let rec loop (discrs : List Syntax) (discrsNew : Array Syntax) (foundFVars : NameSet) := do
+      let rec loop (discrs : List Syntax) (discrsNew : Array Syntax) (foundFVars : FVarIdSet) := do
         match discrs with
         | [] =>
           let discrs := Syntax.mkSep discrsNew (mkAtomFrom matchStx ", ");

src/Lean/Elab/MutualDef.lean

@@ -266,7 +266,7 @@ private def checkLetRecsToLiftTypes (funVars : Array Expr) (letRecsToLift : List
 namespace MutualClosure
 
 /- A mapping from FVarId to Set of FVarIds. -/
-abbrev UsedFVarsMap := NameMap NameSet
+abbrev UsedFVarsMap := FVarIdMap FVarIdSet
 
 /-
 Create the `UsedFVarsMap` mapping that takes the variable id for the mutually recursive functions being defined to the set of
@@ -369,7 +369,7 @@ private def getUsedFVarsMap : M UsedFVarsMap := do pure (← get).usedFVarsMap
 private def modifyUsedFVars (f : UsedFVarsMap → UsedFVarsMap) : M Unit := modify fun s => { s with usedFVarsMap := f s.usedFVarsMap }
 
 -- merge s₂ into s₁
-private def merge (s₁ s₂ : NameSet) : M NameSet :=
+private def merge (s₁ s₂ : FVarIdSet) : M FVarIdSet :=
   s₂.foldM (init := s₁) fun s₁ k => do
     if s₁.contains k then
       pure s₁
@@ -408,7 +408,7 @@ def run (letRecFVarIds : List FVarId) (usedFVarsMap : UsedFVarsMap) : UsedFVarsM
 
 end FixPoint
 
-abbrev FreeVarMap := NameMap (Array FVarId)
+abbrev FreeVarMap := FVarIdMap (Array FVarId)
 
 private def mkFreeVarMap
     (mctx : MetavarContext) (sectionVars : Array Expr) (mainFVarIds : Array FVarId)
@@ -524,7 +524,7 @@ private def mkLetRecClosures (letRecsToLift : List LetRecToLift) (freeVarMap : F
   letRecsToLift.mapM fun toLift => mkLetRecClosureFor toLift (freeVarMap.find? toLift.fvarId).get!
 
 /- Mapping from FVarId of mutually recursive functions being defined to "closure" expression. -/
-abbrev Replacement := NameMap Expr
+abbrev Replacement := FVarIdMap Expr
 
 def insertReplacementForMainFns (r : Replacement) (sectionVars : Array Expr) (mainHeaders : Array DefViewElabHeader) (mainFVars : Array Expr) : Replacement :=
   mainFVars.size.fold (init := r) fun i r =>

src/Lean/Elab/PatternVar.lean

@@ -18,7 +18,7 @@ inductive PatternVar where
 
 instance : ToString PatternVar := ⟨fun
   | PatternVar.localVar x          => toString x
-  | PatternVar.anonymousVar mvarId => s!"?m{mvarId}"⟩
+  | PatternVar.anonymousVar mvarId => s!"?m{mvarId.name}"⟩
 
 /--
   Create an auxiliary Syntax node wrapping a fresh metavariable id.
@@ -30,7 +30,7 @@ private def mkMVarSyntax : TermElabM Syntax := do
 
 /-- Given a syntax node constructed using `mkMVarSyntax`, return its MVarId -/
 def getMVarSyntaxMVarId (stx : Syntax) : MVarId :=
-  stx[0].getKind
+  { name := stx[0].getKind }
 
 /-
   Patterns define new local variables.

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -181,7 +181,7 @@ private def sortFVarIds (fvarIds : Array FVarId) : TacticM (Array FVarId) :=
       | some d₁, some d₂ => d₁.index > d₂.index
       | some _,  none    => false
       | none,    some _  => true
-      | none,    none    => Name.quickLt fvarId₁ fvarId₂
+      | none,    none    => Name.quickLt fvarId₁.name fvarId₂.name
 
 @[builtinTactic Lean.Parser.Tactic.clear] def evalClear : Tactic := fun stx =>
   match stx with

src/Lean/Elab/Tactic/Induction.lean

@@ -376,7 +376,7 @@ private def generalizeTargets (exprs : Array Expr) : TacticM (Array Expr) := do
       appendGoals result.others.toList
 where
   checkTargets (targets : Array Expr) : MetaM Unit := do
-    let mut foundFVars : NameSet := {}
+    let mut foundFVars : FVarIdSet := {}
     for target in targets do
       unless target.isFVar do
         throwError "index in target's type is not a variable (consider using the `cases` tactic instead){indentExpr target}"

src/Lean/Elab/Tactic/Simp.lean

@@ -121,7 +121,7 @@ where
     else
       Term.elabCDotFunctionAlias? simpArgTerm
 
-abbrev FVarIdToLemmaId := NameMap Name
+abbrev FVarIdToLemmaId := FVarIdMap Name
 
 -- TODO: move?
 private def getPropHyps : MetaM (Array FVarId) := do

src/Lean/Elab/Term.lean

@@ -483,7 +483,7 @@ def logUnassignedUsingErrorInfos (pendingMVarIds : Array MVarId) (extraMsg? : Op
   let s ← get
   let hasOtherErrors := s.messages.hasErrors
   let mut hasNewErrors := false
-  let mut alreadyVisited : NameSet := {}
+  let mut alreadyVisited : MVarIdSet := {}
   for mvarErrorInfo in s.mvarErrorInfos do
     let mvarId := mvarErrorInfo.mvarId
     unless alreadyVisited.contains mvarId do

src/Lean/Expr.lean

@@ -157,8 +157,27 @@ def Expr.mkDataForLet (h : UInt64) (looseBVarRange : Nat) (approxDepth : UInt8)
 
 open Expr
 
-abbrev MVarId := Name
-abbrev FVarId := Name
+structure FVarId where
+  name : Name
+  deriving Inhabited, BEq, Hashable
+
+instance : Repr FVarId where
+  reprPrec n p := reprPrec n.name p
+
+def FVarIdSet := Std.RBTree FVarId (Name.quickCmp ·.name ·.name)
+  deriving Inhabited, EmptyCollection
+
+instance : ForIn m FVarIdSet FVarId := inferInstanceAs (ForIn _ (Std.RBTree ..) ..)
+
+def FVarIdHashSet := Std.HashSet FVarId
+  deriving Inhabited, EmptyCollection
+
+def FVarIdMap (α : Type) := Std.RBMap FVarId α (Name.quickCmp ·.name ·.name)
+
+instance : EmptyCollection (FVarIdMap α) := inferInstanceAs (EmptyCollection (Std.RBMap ..))
+
+instance : Inhabited (FVarIdMap α) where
+  default := {}
 
 /- We use the `E` suffix (short for `Expr`) to avoid collision with keywords.
    We considered using «...», but it is too inconvenient to use. -/
@@ -1077,10 +1096,10 @@ def isLHSGoal? (e : Expr) : Option Expr :=
       none
 
 def mkFreshFVarId {m : Type → Type} [Monad m] [MonadNameGenerator m] : m FVarId :=
-  mkFreshId
+  return { name := (← mkFreshId) }
 
-def mkFreshMVarId {m : Type → Type} [Monad m] [MonadNameGenerator m] : m FVarId :=
-  mkFreshId
+def mkFreshMVarId {m : Type → Type} [Monad m] [MonadNameGenerator m] : m MVarId :=
+  return { name := (← mkFreshId) }
 
 def mkNot (p : Expr) : Expr := mkApp (mkConst ``Not) p
 def mkOr (p q : Expr) : Expr := mkApp2 (mkConst ``Or) p q

src/Lean/Level.lean

@@ -50,13 +50,32 @@ def Level.mkData (h : UInt64) (depth : Nat) (hasMVar hasParam : Bool) : Level.Da
 
 open Level
 
+structure MVarId where
+  name : Name
+  deriving Inhabited, BEq, Hashable
+
+instance : Repr MVarId where
+  reprPrec n p := reprPrec n.name p
+
+def MVarIdSet := Std.RBTree MVarId (Name.quickCmp ·.name ·.name)
+  deriving Inhabited, EmptyCollection
+
+instance : ForIn m MVarIdSet MVarId := inferInstanceAs (ForIn _ (Std.RBTree ..) ..)
+
+def MVarIdMap (α : Type) := Std.RBMap MVarId α (Name.quickCmp ·.name ·.name)
+
+instance : EmptyCollection (MVarIdMap α) := inferInstanceAs (EmptyCollection (Std.RBMap ..))
+
+instance : Inhabited (MVarIdMap α) where
+  default := {}
+
 inductive Level where
   | zero   : Data → Level
   | succ   : Level → Data → Level
   | max    : Level → Level → Data → Level
   | imax   : Level → Level → Data → Level
   | param  : Name → Data → Level
-  | mvar   : Name → Data → Level
+  | mvar   : MVarId → Data → Level
   deriving Inhabited
 
 namespace Level
@@ -93,7 +112,7 @@ end Level
 def levelZero :=
   Level.zero $ mkData 2221 0 false false
 
-def mkLevelMVar (mvarId : Name) :=
+def mkLevelMVar (mvarId : MVarId) :=
   Level.mvar mvarId $ mkData (mixHash 2237 $ hash mvarId) 0 true false
 
 def mkLevelParam (name : Name) :=
@@ -116,7 +135,7 @@ def levelOne := mkLevelSucc levelZero
 
 @[export lean_level_mk_zero] def mkLevelZeroEx : Unit → Level := fun _ => levelZero
 @[export lean_level_mk_succ] def mkLevelSuccEx : Level → Level := mkLevelSucc
-@[export lean_level_mk_mvar] def mkLevelMVarEx : Name → Level := mkLevelMVar
+@[export lean_level_mk_mvar] def mkLevelMVarEx : MVarId → Level := mkLevelMVar
 @[export lean_level_mk_param] def mkLevelParamEx : Name → Level := mkLevelParam
 @[export lean_level_mk_max] def mkLevelMaxEx : Level → Level → Level := mkLevelMax
 @[export lean_level_mk_imax] def mkLevelIMaxEx : Level → Level → Level := mkLevelIMax
@@ -152,7 +171,7 @@ def isMVar : Level → Bool
   | mvar .. => true
   | _       => false
 
-def mvarId! : Level → Name
+def mvarId! : Level → MVarId
   | mvar mvarId _ => mvarId
   | _             => panic! "metavariable expected"
 
@@ -231,7 +250,7 @@ partial def normLtAux : Level → Nat → Level → Nat → Bool
     else if l₁₁ != l₂₁ then normLtAux l₁₁ 0 l₂₁ 0
     else normLtAux l₁₂ 0 l₂₂ 0
   | param n₁ _, k₁, param n₂ _, k₂ => if n₁ == n₂ then k₁ < k₂ else Name.lt n₁ n₂     -- use Name.lt because it is lexicographical
-  | mvar n₁ _, k₁, mvar n₂ _, k₂ => if n₁ == n₂ then k₁ < k₂ else Name.quickLt n₁ n₂  -- metavariables are temporary, the actual order doesn't matter
+  | mvar n₁ _, k₁, mvar n₂ _, k₂ => if n₁ == n₂ then k₁ < k₂ else Name.quickLt n₁.name n₂.name  -- metavariables are temporary, the actual order doesn't matter
   | l₁, k₁, l₂, k₂ => if l₁ == l₂ then k₁ < k₂ else ctorToNat l₁ < ctorToNat l₂
 
 /--
@@ -386,7 +405,7 @@ def toResult : Level → Result
   | imax l₁ l₂ _ => Result.imax (toResult l₁) (toResult l₂)
   | param n _    => Result.leaf n
   | mvar n _     =>
-    let n := n.replacePrefix `_uniq (Name.mkSimple "?u");
+    let n := n.name.replacePrefix `_uniq (Name.mkSimple "?u");
     Result.leaf n
 
 private def parenIfFalse : Format → Bool → Format
@@ -531,7 +550,7 @@ abbrev LevelSet := HashSet Level
 abbrev PersistentLevelSet := PHashSet Level
 abbrev PLevelSet := PersistentLevelSet
 
-def Level.collectMVars (u : Level) (s : NameSet := {}) : NameSet :=
+def Level.collectMVars (u : Level) (s : MVarIdSet := {}) : MVarIdSet :=
   match u with
   | succ v _   => collectMVars v s
   | max u v _  => collectMVars u (collectMVars v s)

src/Lean/Meta/AbstractMVars.lean

@@ -24,8 +24,8 @@ structure State where
   nextParamIdx : Nat := 0
   paramNames   : Array Name := #[]
   fvars        : Array Expr  := #[]
-  lmap         : HashMap Name Level := {}
-  emap         : HashMap Name Expr  := {}
+  lmap         : HashMap MVarId Level := {}
+  emap         : HashMap MVarId Expr  := {}
 
 abbrev M := StateM State
 
@@ -35,6 +35,9 @@ def mkFreshId : M Name := do
   modify fun s => { s with ngen := s.ngen.next }
   pure fresh
 
+def mkFreshFVarId : M FVarId :=
+  return { name := (← mkFreshId) }
+
 private partial def abstractLevelMVars (u : Level) : M Level := do
   if !u.hasMVar then
     return u
@@ -91,7 +94,7 @@ partial def abstractExprMVars (e : Expr) : M Expr := do
             return e
           | none   =>
             let type   ← abstractExprMVars decl.type
-            let fvarId ← mkFreshId
+            let fvarId ← mkFreshFVarId
             let fvar := mkFVar fvarId;
             let userName := if decl.userName.isAnonymous then (`x).appendIndexAfter s.fvars.size else decl.userName
             modify fun s => {

src/Lean/Meta/Basic.lean

@@ -157,7 +157,7 @@ structure State where
   mctx        : MetavarContext := {}
   cache       : Cache := {}
   /- When `trackZeta == true`, then any let-decl free variable that is zeta expansion performed by `MetaM` is stored in `zetaFVarIds`. -/
-  zetaFVarIds : NameSet := {}
+  zetaFVarIds : FVarIdSet := {}
   postponed   : PersistentArray PostponedEntry := {}
   deriving Inhabited
 
@@ -264,7 +264,7 @@ def setMCtx (mctx : MetavarContext) : MetaM Unit :=
 def resetZetaFVarIds : MetaM Unit :=
   modify fun s => { s with zetaFVarIds := {} }
 
-def getZetaFVarIds : MetaM NameSet :=
+def getZetaFVarIds : MetaM FVarIdSet :=
   return (← get).zetaFVarIds
 
 def getPostponed : MetaM (PersistentArray PostponedEntry) :=
@@ -302,10 +302,10 @@ def mkFreshExprMVarAt
     (lctx : LocalContext) (localInsts : LocalInstances) (type : Expr)
     (kind : MetavarKind := MetavarKind.natural) (userName : Name := Name.anonymous) (numScopeArgs : Nat := 0)
     : MetaM Expr := do
-  mkFreshExprMVarAtCore (← mkFreshId) lctx localInsts type kind userName numScopeArgs
+  mkFreshExprMVarAtCore (← mkFreshMVarId) lctx localInsts type kind userName numScopeArgs
 
 def mkFreshLevelMVar : MetaM Level := do
-  let mvarId ← mkFreshId
+  let mvarId ← mkFreshMVarId
   modifyMCtx fun mctx => mctx.addLevelMVarDecl mvarId;
   return mkLevelMVar mvarId
 
@@ -365,7 +365,7 @@ def shouldReduceReducibleOnly : MetaM Bool :=
 def getMVarDecl (mvarId : MVarId) : MetaM MetavarDecl := do
   match (← getMCtx).findDecl? mvarId with
   | some d => pure d
-  | none   => throwError "unknown metavariable '?{mvarId}'"
+  | none   => throwError "unknown metavariable '?{mvarId.name}'"
 
 def setMVarKind (mvarId : MVarId) (kind : MetavarKind) : MetaM Unit :=
   modifyMCtx fun mctx => mctx.setMVarKind mvarId kind
@@ -387,7 +387,7 @@ def isReadOnlyOrSyntheticOpaqueExprMVar (mvarId : MVarId) : MetaM Bool := do
 def getLevelMVarDepth (mvarId : MVarId) : MetaM Nat := do
   match (← getMCtx).findLevelDepth? mvarId with
   | some depth => return depth
-  | _          => throwError "unknown universe metavariable '?{mvarId}'"
+  | _          => throwError "unknown universe metavariable '?{mvarId.name}'"
 
 def isReadOnlyLevelMVar (mvarId : MVarId) : MetaM Bool := do
   if (← getConfig).ignoreLevelMVarDepth then
@@ -684,7 +684,7 @@ mutual
       | Expr.forallE n d b c =>
         if fvarsSizeLtMaxFVars fvars maxFVars? then
           let d     := d.instantiateRevRange j fvars.size fvars
-          let fvarId ← mkFreshId
+          let fvarId ← mkFreshFVarId
           let lctx  := lctx.mkLocalDecl fvarId n d c.binderInfo
           let fvar  := mkFVar fvarId
           let fvars := fvars.push fvar
@@ -785,14 +785,14 @@ where
     match consumeLet, e with
     | _, Expr.lam n d b c =>
       let d := d.instantiateRevRange j fvars.size fvars
-      let fvarId ← mkFreshId
+      let fvarId ← mkFreshFVarId
       let lctx := lctx.mkLocalDecl fvarId n d c.binderInfo
       let fvar := mkFVar fvarId
       process consumeLet lctx (fvars.push fvar) j b
     | true, Expr.letE n t v b _ => do
       let t := t.instantiateRevRange j fvars.size fvars
       let v := v.instantiateRevRange j fvars.size fvars
-      let fvarId ← mkFreshId
+      let fvarId ← mkFreshFVarId
       let lctx := lctx.mkLetDecl fvarId n t v
       let fvar := mkFVar fvarId
       process true lctx (fvars.push fvar) j b
@@ -884,7 +884,7 @@ private def withNewFVar (fvar fvarType : Expr) (k : Expr → MetaM α) : MetaM
   | some c => withNewLocalInstance c fvar <| k fvar
 
 private def withLocalDeclImp (n : Name) (bi : BinderInfo) (type : Expr) (k : Expr → MetaM α) : MetaM α := do
-  let fvarId ← mkFreshId
+  let fvarId ← mkFreshFVarId
   let ctx ← read
   let lctx := ctx.lctx.mkLocalDecl fvarId n type bi
   let fvar := mkFVar fvarId
@@ -924,7 +924,7 @@ def withNewBinderInfos (bs : Array (FVarId × BinderInfo)) (k : n α) : n α :=
   mapMetaM (fun k => withNewBinderInfosImp bs k) k
 
 private def withLetDeclImp (n : Name) (type : Expr) (val : Expr) (k : Expr → MetaM α) : MetaM α := do
-  let fvarId ← mkFreshId
+  let fvarId ← mkFreshFVarId
   let ctx ← read
   let lctx := ctx.lctx.mkLetDecl fvarId n type val
   let fvar := mkFVar fvarId

src/Lean/Meta/DiscrTree.lean

@@ -60,7 +60,7 @@ def Key.ctorIdx : Key → Nat
 
 def Key.lt : Key → Key → Bool
   | Key.lit v₁,      Key.lit v₂      => v₁ < v₂
-  | Key.fvar n₁ a₁,  Key.fvar n₂ a₂  => Name.quickLt n₁ n₂ || (n₁ == n₂ && a₁ < a₂)
+  | Key.fvar n₁ a₁,  Key.fvar n₂ a₂  => Name.quickLt n₁.name n₂.name || (n₁ == n₂ && a₁ < a₂)
   | Key.const n₁ a₁, Key.const n₂ a₂ => Name.quickLt n₁ n₂ || (n₁ == n₂ && a₁ < a₂)
   | Key.proj s₁ i₁,  Key.proj s₂ i₂  => Name.quickLt s₁ s₂ || (s₁ == s₂ && i₁ < i₂)
   | k₁,              k₂              => k₁.ctorIdx < k₂.ctorIdx
@@ -75,7 +75,7 @@ def Key.format : Key → Format
   | Key.lit (Literal.strVal v) => repr v
   | Key.const k _              => Std.format k
   | Key.proj s i               => Std.format s ++ "." ++ Std.format i
-  | Key.fvar k _               => Std.format k
+  | Key.fvar k _               => Std.format k.name
   | Key.arrow                  => "→"
 
 instance : ToFormat Key := ⟨Key.format⟩
@@ -109,7 +109,7 @@ instance [ToFormat α] : ToFormat (DiscrTree α) := ⟨format⟩
 
 /- The discrimination tree ignores implicit arguments and proofs.
    We use the following auxiliary id as a "mark". -/
-private def tmpMVarId : MVarId := `_discr_tree_tmp
+private def tmpMVarId : MVarId := { name := `_discr_tree_tmp }
 private def tmpStar := mkMVar tmpMVarId
 
 instance : Inhabited (DiscrTree α) where

src/Lean/Meta/ExprDefEq.lean

@@ -211,7 +211,7 @@ private partial def isDefEqBindingAux (lctx : LocalContext) (fvars : Array Expr)
   let process (n : Name) (d₁ d₂ b₁ b₂ : Expr) : MetaM Bool := do
     let d₁     := d₁.instantiateRev fvars
     let d₂     := d₂.instantiateRev fvars
-    let fvarId ← mkFreshId
+    let fvarId ← mkFreshFVarId
     let lctx   := lctx.mkLocalDecl fvarId n d₁
     let fvars  := fvars.push (mkFVar fvarId)
     isDefEqBindingAux lctx fvars b₁ b₂ (ds₂.push d₂)
@@ -303,8 +303,8 @@ where
 
   /- Traverse `e` and stores in the state `NameHashSet` any let-declaration with index greater than `(← read)`.
      The context `Nat` is the position of `xs[0]` in the local context. -/
-  collectLetDeclsFrom (e : Expr) : ReaderT Nat (StateRefT NameHashSet MetaM) Unit := do
-    let rec visit (e : Expr) : MonadCacheT Expr Unit (ReaderT Nat (StateRefT NameHashSet MetaM)) Unit :=
+  collectLetDeclsFrom (e : Expr) : ReaderT Nat (StateRefT FVarIdHashSet MetaM) Unit := do
+    let rec visit (e : Expr) : MonadCacheT Expr Unit (ReaderT Nat (StateRefT FVarIdHashSet MetaM)) Unit :=
       checkCache e fun _ => do
         match e with
         | Expr.forallE _ d b _   => visit d; visit b
@@ -326,7 +326,7 @@ where
     or equal to the position of `xs.back` in the local context.
     The `Nat` context `(← read)` is the position of `xs[0]` in the local context.
   -/
-  collectLetDepsAux : Nat → ReaderT Nat (StateRefT NameHashSet MetaM) Unit
+  collectLetDepsAux : Nat → ReaderT Nat (StateRefT FVarIdHashSet MetaM) Unit
     | 0   => return ()
     | i+1 => do
       if i+1 == (← read) then
@@ -343,7 +343,7 @@ where
           collectLetDepsAux i
 
   /- Computes the set `ys`. It is a set of `FVarId`s, -/
-  collectLetDeps : MetaM NameHashSet := do
+  collectLetDeps : MetaM FVarIdHashSet := do
     let lctx ← getLCtx
     let start := lctx.getFVar! xs[0] |>.index
     let stop  := lctx.getFVar! xs.back |>.index

src/Lean/Meta/GeneralizeVars.lean

@@ -11,7 +11,7 @@ namespace Lean.Meta
 /--
   Add to `forbidden` all a set of `FVarId`s containing `targets` and all variables they depend on.
 -/
-partial def mkGeneralizationForbiddenSet (targets : Array Expr) (forbidden : NameSet := {}) : MetaM NameSet := do
+partial def mkGeneralizationForbiddenSet (targets : Array Expr) (forbidden : FVarIdSet := {}) : MetaM FVarIdSet := do
   let mut s := { fvarSet := forbidden }
   let mut todo := #[]
   for target in targets do
@@ -21,7 +21,7 @@ partial def mkGeneralizationForbiddenSet (targets : Array Expr) (forbidden : Nam
       s := collectFVars s (← instantiateMVars (← inferType target))
   loop todo.toList s.fvarSet
 where
-  visit (fvarId : FVarId) (todo : List FVarId) (s : NameSet) : MetaM (List FVarId × NameSet) := do
+  visit (fvarId : FVarId) (todo : List FVarId) (s : FVarIdSet) : MetaM (List FVarId × FVarIdSet) := do
     let localDecl ← getLocalDecl fvarId
     let mut s' := collectFVars {} (← instantiateMVars localDecl.type)
     if let some val := localDecl.value? then
@@ -34,7 +34,7 @@ where
         s := s.insert fvarId
     return (todo, s)
 
-  loop (todo : List FVarId) (s : NameSet) : MetaM NameSet := do
+  loop (todo : List FVarId) (s : FVarIdSet) : MetaM FVarIdSet := do
     match todo with
     | [] => return s
     | fvarId::todo =>
@@ -54,9 +54,9 @@ where
   Remark: we *not* collect instance implicit arguments nor auxiliary declarations for compiling
   recursive declarations.
 -/
-def getFVarSetToGeneralize (targets : Array Expr) (forbidden : NameSet) : MetaM NameSet := do
-  let mut s : NameSet := targets.foldl (init := {}) fun s target => if target.isFVar then s.insert target.fvarId! else s
-  let mut r : NameSet := {}
+def getFVarSetToGeneralize (targets : Array Expr) (forbidden : FVarIdSet) : MetaM FVarIdSet := do
+  let mut s : FVarIdSet := targets.foldl (init := {}) fun s target => if target.isFVar then s.insert target.fvarId! else s
+  let mut r : FVarIdSet := {}
   for localDecl in (← getLCtx) do
     unless forbidden.contains localDecl.fvarId do
       unless localDecl.isAuxDecl || localDecl.binderInfo.isInstImplicit do
@@ -65,12 +65,12 @@ def getFVarSetToGeneralize (targets : Array Expr) (forbidden : NameSet) : MetaM
         s := s.insert localDecl.fvarId
   return r
 
-def sortFVars (fvars : NameSet) : MetaM (Array FVarId) := do
+def sortFVars (fvars : FVarIdSet) : MetaM (Array FVarId) := do
   let fvarIds := fvars.fold (init := #[]) fun s fvarId => s.push fvarId
   let lctx ← getLCtx
   return fvarIds.qsort fun x y => (lctx.get! x).index < (lctx.get! y).index
 
-def getFVarsToGeneralize (targets : Array Expr) (forbidden : NameSet := {}) : MetaM (Array FVarId) := do
+def getFVarsToGeneralize (targets : Array Expr) (forbidden : FVarIdSet := {}) : MetaM (Array FVarId) := do
   let forbidden ← mkGeneralizationForbiddenSet targets forbidden
   let s ← getFVarSetToGeneralize targets forbidden
   sortFVars s

src/Lean/Meta/InferType.lean

@@ -152,12 +152,12 @@ private def inferLambdaType (e : Expr) : MetaM Expr :=
 
 @[inline] private def withLocalDecl' {α} (name : Name) (bi : BinderInfo) (type : Expr) (x : Expr → MetaM α) : MetaM α :=
   savingCache do
-    let fvarId ← mkFreshId
+    let fvarId ← mkFreshFVarId
     withReader (fun ctx => { ctx with lctx := ctx.lctx.mkLocalDecl fvarId name type bi }) do
       x (mkFVar fvarId)
 
 def throwUnknownMVar {α} (mvarId : MVarId) : MetaM α :=
-  throwError "unknown metavariable '?{mvarId}'"
+  throwError "unknown metavariable '?{mvarId.name}'"
 
 private def inferMVarType (mvarId : MVarId) : MetaM Expr := do
   match (← getMCtx).findDecl? mvarId with

src/Lean/Meta/Match/CaseValues.lean

@@ -46,7 +46,7 @@ private def caseValueAux (mvarId : MVarId) (fvarId : FVarId) (value : Expr) (hNa
     let clearH := false
     let (thenSubst, thenMVarId) ← substCore thenMVarId thenH symm subst clearH
     withMVarContext thenMVarId do
-      trace[Meta] "subst domain: {thenSubst.domain}"
+      trace[Meta] "subst domain: {thenSubst.domain.map (·.name)}"
       let thenH := (thenSubst.get thenH).fvarId!
       trace[Meta] "searching for decl"
       let decl ← getLocalDecl thenH

src/Lean/Meta/Match/MVarRenaming.lean

@@ -9,7 +9,7 @@ namespace Lean.Meta
 
 /- A mapping from MVarId to MVarId -/
 structure MVarRenaming where
-  map : NameMap MVarId := {}
+  map : MVarIdMap MVarId := {}
 
 def MVarRenaming.isEmpty (s : MVarRenaming) : Bool :=
   s.map.isEmpty

src/Lean/Meta/Match/MatchEqs.lean

@@ -197,13 +197,13 @@ private partial def mkSplitterProof (matchDeclName : Name) (template : Expr) (al
     proveSubgoal mvarId
   instantiateMVars proof
 where
-  mkMap : NameMap Expr := do
+  mkMap : FVarIdMap Expr := do
     let mut m := {}
     for alt in alts, altNew in altsNew do
       m := m.insert alt.fvarId! altNew
     return m
 
-  convertTemplate (m : NameMap Expr) : StateRefT (Array MVarId) MetaM Expr :=
+  convertTemplate (m : FVarIdMap Expr) : StateRefT (Array MVarId) MetaM Expr :=
     transform template fun e => do
       match e.getAppFn with
       | Expr.fvar fvarId .. =>

src/Lean/Meta/PPGoal.lean

@@ -29,8 +29,8 @@ def withPPInaccessibleNames [MonadControlT MetaM m] [Monad m] (x : m α) (flag :
 namespace ToHide
 
 structure State where
-  hiddenInaccessibleProp : NameSet := {} -- FVarIds of Propostions with inaccessible names but containing only visible names. We show only their types
-  hiddenInaccessible     : NameSet := {} -- FVarIds with inaccessible names, but not in hiddenInaccessibleProp
+  hiddenInaccessibleProp : FVarIdSet := {} -- FVarIds of Propostions with inaccessible names but containing only visible names. We show only their types
+  hiddenInaccessible     : FVarIdSet := {} -- FVarIds with inaccessible names, but not in hiddenInaccessibleProp
   modified               : Bool := false
 
 structure Context where
@@ -125,7 +125,7 @@ The `goalTarget` counts as a forward dependency.
 
 We say a name is visible if it is a free variable with FVarId not in `hiddenInaccessible` nor `hiddenInaccessibleProp`
 -/
-def collect (goalTarget : Expr) : MetaM (NameSet × NameSet) := do
+def collect (goalTarget : Expr) : MetaM (FVarIdSet × FVarIdSet) := do
   if pp.inaccessibleNames.get (← getOptions) then
     /- Don't hide inaccessible names when `pp.inaccessibleNames` is set to true. -/
     return ({}, {})

src/Lean/Meta/SortLocalDecls.lean

@@ -28,12 +28,12 @@ mutual
     | Expr.app f a _       => visitExpr f; visitExpr a
     | Expr.mdata _ b _     => visitExpr b
     | Expr.mvar _ _        => let v ← instantiateMVars e; unless v.isMVar do visitExpr v
-    | Expr.fvar fvarId _   => if let some localDecl := (← read).localDecls.find? fvarId then visitLocalDecl localDecl
+    | Expr.fvar fvarId _   => if let some localDecl := (← read).localDecls.find? fvarId.name then visitLocalDecl localDecl
     | _                    => return ()
 
   partial def visitLocalDecl (localDecl : LocalDecl) : M Unit := do
-    unless (← get).visited.contains localDecl.fvarId do
-      modify fun s => { s with visited := s.visited.insert localDecl.fvarId }
+    unless (← get).visited.contains localDecl.fvarId.name do
+      modify fun s => { s with visited := s.visited.insert localDecl.fvarId.name }
       visitExpr localDecl.type
       if let some val := localDecl.value? then
         visitExpr val
@@ -45,6 +45,6 @@ end SortLocalDecls
 open SortLocalDecls in
 def sortLocalDecls (localDecls : Array LocalDecl) : MetaM (Array LocalDecl) :=
   let aux : M (Array LocalDecl) := do localDecls.forM visitLocalDecl; return (← get).result
-  aux.run { localDecls := localDecls.foldl (init := {}) fun s d => s.insert d.fvarId d } |>.run' {}
+  aux.run { localDecls := localDecls.foldl (init := {}) fun s d => s.insert d.fvarId.name d } |>.run' {}
 
-end Lean.Meta
+end Lean.Meta

src/Lean/Meta/SynthInstance.lean

@@ -131,7 +131,7 @@ partial def normExpr (e : Expr) : M Expr := do
         match s.emap.find? mvarId with
         | some e' => pure e'
         | none    => do
-          let e' := mkFVar $ Name.mkNum `_tc s.nextIdx
+          let e' := mkFVar { name := Name.mkNum `_tc s.nextIdx }
           modify fun s => { s with nextIdx := s.nextIdx + 1, emap := s.emap.insert mvarId e' }
           pure e'
     | _ => pure e

src/Lean/Meta/Tactic/Intro.lean

@@ -28,7 +28,7 @@ namespace Lean.Meta
       let type   := type.instantiateRevRange j fvars.size fvars
       let type   := type.headBeta
       let val    := val.instantiateRevRange j fvars.size fvars
-      let fvarId ← mkFreshId
+      let fvarId ← mkFreshFVarId
       let (n, s) ← mkName lctx n true s
       let lctx   := lctx.mkLetDecl fvarId n type val
       let fvar   := mkFVar fvarId
@@ -37,7 +37,7 @@ namespace Lean.Meta
     | (i+1), lctx, fvars, j, s, Expr.forallE n type body c => do
       let type   := type.instantiateRevRange j fvars.size fvars
       let type   := type.headBeta
-      let fvarId ← mkFreshId
+      let fvarId ← mkFreshFVarId
       let (n, s) ← mkName lctx n c.binderInfo.isExplicit s
       let lctx   := lctx.mkLocalDecl fvarId n type c.binderInfo
       let fvar   := mkFVar fvarId

src/Lean/Meta/Tactic/Simp/CongrLemmas.lean

@@ -52,7 +52,7 @@ def mkCongrLemma (declName : Name) (prio : Nat) : MetaM CongrLemma := withReduci
     lhs.withApp fun lhsFn lhsArgs => rhs.withApp fun rhsFn rhsArgs => do
       unless lhsFn.isConst && rhsFn.isConst && lhsFn.constName! == rhsFn.constName! && lhsArgs.size == rhsArgs.size do
         throwError "invalid 'congr' theorem, equality left/right-hand sides must be applications of the same function{indentExpr type}"
-      let mut foundMVars : NameSet := {}
+      let mut foundMVars : MVarIdSet := {}
       for lhsArg in lhsArgs do
         unless lhsArg.isSort do
           unless lhsArg.isMVar do
@@ -98,7 +98,7 @@ def mkCongrLemma (declName : Name) (prio : Nat) : MetaM CongrLemma := withReduci
       }
 where
   /-- Return `true` if `t` contains a metavariable that is not in `mvarSet` -/
-  onlyMVarsAt (t : Expr) (mvarSet : NameSet) : Bool :=
+  onlyMVarsAt (t : Expr) (mvarSet : MVarIdSet) : Bool :=
     Option.isNone <| t.find? fun e => e.isMVar && !mvarSet.contains e.mvarId!
 
 def addCongrLemma (declName : Name) (attrKind : AttributeKind) (prio : Nat) : MetaM Unit := do

src/Lean/Meta/Tactic/Simp/Main.lean

@@ -430,7 +430,7 @@ def simpLocalDecl (mvarId : MVarId) (fvarId : FVarId) (ctx : Simp.Context) (disc
       else
         return some (fvarId, mvarId)
 
-abbrev FVarIdToLemmaId := NameMap Name
+abbrev FVarIdToLemmaId := FVarIdMap Name
 
 def simpGoal (mvarId : MVarId) (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none) (simplifyTarget : Bool := true) (fvarIdsToSimp : Array FVarId := #[]) (fvarIdToLemmaId : FVarIdToLemmaId := {}) : MetaM (Option (Array FVarId × MVarId)) := do
   withMVarContext mvarId do

src/Lean/Meta/Tactic/Subst.lean

@@ -28,7 +28,7 @@ def substCore (mvarId : MVarId) (hFVarId : FVarId) (symm := false) (fvarSubst :
       match a with
       | Expr.fvar aFVarId _ => do
         let aFVarIdOriginal := aFVarId
-        trace[Meta.Tactic.subst] "substituting {a} (id: {aFVarId}) with {b}"
+        trace[Meta.Tactic.subst] "substituting {a} (id: {aFVarId.name}) with {b}"
         let mctx ← getMCtx
         if mctx.exprDependsOn b aFVarId then
           throwTacticEx `subst mvarId m!"'{a}' occurs at{indentExpr b}"
@@ -37,7 +37,7 @@ def substCore (mvarId : MVarId) (hFVarId : FVarId) (symm := false) (fvarSubst :
         trace[Meta.Tactic.subst] "after revert {MessageData.ofGoal mvarId}"
         let (twoVars, mvarId) ← introNP mvarId 2
         trace[Meta.Tactic.subst] "after intro2 {MessageData.ofGoal mvarId}"
-        trace[Meta.Tactic.subst] "reverted variables {vars}"
+        trace[Meta.Tactic.subst] "reverted variables {vars.map (·.name)}"
         let aFVarId := twoVars[0]
         let a       := mkFVar aFVarId
         let hFVarId := twoVars[1]

src/Lean/Meta/Tactic/Util.lean

@@ -59,7 +59,7 @@ def headBetaMVarType (mvarId : MVarId) : MetaM Unit := do
 /-- Collect nondependent hypotheses that are propositions. -/
 def getNondepPropHyps (mvarId : MVarId) : MetaM (Array FVarId) :=
   withMVarContext mvarId do
-    let mut candidates : NameHashSet := {}
+    let mut candidates : FVarIdHashSet := {}
     for localDecl in (← getLCtx) do
       unless localDecl.isAuxDecl do
         candidates ← removeDeps localDecl.type candidates
@@ -78,9 +78,9 @@ def getNondepPropHyps (mvarId : MVarId) : MetaM (Array FVarId) :=
           result := result.push localDecl.fvarId
       return result
 where
-  removeDeps (e : Expr) (candidates : NameHashSet) : MetaM NameHashSet := do
+  removeDeps (e : Expr) (candidates : FVarIdHashSet) : MetaM FVarIdHashSet := do
     let e ← instantiateMVars e
-    let visit : StateRefT NameHashSet MetaM NameHashSet := do
+    let visit : StateRefT FVarIdHashSet MetaM FVarIdHashSet := do
       e.forEach fun
         | Expr.fvar fvarId _ => modify fun s => s.erase fvarId
         | _ => pure ()

src/Lean/MetavarContext.lean

@@ -906,7 +906,7 @@ mutual
           let newLocalInsts := mvarDecl.localInstances.filter fun inst => toRevert.all fun x => inst.fvar != x
           -- Remark: we must reset the before processing `mkAuxMVarType` because `toRevert` may not be equal to `xs`
           let newMVarType ← withFreshCache do mkAuxMVarType mvarLCtx toRevert newMVarKind mvarDecl.type
-          let newMVarId    := (← get).ngen.curr
+          let newMVarId    := { name := (← get).ngen.curr }
           let newMVar      := mkMVar newMVarId
           let result       := mkMVarApp mvarLCtx newMVar toRevert newMVarKind
           let numScopeArgs := mvarDecl.numScopeArgs + result.getAppNumArgs

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -29,7 +29,7 @@ try
   maybeAddBlockImplicit (mkIdent l.userName)
 catch _ =>
   -- loose free variable, use internal name
-  maybeAddBlockImplicit $ mkIdent id
+  maybeAddBlockImplicit $ mkIdent id.name
 
 -- loose bound variable, use pseudo syntax
 @[builtinDelab bvar]
@@ -43,7 +43,7 @@ def delabMVar : Delab := do
   let mvarDecl ← getMVarDecl n
   let n :=
     match mvarDecl.userName with
-    | Name.anonymous => n.replacePrefix `_uniq `m
+    | Name.anonymous => n.name.replacePrefix `_uniq `m
     | n => n
   `(?$(mkIdent n))
 

src/Lean/Util/CollectFVars.lean

@@ -9,7 +9,7 @@ namespace Lean.CollectFVars
 
 structure State where
   visitedExpr  : ExprSet  := {}
-  fvarSet      : NameSet  := {}
+  fvarSet      : FVarIdSet  := {}
   deriving Inhabited
 
 abbrev Visitor := State → State

src/Lean/Widget/InteractiveGoal.lean

@@ -68,7 +68,7 @@ open Meta in
 /-- A variant of `Meta.ppGoal` which preserves subexpression information for interactivity. -/
 def goalToInteractive (mvarId : MVarId) : MetaM InteractiveGoal := do
   let some mvarDecl ← (← getMCtx).findDecl? mvarId
-    | throwError "unknown goal {mvarId}"
+    | throwError "unknown goal {mvarId.name}"
   let ppAuxDecls := pp.auxDecls.get (← getOptions)
   let lctx := mvarDecl.lctx
   let lctx := lctx.sanitizeNames.run' { options := (← getOptions) }