feat(frontends/lean): improve error messages when elaborator cannot instantiate all metavariables

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

src/frontends/lean/frontend_elaborator.cpp

@@ -435,7 +435,7 @@ public:
         m_normalizer(m_env) {
     }
 
-    expr elaborate(expr const & e) {
+    std::pair<expr, metavar_env> elaborate(expr const & e) {
         // std::cout << "Elaborate " << e << "\n";
         clear();
         expr new_e = preprocessor(*this)(e);
@@ -447,9 +447,9 @@ public:
             //     std::cout << c.pp(fmt, options(), nullptr, false) << "\n";
             // }
             metavar_env new_menv = elaborate_core();
-            return new_menv->instantiate_metavars(new_e);
+            return mk_pair(new_menv->instantiate_metavars(new_e), new_menv);
         } else {
-            return new_e;
+            return mk_pair(new_e, metavar_env());
         }
     }
 
@@ -505,7 +505,7 @@ public:
 
 frontend_elaborator::frontend_elaborator(environment const & env):m_ptr(new imp(env)) {}
 frontend_elaborator::~frontend_elaborator() {}
-expr frontend_elaborator::operator()(expr const & e) { return m_ptr->elaborate(e); }
+std::pair<expr, metavar_env> frontend_elaborator::operator()(expr const & e) { return m_ptr->elaborate(e); }
 std::tuple<expr, expr, metavar_env> frontend_elaborator::operator()(name const & n, expr const & t, expr const & e) {
     return m_ptr->elaborate(n, t, e);
 }

src/frontends/lean/frontend_elaborator.h

@@ -29,7 +29,7 @@ public:
     /**
        \brief Elaborate the given expression.
     */
-    expr operator()(expr const & e);
+    std::pair<expr, metavar_env> operator()(expr const & e);
     /**
        \brief Elaborate the given type and expression. The typeof(e) == t.
        This information is used by the elaborator. The result is a new

src/frontends/lean/parser.cpp

@@ -34,6 +34,7 @@ Author: Leonardo de Moura
 #include "kernel/printer.h"
 #include "kernel/metavar.h"
 #include "kernel/for_each_fn.h"
+#include "kernel/find_fn.h"
 #include "kernel/type_checker_justification.h"
 #include "library/expr_lt.h"
 #include "library/type_inferer.h"
@@ -190,6 +191,15 @@ class parser::imp {
         virtual void rethrow() const { throw *this; }
     };
 
+    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) {}
+    };
+
     template<typename F>
     typename std::result_of<F(lua_State * L)>::type using_script(F && f) {
         return m_script_state->apply([&](lua_State * L) {
@@ -371,6 +381,14 @@ class parser::imp {
         regular(m_io_state) << " " << ex << endl;
     }
 
+    void display_error(metavar_not_synthesized_exception const & ex) {
+        display_error_pos(some_expr(m_elaborator.get_original(ex.m_mvar)));
+        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";
+    }
+
     struct lean_pos_info_provider : public pos_info_provider {
         imp const & m_ref;
         lean_pos_info_provider(imp const & r):m_ref(r) {}
@@ -450,6 +468,13 @@ class parser::imp {
             sync();
             if (m_use_exceptions)
                 throw;
+        } catch (metavar_not_synthesized_exception & ex) {
+            m_found_errors = true;
+            if (m_show_errors)
+                display_error(ex);
+            sync();
+            if (m_use_exceptions)
+                throw;
         } catch (script_exception & ex) {
             m_found_errors = true;
             reset_interrupt();
@@ -1730,6 +1755,35 @@ class parser::imp {
         }
     }
 
+    std::pair<expr, context> get_metavar_ctx_and_type(expr const & mvar, metavar_env const & menv) {
+        expr mvar_type = menv->instantiate_metavars(menv->get_type(mvar));
+        buffer<context_entry> new_entries;
+        for (auto e : menv->get_context(mvar)) {
+            optional<expr> d = e.get_domain();
+            optional<expr> b = e.get_body();
+            if (d) d = menv->instantiate_metavars(*d);
+            if (b) b = menv->instantiate_metavars(*b);
+            if (d)
+                new_entries.emplace_back(e.get_name(), *d, b);
+            else
+                new_entries.emplace_back(e.get_name(), d, *b);
+        }
+        context mvar_ctx(to_list(new_entries.begin(), new_entries.end()));
+        return mk_pair(mvar_type, mvar_ctx);
+    }
+
+    /** \brief Throw an exception if \c e contains a metavariable */
+    void 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 (m) {
+            auto p = get_metavar_ctx_and_type(*m, menv);
+            throw metavar_not_synthesized_exception(p.second, *m, p.first, msg);
+        }
+    }
+    void check_no_metavar(std::pair<expr, metavar_env> const & p, char const * msg) {
+        check_no_metavar(p.first, p.second, msg);
+    }
+
     /**
        \brief Try to fill the 'holes' in \c val using tactics.
        The metavar_env \c menv contains the definition of the metavariables occurring in \c val.
@@ -1748,23 +1802,14 @@ class parser::imp {
             });
         std::sort(mvars.begin(), mvars.end(), [](expr const & e1, expr const & e2) { return is_lt(e1, e2, false); });
         for (auto mvar : mvars) {
-            expr    mvar_type = menv->instantiate_metavars(menv->get_type(mvar));
+            auto p = get_metavar_ctx_and_type(mvar, menv);
+            expr mvar_type   = p.first;
+            context mvar_ctx = p.second;
             if (has_metavar(mvar_type))
-                throw exception("failed to synthesize metavar, its type contains metavariables");
-            buffer<context_entry> new_entries;
-            for (auto e : menv->get_context(mvar)) {
-                optional<expr> d = e.get_domain();
-                optional<expr> b = e.get_body();
-                if (d) d = menv->instantiate_metavars(*d);
-                if (b) b = menv->instantiate_metavars(*b);
-                if (d)
-                    new_entries.emplace_back(e.get_name(), *d, b);
-                else
-                    new_entries.emplace_back(e.get_name(), d, *b);
-            }
-            context mvar_ctx(to_list(new_entries.begin(), new_entries.end()));
+                throw metavar_not_synthesized_exception(mvar_ctx, mvar, mvar_type,
+                                                        "failed to synthesize metavar, its type contains metavariables");
             if (!m_type_inferer.is_proposition(mvar_type, mvar_ctx))
-                throw exception("failed to synthesize metavar, its type is not a proposition");
+                throw metavar_not_synthesized_exception(mvar_ctx, mvar, mvar_type, "failed to synthesize metavar, its type is not a proposition");
             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);
             if (hint_and_pos.first) {
@@ -1828,13 +1873,13 @@ class parser::imp {
         expr type = std::get<0>(r);
         expr val  = std::get<1>(r);
         metavar_env menv = std::get<2>(r);
-        if (has_metavar(type))
-            throw exception("invalid definition, type still contains metavariables after elaboration");
+        check_no_metavar(type, menv, "invalid definition, type still contains metavariables after elaboration");
         if (!is_definition && has_metavar(val)) {
             val = apply_tactics(val, menv);
+        } else {
+            check_no_metavar(val, menv, "invalid definition, value still contains metavariables after elaboration");
         }
-        if (has_metavar(val))
-            throw exception("invalid definition, value still contains metavariables after elaboration");
+        lean_assert(!has_metavar(val));
         if (is_definition) {
             m_env->add_definition(id, type, val);
             if (m_verbose)
@@ -1877,13 +1922,17 @@ class parser::imp {
         expr type;
         if (curr_is_colon()) {
             next();
-            type = m_elaborator(parse_expr());
+            auto p = m_elaborator(parse_expr());
+            check_no_metavar(p, "invalid declaration, type still contains metavariables after elaboration");
+            type = p.first;
         } else {
             mk_scope scope(*this);
             parse_object_bindings(bindings);
             check_colon_next("invalid variable/axiom declaration, ':' expected");
             expr type_body = parse_expr();
-            type = m_elaborator(mk_abstraction(false, bindings, type_body));
+            auto p = m_elaborator(mk_abstraction(false, bindings, type_body));
+            check_no_metavar(p, "invalid declaration, type still contains metavariables after elaboration");
+            type = p.first;
         }
         if (is_var)
             m_env->add_var(id, type);
@@ -1939,7 +1988,7 @@ class parser::imp {
     /** \brief Parse 'Eval' expr */
     void parse_eval() {
         next();
-        expr v = m_elaborator(parse_expr());
+        expr v = m_elaborator(parse_expr()).first;
         normalizer norm(m_env);
         expr r = norm(v, context(), true);
         regular(m_io_state) << r << endl;
@@ -1991,7 +2040,7 @@ class parser::imp {
                 throw parser_error("invalid Show command, expression, 'Options' or 'Environment' expected", m_last_cmd_pos);
             }
         } else {
-            expr v = m_elaborator(parse_expr());
+            expr v = m_elaborator(parse_expr()).first;
             regular(m_io_state) << v << endl;
         }
     }
@@ -1999,7 +2048,9 @@ class parser::imp {
     /** \brief Parse 'Check' expr */
     void parse_check() {
         next();
-        expr v = m_elaborator(parse_expr());
+        auto p = m_elaborator(parse_expr());
+        check_no_metavar(p, "invalid expression, it still contains metavariables after elaboration");
+        expr v = p.first;
         expr t = infer_type(v, m_env);
         formatter fmt = m_io_state.get_formatter();
         options opts  = m_io_state.get_options();
@@ -2441,7 +2492,9 @@ public:
     /** \brief Parse an expression. */
     expr parse_expr_main() {
         try {
-            return m_elaborator(parse_expr());
+            auto p = m_elaborator(parse_expr());
+            check_no_metavar(p, "invalid expression, it still contains metavariables after elaboration");
+            return p.first;
         } catch (parser_error & ex) {
             throw parser_exception(ex.what(), ex.m_pos.first, ex.m_pos.second);
         }

src/frontends/lean/pp.cpp

@@ -1216,14 +1216,17 @@ class pp_formatter_cell : public formatter_cell {
             c2 = replace_var_with_name(fake_context_rest(c2), n1);
         }
         if (include_e) {
-            if (first)
-                r += format{line(), fn(c2)};
-            else
+            if (!first) {
+                bool unicode     = get_pp_unicode(opts);
+                format turnstile = unicode ? format("\u22A2") /* ⊢ */ : format("|-");
+                r += format{line(), turnstile, space(), fn(c2)};
+            } else {
                 r = fn(c2);
+            }
+            return group(r);
         } else {
-            return r;
+            return group(r);
         }
-        return r;
     }
 
     format pp_definition(char const * kwd, name const & n, expr const & t, expr const & v, options const & opts) {

tests/lean/elab1.lean.expected.out

@@ -108,7 +108,8 @@ Failed to solve
                                          ⊢ ?M::1 ≈ nat_to_real
                                             Assumption 2
   Assumed: g
-Error (line: 7, pos: 8) unexpected metavariable occurrence
+Error (line: 7, pos: 8) invalid expression, it still contains metavariables after elaboration, metavariable: ?M::1, type:
+Type
   Assumed: h
 Failed to solve
 x : ?M::0, A : Type ⊢ ?M::0 ≺ A

tests/lean/lua8.lean.expected.out

@@ -1,7 +1,6 @@
   Set: pp::colors
   Set: pp::unicode
   Assumed: x
-x : ℤ,
-y : ℤ
+x : ℤ, y : ℤ
 Variable x : ℤ
 nil

tests/lean/ty1.lean.expected.out

@@ -3,7 +3,8 @@
   Assumed: i
 λ x : ℤ, x + i : ℤ → ℤ
 λ x : ℕ, x + 1 : ℕ → ℕ
-Error (line: 4, pos: 10) unexpected metavariable occurrence
+Error (line: 4, pos: 10) invalid expression, it still contains metavariables after elaboration, metavariable: ?M::0, type:
+(Type U)
 λ x y : ℤ, y + i + 1 + x : ℤ → ℤ → ℤ
 (λ x : ℤ, x) i : ℤ
 (λ x : ℤ → ℤ → ℤ, x i) (λ x y : ℤ, x + 1 + y) : ℤ → ℤ