fix: make sure the structure instance notation does not leak auxiliary type annotations (e.g., autoParam and optParam)

src/Lean/Elab/StructInst.lean

@@ -621,7 +621,7 @@ private partial def elabStruct (s : Struct) (expectedType? : Option Expr) : Term
           let field := { field with expr? := some val }
           pure (e, type, field::fields)
         match field.val with
-        | FieldVal.term stx => cont (← elabTermEnsuringType stx d) field
+        | FieldVal.term stx => cont (← elabTermEnsuringType stx d.consumeTypeAnnotations) field
         | FieldVal.nested s => do
           -- if all fields of `s` are marked as `default`, then try to synthesize instance
           match (← trySynthStructInstance? s d) with
@@ -634,7 +634,7 @@ private partial def elabStruct (s : Struct) (expectedType? : Option Expr) : Term
             | Except.error err       => throwError err
             | Except.ok tacticSyntax =>
               let stx ← `(by $tacticSyntax)
-              cont (← elabTermEnsuringType stx (d.getArg! 0)) field
+              cont (← elabTermEnsuringType stx (d.getArg! 0).consumeTypeAnnotations) field
           | _ =>
             let val ← withRef field.ref <| mkFreshExprMVar (some d)
             cont (markDefaultMissing val) field

tests/lean/autoIssue.lean

@@ -47,3 +47,26 @@ def tst : MetaM Unit :=
     IO.println (← Meta.ppExpr (← inferType e))
 
 #eval tst
+
+example (z : A) : z.x = 1 := by
+  match z with
+  | { a' := h } => trace_state; exact h
+
+example (z : A) : z.x = 1 := by
+  match z with
+  | A.mk x a' => trace_state; exact a'
+
+example : A :=
+  { x := 1, a' := _ }
+
+example : A :=
+  A.mk 1 _
+
+def f (x : Nat) (h : x = 1) : A := A.mk x h
+
+example : A :=
+  f 2 _
+
+example : A := by
+  apply f
+  done

tests/lean/autoIssue.lean.expected.out

@@ -18,3 +18,26 @@ case mk
 x y : Nat
 ⊢ { x := x, y := y } = { x := { x := x, y := y }.x, y := { x := x, y := y }.y }
 a.1 = 1
+z : A
+x✝ : Nat
+h : x✝ = 1
+⊢ (A.mk x✝).x = 1
+z : A
+x : Nat
+a' : x = 1
+⊢ (A.mk x).x = 1
+autoIssue.lean:60:18-60:19: error: don't know how to synthesize placeholder
+context:
+⊢ 1 = 1
+autoIssue.lean:63:9-63:10: error: don't know how to synthesize placeholder for argument 'a''
+context:
+⊢ 1 = 1
+autoIssue.lean:68:6-68:7: error: don't know how to synthesize placeholder for argument 'h'
+context:
+⊢ 2 = 1
+autoIssue.lean:72:2-72:6: error: unsolved goals
+case h
+⊢ ?x = 1
+
+case x
+⊢ Nat