diff --git a/src/Lean/Compiler/ConstFolding.lean b/src/Lean/Compiler/ConstFolding.lean
index 34b7e6cf6d5e..ee99319fd2da 100644
--- a/src/Lean/Compiler/ConstFolding.lean
+++ b/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),
diff --git a/tests/lean/run/4306.lean b/tests/lean/run/4306.lean
new file mode 100644
index 000000000000..5f3920a2f519
--- /dev/null
+++ b/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