fix: collect level parameters in evalExpr

`elabEvalUnsafe` already does something similar.

Author: eric-wieser

src/Lean/Meta/Eval.lean

@@ -4,19 +4,21 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sebastian Ullrich, Leonardo de Moura
 -/
 import Lean.Meta.Check
+import Lean.Util.CollectLevelParams
 
 namespace Lean.Meta
 
 unsafe def evalExprCore (α) (value : Expr) (checkType : Expr → MetaM Unit) (safety := DefinitionSafety.safe) : MetaM α :=
   withoutModifyingEnv do
     let name ← mkFreshUserName `_tmp
     let value ← instantiateMVars value
+    let us := collectLevelParams {} value |>.params
     if value.hasMVar then
       throwError "failed to evaluate expression, it contains metavariables{indentExpr value}"
     let type ← inferType value
     checkType type
     let decl := Declaration.defnDecl {
-       name, levelParams := [], type
+       name, levelParams := us.toList, type
        value, hints := ReducibilityHints.opaque,
        safety
     }

tests/lean/run/3091.lean

@@ -0,0 +1,13 @@
+import Lean
+
+open Lean
+
+def foo.{u} : Nat := (ULift.up.{u} Nat.zero).down
+
+universe u in
+#eval foo.{u}
+
+-- this used to produce an error
+#eval do
+  let u : Lean.Level := .param `u
+  Meta.evalExpr Nat (.const ``Nat []) (.const ``foo [u])