[Haskell-cafe] translation between two flavors of lexically-scoped type variables

[oleg at okmij.org]

> Do you know why they switched over in GHC 6.6?

If I were to speculate, I'd say it is related to GADTs. Before GADTs,
we can keep conflating quantified type variables with schematic type
variables. GADTs seem to force us to make the distinction.

Consider this code:

data G a where
    GI :: Int  -> G Int
    GB :: Bool -> G Bool


evG :: G a -> a
evG (GI x) = x
evG (GB x) = x

To type check the first clause of evG, we assume the equality 
(a ~ Int) for the duration of type checking the clause. To type-check the
second clause, we assume the equality (a ~ Bool) for the clause. We
sort of assumed that a is universally quantified, so we may indeed
think that it could reasonably be an Int or a Bool. Now consider that
evG above was actually a part of a larger function


foo = ...
 where
  evG :: G a -> a
  evG (GI x) = x
  evG (GB x) = x

  bar x = ... x :: Int ... x::a ...

We were happily typechecking evG thinking that a is universally
quantified when in fact it wasn't. And some later in the code it is
revealed that a is actually an Int. Now, one of our assumptions,
a ~ Bool (which we used to typecheck the second clause of evG) no
longer makes sense.

One can say that logically, from the point of view of _material
implication_, this is not a big deal. If a is Int, the GB clause of evG
can never be executed. So, there is no problem here. This argument
is akin to saying that in the code
	let x = any garbage in 1
any garbage will never be evaluated, so we just let it to be garbage.
People don't buy this argument. For the same reason, GHC refuses to type
check the following

evG1 :: G Int -> Int
evG1 (GI x) = x
evG1 (GB x) = x


Thus, modular type checking of GADTs requires us to differentiate
between schematic variables (which are akin to `logical' variables,
free at one time and bound some time later) and quantified variables,
which GHC calls `rigid' variables, which can't become bound (within
the scope of the quantifier). For simplicity, GHC just banned
schematic variables.

The same story is now played in OCaml, only banning of the old type
variables was out of the question to avoid breaking a lot of code.
GADTs forced the introduction of rigid variables, which are
syntactically distinguished from the old, schematic type variables. 
We thus have two type variables: schematic 'a and rigid a
(the latter unfortunately look exactly like type constants, but they
are bound by the `type' keyword). There are interesting and sometimes
confusing interactions between the two. OCaml 4 will be released any
hour now. It is interesting to see how the interaction of the two type
variables plays out in practice.