Non-H98 crusade, contd.

[Ross Paterson]

On Mon, Feb 28, 2005 at 12:40:42PM +0000, Keean Schupke wrote:
> Ross Paterson wrote:
> 
> >Where can I read this understanding?  The GHC docs on FDs are terse,
> >referring to the original paper, but that paper is somewhat informal,
> >and describes a weaker system than what is implemented.  For example,
> >(taken from s7 of the paper), given
> >
> >	class U a b | a -> b where u :: a -> b
> >	class U a b => V a b where v :: a -> b
> >
> >the paper says that the principal type of \x -> (u x, v x) is
> >
> >	(U a b, V a c) => a -> (b,c)
> >
> >According to GHC and Hugs, it is
> >
> >	V a b => a -> (b,b)
> >
> >I think that's sensible, but where are the rules that give it?
> >I suspect that writing this addendum may take a while.
> >
> Thats just a type simplification, in the source, we have
> 
> \x -> (u x, v x)
> 
> the type checker knows both x's are the same, and it knows
> that (V a b) is the same as (U a b)...
> 
> So in this case it looks like the second type is just a simplification
> of the first... so they really agree on the type, not disagree.

No, the paper is clear on this point:
"For example, given two predicates U a b and V a c, nothing in the rules
from Section 6 will allow us to infer that b = c."

I agree that they should be identified, but the type system that does
it isn't written down anywhere (outside of the GHC and Hugs sources,
and the Hugs version has a number of bugs).