diff --git a/src/Init/Lean/Expr.lean b/src/Init/Lean/Expr.lean
index 66599ffc91..7945a0cd68 100644
--- a/src/Init/Lean/Expr.lean
+++ b/src/Init/Lean/Expr.lean
@@ -160,12 +160,15 @@ Expr.mkDataCore h looseBVarRange hasFVar hasExprMVar hasLevelMVar hasLevelParam
 
 open Expr
 
+abbrev MVarId := Name
+abbrev FVarId := Name
+
 /- We use the `E` suffix (short for `Expr`) to avoid collision with keywords.
    We considered using «...», but it is too inconvenient to use. -/
 inductive Expr
 | bvar    : Nat → Data → Expr                       -- bound variables
-| fvar    : Name → Data → Expr                      -- free variables
-| mvar    : Name → Data → Expr                      -- meta variables
+| fvar    : FVarId → Data → Expr                    -- free variables
+| mvar    : MVarId → Data → Expr                    -- meta variables
 | sort    : Level → Data → Expr                     -- Sort
 | const   : Name → List Level → Data → Expr         -- constants
 | app     : Expr → Expr → Data → Expr               -- application
@@ -261,10 +264,10 @@ Expr.bvar idx $ mkData (mixHash 7 $ hash idx) (idx+1)
 def mkSort (lvl : Level) : Expr :=
 Expr.sort lvl $ mkData (mixHash 11 $ hash lvl) 0 false false lvl.hasMVar lvl.hasParam
 
-def mkFVar (fvarId : Name) : Expr :=
+def mkFVar (fvarId : FVarId) : Expr :=
 Expr.fvar fvarId $ mkData (mixHash 13 $ hash fvarId) 0 true
 
-def mkMVar (fvarId : Name) : Expr :=
+def mkMVar (fvarId : MVarId) : Expr :=
 Expr.mvar fvarId $ mkData (mixHash 17 $ hash fvarId) 0 false true
 
 def mkMData (d : MData) (e : Expr) : Expr :=
@@ -309,12 +312,13 @@ Expr.letE x t v b $ mkDataForLet (mixHash 41 $ mixHash (hash t) $ mixHash (hash
   (t.hasLevelParam || v.hasLevelParam || b.hasLevelParam)
   nonDep
 
+-- TODO: delete
 def mkLocal (x u : Name) (t : Expr) (bi : BinderInfo) : Expr :=
 Expr.localE x u t $ mkDataForBinder (mixHash 43 $ hash t) t.looseBVarRange true t.hasExprMVar t.hasLevelMVar t.hasLevelParam bi
 
 @[export lean_expr_mk_bvar] def mkBVarEx : Nat → Expr := mkBVar
-@[export lean_expr_mk_fvar] def mkFVarEx : Name → Expr := mkFVar
-@[export lean_expr_mk_mvar] def mkMVarEx : Name → Expr := mkMVar
+@[export lean_expr_mk_fvar] def mkFVarEx : FVarId → Expr := mkFVar
+@[export lean_expr_mk_mvar] def mkMVarEx : MVarId → Expr := mkMVar
 @[export lean_expr_mk_sort] def mkSortEx : Level → Expr := mkSort
 @[export lean_expr_mk_const] def mkConstEx (c : Name) (lvls : List Level) : Expr := mkConst c lvls
 @[export lean_expr_mk_app] def mkAppEx : Expr → Expr → Expr := mkApp
@@ -507,11 +511,11 @@ def bvarIdx! : Expr → Nat
 | bvar idx _ => idx
 | _          => panic! "bvar expected"
 
-def fvarId! : Expr → Name
+def fvarId! : Expr → FVarId
 | fvar n _ => n
 | _        => panic! "fvar expected"
 
-def mvarId! : Expr → Name
+def mvarId! : Expr → MVarId
 | mvar n _ => n
 | _        => panic! "mvar expected"
 
diff --git a/src/Init/Lean/LocalContext.lean b/src/Init/Lean/LocalContext.lean
index 87e684224a..8a257596db 100644
--- a/src/Init/Lean/LocalContext.lean
+++ b/src/Init/Lean/LocalContext.lean
@@ -11,8 +11,8 @@ import Init.Lean.Expr
 namespace Lean
 
 inductive LocalDecl
-| cdecl (index : Nat) (name : Name) (userName : Name) (type : Expr) (bi : BinderInfo)
-| ldecl (index : Nat) (name : Name) (userName : Name) (type : Expr) (value : Expr)
+| cdecl (index : Nat) (fvarId : FVarId) (userName : Name) (type : Expr) (bi : BinderInfo)
+| ldecl (index : Nat) (fvarId : FVarId) (userName : Name) (type : Expr) (value : Expr)
 
 namespace LocalDecl
 instance : Inhabited LocalDecl := ⟨ldecl (arbitrary _) (arbitrary _) (arbitrary _) (arbitrary _) (arbitrary _)⟩
@@ -25,9 +25,9 @@ def index : LocalDecl → Nat
 | cdecl idx _ _ _ _ => idx
 | ldecl idx _ _ _ _ => idx
 
-def name : LocalDecl → Name
-| cdecl _ n _ _ _ => n
-| ldecl _ n _ _ _ => n
+def fvarId : LocalDecl → FVarId
+| cdecl _ id _ _ _ => id
+| ldecl _ id _ _ _ => id
 
 def userName : LocalDecl → Name
 | cdecl _ _ n _ _ => n
@@ -50,17 +50,17 @@ def value : LocalDecl → Expr
 | ldecl _ _ _ _ v => v
 
 def updateUserName : LocalDecl → Name → LocalDecl
-| cdecl index name _ type bi,  userName => cdecl index name userName type bi
-| ldecl index name _ type val, userName => ldecl index name userName type val
+| cdecl index id _ type bi,  userName => cdecl index id userName type bi
+| ldecl index id _ type val, userName => ldecl index id userName type val
 
 def toExpr (decl : LocalDecl) : Expr :=
-mkFVar decl.name
+mkFVar decl.fvarId
 
 end LocalDecl
 
 structure LocalContext :=
-(nameToDecl : PersistentHashMap Name LocalDecl := {})
-(decls      : PersistentArray (Option LocalDecl) := {})
+(fvarIdToDecl : PersistentHashMap Name LocalDecl := {})
+(decls        : PersistentArray (Option LocalDecl) := {})
 
 namespace LocalContext
 instance : Inhabited LocalContext := ⟨{}⟩
@@ -74,34 +74,34 @@ def empty : LocalContext :=
 
 @[export lean_local_ctx_is_empty]
 def isEmpty (lctx : LocalContext) : Bool :=
-lctx.nameToDecl.isEmpty
+lctx.fvarIdToDecl.isEmpty
 
 /- Low level API for creating local declarations. It is used to implement actions in the monads `Elab` and `Tactic`. It should not be used directly since the argument `(name : Name)` is assumed to be "unique". -/
 @[export lean_local_ctx_mk_local_decl]
-def mkLocalDecl (lctx : LocalContext) (fvarId : Name) (userName : Name) (type : Expr) (bi : BinderInfo := BinderInfo.default) : LocalContext :=
+def mkLocalDecl (lctx : LocalContext) (fvarId : FVarId) (userName : Name) (type : Expr) (bi : BinderInfo := BinderInfo.default) : LocalContext :=
 match lctx with
-| { nameToDecl := map, decls := decls } =>
+| { fvarIdToDecl := map, decls := decls } =>
   let idx  := decls.size;
   let decl := LocalDecl.cdecl idx fvarId userName type bi;
-  { nameToDecl := map.insert fvarId decl, decls := decls.push decl }
+  { fvarIdToDecl := map.insert fvarId decl, decls := decls.push decl }
 
 @[export lean_local_ctx_mk_let_decl]
-def mkLetDecl (lctx : LocalContext) (fvarId : Name) (userName : Name) (type : Expr) (value : Expr) : LocalContext :=
+def mkLetDecl (lctx : LocalContext) (fvarId : FVarId) (userName : Name) (type : Expr) (value : Expr) : LocalContext :=
 match lctx with
-| { nameToDecl := map, decls := decls } =>
+| { fvarIdToDecl := map, decls := decls } =>
   let idx  := decls.size;
   let decl := LocalDecl.ldecl idx fvarId userName type value;
-  { nameToDecl := map.insert fvarId decl, decls := decls.push decl }
+  { fvarIdToDecl := map.insert fvarId decl, decls := decls.push decl }
 
 @[export lean_local_ctx_find]
-def find (lctx : LocalContext) (fvarId : Name) : Option LocalDecl :=
-lctx.nameToDecl.find fvarId
+def find (lctx : LocalContext) (fvarId : FVarId) : Option LocalDecl :=
+lctx.fvarIdToDecl.find fvarId
 
 def findFVar (lctx : LocalContext) (e : Expr) : Option LocalDecl :=
 lctx.find e.fvarId!
 
-def contains (lctx : LocalContext) (fvarId : Name) : Bool :=
-lctx.nameToDecl.contains fvarId
+def contains (lctx : LocalContext) (fvarId : FVarId) : Bool :=
+lctx.fvarIdToDecl.contains fvarId
 
 def containsFVar (lctx : LocalContext) (e : Expr) : Bool :=
 lctx.contains e.fvarId!
@@ -114,21 +114,21 @@ private partial def popTailNoneAux : PArray (Option LocalDecl) → PArray (Optio
     | some _ => a
 
 @[export lean_local_ctx_erase]
-def erase (lctx : LocalContext) (fvarId : Name) : LocalContext :=
+def erase (lctx : LocalContext) (fvarId : FVarId) : LocalContext :=
 match lctx with
-| { nameToDecl := map, decls := decls } =>
+| { fvarIdToDecl := map, decls := decls } =>
   match map.find fvarId with
   | none      => lctx
-  | some decl => { nameToDecl := map.erase fvarId, decls := popTailNoneAux (decls.set decl.index none) }
+  | some decl => { fvarIdToDecl := map.erase fvarId, decls := popTailNoneAux (decls.set decl.index none) }
 
 @[export lean_local_ctx_pop]
 def pop (lctx : LocalContext): LocalContext :=
 match lctx with
-| { nameToDecl := map, decls := decls } =>
+| { fvarIdToDecl := map, decls := decls } =>
   if decls.size == 0 then lctx
   else match decls.get! (decls.size - 1) with
     | none      => lctx -- unreachable
-    | some decl => { nameToDecl := map.erase decl.name, decls := popTailNoneAux decls.pop }
+    | some decl => { fvarIdToDecl := map.erase decl.fvarId, decls := popTailNoneAux decls.pop }
 
 @[export lean_local_ctx_find_from_user_name]
 def findFromUserName (lctx : LocalContext) (userName : Name) : Option LocalDecl :=
@@ -159,13 +159,13 @@ lctx.decls.get! (lctx.decls.size - 1)
 @[export lean_local_ctx_rename_user_name]
 def renameUserName (lctx : LocalContext) (fromName : Name) (toName : Name) : LocalContext :=
 match lctx with
-| { nameToDecl := map, decls := decls } =>
+| { fvarIdToDecl := map, decls := decls } =>
   match lctx.findFromUserName fromName with
   | none      => lctx
   | some decl =>
     let decl := decl.updateUserName toName;
-    { nameToDecl := map.insert decl.name decl,
-      decls      := decls.set decl.index decl }
+    { fvarIdToDecl := map.insert decl.fvarId decl,
+      decls        := decls.set decl.index decl }
 
 @[export lean_local_ctx_num_indices]
 def numIndices (lctx : LocalContext) : Nat :=
@@ -231,7 +231,7 @@ partial def isSubPrefixOfAux (a₁ a₂ : PArray (Option LocalDecl)) : Nat → N
       match a₂.get! j with
       | none => isSubPrefixOfAux i (j+1)
       | some decl₂ =>
-        if decl₁.name == decl₂.name then isSubPrefixOfAux (i+1) (j+1) else isSubPrefixOfAux i (j+1)
+        if decl₁.fvarId == decl₂.fvarId then isSubPrefixOfAux (i+1) (j+1) else isSubPrefixOfAux i (j+1)
   else false
   else true
 
diff --git a/src/Init/Lean/Meta/Basic.lean b/src/Init/Lean/Meta/Basic.lean
index ca813510c9..953b97b7e4 100644
--- a/src/Init/Lean/Meta/Basic.lean
+++ b/src/Init/Lean/Meta/Basic.lean
@@ -257,38 +257,38 @@ adaptReader
     { config := { transparency := mode, .. ctx.config }, .. ctx })
   x
 
-def isSyntheticExprMVar (mvarId : Name) : MetaM Bool :=
+def isSyntheticExprMVar (mvarId : MVarId) : MetaM Bool :=
 do mctx ← getMCtx;
    match mctx.findDecl mvarId with
    | some d => pure $ d.synthetic
    | _      => throwEx $ Exception.unknownExprMVar mvarId
 
-def isReadOnlyExprMVar (mvarId : Name) : MetaM Bool :=
+def isReadOnlyExprMVar (mvarId : MVarId) : MetaM Bool :=
 do mctx ← getMCtx;
    match mctx.findDecl mvarId with
    | some d => pure $ d.depth != mctx.depth
    | _      => throwEx $ Exception.unknownExprMVar mvarId
 
-def isReadOnlyOrSyntheticExprMVar (mvarId : Name) : MetaM Bool :=
+def isReadOnlyOrSyntheticExprMVar (mvarId : MVarId) : MetaM Bool :=
 do mctx ← getMCtx;
    match mctx.findDecl mvarId with
    | some d => pure $ d.synthetic || d.depth != mctx.depth
    | _      => throwEx $ Exception.unknownExprMVar mvarId
 
-def isReadOnlyLevelMVar (mvarId : Name) : MetaM Bool :=
+def isReadOnlyLevelMVar (mvarId : MVarId) : MetaM Bool :=
 do mctx ← getMCtx;
    match mctx.findLevelDepth mvarId with
    | some depth => pure $ depth != mctx.depth
    | _          => throwEx $ Exception.unknownLevelMVar mvarId
 
-@[inline] def isExprMVarAssigned (mvarId : Name) : MetaM Bool :=
+@[inline] def isExprMVarAssigned (mvarId : MVarId) : MetaM Bool :=
 do mctx ← getMCtx;
    pure $ mctx.isExprAssigned mvarId
 
-@[inline] def getExprMVarAssignment (mvarId : Name) : MetaM (Option Expr) :=
+@[inline] def getExprMVarAssignment (mvarId : MVarId) : MetaM (Option Expr) :=
 do mctx ← getMCtx; pure (mctx.getExprAssignment mvarId)
 
-def assignExprMVar (mvarId : Name) (val : Expr) : MetaM Unit :=
+def assignExprMVar (mvarId : MVarId) (val : Expr) : MetaM Unit :=
 do whenDebugging $ whenM (isExprMVarAssigned mvarId) $ throwBug $ Bug.overwritingExprMVar mvarId;
    modify $ fun s => { mctx := s.mctx.assignExpr mvarId val, .. s }
 
@@ -329,7 +329,7 @@ getConstAux constName true
 @[inline] def getConstNoEx (constName : Name) : MetaM (Option ConstantInfo) :=
 getConstAux constName false
 
-def getLocalDecl (fvarId : Name) : MetaM LocalDecl :=
+def getLocalDecl (fvarId : FVarId) : MetaM LocalDecl :=
 do lctx ← getLCtx;
    match lctx.find fvarId with
    | some d => pure d
@@ -635,10 +635,10 @@ fun _ s =>
 def instantiateLevelMVars (lvl : Level) : MetaM Level :=
 liftStateMCtx $ MetavarContext.instantiateLevelMVars lvl
 
-def assignLevelMVar (mvarId : Name) (lvl : Level) : MetaM Unit :=
+def assignLevelMVar (mvarId : MVarId) (lvl : Level) : MetaM Unit :=
 modify $ fun s => { mctx := MetavarContext.assignLevel s.mctx mvarId lvl, .. s }
 
-def mkFreshLevelMVarId : MetaM Name :=
+def mkFreshLevelMVarId : MetaM MVarId :=
 do mvarId ← mkFreshId;
    modify $ fun s => { mctx := s.mctx.addLevelMVarDecl mvarId, .. s };
    pure mvarId
diff --git a/src/Init/Lean/Meta/DiscrTree.lean b/src/Init/Lean/Meta/DiscrTree.lean
index 71c117cbe7..7633d7c20b 100644
--- a/src/Init/Lean/Meta/DiscrTree.lean
+++ b/src/Init/Lean/Meta/DiscrTree.lean
@@ -53,7 +53,7 @@ namespace DiscrTree
 
 inductive Key
 | const : Name → Nat → Key
-| fvar  : Name → Nat → Key
+| fvar  : FVarId → Nat → Key
 | lit   : Literal → Key
 | star  : Key
 | other : Key
@@ -127,7 +127,7 @@ def empty {α} : DiscrTree α := { root := {} }
 
 /- The discrimination tree ignores implicit arguments and proofs.
    We use the following auxiliary id as a "mark". -/
-private def tmpMVarId : Name := `_discr_tree_tmp
+private def tmpMVarId : MVarId := `_discr_tree_tmp
 private def tmpStar := mkMVar tmpMVarId
 
 instance {α} : Inhabited (DiscrTree α) := ⟨{}⟩
diff --git a/src/Init/Lean/Meta/Exception.lean b/src/Init/Lean/Meta/Exception.lean
index d9dead3c64..6d3614dfd8 100644
--- a/src/Init/Lean/Meta/Exception.lean
+++ b/src/Init/Lean/Meta/Exception.lean
@@ -19,18 +19,18 @@ inductive Bug
 
 inductive Exception
 | unknownConst         (constName : Name) (ctx : ExceptionContext)
-| unknownFVar          (fvarId : Name) (ctx : ExceptionContext)
-| unknownExprMVar      (mvarId : Name) (ctx : ExceptionContext)
-| unknownLevelMVar     (mvarId : Name) (ctx : ExceptionContext)
+| unknownFVar          (fvarId : FVarId) (ctx : ExceptionContext)
+| unknownExprMVar      (mvarId : MVarId) (ctx : ExceptionContext)
+| unknownLevelMVar     (mvarId : MVarId) (ctx : ExceptionContext)
 | unexpectedBVar       (bvarIdx : Nat)
 | functionExpected     (f a : Expr) (ctx : ExceptionContext)
 | typeExpected         (type : Expr) (ctx : ExceptionContext)
 | incorrectNumOfLevels (constName : Name) (constLvls : List Level) (ctx : ExceptionContext)
 | invalidProjection    (structName : Name) (idx : Nat) (s : Expr) (ctx : ExceptionContext)
 | revertFailure        (toRevert : Array Expr) (decl : LocalDecl) (ctx : ExceptionContext)
-| readOnlyMVar         (mvarId : Name) (ctx : ExceptionContext)
+| readOnlyMVar         (mvarId : MVarId) (ctx : ExceptionContext)
 | isDefEqStuck         (t s : Expr) (ctx : ExceptionContext)
-| letTypeMismatch      (fvarId : Name) (ctx : ExceptionContext)
+| letTypeMismatch      (fvarId : FVarId) (ctx : ExceptionContext)
 | appTypeMismatch      (f a : Expr) (ctx : ExceptionContext)
 | bug                  (b : Bug) (ctx : ExceptionContext)
 | other                (msg : String)
diff --git a/src/Init/Lean/Meta/ExprDefEq.lean b/src/Init/Lean/Meta/ExprDefEq.lean
index b373190188..c5dc5cc730 100644
--- a/src/Init/Lean/Meta/ExprDefEq.lean
+++ b/src/Init/Lean/Meta/ExprDefEq.lean
@@ -339,7 +339,7 @@ namespace CheckAssignment
 
 structure Context :=
 (lctx         : LocalContext)
-(mvarId       : Name)
+(mvarId       : MVarId)
 (mvarDecl     : MetavarDecl)
 (fvars        : Array Expr)
 (ctxApprox    : Bool)
@@ -348,10 +348,10 @@ structure Context :=
 inductive Exception
 | occursCheck
 | useFOApprox
-| outOfScopeFVar                     (fvarId : Name)
-| readOnlyMVarWithBiggerLCtx         (mvarId : Name)
-| mvarTypeNotWellFormedInSmallerLCtx (mvarId : Name)
-| unknownExprMVar                    (mvarId : Name)
+| outOfScopeFVar                     (fvarId : FVarId)
+| readOnlyMVarWithBiggerLCtx         (mvarId : MVarId)
+| mvarTypeNotWellFormedInSmallerLCtx (mvarId : MVarId)
+| unknownExprMVar                    (mvarId : MVarId)
 
 structure State :=
 (mctx  : MetavarContext)
@@ -435,7 +435,7 @@ partial def check : Expr → CheckAssignmentM Expr
 
 end CheckAssignment
 
-private def checkAssignmentFailure (mvarId : Name) (fvars : Array Expr) (v : Expr) (ex : CheckAssignment.Exception) : MetaM (Option Expr) :=
+private def checkAssignmentFailure (mvarId : MVarId) (fvars : Array Expr) (v : Expr) (ex : CheckAssignment.Exception) : MetaM (Option Expr) :=
 match ex with
 | CheckAssignment.Exception.occursCheck => do
   trace `Meta.isDefEq.assign.occursCheck $ fun _ => mkMVar mvarId ++ fvars ++ " := " ++ v;
@@ -462,7 +462,7 @@ if !e.hasExprMVar && !e.hasFVar then true else f e
 
 partial def check
     (hasCtxLocals ctxApprox : Bool)
-    (mctx : MetavarContext) (lctx : LocalContext) (mvarDecl : MetavarDecl) (mvarId : Name) (fvars : Array Expr) : Expr → Bool
+    (mctx : MetavarContext) (lctx : LocalContext) (mvarDecl : MetavarDecl) (mvarId : MVarId) (fvars : Array Expr) : Expr → Bool
 | e@(Expr.mdata _ b _)     => check b
 | e@(Expr.proj _ _ s _)    => check s
 | e@(Expr.app f a _)       => visit check f && visit check a
@@ -506,7 +506,7 @@ end CheckAssignmentQuick
   The result is `none` if the assignment can't be performed.
   The result is `some newV` where `newV` is a possibly updated `v`. This method may need
   to unfold let-declarations. -/
-def checkAssignment (mvarId : Name) (fvars : Array Expr) (v : Expr) : MetaM (Option Expr) :=
+def checkAssignment (mvarId : MVarId) (fvars : Array Expr) (v : Expr) : MetaM (Option Expr) :=
 fun ctx s => if !v.hasExprMVar && !v.hasFVar then EStateM.Result.ok (some v) s else
   let mvarDecl     := s.mctx.getDecl mvarId;
   let hasCtxLocals := fvars.any $ fun fvar => mvarDecl.lctx.containsFVar fvar;
@@ -885,7 +885,7 @@ match t.etaExpanded? with
 | some t => t == s
 | none   => false
 
-private def isLetFVar (fvarId : Name) : MetaM Bool :=
+private def isLetFVar (fvarId : FVarId) : MetaM Bool :=
 do decl ← getLocalDecl fvarId;
    pure decl.isLet
 
diff --git a/src/Init/Lean/Meta/InferType.lean b/src/Init/Lean/Meta/InferType.lean
index 7fe7750be7..c3e7b52308 100644
--- a/src/Init/Lean/Meta/InferType.lean
+++ b/src/Init/Lean/Meta/InferType.lean
@@ -104,13 +104,13 @@ savingCache $ do
   adaptReader (fun (ctx : Context) => { lctx := ctx.lctx.mkLocalDecl fvarId name type bi, .. ctx }) $
     x (mkFVar fvarId)
 
-private def inferMVarType (mvarId : Name) : MetaM Expr :=
+private def inferMVarType (mvarId : MVarId) : MetaM Expr :=
 do mctx ← getMCtx;
    match mctx.findDecl mvarId with
    | some d => pure d.type
    | none   => throwEx $ Exception.unknownExprMVar mvarId
 
-private def inferFVarType (fvarId : Name) : MetaM Expr :=
+private def inferFVarType (fvarId : FVarId) : MetaM Expr :=
 do lctx ← getLCtx;
    match lctx.find fvarId with
    | some d => pure d.type
diff --git a/src/Init/Lean/Meta/LevelDefEq.lean b/src/Init/Lean/Meta/LevelDefEq.lean
index 3e52a3a3d3..6374137577 100644
--- a/src/Init/Lean/Meta/LevelDefEq.lean
+++ b/src/Init/Lean/Meta/LevelDefEq.lean
@@ -21,7 +21,7 @@ private def strictOccursMax (lvl : Level) : Level → Bool
 | _               => false
 
 /-- `mkMaxArgsDiff mvarId (max u_1 ... (mvar mvarId) ... u_n) v` => `max v u_1 ... u_n` -/
-private def mkMaxArgsDiff (mvarId : Name) : Level → Level → Level
+private def mkMaxArgsDiff (mvarId : MVarId) : Level → Level → Level
 | Level.max u v _,     acc => mkMaxArgsDiff v $ mkMaxArgsDiff u acc
 | l@(Level.mvar id _), acc => if id != mvarId then mkLevelMax acc l else acc
 | l,                   acc => mkLevelMax acc l
@@ -29,9 +29,9 @@ private def mkMaxArgsDiff (mvarId : Name) : Level → Level → Level
 /--
   Solve `?m =?= max ?m v` by creating a fresh metavariable `?n`
   and assigning `?m := max ?n v` -/
-private def solveSelfMax (mId : Name) (v : Level) : MetaM Unit :=
+private def solveSelfMax (mvarId : MVarId) (v : Level) : MetaM Unit :=
 do n ← mkFreshLevelMVar;
-   assignLevelMVar mId $ mkMaxArgsDiff mId v n
+   assignLevelMVar mvarId $ mkMaxArgsDiff mvarId v n
 
 private def postponeIsLevelDefEq (lhs : Level) (rhs : Level) : MetaM Unit :=
 modify $ fun s => { postponed := s.postponed.push { lhs := lhs, rhs := rhs }, .. s }
diff --git a/src/Init/Lean/MetavarContext.lean b/src/Init/Lean/MetavarContext.lean
index ead7aa352b..8d93b64c81 100644
--- a/src/Init/Lean/MetavarContext.lean
+++ b/src/Init/Lean/MetavarContext.lean
@@ -222,11 +222,11 @@ structure DelayedMetavarAssignment :=
 
 structure MetavarContext :=
 (depth       : Nat := 0)
-(lDepth      : PersistentHashMap Name Nat := {})
-(decls       : PersistentHashMap Name MetavarDecl := {})
-(lAssignment : PersistentHashMap Name Level := {})
-(eAssignment : PersistentHashMap Name Expr := {})
-(dAssignment : PersistentHashMap Name DelayedMetavarAssignment := {})
+(lDepth      : PersistentHashMap MVarId Nat := {})
+(decls       : PersistentHashMap MVarId MetavarDecl := {})
+(lAssignment : PersistentHashMap MVarId Level := {})
+(eAssignment : PersistentHashMap MVarId Expr := {})
+(dAssignment : PersistentHashMap MVarId DelayedMetavarAssignment := {})
 
 namespace MetavarContext
 
@@ -238,10 +238,10 @@ fun _ => {}
 
 /- Low level API for adding/declaring metavariable declarations.
    It is used to implement actions in the monads `MetaM`, `ElabM` and `TacticM`.
-   It should not be used directly since the argument `(mvarId : Name)` is assumed to be "unique". -/
+   It should not be used directly since the argument `(mvarId : MVarId)` is assumed to be "unique". -/
 @[export lean_metavar_ctx_mk_decl]
 def addExprMVarDecl (mctx : MetavarContext)
-    (mvarId : Name)
+    (mvarId : MVarId)
     (userName : Name)
     (lctx : LocalContext)
     (localInstances : LocalInstances)
@@ -257,74 +257,74 @@ def addExprMVarDecl (mctx : MetavarContext)
 
 /- Low level API for adding/declaring universe level metavariable declarations.
    It is used to implement actions in the monads `MetaM`, `ElabM` and `TacticM`.
-   It should not be used directly since the argument `(mvarId : Name)` is assumed to be "unique". -/
-def addLevelMVarDecl (mctx : MetavarContext) (mvarId : Name) : MetavarContext :=
+   It should not be used directly since the argument `(mvarId : MVarId)` is assumed to be "unique". -/
+def addLevelMVarDecl (mctx : MetavarContext) (mvarId : MVarId) : MetavarContext :=
 { lDepth := mctx.lDepth.insert mvarId mctx.depth,
   .. mctx }
 
 @[export lean_metavar_ctx_find_decl]
-def findDecl (mctx : MetavarContext) (mvarId : Name) : Option MetavarDecl :=
+def findDecl (mctx : MetavarContext) (mvarId : MVarId) : Option MetavarDecl :=
 mctx.decls.find mvarId
 
-def getDecl (mctx : MetavarContext) (mvarId : Name) : MetavarDecl :=
+def getDecl (mctx : MetavarContext) (mvarId : MVarId) : MetavarDecl :=
 match mctx.decls.find mvarId with
 | some decl => decl
 | none      => panic! "unknown metavariable"
 
-def findLevelDepth (mctx : MetavarContext) (mvarId : Name) : Option Nat :=
+def findLevelDepth (mctx : MetavarContext) (mvarId : MVarId) : Option Nat :=
 mctx.lDepth.find mvarId
 
-def getLevelDepth (mctx : MetavarContext) (mvarId : Name) : Nat :=
+def getLevelDepth (mctx : MetavarContext) (mvarId : MVarId) : Nat :=
 match mctx.findLevelDepth mvarId with
 | some d => d
 | none   => panic! "unknown metavariable"
 
 @[export lean_metavar_ctx_assign_level]
-def assignLevel (m : MetavarContext) (mvarId : Name) (val : Level) : MetavarContext :=
+def assignLevel (m : MetavarContext) (mvarId : MVarId) (val : Level) : MetavarContext :=
 { lAssignment := m.lAssignment.insert mvarId val, .. m }
 
 @[export lean_metavar_ctx_assign_expr]
-def assignExpr (m : MetavarContext) (mvarId : Name) (val : Expr) : MetavarContext :=
+def assignExpr (m : MetavarContext) (mvarId : MVarId) (val : Expr) : MetavarContext :=
 { eAssignment := m.eAssignment.insert mvarId val, .. m }
 
 @[export lean_metavar_ctx_assign_delayed]
-def assignDelayed (m : MetavarContext) (mvarId : Name) (lctx : LocalContext) (fvars : Array Expr) (val : Expr) : MetavarContext :=
+def assignDelayed (m : MetavarContext) (mvarId : MVarId) (lctx : LocalContext) (fvars : Array Expr) (val : Expr) : MetavarContext :=
 { dAssignment := m.dAssignment.insert mvarId { lctx := lctx, fvars := fvars, val := val }, .. m }
 
 @[export lean_metavar_ctx_get_level_assignment]
-def getLevelAssignment (m : MetavarContext) (mvarId : Name) : Option Level :=
+def getLevelAssignment (m : MetavarContext) (mvarId : MVarId) : Option Level :=
 m.lAssignment.find mvarId
 
 @[export lean_metavar_ctx_get_expr_assignment]
-def getExprAssignment (m : MetavarContext) (mvarId : Name) : Option Expr :=
+def getExprAssignment (m : MetavarContext) (mvarId : MVarId) : Option Expr :=
 m.eAssignment.find mvarId
 
 @[export lean_metavar_ctx_get_delayed_assignment]
-def getDelayedAssignment (m : MetavarContext) (mvarId : Name) : Option DelayedMetavarAssignment :=
+def getDelayedAssignment (m : MetavarContext) (mvarId : MVarId) : Option DelayedMetavarAssignment :=
 m.dAssignment.find mvarId
 
 @[export lean_metavar_ctx_is_level_assigned]
-def isLevelAssigned (m : MetavarContext) (mvarId : Name) : Bool :=
+def isLevelAssigned (m : MetavarContext) (mvarId : MVarId) : Bool :=
 m.lAssignment.contains mvarId
 
 @[export lean_metavar_ctx_is_expr_assigned]
-def isExprAssigned (m : MetavarContext) (mvarId : Name) : Bool :=
+def isExprAssigned (m : MetavarContext) (mvarId : MVarId) : Bool :=
 m.eAssignment.contains mvarId
 
 @[export lean_metavar_ctx_is_delayed_assigned]
-def isDelayedAssigned (m : MetavarContext) (mvarId : Name) : Bool :=
+def isDelayedAssigned (m : MetavarContext) (mvarId : MVarId) : Bool :=
 m.dAssignment.contains mvarId
 
 @[export lean_metavar_ctx_erase_delayed]
-def eraseDelayed (m : MetavarContext) (mvarId : Name) : MetavarContext :=
+def eraseDelayed (m : MetavarContext) (mvarId : MVarId) : MetavarContext :=
 { dAssignment := m.dAssignment.erase mvarId, .. m }
 
-def isLevelAssignable (mctx : MetavarContext) (mvarId : Name) : Bool :=
+def isLevelAssignable (mctx : MetavarContext) (mvarId : MVarId) : Bool :=
 match mctx.lDepth.find mvarId with
 | some d => d == mctx.depth
 | _      => panic! "unknown universe metavariable"
 
-def isExprAssignable (mctx : MetavarContext) (mvarId : Name) : Bool :=
+def isExprAssignable (mctx : MetavarContext) (mvarId : MVarId) : Bool :=
 let decl := mctx.getDecl mvarId;
 decl.depth == mctx.depth
 
@@ -424,7 +424,7 @@ modify $ fun s => { state := f s.state, .. s }
         instantiateDelayedAux i (mkLet n ty val b)
 
 /-- Try to instantiate a delayed assignment. Return `none` (i.e., fail) if assignment still contains variables. -/
-@[inline] private def instantiateDelayed (main : Expr → M Expr) (mvarId : Name) : DelayedMetavarAssignment → M (Option Expr)
+@[inline] private def instantiateDelayed (main : Expr → M Expr) (mvarId : MVarId) : DelayedMetavarAssignment → M (Option Expr)
 | { lctx := lctx, fvars := fvars, val := val } => do
   newVal ← visit main val;
   let fail : M (Option Expr) := do {
@@ -504,7 +504,7 @@ else do
 @[inline] private def visit (main : Expr → M Bool) (e : Expr) : M Bool :=
 condM (visit? e) (main e) (pure false)
 
-@[specialize] private partial def dep (mctx : MetavarContext) (p : Name → Bool) : Expr → M Bool
+@[specialize] private partial def dep (mctx : MetavarContext) (p : FVarId → Bool) : Expr → M Bool
 | e@(Expr.proj _ _ s _)    => visit dep s
 | e@(Expr.forallE _ d b _) => visit dep d <||> visit dep b
 | e@(Expr.lam _ d b _)     => visit dep d <||> visit dep b
@@ -516,11 +516,11 @@ condM (visit? e) (main e) (pure false)
   | some a => visit dep a
   | none   =>
     let lctx := (mctx.getDecl mvarId).lctx;
-    pure $ lctx.any $ fun decl => p decl.name
+    pure $ lctx.any $ fun decl => p decl.fvarId
 | e@(Expr.fvar fvarId _)   => pure $ p fvarId
 | e                        => pure false
 
-@[inline] partial def main (mctx : MetavarContext) (p : Name → Bool) (e : Expr) : M Bool :=
+@[inline] partial def main (mctx : MetavarContext) (p : FVarId → Bool) (e : Expr) : M Bool :=
 if !e.hasFVar && !e.hasMVar then pure false else dep mctx p e
 
 end DependsOn
@@ -531,13 +531,13 @@ end DependsOn
   1- If `?m := t`, then we visit `t` looking for `x`
   2- If `?m` is unassigned, then we consider the worst case and check whether `x` is in the local context of `?m`.
      This case is a "may dependency". That is, we may assign a term `t` to `?m` s.t. `t` contains `x`. -/
-@[inline] def exprDependsOn (mctx : MetavarContext) (p : Name → Bool) (e : Expr) : Bool :=
+@[inline] def exprDependsOn (mctx : MetavarContext) (p : FVarId → Bool) (e : Expr) : Bool :=
 (DependsOn.main mctx p e).run' {}
 
 /--
   Similar to `exprDependsOn`, but checks the expressions in the given local declaration
   depends on a free variable `x` s.t. `p x` is `true`. -/
-@[inline] def localDeclDependsOn (mctx : MetavarContext) (p : Name → Bool) : LocalDecl → Bool
+@[inline] def localDeclDependsOn (mctx : MetavarContext) (p : FVarId → Bool) : LocalDecl → Bool
 | LocalDecl.cdecl _ _ _ type _     => exprDependsOn mctx p type
 | LocalDecl.ldecl _ _ _ type value => (DependsOn.main mctx p type <||> DependsOn.main mctx p value).run' {}
 
@@ -545,7 +545,7 @@ namespace MkBinding
 
 inductive Exception
 | revertFailure (mctx : MetavarContext) (lctx : LocalContext) (toRevert : Array Expr) (decl : LocalDecl)
-| readOnlyMVar (mctx : MetavarContext) (mvarId : Name)
+| readOnlyMVar (mctx : MetavarContext) (mvarId : MVarId)
 
 def Exception.toString : Exception → String
 | Exception.revertFailure _ lctx toRevert decl =>
@@ -632,7 +632,7 @@ else
   let minDecl := getLocalDeclWithSmallestIdx lctx toRevert;
   lctx.foldlFromM
     (fun newToRevert decl =>
-      if toRevert.any (fun x => decl.name == x.fvarId!) then
+      if toRevert.any (fun x => decl.fvarId == x.fvarId!) then
         pure (newToRevert.push decl.toExpr)
       else if localDeclDependsOn mctx (fun fvarId => newToRevert.any $ fun x => x.fvarId! == fvarId) decl then
         if decl.binderInfo.isAuxDecl then
@@ -689,7 +689,7 @@ mkForall
 private def mkMVarApp (lctx : LocalContext) (mvar : Expr) (xs : Array Expr) : Expr :=
 xs.foldl (fun e x => if (lctx.findFVar x).get!.isLet then e else mkApp e x) mvar
 
-private def mkAuxMVar (lctx : LocalContext) (localInsts : LocalInstances) (type : Expr) (synthetic : Bool) : M Name :=
+private def mkAuxMVar (lctx : LocalContext) (localInsts : LocalInstances) (type : Expr) (synthetic : Bool) : M MVarId :=
 do s ← get;
    let mvarId := s.ngen.curr;
    modify $ fun s => { mctx := s.mctx.addExprMVarDecl mvarId Name.anonymous lctx localInsts type synthetic, ngen := s.ngen.next, .. s };
diff --git a/src/Init/Lean/WHNF.lean b/src/Init/Lean/WHNF.lean
index 4cd439d094..f056fecf1b 100644
--- a/src/Init/Lean/WHNF.lean
+++ b/src/Init/Lean/WHNF.lean
@@ -277,8 +277,8 @@ else
     (whnf              : Expr → m Expr)
     (inferType         : Expr → m Expr)
     (isDefEq           : Expr → Expr → m Bool)
-    (getLocalDecl      : Name → m LocalDecl)
-    (getMVarAssignment : Name → m (Option Expr)) : Expr → m Expr
+    (getLocalDecl      : FVarId → m LocalDecl)
+    (getMVarAssignment : MVarId → m (Option Expr)) : Expr → m Expr
 | e => whnfEasyCases getLocalDecl getMVarAssignment e $ fun e =>
   match e with
   | e@(Expr.const _ _ _)    => pure e
@@ -321,8 +321,8 @@ else
     (inferType         : Expr → m Expr)
     (isDefEq           : Expr → Expr → m Bool)
     (synthesizePending : Expr → m Bool)
-    (getLocalDecl      : Name → m LocalDecl)
-    (getMVarAssignment : Name → m (Option Expr))
+    (getLocalDecl      : FVarId → m LocalDecl)
+    (getMVarAssignment : MVarId → m (Option Expr))
     : Expr → m Expr
 | e => do
   e ← whnfCore getConst isAuxDef? whnf inferType isDefEq getLocalDecl getMVarAssignment e;
@@ -338,8 +338,8 @@ else
     (inferType         : Expr → m Expr)
     (isDefEq           : Expr → Expr → m Bool)
     (synthesizePending : Expr → m Bool)
-    (getLocalDecl      : Name → m LocalDecl)
-    (getMVarAssignment : Name → m (Option Expr))
+    (getLocalDecl      : FVarId → m LocalDecl)
+    (getMVarAssignment : MVarId → m (Option Expr))
     (e : Expr) : m (Option Expr) :=
 match e with
 | Expr.app f _ _ =>
@@ -380,8 +380,8 @@ match e with
     (inferType         : Expr → m Expr)
     (isDefEq           : Expr → Expr → m Bool)
     (synthesizePending : Expr → m Bool)
-    (getLocalDecl      : Name → m LocalDecl)
-    (getMVarAssignment : Name → m (Option Expr))
+    (getLocalDecl      : FVarId → m LocalDecl)
+    (getMVarAssignment : MVarId → m (Option Expr))
     : Expr → m Expr
 | e => do
   e ← whnfCore getConst isAuxDef? whnfMain inferType isDefEq getLocalDecl getMVarAssignment e;