Elimination constraints for bounded sort polymorphism

[jrosain]

Rendered https://github.com/jrosain/rocq-rfcs/blob/elimination-constraints/text/elimination-constraints.md

[jfehrle]

Since Roq uses the concept of polymorphism in many ways, perhaps it would be better to have a more descriptive string than just "poly" in nonterminal names in the grammar. "sort_poly" would be much clearer and it only makes names a little bit longer on the doc.

[jrosain]

That's a good point, it'll be done.

[yannl35133]

What properties is "eliminates to" expected to have? Reflexivity and transitivity are somewhat implicit here, but I mostly wonder about antisymmetry wrt. sort conversion, similar to universe level comparison being antisymmetric wrt. level conversion.

[jrosain]

What properties is "eliminates to" expected to have? Reflexivity and transitivity are somewhat implicit here, but I mostly wonder about antisymmetry wrt. sort conversion, similar to universe level comparison being antisymmetric wrt. level conversion.

Right! Note that we may have non-reflexive sorts, iirc @tabareau has some examples of this.

About antisymmetry: if s eliminates to s' and conversely, every type of s is also a type of s', and every type of s' is a type of s so s and s' cannot be distinguished. We believe that it makes two sorts equal for conversion, but we don't have a strong theoretical justification for this yet.

[ppedrot]

I'm planning to actually change that before the release, not only because there is no justification for that, but also because this is basically an implementation leak.

[jrosain]

Yes, I agree that it was premature, and it makes sense to remove this for the time being.