Add a way to disable typeclass search in `Program` obligations

From the coqdoc of the new feature:

(** When using [Program], you can use [notc_hole] in place of [_] to create
an obligation that does not trigger typeclass search. That is useful if the
search fails slowly, for instance for [Proper] obligations.
Should https://github.com/coq/coq/issues/12147 be fixed, this can be
deprecated or replaced by the new syntax. *)

Rationale for inclusion

I think https://github.com/coq/coq/issues/12147 is potentially bad enough that it could belong in stdpp. I haven't found very compelling usecases in iris: in part, you already avoid writing Program Definition foo ...: A -n> B, at the cost of more boilerplate.

See also: discussion from https://mattermost.mpi-sws.org/iris/pl/r885z6apefr9bjpuctczruogrr onwards.

changed the description

Why cannot you define this thing as tc_opaque _.

I don't understand what you wrote in the Mattermost thread:

what matters is that disable_tc_search takes id T instead of T — so that changes the hole's type enough to disable TC search.

What does it mean to take id T?

edit It's about the argument... I see now.

Sounds like I probably should add a testcase, also as documentation.

I think it would be good to upstream this to Coq.

However, that said, since we already have many such TC tricks in std++ I'm fine including this. We probably should bikeshed a bit about naming, so it is consistent with the tc_ like names we have.

@Blaisorblade: Do you consider upstreaming this to Coq? Any suggestions for more consistent names?

As names, what about tc_disable_hole (for the notation) and __tc_disable_hole_helper (feel free to drop the underscores, but that's not meant to be in the default namespace)? The latter is a candidate for a Local definition, if that actually works.

On upstreaming: I'm not sure this deserves upstreaming any more than the existing TC tricks, and Coq has a much longer release cycle. It'd also be less discoverable; reading base.v is way more instructive than the stdlib!

As names, what about tc_disable_hole (for the notation) and __tc_disable_hole_helper (feel free to drop the underscores, but that's not meant to be in the default namespace)? The latter is a candidate for a Local definition, if that actually works.

Yes, indeed, #[local] would be good, and better than the underscores?

I don't know if #[local] actually works in the old Coq versions we support, but Local Definition exists for a long time. So we could use that too.

Can you try?

@Blaisorblade What's the status of this?

Can't do it today, so not for the release.

@Blaisorblade What's the status of this? Do you plan to work on this?

Yes, sorry — and this is a good time for it. But we can still close the MR for the moment to clarify status if you want.

Closing this MR then, but feel free to reopen once you've fixed the issues.

closed

changed the description