I was trying to use typeclasses to generalize the different notions of homomorphisms, but I’ve run into an annoying issue. Consider this code which demonstrates the issue:

```
(* Note that I don't actually have this class in my real code, this is just the
simplest way I could find to demonstrate the issue. *)
Class Trivial {U V} (f : U -> V) := {
trivial : forall a b, f a = f b
}.
Definition zero (a : nat) := 0.
Instance zero_trivial : Trivial zero.
Proof.
split.
reflexivity.
Qed.
Theorem fails : zero 0 = 0.
Proof.
rewrite (trivial (f := zero) 0 1). (* succeeds *)
rewrite (trivial 1 0). (* succeeds *)
rewrite (trivial 0 1). (* fails *)
Abort.
```

When trying to run that last rewrite, Coq says

```
Unable to satisfy the following constraints:
?Trivial : "Trivial (eq (zero 0))"
```

It seems that Coq is interpreting equality as the function I’m trying to say is trivial. I can get around this by specifying the function explicitly as I did in the first rewrite, but that’s cumbersome. So I guess I have two questions. First, I thought that typeclass resolution would keep skipping things until it found something that worked. So why is it getting stuck on trying to use equality as my function? It’s also strange that the second rewrite works but the third one doesn’t. Second, is there any easy way around this issue? I know that I can specify the function explicitly as above. I could also do some crazy thing where I make functions that typeclasses can apply to be their own type, but I feel like there has to be a simple way to do this.