Stream: Coq users

Topic: typeclasses eauto: restricting the use of the local context


view this post on Zulip 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…

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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)

view this post on Zulip Armaël Guéneau (Nov 22 2020 at 13:38):

but thanks, that sounds like it could work indeed


Last updated: Feb 06 2023 at 13:03 UTC