Organization of the library of `constr`/`econstr` combinators

[herbelin]

Rendered here.

[herbelin]

Any comment on this ceps?

Basic common directions I proposed to follow are:

• to stop restricting ourselves to add combinators to Constr;
• in particular, to have the same sets of combinators on constr as on econstr: it is frustrating to need some combinator on some type, to see that it exists only on the other type, and to need a copy-paste or to try some contorsion to avoid the missing combinator;
• to consistently adopt the model Constr.map and EConstr.map after a public announcement to plugin developers on whether the price to pay for this consistency of style is acceptable for them.

On the other side, we can also live with things as they are too, if it is too complicated. One way to go would be to ask plugin developers. For those who are in interaction with some of them, what do you think would be best?

[ejgallego]

@herbelin the CEP looks pretty good to me, I'd say let's follow the plan.

Worth mentioning too is the effort by Gaëtan ( cc @skyskimmer ) unifying both types using a type-level index. IMHO that was very interesting but I think this PR would indeed help his effort.

[herbelin]

unifying both types using a type-level index.

I missed that. Is it a PR?

[SkySkimmer]

I missed that. Is it a PR?

See https://github.com/coq/coq/issues/6258#issuecomment-385292328

[herbelin]

Very interesting. So, basically, what you gain is that you don't need conversions to use constr functions on econstr when you know that the econstr is ground. What about the dependency of econstr functions on sigma? Do you plan to have all the combinators in the kernel (or in a constr library coming before the kernel) depending on a kind observer, and then, the kernel would instantiate these combinators with Constr.kind and the econstr level would instantiate them with EConstr.kind?

[SkySkimmer]

I don't have a plan. I had the idea and I'm experimenting with it (with low priority).

[herbelin]

I don't have a plan. I had the idea and I'm experimenting with it (with low priority).

Any update about that? I'm currently facing the need to use Inductiveops both on constr and econstr and the polymorphic constr approach seems very appealing.