fix: miscompilation in constant folding

closes #4306

src/Lean/Compiler/ConstFolding.lean

@@ -193,12 +193,13 @@ def foldCharOfNat (beforeErasure : Bool) (a : Expr) : Option Expr := do
   else
     return mkUInt32Lit 0
 
-def foldToNat (_ : Bool) (a : Expr) : Option Expr := do
+def foldToNat (size : Nat) (_ : Bool) (a : Expr) : Option Expr := do
   let n ← getNumLit a
-  return mkRawNatLit n
+  return mkRawNatLit (n % size)
+
 
 def uintFoldToNatFns : List (Name × UnFoldFn) :=
-  numScalarTypes.foldl (fun r info => (info.toNatFn, foldToNat) :: r) []
+  numScalarTypes.foldl (fun r info => (info.toNatFn, foldToNat info.size) :: r) []
 
 def unFoldFns : List (Name × UnFoldFn) :=
   [(``Nat.succ, foldNatSucc),

tests/lean/run/4306.lean

@@ -0,0 +1,24 @@
+/--
+info: 12776324570088369205
+-/
+#guard_msgs in
+#eval (123456789012345678901).toUInt64
+
+/--
+info: 12776324570088369205
+-/
+#guard_msgs in
+#eval (123456789012345678901).toUInt64.toNat
+
+/--
+error: application type mismatch
+  Lean.ofReduceBool false._nativeDecide_1 true (Eq.refl true)
+argument has type
+  true = true
+but function has type
+  Lean.reduceBool false._nativeDecide_1 = true → false._nativeDecide_1 = true
+-/
+#guard_msgs in
+theorem false : False := by
+  have : (123456789012345678901).toUInt64.toNat = 123456789012345678901 := by native_decide
+  simp [Nat.toUInt64] at this