Merge PR #13909: Minimize the set of multiple inheritance (coercion) paths to check for conversion

Reviewed-by: gares
Ack-by: SkySkimmer

2 files changed, 86 insertions, 36 deletions

diff --git a/test-suite/output/relaxed_ambiguous_paths.out b/test-suite/output/relaxed_ambiguous_paths.out
index 48368c7ede..6bf03d30d3 100644
--- a/test-suite/output/relaxed_ambiguous_paths.out
+++ b/test-suite/output/relaxed_ambiguous_paths.out
@@ -1,13 +1,24 @@
-File "stdin", line 10, characters 0-28:
+File "stdin", line 13, characters 0-29:
 Warning:
-New coercion path [ac; cd] : A >-> D is ambiguous with existing 
-[ab; bd] : A >-> D. [ambiguous-paths,typechecker]
-[ab] : A >-> B
-[ac] : A >-> C
-[ab; bd] : A >-> D
-[bd] : B >-> D
-[cd] : C >-> D
-File "stdin", line 26, characters 0-28:
+New coercion path [g1; f2] : A >-> B' is ambiguous with existing 
+[f1; g2] : A >-> B'. [ambiguous-paths,typechecker]
+File "stdin", line 14, characters 0-29:
+Warning:
+New coercion path [h1; f3] : B >-> C' is ambiguous with existing 
+[f2; h2] : B >-> C'. [ambiguous-paths,typechecker]
+[f1] : A >-> A'
+[g1] : A >-> B
+[f1; g2] : A >-> B'
+[g1; h1] : A >-> C
+[f1; g2; h2] : A >-> C'
+[g2] : A' >-> B'
+[g2; h2] : A' >-> C'
+[f2] : B >-> B'
+[h1] : B >-> C
+[f2; h2] : B >-> C'
+[h2] : B' >-> C'
+[f3] : C >-> C'
+File "stdin", line 33, characters 0-28:
 Warning:
 New coercion path [ab; bc] : A >-> C is ambiguous with existing 
 [ac] : A >-> C. [ambiguous-paths,typechecker]
@@ -17,6 +28,19 @@ New coercion path [ab; bc] : A >-> C is ambiguous with existing
 [bc] : B >-> C
 [bc; cd] : B >-> D
 [cd] : C >-> D
+File "stdin", line 50, characters 0-28:
+Warning:
+New coercion path [ab; bc] : A >-> C is ambiguous with existing 
+[ac] : A >-> C. [ambiguous-paths,typechecker]
+File "stdin", line 51, characters 0-28:
+Warning:
+New coercion path [ba; ab] : B >-> B is not definitionally an identity function.
+New coercion path [ab; ba] : A >-> A is not definitionally an identity function.
+[ambiguous-paths,typechecker]
+[ab] : A >-> B
+[ac] : A >-> C
+[ba] : B >-> A
+[bc] : B >-> C
 [B_A] : B >-> A
 [C_A] : C >-> A
 [D_A] : D >-> A
@@ -31,7 +55,7 @@ New coercion path [ab; bc] : A >-> C is ambiguous with existing
 [D_B; B_A'] : D >-> A'
 [D_B] : D >-> B
 [D_C] : D >-> C
-File "stdin", line 121, characters 0-86:
+File "stdin", line 147, 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]
@@ -44,15 +68,15 @@ New coercion path [D_C; C_A'] : D >-> A' is ambiguous with existing
 [D_B; B_A'] : D >-> A'
 [D_B] : D >-> B
 [D_C] : D >-> C
-File "stdin", line 130, characters 0-47:
+File "stdin", line 156, 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:
+File "stdin", line 157, 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:
+File "stdin", line 158, 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 41322045f2..182e155273 100644
--- a/test-suite/output/relaxed_ambiguous_paths.v
+++ b/test-suite/output/relaxed_ambiguous_paths.v
@@ -1,13 +1,20 @@
 Module test1.
 Section test1.
 
-Variable (A B C D : Type).
-Variable (ab : A -> B) (bd : B -> D) (ac : A -> C) (cd : C -> D).
-
-Local Coercion ab : A >-> B.
-Local Coercion bd : B >-> D.
-Local Coercion ac : A >-> C.
-Local Coercion cd : C >-> D.
+Variable (A B C A' B' C' : Type).
+Variable (f1 : A -> A') (f2 : B -> B') (f3 : C -> C').
+Variable (g1 : A -> B) (g2 : A' -> B') (h1 : B -> C) (h2 : B' -> C').
+
+Local Coercion g1 : A >-> B.
+Local Coercion g2 : A' >-> B'.
+Local Coercion h1 : B >-> C.
+Local Coercion h2 : B' >-> C'.
+Local Coercion f1 : A >-> A'.
+Local Coercion f2 : B >-> B'.
+Local Coercion f3 : C >-> C'.
+(* [g1; h1; f3], [f1; g2; h2] : A >-> C' should not be reported as ambiguous  *)
+(* paths because they are redundant with `[g1; f2], [f1; g2] : A >-> B'` and  *)
+(* `[h1; f3], [f2; h2] : B >-> C'`.                                           *)
 
 Print Graph.
 
@@ -24,8 +31,8 @@ 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`.           *)
+(* `[ab; bc; cd], [ac; cd] : A >-> D` should not be reported as ambiguous     *)
+(* paths because they are redundant with `[ab; bc], [ac] : A >-> C`.          *)
 
 Print Graph.
 
@@ -34,6 +41,25 @@ End test2.
 
 Module test3.
 Section test3.
+
+Variable (A B C : Type).
+Variable (ab : A -> B) (ba : B -> A) (ac : A -> C) (bc : B -> C).
+
+Local Coercion ac : A >-> C.
+Local Coercion bc : B >-> C.
+Local Coercion ab : A >-> B.
+Local Coercion ba : B >-> A.
+(* `[ba; ac], [bc] : B >-> C` should not be reported as ambiguous paths       *)
+(* because they are redundant with `[ab; bc], [ac] : A >-> C` and             *)
+(* `[ba; ab] : B >-> B`.                                                      *)
+
+Print Graph.
+
+End test3.
+End test3.
+
+Module test4.
+Section test4.
 Variable (A : Type) (P Q : A -> Prop).
 
 Record B := {
@@ -57,11 +83,11 @@ Local Coercion D_C (d : D) : C := Build_C (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).
 
@@ -89,11 +115,11 @@ Local Coercion D_C (d : D) : C true := Build_C true (D_A d) (D_Q d).
 
 Print Graph.
 
-End test4.
-End test4.
+End test5.
+End test5.
 
-Module test5.
-Section test5.
+Module test6.
+Section test6.
 
 Variable (A : Type) (P Q : A -> Prop).
 
@@ -123,18 +149,18 @@ Local Coercion D_C (d : D) : C true :=
 
 Print Graph.
 
-End test5.
-End test5.
+End test6.
+End test6.
 
-Module test6.
+Module test7.
 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.
+End test7.
 
-Module test7.
+Module test8.
 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.
+End test8.