diff --git a/src/Lean/Compiler/IR/ToIR.lean b/src/Lean/Compiler/IR/ToIR.lean
index 552814e4a8..7fdab2bff3 100644
--- a/src/Lean/Compiler/IR/ToIR.lean
+++ b/src/Lean/Compiler/IR/ToIR.lean
@@ -101,14 +101,14 @@ partial def lowerCode (c : LCNF.Code .impure) : M FnBody := do
     let ret ← getFVarValue fvarId
     return .ret ret
   | .unreach .. => return .unreachable
-  | .sset var i offset y type k _ =>
+  | .sset fvarId i offset y type k _ =>
     let .var y ← getFVarValue y | unreachable!
-    let .var var ← getFVarValue var | unreachable!
-    return .sset var i offset y (toIRType type) (← lowerCode k)
-  | .uset var i y k _ =>
+    let .var fvarId ← getFVarValue fvarId | unreachable!
+    return .sset fvarId i offset y (toIRType type) (← lowerCode k)
+  | .uset fvarId i y k _ =>
     let .var y ← getFVarValue y | unreachable!
-    let .var var ← getFVarValue var | unreachable!
-    return .uset var i y (← lowerCode k)
+    let .var fvarId ← getFVarValue fvarId | unreachable!
+    return .uset fvarId i y (← lowerCode k)
   | .inc fvarId n check persistent k _ =>
     let .var var ← getFVarValue fvarId | unreachable!
     return .inc var n check persistent (← lowerCode k)
diff --git a/src/Lean/Compiler/LCNF/AlphaEqv.lean b/src/Lean/Compiler/LCNF/AlphaEqv.lean
index 16490b22b6..ddf835ad84 100644
--- a/src/Lean/Compiler/LCNF/AlphaEqv.lean
+++ b/src/Lean/Compiler/LCNF/AlphaEqv.lean
@@ -143,16 +143,16 @@ partial def eqv (code₁ code₂ : Code pu) : EqvM Bool := do
     eqvFVar c₁.discr c₂.discr <&&>
     eqvType c₁.resultType c₂.resultType <&&>
     eqvAlts c₁.alts c₂.alts
-  | .sset var₁ i₁ offset₁ y₁ ty₁ k₁ _, .sset var₂ i₂ offset₂ y₂ ty₂ k₂ _ =>
+  | .sset fvarId₁ i₁ offset₁ y₁ ty₁ k₁ _, .sset fvarId₂ i₂ offset₂ y₂ ty₂ k₂ _ =>
     pure (i₁ == i₂) <&&>
     pure (offset₁ == offset₂) <&&>
-    eqvFVar var₁ var₂ <&&>
+    eqvFVar fvarId₁ fvarId₂ <&&>
     eqvFVar y₁ y₂ <&&>
     eqvType ty₁ ty₂ <&&>
     eqv k₁ k₂
-  | .uset var₁ i₁ y₁ k₁ _, .uset var₂ i₂ y₂ k₂ _ =>
+  | .uset fvarId₁ i₁ y₁ k₁ _, .uset fvarId₂ i₂ y₂ k₂ _ =>
     pure (i₁ == i₂) <&&>
-    eqvFVar var₁ var₂ <&&>
+    eqvFVar fvarId₁ fvarId₂ <&&>
     eqvFVar y₁ y₂ <&&>
     eqv k₁ k₂
   | .inc fvarId₁ n₁ c₁ p₁ k₁ _, .inc fvarId₂ n₂ c₂ p₂ k₂ _ =>
diff --git a/src/Lean/Compiler/LCNF/Basic.lean b/src/Lean/Compiler/LCNF/Basic.lean
index bf650656dd..aa910edebb 100644
--- a/src/Lean/Compiler/LCNF/Basic.lean
+++ b/src/Lean/Compiler/LCNF/Basic.lean
@@ -361,8 +361,8 @@ inductive Code (pu : Purity) where
   | cases (cases : Cases pu)
   | return (fvarId : FVarId)
   | unreach (type : Expr)
-  | uset (var : FVarId) (i : Nat) (y : FVarId) (k : Code pu) (h : pu = .impure := by purity_tac)
-  | sset (var : FVarId) (i : Nat) (offset : Nat) (y : FVarId) (ty : Expr) (k : Code pu) (h : pu = .impure := by purity_tac)
+  | uset (fvarId : FVarId) (i : Nat) (y : FVarId) (k : Code pu) (h : pu = .impure := by purity_tac)
+  | sset (fvarId : FVarId) (i : Nat) (offset : Nat) (y : FVarId) (ty : Expr) (k : Code pu) (h : pu = .impure := by purity_tac)
   | inc (fvarId : FVarId) (n : Nat) (check : Bool) (persistent : Bool) (k : Code pu) (h : pu = .impure := by purity_tac)
   | dec (fvarId : FVarId) (n : Nat) (check : Bool) (persistent : Bool) (k : Code pu) (h : pu = .impure := by purity_tac)
   deriving Inhabited
@@ -440,8 +440,8 @@ inductive CodeDecl (pu : Purity) where
   | let (decl : LetDecl pu)
   | fun (decl : FunDecl pu) (h : pu = .pure := by purity_tac)
   | jp (decl : FunDecl pu)
-  | uset (var : FVarId) (i : Nat) (y : FVarId) (h : pu = .impure := by purity_tac)
-  | sset (var : FVarId) (i : Nat) (offset : Nat) (y : FVarId)  (ty : Expr) (h : pu = .impure := by purity_tac)
+  | uset (fvarId : FVarId) (i : Nat) (y : FVarId) (h : pu = .impure := by purity_tac)
+  | sset (fvarId : FVarId) (i : Nat) (offset : Nat) (y : FVarId)  (ty : Expr) (h : pu = .impure := by purity_tac)
   | inc (fvarId : FVarId) (n : Nat) (check : Bool) (persistent : Bool) (h : pu = .impure := by purity_tac)
   | dec (fvarId : FVarId) (n : Nat) (check : Bool) (persistent : Bool) (h : pu = .impure := by purity_tac)
   deriving Inhabited
@@ -454,8 +454,8 @@ def Code.toCodeDecl! : Code pu → CodeDecl pu
 | .let decl _ => .let decl
 | .fun decl _ _ => .fun decl
 | .jp decl _ => .jp decl
-| .uset var i y _ _ => .uset var i y
-| .sset var i offset ty y _ _ => .sset var i offset ty y
+| .uset fvarId i y _ _ => .uset fvarId i y
+| .sset fvarId i offset ty y _ _ => .sset fvarId i offset ty y
 | .inc fvarId n check persistent _ _ => .inc fvarId n check persistent
 | .dec fvarId n check persistent _ _ => .dec fvarId n check persistent
 | _ => unreachable!
@@ -469,8 +469,8 @@ where
       | .let decl => go (i-1) (.let decl code)
       | .fun decl _ => go (i-1) (.fun decl code)
       | .jp decl => go (i-1) (.jp decl code)
-      | .uset var idx y _ => go (i-1) (.uset var idx y code)
-      | .sset var idx offset y ty _ => go (i-1) (.sset var idx offset y ty code)
+      | .uset fvarId idx y _ => go (i-1) (.uset fvarId idx y code)
+      | .sset fvarId idx offset y ty _ => go (i-1) (.sset fvarId idx offset y ty code)
       | .inc fvarId n check persistent _ => go (i-1) (.inc fvarId n check persistent code)
       | .dec fvarId n check persistent _ => go (i-1) (.dec fvarId n check persistent code)
     else
@@ -1078,8 +1078,8 @@ partial def Code.collectUsed (code : Code pu) (s : FVarIdHashSet := {}) : FVarId
   | .return fvarId => s.insert fvarId
   | .unreach type => collectType type s
   | .jmp fvarId args => collectArgs args <| s.insert fvarId
-  | .sset var _ _ y _ k _ | .uset var _ y k _ =>
-    let s := s.insert var
+  | .sset fvarId _ _ y _ k _ | .uset fvarId _ y k _ =>
+    let s := s.insert fvarId
     let s := s.insert y
     k.collectUsed s
   | .inc (fvarId := fvarId) (k := k) .. | .dec (fvarId := fvarId) (k := k) .. =>
@@ -1093,7 +1093,8 @@ def CodeDecl.collectUsed (codeDecl : CodeDecl pu) (s : FVarIdHashSet := ∅) : F
   match codeDecl with
   | .let decl => collectLetValue decl.value <| collectType decl.type s
   | .jp decl | .fun decl _ => decl.collectUsed s
-  | .sset (var := var) (y := y) .. | .uset (var := var) (y := y) .. => s.insert var |>.insert y
+  | .sset (fvarId := fvarId) (y := y) .. | .uset (fvarId := fvarId) (y := y) .. =>
+    s.insert fvarId |>.insert y
   | .inc (fvarId := fvarId) .. | .dec (fvarId := fvarId) .. => s.insert fvarId
 
 /--
diff --git a/src/Lean/Compiler/LCNF/DependsOn.lean b/src/Lean/Compiler/LCNF/DependsOn.lean
index f4ca834a5d..2f2fc4a022 100644
--- a/src/Lean/Compiler/LCNF/DependsOn.lean
+++ b/src/Lean/Compiler/LCNF/DependsOn.lean
@@ -66,8 +66,9 @@ def CodeDecl.dependsOn (decl : CodeDecl pu) (s : FVarIdSet) : Bool :=
   match decl with
   | .let decl => decl.dependsOn s
   | .jp decl | .fun decl _ => decl.dependsOn s
-  | .uset (var := var) (y := y) .. | .sset (var := var) (y := y) .. => s.contains var || s.contains y
-  | .inc (fvarId := fvarId) .. | .dec (fvarId := fvarId) .. => s.contains fvarId 
+  | .uset (fvarId := fvarId) (y := y) .. | .sset (fvarId := fvarId) (y := y) .. =>
+    s.contains fvarId || s.contains y
+  | .inc (fvarId := fvarId) .. | .dec (fvarId := fvarId) .. => s.contains fvarId
 
 /--
 Return `true` is `c` depends on a free variable in `s`.
diff --git a/src/Lean/Compiler/LCNF/ElimDead.lean b/src/Lean/Compiler/LCNF/ElimDead.lean
index 863624dde1..43343f3089 100644
--- a/src/Lean/Compiler/LCNF/ElimDead.lean
+++ b/src/Lean/Compiler/LCNF/ElimDead.lean
@@ -95,9 +95,9 @@ partial def Code.elimDead (code : Code pu) : M (Code pu) := do
   | .return fvarId => collectFVarM fvarId; return code
   | .jmp fvarId args => collectFVarM fvarId; args.forM collectArgM; return code
   | .unreach .. => return code
-  | .uset var _ y k _ | .sset var _ _ y _ k _ =>
+  | .uset fvarId _ y k _ | .sset fvarId _ _ y _ k _ =>
     let k ← k.elimDead
-    if (← get).contains var then
+    if (← get).contains fvarId then
       collectFVarM y
       return code.updateCont! k
     else
diff --git a/src/Lean/Compiler/LCNF/ExplicitBoxing.lean b/src/Lean/Compiler/LCNF/ExplicitBoxing.lean
index d35a1db04b..0133e1977f 100644
--- a/src/Lean/Compiler/LCNF/ExplicitBoxing.lean
+++ b/src/Lean/Compiler/LCNF/ExplicitBoxing.lean
@@ -274,14 +274,14 @@ partial def Code.explicitBoxing (code : Code .impure) : BoxM (Code .impure) := d
     let decl ← decl.update (← getResultType) decl.params value
     let k ← k.explicitBoxing
     return code.updateFun! decl k
-  | .uset var i y k _ =>
+  | .uset fvarId i y k _ =>
     let k ← k.explicitBoxing
     castVarIfNeeded y ImpureType.usize fun y =>
-      return code.updateUset! var i y k
-  | .sset var i offset y ty k _ =>
+      return code.updateUset! fvarId i y k
+  | .sset fvarId i offset y ty k _ =>
     let k ← k.explicitBoxing
     castVarIfNeeded y ty fun y =>
-      return code.updateSset! var i offset y ty k
+      return code.updateSset! fvarId i offset y ty k
   | .cases cs =>
     let alts ← cs.alts.mapMonoM (·.mapCodeM (·.explicitBoxing))
     castVarIfNeeded cs.discr (mkConst cs.typeName) fun discr =>
diff --git a/src/Lean/Compiler/LCNF/ExplicitRC.lean b/src/Lean/Compiler/LCNF/ExplicitRC.lean
index 785ae0c815..1be1eb3151 100644
--- a/src/Lean/Compiler/LCNF/ExplicitRC.lean
+++ b/src/Lean/Compiler/LCNF/ExplicitRC.lean
@@ -638,10 +638,10 @@ partial def Code.explicitRc (code : Code .impure) : RcM (Code .impure) := do
       addInc fvarId code
     else
       return code
-  | .uset (var := var) (k := k) .. | .sset (var := var) (k := k) .. =>
+  | .uset (fvarId := fvarId) (k := k) .. | .sset (fvarId := fvarId) (k := k) .. =>
     let k ← k.explicitRc
-    -- We don't need to insert `var` since we only need to track live variables that are references at runtime
-    useVar var
+    -- We don't need to insert `fvarId` since we only need to track live variables that are references at runtime
+    useVar fvarId
     return code.updateCont! k
   | .unreach .. =>
     setRetLiveVars
diff --git a/src/Lean/Compiler/LCNF/FVarUtil.lean b/src/Lean/Compiler/LCNF/FVarUtil.lean
index 27fe132b03..74247fa8be 100644
--- a/src/Lean/Compiler/LCNF/FVarUtil.lean
+++ b/src/Lean/Compiler/LCNF/FVarUtil.lean
@@ -209,8 +209,8 @@ instance : TraverseFVar (CodeDecl pu) where
     | .fun decl _ => return .fun (← mapFVarM f decl)
     | .jp decl => return .jp (← mapFVarM f decl)
     | .let decl => return .let (← mapFVarM f decl)
-    | .uset var i y _ => return .uset (← f var) i (← f y)
-    | .sset var i offset y ty _ => return .sset (← f var) i offset (← f y) (← mapFVarM f ty)
+    | .uset fvarId i y _ => return .uset (← f fvarId) i (← f y)
+    | .sset fvarId i offset y ty _ => return .sset (← f fvarId) i offset (← f y) (← mapFVarM f ty)
     | .inc fvarId n check persistent _ => return .inc (← f fvarId) n check persistent
     | .dec fvarId n check persistent _ => return .dec (← f fvarId) n check persistent
   forFVarM f decl :=
@@ -218,8 +218,8 @@ instance : TraverseFVar (CodeDecl pu) where
     | .fun decl _ => forFVarM f decl
     | .jp decl => forFVarM f decl
     | .let decl => forFVarM f decl
-    | .uset var i y _ => do f var; f y
-    | .sset var i offset y ty _ => do f var; f y; forFVarM f ty
+    | .uset fvarId i y _ => do f fvarId; f y
+    | .sset fvarId i offset y ty _ => do f fvarId; f y; forFVarM f ty
     | .inc (fvarId := fvarId) .. | .dec (fvarId := fvarId) .. => f fvarId
 
 instance : TraverseFVar (Alt pu) where
diff --git a/src/Lean/Compiler/LCNF/Internalize.lean b/src/Lean/Compiler/LCNF/Internalize.lean
index 07048ffc59..6c6d9766d4 100644
--- a/src/Lean/Compiler/LCNF/Internalize.lean
+++ b/src/Lean/Compiler/LCNF/Internalize.lean
@@ -180,16 +180,16 @@ partial def internalizeCodeDecl (decl : CodeDecl pu) : InternalizeM pu (CodeDecl
   | .let decl => return .let (← internalizeLetDecl decl)
   | .fun decl _ => return .fun (← internalizeFunDecl decl)
   | .jp decl => return .jp (← internalizeFunDecl decl)
-  | .uset var i y _ =>
+  | .uset fvarId i y _ =>
     -- Something weird should be happening if these become erased...
-    let .fvar var ← normFVar var | unreachable!
+    let .fvar fvarId ← normFVar fvarId | unreachable!
     let .fvar y ← normFVar y | unreachable!
-    return .uset var i y
-  | .sset var i offset y ty _ =>
-    let .fvar var ← normFVar var | unreachable!
+    return .uset fvarId i y
+  | .sset fvarId i offset y ty _ =>
+    let .fvar fvarId ← normFVar fvarId | unreachable!
     let .fvar y ← normFVar y | unreachable!
     let ty ← normExpr ty
-    return .sset var i offset y ty
+    return .sset fvarId i offset y ty
   | .inc fvarId n check offset _ =>
     let .fvar fvarId ← normFVar fvarId | unreachable!
     return .inc fvarId n check offset
diff --git a/src/Lean/Compiler/LCNF/LiveVars.lean b/src/Lean/Compiler/LCNF/LiveVars.lean
index db2f95db72..0db5e6158e 100644
--- a/src/Lean/Compiler/LCNF/LiveVars.lean
+++ b/src/Lean/Compiler/LCNF/LiveVars.lean
@@ -63,8 +63,8 @@ where
     match c with
     | .let decl k => (pure <| decl.dependsOn (← read).targetSet) <||> go k
     | .jp decl k => go decl.value <||> (do markJpVisited decl.fvarId; go k)
-    | .uset var _ y k _ | .sset var _ _ y _ k _ =>
-      visitVar var <||> visitVar y <||> go k
+    | .uset fvarId _ y k _ | .sset fvarId _ _ y _ k _ =>
+      visitVar fvarId <||> visitVar y <||> go k
     | .cases c => visitVar c.discr <||> c.alts.anyM (go ·.getCode)
     | .jmp fvarId args =>
       (pure <| args.any (·.dependsOn (← read).targetSet)) <||> do
diff --git a/src/Lean/Compiler/LCNF/PushProj.lean b/src/Lean/Compiler/LCNF/PushProj.lean
index 4c01cc3a79..1eed19bdaa 100644
--- a/src/Lean/Compiler/LCNF/PushProj.lean
+++ b/src/Lean/Compiler/LCNF/PushProj.lean
@@ -133,10 +133,10 @@ where
     | .jp decl k =>
       let decl ← decl.updateValue (← decl.value.pushProj)
       go k (decls.push (.jp decl))
-    | .uset var i y k _ =>
-      go k (decls.push (.uset var i y))
-    | .sset var i offset y ty k _ =>
-      go k (decls.push (.sset var i offset y ty))
+    | .uset fvarId i y k _ =>
+      go k (decls.push (.uset fvarId i y))
+    | .sset fvarId i offset y ty k _ =>
+      go k (decls.push (.sset fvarId i offset y ty))
     | .inc fvarId n check persistent k _ =>
       go k (decls.push (.inc fvarId n check persistent))
     | .dec fvarId n check persistent k _ =>