[Haskell-cafe] type inference and named fields

[Jonathan Cast]

Lennart Augustsson <lennart at augustsson.net> 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