Lennart Augustsson <[EMAIL PROTECTED]> wrote: > A somewhat similar problem exists even without fields: > > 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. Here is (approximately) the Core translation of foo above: > foo :: forall a b. Either a b -> Either () b > foo = /\ a b -> \ e -> case e of > Left _ -> Left @() @b () > Right _ -> e You call this as (foo @a @b e), where e has type (Either a b). So, the call (foo @a @b (Right @a @b x)) reduces (ignoring types) to (Right @a @b x). This reduces a term of type (Either () b) to one of type (Either a b). That's not type safe. Jon Cast _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe