Repr for Substring doesn't give a faithful representation

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

The default Repr instance for Substrings does not give an accurate representation of the object. It corresponds to toSubstring (toString s) which is == but not exactly the same as s in general.

def s : Substring := { str:="abcdef", startPos:=⟨1⟩, stopPos := ⟨3⟩ }

#eval repr s -- "bc".toSubstring

(Note that Repr and ToString are different: toString s should evaluate to "bc".)

The derive handler does a better job:

deriving instance Repr for Substring

#eval repr s -- { str := "abcdef", startPos := { byteIdx := 1 }, stopPos := { byteIdx := 3 } }

Expected behavior: The behavior obtained from the derive handler is what I would expect.

Actual behavior: As described above.

Reproduces how often: Always.

Versions

Lean (version 4.0.0-nightly-2023-08-17, commit f1412ddb4550, Release)

Start with the self-contained Substring example in the issue and inspect the default Repr instance for Substring. Compare its output with the derived Repr output shown there. Done means repr preserves the underlying string and start and stop positions rather than only the substring text.