Unexpected behavior for `Subarray` ranges

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

This was discussed on Zulip a while ago but I forgot to submit a bug report.

def a : Array Nat := #[0,1,2,3,4,5,6]

def b : Subarray Nat := a[1:5]

#eval (b.as, b.start, b.stop) -- (#[0,1,2,3,4,5,6], 1, 5)

def c : Subarray Nat := b[1:3]

#eval (c.as, c.start, c.stop) -- (#[1,2,3,4], 1, 3) !?

The expected result for the last eval is (#[0,1,2,3,4,5,6], 2, 4).

The reason for this odd behavior is that the a[start:stop] notation assumes that a is an array. So when calculating c, Lean first coerces b into an array and then calculates the subarray of that.

Versions

Lean (version 4.0.0-nightly-2023-07-15, commit d37bbf4292c7, Release)

Additional Information

In my opinion, there should not be a coercion from Subarray to Array (which involves a possibly expensive array copy), but there should be one from Array to Subarray (which is essentially zero cost). Then the a[start:stop] could be refactored to assume that a is a subarray instead.

The Subarray to Array coercion is not used in Init in any essential way, but it is used lot in Lean so this would not be a trivial change.

Run the self-contained reproducer and inspect the a[start:stop] notation in src/Init/Data/Array/Subarray.lean at the linked lines. Trace how nested Subarray slicing handles the underlying array and bounds, including the coercion mentioned in the issue. Done means the final evaluation preserves the original array and reports (2, 4) for c.start and c.stop, with relevant Lean uses still working.