inconsistent type checking behavior

[Brandon S. Allbery KF8NH]

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 at kf8nh.com
system administrator [openafs,heimdal,too many hats] allbery at ece.cmu.edu
electrical and computer engineering, carnegie mellon university    KF8NH


-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20081112/6b1e878d/attachment-0001.htm