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.

Answer 2

As I understand it, a "Skolem variable" is a variable which does not match any other variable, including itself.

This seems to pop up in Haskell when you use features like explicit foralls, GADTs, and other type system extensions.

For example, consider the following type:

data AnyWidget = forall x. Widget x => AnyWidget x

What this says is that you can take any type that implements the Widget class, and wrap it into an AnyWidget type. Now, suppose you try to unwrap this:

unwrap (AnyWidget w) = w

Um, no, you can't do that. Because, at compile-time, we have no idea what type w has, so there's no way to write a correct type signature for this. Here the type of w has "escaped" from AnyWidget, which is not allowed.

As I understand it, internally GHC gives w a type which is a Skolem variable, to represent the fact that it must not escape. (This is not the only such scenario; there's a couple of other places where a certain value cannot escape due to typing issues.)

Answer 3

The error message pops up when a type variable tries to escape its scope.

It took me a while to figure out this, so I'll write an example.

{-# LANGUAGE ExistentialQuantification #-}
data I a = I a deriving (Show)
data SomeI = forall a. MkSomeI (I a)

Then if we try to write a function

 unI (MkSomeI i) = i

GHC refuses to type-infer/type-check this function.

---

Why? Let's try to infer the type ourselves:

• unI is a lambda definition, so it's type is x -> y for some types x and y.
• MkSomeI has a type forall a. I a -> SomeI
  • MkSomeI i has a type SomeI
  • i on the LHS has a type I z for some type z. Because of forall quantifier, we had to introduce new (fresh) type variable. Note, that it's not universal, as it's bound inside (SomeI i) expression.
  • thus we can unify type variable x with SomeI, this is ok. So the unI should have type SomeI -> y.
• i on the RHS thus have type I z too.
• At this point unifier tries to unify y and I z, but it notices that z is introduced in the lower context. Thus it fails.

Otherwise the type for unI would have type forall z. SomeI -> I z, but the correct one is exists z. SomeI -> I z. Yet that one GHC cannot represent directly.

---

Similarly, we can see why

data AnyEq = forall a. Eq a => AE a
-- reflexive :: AnyEq -> Bool
reflexive (AE x) = x == x

works.

The (existential) variable inside AE x doesn't escape into outer scope, so everything is ok.

---

Also I encountered a "feature" in GHC 7.8.4 and 7.10.1 where RankNTypes on itself is ok, but adding GADTs triggers the error

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE GADTs #-}

example :: String -> I a -> String
example str x = withContext x s
  where
    s i = "Foo" ++ str

withContext :: I a -> (forall b. I b -> c) -> c
withContext x f = f x

So it might be nothing wrong with your code. It might be GHC, which cannot figure everything out consistently.

EDIT: The solution is to give a type to s :: forall a. I a -> String.

GADTs turn on MonoLocalBinds, which makes inferred type of s to have skolem variable, so the type is not forall a. I a -> String, but t -> String, were t gets bound in the wrong context. See: https://ghc.haskell.org/trac/ghc/ticket/10644

Answer 4

Whats a Skolem?

An Existentially Quantified variable, IE it "has a rigid/concrete type, that the outside world cannot know, but the inside world can".

So how do you use Skolems?

TL;DR

unwrapBroken (ExistentiallyTyped x) = x

unwrapOk (ExistentiallyTyped x) = useConstraint x

---

Skolems are useful when they have some Instance of a Typeclass you care about. You can (only?) use the unwrapped thing via it's constraints.

So to be succinct, here's the skolem (that a within forall a. ExistentiallyTyped a) escaping:

data ExistentiallyTyped = forall a. SomeConstraint a => ExistentiallyTyped a

unwrapBroken :: forall a. ExistentiallyTyped -> a  <---- what? how'd that `a` break out? not the same `a` as in ExistentiallyTyped
unwrapBroken (ExistentiallyTyped x) = x :: a  <---- not the same `a` as above!

You can't do that, that a from x :: a is quantified within the ExistentiallyTyped wrapping, but think about the a on the line unwrapBroken :: forall a. .... Now it's somewhow Universally quantified?! (caveat, i think this starts to become possible with Dependent Types, which haskell doesn't have... yet). So you're tellin me this function can return Int or String or AnyFrigginThing?

No. But you can make use of that x :: a via its constraint:

unwrapOk :: ExistentiallyTyped -> ResultOfUseConstraint
unwrapOk (ExistentiallyTyped x) = useConstraint x

So for instance, I've made use of this when I wanted to have a list of types that shared some typeclass:

notPossible :: HasBork a => [Proxy a]
notPossible = [Proxy @Thing1, Proxy @Thing2]
-- Error! expected a `Proxy a` but got a `Proxy Thing1`

so instead:

data Borkable = forall a. HasBork a => Borkable a

borks :: [Borkable]
borks = [thing1, thing2]

later = useBork <$> borks