Adapt w.r.t. coq/coq#14876.

[ppedrot]

No description provided.

[jdchristensen]

Maybe it would be helpful if there were comments explaining why those Hint Extern lines are needed. Even better if they could be removed or made more specific.

[jdchristensen]

Suggested change

	#[local]
	Hint Extern 4 => progress (cbv beta iota) : typeclass_instances.
	#[local] Hint Extern 4 => progress (cbv beta iota) : typeclass_instances.

[ppedrot]

See rocq-prover/rocq#14876. It introduces a change of semantics of Hint Unfold which is hit quite a bit by HoTT, probably because it's one of the only devs that uses Hint Unfold for typeclasses. I am not sure that this change is desired, but I wanted to attract the attention of the HoTT developers (which has succeeded it seems).

So, the doc states that Hint Unfold only applies to goals whose head is the global reference being unfolded, but this is only true for undiscriminated databases (i.e. virtually everybody except typeclass_instances). For discriminated databases (i.e. typeclasses) it actually unfolds the constant regardless of the goal, but this only happens when the hint is triggered (so this is conditioned by the priority, which is 4 for unfolding hints). The PR changes this behaviour to only trigger when the goal contains a constant to unfold, because otherwise this leads to a combinatorial explosion of the proof search (see the linked issue in the PR).

Now the funny thing is that unfolding a constant that does not appear in the goal turns out not to be a no-op. Indeed, unfold also performs βι-normalization of the goal. So, what happens in HoTT is that by merely adding a Hint Unfold in the typeclass db, one gets free βι-normalization from time to time, namely when proof depth is low enough. As demonstrated by the upstream PR, this behaviour is needed for a couple of TC resolutions. This is, I believe, a bug exploit.

The easy fix is the one demonstrated by the changes of this PR, namely to emulate the same "random βι-normalization" through a Hint Extern for the few resolutions that depend on the bug. Some places just needed normalization of the goal, hence the simpl. In any case this should be backwards compatible, but I need to be sure that you agree with the analysis that HoTT was exploiting a bug to proceed with the upstream PR.

[jdchristensen]

I think @JasonGross would have some good input here.

[JasonGross]

I'm in favor of this change, and the Coq PR. I would be fine even adding a #[global] or #[export] hint to do beta-iota simplification in typeclasses everywhere

[jdchristensen]

If we don't do it globally, then as people write new proofs, typeclass inference might not find things that it should, and they might not think to add the #[local] Hint. So that's an argument in favour of doing it globally. But someone should check whether it has a non-trivial cost in terms of build time...

[ppedrot]

I think we can enforce this on the Coq side, though. Most hints produces only βι-normalized goals, to the notable exception of Hint Extern. Even the dnet filtering relies implicitly on getting a normalized goal, so in some sense the latter behaviour could be considered a bug. I'll fiddle a bit with the auto implementations to see what happens.

[ppedrot]

I had a look and it seems that HoTT relies quite pervasively on typeclass resolution not preserving the invariant that all the goals it applies to are βι-normal. One the major reason for this failure is that composition is just a notation rather than a definition, so it tend to disappear after normalization. I don't know if this design pattern is HoTT-specific though.

[ppedrot]

I've reopened rocq-prover/rocq#14679 and closed rocq-prover/rocq#14876. See #1573 for the corresponding HoTT PR. Compared to this one I had to turn two Hint Unfold local to a section to an extern hint but that's about it.