feat(frontends/lean/elaborator): better error message on field notation that was probably supposed to be a single ident

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();

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

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'