From c33fd8b0fdb0b9e1127fdc79ac00534ac0c5df5b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 18 Jun 2017 16:12:01 -0700
Subject: [PATCH] fix(frontends/lean/elaborator): fixes #1669

---
 src/frontends/lean/elaborator.cpp | 8 +++++---
 src/frontends/lean/elaborator.h   | 2 +-
 tests/lean/1669.lean              | 3 +++
 tests/lean/1669.lean.expected.out | 5 +++++
 4 files changed, 14 insertions(+), 4 deletions(-)
 create mode 100644 tests/lean/1669.lean
 create mode 100644 tests/lean/1669.lean.expected.out

diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 5db8be9207..91686ac796 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -2291,7 +2291,7 @@ bool elaborator::keep_do_failure_eq(expr const & first_eq) {
     return is_app(type) && is_monad_fail(app_fn(type));
 }
 
-expr elaborator::mk_aux_meta_def(expr const & e) {
+expr elaborator::mk_aux_meta_def(expr const & e, expr const & ref) {
     name aux_name(m_decl_name, "_aux_meta");
     aux_name = aux_name.append_after(m_aux_meta_idx);
     m_aux_meta_idx++;
@@ -2299,7 +2299,9 @@ expr elaborator::mk_aux_meta_def(expr const & e) {
     metavar_context mctx = m_ctx.mctx();
     std::tie(m_env, new_c) = mk_aux_definition(m_env, mctx, local_context(),
                                                aux_name, e, optional<bool>(true));
-    lean_assert(is_constant(new_c));
+    if (!is_constant(new_c)) {
+        throw elaborator_exception(ref, "failed to create auxiliary definition");
+    }
     m_env = vm_compile(m_env, m_env.get(const_name(new_c)));
     m_ctx.set_env(m_env);
     m_ctx.set_mctx(mctx);
@@ -2323,7 +2325,7 @@ expr elaborator::visit_equations(expr const & e) {
         new_tacs  = visit(equations_wf_tactics(e), some_expr(type));
         new_tacs  = enforce_type(*new_tacs, type, "well_founded_tactics object expected", ref);
         if (!is_constant(*new_tacs)) {
-            new_tacs = mk_aux_meta_def(*new_tacs);
+            new_tacs = mk_aux_meta_def(*new_tacs, ref);
         }
     }
 
diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h
index 184b2026cd..823843311e 100644
--- a/src/frontends/lean/elaborator.h
+++ b/src/frontends/lean/elaborator.h
@@ -286,7 +286,7 @@ private:
     expr mk_auto_param(expr const & name_lit, expr const & expected_type, expr const & ref);
     optional<expr> process_optional_and_auto_params(expr type, expr const & ref, buffer<expr> & eta_args, buffer<expr> & new_args);
 
-    expr mk_aux_meta_def(expr const & e);
+    expr mk_aux_meta_def(expr const & e, expr const & ref);
 
 public:
     elaborator(environment const & env, options const & opts, name const & decl_name,
diff --git a/tests/lean/1669.lean b/tests/lean/1669.lean
new file mode 100644
index 0000000000..26ce7ed58c
--- /dev/null
+++ b/tests/lean/1669.lean
@@ -0,0 +1,3 @@
+def f : ℕ → ℕ
+| a := f a
+using_well_founded ⟨{0}, well_founded_tactics.default_dec_tac⟩
diff --git a/tests/lean/1669.lean.expected.out b/tests/lean/1669.lean.expected.out
new file mode 100644
index 0000000000..349e62da0e
--- /dev/null
+++ b/tests/lean/1669.lean.expected.out
@@ -0,0 +1,5 @@
+1669.lean:3:20: error: failed to synthesize type class instance for
+⊢ has_emptyc (expr → list expr → tactic unit)
+1669.lean:3:20: error: failed to synthesize type class instance for
+⊢ has_insert ?m_1 (expr → list expr → tactic unit)
+1669.lean:1:4: error: failed to create auxiliary definition