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

Reviewed-by: gares
Ack-by: SkySkimmer

6 files changed, 174 insertions, 81 deletions

diff --git a/doc/changelog/07-vernac-commands-and-options/13909-reduce-ambiguous-paths.rst b/doc/changelog/07-vernac-commands-and-options/13909-reduce-ambiguous-paths.rst
new file mode 100644
index 0000000000..c5a2172005
--- /dev/null
+++ b/doc/changelog/07-vernac-commands-and-options/13909-reduce-ambiguous-paths.rst
@@ -0,0 +1,6 @@
+- **Changed:**
+  Improve the :cmd:`Coercion` command to reduce the number of ambiguous paths to
+  report. A pair of multiple inheritance paths that can be reduced to smaller
+  adjoining pairs will not be reported as ambiguous paths anymore.
+  (`#13909 <https://github.com/coq/coq/pull/13909>`_,
+  by Kazuhiko Sakaguchi).
diff --git a/pretyping/coercionops.ml b/pretyping/coercionops.ml
index 274dbfd7ed..9b25d63640 100644
--- a/pretyping/coercionops.ml
+++ b/pretyping/coercionops.ml
@@ -30,10 +30,6 @@ type cl_typ =
   | CL_IND of inductive
   | CL_PROJ of Projection.Repr.t
 
-type cl_info_typ = {
-  cl_param : int
-}
-
 let cl_typ_ord t1 t2 = match t1, t2 with
   | CL_SECVAR v1, CL_SECVAR v2 -> Id.compare v1 v2
   | CL_CONST c1, CL_CONST c2 -> Constant.CanOrd.compare c1 c2
@@ -56,9 +52,21 @@ struct
     if Int.equal c 0 then cl_typ_ord j1 j2 else c
 end
 
+module ClTypSet = Set.Make(ClTyp)
 module ClTypMap = Map.Make(ClTyp)
 module ClPairMap = Map.Make(ClPairOrd)
 
+type cl_info_typ = {
+  (* The number of parameters of the coercion class. *)
+  cl_param : int;
+  (* The sets of coercion classes respectively reachable from and to the
+     coercion class. *)
+  cl_reachable_from : ClTypSet.t;
+  cl_reachable_to : ClTypSet.t;
+  (* The representative class of the strongly connected component. *)
+  cl_repr : cl_typ;
+}
+
 type coe_typ = GlobRef.t
 
 module CoeTypMap = GlobRef.Map_env
@@ -73,18 +81,18 @@ type coe_info_typ = {
   coe_param : int;
 }
 
-let coe_info_typ_equal c1 c2 =
-  GlobRef.equal c1.coe_value c2.coe_value &&
-    c1.coe_local == c2.coe_local &&
-    c1.coe_is_identity == c2.coe_is_identity &&
-    c1.coe_is_projection == c2.coe_is_projection &&
-    Int.equal c1.coe_param c2.coe_param
-
 type inheritance_path = coe_info_typ list
 
 let init_class_tab =
   let open ClTypMap in
-  add CL_FUN { cl_param = 0 } (add CL_SORT { cl_param = 0 } empty)
+  let cl_info params cl =
+    let cl_singleton = ClTypSet.singleton cl in
+    { cl_param = params;
+      cl_reachable_from = cl_singleton;
+      cl_reachable_to = cl_singleton;
+      cl_repr = cl }
+  in
+  add CL_FUN (cl_info 0 CL_FUN) (add CL_SORT (cl_info 0 CL_SORT) empty)
 
 let class_tab =
   Summary.ref ~name:"class_tab" (init_class_tab : cl_info_typ ClTypMap.t)
@@ -98,8 +106,7 @@ let inheritance_graph =
 (* ajout de nouveaux "objets" *)
 
 let add_new_class cl s =
-  if not (ClTypMap.mem cl !class_tab) then
-    class_tab := ClTypMap.add cl s !class_tab
+  class_tab := ClTypMap.add cl s !class_tab
 
 let add_new_coercion coe s =
   coercion_tab := CoeTypMap.add coe s !coercion_tab
@@ -111,6 +118,8 @@ let add_new_path x y =
 
 let class_info cl = ClTypMap.find cl !class_tab
 
+let class_nparams cl = (class_info cl).cl_param
+
 let class_exists cl = ClTypMap.mem cl !class_tab
 
 let coercion_info coe = CoeTypMap.find coe !coercion_tab
@@ -283,54 +292,80 @@ let different_class_params env ci =
     | _ -> false
 
 let add_coercion_in_graph env sigma ic =
+  let source = ic.coe_source in
+  let target = ic.coe_target in
+  let source_info = class_info source in
+  let target_info = class_info target in
   let old_inheritance_graph = !inheritance_graph in
   let ambig_paths :
     ((cl_typ * cl_typ) * inheritance_path * inheritance_path) list ref =
     ref [] in
+  let check_coherence (i, j as ij) p q =
+    let i_info = class_info i in
+    let j_info = class_info j in
+    let between_ij = ClTypSet.inter i_info.cl_reachable_from j_info.cl_reachable_to in
+    if cl_typ_eq i_info.cl_repr i &&
+       cl_typ_eq j_info.cl_repr j &&
+       ClTypSet.is_empty
+         (ClTypSet.diff (ClTypSet.inter between_ij source_info.cl_reachable_to)
+            i_info.cl_reachable_to) &&
+       ClTypSet.is_empty
+         (ClTypSet.diff
+            (ClTypSet.inter between_ij target_info.cl_reachable_from)
+            j_info.cl_reachable_from) &&
+       not (compare_path env sigma i p q)
+    then
+      ambig_paths := (ij, p, q) :: !ambig_paths
+  in
   let try_add_new_path (i,j as ij) p =
-    (* If p is a cycle, we check whether p is definitionally an identity
-       function or not. If it is not, we report p as an ambiguous inheritance
-       path. *)
-    if cl_typ_eq i j && not (compare_path env sigma i p []) then
-      ambig_paths := (ij,p,[])::!ambig_paths;
+    if cl_typ_eq i j then check_coherence ij p [];
     if not (cl_typ_eq i j) || different_class_params env i then
       match lookup_path_between_class ij with
-      | q ->
-        (* p has the same source and target classes as an existing path q. We
-           report them as ambiguous inheritance paths if
-           1. p and q have no common element, and
-           2. p and q are not convertible.
-           If 1 does not hold, say p = p1 @ [c] @ p2 and q = q1 @ [c] @ q2,
-           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 not (List.exists (fun c -> List.exists (coe_info_typ_equal c) q) p ||
-                compare_path env sigma i p q) then
-          ambig_paths := (ij,p,q)::!ambig_paths;
-        false
-      | exception Not_found -> (add_new_path ij p; true)
+      | q -> (if not (cl_typ_eq i j) then check_coherence ij p q); false
+      | exception Not_found -> add_new_path ij p; true
     else
       false
   in
   let try_add_new_path1 ij p =
     let _ = try_add_new_path ij p in ()
   in
-  if try_add_new_path (ic.coe_source, ic.coe_target) [ic] then begin
+  if try_add_new_path (source, target) [ic] then begin
     ClPairMap.iter
       (fun (s,t) p ->
          if not (cl_typ_eq s t) then begin
-           if cl_typ_eq t ic.coe_source then begin
-             try_add_new_path1 (s, ic.coe_target) (p@[ic]);
+           if cl_typ_eq t source then begin
+             try_add_new_path1 (s, target) (p@[ic]);
              ClPairMap.iter
                (fun (u,v) q ->
-                  if not (cl_typ_eq u v) && cl_typ_eq u ic.coe_target then
+                  if not (cl_typ_eq u v) && cl_typ_eq u target then
                     try_add_new_path1 (s,v) (p@[ic]@q))
                old_inheritance_graph
            end;
-           if cl_typ_eq s ic.coe_target then
-             try_add_new_path1 (ic.coe_source, t) (ic::p)
+           if cl_typ_eq s target then try_add_new_path1 (source, t) (ic::p)
          end)
       old_inheritance_graph
   end;
+  class_tab := ClTypMap.mapi (fun k k_info ->
+      let reachable_k_source = ClTypSet.mem k source_info.cl_reachable_to in
+      let reachable_target_k = ClTypSet.mem k target_info.cl_reachable_from in
+      { k_info with
+        cl_reachable_from =
+          if reachable_k_source then
+            ClTypSet.union
+              k_info.cl_reachable_from target_info.cl_reachable_from
+          else
+            k_info.cl_reachable_from;
+        cl_reachable_to =
+          if reachable_target_k then
+            ClTypSet.union k_info.cl_reachable_to source_info.cl_reachable_to
+          else
+            k_info.cl_reachable_to;
+        cl_repr =
+          if reachable_k_source && reachable_target_k then
+            target_info.cl_repr
+          else
+            k_info.cl_repr
+      }) !class_tab;
   match !ambig_paths with [] -> () | _ -> warn_ambiguous_path !ambig_paths
 
 let subst_coercion subst c =
@@ -365,7 +400,13 @@ let class_params env sigma = function
 (* add_class : cl_typ -> locality_flag option -> bool -> unit *)
 
 let add_class env sigma cl =
-  add_new_class cl { cl_param = class_params env sigma cl }
+  if not (class_exists cl) then
+    let cl_singleton = ClTypSet.singleton cl in
+    add_new_class cl {
+      cl_param = class_params env sigma cl;
+      cl_reachable_from = cl_singleton;
+      cl_reachable_to = cl_singleton;
+      cl_repr = cl }
 
 let declare_coercion env sigma c =
   let () = add_class env sigma c.coe_source in
diff --git a/pretyping/coercionops.mli b/pretyping/coercionops.mli
index fb5621dd3a..af91dd1d0e 100644
--- a/pretyping/coercionops.mli
+++ b/pretyping/coercionops.mli
@@ -31,10 +31,6 @@ val subst_cl_typ : env -> substitution -> cl_typ -> cl_typ
 (** Comparison of [cl_typ] *)
 val cl_typ_ord : cl_typ -> cl_typ -> int
 
-(** This is the type of infos for declared classes *)
-type cl_info_typ = {
-  cl_param : int }
-
 (** This is the type of coercion kinds *)
 type coe_typ = GlobRef.t
 
@@ -57,7 +53,7 @@ type inheritance_path = coe_info_typ list
 val class_exists : cl_typ -> bool
 
 (** @raise Not_found if this type is not a class *)
-val class_info : cl_typ -> cl_info_typ
+val class_nparams : cl_typ -> int
 
 (** [find_class_type env sigma c] returns the head reference of [c],
     its universe instance and its arguments *)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 800096f2b3..de1af62043 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -1419,7 +1419,7 @@ let path_convertible env sigma cl p q =
           p'
     | [] ->
       (* identity function for the class [i]. *)
-      let params = (class_info cl).cl_param in
+      let params = class_nparams cl in
       let clty =
         match cl with
         | CL_SORT -> mkGSort (Glob_term.UAnonymous {rigid=false})
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.