Minimize the set of multiple inheritance (coercion) paths to check for conversion

[pi8027]

The coercion mechanism reports a pair of inheritance paths sharing the same source and target classes (hereinafter a diamond) as ambiguous paths if they are inconvertible, to let the user ensure the coherence of the inheritance graph. In general, we do not necessarily have to check all the diamonds in an inheritance graph to verify its coherence. For example, it is sufficient to check two (small) diamonds ([f1; g2], [g1, f2]) and ([f2; h2], [h1; f3]) in the following diagram, since commutations of other (large) diamonds can be deduced from those of small ones using basic equational reasoning. In practice, not checking such large diamonds may reduce the number of ambiguous path warnings.

     /\
    /  \
f1 /    \ g1
  /      \
 /        \
 \        /\
  \   f2 /  \
g2 \    /    \ h1
    \  /      \
     \/        \
      \        /
       \      /
     h2 \    / f3
         \  /
          \/

This PR implements the most general way to do such reduction I could find, which is proved correct in the sense that the inheritance graph is coherent if Coq does not report any ambiguous path. (I also have a draft paper briefly explain this, which I think I can partially share if needed.) To check if a diamond is reducible or not, the table of coercion classes (class_tab) has been extended with:

1. the two sets of coercion classes reachable from (cl_reachable_from) and to (cl_reachable_to) the class, respectively, and
2. the representative element of the strongly connected component including the class (cl_repr).

(I will add more explanations later depending on what reviewers request. Let me run CI first.)

Kind: enhancement.

• Added / updated test-suite

• Corresponding documentation was added / updated (including any warning and error messages added / removed / modified).
• Entry added in the changelog (see https://github.com/coq/coq/tree/master/doc/changelog#unreleased-changelog for details).

[pi8027]

BTW, I still do not understand the following things in coercionops.ml:

• Bijint and cl_index are really needed? Replacing them with ClTypMap and cl_typ would work and simplify the implementation. (I believe there is no performance issue here. Another potential issue would be that the printing order of Print Graph will change.)
• A circular inheritance path of C >-> C can be registered to inheritance_graph only if different_class_params holds for C. What are the use cases of this?

[gares]

Bijint and cl_index are really needed? Replacing them with ClTypMap and cl_typ would work and simplify the implementation. (I believe there is no performance issue here. Another potential issue would be that the printing order of Print Graph will change.)

I'm OK with that. BTW, if you are going to refactor the code, in spite of #13902 being merged, I still don't have an API that given a GlobRef.t tells me the number of parameters and the src/tgt classes. Would you mind making it possible? (adding the missing fields to coe_info_typ should suffice)

A circular inheritance path of C >-> C can be registered to inheritance_graph only if different_class_params holds for C. What are the use cases of this?

If I'm not mistake these are not "loops" but rather a form of "identity coercions": indexing looking just at the head constant is too simplistic.

[pi8027]

Bijint and cl_index are really needed? Replacing them with ClTypMap and cl_typ would work and simplify the implementation. (I believe there is no performance issue here. Another potential issue would be that the printing order of Print Graph will change.)

I'm OK with that. BTW, if you are going to refactor the code, in spite of #13902 being merged, I still don't have an API that given a GlobRef.t tells me the number of parameters and the src/tgt classes. Would you mind making it possible? (adding the missing fields to coe_info_typ should suffice)

Sure. I will do that first and then redo this PR on top of it.

A circular inheritance path of C >-> C can be registered to inheritance_graph only if different_class_params holds for C. What are the use cases of this?

If I'm not mistake these are not "loops" but rather a form of "identity coercions": indexing looking just at the head constant is too simplistic.

I don't think so. In the following condition, different_class_params env i is relevant only if the source class i is equal to the target class j. If it is an identity coercion, the source class should be a constant that unfolds to the target class applied to some arguments; thus, they are not the same, as you said.

coq/pretyping/coercionops.ml

Line 341 in 4a0cf0f

if not (Bijint.Index.equal i j) || different_class_params env i then

[gares]

I think you can nor rebase on top of the refactoring PR which was merged

[pi8027]

I don't think I have to update the reference manual in accordance with this change. So this PR is ready for review.

[gares]

@pi8027 can you take of the request by @SkySkimmer ? Otherwise this seems ready to me.

[pi8027]

Yes. I will do that by the end of this week.

[gares]

@coqbot merge now

[coqbot-app]

@gares: You can't merge the PR because you're not among the assignees and no milestone is set.

[gares]

@coqbot merge now