From cc6104b369dafe920af0b591e013b5bf2bca4cfa Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 11 Sep 2020 14:04:44 -0700
Subject: [PATCH] fix: bug in the old frontend

It had to be fixed because we have code that needs to be compiled with
the old frontend, and the hacks we used to workaround this issue are
incompatible with the new frontend.
---
 src/frontends/lean/elaborator.cpp        | 20 ++++++++++++--------
 tests/lean/run/emptycOverloadIssues.lean |  8 ++++++++
 2 files changed, 20 insertions(+), 8 deletions(-)
 create mode 100644 tests/lean/run/emptycOverloadIssues.lean

diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index f49f355660..30ace798c7 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -3519,14 +3519,18 @@ expr elaborator::visit_emptyc_or_emptys(expr const & e, optional<expr> const & e
     } else {
         synthesize_type_class_instances();
         expr new_expected_type = instantiate_mvars(*expected_type);
-        if (is_optional_param(new_expected_type))
-            new_expected_type = app_arg(app_fn(new_expected_type));
-        expr S = get_app_fn(new_expected_type);
-        if (is_constant(S) && is_structure(m_env, const_name(S))) {
-            expr empty_struct = copy_pos(e, mk_structure_instance(name(), buffer<name>(), buffer<expr>()));
-            return visit(empty_struct, expected_type);
-        } else {
-            return visit(mk_emptyc(e), expected_type);
+        try {
+            bool mask[2] = { true, false };
+            return mk_app(m_ctx, get_has_emptyc_emptyc_name(), 2, mask, &new_expected_type);
+        } catch (exception &) {
+            new_expected_type = whnf(new_expected_type);
+            expr S = get_app_fn(new_expected_type);
+            if (is_constant(S) && is_structure(m_env, const_name(S))) {
+                expr empty_struct = copy_pos(e, mk_structure_instance(name(), buffer<name>(), buffer<expr>()));
+                return visit(empty_struct, expected_type);
+            } else {
+                return visit(mk_emptyc(e), expected_type);
+            }
         }
     }
 }
diff --git a/tests/lean/run/emptycOverloadIssues.lean b/tests/lean/run/emptycOverloadIssues.lean
new file mode 100644
index 0000000000..c13733ba37
--- /dev/null
+++ b/tests/lean/run/emptycOverloadIssues.lean
@@ -0,0 +1,8 @@
+structure A :=
+(x : Nat := 10)
+
+abbrev B := A
+
+structure C :=
+(a : A := {})
+(b : B := {})