From efc89eb4e1ed15d67b7e193daf1afbe05b480c89 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 10 Mar 2022 08:14:30 -0800
Subject: [PATCH] fix: make sure `inferProjType` consume auxiliary type
 annotations

---
 src/Lean/Meta/InferType.lean           |  2 +-
 tests/lean/autoIssue.lean              | 11 +++++++++++
 tests/lean/autoIssue.lean.expected.out |  1 +
 3 files changed, 13 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Meta/InferType.lean b/src/Lean/Meta/InferType.lean
index c45d4c352e..4e3065e44b 100644
--- a/src/Lean/Meta/InferType.lean
+++ b/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 α :=
diff --git a/tests/lean/autoIssue.lean b/tests/lean/autoIssue.lean
index 53daeea73a..7356995095 100644
--- a/tests/lean/autoIssue.lean
+++ b/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
diff --git a/tests/lean/autoIssue.lean.expected.out b/tests/lean/autoIssue.lean.expected.out
index aedf0503e8..670ba41a24 100644
--- a/tests/lean/autoIssue.lean.expected.out
+++ b/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