fix: collect level parameters in evalExpr

[eric-wieser]

elabEvalUnsafe already does something similar: it also instantiates universe metavariables, but it is not clear to me whether that is sensible here.
To be conservative, I leave it out of this PR.

See #3090 (comment) for a comparison between #eval and Meta.evalExpr. This PR is not trying to fully align them, but just to fix one particular misalignment that I am impacted by.

Closes #3091

[leanprover-community-mathlib4-bot]

• ❗ Mathlib CI will not be attempted unless you rebase your PR onto the 'nightly' branch. (2023-12-18 15:50:28)
• ✅ Mathlib branch lean-pr-testing-3090 has successfully built against this PR. (2023-12-20 12:34:38) View Log
• ✅ Mathlib branch lean-pr-testing-3090 has successfully built against this PR. (2023-12-20 13:12:04) View Log

[kim-em]

It would be good to have a Mathlib build for this one. Could you rebase onto nightly-with-mathlib?

[eric-wieser]

I'm afraid I probably have no time today to do so, but might later this week.

My figuring is that this is very unlikely to break anything, since the change only affects code that was previously producing kernel errors; but indeed it's good practice to test it anyway.

[eric-wieser]

elabEvalUnsafe uses

lean4/src/Lean/Elab/BuiltinCommand.lean

Lines 634 to 637 in 8335d4e

	let value ← Term.levelMVarToParam (← instantiateMVars value)
	let type ← inferType value
	let us := collectLevelParams {} value |>.params
	let value ← instantiateMVars value

which rather puzzlingly uses instantiateMVars twice. I don't really know which if either is right, so I've limited this to the minimal change that fixes my bug.

[eric-wieser]

@kmill, do you have any guesses as to why inferType happens to the pre-instantiateMVarsd value in the other file referenced above?

[eric-wieser]

@digama0, @semorrison, do you have any thoughts on what's going on here?

[kmill]

I don't see a reason to instantiateMVars that second time, but I do wonder if it should be let type ← instantiateMVars type instead, since there's no reason why the inferred type will be metavariable-free.

[eric-wieser]

How can a value have no metavariables but its inferred type have some?

[digama0]

If the value is a where a : ?m1 is a hypothesis then this can happen.

[eric-wieser]

But eval can't work if there are free variables anyway, so presumably this doesn't matter?

[eric-wieser]

It would be good to have a Mathlib build for this one. Could you rebase onto nightly-with-mathlib?

I did this rebase @semorrison, but I guess CI won't run until tomorrow?

[nomeata]

It would be good to have a Mathlib build for this one. Could you rebase onto nightly-with-mathlib?

I did this rebase @semorrison, but I guess CI won't run until tomorrow?

The workflow is a bit racy; by the time it ran, a new nightly tag appeared (2023-12-19), but nightly-with-mathlib did not advance. I hope that #3097 will fix that. Once that hits master, I can re-trigger the workflow and then it hopefully works. Sorry for the delays.

[nomeata]

Seems to work (https://github.com/leanprover/lean4/actions/runs/7274620683/job/19820906002), mathlib CI should be running

[eric-wieser]

awaiting-review

[eric-wieser]

@semorrison, do you think this is ok as is? While there's some discussion above about instantiating metavariables, it's mainly about code that isn't part of this patch anyway; and the actual change is only two lines!

[eric-wieser]

Just to note this now also impacts eval% in mathlib:

import Mathlib.Tactic.Eval

def foo.{u} (x : PUnit.{u}) : Nat := 37

-- fails without this PR
def bar.{u} (x : PUnit.{u}) : Nat := eval% foo.{u} PUnit.unit