Merge branch 'tc-test-suite' of https://github.com/JasonGross/coq into JasonGross-tc

2 files changed, 43 insertions, 1 deletions

diff --git a/test-suite/bugs/opened/3325.v b/test-suite/bugs/opened/3325.v
index 4c221dc7f..b4d1a79c0 100644
--- a/test-suite/bugs/opened/3325.v
+++ b/test-suite/bugs/opened/3325.v
@@ -1,3 +1,6 @@
+Typeclasses eauto := debug.
+Set Printing All.
+
 Axiom SProp : Set.
 Axiom sp : SProp.
 
@@ -16,7 +19,6 @@ Class LogicOps F := { land: F -> F }.
 Instance : LogicOps SProp. Admitted.
 Instance : LogicOps Prop. Admitted.
 
-Set Printing All.
 Parameter (n : nat).
 (* If this is a [Definition], the resolution goes through fine. *)
 Notation vn := (@stateIs _ n).
@@ -26,3 +28,19 @@ Definition GOOD : SProp :=
 (* This doesn't resolve, if PropLogicOps is defined later than SPropLogicOps *)
 Fail Definition BAD : SProp :=
   @land _ _ vn.
+
+
+Class A T := { foo : T -> Prop }.
+Instance: A nat. Admitted.
+Instance: A Set. Admitted.
+
+Class B := { U : Type ; b : U }.
+Instance bi: B := {| U := nat ; b := 0 |}.
+
+Notation b0N := (@b _ : nat).
+Notation b0Ni := (@b bi : nat).
+Definition b0D := (@b _ : nat).
+Definition GOOD1 := (@foo _ _ b0D).
+Definition GOOD2 := (let x := b0N in @foo _ _ x).
+Definition GOOD3 := (@foo _ _ b0Ni).
+Fail Definition BAD1 := (@foo _ _ b0N). (* Error: The term "b0Ni" has type "nat" while it is expected to have type "Set". *)
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.