The Coq mailing list

[Gregory Malecha <gmalecha AT eecs.harvard.edu>]

Hello --

I've got a simple goal that I can't seem to get type class resolution to work out. It seems like things should work but there is a unification variable that isn't being instantiated. Here's what I have: 

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.

The trace says:

1.1: exact S on

(SetI t)

2: no match for (@SetI_P t S E)

0 possibilities

backtracked after exact S

So it is solving the SetI, but it isn't looking into the context to find p.

Any idea what could be going wrong in this? Thanks.

-- 
gregory malecha

http://www.people.fas.harvard.edu/~gmalecha/