#eval on let rec causes error in kernel

[Vierkantor]

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

Running #eval on an expression that contains a let rec cause the kernel to report an error: "(kernel) declaration has metavariables". I understand the (kernel) in this message indicates a bug where the evaluator sends an incorrect term to the kernel. Ideally evaluation would succeed for these expressions, or failing that, at least the evaluator would report an error instead of the kernel.

It seems the presence of let rec itself is the cause, not actual recursion or even using the let-introduced binding. When the same expression is instead used in the body as a def and then the def is given to #eval, evaluation succeeds. Similarly, when the let rec becomes a simple let, everything works.

Original Zulip thread.

I found a similar but seemingly distinct issue #2071.

Steps to Reproduce

Minimized reproduction:

def foo :=
  let rec bar : Nat := 1
  37
#eval foo -- works, evaluates to 37

#eval -- error: (kernel) declaration has metavariables '_eval'
  let rec bar : Nat := 1
  37

Expected behavior: Both #evals should return 37. Or the error in the kernel reported by the second #eval should become an error in the elaborator.

Actual behavior: Error in the kernel.

Reproduces how often: Always: all occurrences of let rec in #eval I could think of caused this error. Removing the rec keyword causes #eval to succeed.

Versions

$ lean --version
Lean (version 4.0.0-nightly-2023-07-30, commit 2eaa400b8e64, Release)
$ uname -a
Linux vouwvervorming 6.1.35-1-lts #1 SMP PREEMPT_DYNAMIC Wed, 21 Jun 2023 15:54:02 +0000 x86_64 GNU/Linux