[Haskell-cafe] type inference and named fields
danb at cs.utexas.edu
Fri Jun 24 10:39:50 EDT 2005
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`.
More information about the Haskell-Cafe