From b71a68c60692ced9fdb72bf7183fcf06ba112958 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 18 Oct 2015 17:25:22 -0700 Subject: [PATCH] fix(frontends/lean/elaborator): visit_prenum was creating unnecessary universe metavariable This was creating problems for the new type class resolution procedure since visit_prenum was also not creating any constraint that enforced the universe level of A to be equal to the superfluous universe level. --- src/frontends/lean/elaborator.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) 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())