Coherence checking for coercions

This change improves the relaxed ambiguous path condition of coercions (#9743)
to check that any circular inheritance path of `C >-> C` is definitionally equal
to the identity function of the class `C`. Moreover, for a new inheritance path
`p : C >-> D` and existing (valid) one `q : C >-> D`, the new mechanism does not
report the ambiguity of `p` and `q` if they have a common element, that is to
say:
`p = p1 @ [c] @ p2` and `q = q1 @ [c] @ q2`
  for some coercion `c` and inheritance paths `p1`, `p2`, `q1`, and `q2`.
In that case, convertibility of `p1` and `q1`, also, `p2` and `q2` should be
checked; thus, checking the ambiguity of `p` and `q` is redundant with them.

If the new mechanism does not report any ambiguous path, the inheritance graph
must be coherent [Barthe 1995, Sect. 3.2] [Saïbi 1997, Sect. 7]:
1. for any circular path `p : C >-> C`, `p` is definitionally equal to the
   identity function, and
2. for any two paths `p, q : C >-> D`, `p` and `q` are convertible.

[Barthe 1995] Gilles Barthe, Implicit coercions in type systems, In: TYPES '95,
              LNCS, vol 1158, Springer, 1996, pp 1-15.
[Saïbi 1997]  Amokrane Saïbi, Typing algorithm in type theory with inheritance,
              In: POPL '97, ACM, 1997, pp 292-301.

2 files changed, 16 insertions, 0 deletions

diff --git a/doc/changelog/07-commands-and-options/11258-coherence.rst b/doc/changelog/07-commands-and-options/11258-coherence.rst
new file mode 100644
index 0000000000..f04a120417
--- /dev/null
+++ b/doc/changelog/07-commands-and-options/11258-coherence.rst
@@ -0,0 +1,10 @@
+- **Changed:**
+  The :cmd:`Coercion` command has been improved to check the coherence of the
+  inheritance graph. It checks whether a circular inheritance path of `C >-> C`
+  is convertible with the identity function or not, then report it as an
+  ambiguous path if it is not.  The new mechanism does not report ambiguous
+  paths that are redundant with others. For example, checking the ambiguity of
+  `[f; g]` and `[f'; g]` is redundant with that of `[f]` and `[f']` thus will
+  not be reported
+  (`#11258 <https://github.com/coq/coq/pull/11258>`_,
+  by Kazuhiko Sakaguchi).
diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst
index c3b197288f..19b33f0d90 100644
--- a/doc/sphinx/addendum/implicit-coercions.rst
+++ b/doc/sphinx/addendum/implicit-coercions.rst
@@ -165,6 +165,12 @@ Declaring Coercions
      convertible with existing ones when they have coercions that don't satisfy
      the uniform inheritance condition.
 
+  .. warn:: ... is not definitionally an identity function.
+
+     If a coercion path has the same source and target class, that is said to be
+     circular. When a new circular coercion path is not convertible with the
+     identity function, it will be reported as ambiguous.
+
   .. cmdv:: Local Coercion @qualid : @class >-> @class
 
      Declares the construction denoted by :token:`qualid` as a coercion local to