inconsistent type checking behavior

[Jeff Polakow]

Hello,

Thinking about this more, I have changed my mind about what should type 
check, but I still think GHC's behavior is inconsistent...

> (Side-stepping your main point, rather, which I think Chris K answered 
> correctly)
> 
Chris explained that the types are not equivalent to GHC by showing a 
context for which GHC's type checker differentiates the two types. My 
point was that GHC is arguably wrong (but perhaps pragmatically correct). 
The example Chris used assumes predicative polymorphism, but GHC 
supposedly has impredicative polymorphism and under impredicative 
polymorphism, I don't think there is a Haskell context which can 
differentiate the two types. But this is a bit of a distraction from the 
point I am trying to make which is... 

GHC's type checker seems to have a bug or, at least, an infelicity. Here 
is a description of the strange behavior which led me to this conclusion.

Note that all of the following is in GHC  6.10.1 with 
-XImpredicativeTypes.

GHC's type checker accepts the following code:

    b :: String -> forall b. b -> Int
    b = \x y -> 0
    f :: forall b. String -> b -> Int
    f = \x y -> 0

GHC's also accepts the following code (I think this is wrong, see below):

    b :: String -> forall b. b -> Int
    b = \x y -> 0
    f :: forall b. String -> b -> Int
    f = b

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.

> This is a non-sequitur.
> 
On the contrary, this is the crux of the matter; derivations are type 
checking. To figure out what should type check we need to look at what is 
derivable.

> The fact that A |- B and B |- A does not make them the same type. It 
> makes them isomorphic types.
> 
True, the derivations are isomorphic, and in a language with explicit 
type-lambdas and type-applications, there would be two different but 
isomorphic terms for the two types. However, since Haskell leaves 
type-lambdas and type-applications implicit, the exact same Haskell term 
can have both types (as shown above). So it is not so crazy to think that 
(f = b) and (foo = bar) might type check. 

Furthermore, it is by looking at the typing derivation system that I've 
come the conclusion that (f = b) should not type check. In order to type 
check (f = b) we have to derive the following (assuming no explicit terms 
for type-lambdas and type-applications):

    b :: String -> forall a. a -> Int  |-  b :: forall b . String -> b -> 
Int

which can't be done, whereas

    b :: String -> forall a. a -> Int  |-  \x -> b x :: forall b . String 
-> b -> Int
 
can be derived.

-Jeff


---

This e-mail may contain confidential and/or privileged information. If you 
are not the intended recipient (or have received this e-mail in error) 
please notify the sender immediately and destroy this e-mail. Any 
unauthorized copying, disclosure or distribution of the material in this 
e-mail is strictly forbidden.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20081112/e5015f85/attachment.htm