Release plans
Doaitse Swierstra
doaitse at cs.uu.nl
Tue Apr 17 09:23:02 EDT 2007
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
>
More information about the Glasgow-haskell-users
mailing list