FDs and confluence

[Ross Paterson]

On Mon, Apr 10, 2006 at 05:49:15PM +0800, Martin Sulzmann wrote:
> Ross Paterson writes:
>  > 1) consider the two constraint sets equivalent, since they describe
>  >    the same set of ground instances, or
> 
> That's troublesome for (complete) type inference.
> Two constraint stores are equivalent if they are equivalent
> for any satisfying ground instance? How to check that?

You can't check it; it has to be proven for the system.

> I'm not following you here, you're saying?
> 
> rule C [a] b d ==> d=Bool

That's right.

> Are you sure that you're not introducing further "critical pairs"?

I don't see how -- there are no new redexes.  Instance improvement was
already applicable, but now it has a different output.

> Maybe, you found a "simple" solution (that would be great)
> but I'not 100% convinced yet.
> 
> The problem you're addressing only arises for non-full FDs.
> Aren't such cases very rare in practice?

My aim is not coverage but simplicity of description, and this version
still isn't simple enough.