chore: add test for recursive structures (#6173)

Closes #6140. This was fixed by #6125.

tests/lean/run/structure_recursive.lean

@@ -108,6 +108,18 @@ structure A5 extends A4 Nat Bool where
   x := 0
   y := true
 
+/-!
+Default value whose type depends on the recursive structure.
+Reported in https://github.com/leanprover/lean4/issues/6140
+-/
+
+structure RecS where
+  n : Nat
+  recS : Option RecS := none
+
+/-- info: { n := 0, recS := none } : RecS -/
+#guard_msgs in #check ({ n := 0 } : RecS)
+
 /-!
 Incidental new feature: checking projections when the structure is Prop.
 -/