diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index e35bab1682..0ef3492fea 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -1584,7 +1584,6 @@ expr elaborator::visit_prenum(expr const & e, constraint_seq & cs) {
     lean_assert(is_prenum(e));
     mpz const & v  = prenum_value(e);
     tag e_tag      = e.get_tag();
-    levels ls      = levels(mk_meta_univ(m_ngen.next()));
     // Remark: In HoTT mode, we only partially support the new encoding for numerals.
     // We fix A to num, and we rely on coercions to cast them to other types.
     // This is quite different from the approach used in the standard library
@@ -1593,6 +1592,8 @@ expr elaborator::visit_prenum(expr const & e, constraint_seq & cs) {
         A = m_full_context.mk_meta(m_ngen, none_expr(), e_tag);
     else
         A = mk_constant(get_num_name()).set_tag(e_tag);
+    level A_lvl = sort_level(m_tc->ensure_type(A, cs));
+    levels ls(A_lvl);
     bool is_strict = true;
     bool inst_imp  = true;
     if (v.is_neg())