fix(frontends/lean/pp): fix #1922

Fixes #1922

src/frontends/lean/pp.cpp

@@ -856,23 +856,25 @@ auto pretty_fn::pp_structure_instance(expr const & e) -> result {
     }
 }
 
-static bool is_field_notation_candidate(environment const & env, expr const & e, bool implicit) {
+bool pretty_fn::is_field_notation_candidate(expr const & e) {
     expr const & f = get_app_fn(e);
     if (!is_constant(f)) return false;
-    projection_info const * info = get_projection_info(env, const_name(f));
+    projection_info const * info = get_projection_info(m_env, const_name(f));
     if (!info) return false; /* it is not a projection */
     if (get_app_num_args(e) != info->m_nparams + 1) return false;
     /* If implicit arguments is true, and the structure has parameters, we should not
        pretty print using field notation because we will not be able to see the parameters. */
-    if (implicit && info->m_nparams) return false;
+    if (m_implict && info->m_nparams) return false;
+    /* The @ explicitness annotation cannot be combined with field notation, so fail on implicit args */
+    if (m_implict && has_implicit_args(e)) return false;
     name const & S = const_name(f).get_prefix();
     /* We should not use field notation with type classes since the structure is implicit. */
-    if (is_class(env, S)) return false;
+    if (is_class(m_env, S)) return false;
     return true;
 }
 
 auto pretty_fn::pp_field_notation(expr const & e) -> result {
-    lean_assert(is_field_notation_candidate(m_env, e, m_implict));
+    lean_assert(is_field_notation_candidate(e));
     buffer<expr> args;
     expr const & f   = get_app_args(e, args);
     bool ignore_hide = true;
@@ -888,7 +890,7 @@ auto pretty_fn::pp_app(expr const & e) -> result {
     expr const & fn = app_fn(e);
     if (m_structure_instances && is_structure_instance(m_env, e, m_implict))
         return pp_structure_instance(e);
-    if (m_structure_projections && is_field_notation_candidate(m_env, e, m_implict))
+    if (m_structure_projections && is_field_notation_candidate(e))
         return pp_field_notation(e);
     // If the application contains a metavariable, then we want to
     // show the function, otherwise it would be hard to understand the

src/frontends/lean/pp.h

@@ -142,6 +142,7 @@ private:
     result pp_app(expr const & e);
     result pp_lambda(expr const & e);
     result pp_structure_instance(expr const & e);
+    bool is_field_notation_candidate(expr const & e);
     result pp_field_notation(expr const & e);
     result pp_pi(expr const & e);
     result pp_have(expr const & e);

tests/lean/1922.lean

@@ -0,0 +1,8 @@
+set_option pp.implicit true
+
+structure C :=
+( d : Π { X : Type }, list X → list X )
+
+def P(c : C):= c.d [0]
+
+#print P

tests/lean/1922.lean.expected.out

@@ -0,0 +1,2 @@
+def P : C → list ℕ :=
+λ (c : C), @C.d c ℕ [0]