strange implicit type for eq_refl

Question

In Coq, propositions are types and proofs are values. For example we may write a simple proof like this, which proves 0=0.

Definition test : (eq 0 0) := eq_refl 0.

Interestingly, when checking the type of eq_refl, it shows

eq_refl
     : ?x = ?x
where
?A : [ |- Type] 
?x : [ |- ?A]

That means all the arguments of eq_refl are implicit. In Coq, implicit arguments are usually not allowed to determined explicitly, unless using @. To prove 0=0, we can write explicitly @eq_refl nat 0 or just eq_refl as nat and 0 can be deduced. But in the example at beginning, eq_refl 0 also works. Why?

This thing does not work in general, e.g.

Definition foobar {A : Type -> Type} {T : Type} :  list (A T) := [].
Definition test : list (list nat) := foobar.
Fail Definition test' : list (list nat) := foobar nat.

Answer 1

Implicit arguments structures of constants may sometimes rely on several Arguments directives, as can be seen in the file $COQLIB/theories/Init/Logic.v, lines 309 and 310, reproduced here:

Arguments eq {A} x _.
Arguments eq_refl {A x} , [A] x.

The use of the Arguments command is documented here, but I did not see it mentioned that several implicit arguments configuration are accepted.

On the other hand, the command Print Implicit eq_refl. returns precise information about the fact that two methods of understanding implicit arguments can be used, one when the functions receives 1 argument, and when the function receives 0 arguments.