From 93fdfdc4b6dc4ba184595fa9b28ca117f2e37f78 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 30 Mar 2017 15:27:45 +0200
Subject: [PATCH] feat(frontends/lean/elaborator): better error message on
 field notation that was probably supposed to be a single ident

---
 src/frontends/lean/elaborator.cpp         | 15 +++++++++++++++
 tests/lean/field_access.lean              | 19 +++++++++++--------
 tests/lean/field_access.lean.expected.out |  1 +
 3 files changed, 27 insertions(+), 8 deletions(-)

diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 760ef9f70d..e0cf7ec549 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -2372,6 +2372,21 @@ expr elaborator::visit_inaccessible(expr const & e, optional<expr> const & expec
 }
 
 name elaborator::field_to_decl(expr const & e, expr const & s, expr const & s_type) {
+    // prefer 'unknown identifier' error when lhs is a constant of non-value type
+    if (is_field_notation(e)) {
+        auto lhs = macro_arg(e, 0);
+        if (is_constant(lhs)) {
+            expr t = whnf(s_type);
+            while (is_pi(t)) {
+                t = whnf(binding_body(t));
+            }
+            if (is_sort(t)) {
+                name fname = get_field_notation_field_name(e);
+                throw elaborator_exception(lhs, format("unknown identifier '") + format(const_name(lhs)) + format(".") +
+                                                format(fname) + format("'"));
+            }
+        }
+    }
     expr I      = get_app_fn(s_type);
     if (!is_constant(I)) {
         auto pp_fn = mk_pp_ctx();
diff --git a/tests/lean/field_access.lean b/tests/lean/field_access.lean
index fb3344ef35..fdbc68f1c6 100644
--- a/tests/lean/field_access.lean
+++ b/tests/lean/field_access.lean
@@ -2,24 +2,27 @@
 
 variable l : list nat
 
-#check l^.1 -- Error l is not a structure
+#check l.1 -- Error l is not a structure
 
-#check (1, 2)^.5 -- Error insufficient fields
+#check (1, 2).5 -- Error insufficient fields
 
 example (l : list nat) : list nat :=
-l^.forr (λ x, x + 1) -- Error there is no list.forr
+l.forr (λ x, x + 1) -- Error there is no list.forr
 
 example (A : Type) (a : A) : A :=
-a^.symm -- Error type of 'a' is not a constant application
+a.symm -- Error type of 'a' is not a constant application
+
+example (A : Type) (a : A) : A :=
+eq.sym -- Error unknown identifier
 
 example (l : list nat) : list nat :=
-l^.for (λ x, x + 1)
+l.for (λ x, x + 1)
 
 example (l : list nat) : list nat :=
-l^.for (λ x, x + 1)
+l.for (λ x, x + 1)
 
 example (a b : nat) (h : a = b) : b = a :=
-h^.symm
+h.symm
 
 example (a b : nat) (h : a = b) : b = a :=
-h^.symm
+h.symm
diff --git a/tests/lean/field_access.lean.expected.out b/tests/lean/field_access.lean.expected.out
index f9ada085c3..d991dee6bf 100644
--- a/tests/lean/field_access.lean.expected.out
+++ b/tests/lean/field_access.lean.expected.out
@@ -15,3 +15,4 @@ field_access.lean:13:1: error: invalid '^.' notation, type is not of the form (C
   a
 has type
   A
+field_access.lean:16:0: error: unknown identifier 'eq.sym'