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

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

3 files changed, 57 insertions, 20 deletions

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