`by_elab` with variables from local context gives cryptic error message

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

When using by_elab with a term containing free variables, a kernel typechecking error occurs. The error message does not describe the problem in an easy to understand way.

Context

I was trying to access a private declaration while debugging #lean4 > Emulating type ascriptions and used a let-variable to store the name.

Steps to Reproduce

import Lean

def MyNat :=
  let nat := Lean.Expr.const ``Nat []
  -- (kernel) declaration has free variables '_tmp✝'
  by_elab pure nat

-- the solution
def MyNat :=
  by_elab
    let nat := Lean.Expr.const ``Nat []
    pure nat

Expected behavior:
A better error message, like by_elab cannot compile elaboration function which depends on free variable nat. Optionally, also unfold local let variables in by_elab

Actual behavior:
The error message (kernel) declaration has free variables '_tmp✝' which was hard to interpret, since there is no declaration called _tmp✝ visible in the syntax.

Versions

• Lean 4.19.0-nightly-2025-03-24
  Target: x86_64-unknown-linux-gnu
• Lean 4.13.0
  Target: x86_64-w64-windows-gnu Windows

Additional Information

[Additional information, configuration or data that might be necessary to reproduce the issue]

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start by running the self-contained by_elab examples against the reported Lean versions and compare the kernel error with the requested diagnostic. Trace the by_elab handling for terms containing free variables; done means the reproduction reports that the elaboration function depends on the local variable, with any let-unfolding behavior verified separately.