Merge PR #11258: Coherence checking for coercions

Reviewed-by: gares

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.