fix: make sure inferProjType consume auxiliary type annotations

src/Lean/Meta/InferType.lean

@@ -116,7 +116,7 @@ private def inferProjType (structName : Name) (idx : Nat) (e : Expr) : MetaM Exp
         | _ => failed ()
       ctorType ← whnf ctorType
       match ctorType with
-      | Expr.forallE _ d _ _ => return d
+      | Expr.forallE _ d _ _ => return d.consumeTypeAnnotations
       | _                    => failed ()
 
 def throwTypeExcepted {α} (type : Expr) : MetaM α :=

tests/lean/autoIssue.lean

@@ -1,3 +1,4 @@
+import Lean
 structure A :=
   x : Nat
   a' : x = 1 := by trivial
@@ -36,3 +37,13 @@ structure B :=
 example (b : B) : b = { x := b.x, y := b.y } := by
   cases b with
   | mk x y => trace_state; rfl
+
+open Lean
+open Lean.Meta
+
+def tst : MetaM Unit :=
+  withLocalDeclD `a (mkConst ``A) fun a => do
+    let e := mkProj ``A 1 a
+    IO.println (← Meta.ppExpr (← inferType e))
+
+#eval tst

tests/lean/autoIssue.lean.expected.out

@@ -17,3 +17,4 @@ a' : x = 1
 case mk
 x y : Nat
 ⊢ { x := x, y := y } = { x := { x := x, y := y }.x, y := { x := x, y := y }.y }
+a.1 = 1