[PRL] first-class polymorphic values

[Dave Herman]

I know that FX supported first-class polymorphic values, and O'Toole and 
Gifford have a PLDI'89 paper on supporting type inference in languages 
with polymorphic values. Does anyone know of other languages that have 
allowed first-class polymorphic values?

Also, I'm a little confused about alpha conversion of type variables. Do 
type systems with first-class polymorphic values or higher-rank 
polymorphism have to deal with alpha equality. For example, imagine a 
function that returns a polymorphic function:

     f :: forall a . a -> (forall b . (a,b))
     fun f = \x.\y.(x,y)

Now if I use this in a context that already has the type variable `b' 
bound, I have to alpha-convert the result type of `f' in order to 
express the result type:

     g :: forall b . [b] -> forall c . (b,c)
     g (x:_) = f x
     ...

Do type checkers for higher-rank polymorphism have to consider type 
equality up to alpha-equivalence of type names? Do inference algorithms 
for languages with higher-rank polymorphic types have to freshen type 
names when they synthesize polymorphic types?

One last question: is there a distinction between "first class 
polymorphic values" and "higher-rank polymorphism"?

Thanks,
Dave