
17 Apr
2007
17 Apr
'07
12:57 p.m.
| 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. Simon