1 files changed, 24 insertions, 0 deletions
diff --git a/test-suite/bugs/opened/3397.v b/test-suite/bugs/opened/3397.v
new file mode 100644
index 000000000..f5d406d3a
--- /dev/null
+++ b/test-suite/bugs/opened/3397.v
@@ -0,0 +1,24 @@
+Set Printing All.
+Typeclasses eauto := debug.
+Module success.
+  Class foo := { F : nat }.
+  Class bar := { B : nat }.
+  Instance: foo := { F := 1 }.
+  Instance: foo := { F := 0 }.
+  Instance: bar := { B := 0 }.
+  Definition BAZ := eq_refl : @F _ = @B _.
+End success.
+
+Module failure.
+  Class foo := { F : nat }.
+  Class bar := { B : nat }.
+  Instance f0: foo := { F := 0 }.
+  Instance f1: foo := { F := 1 }.
+  Instance b0: bar := { B := 0 }.
+  Fail Definition BAZ := eq_refl : @F _ = @B _.
+  (* Toplevel input, characters 18-25:
+Error:
+The term "@eq_refl nat (@F f1)" has type "@eq nat (@F f1) (@F f1)"
+while it is expected to have type "@eq nat (@F f1) (@B b0)"
+(cannot unify "@F f1" and "@B b0"). *)
+End failure.