From 8edcfbe7760ae22b31c58ce5216ea24a9b89f628 Mon Sep 17 00:00:00 2001
From: Cameron Zwarich <cameron@lean-fro.org>
Date: Mon, 4 Aug 2025 19:14:07 -0700
Subject: [PATCH] fix: correctly handle non-`Nat` literal types in LCNF
 `elimDeadBranches` (#9703)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR changes the LCNF `elimDeadBranches` pass so that it considers
all non-`Nat` literal types to be `⊤`. It turns out that fixing this to
correctly handle all of these types with the current abstract value
representation is surprisingly nontrivial, and it's better to just land
the fix first.
---
 src/Lean/Compiler/LCNF/ElimDeadBranches.lean  |  6 ++---
 .../run/elimDeadBranchesUInt64Literal.lean    | 27 +++++++++++++++++++
 2 files changed, 29 insertions(+), 4 deletions(-)
 create mode 100644 tests/lean/run/elimDeadBranchesUInt64Literal.lean

diff --git a/src/Lean/Compiler/LCNF/ElimDeadBranches.lean b/src/Lean/Compiler/LCNF/ElimDeadBranches.lean
index 87facb7437..7450ae2c71 100644
--- a/src/Lean/Compiler/LCNF/ElimDeadBranches.lean
+++ b/src/Lean/Compiler/LCNF/ElimDeadBranches.lean
@@ -171,12 +171,10 @@ where
 
 def ofLCNFLit : LCNF.LitValue → Value
 | .nat n => ofNat n
+-- TODO: Make this work for other numeric literal types.
+| .uint8 _ | .uint16 _ | .uint32 _ | .uint64 _ | .usize _ => .top
 -- TODO: We could make this much more precise but the payoff is questionable
 | .str .. => .top
-| .uint8 v => ofNat (UInt8.toNat v)
-| .uint16 v => ofNat (UInt16.toNat v)
-| .uint32 v => ofNat (UInt32.toNat v)
-| .uint64 v | .usize v => ofNat (UInt64.toNat v)
 
 partial def proj : Value → Nat → Value
 | .ctor _ vs , i => vs.getD i bot
diff --git a/tests/lean/run/elimDeadBranchesUInt64Literal.lean b/tests/lean/run/elimDeadBranchesUInt64Literal.lean
new file mode 100644
index 0000000000..0b8f97b6de
--- /dev/null
+++ b/tests/lean/run/elimDeadBranchesUInt64Literal.lean
@@ -0,0 +1,27 @@
+structure UInt128 where
+  lo : UInt64
+  hi : UInt64
+
+def zero : UInt128 := ⟨0, 0⟩
+
+@[noinline]
+def compl (n : UInt64) : UInt64 := n.complement
+
+def exp : UInt64 := compl <| compl <| compl zero.hi
+
+#eval exp
+
+abbrev UnsignedInt64 := UInt64
+
+structure UnsignedInt128 where
+  hi : UnsignedInt64
+  lo : UnsignedInt64
+
+def zero' : UnsignedInt128 := ⟨0, 0⟩
+
+@[noinline]
+def compl' (n : UnsignedInt64) : UnsignedInt64 := n.complement
+
+def exp' : UnsignedInt64 := compl' <| compl' <| compl' zero'.hi
+
+#eval exp'