From 8621be63353b299b0da9106f4e7c8ca5e271941d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 2 Jan 2018 12:27:39 -0800
Subject: [PATCH] fix(frontends/lean): closes #1898

---
 src/frontends/lean/builtin_exprs.cpp       | 3 ---
 src/frontends/lean/elaborator.cpp          | 4 +++-
 tests/lean/1898.lean                       | 1 +
 tests/lean/1898.lean.expected.out          | 6 ++++++
 tests/lean/proj_notation.lean.expected.out | 2 +-
 5 files changed, 11 insertions(+), 5 deletions(-)
 create mode 100644 tests/lean/1898.lean
 create mode 100644 tests/lean/1898.lean.expected.out

diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp
index f8f7324de7..f8ea991611 100644
--- a/src/frontends/lean/builtin_exprs.cpp
+++ b/src/frontends/lean/builtin_exprs.cpp
@@ -1061,10 +1061,7 @@ parse_table init_nud_table() {
 static expr parse_field(parser_state & p, unsigned, expr const * args, pos_info const & pos) {
     try {
         if (p.curr_is_numeral()) {
-            pos_info num_pos = p.pos();
             unsigned fidx = p.parse_small_nat();
-            if (fidx == 0)
-                return p.parser_error_or_expr({"invalid projection, index must be greater than 0", num_pos});
             return p.save_pos(mk_field_notation(args[0], fidx), pos);
         } else {
             name field = p.check_id_next("identifier or numeral expected");
diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 47818ad787..8bed99c5a7 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -2784,7 +2784,9 @@ elaborator::field_resolution elaborator::field_to_decl(expr const & e, expr cons
         }
         auto fnames = get_structure_fields(m_env, const_name(I));
         unsigned fidx = get_field_notation_field_idx(e);
-        lean_assert(fidx > 0);
+        if (fidx  == 0) {
+            throw elaborator_exception(e, "invalid projection, index must be greater than 0");
+        }
         if (fidx > fnames.size()) {
             auto pp_fn = mk_pp_ctx();
             throw elaborator_exception(e, format("invalid projection, structure has only ") +
diff --git a/tests/lean/1898.lean b/tests/lean/1898.lean
new file mode 100644
index 0000000000..1a329b76a2
--- /dev/null
+++ b/tests/lean/1898.lean
@@ -0,0 +1 @@
+def X (R : Type) [H : comm_ring R] := H.0
diff --git a/tests/lean/1898.lean.expected.out b/tests/lean/1898.lean.expected.out
new file mode 100644
index 0000000000..f7fd3dce29
--- /dev/null
+++ b/tests/lean/1898.lean.expected.out
@@ -0,0 +1,6 @@
+1898.lean:1:39: error: invalid projection, index must be greater than 0
+1898.lean:1:4: error: don't know how to synthesize placeholder
+context:
+R : Type,
+H : comm_ring R
+⊢ Sort ?
diff --git a/tests/lean/proj_notation.lean.expected.out b/tests/lean/proj_notation.lean.expected.out
index a66fcb1824..0b3700e958 100644
--- a/tests/lean/proj_notation.lean.expected.out
+++ b/tests/lean/proj_notation.lean.expected.out
@@ -10,7 +10,7 @@ proj_notation.lean:29:19: error: invalid field notation, 'fst' is not a valid "f
 which has type
   car
 λ (c : car), ⁇ : car → ?M_1
-proj_notation.lean:31:21: error: invalid projection, index must be greater than 0
+proj_notation.lean:31:19: error: invalid projection, index must be greater than 0
 λ (c : car), ⁇ : car → ?M_1
 proj_notation.lean:33:19: error: invalid projection, structure has only 2 field(s)
   c