Merge PR #10858: Implementing postponed constraints in TC resolution

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

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.