How to report the status of existential variables in a UI in the future?

[hendriktews]

Is your feature request related to a problem?

In #18991, which attempts to fix #18980, @ppedrot commented that future Coq versions might not feature the dependent evar line. I opened this issue to discuss how a Coq user interface could obtain the necessary information from Coq in order to indicate the status of existential variables for such a future Coq version.
With the dependent evar line, a user interface can give information about which existential variables are not instantiated yet, which are partially instantiated (in the sense that they are instantiated with a term which still contains an open existential variable), and which are fully instantiated.
When such information is present in the user interface, one can immediately investigate when some existential variable is not completely instantiated as expected during proof development. Without such information in the user interface one might only see at the end of the proof that some existential variable still needs to be instantiated.
I would be interested how one can retrieve the information that is present in the dependent evar line in 8.17 without using this line.

Proposed solution

No response

Alternative solutions

No response

Additional context

No response

[ppedrot]

a user interface can give information about which existential variables are not instantiated yet, which are partially instantiated (in the sense that they are instantiated with a term which still contains an open existential variable), and which are fully instantiated.

This spec is perfectly reasonable, but this is not what the dependent evar printing mechanism is doing. The thing that is very much not compatible with the proof engine is the ability to check that an instantiated evar depends on another instantiated evar, because an instantiated evar should behave exactly like its expansion.

[SkySkimmer]

If you save a econstr which is the evar when it's uninstantiated, you can inspect it in a later evar map to see if it got instantiated (assuming Optimize Proof or other hypothetical GC mechanisms didn't invalidate it).
That requires some upfront work though.