Explicit Universal Quantification Bug?

24 Jan 2002

      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}
however when i try to actually compile it with ghc 5.02.1 it
gives this error

...
C:\exp>ghc -fglasgow-exts -package lang x.lhs
~
x.lhs:8:
    Inferred type is less polymorphic than expected
        Quantified type variable `s' escapes
        It unifies with `s1', which is mentioned in the environment
        The following variables in the environment mention `s1'
          l :: ST s1 (Maybe a)
    Signature type:     forall s. ST s a1
    Type to generalise: ST s1 (Maybe a)
    When checking an expression type signature
    In the first argument of `runST', namely `l'
    In a case alternative: runST l

C:\exp>
...

so, is this a bug?

I noticed also the following code compiles fine. (slightly modified
from a message on this list titled "Re: Type problem with ST monad"
dating April 23, 1999
...
module Dummy where
import ST
newtype TIM s a = TIM (ST s (Maybe a))
runTIM :: (forall s. TIM s a) -> Maybe a
runTIM t = runST (deTIM t)
deTIM (TIM t) = t
so, is using a pattern matching function the truly accepted way instead of
using the case statement mentioned in the docs?  Is the ghc manual
outdated?

Thanks

Jay Cox