On 2008 Nov 12, at 10:53, Jeff Polakow wrote:
Now, if we switch to an analogous, though slightly more complicated type, GHC's type checker accepts the following code:
bar :: (forall b. b -> String, Int) bar = (const "hi", 0) foo :: forall b.(b -> String, Int) foo = (const "hi", 0)
however GHC's type checker rejects the following code (I now think this is correct):
bar :: (forall b. b -> String, Int) bar = (const "hi", 0) foo :: forall b.(b -> String, Int) foo = bar
with the error :
Couldn't match expected type `b -> String' against inferred type `forall b1. b1 -> String'
and yet GHC accepts the following code:
bar :: (forall b. b -> String, Int) bar = (const "hi", 0) foo :: forall b.(b -> String, Int) foo = (fst bar, snd bar)
which is just the eta-expansion of the previous code.
This behavior seems inconsistent to me. I don't see any reason why the (f = b) should be different than (foo = bar). In fact, thinking more carefully about the types, I think that (f = b) should not type and the eta expansion (f = \x -> b x) should be required.
Seems right to me: symbolically it may be an eta-expansion, but practically GHC's tuples are actually types, so the latter is a new tuple with a different type from the former. (GHC's handling of tuples is often infelicitous.) -- brandon s. allbery [solaris,freebsd,perl,pugs,haskell] allbery@kf8nh.com system administrator [openafs,heimdal,too many hats] allbery@ece.cmu.edu electrical and computer engineering, carnegie mellon university KF8NH