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