Stream: Coq users

Topic: Hint priority in typeclasses eauto with multiple DBs

view this post on Zulip Janno (Dec 02 2021 at 16:18):

I expected typeclasses eauto with dbA dbB to treat hints from dbA and dbB the same way. In particular, if dbA has low priority hints and dbB has high priority hints, hints from dbB should be applied first. That's what I thought, at least. However, this is not the case: see the (synthetic) example below. Is this behavior intended? The documentation doesn't seem to mention anything about this. (The behavior is the same with discriminated hint databases.)

Create HintDb dbA.
Create HintDb dbB.
Class H := {h : nat}.
Definition h1 : H := {|h:=1|}.
Definition h2 : H := {|h:=2|}.
#[local] Hint Resolve h1 | 100 : dbA.
#[local] Hint Resolve h2 | 0   : dbB.
Goal exists i, i.(@h) = 2.
  unshelve econstructor; [typeclasses eauto with dbA dbB|cbn].
  Fail reflexivity.             (* 1 =/= 2 *)

I fear that this makes it very difficult to split up a large database into smaller ones.

view this post on Zulip Janno (Dec 02 2021 at 16:37):

It seems this was already reported on the issue tracker: https://github.com/coq/coq/issues/5304

Last updated: Sep 23 2023 at 13:01 UTC