Re: [Haskell-cafe] type inference and named fields

Daniel Brown wrote:

Jonathan Cast wrote:

...

Lennart Augustsson wrote:

...

foo :: Either a b -> Either () b foo (Left _) = Left () foo x@(Right _) = x

Since Haskell type checking doesn't use the information gained by pattern matching to refine types we just have to accept that some perfectly safe programs don't type check.

Well, not perfectly safe. We already had this discussion (about []), but to say it again: the value bound by any pattern has some particular type. x above doesn't have type (Either a b) for arbitrary a and b, but rather (Either a b) for some specific a and b. Unless that specific a happens to be (), x doesn't have the correct type to be the rhs of foo. It would require a radical change to GHC (moving away from System F as a basis for the intermediate language Core) to implement a language in which this wasn't true.

I see that the argument to foo has type `Either a b` (unquantified), but why can't x, bound to the value that matches the pattern, have the type of the pattern?

Because it's bound to a value of the type of the argument, not of the type of the pattern. What about the function

bar :: alpha -> beta bar x = x

? The pattern here is x, and its type is (x :: forall tau. tau). But, I think it axiomatic that typing rules have to forbid functions like bar.

In this case, that would let `x :: forall x. Either x b`, which unifies with `Either () b`.

Jon Cast