Generalized coercions

[Tragicus]

This PR adds better support for coercions:

• declares the constructor of the class as an elpi coercion, using elaborate-skeleton to fill in the holes,
• declares the sort projection as an elpi coercion when there is no coercion target,
• declares axioms_ as a typeclass (enables inference in the first coercion)

[gares]

@CohenCyril LGTM. Can you double check and merge?

[Tragicus]

As your tests show, the sort coercion postcomposes and does not precompose with Coq's coercions. This is because when the algorithm sees that the type of the input term is a structure, it applies the projection and then asks for a coercion to the target type. The converse holds for the reverse coercion: it precomposes and does not postcompose with Coq's coercions. This is because when the algorithm sees that the target type is a structure, it tries to build the package and lets the elaborator find the missing class. I assume that the elaborator also catches the type mismatch of the subjects and looks for a coercion.

[gares]

About post composition, the code does not look at the expected type. If the inferred type is a structure it elaborates (sort t) against the expected type. So Coq can insert further coercions.

If the inferred type is not a structure, then it does nothing.

In your last examples I think that the first coercion from C to sigType is inserted by Coq, then elpi goes to A and then Coq goes to C.

I'm not so sure I see a use case for something (that is not a structure) coercing to a structure.

[CohenCyril]

I'm not so sure I see a use case for something (that is not a structure) coercing to a structure.

One way to test it on a large scale would be to systematically replace Coq coercions by elpi coercions even for structures in Type and see if/where it breaks.

[Tragicus]

A use case for something that is not a structure coercing to a structure is when you have an object that satisfies properties that would promote it to a structure, e.g. morphisms and subobjects. This coercion allows you to skip the packaging phase.

[gares]

IMO, the only missing bit is a documentation, et least in the changelog.

[gares]

@CohenCyril can you look at the PR again and decide what to do?

[gares]

I did a couple of suggestions, to be tested. Other than that it looks OK. @CohenCyril ?

[CohenCyril]

Taking a look this afternoon

[CohenCyril]

Could you squash and rebase? I am considering backtracking on the default status of #[typeclass], would you mind running a bench to check the impact on MC and MCA in both scenarios?

[Tragicus]

Do we have tools to do a benchmark?

[gares]

I think it would be enough to time make -j1. You can also make TIMED=1 to get a per file compilation time.

[Tragicus]

Ok thanks, I will do that tonight or tomorrow.

[Tragicus]

It took forever, but the bench is done. Interestingly enough, the version with typeclasses by default is slightly slower and uses slightly less memory, though the difference is negligible. bench.ods Should I compare with a bench of master?

[Tragicus]

Well, I did it anyway, and master is about 3x faster than proto-coercion. bench.ods.

[Tragicus]

Here is the new bench, proto-coercion is a little less than 2x slower than master. The profiling might be complicated since the slowdown occurs in tactics like apply:. benchcoe.ods

[gares]

Damn, I guess we will have to wait for some speedup in the bootstrap time of elpi... or disable coercion in apply: but I don't know if the api makes it easy.