The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

I know this is from quite a while ago, and I don't know if you've since solved it, but I was clearing out my inbox, and figured I'd take a crack at it.

If you move [Existing Class SetI_P.] to above your [Context] line, it works fine.  It also works fine if you add [Existing Instance p.] after [Existing Class SetI_P.].  I suspect that Coq only checks known instances, rather than the context.

On Thu, Nov 15, 2012 at 5:14 PM, Gregory Malecha <gmalecha AT eecs.harvard.edu> wrote:

Class SetI t :=

{ SetI_P : Type -> Type

; sinsert_with : forall {E} {p:SetI_P E}, (E -> E -> E) -> E -> t E -> t E

}.

Definition const {A B} : A -> B -> A := fun x _ => x.

Section SetI.

  Context {t} {E:Type} {S:SetI t} {p:SetI_P (t:=t) (SetI:=S) E}.

(* Typeclasses Transparent SetI_P. *)

  Set Printing Implicit.

  Typeclasses eauto := debug dfs.

  Existing Class SetI_P.

(*  Hint Extern 5 (@SetI_P _ _ _) => eassumption : typeclass_instances. *)

  Definition sinsertl : E -> t E -> t E := sinsert_with const.

End SetI.