Why does binding to an "unrestricted" type variable make a variable rigid?

Question

I have this function to generate a list of random values and get the generator back (if anyone knows a better way, feel free to leave it in the comments):

-- randomN :: (Random a, RandomGen g) => g -> Int -> ([a], g)
randomN gen n = (map fst rs, snd (last rs)) where
    rs = take n (pool gen)
    pool g = (r, g'):(pool g') where (r, g') = random g

I want to use it to shuffle lists. I created this function:

shuffle gen stuff = (map snd $ sortOn fst $ zip rs stuff, gen') where
    rs :: [Int]
    (rs, gen') = randomN gen (length stuff)

I understand that I need to explicitly instantiate rs, GHC will not magically figure how I want to sort the list.

Here is the question: my original attempt looked like this:

shuffle gen stuff = (map snd $ sortOn fst $ zip rs stuff, gen') where
    (rs, gen') = randomN gen (length stuff) :: ([Int], g)

But that failed with the following error:

shuffle_minimal.hs:11:18: error:
    • Couldn't match type ‘t1’ with ‘g’
        because type variable ‘g’ would escape its scope
      This (rigid, skolem) type variable is bound by
        an expression type signature:
          ([Int], g)
        at shuffle_minimal.hs:11:18-57
      Expected type: ([Int], g)
        Actual type: ([Int], t1)
    • In the expression: randomN gen (length stuff) :: ([Int], g)
      In a pattern binding:
        (rs, gen') = randomN gen (length stuff) :: ([Int], g)
      In an equation for ‘shuffle’:
          shuffle gen stuff
            = (map snd $ sortOn fst $ zip rs stuff, gen')
            where
                (rs, gen') = randomN gen (length stuff) :: ([Int], g)
    • Relevant bindings include
        gen :: t1 (bound at shuffle_minimal.hs:10:9)
        shuffle :: t1 -> [b] -> ([b], t) (bound at shuffle_minimal.hs:10:1)

If the type variable is something as general as "g", how come the compiler is not able to match it with whatever other type?

What does "because type variable ‘g’ would escape its scope"? I have tried reading some other post but I do not really understand it :-(

Thanks!

score 4 · Accepted Answer · edited Dec 17 '17 at 22:12

Because it's not the same g.

The inferred type of shuffle in your definition looks like this:

 shuffle :: (RandomGen t1) => t1 -> [a] -> [a]
 shuffle gen stuff = ...
      where 
          (res, gen') = ... :: (Int, g)

The type of generator in the shuffle type signature t1 and the type of generator in the gen' signature g are different types from the compiler's point of view. There is nothing in your code to say that they are the same type. So the compiler complains.

The first obvious solution would be to give them the same name explicitly:

 shuffle :: (RandomGen g) => g -> [a] -> [a]
 shuffle gen stuff = ...
      where 
          (res, gen') = ... :: (Int, g)

However, that will not work either. Due to some complicated historic reasons, even when declared like that, the two g types will still not be considered the same type.

Yes, this is frustrating. So modern GHC offers a couple of handy extensions to fix it: ExplicitForAll and ScopedTypeVariables (enabling the latter automatically enables the former).

With these extensions enabled, you can amend your function like this:

 shuffle :: forall g a. (RandomGen g) => g -> [a] -> [a]
 shuffle gen stuff = ...
      where 
          (res, gen') = ... :: (Int, g)

The forall in the signature (enabled by the ExplicitForAll extension) is important: it opens a new scope for type variables and says that the variables g and a are two fresh types in that scope. The scope size is the whole function body, and with ScopedTypeVariables enabled, any mention of these type variables in that scope will mean a reference to these same types, rather than a fresh type.

Also, it might be worth noting that `ScopedTypeVariables` enables `ExplicitForAll` automatically. — K. A. Buhr, Dec 17 '17 at 20:06

chi · Answer 2 · 2017-12-18T08:49:13.273

Here is the question: [...]

If the type variable is something as general as "g", how come the compiler is not able to match it with whatever other type?

First of all, note that providing a type annotation to shuffle would have prevented this error message. Indeed, this is why most Haskellers strongly recommend adding type annotations for all top-level bindings (at least).

Without an explicit type providing GHC with your intent, GHC has to guess -- using its inference engine to do so.

shuffle gen stuff = ...

What type is gen? GHC does not know that, so it generates a fresh type variable, t1, to represent its type. This variable is not rigid, meaning that later on GHC might choose to unify t1 with some other type. E.g. If your code contained gen == "hi" then GHC would unify t1 ~ String.

Later on we find

randomN gen (length stuff) :: ([Int], g)

which actually means

randomN gen (length stuff) :: forall g. ([Int], g)

meaning that such expression is of type ([Int], String) and ([Int], Bool) and ([Int], Whatever). The implicit universal quantification on g makes it stand for "any arbitrary type". Here g is rigid: GHC can't just pick only one type -- the signature demands all types!

However, the expression is of type ([Int], t1) since its second pair returns a new generator of the same type as gen. This would make t1 unify with g -- but this makes no sense! Indeed, t1 stands for a single type, and g stands for an "arbitrary" type: choosing t1 ~ g would implicitly fix g to a single type. Or in other words, we can't choose t1 to be "equal to all types g" -- it would be nonsense.

GHC prevents this wrong unification by comparing the scopes of g and t1: since the non-rigid t1 has a larger scope, it can't be unified with the rigid g.

I was under the impression that even providing a type signature wouldn't help without `ScopedTypeVariables` enabled, would it? — Fyodor Soikin, Dec 17 '17 at 20:04
@FyodorSoikin Correct. IMO, that extension should be on by default. However, even without that, writing a signature would provide a better error message, at least. — chi, Dec 17 '17 at 20:34
But then, even with the extension enabled, don't you need an explicit `forall` as well? As far as I understand, a type signature doesn't automatically create a new type scope, does it? — Fyodor Soikin, Dec 17 '17 at 20:49
I think I am missing something. Adding `ScopedTypeVariables` and the type signature shuffle ::(RandomGen g) => g -> [a] -> ([a], g) still does not work. Thanks for the explanation though! EDIT: I read now @FyodorSoikin 's reply, that includes the explicit forall that fixes the whole thing. — Sergio Losilla, Dec 17 '17 at 21:10
@FyodorSoikin Yes, you need that, otherwise the extension has no effect. — chi, Dec 18 '17 at 08:47

Why does binding to an "unrestricted" type variable make a variable rigid?

2 Answers2