Armaël Guéneau (Nov 22 2020 at 13:16): Armaël Guéneau (Nov 22 2020 at 13:16):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.
In 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…
Paolo Giarrusso (Nov 22 2020 at 13:34):you could “lock” assumptions in context — here it’s enough to change H : T into H : id T, and back.
Paolo Giarrusso (Nov 22 2020 at 13:35):(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)
Armaël Guéneau (Nov 22 2020 at 13:38):(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)
Armaël Guéneau (Nov 22 2020 at 13:38):but thanks, that sounds like it could work indeed
Last updated: Sep 26 2023 at 13:01 UTC