The Coq mailing list

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

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