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

oleg at okmij.org oleg at okmij.org
Wed Jan 4 14:48:14 CET 2012

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