On Apr 17, 2007, at 2:57 PM, Simon Peyton-Jones wrote:
| Just to show what kind of problems we are currently facing. The | following type checks in our EHC compiler and in Hugs, but not in the | GHC: | | module Test where | | data T s = forall x. T (s -> (x -> s) -> (x, s, Int)) | | run :: (forall s . T s) -> Int | run ts = case ts of | T g -> let (x,_, b) = g x id | in b
And indeed it should be rejected!
If you think it should be rejected, can you give me the translation into System F + data types? I don't think there is one, and that's why GHC rejects it.
Yes, but where is it written that what cannot be expressed in system- F is type incorrect? We think it is still type safe, and it is an extrcat of a larger program that is quite useful (if we managed to compile it), Doaitse
Simon