fix: resulting type of projection functions should not include auxiliary type annotations (e.g., autoParam)

src/Lean/Expr.lean

@@ -941,6 +941,7 @@ def isOptParam (e : Expr) : Bool :=
 def isAutoParam (e : Expr) : Bool :=
   e.isAppOfArity `autoParam 2
 
+@[export lean_expr_consume_type_annotations]
 partial def consumeTypeAnnotations (e : Expr) : Expr :=
   if e.isOptParam || e.isAutoParam then
     consumeTypeAnnotations e.appFn!.appArg!

src/library/constructions/projection.cpp

@@ -30,6 +30,9 @@ static bool is_prop(expr type) {
     return is_sort(type) && is_zero(sort_level(type));
 }
 
+extern "C" object * lean_expr_consume_type_annotations(obj_arg e);
+expr consume_type_annotations(expr const & e) { return expr(lean_expr_consume_type_annotations(e.to_obj_arg())); }
+
 environment mk_projections(environment const & env, name const & n, buffer<name> const & proj_names,
                            buffer<implicit_infer_kind> const & infer_kinds, bool inst_implicit) {
     lean_assert(proj_names.size() == infer_kinds.size());
@@ -85,7 +88,7 @@ environment mk_projections(environment const & env, name const & n, buffer<name>
         if (!is_pi(cnstr_type))
             throw exception(sstream() << "generating projection '" << proj_name << "', '"
                             << n << "' does not have sufficient data");
-        expr result_type   = binding_domain(cnstr_type);
+        expr result_type   = consume_type_annotations(binding_domain(cnstr_type));
         if (is_predicate && !type_checker(new_env, lctx).is_prop(result_type)) {
             throw exception(sstream() << "failed to generate projection '" << proj_name << "' for '" << n << "', "
                             << "type is an inductive predicate, but field is not a proposition");

tests/lean/autoIssue.lean

@@ -0,0 +1,15 @@
+structure A :=
+  x : Nat
+  a' : x = 1 := by trivial
+
+#check @A.a'
+
+example (z : A) : z.x = 1 := by
+  have := z.a'
+  trace_state
+  exact this
+
+example (z : A) : z.x = 1 := by
+  have := z.2
+  trace_state
+  exact this

tests/lean/autoIssue.lean.expected.out

@@ -0,0 +1,7 @@
+A.a' : ∀ (self : A), self.x = 1
+z : A
+this : z.x = 1
+⊢ z.x = 1
+z : A
+this : z.x = 1
+⊢ z.x = 1