One should keep in mind the distinction between schematic variables (which participate in unification) and universally quantified variables. Let's look at the forall-elimination rule G |- e : forall a. A -------------------- E G |- e : A[a := t] If the term e has the type forall a. A, we can use the term at some specific type t. Often the type checker doesn't know which specific type t to choose. Therefore, the type checker inserts a schematic type variable X (think of Prolog logic variable), to defer the decision. Further down the type-checking road, more information becomes available and it will become clear what concrete type t to use. Like in Prolog, a logic variable denotes a guess, or a promise, to be forced later (there is a deep connection between laziness and logic variables). So, the forall-elimination rule becomes G |- e : forall a. A -------------------- E G |- e : A[a := X] Let's look at the forall-introduction rule G |- e : A [a := aeigen] -------------------- I where aeigen \not\in G G |- e : forall a. A To type-check that a term e has a polymorphic type (which happens when the user gave a type signatures which contains type variables, implicitly quantified), the type-checker generates a fresh, unique _constant_ (called eigenvariable) and type-checks the term with the constant substituted for the type variable. If the term type-checks, it does have the polymorphic type. (One may ask why this fresh constant is called eigen_variable_ if it doesn't actually vary. That is a very good question, answered in http://okmij.org/ftp/formalizations/inductive-definitions.html#eigenvariable... ). GHC calls these eigenvariable rigid variables. The upshot: eigenvariabes are constants and can't be changed by unification. Schematic variables are variables and can be substituted by unification. Quantified type variables are replaced by schematic variables when _using_ a polymorphic term. Quantified type variables are replaced by constants (or, rigid variables) when _type-checking_ a term. The earlier example: f :: a -> a f x = x :: a can be alpha-converted [recall, ScopedTypeVariable extension is off] as f :: a -> a f x = x :: b First the type-checker generates beigen. To check if 'f' can indeed be given the type signature a -> a, GHC generates the eigenvariable aeigen and type-checks (\x::aeigen -> x :: beigen) :: aeigen The problem becomes obvious. The error message is very precise, describing the precise location where type variables are bound. Couldn't match type `a' with `b' `a' is a rigid type variable bound by the type signature for f :: a -> a at /tmp/e.hs:2:1 `b' is a rigid type variable bound by an expression type signature: b at /tmp/e.hs:2:7 In the expression: x :: b In an equation for `f': f x = x :: b Again, read `rigid type variable' as eigen-variable. In OCaml, type variables are schematic variables (in many contexts). For example: # let f1 (x:'a) = (x:'b);; val f1 : 'a -> 'a = <fun> # let f2 (x:'a) = x + 1;; val f2 : int -> int = <fun> The function f2 is not polymorphic at all, although it may appear so from the use of the type variable 'a. But in other contexts OCaml does work like GHC: # module F : sig val f5 : 'a -> 'a end = struct let f5 x = x + 1 end;; Error: Signature mismatch: Modules do not match: sig val f5 : int -> int end is not included in sig val f5 : 'a -> 'a end Values do not match: val f5 : int -> int is not included in val f5 : 'a -> 'a Further, OCaml has now a specific construct to introduce rigid type variables (which appear as type constants). # let f4 (type a) (x:a) = (x:a) + 1;; Characters 25-26: let f4 (type a) (x:a) = (x:a) + 1;; ^ Error: This expression has type a but an expression was expected of type int