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 := {})