A universally quantified or "polymorphic" type has the form forall v1 v2 vn. t, where t is a type. The type t may involve the variables v1 through vn.
The symbol ∀ is an alias for forall.
A type like forall x. F x can be written simply as F x (the forall x is implied) as long as x is free in F x (it is not bound by an outer scope; see Scoped type variables below).
A polymorphic type may be instantiated at any given type. For example, the empty list [] has type forall x. [x]. So it's a type-polymorphic value. Its type can be instantiated at Int, for example, which binds x to Int resulting in [Int] which is also a valid type for the empty list. In fact, we can say that the empty list [] is a value of type [x] for all choices of element type e, hence the type forall x. [x].
Likewise the identity function (x -> x), which simply returns its argument, has a polymorphic type forall t. t -> t. It has type t -> t for all choices of t.