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.