diff --git a/tests/lean/run/structure_recursive.lean b/tests/lean/run/structure_recursive.lean
index 5e7b48d79ce3..97572f0b4d80 100644
--- a/tests/lean/run/structure_recursive.lean
+++ b/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.
 -/