diff --git a/src/frontends/lean/definition_cmds.cpp b/src/frontends/lean/definition_cmds.cpp
index f286f74784..5e750c3963 100644
--- a/src/frontends/lean/definition_cmds.cpp
+++ b/src/frontends/lean/definition_cmds.cpp
@@ -144,7 +144,7 @@ environment mutual_definition_cmd_core(parser & p, def_cmd_kind kind, decl_modif
     buffer<expr> fns, params;
     declaration_info_scope scope(p, kind, modifiers);
     expr val = parse_mutual_definition(p, lp_names, fns, params);
-    elaborator elab(p.env(), p.get_options(), metavar_context(), local_context());
+    elaborator elab(p.env(), p.get_options(), metavar_context(), local_context(), p.infom());
     buffer<expr> new_params;
     elaborate_params(elab, params, new_params);
     val = replace_locals_preserving_pos_info(val, params, new_params);
@@ -562,7 +562,7 @@ environment single_definition_cmd_core(parser & p, def_cmd_kind kind, decl_modif
     if (is_instance)
         attrs.set_attribute(p.env(), "instance");
     std::tie(fn, val) = parse_definition(p, lp_names, params, is_example, is_instance);
-    elaborator elab(p.env(), p.get_options(), metavar_context(), local_context());
+    elaborator elab(p.env(), p.get_options(), metavar_context(), local_context(), p.infom());
     buffer<expr> new_params;
     elaborate_params(elab, params, new_params);
     elab.set_instance_fingerprint();
diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 92026f52a3..3e5a26f9c5 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -104,7 +104,7 @@ elaborator_strategy get_elaborator_strategy(environment const & env, name const
 #define trace_elab_debug(CODE) lean_trace("elaborator_debug", scope_trace_env _scope(m_env, m_ctx); CODE)
 
 elaborator::elaborator(environment const & env, options const & opts, metavar_context const & mctx,
-                       local_context const & lctx, optional<info_manager> infom):
+                       local_context const & lctx, optional<info_manager> & infom):
     m_env(env), m_opts(opts),
     m_ctx(env, opts, mctx, lctx, get_tcm(), transparency_mode::Semireducible), m_infom(infom) {
     unsigned line, col;
@@ -656,8 +656,10 @@ expr elaborator::visit_const_core(expr const & e) {
 /** \brief Auxiliary function for saving information about which overloaded identifier was used by the elaborator. */
 void elaborator::save_identifier_info(expr const & f) {
     if (!m_no_info && m_infom && get_pos_info_provider() && is_constant(f)) {
-        if (auto p = get_pos_info_provider()->get_pos_info(f))
+        if (auto p = get_pos_info_provider()->get_pos_info(f)) {
             m_infom->add_identifier_info(p->first, p->second, const_name(f));
+            m_infom->add_type_info(p->first, p->second, infer_type(f));
+        }
     }
 }
 
@@ -680,7 +682,7 @@ expr elaborator::visit_function(expr const & fn, bool has_args, expr const & ref
     case expr_kind::Lambda:    r = visit_lambda(fn, none_expr()); break;
     case expr_kind::Let:       r = visit_let(fn, none_expr()); break;
     }
-    save_identifier_info(fn);
+    save_identifier_info(r);
     if (has_args)
         r = ensure_function(r, ref);
     return r;
@@ -2734,10 +2736,6 @@ elaborate(environment & env, options const & opts,
     auto p = elab.finalize(r, check_unassigned, true);
     mctx = elab.mctx();
     env  = elab.env();
-    if (infom) {
-        lean_assert(elab.infom());
-        infom = *elab.infom();
-    }
     return p;
 }
 
@@ -2781,7 +2779,9 @@ static expr translate(environment const & env, local_context const & lctx, expr
 
 expr nested_elaborate(environment & env, options const & opts, metavar_context & mctx, local_context const & lctx,
                       expr const & e, bool relaxed) {
-    elaborator elab(env, opts, mctx, lctx);
+    // TODO(sullrich): pass through info_manager?
+    optional<info_manager> infom;
+    elaborator elab(env, opts, mctx, lctx, infom);
     expr r = elab.elaborate(translate(env, lctx, e));
     if (!relaxed)
         elab.ensure_no_unassigned_metavars(r);
diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h
index da58fa1e2d..9429f8e419 100644
--- a/src/frontends/lean/elaborator.h
+++ b/src/frontends/lean/elaborator.h
@@ -88,7 +88,7 @@ private:
     /* Position information for show goal feature */
     optional<pos_info> m_show_goal_pos;
 
-    optional<info_manager> m_infom;
+    optional<info_manager> & m_infom;
 
     expr get_default_numeral_type();
 
@@ -239,7 +239,7 @@ private:
     void unassigned_uvars_to_params(expr const & e);
 public:
     elaborator(environment const & env, options const & opts, metavar_context const & mctx, local_context const & lctx,
-               optional<info_manager> infom = optional<info_manager>());
+               optional<info_manager> & infom);
     metavar_context const & mctx() const { return m_ctx.mctx(); }
     local_context const & lctx() const { return m_ctx.lctx(); }
     expr push_local(name const & n, expr const & type, binder_info const & bi = binder_info()) {
diff --git a/src/frontends/lean/inductive_cmds.cpp b/src/frontends/lean/inductive_cmds.cpp
index 7bec9c473c..33af73ce61 100644
--- a/src/frontends/lean/inductive_cmds.cpp
+++ b/src/frontends/lean/inductive_cmds.cpp
@@ -286,7 +286,7 @@ class inductive_cmd_fn {
     void elaborate_inductive_decls(buffer<expr> const & params, buffer<expr> const & inds, buffer<buffer<expr> > const & intro_rules,
                                    buffer<expr> & new_params, buffer<expr> & new_inds, buffer<buffer<expr> > & new_intro_rules) {
         options opts = m_p.get_options();
-        elaborator elab(m_env, opts, metavar_context(), local_context());
+        elaborator elab(m_env, opts, metavar_context(), local_context(), m_p.infom());
 
         buffer<expr> params_no_inds;
         for (expr const & p : params) {