From b45ab9dc302af67be88cebe576f91aad34c5fb26 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 30 Jan 2014 14:13:17 -0800 Subject: [PATCH] feat(library/elaborator): use equality constraints instead of convertability constraints on definitions Convertability constraints are harder to solve than equality constraints, and it seems they don't buy us anything definitions. They are just increasing the search space for the elaborator. Signed-off-by: Leonardo de Moura --- src/frontends/lean/frontend_elaborator.cpp | 4 ++-- src/library/elaborator/elaborator.cpp | 2 +- tests/lean/elab1.lean.expected.out | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/frontends/lean/frontend_elaborator.cpp b/src/frontends/lean/frontend_elaborator.cpp index 4638f9174..871d0fe6f 100644 --- a/src/frontends/lean/frontend_elaborator.cpp +++ b/src/frontends/lean/frontend_elaborator.cpp @@ -469,8 +469,8 @@ public: if (has_metavar(new_e) || has_metavar(new_t)) { m_type_checker.check(new_t, context(), m_menv, m_ucs); expr new_e_t = m_type_checker.check(new_e, context(), m_menv, m_ucs); - m_ucs.push_back(mk_convertible_constraint(context(), new_e_t, new_t, - mk_def_type_match_justification(context(), n, e))); + m_ucs.push_back(mk_eq_constraint(context(), new_e_t, new_t, + mk_def_type_match_justification(context(), n, e))); // for (auto c : m_ucs) { // formatter fmt = mk_simple_formatter(); // std::cout << c.pp(fmt, options(), nullptr, false) << "\n"; diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp index 5b365ad2f..313b56b97 100644 --- a/src/library/elaborator/elaborator.cpp +++ b/src/library/elaborator/elaborator.cpp @@ -414,7 +414,7 @@ class elaborator::imp { expr tv = m_type_inferer(v, ctx, menv, ucs); push_active(ucs); justification new_jst(new typeof_mvar_justification(ctx, m, menv->get_type(m), tv, jst)); - push_active(mk_convertible_constraint(ctx, tv, menv->get_type(m), new_jst)); + push_active(mk_eq_constraint(ctx, tv, menv->get_type(m), new_jst)); } m_state.m_recently_assigned.insert(metavar_name(m)); return true; diff --git a/tests/lean/elab1.lean.expected.out b/tests/lean/elab1.lean.expected.out index 49bd654a6..c3aac5c48 100644 --- a/tests/lean/elab1.lean.expected.out +++ b/tests/lean/elab1.lean.expected.out @@ -34,7 +34,7 @@ A : Type, B : Type, a : ?M::0, b : ?M::1, C : Type ⊢ ?M::0[lift:0:3] ≺ C Assumed: b Assumed: H Failed to solve - ⊢ ∀ H1 : ?M::0, ?M::1 ∧ a ≺ b + ⊢ ∀ H1 : ?M::0, ?M::1 ∧ a ≈ b elab1.lean:18:18: Type of definition 't1' must be convertible to expected type. Failed to solve ⊢ @eq ?M::6 b b ≺ @eq ?M::1 a b