[Haskell-cafe] type inference and named fields

[Daniel Brown]

Jonathan Cast wrote:
> Lennart Augustsson <lennart at augustsson.net> 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? In this case, that would let `x :: forall x. Either x 
b`, which unifies with `Either () b`.

  Dan