diff --git a/src/Init/Data/String/Defs.lean b/src/Init/Data/String/Defs.lean
index 05fd208533..2b1e908931 100644
--- a/src/Init/Data/String/Defs.lean
+++ b/src/Init/Data/String/Defs.lean
@@ -421,6 +421,9 @@ def toSlice (s : String) : Slice where
   endExclusive := s.endPos
   startInclusive_le_endExclusive := by simp [Pos.le_iff, Pos.Raw.le_iff]
 
+instance : Coe String String.Slice where
+  coe := String.toSlice
+
 @[simp]
 theorem startInclusive_toSlice {s : String} : s.toSlice.startInclusive = s.startPos := rfl
 
diff --git a/src/Lean/Shell.lean b/src/Lean/Shell.lean
index 6cf5b53dd1..af3c89ffdb 100644
--- a/src/Lean/Shell.lean
+++ b/src/Lean/Shell.lean
@@ -255,7 +255,7 @@ def shellMain
     if contents.startsWith "#lang" then
       let endLinePos := contents.find '\n'
       let langId := String.Pos.Raw.extract contents ⟨6⟩ endLinePos.offset |>.trimAscii
-      if langId == "lean4".toSlice then
+      if langId == "lean4" then
         pure () -- do nothing for now
       else
         IO.eprintln s!"unknown language '{langId}'\n";
diff --git a/src/lake/Lake/Util/Version.lean b/src/lake/Lake/Util/Version.lean
index 38e59744ee..6602442fc4 100644
--- a/src/lake/Lake/Util/Version.lean
+++ b/src/lake/Lake/Util/Version.lean
@@ -269,7 +269,7 @@ public def ofString (ver : String) : ToolchainVer := Id.run do
       if noOrigin then
         return .nightly date
       else if let some suffix := origin.dropPrefix? defaultOrigin then
-        if suffix.isEmpty || suffix == "-nightly".toSlice then
+        if suffix.isEmpty || suffix == "-nightly" then
           return .nightly date
   else if let some n := tag.dropPrefix?  "pr-release-" then
     if let some n := n.toNat? then