Correctly classify variables as being unfoldable in dnet patterns.

[ppedrot]

Fixes #12571.

• Added / updated test-suite
• Entry added in the changelog (see https://github.com/coq/coq/tree/master/doc/changelog#unreleased-changelog for details).

[ppedrot]

This will need a (backwards compatible) overlay for HoTT.

[ppedrot]

The bug was correctly identified in many places in HoTT, there were several comments wondering why typeclass resolution was not solving the goal...

[maximedenes]

How about removing the default case, so as to prevent similar future problems? Maybe also in constr_pat_discr_st.

[maximedenes]

Could this improve the compatibility story for switching to discriminated bases (in which case it could be good to re-evaluate it), or is it a separate mechanism?

[ppedrot]

@maximedenes do you mean that we need to explicit all constr constructors? I don't think it'd help much, the problem here seems to have arised from the when clause instead.

[ppedrot]

Could this improve the compatibility story for switching to discriminated bases

I don't think it'd matter much, it's fairly uncommon to have local definitions.

[maximedenes]

do you mean that we need to explicit all constr constructors?

Yes, this is what I mean.

I don't think it'd help much, the problem here seems to have arised from the when clause instead.

In general, I tend to recommend to avoid fragile pattern matchings on constr, as it makes it very hard to extend terms. The only exception is when you are really looking for a specific kind of terms.

Also, is there any drawback in listing the few remaining cases?

[ppedrot]

In general, I tend to recommend to avoid fragile pattern matchings on constr

As far as I am concerned, I hate when clauses with a passion, even for non-constr matchings. They're an incredible source of bugs and subtle code, when it should be straightforward to inline an if-then-else branch that ensures statically a lot of stuff. Most other people seem to like them so I don't make a fuss, but personally I never introduce them.

Also, is there any drawback in listing the few remaining cases?

It's going to make this one-line fix bigger, but if you insist...

[maximedenes]

It's going to make this one-line fix bigger

I don't think it's a big problem to add 3-4 lines to this patch.

[ppedrot]

Your desires are orders.

[maximedenes]

Well spotted!

[ppedrot]

The HoTT overlay has been merged upstream, this should be ready now.

[maximedenes]

@mattam82 do you want to be the assignee, or should I take it, as this looks like a straightforward fix?

[ppedrot]

@maximedenes you should probably assign it's quite a straightforward PR.

[ppedrot]

@maximedenes ping