The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT gmail.com>]

Hi,

Le 11 mars 2011 à 02:13, Tom Prince a écrit :

> On 2011-03-10, Daniel Schepler wrote:
>> Let me add my own question on typeclasses:
>> 
>> Suppose I define
>> 
>> Generalizable All Variables.
>> 
>> Class ExtEqual {X Y} (f g:X->Y) : Prop :=
>>  extensional_equality : forall x:X, f x = g x.
>> 
>> Class injective `(f:X->Y) : Prop :=
>>  injectivity: forall x1 x2:X, f x1 = f x2 -> x1 = x2.
>> 
>> Instance injective_properness
>>  `{ExtEqual X Y f g} `{injective _ _ f} :
>>  injective g.
>> 
>> Here why do I have to fill in the implicit arguments for ExtEqual and 
>> injective?  Is that the intended behavior?
> 
> You can get the usual handling of implicit arguments by inserting ! at
> the begining of an generalizing binder, which also turns off the
> implicit generalization of unspecified arguments. I don't know what the
> rational for this behaviour is.

The idea is that one can easily bind all the parameters in one go, as in 
`{ExtEqual X Y f g}. Compare with [{X Y} {f : X -> Y} {g} {ExtEqual f g}].
You could simply write {_:injective f} for the second binder.

> 
>> Also, it seems if I add too many instances along these lines (fg injective 
>> -> 
>> g injective, id injective and surjective, etc.) I tend to end up with the 
>> resolver failing in simple situations, and "typeclasses eauto" looping.
> 
> I think that this is a known issue. I don't know of any general
> workarounds. One suggestion that I have seen for some cases, is to add a
> hint conditioned with a more specific pattern to the typeclass_instances
> database. (An instance is, as far as I can tell, essentially a hint in
> this databse)

Indeed it is. Clearly [fg injective -> g injective] is dangerous as it may
be applied infinitely often, starting with any [injective] goal.

-- Matthieu