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

feat(library/unifier): improve error message when metavar assignment is type incorrect

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-19 21:21:34 +01:00
parent e39a6e732a
commit 438a42d010
2 changed files with 6 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/kernel/error_msgs.cpp
View file

@ -41,7 +41,7 @@ format pp_def_type_mismatch(formatter const & fmt, name const & n, expr const &
}
format pp_type_mismatch(formatter const & fmt, expr const & expected_type, expr const & given_type) {
format r("type mismatch, expected type");
format r("type mismatch, expected type:");
r += ::lean::pp_indent_expr(fmt, expected_type);
r += compose(line(), format("given type:"));
r += ::lean::pp_indent_expr(fmt, given_type);

6
src/library/unifier.cpp
View file

@ -17,6 +17,7 @@ Author: Leonardo de Moura
#include "kernel/instantiate.h"
#include "kernel/type_checker.h"
#include "kernel/kernel_exception.h"
#include "kernel/error_msgs.h"
#include "library/occurs.h"
#include "library/unifier.h"
#include "library/opaque_hints.h"
@ -431,7 +432,10 @@ struct unifier_fn {
}
if (in_conflict())
return false;
if (!is_def_eq(m_type, v_type, j))
justification j1 = mk_justification(m, [=](formatter const & fmt, substitution const & subst) {
return pp_type_mismatch(fmt, subst.instantiate(m_type), subst.instantiate(v_type));
});
if (!is_def_eq(m_type, v_type, mk_composite1(j1, j)))
return false;
auto it = m_mvar_occs.find(mlocal_name(m));
if (it) {