HB. commands should insert coercions when necessary about hierarchy-builder HOT 7 CLOSED

So should we implement [1, Sect. 4] to the elaborator [2] of Coq-elpi? Supporting the only coercions to Sortclass might be sufficient with regard to canonical instance declarations and easier than implementing the complete typing algorithm. I'm not sure.

• [1] https://dl.acm.org/doi/10.1145/263699.263742
• [2] https://github.com/LPCIC/coq-elpi/blob/master/engine/elaborator.elpi

from hierarchy-builder.

Yes that would be my plan, but I would not work on it now (before writing the Hb paper)

We can live with it, or have a type of arguments that are elaborated by coq beforehand (syntax needed).

Ftr coq.elaborate was supposed to insert coercions but was broken beyond repair wrt universes and evars. Pretyping.ml wants a glob_constr in input, not a constr, and the detyping phase messes up evars (I could found a hack for univs). I can put it back, but it would be tricky to use. I'll think more about it later today, it may work for the simple use case we discuss here as a temporary solution

from hierarchy-builder.

@pi8027 https://github.com/LPCIC/coq-elpi/blob/1d82b967672ff0f77529a6aca4a894bc523162cf/engine/elaborator.elpi#L309 has some (inefficient since it computes the closure every time and not well tested) support for coercions but you need to load the context with clauses representing coercions and enable coercions, see https://github.com/LPCIC/coq-elpi/blob/1d82b967672ff0f77529a6aca4a894bc523162cf/theories/tests/test_elaborator.v#L91. for sortclass it may even work

from hierarchy-builder.

I'm a shame. @CohenCyril @pi8027 this is how to make of insert Ring.sort: https://github.com/LPCIC/coq-elpi/blob/1d82b967672ff0f77529a6aca4a894bc523162cf/theories/tests/test_elaborator.v#L147

from hierarchy-builder.

At least, I'm familiar with the construction of inheritance graphs (in Coq). I will try to work on that on Monday.

from hierarchy-builder.

see #35

from hierarchy-builder.

See also LPCIC/coq-elpi#170 what should provide a solid approach to this

from hierarchy-builder.