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.