Hi Tom, It seems we are thinking of different things. I was referring to the characterization of a type of the form P => t as being "ambiguous" if there is a type variable in P that is not determined by the variables in t; this condition is used in Haskell to establish coherence (i.e., to show that a program has a well-defined semantics). I don't know if you have defined/studied corresponding notions of ambiguity/coherence in your framework. Instead, I was referring to what Manuel described as "the equivalent problem using FDs": class IdC a b | a -> b instance IdC Int Int bar :: IdC a b => b -> b bar = id bar' :: IdC a b => b -> b bar' = bar In this program, both bar and bar' have ambiguous types (the variable 'a' in each of the contexts is not uniquely determined by the variable 'b' appearing on the right), and so *neither* one of these definitions is valid. This behavior differs from what has been described for your approach, so perhaps Manuel's example isn't really "equivalent" after all. Technically, one could ignore the ambiguous type signature for bar, because the *principal* type of bar (as opposed to the *declared type*) is not ambiguous. However, in practice, there is little reason to allow the definition of a function with an ambiguous type because such functions cannot be used in practice: the ambiguity that is introduced in the type of bar will propagate to any other function that calls it, either directly or indirectly. For this reason, it makes sense to report the ambiguity at the point where bar is defined, instead of deferring that error to places where it is used, like the definition of bar'. (The latter is what I mean by "delayed" ambiguity checking.) Hope that helps, Mark Tom Schrijvers wrote:
On Mon, 7 Apr 2008, Mark P Jones wrote:
The surprising thing about this example is the fact that the definition of foo is accepted, and not the fact that the definition of foo' is rejected. At least in Manuel's "equivalent" program using functional dependencies, both functions have ambiguous types, and hence both would be rejected. It sounds like your implementation may be using a relaxed approach to ambiguity checking that delays ambiguity checking from the point of definition to the point of use. Although this is probably still sound, it can lead to puzzling error diagnostics ...
On the algorithmic level I don't see a relaxed approach to ambiguity checking.
If alpha is a unifiction variable, you get for the first body
(Id a -> Id a) ~ (alpha ~ alpha)
where there is no ambiguity: the unique solution (modulo equality theory) is alpha := Id a.
For the second body you get
(Id a -> Id a) ~ (Id alpha -> Id alhpa)
This equation reduces to Id a ~ Id alpha. Our algorithm stops here. There is in general no single solution for alpha (*) in such an equation, as opposed to the above case.
I hope this clarifies our algorithm.
Cheers,
Tom