feat(frontends/lean/elaborator): add support for partial explicit in the elaborator

src/frontends/lean/elaborator.cpp

@@ -670,7 +670,8 @@ expr elaborator::visit_app(expr const & e, constraint_seq & cs) {
     if (is_choice_app(e))
         return visit_choice_app(e, cs);
     constraint_seq f_cs;
-    bool expl   = is_nested_explicit(get_app_fn(e));
+    bool expl         = is_nested_explicit(get_app_fn(e));
+    bool partial_expl = is_nested_partial_explicit(get_app_fn(e));
     expr f      = visit(app_fn(e), f_cs);
     auto f_t    = ensure_fun(f, f_cs);
     f           = f_t.first;
@@ -682,10 +683,13 @@ expr elaborator::visit_app(expr const & e, constraint_seq & cs) {
                binding_info(f_type).is_implicit() ||
                binding_info(f_type).is_inst_implicit()) {
             lean_assert(binding_info(f_type).is_strict_implicit() || !first);
+            expr const & d_type = binding_domain(f_type);
+            if (partial_expl || is_pi(whnf(d_type).first))
+                break;
             tag g          = f.get_tag();
             bool is_strict = true;
             bool inst_imp  = binding_info(f_type).is_inst_implicit();
-            expr imp_arg   = mk_placeholder_meta(mk_mvar_suffix(f_type), some_expr(binding_domain(f_type)),
+            expr imp_arg   = mk_placeholder_meta(mk_mvar_suffix(f_type), some_expr(d_type),
                                                  g, is_strict, inst_imp, f_cs);
             f              = mk_app(f, imp_arg, g);
             auto f_t       = ensure_fun(f, f_cs);
@@ -1268,8 +1272,8 @@ expr elaborator::visit_equation(expr const & eq, constraint_seq & cs) {
     expr const & lhs = equation_lhs(eq);
     expr const & rhs = equation_rhs(eq);
     expr lhs_fn = get_app_fn(lhs);
-    if (is_explicit(lhs_fn))
+    if (is_explicit_or_partial_explicit(lhs_fn))
-        lhs_fn = get_explicit_arg(lhs_fn);
+        lhs_fn = get_explicit_or_partial_explicit_arg(lhs_fn);
     if (!is_local(lhs_fn))
         throw exception("ill-formed equation");
     expr new_lhs, new_rhs;
@@ -1657,9 +1661,9 @@ expr elaborator::visit_core(expr const & e, constraint_seq & cs) {
     } else if (is_consume_args(e)) {
         // ignore annotation
         return visit_core(get_consume_args_arg(e), cs);
-    } else if (is_explicit(e)) {
+    } else if (is_explicit_or_partial_explicit(e)) {
         // ignore annotation
-        return visit_core(get_explicit_arg(e), cs);
+        return visit_core(get_explicit_or_partial_explicit_arg(e), cs);
     } else if (is_sorry(e)) {
         return visit_sorry(e);
     } else if (is_equations(e)) {
@@ -1719,12 +1723,33 @@ pair<expr, constraint_seq> elaborator::visit(expr const & e) {
         r    = visit_equations(e, cs);
     } else if (is_explicit(get_app_fn(e))) {
         r    = visit_core(e, cs);
+    } else if (is_partial_explicit(get_app_fn(e))) {
+        r = visit_core(e, cs);
+        tag  g         = e.get_tag();
+        expr r_type    = whnf(infer_type(r, cs), cs);
+        expr imp_arg;
+        bool is_strict = true;
+        while (is_pi(r_type)) {
+            binder_info bi = binding_info(r_type);
+            if (!bi.is_implicit() && !bi.is_inst_implicit()) {
+                break;
+            }
+            expr const & d_type = binding_domain(r_type);
+            if (is_pi(whnf(d_type).first)) {
+                break;
+            }
+            bool inst_imp = bi.is_inst_implicit();
+            imp_arg = mk_placeholder_meta(mk_mvar_suffix(r_type), some_expr(d_type),
+                                          g, is_strict, inst_imp, cs);
+            r       = mk_app(r, imp_arg, g);
+            r_type  = whnf(instantiate(binding_body(r_type), imp_arg), cs);
+        }
     } else {
         bool consume_args = false;
         if (is_as_atomic(e)) {
             flet<bool> let(m_no_info, true);
             r = get_as_atomic_arg(e);
-            if (is_explicit(r)) r = get_explicit_arg(r);
+            if (is_explicit_or_partial_explicit(r)) r = get_explicit_or_partial_explicit_arg(r);
             r = visit_core(r, cs);
         } else if (is_consume_args(e)) {
             consume_args = true;

src/library/explicit.cpp

@@ -26,6 +26,9 @@ bool is_partial_explicit(expr const & e) { return is_annotation(e, *g_partial_ex
 bool is_nested_partial_explicit(expr const & e) { return is_nested_annotation(e, *g_partial_explicit_name); }
 expr const & get_partial_explicit_arg(expr const & e) { lean_assert(is_partial_explicit(e)); return get_annotation_arg(e); }
 
+bool is_explicit_or_partial_explicit(expr const & e) { return is_explicit(e) || is_partial_explicit(e); }
+expr get_explicit_or_partial_explicit_arg(expr const & e) { lean_assert(is_explicit_or_partial_explicit(e)); return get_annotation_arg(e); }
+
 expr mk_as_is(expr const & e) { return mk_annotation(*g_as_is_name, e); }
 bool is_as_is(expr const & e) { return is_annotation(e, *g_as_is_name); }
 expr const & get_as_is_arg(expr const & e) { lean_assert(is_as_is(e)); return get_annotation_arg(e); }

src/library/explicit.h

@@ -35,6 +35,8 @@ bool is_nested_partial_explicit(expr const & e);
 */
 expr const & get_partial_explicit_arg(expr const & e);
 
+bool is_explicit_or_partial_explicit(expr const & e);
+expr get_explicit_or_partial_explicit_arg(expr const & e);
 
 /** \brief Create an explicit expression that is accepted as is
     by the elaborator.