fix: String regressions (#10523)

This PR fixes some regressions introduced by #10304.

Author: TwoFX

src/Init/Data/ByteArray/Basic.lean

@@ -87,6 +87,7 @@ def copySlice (src : @& ByteArray) (srcOff : Nat) (dest : ByteArray) (destOff le
 def extract (a : ByteArray) (b e : Nat) : ByteArray :=
   a.copySlice b empty 0 (e - b)
 
+@[inline]
 protected def fastAppend (a : ByteArray) (b : ByteArray) : ByteArray :=
   -- we assume that `append`s may be repeated, so use asymptotic growing; use `copySlice` directly to customize
   b.copySlice 0 a a.size b.size false

src/Init/Data/String/Basic.lean

@@ -160,7 +160,7 @@ Examples:
  * `"" ++ "" = ""`
 -/
 @[extern "lean_string_append", expose]
-def String.append (s t : String) : String where
+def String.append (s : String) (t : @& String) : String where
   bytes := s.bytes ++ t.bytes
   isValidUtf8 := s.isValidUtf8.append t.isValidUtf8
 
@@ -221,7 +221,7 @@ Examples:
 * `"L∃∀N".length = 4`
 -/
 @[extern "lean_string_length"]
-def String.length (b : String) : Nat :=
+def String.length (b : @& String) : Nat :=
   b.data.length
 
 @[simp]

src/Init/Data/String/Bootstrap.lean

@@ -141,7 +141,7 @@ Examples:
  * `[].asString = ""`
  * `['a', 'a', 'a'].asString = "aaa"`
 -/
-@[expose]
+@[expose, inline]
 def List.asString (s : List Char) : String :=
   String.mk s
 

src/Init/Data/String/Decode.lean

@@ -1177,6 +1177,7 @@ public theorem ByteArray.isSome_utf8DecodeChar?_append {b : ByteArray} {i : Nat}
   obtain ⟨c, hc⟩ := Option.isSome_iff_exists.1 h
   rw [utf8DecodeChar?_append_eq_some hc, Option.isSome_some]
 
+@[inline]
 public def ByteArray.utf8DecodeChar (bytes : ByteArray) (i : Nat) (h : (utf8DecodeChar? bytes i).isSome) : Char :=
   (utf8DecodeChar? bytes i).get h