Telescope action on binders/let values

Stream: lean4

[Arthur Adjedj]

Hi. Currently, functions like forallTelescope and lambdaTelescope are useful in that they allow one to traverse terms easily, but don't allow the user to i.e influence the values/types of variables added in the local context.
Take for example the following function in Lean.Meta.Reduce, which is used to elaborate the #reduce command:

partial def reduce (e : Expr) (explicitOnly skipTypes skipProofs := true) : MetaM Expr :=
  let rec visit (e : Expr) : MonadCacheT Expr Expr MetaM Expr :=
    checkCache e fun _ => Core.withIncRecDepth do
      if (← (pure skipTypes <&&> isType e)) then
        return e
      else if (← (pure skipProofs <&&> isProof e)) then
        return e
      else
        let e ← whnf e
        match e with
        | Expr.app .. =>
          let f     ← visit e.getAppFn
          let nargs := e.getAppNumArgs
          let finfo ← getFunInfoNArgs f nargs
          let mut args  := e.getAppArgs
          for i in [:args.size] do
            if i < finfo.paramInfo.size then
              let info := finfo.paramInfo[i]!
              if !explicitOnly || info.isExplicit then
                args ← args.modifyM i visit
            else
              args ← args.modifyM i visit
          if f.isConstOf ``Nat.succ && args.size == 1 && args[0]!.isNatLit then
            return mkRawNatLit (args[0]!.natLit?.get! + 1)
          else
            return mkAppN f args
        | Expr.lam ..        => lambdaTelescope e fun xs b => do mkLambdaFVars xs (← visit b)
        | Expr.forallE ..    => forallTelescope e fun xs b => do mkForallFVars xs (← visit b)
        | Expr.proj n i s .. => return mkProj n i (← visit s)
        | _                  => return e
  visit e |>.run

This function visits and reduces every redex. However, it doesn't reduce binder types. For example, #reduce (x : id Nat) -> Fin x doesn't reduce id Nat. My initial attempt at fixing such things has been to manipulate the local context during the traversal, by overwriting variables to the local context and modifying their types/values, as such:

forallTelescope e fun xs b => do
  let mut lctx ← getLCtx
  for e in xs do
    let some lcdl := lctx.findFVar? e | unreachable!
    let value ← withReader (fun ctx => {ctx with lctx := lctx})
      (visit lcdl.value)
    lctx := LocalContext.addDecl lctx (lcdl.setValue value)
  withReader (fun ctx => {ctx with lctx := lctx})
    (mkForallFVars xs (← visit b))

but this doesn't look elegant nor efficient to me. Is there any nice way to do something like this, apart from writing separate telescope functions ?

[Arthur Adjedj]

This is one example where I've encountered the need to do such a thing, a second one, which occurred to me now, happens here: the let declarations' bodies don't get reduced before being added to the local context, leading to some metavariables not getting assigned. Fixing this resolves #3146