fix(frontends/lean/elaborator): save type information for 'obtain' declarations

src/frontends/lean/elaborator.cpp

@@ -1403,7 +1403,10 @@ expr elaborator::process_obtain_expr(list<obtain_struct> const & s_list, list<ex
         lean_assert(is_local(from));
         expr const & from_type = mlocal_type(from);
         // fix user visible name
-        expr goal_domain = visit(binding_domain(goal), cs);
+        expr d0          = binding_domain(goal);
+        expr goal_domain = visit(d0, cs);
+        if (is_placeholder(d0) && !is_explicit_placeholder(d0))
+            save_binder_type(d0, goal_domain);
         expr new_from    = ::lean::mk_local(mlocal_name(from), binding_name(goal), goal_domain, binder_info());
         if (!is_lambda(goal))
             throw_elaborator_exception("invalid 'obtain' expression, insufficient number of local declarations", src);

tests/lean/interactive/obtain_type_info.input

@@ -0,0 +1,16 @@
+VISIT obtain_type_info.lean
+SYNC 12
+open eq
+inductive I (F : Type₁ → Prop) : Type₁ :=
+mk : I F
+axiom InjI : ∀ {x y}, I x = I y → x = y
+definition P (x : Type₁) : Prop := ∃ a, I a = x ∧ (a x → false).
+definition p := I P
+lemma false_of_Pp (H : P p) : false :=
+obtain a Ha0 Ha1, from H,
+  subst (InjI Ha0) Ha1 H
+lemma contradiction : false :=
+have Pp : P p, from exists.intro P (and.intro rfl false_of_Pp),
+false_of_Pp Pp
+WAIT
+INFO 8

tests/lean/interactive/obtain_type_info.input.expected.out

@@ -0,0 +1,31 @@
+-- BEGINWAIT
+-- ENDWAIT
+-- BEGININFO
+-- SYMBOL|8|0
+obtain
+-- ACK
+-- TYPE|8|7
+Type₁ → Prop
+-- ACK
+-- IDENTIFIER|8|7
+a
+-- ACK
+-- TYPE|8|9
+I a = p
+-- ACK
+-- IDENTIFIER|8|9
+Ha0
+-- ACK
+-- TYPE|8|13
+a p → false
+-- ACK
+-- IDENTIFIER|8|13
+Ha1
+-- ACK
+-- TYPE|8|23
+P p
+-- ACK
+-- IDENTIFIER|8|23
+H
+-- ACK
+-- ENDINFO