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