Coherence checking for coercions

This change improves the relaxed ambiguous path condition of coercions (#9743)
to check that any circular inheritance path of `C >-> C` is definitionally equal
to the identity function of the class `C`. Moreover, for a new inheritance path
`p : C >-> D` and existing (valid) one `q : C >-> D`, the new mechanism does not
report the ambiguity of `p` and `q` if they have a common element, that is to
say:
`p = p1 @ [c] @ p2` and `q = q1 @ [c] @ q2`
  for some coercion `c` and inheritance paths `p1`, `p2`, `q1`, and `q2`.
In that case, 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 the new mechanism does not report any ambiguous path, the inheritance graph
must be coherent [Barthe 1995, Sect. 3.2] [Saïbi 1997, Sect. 7]:
1. for any circular path `p : C >-> C`, `p` is definitionally equal to the
   identity function, and
2. for any two paths `p, q : C >-> D`, `p` and `q` are convertible.

[Barthe 1995] Gilles Barthe, Implicit coercions in type systems, In: TYPES '95,
              LNCS, vol 1158, Springer, 1996, pp 1-15.
[Saïbi 1997]  Amokrane Saïbi, Typing algorithm in type theory with inheritance,
              In: POPL '97, ACM, 1997, pp 292-301.

7 files changed, 129 insertions, 23 deletions

diff --git a/doc/changelog/07-commands-and-options/11258-coherence.rst b/doc/changelog/07-commands-and-options/11258-coherence.rst
new file mode 100644
index 0000000000..f04a120417
--- /dev/null
+++ b/doc/changelog/07-commands-and-options/11258-coherence.rst
@@ -0,0 +1,10 @@
+- **Changed:**
+  The :cmd:`Coercion` command has been improved to check the coherence of the
+  inheritance graph. It checks whether a circular inheritance path of `C >-> C`
+  is convertible with the identity function or not, then report it as an
+  ambiguous path if it is not.  The new mechanism does not report ambiguous
+  paths that are redundant with others. For example, checking the ambiguity of
+  `[f; g]` and `[f'; g]` is redundant with that of `[f]` and `[f']` thus will
+  not be reported
+  (`#11258 <https://github.com/coq/coq/pull/11258>`_,
+  by Kazuhiko Sakaguchi).
diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst
index c3b197288f..19b33f0d90 100644
--- a/doc/sphinx/addendum/implicit-coercions.rst
+++ b/doc/sphinx/addendum/implicit-coercions.rst
@@ -165,6 +165,12 @@ Declaring Coercions
      convertible with existing ones when they have coercions that don't satisfy
      the uniform inheritance condition.
 
+  .. warn:: ... is not definitionally an identity function.
+
+     If a coercion path has the same source and target class, that is said to be
+     circular. When a new circular coercion path is not convertible with the
+     identity function, it will be reported as ambiguous.
+
   .. cmdv:: Local Coercion @qualid : @class >-> @class
 
      Declares the construction denoted by :token:`qualid` as a coercion local to
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index c12a236d8e..16021b66f8 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -297,15 +297,15 @@ let lookup_pattern_path_between env (s,t) =
 
 (* rajouter une coercion dans le graphe *)
 
-let path_printer : ((Bijint.Index.t * Bijint.Index.t) * inheritance_path -> Pp.t) ref =
+let path_printer : ((cl_index * cl_index) * inheritance_path -> Pp.t) ref =
   ref (fun _ -> str "<a class path>")
 
 let install_path_printer f = path_printer := f
 
 let print_path x = !path_printer x
 
-let path_comparator : (Environ.env -> Evd.evar_map -> inheritance_path -> inheritance_path -> bool) ref =
-  ref (fun _ _ _ _ -> false)
+let path_comparator : (Environ.env -> Evd.evar_map -> cl_index -> inheritance_path -> inheritance_path -> bool) ref =
+  ref (fun _ _ _ _ _ -> false)
 
 let install_path_comparator f = path_comparator := f
 
@@ -315,7 +315,10 @@ let warn_ambiguous_path =
   CWarnings.create ~name:"ambiguous-paths" ~category:"typechecker"
     (fun l -> prlist_with_sep fnl (fun (c,p,q) ->
          str"New coercion path " ++ print_path (c,p) ++
-         str" is ambiguous with existing " ++ print_path (c, q) ++ str".") l)
+         if List.is_empty q then
+           str" is not definitionally an identity function."
+         else
+           str" is ambiguous with existing " ++ print_path (c, q) ++ str".") l)
 
 (* add_coercion_in_graph : coe_index * cl_index * cl_index -> unit
                          coercion,source,target *)
@@ -334,10 +337,23 @@ let add_coercion_in_graph env sigma (ic,source,target) =
   let ambig_paths =
     (ref [] : ((cl_index * cl_index) * inheritance_path * inheritance_path) list ref) 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 Bijint.Index.equal i j && not (compare_path env sigma i p []) then
+      ambig_paths := (ij,p,[])::!ambig_paths;
     if not (Bijint.Index.equal i j) || different_class_params env i then
       match lookup_path_between_class ij with
       | q ->
-        if not (compare_path env sigma p q) then
+        (* 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)
@@ -355,7 +371,7 @@ let add_coercion_in_graph env sigma (ic,source,target) =
              try_add_new_path1 (s,target) (p@[ic]);
              ClPairMap.iter
                (fun (u,v) q ->
-                  if not (Bijint.Index.equal u v) && Bijint.Index.equal u target &&  not (List.equal coe_info_typ_equal p q) then
+                  if not (Bijint.Index.equal u v) && Bijint.Index.equal u target then
                     try_add_new_path1 (s,v) (p@[ic]@q))
                old_inheritance_graph
            end;
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index 9c5274286e..9f633843eb 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -111,7 +111,7 @@ val lookup_pattern_path_between :
 val install_path_printer :
   ((cl_index * cl_index) * inheritance_path -> Pp.t) -> unit
 val install_path_comparator :
-  (env -> evar_map -> inheritance_path -> inheritance_path -> bool) -> unit
+  (env -> evar_map -> cl_index -> inheritance_path -> inheritance_path -> bool) -> unit
 (**/**)
 
 (** {6 This is for printing purpose } *)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 43f9e55e14..0364e1b61f 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -1325,19 +1325,20 @@ 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 env sigma p q =
+let path_convertible env sigma i 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,Explicit,t,b) in
+  let mkGSort u           = DAst.make @@ Glob_term.GSort u 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)
+        List.init (ic.coe_param + 1)
+          (fun n -> Id.of_string ("x" ^ string_of_int n))
       in
       List.fold_right
         (fun id t -> mkGLambda (Name id, mkGHole (), t)) names @@
@@ -1345,9 +1346,29 @@ let path_convertible env sigma p q =
           (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))
+          (mkGApp (mkGRef ic.coe_value, List.map mkGVar names))
           p'
-    | [] -> anomaly (str "A coercion path shouldn't be empty.")
+    | [] ->
+      (* identity function for the class [i]. *)
+      let cl,params = class_info_from_index i in
+      let clty =
+        match cl with
+        | CL_SORT -> mkGSort (Glob_term.UAnonymous {rigid=false})
+        | CL_FUN -> anomaly (str "A source class must not be Funclass.")
+        | CL_SECVAR v -> mkGRef (GlobRef.VarRef v)
+        | CL_CONST c -> mkGRef (GlobRef.ConstRef c)
+        | CL_IND i -> mkGRef (GlobRef.IndRef i)
+        | CL_PROJ p -> mkGRef (GlobRef.ConstRef (Projection.Repr.constant p))
+      in
+      let names =
+        List.init params.cl_param
+          (fun n -> Id.of_string ("x" ^ string_of_int n))
+      in
+      List.fold_right
+        (fun id t -> mkGLambda (Name id, mkGHole (), t)) names @@
+        mkGLambda (Name (Id.of_string "x"),
+                   mkGApp (clty, List.map mkGVar names),
+                   mkGVar (Id.of_string "x"))
   in
   try
     let sigma,tp = understand_tcc env sigma (path_to_gterm p) in
diff --git a/test-suite/output/relaxed_ambiguous_paths.out b/test-suite/output/relaxed_ambiguous_paths.out
index dc793598a9..ac5a09bad7 100644
--- a/test-suite/output/relaxed_ambiguous_paths.out
+++ b/test-suite/output/relaxed_ambiguous_paths.out
@@ -7,6 +7,16 @@ New coercion path [ac; cd] : A >-> D is ambiguous with existing
 [ac] : A >-> C
 [bd] : B >-> D
 [cd] : C >-> D
+File "stdin", line 26, characters 0-28:
+Warning:
+New coercion path [ab; bc] : A >-> C is ambiguous with existing 
+[ac] : A >-> C. [ambiguous-paths,typechecker]
+[ac] : A >-> C
+[ac; cd] : A >-> D
+[ab] : A >-> B
+[cd] : C >-> D
+[bc] : B >-> C
+[bc; cd] : B >-> D
 [B_A] : B >-> A
 [C_A] : C >-> A
 [D_B] : D >-> B
@@ -21,7 +31,7 @@ New coercion path [ac; cd] : A >-> D is ambiguous with existing
 [D_A] : D >-> A
 [D_B] : D >-> B
 [D_C] : D >-> C
-File "stdin", line 103, characters 0-86:
+File "stdin", line 121, 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]
@@ -34,3 +44,15 @@ New coercion path [D_C; C_A'] : D >-> A' is ambiguous with existing
 [D_A] : D >-> A
 [D_B] : D >-> B
 [D_C] : D >-> C
+File "stdin", line 130, 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:
+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:
+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 a4af27539c..41322045f2 100644
--- a/test-suite/output/relaxed_ambiguous_paths.v
+++ b/test-suite/output/relaxed_ambiguous_paths.v
@@ -16,6 +16,24 @@ End test1.
 
 Module test2.
 Section test2.
+
+Variable (A B C D : Type).
+Variable (ab : A -> B) (bc : B -> C) (ac : A -> C) (cd : C -> D).
+
+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`.           *)
+
+Print Graph.
+
+End test2.
+End test2.
+
+Module test3.
+Section test3.
 Variable (A : Type) (P Q : A -> Prop).
 
 Record B := {
@@ -39,11 +57,11 @@ Local Coercion D_C (d : D) : C := Build_C (D_A d) (D_Q d).
 
 Print Graph.
 
-End test2.
-End test2.
+End test3.
+End test3.
 
-Module test3.
-Section test3.
+Module test4.
+Section test4.
 
 Variable (A : Type) (P Q : A -> Prop).
 
@@ -71,11 +89,11 @@ Local Coercion D_C (d : D) : C true := Build_C true (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).
 
@@ -105,5 +123,18 @@ Local Coercion D_C (d : D) : C true :=
 
 Print Graph.
 
-End test4.
-End test4.
+End test5.
+End test5.
+
+Module test6.
+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.
+
+Module test7.
+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.