From a50cbf07ab437da473d3106a059095d48cd91c2a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 20 Jul 2016 19:42:21 -0400 Subject: [PATCH] fix(library/app_builder): do not try to instantiate type class instances that have been explicitly provided --- src/library/app_builder.cpp | 18 ++++++++++++------ 1 file changed, 12 insertions(+), 6 deletions(-) diff --git a/src/library/app_builder.cpp b/src/library/app_builder.cpp index 8d9748bb79..6707f7bef8 100644 --- a/src/library/app_builder.cpp +++ b/src/library/app_builder.cpp @@ -260,17 +260,23 @@ class app_builder { for (optional const & inst_arg : e.m_inst_args) { lean_assert(i > 0); --i; - if (inst_arg) { - expr type = m_ctx.instantiate_mvars(mlocal_type(*inst_arg)); - if (auto v = m_ctx.mk_class_instance(type)) { - if (!m_ctx.is_def_eq(*inst_arg, *v)) + if (!m_ctx.get_tmp_mvar_assignment(i)) { + if (inst_arg) { + expr type = m_ctx.instantiate_mvars(mlocal_type(*inst_arg)); + if (auto v = m_ctx.mk_class_instance(type)) { + if (!m_ctx.is_def_eq(*inst_arg, *v)) { + // failed to assign instance + return false; + } + } else { + // failed to generate instance return false; + } } else { + // unassined metavar return false; } } - if (!m_ctx.get_tmp_mvar_assignment(i)) - return false; } for (unsigned i = 0; i < e.m_num_umeta; i++) { if (!m_ctx.get_tmp_uvar_assignment(i))