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

feat(library/unifier): add more information in error messages due to type errors when assigning metavariables

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-08-03 09:49:30 -07:00
parent 938b4e8421
commit 50b0c17092
2 changed files with 34 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

26
src/library/unifier.cpp
View file

@ -476,6 +476,29 @@ struct unifier_fn {
} }
} }
justification mk_assign_justification(expr const & m, expr const & m_type, expr const & v_type, justification const & j) {
auto r = j.get_main_expr();
if (!r) r = m;
justification new_j = mk_justification(r, [=](formatter const & fmt, substitution const & subst) {
substitution s(subst);
format r = format("type error in placeholder when trying to solve");
r += nest(2*get_pp_indent(fmt.get_options()), compose(line(), j.pp(fmt, nullptr, subst)));
expr _m = s.instantiate(m);
if (!is_meta(_m)) {
r += compose(line(), format("placeholder was assigned to"));
r += pp_indent_expr(fmt, _m);
}
format expected_fmt, given_fmt;
std::tie(expected_fmt, given_fmt) = pp_until_different(fmt, m_type, v_type);
r += compose(line(), format("placeholder is expected of type"));
r += expected_fmt;
r += compose(line(), format("but is given type"));
r += given_fmt;
return r;
});
return mk_composite1(new_j, j);
}
/** /**
\brief Assign \c v to metavariable \c m with justification \c j. \brief Assign \c v to metavariable \c m with justification \c j.
The type of v and m are inferred, and is_def_eq is invoked. The type of v and m are inferred, and is_def_eq is invoked.
@ -499,7 +522,8 @@ struct unifier_fn {
return false; return false;
} }
lean_assert(!in_conflict()); lean_assert(!in_conflict());
if (!is_def_eq(m_type, v_type, j, relax)) justification new_j = mk_assign_justification(m, m_type, v_type, j);
if (!is_def_eq(m_type, v_type, new_j, relax))
return false; return false;
auto it = m_mvar_occs.find(mlocal_name(m)); auto it = m_mvar_occs.find(mlocal_name(m));
if (it) { if (it) {

11
tests/lean/empty.lean.expected.out
View file

@ -1,2 +1,9 @@
empty.lean:5:25: error: failed to synthesize placeholder empty.lean:5:25: error: type error in placeholder when trying to solve
⊢ inhabited Empty failed to synthesize placeholder
⊢ inhabited Empty
placeholder was assigned to
inhabited_Prop
placeholder is expected of type
inhabited ?M_1
but is given type
inhabited Prop