Instance search for HSubst vl ?X picks an arbitrary solution instead of giving an ambiguity error, and that is only desirable for languages with one HSubst instance. So it's easy to accidentally declare lemmas for the wrong types and notice later.
This is a matter of design choice, but using Hint Mode seems fairly common practice among typeclass users.
Below's an excerpt from some development of mine:
Instance Subst_vl : Subst vl := vl_subst.
Instance HSubst_tm : HSubst vl tm := tm_hsubst.
Instance HSubst_ty : HSubst vl ty := ty_hsubst.
Goal ∀ s x, x.|[s] = x.
(* x is inferred to have type [ty] because that was the last declared instance — swapping the instances changes the type. *)
Abort.
Hint Mode HSubst - +: typeclass_instances.
(* [Hint Mode HSubst - !: typeclass_instances.] would also work in this test, but I can't think of a case where that's preferable. *)
Fail Goal ∀ s x , x.|[s] = x.
Goal ∀ s (x: ty) , x.|[s] = x. Abort.
I'm aware the library is not actively developed, but it is actively used, so this might be useful to other readers.
Instance search for
HSubst vl ?Xpicks an arbitrary solution instead of giving an ambiguity error, and that is only desirable for languages with one HSubst instance. So it's easy to accidentally declare lemmas for the wrong types and notice later.This is a matter of design choice, but using
Hint Modeseems fairly common practice among typeclass users.Below's an excerpt from some development of mine:
I'm aware the library is not actively developed, but it is actively used, so this might be useful to other readers.