michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/class_instance_resolution): bug in mk_choice

Browse source
This commit is contained in:
Leonardo de Moura 2015-10-18 16:38:24 -07:00
parent 9348701a5b
commit eb2236f036
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/library/class_instance_resolution.cpp
View file

@ -1027,6 +1027,8 @@ struct cienv {
"(the class-instance resolution trace can be visualized by setting option 'class.trace_instances')", "(the class-instance resolution trace can be visualized by setting option 'class.trace_instances')",
mlocal_type(m_main_mvar)); mlocal_type(m_main_mvar));
} }
m_choices.push_back(choice());
choice & r = m_choices.back();
expr mvar_type = instantiate_uvars_mvars(mlocal_type(mvar)); expr mvar_type = instantiate_uvars_mvars(mlocal_type(mvar));
if (has_expr_metavar_relaxed(mvar_type)) { if (has_expr_metavar_relaxed(mvar_type)) {
// Remark: we use has_expr_metavar_relaxed instead of has_expr_metavar, because // Remark: we use has_expr_metavar_relaxed instead of has_expr_metavar, because
@ -1037,7 +1039,6 @@ struct cienv {
auto cname = is_class(mvar_type); auto cname = is_class(mvar_type);
if (!cname) if (!cname)
return false; return false;
choice r;
r.m_local_instances = get_local_instances(*cname); r.m_local_instances = get_local_instances(*cname);
if (m_trans_instances && m_choices.empty()) { if (m_trans_instances && m_choices.empty()) {
// we only use transitive instances in the top-level // we only use transitive instances in the top-level
@ -1047,7 +1048,6 @@ struct cienv {
if (empty(r.m_local_instances) && empty(r.m_trans_instances) && empty(r.m_instances)) if (empty(r.m_local_instances) && empty(r.m_trans_instances) && empty(r.m_instances))
return false; return false;
r.m_state = m_state; r.m_state = m_state;
m_choices.push_back(r);
return true; return true;
} }