| 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