The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

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