How does this constitute a Haskell rigid type error?

Question

This works:

data Wrapped a = Wrapped a

alpha :: IO s -> IO ()
alpha x = do
    rv <- wrapit x
    return ()
    where       
        wrapit :: IO s -> IO (Wrapped s)
        wrapit x' = do 
            a <- x'
            return (Wrapped a)

This doesn't:

data Wrapped a = Wrapped a

alpha :: IO s -> IO ()
alpha x = do
    rv <- wrapit
    return ()
    where       
        wrapit :: IO (Wrapped s)
        wrapit = do 
            a <- x
            return (Wrapped a)

Why?

Answer 1

This is due to the way in which type variables are scoped and quantified in standard Haskell. You can make the second version work like so:

{-# LANGUAGE RankNTypes, ScopedTypeVariables #-}

module RigidProblem where

data Wrapped a = Wrapped a

alpha :: forall s. IO s -> IO ()                                                
alpha x = do
    rv <- wrapit
    return ()
    where       
        wrapit :: IO (Wrapped s)
        wrapit = do 
            a <- x
            return (Wrapped a)

There are two changes: the RankNTypes and ScopedTypeVariables language extensions are enabled and the explicit forall s is added in the type signature of alpha. The first of the two extensions is what allows us to introduce the explicit forall s thus bringing the s into scope inside the body of alpha, whereas the second makes it so that the signature on wrapit is not taken by the type inference engine to contain an implicit forall s -- instead, the s in that signature is taken to name a type variable which should be in scope and is identified with it.

The current default situation in Haskell, if I understand correctly, is that all rigid type variables (meaning type variables occurring in type signatures explicitly provided by the programmer) are implicitly quantified and not lexically scoped, so that there is no way to refer to a rigid type variable from an outer scope in an explicit signature provided in an inner scope... (Oh bother, I'm sure someone could phrase it better than this.) Anyway, from the type checker's point of view, the s in alpha's signature and the one in wrapit's signature are totally unrelated and cannot be unified -- thus the error.

See this page from the GHC docs and this page from Haskell Prime wiki for more information.

Update: I just realised that I never explained why the first version works. For the sake of completeness: note that with the first version, you could use t in place of s in wrapit's signature and nothing would change. You could even take wrapit out of the where block and make it a separate top level function. The key point is that it is a polymorphic function, so that the type of wrapit x is determined by the type of x. No relation of the type variable used in the first version wrapit's signature to that used in alpha's signature would be of any use here. With the second version this is of course different and you have to resort to the above mentioned trickery to make wrapit's s be the same thing as alpha's s.