I'm reading chapter 4 of the reference manual of Coq. According to the typing rules described by the reference, the type of term fun x: nat => x is forall x: nat, nat.
Assume that E is [nat: Set].
... ...
------------------------------ Prod-Set ------------------- Var
E[] ⊢ forall x: nat, nat : Set E[x: nat] ⊢ x : nat
------------------------------------------------------------ Lam
E[] ⊢ fun x: nat => x : forall x: nat, nat
However, when I Check this term by Coq, it is typed nat -> nat.
Welcome to Coq 8.5pl2 (July 2016)
Coq < Check fun x: nat => x.
fun x : nat => x
: nat -> nat
Are these two types same ones? If so, do arrows have hidden names of bound variables?
The actual type of fun x: nat => x is nat -> nat because their is no type dependency. The arrow is syntax sugar for forall _:nat, nat: the type of the body does not depend on the value of x, only the body itself is using x. An example of type dependency would be vector.
vector A n is the type of list of length n containing elements of type A. Let's consider the concat function which concatenate two vectors:
concat : forall n m: nat, vector n A -> vector m A -> vector (n + m) A
It takes as input two integers, n and m, two vectors of respective size n and m and concatenate them. This time, the type of concat depends on the value of n and m so you have to name them and use the forall instead of the ->. If you try to write nat -> nat -> vector n A -> ..., the variable n won't be correctly bounded.