fix(library/tactic/eval,kernel/kernel_exception): hide internal definition name on eval_expr type error

src/kernel/kernel_exception.cpp

@@ -9,10 +9,15 @@ Author: Leonardo de Moura
 #include "util/sstream.h"
 #include "kernel/scope_pos_info_provider.h"
 #include "kernel/kernel_exception.h"
+#include "kernel/error_msgs.h"
 
 namespace lean {
 format kernel_exception::pp(formatter const &) const { return format(what()); }
 
+format definition_type_mismatch_exception::pp(formatter const & fmt) const {
+    return pp_def_type_mismatch(fmt, m_decl.get_name(), m_decl.get_type(), m_given_type, true);
+}
+
 class generic_kernel_exception : public kernel_exception {
 protected:
     optional<pos_info> m_pos;

src/kernel/kernel_exception.h

@@ -7,6 +7,7 @@ Author: Leonardo de Moura
 #pragma once
 #include "kernel/environment.h"
 #include "kernel/ext_exception.h"
+#include "kernel/scope_pos_info_provider.h"
 
 namespace lean {
 class environment;
@@ -24,6 +25,19 @@ public:
     virtual void rethrow() const override { throw *this; }
 };
 
+class definition_type_mismatch_exception : public kernel_exception {
+    declaration m_decl;
+    expr m_given_type;
+public:
+    definition_type_mismatch_exception(environment const & env, declaration const & decl, expr const & given_type):
+            kernel_exception(env), m_decl(decl), m_given_type(given_type) {}
+    expr const & get_given_type() const { return m_given_type; }
+    virtual optional<pos_info> get_pos() const override { return get_pos_info(m_decl.get_value()); }
+    virtual format pp(formatter const & fmt) const override;
+    virtual throwable * clone() const override { return new definition_type_mismatch_exception(m_env, m_decl, m_given_type); }
+    virtual void rethrow() const override { throw *this; }
+};
+
 [[ noreturn ]] void throw_kernel_exception(environment const & env, char const * msg, optional<expr> const & m = none_expr());
 [[ noreturn ]] void throw_kernel_exception(environment const & env, sstream const & strm, optional<expr> const & m = none_expr());
 [[ noreturn ]] void throw_kernel_exception(environment const & env, char const * msg, expr const & m);

src/kernel/type_checker.cpp

@@ -735,9 +735,7 @@ static void check_definition(environment const & env, declaration const & d, typ
     check_no_mlocal(env, d.get_name(), d.get_value(), false);
     expr val_type = checker.check(d.get_value(), d.get_univ_params());
     if (!checker.is_def_eq(val_type, d.get_type())) {
-        throw_kernel_exception(env, d.get_value(), [=](formatter const &fmt) {
-            return pp_def_type_mismatch(fmt, d.get_name(), d.get_type(), val_type, true);
-        });
+        throw definition_type_mismatch_exception(env, d, val_type);
     }
 }
 

src/library/tactic/eval.cpp

@@ -7,6 +7,7 @@ Author: Leonardo de Moura
 #include "util/fresh_name.h"
 #include "kernel/type_checker.h"
 #include "kernel/kernel_exception.h"
+#include "kernel/error_msgs.h"
 #include "library/vm/vm.h"
 #include "library/vm/vm_expr.h"
 #include "library/compiler/vm_compiler.h"
@@ -29,13 +30,25 @@ static vm_obj eval(expr const & A, expr a, tactic_state const & s) {
         vm_state & S = get_vm_state();
         environment aux_env = S.env();
         name eval_aux_name = mk_tagged_fresh_name("_eval_expr");
-        /* We use nested_exception_without_pos to make sure old position information nested in 'a' is used
-           in type error messages. */
         try {
             auto cd = check(aux_env, mk_definition(aux_env, eval_aux_name, {}, A, a, true, false));
             aux_env = aux_env.add(cd);
+        } catch (definition_type_mismatch_exception & ex) {
+            expr given_type = ex.get_given_type();
+            return tactic::mk_exception([=]() {
+                io_state_stream ios = tout();
+                formatter fmt = ios.get_formatter();
+
+                format expected_fmt, given_fmt;
+                std::tie(expected_fmt, given_fmt) = pp_until_different(fmt, A, given_type);
+                return format("type error at eval_expr, argument has type '") + given_fmt +
+                    compose(line(), format("but is expected to have type")) +
+                    expected_fmt;
+            }, s);
         } catch (kernel_exception & ex) {
-            return tactic::mk_exception(nested_exception_without_pos("eval_expr failed due to type error", ex), s);
+            /* We use nested_exception_without_pos to make sure old position information nested in 'a' is not used
+               in type error messages. */
+            return tactic::mk_exception(nested_exception_without_pos("eval_expr failed", ex), s);
         }
         try {
             aux_env = vm_compile(aux_env, aux_env.get(eval_aux_name));

tests/lean/type_error_at_eval_expr.lean.expected.out

@@ -1,6 +1,4 @@
-type_error_at_eval_expr.lean:3:0: error: eval_expr failed due to type error
-nested exception message:
-type mismatch at definition '_eval_expr.16.500', has type
+type_error_at_eval_expr.lean:3:0: error: type error at eval_expr, argument has type '
   list ℕ
 but is expected to have type
   ℕ