Jason Gross (Apr 13 2023 at 08:37): 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)
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"?
Jason Gross (Apr 13 2023 at 19:54):I mean "why is it not run before"
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?
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
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)
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
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
Jason Gross (Apr 14 2023 at 01:18):Do you know why https://github.com/coq/coq/pull/13071 was abandoned?
Last updated: Oct 13 2024 at 01:02 UTC