diff options
| author | Kazuhiko Sakaguchi | 2019-12-08 19:24:43 +0900 |
|---|---|---|
| committer | Kazuhiko Sakaguchi | 2019-12-20 01:40:29 +0900 |
| commit | 025dc51c2eef7e7ea302465ff05d04d6fd4e7173 (patch) | |
| tree | a46e0839f515a4ff0482a6bf279f56ef5027e4a3 /doc/changelog | |
| parent | 6621e7cf79d7d824461de14007b2a06cabe59aef (diff) | |
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.
Diffstat (limited to 'doc/changelog')
| -rw-r--r-- | doc/changelog/07-commands-and-options/11258-coherence.rst | 10 |
1 files changed, 10 insertions, 0 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). |