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.

1 files changed, 26 insertions, 5 deletions

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