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

fix(library/class_instance_resolution): bug in mk_choice_point

Browse source
This commit is contained in:
Leonardo de Moura 2015-10-20 12:45:05 -07:00
parent 0446c43ebf
commit 21bd30d51a
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/library/class_instance_resolution.cpp
View file

@ -632,6 +632,7 @@ 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));
} }
bool toplevel_choice = m_choices.empty();
m_choices.push_back(choice()); m_choices.push_back(choice());
choice & r = m_choices.back(); choice & r = m_choices.back();
expr mvar_type = instantiate_uvars_mvars(mlocal_type(mvar)); expr mvar_type = instantiate_uvars_mvars(mlocal_type(mvar));
@ -645,7 +646,7 @@ struct cienv {
if (!cname) if (!cname)
return false; return false;
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 && toplevel_choice) {
// we only use transitive instances in the top-level // we only use transitive instances in the top-level
r.m_trans_instances = get_class_derived_trans_instances(m_env, *cname); r.m_trans_instances = get_class_derived_trans_instances(m_env, *cname);
} }