From 549f24335e5115785d29c63665b5c6d7ffdac5f8 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 11 Oct 2014 18:40:48 -0700
Subject: [PATCH] feat(frontends/lean): do not allow coercion definition in
 sections

---
 src/frontends/lean/builtin_cmds.cpp        |  2 ++
 src/frontends/lean/decl_cmds.cpp           |  5 ++++-
 tests/lean/bad_coercions.lean              | 20 ++++++++++++++++++++
 tests/lean/bad_coercions.lean.expected.out |  2 ++
 4 files changed, 28 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/bad_coercions.lean
 create mode 100644 tests/lean/bad_coercions.lean.expected.out

diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index 18d2637ba..c92d60c62 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -377,6 +377,8 @@ environment open_cmd(parser & p) { return open_export_cmd(p, true); }
 environment export_cmd(parser & p) { return open_export_cmd(p, false); }
 
 environment coercion_cmd(parser & p) {
+    if (in_context(p.env()))
+        throw parser_error("invalid 'coercion' command, coercions cannot be defined in contexts", p.pos());
     bool persistent = false;
     parse_persistent(p, persistent);
     name f   = p.check_constant_next("invalid 'coercion' command, constant expected");
diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp
index 39c8775c2..2c48ce02c 100644
--- a/src/frontends/lean/decl_cmds.cpp
+++ b/src/frontends/lean/decl_cmds.cpp
@@ -279,8 +279,11 @@ struct decl_modifiers {
                 m_is_instance = true;
                 p.next();
             } else if (p.curr_is_token(get_coercion_tk())) {
-                m_is_coercion = true;
+                auto pos = p.pos();
                 p.next();
+                if (in_context(p.env()))
+                    throw parser_error("invalid '[coercion]' modifier, coercions cannot be defined in contexts", pos);
+                m_is_coercion = true;
             } else if (p.curr_is_token(get_reducible_tk())) {
                 m_is_reducible = true;
                 p.next();
diff --git a/tests/lean/bad_coercions.lean b/tests/lean/bad_coercions.lean
new file mode 100644
index 000000000..d8830bfbd
--- /dev/null
+++ b/tests/lean/bad_coercions.lean
@@ -0,0 +1,20 @@
+import data.nat.basic
+open nat
+
+constant list.{l} : Type.{l} → Type.{l}
+constant vector.{l} : Type.{l} → nat → Type.{l}
+constant nil (A : Type) : list A
+
+set_option pp.coercions true
+context
+  parameter A : Type
+  parameter n : nat
+
+  definition foo2 [coercion] (v : vector A n) : list A :=
+  nil A
+
+  definition foo (v : vector A n) : list A :=
+  nil A
+
+  coercion foo
+end
diff --git a/tests/lean/bad_coercions.lean.expected.out b/tests/lean/bad_coercions.lean.expected.out
new file mode 100644
index 000000000..70f7526b9
--- /dev/null
+++ b/tests/lean/bad_coercions.lean.expected.out
@@ -0,0 +1,2 @@
+bad_coercions.lean:13:18: error: invalid '[coercion]' modifier, coercions cannot be defined in contexts
+bad_coercions.lean:19:11: error: invalid 'coercion' command, coercions cannot be defined in contexts