The Coq mailing list

["J. Ian Johnson" <ianj AT ccs.neu.edu>]

I am turning the finite map library into a typeclass and extending it to use 
setoids. There are different properties about them that are registered as 
immediate or for resolve, but I can't do that kind of hint registration with 
typeclass members. For example:

Class TC := { mem : forall x : Type, x = x}.

Hint Immediate mem.

Error: Cannot infer the implicit parameter TC of mem.
Could not find an instance for "TC".

This seems like the wrong semantics for hint registration (trying to infer an 
instance at the definition site). Am I misguided in this? Also, it turns out 
that since the environment was so large at this hint definition, the 
inference just went out to lunch. I had to guess that this was the problem.

I also learned that I reaaaaally want a "Section"-like typeclass definition 
form. I ended up having to write a section that defined all the types I 
wanted for the class along with the auxiliary definitions, then defining the 
typeclass with all the quantifiers... blech.

Thanks,
-J. Ian Johnson