Laurent Théry has marked this topic as resolved.
Pierre Roux said:
Do we really want to silence the warning? Shouldn't we rather, when adding a canonical instance, check if it already exist (and maybe also check that the already existing one is indeed the expected one)?
These warnings are about projections that are not used for canonical inference. They keep getting the same keys because the proofs or ops may be the same (or have the same head symbol), but not the main key (S.sort
) which must be different each time, and for these: yes there should be a check in HB that occurs before Coq discovers a duplicate key. The latter problem should indeed have the solution you described, whereas the former (which AFAIK is the one Laurent encounters) should be solved by informing Coq which projections are not keyed.
Last updated: Oct 13 2024 at 01:02 UTC