From 1abaa9eb715a2e0ea21b066f71e177925e0d615f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 10 Dec 2015 10:11:23 -0800
Subject: [PATCH] fix(frontends/lean/parser): fixes #858

---
 src/frontends/lean/decl_cmds.cpp |  2 +-
 src/frontends/lean/parser.cpp    | 20 ++++++++++++++++++++
 src/frontends/lean/parser.h      |  1 +
 src/kernel/error_msgs.h          |  1 +
 tests/lean/858.lean              |  3 +++
 tests/lean/858.lean.expected.out |  2 ++
 6 files changed, 28 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/858.lean
 create mode 100644 tests/lean/858.lean.expected.out

diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp
index 656c7e043..fa5d34f23 100644
--- a/src/frontends/lean/decl_cmds.cpp
+++ b/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);
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 815d43507..852d80932 100644
--- a/src/frontends/lean/parser.cpp
+++ b/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;
 }
diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h
index 844596df6..a78a1474e 100644
--- a/src/frontends/lean/parser.h
+++ b/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; }
diff --git a/src/kernel/error_msgs.h b/src/kernel/error_msgs.h
index 0175ca493..87dc83863 100644
--- a/src/kernel/error_msgs.h
+++ b/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);
 }
diff --git a/tests/lean/858.lean b/tests/lean/858.lean
new file mode 100644
index 000000000..43aeb6ad5
--- /dev/null
+++ b/tests/lean/858.lean
@@ -0,0 +1,3 @@
+section
+  parameter (n : Πa, nat)
+end
diff --git a/tests/lean/858.lean.expected.out b/tests/lean/858.lean.expected.out
new file mode 100644
index 000000000..574ab706a
--- /dev/null
+++ b/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 → ℕ