fix: circular assignment at structure instance elaborator

This PR fixes a stack overflow caused by a cyclic assignment in the
metavariable context. The cycle is unintentionally introduced by the
structure instance elaborator.

closes #3150

src/Lean/Elab/StructInst.lean

@@ -900,8 +900,16 @@ partial def tryToSynthesizeDefault (structs : Array Struct) (allStructNames : Ar
           | none   =>
             let mvarDecl ← getMVarDecl mvarId
             let val ← ensureHasType mvarDecl.type val
-            mvarId.assign val
-            return true
+            /-
+            We must use `checkedAssign` here to ensure we do not create a cyclic
+            assignment. See #3150.
+            This can happen when there are holes in the the fields the default value
+            depends on.
+            Possible improvement: create a new `_` instead of returning `false` when
+            `checkedAssign` fails. Reason: the field will not be needed after the
+            other `_` are resolved by the user.
+            -/
+            mvarId.checkedAssign val
       | _ => loop (i+1) dist
     else
       return false

tests/lean/run/3150.lean

@@ -0,0 +1,24 @@
+class One (α : Type) where
+  one : α
+
+variable (R A : Type) [One R] [One A]
+
+class OneHom where
+  toFun : R → A
+  map_one : toFun One.one = One.one
+
+structure Subone where
+  mem : R → Prop
+  one_mem : mem One.one
+
+structure Subalgebra [OneHom R A] extends Subone A : Type where
+  algebraMap_mem : ∀ r : R, mem (OneHom.toFun r)
+  one_mem := OneHom.map_one (R := R) (A := A) ▸ algebraMap_mem One.one
+
+/--
+error: fields missing: 'one_mem'
+-/
+#guard_msgs in
+example [OneHom R A] : Subalgebra R A where
+  mem := _
+  algebraMap_mem := _