From 9d33f2ad338bf0966f0ce8ea2e43f6ec51090ca6 Mon Sep 17 00:00:00 2001
From: Cameron Zwarich <cameron@lean-fro.org>
Date: Mon, 14 Jul 2025 15:46:40 -0700
Subject: [PATCH] chore: make IR.Arg pattern matching more exhaustive (#9370)

---
 src/Lean/Compiler/IR/Boxing.lean           |  4 ++--
 src/Lean/Compiler/IR/Checker.lean          |  4 ++--
 src/Lean/Compiler/IR/ElimDeadBranches.lean |  4 ++--
 src/Lean/Compiler/IR/EmitC.lean            |  8 ++++----
 src/Lean/Compiler/IR/EmitLLVM.lean         |  4 ++--
 src/Lean/Compiler/IR/ExpandResetReuse.lean |  4 ++--
 src/Lean/Compiler/IR/FreeVars.lean         | 12 ++++++------
 src/Lean/Compiler/IR/LiveVars.lean         |  4 ++--
 src/Lean/Compiler/IR/NormIds.lean          |  8 ++++----
 9 files changed, 26 insertions(+), 26 deletions(-)

diff --git a/src/Lean/Compiler/IR/Boxing.lean b/src/Lean/Compiler/IR/Boxing.lean
index 6435a3e40f..2aa9e3f9c7 100644
--- a/src/Lean/Compiler/IR/Boxing.lean
+++ b/src/Lean/Compiler/IR/Boxing.lean
@@ -208,8 +208,8 @@ def mkCast (x : VarId) (xType : IRType) (expectedType : IRType) : M Expr := do
 
 @[inline] def castArgIfNeeded (x : Arg) (expected : IRType) (k : Arg → M FnBody) : M FnBody :=
   match x with
-  | Arg.var x => castVarIfNeeded x expected (fun x => k (Arg.var x))
-  | _         => k x
+  | .var x => castVarIfNeeded x expected (fun x => k (.var x))
+  | .erased => k x
 
 def castArgsIfNeededAux (xs : Array Arg) (typeFromIdx : Nat → IRType) : M (Array Arg × Array FnBody) := do
   let mut xs' := #[]
diff --git a/src/Lean/Compiler/IR/Checker.lean b/src/Lean/Compiler/IR/Checker.lean
index 9cdd9aefca..bfe208c365 100644
--- a/src/Lean/Compiler/IR/Checker.lean
+++ b/src/Lean/Compiler/IR/Checker.lean
@@ -69,8 +69,8 @@ def checkJP (j : JoinPointId) : M Unit := do
 
 def checkArg (a : Arg) : M Unit :=
   match a with
-  | Arg.var x => checkVar x
-  | _ => pure ()
+  | .var x => checkVar x
+  | .erased => pure ()
 
 def checkArgs (as : Array Arg) : M Unit :=
   as.forM checkArg
diff --git a/src/Lean/Compiler/IR/ElimDeadBranches.lean b/src/Lean/Compiler/IR/ElimDeadBranches.lean
index 6d21c67434..2bb5674775 100644
--- a/src/Lean/Compiler/IR/ElimDeadBranches.lean
+++ b/src/Lean/Compiler/IR/ElimDeadBranches.lean
@@ -158,8 +158,8 @@ def findVarValue (x : VarId) : M Value := do
 
 def findArgValue (arg : Arg) : M Value :=
   match arg with
-  | Arg.var x => findVarValue x
-  | _         => pure top
+  | .var x => findVarValue x
+  | .erased => pure top
 
 def updateVarAssignment (x : VarId) (v : Value) : M Unit := do
   let v' ← findVarValue x
diff --git a/src/Lean/Compiler/IR/EmitC.lean b/src/Lean/Compiler/IR/EmitC.lean
index 2cf7d62170..54e7f3a55f 100644
--- a/src/Lean/Compiler/IR/EmitC.lean
+++ b/src/Lean/Compiler/IR/EmitC.lean
@@ -47,8 +47,8 @@ def emitLns {α : Type} [ToString α] (as : List α) : M Unit :=
 
 def argToCString (x : Arg) : String :=
   match x with
-  | Arg.var x => toString x
-  | _         => "lean_box(0)"
+  | .var x => toString x
+  | .erased => "lean_box(0)"
 
 def emitArg (x : Arg) : M Unit :=
   emit (argToCString x)
@@ -540,8 +540,8 @@ def isTailCall (x : VarId) (v : Expr) (b : FnBody) : M Bool := do
 
 def paramEqArg (p : Param) (x : Arg) : Bool :=
   match x with
-  | Arg.var x => p.x == x
-  | _ => false
+  | .var x => p.x == x
+  | .erased => false
 
 /--
 Given `[p_0, ..., p_{n-1}]`, `[y_0, ..., y_{n-1}]`, representing the assignments
diff --git a/src/Lean/Compiler/IR/EmitLLVM.lean b/src/Lean/Compiler/IR/EmitLLVM.lean
index b2f99e3f54..63b8f05798 100644
--- a/src/Lean/Compiler/IR/EmitLLVM.lean
+++ b/src/Lean/Compiler/IR/EmitLLVM.lean
@@ -548,8 +548,8 @@ def emitLhsSlotStore (builder : LLVM.Builder llvmctx)
 def emitArgSlot_ (builder : LLVM.Builder llvmctx)
     (x : Arg) : M llvmctx (LLVM.LLVMType llvmctx × LLVM.Value llvmctx) := do
   match x with
-  | Arg.var x => emitLhsSlot_ x
-  | _ => do
+  | .var x => emitLhsSlot_ x
+  | .erased => do
     let slotty ← LLVM.voidPtrType llvmctx
     let slot ← buildPrologueAlloca builder slotty "erased_slot"
     let v ← callLeanBox builder (← constIntSizeT 0) "erased_val"
diff --git a/src/Lean/Compiler/IR/ExpandResetReuse.lean b/src/Lean/Compiler/IR/ExpandResetReuse.lean
index 080d234bd4..be0001c76d 100644
--- a/src/Lean/Compiler/IR/ExpandResetReuse.lean
+++ b/src/Lean/Compiler/IR/ExpandResetReuse.lean
@@ -147,11 +147,11 @@ def setFields (y : VarId) (zs : Array Arg) (b : FnBody) : FnBody :=
 /-- Given `set x[i] := y`, return true iff `y := proj[i] x` -/
 def isSelfSet (ctx : Context) (x : VarId) (i : Nat) (y : Arg) : Bool :=
   match y with
-  | Arg.var y =>
+  | .var y =>
     match ctx.projMap[y]? with
     | some (Expr.proj j w) => j == i && w == x
     | _ => false
-  | _ => false
+  | .erased => false
 
 /-- Given `uset x[i] := y`, return true iff `y := uproj[i] x` -/
 def isSelfUSet (ctx : Context) (x : VarId) (i : Nat) (y : VarId) : Bool :=
diff --git a/src/Lean/Compiler/IR/FreeVars.lean b/src/Lean/Compiler/IR/FreeVars.lean
index c969f68481..c9d04d07bc 100644
--- a/src/Lean/Compiler/IR/FreeVars.lean
+++ b/src/Lean/Compiler/IR/FreeVars.lean
@@ -28,8 +28,8 @@ instance : AndThen Collector where
   andThen a b := seq a (b ())
 
 private def collectArg : Arg → Collector
-  | Arg.var x  => collectVar x
-  | _          => skip
+  | .var x  => collectVar x
+  | .erased => skip
 
 private def collectArray {α : Type} (as : Array α) (f : α → Collector) : Collector :=
   fun m => as.foldl (fun m a => f a m) m
@@ -124,8 +124,8 @@ instance : AndThen Collector where
   andThen a b := seq a (b ())
 
 private def collectArg : Arg → Collector
-  | Arg.var x  => collectVar x
-  | _          => skip
+  | .var x  => collectVar x
+  | .erased => skip
 
 private def collectArray {α : Type} (as : Array α) (f : α → Collector) : Collector :=
   fun bv fv => as.foldl (fun fv a => f a bv fv) fv
@@ -184,8 +184,8 @@ def visitVar (w : Index) (x : VarId) : Bool := w == x.idx
 def visitJP (w : Index) (x : JoinPointId) : Bool := w == x.idx
 
 def visitArg (w : Index) : Arg → Bool
-  | Arg.var x => visitVar w x
-  | _         => false
+  | .var x => visitVar w x
+  | .erased => false
 
 def visitArgs (w : Index) (xs : Array Arg) : Bool :=
   xs.any (visitArg w)
diff --git a/src/Lean/Compiler/IR/LiveVars.lean b/src/Lean/Compiler/IR/LiveVars.lean
index 4629dabd36..0f4019e4a2 100644
--- a/src/Lean/Compiler/IR/LiveVars.lean
+++ b/src/Lean/Compiler/IR/LiveVars.lean
@@ -93,8 +93,8 @@ abbrev Collector := LiveVarSet → LiveVarSet
 @[inline] private def collectVar (x : VarId) : Collector := fun s => s.insert x
 
 private def collectArg : Arg → Collector
-  | Arg.var x  => collectVar x
-  | _          => skip
+  | .var x  => collectVar x
+  | .erased => skip
 
 private def collectArray {α : Type} (as : Array α) (f : α → Collector) : Collector := fun s =>
   as.foldl (fun s a => f a s) s
diff --git a/src/Lean/Compiler/IR/NormIds.lean b/src/Lean/Compiler/IR/NormIds.lean
index ec47e0a4c4..c8da2e4c1d 100644
--- a/src/Lean/Compiler/IR/NormIds.lean
+++ b/src/Lean/Compiler/IR/NormIds.lean
@@ -50,8 +50,8 @@ def normJP (x : JoinPointId) : M JoinPointId :=
   JoinPointId.mk <$> normIndex x.idx
 
 def normArg : Arg → M Arg
-  | Arg.var x => Arg.var <$> normVar x
-  | other     => pure other
+  | .var x => .var <$> normVar x
+  | .erased => pure .erased
 
 def normArgs (as : Array Arg) : M (Array Arg) := fun m =>
   as.map fun a => normArg a m
@@ -128,8 +128,8 @@ def Decl.normalizeIds (d : Decl) : Decl :=
 namespace MapVars
 
 @[inline] def mapArg (f : VarId → VarId) : Arg → Arg
-  | Arg.var x => Arg.var (f x)
-  | a         => a
+  | .var x => .var (f x)
+  | .erased => .erased
 
 def mapArgs (f : VarId → VarId) (as : Array Arg) : Array Arg :=
   as.map (mapArg f)