feat(frontends/lean): improve error message for expressions containing unsolved metavariables

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/frontends/lean/parser_cmds.cpp

@@ -84,11 +84,8 @@ void parser_imp::register_implicit_arguments(name const & n, parameter_buffer &
 
 /** \brief Throw an exception if \c e contains a metavariable */
 void parser_imp::check_no_metavar(expr const & e, metavar_env const & menv, char const * msg) {
-    auto m = find(e, [](expr const & e) -> bool { return is_metavar(e); });
+    if (has_metavar(e))
-    if (m) {
+        throw unsolved_metavar_exception(msg, e);
-        auto p = get_metavar_ctx_and_type(*m, menv);
-        throw metavar_not_synthesized_exception(p.second, *m, p.first, msg);
-    }
 }
 
 void parser_imp::check_no_metavar(std::pair<expr, metavar_env> const & p, char const * msg) {

src/frontends/lean/parser_error.cpp

@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #include <utility>
 #include "kernel/kernel_exception.h"
+#include "kernel/for_each_fn.h"
 #include "library/io_state_stream.h"
 #include "library/elaborator/elaborator_justification.h"
 #include "frontends/lean/parser_imp.h"
@@ -50,12 +51,26 @@ void parser_imp::display_error(kernel_exception const & ex) {
     regular(m_io_state) << " " << ex << endl;
 }
 
-void parser_imp::display_error(metavar_not_synthesized_exception const & ex) {
+void parser_imp::display_error(unsolved_metavar_exception const & ex) {
-    display_error_pos(some_expr(m_elaborator.get_original(ex.m_mvar)));
+    display_error_pos(some_expr(m_elaborator.get_original(ex.get_expr())));
-    regular(m_io_state) << " " << ex.what() << ", metavariable: " << ex.m_mvar << ", type:\n";
     formatter fmt = m_io_state.get_formatter();
     options opts  = m_io_state.get_options();
-    regular(m_io_state) << mk_pair(fmt(ex.m_mvar_ctx, ex.m_mvar_type, true, opts), opts) << "\n";
+    unsigned indent = get_pp_indent(opts);
+    format r = nest(indent, compose(line(), fmt(ex.get_expr(), opts)));
+    regular(m_io_state) << " " << ex.what() << mk_pair(r, opts) << endl;
+    name_set already_displayed;
+    for_each(ex.get_expr(), [&](expr const & e, unsigned) -> bool {
+            if (is_metavar(e)) {
+                name const & m = metavar_name(e);
+                if (already_displayed.find(m) == already_displayed.end()) {
+                    already_displayed.insert(m);
+                    for (unsigned i = 0; i < indent; i++) regular(m_io_state) << " ";
+                    display_error_pos(some_expr(m_elaborator.get_original(e)));
+                    regular(m_io_state) << " unsolved metavar " << m << endl;
+                }
+            }
+            return true;
+        });
 }
 
 std::pair<unsigned, unsigned> parser_imp::lean_pos_info_provider::get_pos_info(expr const & e) const {
@@ -128,7 +143,7 @@ void parser_imp::protected_call(std::function<void()> && f, std::function<void()
         CATCH(display_error(ex));
     } catch (elaborator_exception & ex) {
         CATCH(display_error(ex));
-    } catch (metavar_not_synthesized_exception & ex) {
+    } catch (unsolved_metavar_exception & ex) {
         CATCH(display_error(ex));
     } catch (script_exception & ex) {
         reset_interrupt();

src/frontends/lean/parser_error.h

@@ -29,14 +29,4 @@ struct tactic_cmd_error : public parser_error {
     virtual exception * clone() const { return new tactic_cmd_error(m_msg.c_str(), m_pos, m_state); }
     virtual void rethrow() const { throw *this; }
 };
-
-/** \brief Exception used to report that a metavariable could not be synthesized. */
-struct metavar_not_synthesized_exception : public exception {
-    context m_mvar_ctx;
-    expr    m_mvar;
-    expr    m_mvar_type;
-public:
-    metavar_not_synthesized_exception(context const & ctx, expr const & mvar, expr const & mvar_type, char const * msg):
-        exception(msg), m_mvar_ctx(ctx), m_mvar(mvar), m_mvar_type(mvar_type) {}
-};
 }

src/frontends/lean/parser_imp.h

@@ -18,6 +18,7 @@ Author: Leonardo de Moura
 #include "library/kernel_bindings.h"
 #include "library/tactic/tactic.h"
 #include "library/elaborator/elaborator_exception.h"
+#include "library/unsolved_metavar_exception.h"
 #include "frontends/lean/scanner.h"
 #include "frontends/lean/parser_types.h"
 #include "frontends/lean/parser_error.h"
@@ -205,7 +206,7 @@ private:
     void display_error(char const * msg, unsigned line, unsigned pos);
     void display_error(char const * msg);
     void display_error(kernel_exception const & ex);
-    void display_error(metavar_not_synthesized_exception const & ex);
+    void display_error(unsolved_metavar_exception const & ex);
 
     struct lean_pos_info_provider : public pos_info_provider {
         parser_imp const & m_ref;

src/frontends/lean/parser_tactic.cpp

@@ -264,8 +264,7 @@ expr parser_imp::apply_tactics(expr const & val, metavar_env & menv) {
         expr mvar_type   = p.first;
         context mvar_ctx = p.second;
         if (has_metavar(mvar_type))
-            throw metavar_not_synthesized_exception(mvar_ctx, mvar, mvar_type,
+            throw unsolved_metavar_exception(sstream() << "failed to synthesize metavars, type of " << metavar_name(mvar) << " still contains metavariables", val);
-                                                    "failed to synthesize metavar, its type contains metavariables");
         try {
             proof_state s = to_proof_state(m_env, mvar_ctx, mvar_type);
             std::pair<optional<tactic>, pos_info> hint_and_pos = get_tactic_for(mvar);
@@ -283,7 +282,8 @@ expr parser_imp::apply_tactics(expr const & val, metavar_env & menv) {
                 menv->assign(mvar, mvar_val);
             }
         } catch (type_is_not_proposition_exception &) {
-            throw metavar_not_synthesized_exception(mvar_ctx, mvar, mvar_type, "failed to synthesize metavar, its type is not a proposition");
+            throw unsolved_metavar_exception(sstream() << "failed to synthesize metavar " << metavar_name(mvar) << ", it could not be synthesized by type inference and its type is not a proposition",
+                                             val);
         }
     }
     return menv->instantiate_metavars(val);

src/library/unsolved_metavar_exception.h

@@ -0,0 +1,27 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "util/exception.h"
+#include "util/sstream.h"
+#include "kernel/expr.h"
+
+namespace lean {
+/**
+   \brief Auxiliary exception used to sign that an expression still contains unsolved metavariables after
+   elaboration, solving, etc.
+*/
+class unsolved_metavar_exception : public exception {
+    expr m_expr;
+public:
+    unsolved_metavar_exception(char const * msg, expr const & e):exception(msg), m_expr(e) {}
+    unsolved_metavar_exception(sstream const & strm, expr const & e):exception(strm), m_expr(e) {}
+    virtual ~unsolved_metavar_exception() {}
+    expr get_expr() const { return m_expr; }
+    virtual exception * clone() const { return new unsolved_metavar_exception(m_msg.c_str(), m_expr); }
+    virtual void rethrow() const { throw *this; }
+};
+}

tests/lean/elab1.lean.expected.out

@@ -10,8 +10,9 @@ Failed to solve
         10
         ⊤
   Assumed: g
-elab1.lean:5:8: error: invalid expression, it still contains metavariables after elaboration, metavariable: ?M::1, type:
+elab1.lean:5:0: error: invalid expression, it still contains metavariables after elaboration
-Type
+    @g ℕ ?M::1 10
+    elab1.lean:5:8: error: unsolved metavar M::1
   Assumed: h
 Failed to solve
 x : ?M::0, A : Type ⊢ ?M::0 ≺ A

tests/lean/errmsg1.lean.expected.out

@@ -2,9 +2,12 @@
   Set: pp::unicode
 λ x : ?M::0, x
 λ x : ?M::0, x
-errmsg1.lean:4:10: error: invalid expression, it still contains metavariables after elaboration, metavariable: ?M::0, type:
+errmsg1.lean:4:10: error: invalid expression, it still contains metavariables after elaboration
-(Type U)
+    λ x : ?M::0, x
-errmsg1.lean:6:3: error: failed to synthesize metavar, its type is not a proposition, metavariable: ?M::0, type:
+    errmsg1.lean:4:10: error: unsolved metavar M::0
-A : Type, x : A ⊢ A → A
+errmsg1.lean:5:11: error: failed to synthesize metavar M::0, it could not be synthesized by type inference and its type is not a proposition
-errmsg1.lean:8:34: error: invalid definition, type still contains metavariables after elaboration, metavariable: ?M::3, type:
+    λ (A : Type) (x : A), ?M::0
-(Type U)
+    errmsg1.lean:6:3: error: unsolved metavar M::0
+errmsg1.lean:8:0: error: invalid definition, type still contains metavariables after elaboration
+    ∀ x : ?M::3, @eq ?M::3 x x
+    errmsg1.lean:8:34: error: unsolved metavar M::3

tests/lean/ty1.lean.expected.out

@@ -4,8 +4,9 @@
   Assumed: i
 λ x : ℤ, x + i : ℤ → ℤ
 λ x : ℕ, x + 1 : ℕ → ℕ
-ty1.lean:5:10: error: invalid expression, it still contains metavariables after elaboration, metavariable: ?M::0, type:
+ty1.lean:5:10: error: invalid expression, it still contains metavariables after elaboration
-(Type U)
+    λ x : ?M::0, x
+    ty1.lean:5:10: error: unsolved metavar M::0
 λ x y : ℤ, y + i + 1 + x : ℤ → ℤ → ℤ
 (λ x : ℤ, x) i : ℤ
 (λ x : ℤ → ℤ → ℤ, x i) (λ x y : ℤ, x + 1 + y) : ℤ → ℤ