From 2edccf007bc575fa6126c1a4273694dd15c2e023 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 18 Oct 2015 18:38:41 -0700 Subject: [PATCH] fix(library/class_instance_resolution): make sure that terms synthesized by type class resolution have override the ones synthesized by solving unification constraints. --- src/library/class_instance_resolution.cpp | 17 +++++++++-------- 1 file changed, 9 insertions(+), 8 deletions(-) diff --git a/src/library/class_instance_resolution.cpp b/src/library/class_instance_resolution.cpp index 986f9239d..e3e8a3a58 100644 --- a/src/library/class_instance_resolution.cpp +++ b/src/library/class_instance_resolution.cpp @@ -978,7 +978,15 @@ struct cienv { return false; } r = Fun(locals, r); - assign(mvar, r); + if (is_assigned(mvar)) { + // Remark: if the metavariable is already assigned, we should check whether + // the previous assignment (obtained by solving unification constraints) and the + // synthesized one are definitionally equal. We don't do that for performance reasons. + // Moreover, the is_def_eq defined here is not complete (e.g., it only unfolds reducible constants). + update_assignment(mvar, r); + } else { + assign(mvar, r); + } // copy new_inst_mvars to stack unsigned i = new_inst_mvars.size(); while (i > 0) { @@ -1088,13 +1096,6 @@ struct cienv { lean_assert(!is_done()); unsigned depth = head(m_state.m_stack).first; expr mvar = head(m_state.m_stack).second; - if (is_assigned(mvar)) { - // Remark: if the metavariable is already assigned, another alternative is to - // execute type class resolution and ensure the synthesized answer is equal to the - // one assigned by solving unification constraints. - m_state.m_stack = tail(m_state.m_stack); - return true; // metavariable was assigned by solving unification constraints - } if (!mk_choice_point(mvar)) return false; m_state.m_stack = tail(m_state.m_stack);