From 025dc51c2eef7e7ea302465ff05d04d6fd4e7173 Mon Sep 17 00:00:00 2001
From: Kazuhiko Sakaguchi
Date: Sun, 8 Dec 2019 19:24:43 +0900
Subject: 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.
---
 pretyping/classops.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping/classops.mli')

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 } *)
-- 
cgit v1.2.3