The Coq mailing list

[Tom Prince <tom.prince AT ualberta.net>]

On 2011-05-06, Matthieu Sozeau wrote:
> > Class Arrows (O: Type): Type := Arrow: O → O → Type.
> > Instance flipA {Object} {A: Arrows Object}: Arrows Object := flip A.
> > CoInductive dual_arrows_done (T: Type) : Prop := did_dual_arrows.         
> >                
> > Hint Extern 100 (Arrows ?x) => match goal with                            
> >                
> >                                 | _ : dual_arrows_done x |- _ => fail 1   
> >               
> >                                 | |- _ => let H:=fresh "H" in set 
> > (H:=did_dual_arrows x); class_apply @flipA
> >                               end : typeclass_instances.  
> > 
> 
>   There is no way to tell if a flipA should be triggerd here, is there? 
> If you had a dummy [flipObject] definition to act as an index you could 
> control its application using an [Arrows (flipObject ?x)] pattern, but
> I guess you don't want that.

Well, I am not sure I have all the permutations, but I think I can
describe when it should be applied.
1) If we have already tried to apply other instances
*and*
2) We are not deducing the argument of flipA. (in particular, when the
outer flipA is provided by the user, not deduced.

It is a subtle thing, though, since adding the above hint also leads to
cycles caused by the instances defined in terms of flipA, that I haven't
figured out yet.

  Tom