The Coq mailing list

[Gert Smolka <smolka AT ps.uni-saarland.de>]

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
>