[Haskell-beginners] Errors involving rigid skolem types

[Brent Yorgey]

On Mon, Aug 27, 2012 at 11:21:55PM +1000, Matthew Moppett wrote:
> 
> This yields a kind of error message that I've often bashed my head against
> in other code I've written, without ever really understanding what the
> problem is exactly:
> 
> Couldn't match type `a0' with `a1'
>       because type variable `a1' would escape its scope
>     This (rigid, skolem) type variable is bound by
>       an expression type signature: (a1, a1)
>     The following variables have types that mention a0
>       x' :: a0 (bound at Cycle.hs:12:15)
>     In the expression: (x', maxBound) :: (a, a)
>     In a pattern binding: (x, max) = (x', maxBound) :: (a, a)
>     In an equation for `toEnum':
>         toEnum n
>           = Cyc x
>           where
>               (x, max) = (x', maxBound) :: (a, a)
>               x' = toEnum $ n `mod` ((fromEnum max) - 1)
> 
> The problem comes up when I'm trying to give hints to the compiler about
> the type that a particular expression should have.
> 
> My questions are: (1) what exactly is going on here, and (2) is there any
> general technique for specifying types in situations like this that gets
> around this problem?

What is going on here is that the occurrences of 'a' in (x', maxBound)
:: (a,a) are not the same as the occurrences of 'a' in the instance
head.  You might as well have written (x', maxBound) :: (b,b) or ::
(foo,foo).  The idea is that by default, any type with type variables
is generalized to a forall type, so what you really have is

  (x', maxBound) :: forall a. (a,a)

which makes it easier to see why those a's have nothing to do with
those in the instance head.  You don't want x' and maxBound to have
*any* type, you want them to have whatever *particular* type
corresponds to the chosen instance.

The solution is to use an extension called ScopedTypeVariables which
lets you connect type variables across different signatures in exactly
this way.  In this case, simply turning on the extension by putting

  {-# LANGUAGE ScopedTypeVariables #-}

at the top of your file is enough to get the program to compile.  Now
the 'a's in your local type annotation really do refer back to the 'a'
in the instance head.  In general, if you want to have a local type
variable refer to a top-level type signature (as opposed to an
instance head) you also have to put an explicit 'forall' on the
variables you want to be scoped in this way, like

  {-# LANGUAGE ScopedTypeVariables #-}
  foo :: forall a. a -> a -> a
  foo = ...
    where bar = ... :: a -> Int

note the 'forall a' in the top-level signature for foo.

-Brent