The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi Gert,

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
> 

  this is definitely a bug, I'm working on it.
-- Matthieu