Minimize the set of multiple inheritance paths to check for conversion

The table of coercion classes (`class_tab`) has been extended with information
about reachability. The conversion checking of a pair of multiple inheritance
paths (of coercions) will be skipped if these paths can be reduced to smaller
adjoining pairs of multiple inheritance paths, and this reduction will be
determined based on that reachability information.

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.