Instance resolution: restricting the introduction of evars

Using Coq
1

Dear all,

Would there be a way to specify that an instance should not be applied during typeclass resolution if this application leads to the introduction of more evars?
Here is a self contained, minimal but completely silly example to illustrate what I mean:

Class Foo (T: Type): Type := {}.

Instance CBool {A} `{Foo A}: Foo bool := {}.
Instance CAssoc {A B C: Type} `{Foo ((A + B) + C)}: Foo (A + (B + C)) := {}.

Goal Foo bool.
  typeclasses eauto. (* This enters a death loop of evar introductions *)

I wish to be able to reassociate to the right before building interesting instances. However, in the case where the argument being reassociated is an evar, it leads to a loop. Setting a high priority to the rule does not solve the problem, since the depth first search means that it still loops in “dead branches”.
Morally speaking, I only want to reassociate when I have actually three constants or evars at hand to reassociate, hence enforcing the rule to only be applied when it does not introduce new evar would be sufficient.

Would anyone be aware of a mechanism, or a trick, to achieve this?

Thanks in advance,
Best,
Yannick

2

Dear Yannick,

note that in your example the issue is not purely CAssoc. CBool as sole instance already makes typeclasses eauto diverge.

But in you original setting maybe something like the following works:

Class Foo (T: Type): Type := {}.

Definition CBool {A} `{Foo A}: Foo bool := Build_Foo _.
Definition CAssoc {A B C: Type} `{Foo ((A + B) + C)}: Foo (A + (B + C)) := Build_Foo _.

Hint Extern 0 (Foo ?T) => tryif is_evar T then fail 100 else eapply CAssoc : typeclass_instances.

Goal Foo bool.
  typeclasses eauto.

The idea is to not declare an Instance, but to extend the typeclass_instances Hint database which is used by typeclasses eauto manually (I learned this general trick from Felix Rech, but it might be used commonly). In this manual extension, you can restrict the shape of goals you want the instance to apply to, for instance by checking whether the type T is an evar.

Does that help?

Best
Yannick

3

Dear Yannick,

Indeed you are very right that CBool itself here already loops, I was merely using it to force the introduction of an evar. In my actual use case, the association is the sole culprit.

Thanks a lot for the suggestion! I had never tried to manually extend the hint db when working with typeclasses, it definitely seems like the right idea.
And indeed the specific suggestion you have seems great to me, I think it exactly addresses my issue. I’ll test it as soon as possible.

Best,
Yannick