Print information about the origin of constraints in Print Universes

[SkySkimmer]

Current limitations:

• constraints not associated with a constant or inductive have no origin
• the information is only about constraints in currently-open modules, so it's lost after module End and when loading files
• equality constraints have no origin (I didn't want to figure out how to deal with collapsing a cycle)
• constraints foo <(=) Set from declaring a universe have no origin (probably easily could be made to have one)

I think removing these limitations (especially the second one) won't require rewriting these patches so it's worth submitting now.

Here's how it looks after the Logic_lemmas section in Init/Logic.v:

Top.14 <= Top.9 (from eq_rect_r)
Top.13 <= Top.10 (from eq_rect_r)
       <= Top.8 (from eq_rect_r)
Top.12 <= Top.10 (from eq_rec_r)
       <= Top.8 (from eq_rec_r)
Top.11 <= Top.10 (from eq_ind_r)
       <= Top.8 (from eq_ind_r)
Top.10 <= Top.8 (from eq_sym)
Top.7 <= Top.6 (from inst)
Set < Top.14
    < Top.13
    < Top.12
    < Top.11
    < Top.10
    < Top.9
    < Top.8
    < Top.7
    < Top.6
    < Top.5
    < Top.4
    < Top.3
    < Top.2
    < Top.1
Prop < Set

[SkySkimmer]

IIRC @JasonGross was interested in some such feature.

[ppedrot]

I don't think that this should go in the kernel. I am struggling to get rid of monomorphic constraints registered in definitions, because they're completely broken (e.g. side-effects). Instead, this should be registered in some upper layers like declare.

[SkySkimmer]

I don't see how to make that work though.

[ppedrot]

Good question. I don't really know how to explain the semantics of your proposal though, IIUC it only attaches to edges, and this information is not preserved by transitivity (you drop the eq constraints), so I am slightly wary.

[ppedrot]

Also, we should strive for efficiency of the universe graph structure. It is not uncommon to have hundreds of thousands of universes in there, so every allocation is going to be critical. We should not make our users pay for data that is only for debugging purposes.

[JasonGross]

Nice!
Perhaps relatedly: I'd also like to see where the universe itself came from. That is, I'd like to be able to get an answer to the query "Given a global universe u, what is the list of definitions which have Type@{u} somewhere in their type or in their body (or list of constructor types, for (co)inductives), and which also do not transitively depend on any other definition in this list (except for (co)inductives and their constructors, which are allowed to depend on each other)?" Should I open a separate feature request for this?

[JasonGross]

I don't really know how to explain the semantics of your proposal though

@ppedrot Here are some semantics (which might or might not line up with this proposal) which would already be quite useful, even if not complete: The definition associated to a constraint i < j is a definition d such that, if Reset worked across module boundaries, and if all of the dependencies of the current file were inlined, then after Reset d the constraint i < j would no longer appear, and also there is no Reset command that keeps d but removes the constraint i < j.

[SkySkimmer]

I'm going to drop this for now.