fix(frontends/lean/structure_cmd): segfault

src/frontends/lean/structure_cmd.cpp

@@ -923,6 +923,8 @@ struct structure_cmd_fn {
 
     /** \brief Elaborate new fields */
     void elaborate_new_fields() {
+        auto _ = m_p.no_error_recovery_scope(); // we require that m_p.elaborate_type(mk_let()) is a let, etc.
+
         using namespace std::placeholders; // NOLINT
         // NB: telescope is built inside-out, i.e. params -> parents -> fields -> typed defaults -> Prop
         expr tmp = mk_Prop();

tests/lean/1279.lean.expected.out

@@ -6,20 +6,3 @@ has type
   source.Hom A B
 but is expected to have type
   source.Hom C ?m_1
-1279.lean:12:55: error: type mismatch at application
-  target.compose (onMorphisms g) (onMorphisms f)
-term
-  onMorphisms f
-has type
-  target.Hom (onObjects A) (onObjects B)
-but is expected to have type
-  target.Hom (onObjects C) (onObjects ?m_1)
-1279.lean:12:33: error: don't know how to synthesize placeholder
-context:
-source target : Category,
-onObjects : source.Obj → target.Obj,
-onMorphisms : Π ⦃A B : source.Obj⦄, source.Hom A B → target.Hom (onObjects A) (onObjects B),
-A B C : source.Obj,
-f : source.Hom A B,
-g : source.Hom B C
-⊢ source.Obj

tests/lean/structure_elab_segfault.lean

@@ -0,0 +1 @@
+structure test : Type := (f : ∀ x y, true)

tests/lean/structure_elab_segfault.lean.expected.out

@@ -0,0 +1,2 @@
+structure_elab_segfault.lean:1:0: error: infer type failed, sort expected
+  delayed[?m_1]