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, 64 insertions, 11 deletions

diff --git a/test-suite/output/relaxed_ambiguous_paths.out b/test-suite/output/relaxed_ambiguous_paths.out
index dc793598a9..ac5a09bad7 100644
--- a/test-suite/output/relaxed_ambiguous_paths.out
+++ b/test-suite/output/relaxed_ambiguous_paths.out
@@ -7,6 +7,16 @@ New coercion path [ac; cd] : A >-> D is ambiguous with existing
 [ac] : A >-> C
 [bd] : B >-> D
 [cd] : C >-> D
+File "stdin", line 26, characters 0-28:
+Warning:
+New coercion path [ab; bc] : A >-> C is ambiguous with existing 
+[ac] : A >-> C. [ambiguous-paths,typechecker]
+[ac] : A >-> C
+[ac; cd] : A >-> D
+[ab] : A >-> B
+[cd] : C >-> D
+[bc] : B >-> C
+[bc; cd] : B >-> D
 [B_A] : B >-> A
 [C_A] : C >-> A
 [D_B] : D >-> B
@@ -21,7 +31,7 @@ New coercion path [ac; cd] : A >-> D is ambiguous with existing
 [D_A] : D >-> A
 [D_B] : D >-> B
 [D_C] : D >-> C
-File "stdin", line 103, characters 0-86:
+File "stdin", line 121, characters 0-86:
 Warning:
 New coercion path [D_C; C_A'] : D >-> A' is ambiguous with existing 
 [D_B; B_A'] : D >-> A'. [ambiguous-paths,typechecker]
@@ -34,3 +44,15 @@ New coercion path [D_C; C_A'] : D >-> A' is ambiguous with existing
 [D_A] : D >-> A
 [D_B] : D >-> B
 [D_C] : D >-> C
+File "stdin", line 130, characters 0-47:
+Warning:
+New coercion path [unwrap_nat; wrap_nat] : NAT >-> NAT is not definitionally an identity function.
+[ambiguous-paths,typechecker]
+File "stdin", line 131, characters 0-64:
+Warning:
+New coercion path [unwrap_list; wrap_list] : LIST >-> LIST is not definitionally an identity function.
+[ambiguous-paths,typechecker]
+File "stdin", line 132, characters 0-51:
+Warning:
+New coercion path [unwrap_Type; wrap_Type] : TYPE >-> TYPE is not definitionally an identity function.
+[ambiguous-paths,typechecker]
diff --git a/test-suite/output/relaxed_ambiguous_paths.v b/test-suite/output/relaxed_ambiguous_paths.v
index a4af27539c..41322045f2 100644
--- a/test-suite/output/relaxed_ambiguous_paths.v
+++ b/test-suite/output/relaxed_ambiguous_paths.v
@@ -16,6 +16,24 @@ End test1.
 
 Module test2.
 Section test2.
+
+Variable (A B C D : Type).
+Variable (ab : A -> B) (bc : B -> C) (ac : A -> C) (cd : C -> D).
+
+Local Coercion ac : A >-> C.
+Local Coercion cd : C >-> D.
+Local Coercion ab : A >-> B.
+Local Coercion bc : B >-> C.
+(* `[ab; bc; cd], [ac; cd] : A >-> D` should not be shown as ambiguous paths  *)
+(* here because they are redundant with `[ab; bc], [ac] : A >-> C`.           *)
+
+Print Graph.
+
+End test2.
+End test2.
+
+Module test3.
+Section test3.
 Variable (A : Type) (P Q : A -> Prop).
 
 Record B := {
@@ -39,11 +57,11 @@ Local Coercion D_C (d : D) : C := Build_C (D_A d) (D_Q d).
 
 Print Graph.
 
-End test2.
-End test2.
+End test3.
+End test3.
 
-Module test3.
-Section test3.
+Module test4.
+Section test4.
 
 Variable (A : Type) (P Q : A -> Prop).
 
@@ -71,11 +89,11 @@ Local Coercion D_C (d : D) : C true := Build_C true (D_A d) (D_Q d).
 
 Print Graph.
 
-End test3.
-End test3.
+End test4.
+End test4.
 
-Module test4.
-Section test4.
+Module test5.
+Section test5.
 
 Variable (A : Type) (P Q : A -> Prop).
 
@@ -105,5 +123,18 @@ Local Coercion D_C (d : D) : C true :=
 
 Print Graph.
 
-End test4.
-End test4.
+End test5.
+End test5.
+
+Module test6.
+Record > NAT := wrap_nat { unwrap_nat :> nat }.
+Record > LIST (T : Type) := wrap_list { unwrap_list :> list T }.
+Record > TYPE := wrap_Type { unwrap_Type :> Type }.
+End test6.
+
+Module test7.
+Set Primitive Projections.
+Record > NAT_prim := wrap_nat { unwrap_nat :> nat }.
+Record > LIST_prim (T : Type) := wrap_list { unwrap_list :> list T }.
+Record > TYPE_prim := wrap_Type { unwrap_Type :> Type }.
+End test7.