Explicit Universal Quantification Bug?

[Rijk-Jan van Haaften]

Jay Cox wrote:
>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}
<...>
>so, is this a bug?

No, it is correct and expected behaviour, as I will explain below.

>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

Perfect example for explanation of the problem.
The difference is between
> >runTIM t = case t of {TIM l -> runST l}
and
> >runTIM t = runST (deTIM t)
> >deTIM (TIM t) = t

In the last one, after the type checker has verified
that deTIM is type-correct, it can safely generalize
the type of deTIM, because it is a top-level function.
This means that if we have
f :: a -> String
f x = "Hello, world"
we are allowed to apply f to an Int in one place, and to
an Char in another place:
g :: (String, String)
g = (f 3, f 'a')
This is common and well-known behaviour, and it's
possible to prove that this never gives problems.

However, in
> >runTIM t = case t of {TIM l -> runST l}
the argument 't' is non-generic.
If we have the function
g :: (a -> String) -> (String, String)
g f = (f 3, f 'a')
a problem appears. 'f' is used in a generic way, being
applied to arguments of different types, which is not
allowed because if we have
h = f (\x -> show (x + 1))
the second part of the tupel is undefined, though this
would be type-correct. This is clearly undesirable.
So we have to restrict f to be non-generic.

Consequently, types of variables which are derived
from it must be non-generic as well. In particular
this applies to 'l'. Thus, 'l' can't be generalized
to fit in the type of runST.

With this burden of information about generic and
non-generic, we can say in short:
> >runTIM t = case t of {TIM l -> runST l}
is wrong because l CANNOT be generalized to fit the type
of runST.
> >runTIM t = runST (deTIM t)
> >deTIM (TIM t) = t
is correct because deTIM CAN be generalized, so it
fits the type of runST

Rijk-Jan van Haaften