diff --git a/src/Init/Data/FloatArray/Basic.lean b/src/Init/Data/FloatArray/Basic.lean
index 759e3b0de5ad..3ed6826742b0 100644
--- a/src/Init/Data/FloatArray/Basic.lean
+++ b/src/Init/Data/FloatArray/Basic.lean
@@ -42,7 +42,7 @@ instance : EmptyCollection FloatArray where
 def push : FloatArray → Float → FloatArray
   | ⟨ds⟩, b => ⟨ds.push b⟩
 
-@[extern "lean_float_array_size"]
+@[extern "lean_float_array_size", tagged_return]
 def size : (@& FloatArray) → Nat
   | ⟨ds⟩ => ds.size
 
diff --git a/src/Init/Data/SInt/Basic.lean b/src/Init/Data/SInt/Basic.lean
index f60579ced8b3..45147ba8867c 100644
--- a/src/Init/Data/SInt/Basic.lean
+++ b/src/Init/Data/SInt/Basic.lean
@@ -150,7 +150,7 @@ Converts an 8-bit signed integer to an arbitrary-precision integer that denotes
 
 This function is overridden at runtime with an efficient implementation.
 -/
-@[extern "lean_int8_to_int"]
+@[extern "lean_int8_to_int", tagged_return]
 def Int8.toInt (i : Int8) : Int := i.toBitVec.toInt
 /--
 Converts an 8-bit signed integer to a natural number, mapping all negative numbers to `0`.
@@ -503,7 +503,7 @@ Converts a 16-bit signed integer to an arbitrary-precision integer that denotes
 
 This function is overridden at runtime with an efficient implementation.
 -/
-@[extern "lean_int16_to_int"]
+@[extern "lean_int16_to_int", tagged_return]
 def Int16.toInt (i : Int16) : Int := i.toBitVec.toInt
 /--
 Converts a 16-bit signed integer to a natural number, mapping all negative numbers to `0`.
diff --git a/src/Init/Data/String/Basic.lean b/src/Init/Data/String/Basic.lean
index be1f740fb5e7..42f4b1b23603 100644
--- a/src/Init/Data/String/Basic.lean
+++ b/src/Init/Data/String/Basic.lean
@@ -264,7 +264,7 @@ Examples:
 * `"abc".length = 3`
 * `"L∃∀N".length = 4`
 -/
-@[extern "lean_string_length", expose]
+@[extern "lean_string_length", expose, tagged_return]
 def String.length (b : @& String) : Nat :=
   b.toList.length
 
@@ -1652,7 +1652,7 @@ def Slice.pos! (s : Slice) (off : String.Pos.Raw) : s.Pos :=
 
 /-- Advances a valid position on a string to the next valid position, given a proof that the
 position is not the past-the-end position, which guarantees that such a position exists. -/
-@[expose, extern "lean_string_utf8_next_fast"]
+@[expose, extern "lean_string_utf8_next_fast", tagged_return]
 def Pos.next {s : @& String} (pos : @& s.Pos) (h : pos ≠ s.endPos) : s.Pos :=
   ofToSlice (Slice.Pos.next pos.toSlice (ne_of_apply_ne Pos.ofToSlice (by simpa)))
 
@@ -2656,7 +2656,7 @@ This is a legacy function. The recommended alternative is `String.Pos.next`, com
 Example:
 * `let abc := "abc"; abc.get (abc.next' 0 (by decide)) = 'b'`
 -/
-@[extern "lean_string_utf8_next_fast", expose]
+@[extern "lean_string_utf8_next_fast", expose, tagged_return]
 def Pos.Raw.next' (s : @& String) (p : @& Pos.Raw) (h : ¬ p.atEnd s) : Pos.Raw :=
   let c := p.get s
   p + c
diff --git a/src/Init/Data/UInt/BasicAux.lean b/src/Init/Data/UInt/BasicAux.lean
index 03b1ccb5e621..6d01769b9394 100644
--- a/src/Init/Data/UInt/BasicAux.lean
+++ b/src/Init/Data/UInt/BasicAux.lean
@@ -57,7 +57,7 @@ Converts an 8-bit unsigned integer to an arbitrary-precision natural number.
 
 This function is overridden at runtime with an efficient implementation.
 -/
-@[extern "lean_uint8_to_nat"]
+@[extern "lean_uint8_to_nat", tagged_return]
 def UInt8.toNat (n : UInt8) : Nat := n.toBitVec.toNat
 
 instance UInt8.instOfNat : OfNat UInt8 n := ⟨UInt8.ofNat n⟩
@@ -108,7 +108,7 @@ Converts a 16-bit unsigned integer to an arbitrary-precision natural number.
 
 This function is overridden at runtime with an efficient implementation.
 -/
-@[extern "lean_uint16_to_nat"]
+@[extern "lean_uint16_to_nat", tagged_return]
 def UInt16.toNat (n : UInt16) : Nat := n.toBitVec.toNat
 /--
 Converts 16-bit unsigned integers to 8-bit unsigned integers. Wraps around on overflow.
diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index ee41f63e208b..807f073e1430 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -3185,7 +3185,7 @@ This is a cached value, so it is `O(1)` to access. The space allocated for an ar
 its _capacity_, is at least as large as its size, but may be larger. The capacity of an array is an
 internal detail that's not observable by Lean code.
 -/
-@[extern "lean_array_get_size"]
+@[extern "lean_array_get_size", tagged_return]
 def Array.size {α : Type u} (a : @& Array α) : Nat :=
  a.toList.length
 
@@ -3393,7 +3393,7 @@ Returns the number of bytes in the byte array.
 This is the number of bytes actually in the array, as distinct from its capacity, which is the
 amount of memory presently allocated for the array.
 -/
-@[extern "lean_byte_array_size"]
+@[extern "lean_byte_array_size", tagged_return]
 def ByteArray.size : (@& ByteArray) → Nat
   | ⟨bs⟩ => bs.size
 
@@ -3540,7 +3540,7 @@ The number of bytes used by the string's UTF-8 encoding.
 
 At runtime, this function takes constant time because the byte length of strings is cached.
 -/
-@[extern "lean_string_utf8_byte_size"]
+@[extern "lean_string_utf8_byte_size", tagged_return]
 def String.utf8ByteSize (s : @& String) : Nat :=
   s.toByteArray.size
 
diff --git a/tests/lean/run/tagged_return_2.lean b/tests/lean/run/tagged_return_2.lean
new file mode 100644
index 000000000000..eff8ad3c9c4d
--- /dev/null
+++ b/tests/lean/run/tagged_return_2.lean
@@ -0,0 +1,161 @@
+/-! This test asserts that the built-in symbols marked with tagged_return compile correctly -/
+
+/--
+trace: [Compiler.IR] [result]
+    def test1 (x_1 : @& obj) : tobj :=
+      let x_2 : tagged := FloatArray.size x_1;
+      ret x_2
+    def test1._boxed (x_1 : obj) : tobj :=
+      let x_2 : tobj := test1 x_1;
+      dec x_1;
+      ret x_2
+-/
+#guard_msgs in
+set_option trace.compiler.ir.result true in
+def test1 (a : FloatArray) := a.size
+
+/--
+trace: [Compiler.IR] [result]
+    def test2 (x_1 : @& obj) : tobj :=
+      let x_2 : tagged := ByteArray.size x_1;
+      ret x_2
+    def test2._boxed (x_1 : obj) : tobj :=
+      let x_2 : tobj := test2 x_1;
+      dec x_1;
+      ret x_2
+-/
+#guard_msgs in
+set_option trace.compiler.ir.result true in
+def test2 (a : ByteArray) := a.size
+
+/--
+trace: [Compiler.IR] [result]
+    def test3 (x_1 : @& obj) : tobj :=
+      let x_2 : tagged := Array.size ◾ x_1;
+      ret x_2
+    def test3._boxed (x_1 : obj) : tobj :=
+      let x_2 : tobj := test3 x_1;
+      dec x_1;
+      ret x_2
+-/
+#guard_msgs in
+set_option trace.compiler.ir.result true in
+def test3 (a : Array Nat) := a.size
+
+/--
+trace: [Compiler.IR] [result]
+    def test4 (x_1 : @& obj) : tobj :=
+      let x_2 : tagged := String.length x_1;
+      ret x_2
+    def test4._boxed (x_1 : obj) : tobj :=
+      let x_2 : tobj := test4 x_1;
+      dec x_1;
+      ret x_2
+-/
+#guard_msgs in
+set_option trace.compiler.ir.result true in
+def test4 (a : String) := a.length
+
+/--
+trace: [Compiler.IR] [result]
+    def test5 (x_1 : @& obj) : tobj :=
+      let x_2 : tagged := String.utf8ByteSize x_1;
+      ret x_2
+    def test5._boxed (x_1 : obj) : tobj :=
+      let x_2 : tobj := test5 x_1;
+      dec x_1;
+      ret x_2
+-/
+#guard_msgs in
+set_option trace.compiler.ir.result true in
+def test5 (a : String) := a.utf8ByteSize
+
+/--
+warning: declaration uses 'sorry'
+---
+trace: [Compiler.IR] [result]
+    def test6 (x_1 : @& obj) (x_2 : @& tobj) : tobj :=
+      let x_3 : tagged := String.Pos.next x_1 x_2 ◾;
+      ret x_3
+    def test6._boxed (x_1 : obj) (x_2 : tobj) : tobj :=
+      let x_3 : tobj := test6 x_1 x_2;
+      dec x_2;
+      dec x_1;
+      ret x_3
+-/
+#guard_msgs in
+set_option trace.compiler.ir.result true in
+def test6 (a : String) (p : a.Pos) := p.next sorry
+
+/--
+trace: [Compiler.IR] [result]
+    def test8 (x_1 : u8) : tobj :=
+      let x_2 : tagged := UInt8.toNat x_1;
+      ret x_2
+    def test8._boxed (x_1 : tagged) : tobj :=
+      let x_2 : u8 := unbox x_1;
+      let x_3 : tobj := test8 x_2;
+      ret x_3
+-/
+#guard_msgs in
+set_option trace.compiler.ir.result true in
+def test8 (a : UInt8) := a.toNat
+
+/--
+trace: [Compiler.IR] [result]
+    def test9 (x_1 : u16) : tobj :=
+      let x_2 : tagged := UInt16.toNat x_1;
+      ret x_2
+    def test9._boxed (x_1 : tagged) : tobj :=
+      let x_2 : u16 := unbox x_1;
+      let x_3 : tobj := test9 x_2;
+      ret x_3
+-/
+#guard_msgs in
+set_option trace.compiler.ir.result true in
+def test9 (a : UInt16) := a.toNat
+
+/--
+trace: [Compiler.IR] [result]
+    def test10 (x_1 : u8) : tobj :=
+      let x_2 : tagged := Int8.toInt x_1;
+      ret x_2
+    def test10._boxed (x_1 : tagged) : tobj :=
+      let x_2 : u8 := unbox x_1;
+      let x_3 : tobj := test10 x_2;
+      ret x_3
+-/
+#guard_msgs in
+set_option trace.compiler.ir.result true in
+def test10 (a : Int8) := a.toInt
+
+/--
+trace: [Compiler.IR] [result]
+    def test11 (x_1 : u16) : tobj :=
+      let x_2 : tagged := Int16.toInt x_1;
+      ret x_2
+    def test11._boxed (x_1 : tagged) : tobj :=
+      let x_2 : u16 := unbox x_1;
+      let x_3 : tobj := test11 x_2;
+      ret x_3
+-/
+#guard_msgs in
+set_option trace.compiler.ir.result true in
+def test11 (a : Int16) := a.toInt
+
+/--
+warning: declaration uses 'sorry'
+---
+trace: [Compiler.IR] [result]
+    def test12 (x_1 : @& obj) (x_2 : @& tobj) : tobj :=
+      let x_3 : tagged := String.Pos.Raw.next' x_1 x_2 ◾;
+      ret x_3
+    def test12._boxed (x_1 : obj) (x_2 : tobj) : tobj :=
+      let x_3 : tobj := test12 x_1 x_2;
+      dec x_2;
+      dec x_1;
+      ret x_3
+-/
+#guard_msgs in
+set_option trace.compiler.ir.result true in
+def test12 (a : String) (p : String.Pos.Raw) := p.next' a sorry