Merge PR #9743: Relax the ambiguous path condition of coercion

Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: gares
Ack-by: pi8027

7 files changed, 206 insertions, 22 deletions

diff --git a/CHANGES.md b/CHANGES.md
index d43dc668e8..bf4244bdf9 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -156,6 +156,9 @@ Vernacular commands
 - Option `Refine Instance Mode` has been deprecated and will be removed in
   the next version.
 
+- `Coercion` does not warn ambiguous paths which are obviously convertible with
+  existing ones.
+
 Tools
 
 - The `-native-compiler` flag of `coqc` and `coqtop` now takes an argument which can have three values:
diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst
index 795fccbf08..d5523e8561 100644
--- a/doc/sphinx/addendum/implicit-coercions.rst
+++ b/doc/sphinx/addendum/implicit-coercions.rst
@@ -154,8 +154,10 @@ Declaring Coercions
   .. warn:: Ambiguous path.
 
      When the coercion :token:`qualid` is added to the inheritance graph,
-     invalid coercion paths are ignored; they are signaled by a warning
-     displaying these paths of the form :g:`[f₁;..;fₙ] : C >-> D`.
+     invalid coercion paths are ignored. The :cmd:`Coercion` command tries to check
+     that they are convertible with existing ones on the same classes.
+     The paths for which this check fails are displayed by a warning in the form
+     :g:`[f₁;..;fₙ] : C >-> D`.
 
   .. cmdv:: Local Coercion @qualid : @class >-> @class
 
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index ef918a614e..5560e5e5f5 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -305,9 +305,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 *)
@@ -326,21 +333,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 ()
@@ -361,9 +362,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 ed2c5478f0..bd468e62ad 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 8e9a2e114b..3c8d31d671 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -1141,3 +1141,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.