From d03fa17c49525db9d96715fc3495ced52d6d0262 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 10 Aug 2021 09:19:27 -0700
Subject: [PATCH] test: `copyNewFieldsFrom`

---
 tests/lean/diamond6.lean              | 16 ++++++++++++++++
 tests/lean/diamond6.lean.expected.out | 26 ++++++++++++++++++++++++++
 2 files changed, 42 insertions(+)

diff --git a/tests/lean/diamond6.lean b/tests/lean/diamond6.lean
index 8e6034f5fe..27b9786096 100644
--- a/tests/lean/diamond6.lean
+++ b/tests/lean/diamond6.lean
@@ -17,3 +17,19 @@ set_option pp.all true
 #check @FooAC.mk
 
 #print FooAC.toFooAssoc
+
+class FooAssoc' (α : Type) extends FooAssoc α where
+  one : α
+
+class FooAC' (α : Type) extends FooComm α, FooAssoc' α where
+  mul_comm (a b : α) : a * b = b * a
+
+#check @FooAC'.mk
+
+#print FooAC'.toFooAssoc'
+
+def f [FooAssoc α] (a : α) : α :=
+  a * a
+
+def g [FooAC' α] (a : α) : α :=
+  f (a + FooAssoc'.one)
diff --git a/tests/lean/diamond6.lean.expected.out b/tests/lean/diamond6.lean.expected.out
index 37b234edc5..e321ad64a2 100644
--- a/tests/lean/diamond6.lean.expected.out
+++ b/tests/lean/diamond6.lean.expected.out
@@ -21,3 +21,29 @@ def FooAC.toFooAssoc : {α : Type} → [self : FooAC α] → FooAssoc α :=
 fun (α : Type) [self : FooAC α] =>
   @FooAssoc.mk α (@FooComm.toFoo α (@FooAC.toFooComm α self)) (@FooAC.toMul α self) (@FooAC.add_assoc α self)
     (@FooAC.mul_assoc α self)
+@FooAC'.mk : {α : Type} →
+  [toFooComm : FooComm α] →
+    [toMul : Mul.{0} α] →
+      (∀ (a b c : α),
+          @Eq.{1} α
+            (@HAdd.hAdd.{0, 0, 0} α α α (@instHAdd.{0} α (@Foo.toAdd α (@FooComm.toFoo α toFooComm)))
+              (@HAdd.hAdd.{0, 0, 0} α α α (@instHAdd.{0} α (@Foo.toAdd α (@FooComm.toFoo α toFooComm))) a b) c)
+            (@HAdd.hAdd.{0, 0, 0} α α α (@instHAdd.{0} α (@Foo.toAdd α (@FooComm.toFoo α toFooComm))) a
+              (@HAdd.hAdd.{0, 0, 0} α α α (@instHAdd.{0} α (@Foo.toAdd α (@FooComm.toFoo α toFooComm))) b c))) →
+        (∀ (a b c : α),
+            @Eq.{1} α
+              (@HMul.hMul.{0, 0, 0} α α α (@instHMul.{0} α toMul)
+                (@HMul.hMul.{0, 0, 0} α α α (@instHMul.{0} α toMul) a b) c)
+              (@HMul.hMul.{0, 0, 0} α α α (@instHMul.{0} α toMul) a
+                (@HMul.hMul.{0, 0, 0} α α α (@instHMul.{0} α toMul) b c))) →
+          α →
+            (∀ (a b : α),
+                @Eq.{1} α (@HMul.hMul.{0, 0, 0} α α α (@instHMul.{0} α toMul) a b)
+                  (@HMul.hMul.{0, 0, 0} α α α (@instHMul.{0} α toMul) b a)) →
+              FooAC' α
+def FooAC'.toFooAssoc' : {α : Type} → [self : FooAC' α] → FooAssoc' α :=
+fun (α : Type) [self : FooAC' α] =>
+  @FooAssoc'.mk α
+    (@FooAssoc.mk α (@FooComm.toFoo α (@FooAC'.toFooComm α self)) (@FooAC'.toMul α self) (@FooAC'.add_assoc α self)
+      (@FooAC'.mul_assoc α self))
+    (@FooAC'.one α self)