Explicit Universal Quantification Bug?

[Janis Voigtlaender]

Rijk-Jan van Haaften wrote:
> ...
> 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.
> ...
> However, in
> > >runTIM t = case t of {TIM l -> runST l}
> the argument 't' is non-generic.

t is generic over s, since it has type (forall s. TIM s a).

> 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
> ...

This argument is not convincing, because you have simply given a wrong
type for g. Of course, it must be:

g :: (forall a . (a -> String)) -> (String, String)
g f = (f 3, f 'a')

> 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

I don't think it is a problem of "generalization only occurring at
top-level", or how would you then explain that the following compiles
just fine?

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

Regards, Janis.

--
Janis Voigtlaender
http://wwwtcs.inf.tu-dresden.de/~voigt/
mailto:voigt@tcs.inf.tu-dresden.de