mut at binders and pattern matches

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

Currently, mut can only occur in restricted locations. This leads one to introduce
spurious names, that are later copied into the actual mutable variable:

opaque generator : Nat → Float × Nat
def generateN (seed: Nat) (n: Nat) : Array Float × Nat := Id.run do
  -- (1) this is annoying, please let me write '(mut seed : Nat)' in the declaration
  let mut seed := seed
  let mut out := #[]
  for _ in List.range n do
    -- (2) This is annoying, please let me write 'let (val, mut seed) := generator seed'
    let (val, seed') := generator seed
    seed := seed'

    out := out.push val
  return (out, seed)

A quality of life feature request is to be able to annotate binders such as function arguments and subterms of
pattern matches with mut. This would enable one to clean up the above function as:

opaque generator : Nat → Float × Nat
def generateN (mut seed: Nat) (n: Nat) : Array Float × Nat := Id.run do
  let mut out := #[]
  for _ in List.range n do
    let (val, mut seed) := generator seed'
    out := out.push val
  return (out, seed)

@digama0 mentioned that this might be complex, because lean does not have a dedicated grammar for patterns, it just reuses the expr grammar. A proposal was to add a expr macro mut that fails for normal exprs, and elaborates to the expected code when used at appropriate binding locations.

Start by examining Lean's expression grammar and elaboration for binders and pattern matches; the issue notes that patterns reuse the expr grammar. Evaluate the proposed expr macro for mut, including its failure on ordinary expressions. Done means function arguments and pattern-match subterms accept mut while existing restricted locations continue to work.