Fixes #5481: support for unification of universe variables in congruence and f_equal

[herbelin]

We hash declarations without their universe instances while the universe constraints are (anyway) reinferred at the time of building the proof.

Giving two arguments to Ccalgo.Symb as I did is a bit hackish. The alternative would be to have a hash-consing function that discards universes but I did not find one.

Fixes #5481
Fixes #9979

Now also added: unification of universe levels so that congruence works on e.g. Type -> Type, the same way as it works for any non-Type T -> T.

• Added / updated test-suite.
• Added changelog.

[herbelin]

@coqbot run full ci

[ppedrot]

This is very hackish, and somewhat only side-stepping the real problem that we shouldn't ever rely on an ill-defined notion of "equality" for terms in an unification state... I guess this can qualify as a hotfix but I really don't like neither the original code nor the change.

[herbelin]

an ill-defined notion of "equality" for terms in an unification state

Can't we just say that congruence works with its own notion of quotient over terms and that it does not have to be a standard one?

That is, from the moment that congruence is able to reconstruct a CIC proof that the terms it equates are equal, is it blamable that it uses its own quotient?

[This being said, I don't like particularly the patch either, but I don't know what else to do.]

[ppedrot]

That is, from the moment that congruence is able to reconstruct a CIC proof that the terms it equates are equal

Equality only makes sense when the state is around. If you change the values of evars for instance, you'd get a different term. You cannot even EConstr.kind these things without the state.

[herbelin]

The union-find part of congruence currently reasons on the nf_evar-form of the term (EConstr.to_constr ~abort_on_undefined_evars:false sigma t in cctac.decompose_term). Then, it does no unification at all between evars and treat them equal only if syntactically equal.

In the PR, there is unification involved but only between universe levels. With the PR, any two universe levels are assumed unifiable by default and an attempt to actually unify them happens at proof reconstruction, when we are back in the econstr stateful world. (Note that I did not test what happens when it fails to reconstruct, so let's try, ah, it says "Not convertible", which maybe should be turned instead into "congruence failed"...).

Back to evars, would we like to have congruence work also modulo evar-unification? At least, it is unclear to me how to implement union-find up to unification, if that's your point.

[ppedrot]

@herbelin if you implement @SkySkimmer 's change I can merge.

[herbelin]

@herbelin if you implement @SkySkimmer 's change I can merge.

Done.

I also added catching a typing error so that a proper error message is issued when unification of levels fails.

[ppedrot]

@coqbot merge now