haskell - What are skolems?

Question

Eeek! GHCi found Skolems in my code!

...
Couldn't match type `k0' with `b'
  because type variable `b' would escape its scope
This (rigid, skolem) type variable is bound by
  the type signature for
    groupBy :: Ord b => (a -> b) -> Set a -> Set (b, [a])
The following variables have types that mention k0
...

What are they? What do they want with my program? And why are they trying to escape (the ungrateful little blighters)?

Answer 1

To start with, a "rigid" type variable in a context means a type variable bound by a quantifier outside that context, which thus can't be unified with other type variables.

This works a great deal like variables bound by a lambda: Given a lambda (x -> ... ), from the "outside" you can apply it to whatever value you like, of course; but on the inside, you can't simply decide that the value of x should be some particular value. Picking a value for x inside the lambda should sound pretty silly, but that's what errors about "can't match blah blah, rigid type variable, blah blah" mean.

Note that, even without using explicit forall quantifiers, any top-level type signature has an implicit forall for each type variable mentioned.

Of course, that's not the error you're getting. What an "escaped type variable" means is even sillier--it's like having a lambda (x -> ...) and trying to use specific values of x outside the lambda, independently of applying it to an argument. No, not applying the lambda to something and using the result value--I mean actually using the variable itself outside the scope where it's defined.

The reason this can happen with types (without seeming as obviously absurd as the example with a lambda) is because there are two notions of "type variables" floating around: During unification, you have "variables" representing undetermined types, which are then identified with other such variables via type inference. On the other hand, you have the quantified type variables described above which are specifically identified as ranging over possible types.

Consider the type of the lambda expression (x -> x). Starting from a completely undetermined type a, we see it takes one argument and narrow that to a -> b, then we see that it must return something of the same type as its argument, so we narrow it further to a -> a. But now it works for any type a you might want, so we give it a quantifier (forall a. a -> a).

So, an escaped type variable occurs when you have a type bound by a quantifier that GHC infers should be unified with an undetermined type outside the scope of that quantifier.

---

So apparently I forgot to actually explain the term "skolem type variable" here, heh. As mentioned in comments, in our case it's essentially synonymous with "rigid type variable", so the above still explains the idea.

I'm not entirely sure where the term originated from, but I would guess it involves Skolem normal form and representing existential quantification in terms of universal, as is done in GHC. A skolem (or rigid) type variable is one that, within some scope, has an unknown-but-specific type for some reason--being part of a polymorphic type, coming from an existential data type, &c.