Explicit Universal Quantification Bug?

[John Hughes]

    | I'm trying to learn more about Explicit Universal 
    | Quantification so I decide to run the following supposedly 
    | correct code from the ghc user
    | guide:
    | 
    | >module Dummy where
    | >
    | >import ST
    | >
    | >newtype TIM s a = TIM (ST s (Maybe a))
    | >
    | >runTIM :: (forall s. TIM s a) -> Maybe a
    | >runTIM t = case t of {TIM l -> runST l}

Just to explain this a little more, the problem with the above is not the
type of t (which is generic, as the type signature says), it's the type of
l. The type of t is instantiated at the "case t of ...", let's say to 
TIM s' a, and the type of l is thus ST s' (Maybe a), which is NOT generic.
Hence l cannot be passed to runST. The type of l cannot be generalised at the
occurrence in runST l, because the type variable s' appears in the environment
at that point (in the type of l itself).
    
    As you discovered, the correct way to say it is

      runTIM t = runST (case t of {TIM l -> l})

In this case, the (generic) type of t is instantiated as before, and the
entire case expression has type ST s' (Maybe a). But this time l is not 
in scope (outside the case), and so the type variable s' can be generalised.
Hence the case can be passed to runST.
    
Here's another variation for you:
    
    runTIM :: (forall s. TIM s a) -> Maybe a
    runTIM t = let TIM l = t in runST l

This one is OK, because a let binding generalises the type of the bound
variable. Thus l is given the type forall s'. ST s' (Maybe a), and the
call of runST types.

Thus the problem with the first form above is just that a case binding doesn't
generalise the types of the bound variables. As far as I know, there's no
reason why it shouldn't, but that's just the way Haskell is. It's a pain, but
there we are.

John Hughes