Return canonical instance from basic declare.ml APIs + use to fix Program bug

[SkySkimmer]

Fix #13979 (based on #18918)

[herbelin]

OK to me, thanks.

[herbelin]

These lines of code are used at least 2 other times in the code. Would it make sense to add them to the universe API (in particular, they seem obvious to expert, but documenting why they are canonical in some sense - if so - would help non-expert like me).

[herbelin]

By curiosity, why to extract a specific declare_primitive? It is because primitive cannot be polymorphic?

[SkySkimmer]

See the message on the commit which does this change

[herbelin]

OK.

One reason I'm asking is that I started to be afraid at some time by the diversity of code doing this or that manipulation on universes which is sometimes the same sometimes different of what is done in similar functions, and, at the end I felt unable to evaluate whether it is normal that there are difference or if there were oversights.

For instance, so that it is easier to be convinced that the treatment done in declare_primitive_core is consistent with what is done in declare_constant_core would it make sense to encapsulate the following lines beyond a level of abstraction shared with declare_constant_core:

let typ, ubinders, ctx = ... in
let () = Global.push_context_set ~strict:true ctx in
let ubinders = (UState.Monomorphic_entry ctx, ubinders) in
let () = DeclareUniv.declare_univ_binders (GlobRef.ConstRef kn) ubinders in

so that it is clear that it is intended to work as in declare_constant_core?

For instance, are Global.push_context_set and DeclareUniv.declare_univ_binders always supposed to go in pair?

Or, would it make sense to change the level of abstraction of extract_monomorphic to take a pair (univs, ubinders) and return a triple (univ_entry, ctx, (UState.Monomorphic_entry ctx, ubinders))?

PS: My question is more general than the PR and it is not blocking for the PR.

[SkySkimmer]

Seems not that useful in the end