The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Dear Gert,

  the reason is, it is useful to index on those constants for type class 
inference,
and not needlessly unfold them. In the stdlib this is used for type class 
inference related
to setoid rewriting, where one writes Proper _ f instances indexed by [f]. 
List requires
Setoid. Indexing could be finer grained though, e.g. class-based.
-- Matthieu

On 21 juin 2013, at 14:39, Gert Smolka 
<smolka AT ps.uni-saarland.de>
 wrote:

> Dear Matthieu, 
> 
> thanks for the explanation. I understand.
> 
> But there is an obvious next question: Why are "not" and "iff" made opaque 
> by List (and other standard modules)?
> 
> Gert
> 
> On Jun 21, 2013, at 11:43 , Matthieu Sozeau 
> <mattam AT mattam.org>
>  wrote:
> 
>> Dear Gert,
>> 
>> Actually, this is not a bug… Requiring List sets [not] as an opaque 
>> constant
>> for typeclass inference, hence it is no longer unfolded while searching
>> for a proof of [dec (~ X)], which fails. You can [Print HintDb 
>> typeclass_instances]
>> to see which definitions are considered opaque at any given point. 
>> Declaring [Typeclasses Transparent not.] after the import reverts that 
>> setting 
>> and resolution works as before.
>> 
>> Best,
>> -- Matthieu
>> 
>> Le 18 juin 2013 à 14:41, Gert Smolka 
>> <smolka AT ps.uni-saarland.de>
>>  a écrit :
>> 
>>> I stumbled across a very strange behavior of type class inference.
>>> 
>>> Definition dec (X : Prop) : Type := {X} + {~ X}.
>>> Definition decision (X : Prop) (D : dec X) : dec X := D.
>>> Arguments decision X {D}.
>>> Existing Class dec.
>>> 
>>> Instance False_dec :  dec False := 
>>> right (fun A => A).
>>> 
>>> Instance impl_dec (X Y : Prop) :  dec X -> dec Y -> dec (X -> Y).
>>> Proof. unfold dec ; tauto. Qed.
>>> 
>>> Set Printing Implicit.
>>> 
>>> Check (fun (X : Prop) (D : dec X) => decision (~ X)).
>>> 
>>> Require List.
>>> 
>>> Check (fun (X : Prop) (D : dec X) => decision (~ X)).
>>> 
>>> In the first Check the class argument is derived, in the second it is 
>>> not.  Both Checks are identical, the difference stems from requiring List 
>>> in between.
>>> 
>>> Is this  a bug or a feature?   Gert
>> 
>