fix: check redundant sources at structure instance notation

src/Lean/Elab/StructInst.lean

@@ -197,9 +197,12 @@ private def elabModifyOp (stx modifyOp : Syntax) (sources : Array ExplicitSource
   Otherwise, we use the type of the first source. -/
 private def getStructName (stx : Syntax) (expectedType? : Option Expr) (sourceView : Source) : TermElabM Name := do
   tryPostponeIfNoneOrMVar expectedType?
-  let useSource : Unit → TermElabM Name := fun _ =>
+  let useSource : Unit → TermElabM Name := fun _ => do
     match sourceView, expectedType? with
-    | Source.explicit sources, _ => return sources[0].structName
+    | Source.explicit sources, _ =>
+      if sources.size > 1 then
+        throwErrorAt sources[1].stx "invalid \{...} notation, expected type is not known, using the type of the first source, extra sources are not needed"
+      return sources[0].structName
     | _, some expectedType => throwUnexpectedExpectedType expectedType
     | _, none              => throwUnknownExpectedType
   match expectedType? with

tests/lean/structInst1.lean

@@ -0,0 +1,36 @@
+structure A where
+  x : Nat
+  w : Nat
+
+structure B extends A where
+  y : Nat
+
+structure C extends B where
+  z : Nat
+
+def f1 (c : C) (a : A) : C :=
+  { c with toA := a, x := 0 }  -- Error, `toA` and `x` are both updates to field `x`
+
+def f2 (c : C) (a : A) : C :=
+  { c with toA := a }
+
+def f3 (c : C) (a : A) : C :=
+  { a, c with x := 0 }
+
+theorem ex1 (a : A) (c : C) : (f3 c a).x = 0 :=
+  rfl
+
+theorem ex2 (a : A) (c : C) : (f3 c a).w = a.w :=
+  rfl
+
+def f4 (c : C) (a : A) : C :=
+  { c, a with x := 0 } -- TODO: generate error that `a` was not used?
+
+theorem ex3 (a : A) (c : C) : (f4 c a).w = c.w :=
+  rfl
+
+theorem ex4 (a : A) (c : C) : (f4 c a).x = 0 :=
+  rfl
+
+def f5 (c : C) (a : A) :=
+  { c, a with x := 0 } -- Error

tests/lean/structInst1.lean.expected.out

@@ -0,0 +1,2 @@
+structInst1.lean:12:11-12:19: error: field 'toA' has already beed specified
+structInst1.lean:36:7-36:8: error: invalid {...} notation, expected type is not known, using the type of the first source, extra sources are not needed