I'm using the following pattern as part of a tactic:
eapply lemma; try typeclasses eauto with mydb, where
lemma is a user-provided lemma.
mydb I have carefully crafted hints for a number of "known" constants that can appear in side-goals, with corresponding
Hint Modes to make sure that I don't wrongly instantiate evars.
However, it happens that, for side-goals which have no Hint Mode in
mydb, if there's a corresponding assumption in the local context,
typeclasses eauto will just use that, resulting in nonsensical evar instantiations.
Is there a way of either: say that typeclasses eauto should not instantiate evars, unless it has a Hint Mode that allows it; or, that typeclasses eauto should not use assumptions from the local context, unless they belong to some list of whitelisted classes...?
Though I realize this is fairly specific…
you could “lock” assumptions in context — here it’s enough to change
H : T into
H : id T, and back.
(for extra robustness, use a fresh
id function. You don’t even need to make it TC-opaque, IIRC, because TC matching is syntactic on the TC-head)
(it's great that you mention transparency, because I lost 1 hour yesterday debugging a strange bug, to ultimately rediscover https://github.com/coq/coq/issues/5381)
but thanks, that sounds like it could work indeed
Last updated: Feb 06 2023 at 13:03 UTC