Hi Mark,
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.)
You are of course spot on, but this is a difference in how GHC handles functional dependencies compared to Hugs. Hugs does reject bar as being ambiguous, but GHC does not! In other words, it also uses "delayed" ambiguity checking for the FD version, and so raises an error only when seeing bar'. The implementation of type families just mirrors GHC's behaviour for FDs. (This is why I presented the FD example, but I should have mentioned that the equivalence is restricted to GHC.) The rational for the decision to use delayed ambiguity checking in GHC is that it is, in general, not possible to spot and report all ambiguous signatures and *only* those. So, there are three possible choices: (1) Reject all signatures that *may* be ambiguous (and hence reject some perfectly good programs). (2) Reject all signatures that are *guaranteed* to be ambiguous (and accept some programs with functions that can never be applied). (3) Don't check for ambiguity (or "delayed" ambiguity checking). As you wrote, all three choices are perfectly safe - we will never accept a type-incorrect program, but they vary in terms of the range of accepted programs and quality of error messages. Please correct me if I am wrong, but as I understand the situation, Hugs uses Choice (1) and GHC uses Choice (3). As an example, consider this contrived program:
class F a b | a -> b where f1 :: a -> b f2 :: b -> a
instance F Int Int where f1 = id f2 = id
class G x a b where g :: x -> a -> b
instance F a b => G Bool a b where g c v = f1 v
instance F b a => G Int a b where g c v = f2 v
foo1 :: (G Int a b) => a -> a foo1 v = v
foo2 :: (G Bool a b) => a -> a foo2 v = v
bar = foo2 (42::Int)
Here foo1 is actually ambiguous, but foo2 is fine due to the FD in the instance context of the (G Bool a b) instance. GHC accepts this program (not checking for ambiguity) and allows you to evaluate bar. In contrast, Hugs rejects both the signature of foo1 and of foo2, arguably being overly restrictive with foo2. Cheers, Manuel