Stream: Coq devs & plugin devs

Topic: tactics in terms and typeclasses


view this post on Zulip Jason Gross (Apr 13 2023 at 08:37):

Is there a reason that typeclass resolution runs after tactics in terms? (match foo with bar => ltac:(let v := eval cbv [bar] in bar in idtac v; exact v) end shows that foo will not have typeclasses resolved at the point at which the tactic is run)

view this post on Zulip Gaëtan Gilbert (Apr 13 2023 at 09:24):

do you mean "why is it not run before" or "why is it run at all"?

view this post on Zulip Jason Gross (Apr 13 2023 at 19:54):

I mean "why is it not run before"

view this post on Zulip Paolo Giarrusso (Apr 13 2023 at 21:22):

That seems to conflict with "solve all TC goals at once for better errors" and "backtrack on the result of one search if dependent searches fail" (but don't ask me whether that applies here), but can't the ltac run refine to force TC search instead?

view this post on Zulip Paolo Giarrusso (Apr 13 2023 at 21:23):

Or possibly, notypeclasses refine tm; solve [once (typeclasses eauto)] like stdpp's TCNoBackTrack does to avoid solving unrelated evars

view this post on Zulip Paolo Giarrusso (Apr 13 2023 at 21:25):

(source: https://gitlab.mpi-sws.org/iris/stdpp/-/blob/e00878becd64c5971940ecc62b5a1528d085d84d/stdpp/base.v#L62-94, if you enjoy cursed knowledge)

view this post on Zulip Gaëtan Gilbert (Apr 13 2023 at 21:40):

Jason Gross said:

I mean "why is it not run before"

you don't want that in general though
I mean imagine trying to do ltac:(exact (foo : P x)) : P (_ : SomeClass) if TC inference fills the _ with y
and that's assuming it only got called on TC evars in the expected type, it's even worse if it gets called on other evars

view this post on Zulip Gaëtan Gilbert (Apr 13 2023 at 21:42):

stuff like https://github.com/coq/coq/issues/6583 seems related if you want to pass time reading issues btw

view this post on Zulip Jason Gross (Apr 14 2023 at 01:18):

Do you know why https://github.com/coq/coq/pull/13071 was abandoned?


Last updated: Jul 24 2024 at 12:02 UTC