[Haskell-cafe] type inference and named fields

[Jonathan Cast]

Daniel Brown <danb at cs.utexas.edu> wrote:
> 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?

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