RFC: Array operations: Avoid duplicating arguments with (stop := as.size)

The issue

I have just stumbed over the fact that many Array operations (foldl etc.) have a parameter
stop with a default argument (stop := as.size), and this duplicates the array argument, which may be large:

def foo : Bool := Array.any #[1,2,3,4] (fun _ => true)
#print foo

prints

def foo : Bool :=
Array.any #[1, 2, 3, 4] (fun x => true) 0 (Array.size #[1, 2, 3, 4])

This duplication also shows up in other places, e.g. in well-founded recursive definitions (which, unsurprisingly, is how I noticed this) a recursive call in the array will cause the tactic to be invoked multiple times:

def rec : Nat → Bool
 | 0 => true
 | n+1 =>  Array.any #[rec n, rec n, rec n, rec n] id
decreasing_by trace "Tactic is run"; decreasing_tactic -- called 8 times

Worse, nesting these innocent looking funcitons now lead to a combinatoric explosion:

def rec2 : Nat → Bool
 | 0 => true
 | n+1 => 
    Array.any #[
      Array.any #[rec2 n, rec2 n, rec2 n, rec2 n] id,
      Array.any #[rec2 n, rec2 n, rec2 n, rec2 n] id,
      Array.any #[rec2 n, rec2 n, rec2 n, rec2 n] id,
      Array.any #[rec2 n, rec2 n, rec2 n, rec2 n] id
    ] id
decreasing_by trace "Tactic is run"; decreasing_tactic -- called 64 times

Proposal

A possible fix is to update all these functions as follows:

Change

unsafe def foldlMUnsafe {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : β → α → m β) (init : β) (as : Array α) (start := 0) (stop := as.size) : m β :=

to

unsafe def foldlMUnsafe {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : β → α → m β) (init : β) (as : Array α) (start := 0) (stop := Option as.size) : m β :=
  let stop := stop.getD as.size

Many of the ~19 affected functions just pass stop on, so they only change the type, not the implementation.

Alternative

The only alternative I see is to change how optional arguments are elaborated, and if they mention earlier parameters, that parameter is let-bound instead of duplicated.

I do not know if there are users who actually rely on default paramters being able to refer not just to the value of an earlier argument, but actually need the argument syntax to be replicated.

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

Start by reviewing the shown foldlMUnsafe signature, Array.any, and the other Array operations that pass stop through. Compare the proposed Option-based defaults with the alternative elaboration change, then verify that generated terms no longer duplicate earlier array arguments while existing optional-argument behavior remains supported.