The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi Jason,

Le 22 mars 2013 à 05:32, Jason Gross 
<jasongross9 AT gmail.com>
 a écrit :
> 
> Hint Rewrite @FIdentityOf using eauto with typeclass_instances : functor.

>   Fail rewrite @FIdentityOf by auto with typeclass_instances. (* should not 
> fail *)
>   erewrite @FIdentityOf by auto with typeclass_instances.

The problem is that, even before launching type class resolution, [rewrite] 
expects
the metavariables for H and H0 to be instantiated, that's why it fails. If 
instead it
used existential variables (like [setoid_rewrite FIdentityOf] does) it 
wouldn't fail.
There is an (undocumented) tactic [rewrite_db hintdb] which does setoid 
rewrite
using the rewrite hint database hintdb, but it doesn't take care of the side 
condition tactic (yet). You could still use it like this:

Require Import Setoid.
Ltac rewrite_cat := rewrite_db functor; try typeclasses eauto.

And use rewrite_cat instead of your autorewrite.
-- Matthieu