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

2 files changed, 27 insertions, 2 deletions

diff --git a/doc/changelog/02-specification-language/10858-stuck-classed.md b/doc/changelog/02-specification-language/10858-stuck-classed.md
new file mode 100644
index 0000000000..c7186f2c1d
--- /dev/null
+++ b/doc/changelog/02-specification-language/10858-stuck-classed.md
@@ -0,0 +1,12 @@
+- **Changed:**
+  Typeclass resolution, accessible through :tacn:`typeclasses eauto`,
+  now suspends constraints according to their modes
+  instead of failing. If a typeclass constraint does not match
+  any of the declared modes for its class, the constraint is postponed, and
+  the proof search continues on other goals. Proof search does a fixed point
+  computation to try to solve them at a later stage of resolution. It does
+  not fail if there remain only stuck constraints at the end of resolution.
+  This makes typeclasses with declared modes more robust with respect to the
+  order of resolution.
+  (`#10858 <https://github.com/coq/coq/pull/10858>`_,
+  fixes `#9058 <https://github.com/coq/coq/issues/9058>_`, by Matthieu Sozeau).
diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index af4e9051bb..7abeca7815 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -385,8 +385,10 @@ few other commands related to typeclasses.
 .. tacn:: typeclasses eauto
    :name: typeclasses eauto
 
-   This tactic uses a different resolution engine than :tacn:`eauto` and
-   :tacn:`auto`. The main differences are the following:
+   This proof search tactic implements the resolution engine that is run
+   implicitly during type-checking. This tactic uses a different resolution
+   engine than :tacn:`eauto` and :tacn:`auto`. The main differences are the
+   following:
 
    + Contrary to :tacn:`eauto` and :tacn:`auto`, the resolution is done entirely in
      the new proof engine (as of Coq 8.6), meaning that backtracking is
@@ -422,6 +424,17 @@ few other commands related to typeclasses.
      resolution with the local hypotheses use full conversion during
      unification.
 
+   + The mode hints (see :cmd:`Hint Mode`) associated to a class are
+     taken into account by :tacn:`typeclasses eauto`. When a goal
+     does not match any of the declared modes for its head (if any),
+     instead of failing like :tacn:`eauto`, the goal is suspended and
+     resolution proceeds on the remaining goals.
+     If after one run of resolution, there remains suspended goals,
+     resolution is launched against on them, until it reaches a fixed
+     point when the set of remaining suspended goals does not change.
+     Using `solve [typeclasses eauto]` can be used to ensure that
+     no suspended goals remain.
+
    + When considering local hypotheses, we use the union of all the modes
      declared in the given databases.