Relax the ambiguous path condition of coercion

The `Coercion` command did report many ambiguous paths when one declared
multiple inheritances.  This change makes the `Coercion` command to do not
report them when
1. all the coercion in the potentially ambiguous paths respect the uniform
   inheritance condition and
2. functional compositions of the potentially ambiguous paths are convertible to
   each other.
The first condition is not explicitly checked but is used to make the checking
process of the second condition easy.

The key idea of this change:
Let us consider a sequence of coercion
f_1 : C_1 >-> C_2, f_2 : C_2 >-> C_3, ..., f_n : C_n >-> C_(n+1)
which respect the uniform inheritance condition and where the user-defined
classes C_i have m_i parameters respectively (i <= n).
The functional composition f_1 . ... . f_n can be expressed as follows:
(fun x_1 ... x_(m_1) y =>
  f_n _ ... _ (* m_n times repetition of holes *)
      (...
           (f_2 _ ... _ (* m_2 times repetition of holes *)
                (f_1 x_1 ... x_(m_1) y))...)),
and the contents of all the holes can be determined (inferred) without leaving
any existential variables in them thanks to the uniform inheritance condition.

Misc:
- A test case for this change: test-suite/output/relaxed_ambiguous_paths.v
- Turn the ambiguous paths messages into warnings to do output test.

5 files changed, 199 insertions, 20 deletions

diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 306a76e35e..0c44732021 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -308,9 +308,16 @@ let install_path_printer f = path_printer := f
 
 let print_path x = !path_printer x
 
-let message_ambig l =
-  str"Ambiguous paths:" ++ spc () ++
-  prlist_with_sep fnl print_path l
+let path_comparator : (inheritance_path -> inheritance_path -> bool) ref =
+  ref (fun _ _ -> false)
+
+let install_path_comparator f = path_comparator := f
+
+let compare_path p q = !path_comparator p q
+
+let warn_ambiguous_path =
+  CWarnings.create ~name:"ambiguous-paths" ~category:"typechecker"
+    (fun l -> strbrk"Ambiguous paths: " ++ prlist_with_sep fnl print_path l)
 
 (* add_coercion_in_graph : coe_index * cl_index * cl_index -> unit
                          coercion,source,target *)
@@ -329,21 +336,15 @@ let add_coercion_in_graph (ic,source,target) =
   let ambig_paths =
     (ref [] : ((cl_index * cl_index) * inheritance_path) list ref) in
   let try_add_new_path (i,j as ij) p =
-    try
-      if Bijint.Index.equal i j then begin
-	if different_class_params i then begin
-	  let _ = lookup_path_between_class ij in
-          ambig_paths := (ij,p)::!ambig_paths
-	end
-      end else begin
-        let _ = lookup_path_between_class ij in
-        ambig_paths := (ij,p)::!ambig_paths
-      end;
+    if not (Bijint.Index.equal i j) || different_class_params i then
+      match lookup_path_between_class ij with
+      | q ->
+        if not (compare_path p q) then
+          ambig_paths := (ij,p)::!ambig_paths;
+        false
+      | exception Not_found -> (add_new_path ij p; true)
+    else
       false
-    with Not_found -> begin
-      add_new_path ij p;
-      true
-    end
   in
   let try_add_new_path1 ij p =
     let _ = try_add_new_path ij p in ()
@@ -364,9 +365,7 @@ let add_coercion_in_graph (ic,source,target) =
 	 end)
       old_inheritance_graph
   end;
-  let is_ambig = match !ambig_paths with [] -> false | _ -> true in
-  if is_ambig && not !Flags.quiet then
-    Feedback.msg_info (message_ambig !ambig_paths)
+  match !ambig_paths with [] -> () | _ -> warn_ambiguous_path !ambig_paths
 
 type coercion = {
   coercion_type   : coe_typ;
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index 7c4842c8ae..a63f6a7487 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -100,6 +100,8 @@ val lookup_pattern_path_between :
 (* Crade *)
 val install_path_printer :
   ((cl_index * cl_index) * inheritance_path -> Pp.t) -> unit
+val install_path_comparator :
+  (inheritance_path -> inheritance_path -> bool) -> unit
 (**/**)
 
 (** {6 This is for printing purpose } *)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 9612932439..7405060188 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -1128,3 +1128,39 @@ let understand_tcc ?flags env sigma ?expected_type c =
 let understand_ltac flags env sigma lvar kind c =
   let (sigma, c, _) = ise_pretype_gen flags env sigma lvar kind c in
   (sigma, c)
+
+let path_convertible p q =
+  let open Classops in
+  let mkGRef ref          = DAst.make @@ Glob_term.GRef(ref,None) in
+  let mkGVar id           = DAst.make @@ Glob_term.GVar(id) in
+  let mkGApp(rt,rtl)      = DAst.make @@ Glob_term.GApp(rt,rtl) in
+  let mkGLambda(n,t,b)    = DAst.make @@ Glob_term.GLambda(n,Decl_kinds.Explicit,t,b) in
+  let mkGHole ()          = DAst.make @@ Glob_term.GHole(Evar_kinds.BinderType Anonymous,Namegen.IntroAnonymous,None) in
+  let path_to_gterm p =
+    match p with
+    | ic :: p' ->
+      let names =
+        List.map (fun n -> Id.of_string ("x" ^ string_of_int n))
+          (List.interval 0 ic.coe_param)
+      in
+      List.fold_right
+        (fun id t -> mkGLambda (Name id, mkGHole (), t)) names @@
+        List.fold_left
+          (fun t ic ->
+             mkGApp (mkGRef ic.coe_value,
+                     List.make ic.coe_param (mkGHole ()) @ [t]))
+          (mkGApp (mkGRef ic.coe_value, List.map (fun i -> mkGVar i) names))
+          p'
+    | [] -> anomaly (str "A coercion path shouldn't be empty.")
+  in
+  try
+    let e = Global.env () in
+    let sigma,tp = understand_tcc e (Evd.from_env e) (path_to_gterm p) in
+    let sigma,tq = understand_tcc e sigma (path_to_gterm q) in
+    if Evd.has_undefined sigma then
+      false
+    else
+      let _ = Evarconv.unify_delay e sigma tp tq in true
+  with Evarconv.UnableToUnify _ | PretypeError _ -> false
+
+let _ = Classops.install_path_comparator path_convertible
diff --git a/test-suite/output/relaxed_ambiguous_paths.out b/test-suite/output/relaxed_ambiguous_paths.out
new file mode 100644
index 0000000000..2a7ce806d7
--- /dev/null
+++ b/test-suite/output/relaxed_ambiguous_paths.out
@@ -0,0 +1,33 @@
+File "stdin", line 10, characters 0-28:
+Warning: Ambiguous paths: [ac; cd] : A >-> D [ambiguous-paths,typechecker]
+[ab] : A >-> B
+[ab; bd] : A >-> D
+[ac] : A >-> C
+[bd] : B >-> D
+[cd] : C >-> D
+[B_A] : B >-> A
+[C_A] : C >-> A
+[D_B] : D >-> B
+[D_A] : D >-> A
+[D_C] : D >-> C
+[A'_A] : A' >-> A
+[B_A'] : B >-> A'
+[B_A'; A'_A] : B >-> A
+[C_A'] : C >-> A'
+[C_A'; A'_A] : C >-> A
+[D_B; B_A'] : D >-> A'
+[D_A] : D >-> A
+[D_B] : D >-> B
+[D_C] : D >-> C
+File "stdin", line 103, characters 0-86:
+Warning: Ambiguous paths: [D_C; C_A'] : D >-> A'
+[ambiguous-paths,typechecker]
+[A'_A] : A' >-> A
+[B_A'] : B >-> A'
+[B_A'; A'_A] : B >-> A
+[C_A'] : C >-> A'
+[C_A'; A'_A] : C >-> A
+[D_B; B_A'] : D >-> A'
+[D_A] : D >-> A
+[D_B] : D >-> B
+[D_C] : D >-> C
diff --git a/test-suite/output/relaxed_ambiguous_paths.v b/test-suite/output/relaxed_ambiguous_paths.v
new file mode 100644
index 0000000000..a4af27539c
--- /dev/null
+++ b/test-suite/output/relaxed_ambiguous_paths.v
@@ -0,0 +1,109 @@
+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.
+
+Print Graph.
+
+End test1.
+End test1.
+
+Module test2.
+Section test2.
+Variable (A : Type) (P Q : A -> Prop).
+
+Record B := {
+  B_A : A;
+  B_P : P B_A }.
+
+Record C := {
+  C_A : A;
+  C_Q : Q C_A }.
+
+Record D := {
+  D_A : A;
+  D_P : P D_A;
+  D_Q : Q D_A }.
+
+Local Coercion B_A : B >-> A.
+Local Coercion C_A : C >-> A.
+Local Coercion D_A : D >-> A.
+Local Coercion D_B (d : D) : B := Build_B (D_A d) (D_P d).
+Local Coercion D_C (d : D) : C := Build_C (D_A d) (D_Q d).
+
+Print Graph.
+
+End test2.
+End test2.
+
+Module test3.
+Section test3.
+
+Variable (A : Type) (P Q : A -> Prop).
+
+Definition A' (x : bool) := A.
+
+Record B (x : bool) := {
+  B_A' : A' x;
+  B_P : P B_A' }.
+
+Record C (x : bool) := {
+  C_A' : A' x;
+  C_Q : Q C_A' }.
+
+Record D := {
+  D_A : A;
+  D_P : P D_A;
+  D_Q : Q D_A }.
+
+Local Coercion A'_A (x : bool) (a : A' x) : A := a.
+Local Coercion B_A' : B >-> A'.
+Local Coercion C_A' : C >-> A'.
+Local Coercion D_A : D >-> A.
+Local Coercion D_B (d : D) : B false := Build_B false (D_A d) (D_P d).
+Local Coercion D_C (d : D) : C true := Build_C true (D_A d) (D_Q d).
+
+Print Graph.
+
+End test3.
+End test3.
+
+Module test4.
+Section test4.
+
+Variable (A : Type) (P Q : A -> Prop).
+
+Record A' (x : bool) := { A'_A : A }.
+
+Record B (x : bool) := {
+  B_A' : A' x;
+  B_P : P (A'_A x B_A') }.
+
+Record C (x : bool) := {
+  C_A' : A' x;
+  C_Q : Q (A'_A x C_A') }.
+
+Record D := {
+  D_A : A;
+  D_P : P D_A;
+  D_Q : Q D_A }.
+
+Local Coercion A'_A : A' >-> A.
+Local Coercion B_A' : B >-> A'.
+Local Coercion C_A' : C >-> A'.
+Local Coercion D_A : D >-> A.
+Local Coercion D_B (d : D) : B false :=
+  Build_B false (Build_A' false (D_A d)) (D_P d).
+Local Coercion D_C (d : D) : C true :=
+  Build_C true (Build_A' true (D_A d)) (D_Q d).
+
+Print Graph.
+
+End test4.
+End test4.