Make Instance without a body always open a proof

[maximedenes]

This is a follow-up on #9270. It makes Instance without a body always open a proof.

The standard library was easy to fix. The only remaining open problem is how to make backward compatible fixes on downstream devs. This will probably require introducing a deprecated compatibility option.

Based on #9270 and #9273.

[maximedenes]

After this PR, the status of Instance (without Refine Instance Mode) is clear: with a body, it never opens a proof. Without, always.

[SkySkimmer]

Instead of this I would rather replace (if List.is_empty k.cl_props then Some (Inl subst) else None) by constant None. Essentially Instance is replacing on the fly no body with := {} if the class was declared as a trivial class, if we want no-body Instance to always open a proof we shouldn't do that.
Also I would rewrite Instance whatever : Class. to Instance whatever : Class := {}..

[maximedenes]

@SkySkimmer I think you are reading the code incorrectly. Look at the diff, it is about much more than trivial classes.

The change you suggest breaks much more, as it changes the semantics of Instance foo : C.

So I prefer the current version, where the only thing we do is to make Instance foo : C always open a proof (even if solved automatically), without changing the semantics.

[SkySkimmer]

Look at the diff, it is about much more than trivial classes.

I don't know stdlib classes enough to tell, can you explain more?

The change you suggest breaks much more, as it changes the semantics

Isn't changing the semantics the point?

[maximedenes]

I don't know stdlib classes enough to tell, can you explain more?

In fact, I was wrong, they are all trivial. It is just that we unbundle a lot of stuff.

I'll try your change, as it may be a more backward compatible way of doing things. Thanks!

[ppedrot]

LGTM. It looks like it needs many overlays though.

[maximedenes]

LGTM. It looks like it needs many overlays though.

Not really, as all the patches I submitted are backward compatible, so they can be integrated already.

[gares]

finally!

[mattam82]

Congrats!