
On Tue, Apr 17, 2007 at 12:50:48PM +0200, Doaitse Swierstra 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
Consider this additional code which also typechecks in Hugs: v :: forall s . T s v = T f f :: s -> ([s] -> s) -> ([s], s, Int) f v g = let x = [v] in (x, g x, 0) due to parametricity, run v can't depend on x or g x. Apparently id has type [x] -> x. Are EHC and Hugs supposed to support equirecursive types? Brandon

On Tue, Apr 17, 2007 at 11:39:03PM -0700, Brandon Michael Moore wrote:
On Tue, Apr 17, 2007 at 12:50:48PM +0200, Doaitse Swierstra 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
Consider this additional code which also typechecks in Hugs:
v :: forall s . T s v = T f
f :: s -> ([s] -> s) -> ([s], s, Int) f v g = let x = [v] in (x, g x, 0)
due to parametricity, run v can't depend on x or g x. Apparently id has type [x] -> x. Are EHC and Hugs supposed to support equirecursive types?
Brandon
Oops, this should have been a reply to the original thread in glasgow-haskell-users. Brandon
participants (1)
-
Brandon Michael Moore