Daniel Brown <[EMAIL PROTECTED]> wrote: > Jonathan Cast wrote: > > Lennart Augustsson <[EMAIL PROTECTED]> 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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe