fix: correctly handle non-Nat literal types in LCNF elimDeadBranches (#9703)

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

@@ -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

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'