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

fix(library/class_instance_resolution): relax has_expr_metavar test at mk_choice

Browse source
This commit is contained in:
Leonardo de Moura 2015-10-18 12:36:46 -07:00
parent 5f90ff0f07
commit 088b0fb795
1 changed files with 5 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/library/class_instance_resolution.cpp
View file

@ -973,8 +973,12 @@ struct cienv {
mlocal_type(m_main_mvar));
}
expr mvar_type = instantiate_uvars_mvars(mlocal_type(mvar));
if (has_expr_metavar(mvar_type))
if (has_expr_metavar_relaxed(mvar_type)) {
// Remark: we use has_expr_metavar_relaxed instead of has_expr_metavar, because
// we want to ignore metavariables occurring in the type of local constants occurring in mvar_type.
// This can happen when type class resolution is invoked from the unifier.
return false;
}
auto cname = is_class(mvar_type);
if (!cname)
return false;