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

@@ -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);
+            }
         }
     }
 }

tests/lean/run/emptycOverloadIssues.lean

@@ -0,0 +1,8 @@
+structure A :=
+(x : Nat := 10)
+
+abbrev B := A
+
+structure C :=
+(a : A := {})
+(b : B := {})