[Haskell-cafe] Solved but strange error in type inference

[oleg at okmij.org]

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#eigenvariables

). 
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