evalExpr does not handle universe params, but #eval does

[eric-wieser]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

evalExpr fails if any universe parameters are present, but #eval handles them correctly.

Context

This impedes leanprover-community/mathlib4#9135

Steps to Reproduce

import Lean

open Lean

def foo.{u} : Nat := (ULift.up.{u} Nat.zero).down

-- works
universe u in
#eval foo.{u}

-- fails: (kernel) invalid reference to undefined universe level parameter 'u'
#eval do
  let u : Lean.Level := .param `u
  Meta.evalExpr Nat (.const ``Nat []) (.const ``foo [u])

Expected behavior: both examples succeed and output 0

Actual behavior: the second example fails as shown

Versions

4.4.0-rc1

Impact

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