feat(frontends/lean/builtin_exprs): use local field inference for info too

src/frontends/lean/builtin_exprs.cpp

@@ -1066,10 +1066,10 @@ static expr parse_proj(parser_state & p, unsigned, expr const * args, pos_info c
             /* failed to elaborate or infer type */
             throw ex;
         }
-        expr fn       = get_app_fn(lhs_type);
+        expr fn = get_app_fn(lhs_type);
         if (is_constant(fn)) {
-            ex.m_token_info.m_struct  = const_name(fn);
             ex.m_token_info.m_context = break_at_pos_exception::token_context::field;
+            ex.m_token_info.m_struct  = const_name(fn);
         }
         throw;
     }

src/frontends/lean/info_manager.h

@@ -73,7 +73,6 @@ class info_manager : public log_entry_cell {
     std::string m_file_name;
     rb_map<unsigned, line_info_data_set, unsigned_cmp> m_line_data;
 
-    line_info_data_set get_line_info_set(unsigned l) const;
     void add_info(pos_info pos, info_data data);
 public:
     info_manager() {}
@@ -89,6 +88,8 @@ public:
     void add_const_info(environment const & env, pos_info pos, name const & full_id);
     void add_vm_obj_format_info(pos_info pos, environment const & env, vm_obj const & thunk);
 
+    line_info_data_set get_line_info_set(unsigned l) const;
+
     void instantiate_mvars(metavar_context const & mctx);
     void merge(info_manager const & info);
 

src/frontends/lean/interactive.cpp

@@ -129,7 +129,14 @@ void report_info(environment const & env, options const & opts, io_state const &
                     record["tactic_param_idx"] = *idx;
                 has_token_info = true;
                 break;
-            default:
+            case break_at_pos_exception::token_context::field: {
+                auto name = e.m_token_info.m_struct + e.m_token_info.m_token;
+                record["full-id"] = name.to_string();
+                add_source_info(env, name, record);
+                if (auto doc = get_doc_string(env, name))
+                    record["doc"] = *doc;
+                interactive_report_type(env, opts, env.get(name).get_type(), record);
+            } default:
                 break;
         }
     }

tests/lean/interactive/field_info.lean

@@ -2,3 +2,12 @@ def f (n : ℕ) := n^.to_string
                   --^ "command": "info"
 def g (l : list ℕ) := l^.all
                        --^ "command": "info"
+
+-- elaborated, not locally inferable
+def h : list ℕ → (ℕ → bool) → bool :=
+λ l, (l ++ l)^.all
+              --^ "command": "info"
+
+-- not elaborated, locally inferable
+def j := (list.nil^.all
+                   --^ "command": "info"

tests/lean/interactive/field_info.lean.expected.out

@@ -1,3 +1,6 @@
+{"msgs":[{"caption":"","file_name":"f","pos_col":40,"pos_line":13,"severity":"error","text":"invalid expression, `)` expected"}],"response":"all_messages"}
 {"message":"file invalidated","response":"ok","seq_num":0}
 {"record":{"full-id":"nat.to_string","source":,"type":"ℕ → string"},"response":"ok","seq_num":2}
 {"record":{"full-id":"list.all","source":,"type":"Π {α : Type}, list α → (α → bool) → bool"},"response":"ok","seq_num":4}
+{"record":{"full-id":"list.all","source":,"type":"Π {α : Type}, list α → (α → bool) → bool"},"response":"ok","seq_num":9}
+{"record":{"full-id":"list.all","source":,"type":"Π {α : Type u}, list α → (α → bool) → bool"},"response":"ok","seq_num":13}