The Coq mailing list

[nicolas tabareau <nicolas.tabareau AT inria.fr>]

Dear All, 

It seems that when typeclasses eauto manages

to finish a subgoal with exact, it does not backtrack 

on it when the other subgoals fail (below a not too 

long example that exhibits the issue). 

Do I understand the problem correctly ?

Can it be solved without the seely alias trick 

I use ? 

Best, 

-- Nicolas 

Notation "x .1" := (projT1 x) (at level 3).

Parameter myType: Type. 

Class Foo (a:myType) := {}.

Class Bar (a:myType) := {}.

Parameter fooTobar : forall a (H : Foo a), {b: myType & Bar b}.

Hint Extern 5 (Bar ?D.1) =>

    destruct D; simpl : typeclass_instances.

Hint Extern 1 myType => simple refine (fooTobar _ _).1. 

Hint Extern 5 {b: myType & Bar b} =>

  simple refine (existT Bar (_:myType) _).

Definition trivial a (H : Foo a) : {b : myType & Bar b}. 

Proof.

  (* does not try to do simple refine (fooTobar _ _).1. *)

  Fail typeclasses eauto with core typeclass_instances.

Abort.

(* just using an alias, to prevent exact to succeed *)

Definition myType2:= myType.

Hint Extern 1 myType2 => simple refine (fooTobar _ _).1. 

Hint Extern 5 {b: myType2 & Bar b} =>

  simple refine (existT Bar (_:myType2) _).

Definition trivial a (H : Foo a) : {b : myType2 & Bar b}. 

Proof.

  typeclasses eauto with core typeclass_instances.

Defined.