From b14a248dcddfbfadee79a7bd12d3dc33993af85b Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Mon, 29 May 2017 07:37:50 +0200
Subject: [PATCH] fix(frontends/lean/structure_cmd): segfault

---
 src/frontends/lean/structure_cmd.cpp            |  2 ++
 tests/lean/1279.lean.expected.out               | 17 -----------------
 tests/lean/structure_elab_segfault.lean         |  1 +
 .../structure_elab_segfault.lean.expected.out   |  2 ++
 4 files changed, 5 insertions(+), 17 deletions(-)
 create mode 100644 tests/lean/structure_elab_segfault.lean
 create mode 100644 tests/lean/structure_elab_segfault.lean.expected.out

diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp
index e89f9b9e64..2585b61195 100644
--- a/src/frontends/lean/structure_cmd.cpp
+++ b/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();
diff --git a/tests/lean/1279.lean.expected.out b/tests/lean/1279.lean.expected.out
index 0095aadb4e..96706aa67a 100644
--- a/tests/lean/1279.lean.expected.out
+++ b/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
diff --git a/tests/lean/structure_elab_segfault.lean b/tests/lean/structure_elab_segfault.lean
new file mode 100644
index 0000000000..92aea08c95
--- /dev/null
+++ b/tests/lean/structure_elab_segfault.lean
@@ -0,0 +1 @@
+structure test : Type := (f : ∀ x y, true)
diff --git a/tests/lean/structure_elab_segfault.lean.expected.out b/tests/lean/structure_elab_segfault.lean.expected.out
new file mode 100644
index 0000000000..1e8434c1f3
--- /dev/null
+++ b/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]