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
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
