First, kinds and polymorphic types are different things. You can have a HM type system where all types are of the same kind (*), you could also have a system without polymorphism but with complex kinds.
If a term M
is of type ∀a.t
, it means that for whatever type s
we can substitute s
for a
in t
(often written as t[a:=s]
and we'll have that M
is of type t[a:=s]
. This is somewhat similar to logic, where we can substitute any term for a universally quantified variable, but here we're dealing with types.
This is precisely what happens in Haskell, just that in Haskell you don't see the quantifiers. All type variables that appear in a type signature are implicitly quantified, just as if you had forall
in front of the type. For example, map
would have type
map :: forall a . forall b . (a -> b) -> [a] -> [b]
etc. Without this implicit universal quantification, type variables a
and b
would have to have some fixed meaning and map
wouldn't be polymorphic.
The HM algorithm distinguishes types (without quantifiers, monotypes) and type schemas (universaly quantified types, polytypes). It's important that at some places it uses type schemas (like in let
), but at other places only types are allowed. This makes the whole thing decidable.
I also suggest you to read the article about System F. It is a more complex system, which allows forall
anywhere in types (therefore everything there is just called type), but type inference/checking is undecidable. It can help you understand how forall
works. System F is described in depth in Girard, Lafont and Taylor, Proofs and Types.