Unknown identifier error messages for `#eval`

Stream: lean4

[Julian Berman]

I find the error message in cases like:

variable {T : Type}

/-- error: Unknown identifier `T` -/
#guard_msgs in
#eval T

to be a bit confusing considering #check T works, and the identifier clearly "exists", albeit presumably not in the environment #eval is working with.

In slightly realer cases where I have (someexpr).something, and where I mistakenly think my expression gives me a real value it's even a bit further confusing to see the error message telling me someexpr doesn't exist when I see it does . In these cases probably I should train myself to type #reduce instead.

But should #eval's error messages for this say something more specific than claiming the identifier doesn't exist?

[Kyle Miller]

Here's an implementation: lean4#11427

The error is localized to the #eval keyword, and it could be friendlier if it showed errors on uses of free variables.

The reason #eval has its current behavior was because I thought it's marginally friendlier to have the error on a use of a free variable (and to avoid pulling in any typeclasses from variable), rather than on #eval itself.

(In Lean's architecture, section variables are elaborated at each command that wants them, so in that sense it they really don't exist for #eval. Probably it would be better if in general the "unknown identifier" error would have a backup strategy that involves elaborating the section variables to try to infer what the mistake was...)