From ae03f15c92fed5ce240a018a49fbc374f8eaeeb0 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 10 Aug 2021 19:00:34 -0700
Subject: [PATCH] test: default value set at copied structure

---
 src/Lean/Elab/Structure.lean |  2 +-
 tests/lean/run/diamond4.lean | 14 ++++++++++++++
 2 files changed, 15 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/diamond4.lean

diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean
index f030e2892d..8439a49b79 100644
--- a/src/Lean/Elab/Structure.lean
+++ b/src/Lean/Elab/Structure.lean
@@ -380,7 +380,7 @@ where
           let existingFieldType ← inferType existingFieldInfo.fvar
           unless (← isDefEq fieldType existingFieldType) do
             throwError "parent field type mismatch, field '{fieldName}' from parent '{parentStructName}' {← mkHasTypeButIsExpectedMsg fieldType existingFieldType}"
-          -- TODO: if new field has a default value, it should probably override the default at `infos` (if it has one)
+          /- Remark: if structure has a default value for this field, it will be set at the `processOveriddenDefaultValues` below. -/
           copy (i+1) (fieldMap.insert fieldName existingFieldInfo.fvar) infos
         | none =>
           let some fieldInfo ← getFieldInfo? (← getEnv) parentStructName fieldName | unreachable!
diff --git a/tests/lean/run/diamond4.lean b/tests/lean/run/diamond4.lean
new file mode 100644
index 0000000000..d8b738d960
--- /dev/null
+++ b/tests/lean/run/diamond4.lean
@@ -0,0 +1,14 @@
+structure A where
+  a : Nat
+
+structure B where
+  a : Nat := 1
+  b : Nat
+
+structure C extends A, B
+
+def f (b : Nat) : C :=
+  { b }
+
+theorem ex (b : Nat) : (f b).a = 1 :=
+  rfl