Merge PR #10858: Implementing postponed constraints in TC resolution

Reviewed-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: ejgallego

1 files changed, 16 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/bug_9058.v b/test-suite/bugs/closed/bug_9058.v
new file mode 100644
index 0000000000..6de8324641
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9058.v
@@ -0,0 +1,16 @@
+Class A (X : Type) := {}.
+Hint Mode A ! : typeclass_instances.
+
+Class B X {aX: A X} Y := { opB: X -> Y -> Y }.
+Hint Mode B - - ! : typeclass_instances.
+
+Section Section.
+
+Context X {aX: A X} Y {bY: B X Y}.
+
+(* Set Typeclasses Debug. *)
+
+Let ok := fun (x : X) (y : Y) => opB x y.
+Let ok' := fun x (y : Y) => opB x y.
+
+End Section.