Implementing postponed constraints in TC resolution

A constraint can be stuck if it does not match any of the declared modes
for its head (if there are any). In that case, the subgoal is postponed
and the next ones are tried. We do a fixed point computation until there
are no stuck subgoals or the set does not change (it is impossible to
make it grow, as asserted in the code, because it is always a subset of
the initial goals)

This allows constraints on classes with modes to be treated as if they were
in any order (yay for stability of solutions!). Also, ultimately it should
free us to launch resolutions more agressively (avoiding issues like the
ones seen in PR #10762).

Add more examples of the semantics of TC resolution with apply in test-suite

Properly catch ModeMatchFailure on calls to map_e*

Add fixed bug 9058 to the test-suite

Close #9058

Add documentation

Fixes after Gaëtan's review.

Main change is to not use exceptions for control-flow

Update tactics/class_tactics.ml

Clearer and more efficient mode mismatch dispatch

Co-Authored-By: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>

Remove exninfo argument

3 files changed, 97 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.
diff --git a/test-suite/success/HintMode.v b/test-suite/success/HintMode.v
new file mode 100644
index 0000000000..decddb73d1
--- /dev/null
+++ b/test-suite/success/HintMode.v
@@ -0,0 +1,20 @@
+Module Postponing.
+
+Class In A T := { IsIn : A -> T -> Prop }.
+Class Empty T := { empty : T }.
+Class EmptyIn (A T : Type) `{In A T} `{Empty T} :=
+ { isempty : forall x, IsIn x empty -> False }.
+
+Hint Mode EmptyIn ! ! - - : typeclass_instances.
+Hint Mode Empty ! : typeclass_instances.
+Hint Mode In ! - : typeclass_instances.
+Existing Class IsIn.
+Goal forall A T `{In A T} `{Empty T} `{EmptyIn A T}, forall x : A, IsIn x empty -> False.
+ Proof.
+   intros.
+   eapply @isempty. (* Second goal needs to be solved first, to un-stuck the first one
+   (hence the Existing Class IsIn to allow finding the assumption of IsIn here)  *)
+   all:typeclasses eauto.
+Qed.
+
+End Postponing.
diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v
index 3f96bf2c35..66305dfefa 100644
--- a/test-suite/success/Typeclasses.v
+++ b/test-suite/success/Typeclasses.v
@@ -1,3 +1,64 @@
+Module applydestruct.
+  Class Foo (A : Type) :=
+    { bar : nat -> A;
+      baz  : A -> nat }.
+  Hint Mode Foo + : typeclass_instances.
+
+  Class C (A : Type).
+  Hint Mode C + : typeclass_instances.
+
+  Variable fool : forall {A} {F : Foo A} (x : A), C A -> bar 0 = x.
+  (* apply leaves non-dependent subgoals of typeclass type
+     alone *)
+  Goal forall {A} {F : Foo A} (x : A), bar 0 = x.
+  Proof.
+    intros. apply fool.
+    match goal with
+      |[ |- C A ] => idtac
+    end.
+  Abort.
+
+  Variable fooli : forall {A} {F : Foo A} {c : C A} (x : A), bar 0 = x.
+  (* apply tries to resolve implicit argument typeclass
+     constraints. *)
+  Goal forall {A} {F : Foo A} (x : A), bar 0 = x.
+  Proof.
+    intros.
+    Fail apply fooli.
+    Fail unshelve eapply fooli; solve [typeclasses eauto].
+    eapply fooli.
+  Abort.
+
+  (* It applies resolution after unification of the goal *)
+  Goal forall {A} {F : Foo A} {C : C A} (x : A), bar 0 = x.
+  Proof.
+    intros. apply fooli.
+  Abort.
+    Set Typeclasses Debug Verbosity 2.
+
+  Inductive bazdestr {A} (F : Foo A) : nat -> Prop :=
+    | isbas : bazdestr F 1.
+
+  Variable fooinv : forall {A} {F : Foo A} (x : A),
+      bazdestr F (baz x).
+
+  (* Destruct applies resolution early, before finding
+     occurrences to abstract. *)
+  Goal forall {A} {F : Foo A} {C : C A} (x : A), baz x = 0.
+  Proof.
+    intros. Fail destruct (fooinv _).
+    destruct (fooinv x).
+  Abort.
+
+  Goal forall {A} {F : Foo A} (x y : A), x = y.
+  Proof.
+    intros. rewrite <- (fool x). rewrite <- (fool y). reflexivity.
+    match goal with
+      |[ |- C A ] => idtac
+    end.
+  Abort.
+End applydestruct.
+
 Module onlyclasses.
 
 (* In 8.6 we still allow non-class subgoals *)