fix(frontends/lean/parser): fixes #858

src/frontends/lean/decl_cmds.cpp

@@ -144,7 +144,7 @@ static environment declare_var(parser & p, environment env,
         if (k == variable_kind::Parameter)
             p.add_parameter(n, l);
         else
-            p.add_local_expr(n, l, k == variable_kind::Variable);
+            p.add_variable(n, l);
         return env;
     } else {
         lean_assert(k == variable_kind::Constant || k == variable_kind::Axiom);

src/frontends/lean/parser.cpp

@@ -604,8 +604,28 @@ environment parser::add_local_ref(environment const & env, name const & n, expr
     }
 }
 
+static void check_no_metavars(name const & n, expr const & e) {
+    lean_assert(is_local(e));
+    if (has_metavar(e)) {
+        throw_generic_exception(none_expr(), [=](formatter const & fmt) {
+                format r("failed to add declaration '");
+                r += format(n);
+                r += format("' to local context, type has metavariables");
+                r += pp_until_meta_visible(fmt, mlocal_type(e));
+                return r;
+            });
+    }
+}
+
+void parser::add_variable(name const & n, expr const & v) {
+    lean_assert(is_local(v));
+    check_no_metavars(n, v);
+    add_local_expr(n, v, true);
+}
+
 void parser::add_parameter(name const & n, expr const & p) {
     lean_assert(is_local(p));
+    check_no_metavars(n, p);
     add_local_expr(n, p, false);
     m_has_params = true;
 }

src/frontends/lean/parser.h

@@ -470,6 +470,7 @@ public:
     void add_local_level(name const & n, level const & l, bool is_variable = false);
     void add_local_expr(name const & n, expr const & p, bool is_variable = false);
     environment add_local_ref(environment const & env, name const & n, expr const & ref);
+    void add_variable(name const & n, expr const & p);
     void add_parameter(name const & n, expr const & p);
     void add_local(expr const & p) { return add_local_expr(local_pp_name(p), p); }
     bool has_params() const { return m_has_params; }

src/kernel/error_msgs.h

@@ -30,4 +30,5 @@ struct scoped_set_distinguishing_pp_options {
     ~scoped_set_distinguishing_pp_options() { set_distinguishing_pp_options(m_old); }
 };
 std::tuple<format, format> pp_until_different(formatter const & fmt, expr const & e1, expr const & e2);
+format pp_until_meta_visible(formatter const & fmt, expr const & e);
 }

tests/lean/858.lean

@@ -0,0 +1,3 @@
+section
+  parameter (n : Πa, nat)
+end

tests/lean/858.lean.expected.out

@@ -0,0 +1,2 @@
+858.lean:2:2: error: failed to add declaration 'n' to local context, type has metavariables
+  ?M_1 → ℕ