diff --git a/src/Lean/Elab/StructInst.lean b/src/Lean/Elab/StructInst.lean
index d5a74de568..6b5e83f2c2 100644
--- a/src/Lean/Elab/StructInst.lean
+++ b/src/Lean/Elab/StructInst.lean
@@ -851,7 +851,22 @@ private def elabStructInstAux (stx : Syntax) (expectedType? : Option Expr) (sour
   let struct ← liftMacroM <| mkStructView stx structName source
   let struct ← expandStruct struct
   trace[Elab.struct] "{struct}"
-  let (r, struct) ← elabStruct struct expectedType?
+  /- We try to synthesize pending problems with `withSynthesize` combinator before trying to use default values.
+     This is important in examples such as
+      ```
+      structure MyStruct where
+          {α : Type u}
+          {β : Type v}
+          a : α
+          b : β
+
+      #check { a := 10, b := true : MyStruct }
+      ```
+     were the `α` will remain "unknown" until the default instance for `OfNat` is used to ensure that `10` is a `Nat`.
+
+     TODO: investigate whether this design decision may have unintended side effects or produce confusing behavior.
+  -/
+  let (r, struct) ← withSynthesize (mayPostpone := true) <| elabStruct struct expectedType?
   trace[Elab.struct] "before propagate {r}"
   DefaultFields.propagate struct
   return r
diff --git a/tests/lean/run/783.lean b/tests/lean/run/783.lean
new file mode 100644
index 0000000000..3d19b69494
--- /dev/null
+++ b/tests/lean/run/783.lean
@@ -0,0 +1,7 @@
+structure MyStruct where
+    {α : Type u}
+    {β : Type v}
+    a : α
+    b : β
+
+#check { a := 10, b := true : MyStruct }