Hi Simon, all,
Here's a less complicated variant of the same problem:
class C a b | a -> b where {}
instance C Int Int where {}
f :: (C Int b) => Int -> b f x = x
This is interesting, but I'm not entirely sure what the problem is (from a theoretical, not practical, standpoint). Obviously there is no problem in a one module program, so let's assume we have the following modules: module C where class C a b | a -> b where {} module I1 where import C instance C Int Int where {} module I2 where import C instance C Int Bool where {} module U where import C import ? f :: C Int b => Int -> b f x = x Now, there are four cases: 1) U (transitively) imports I1 2) U (transitively) imports I2 3) U (transitively) imports both I1 and I2 4) U (transitively) imports neither I1 nor I2 Suppose we are in case 1. Then the programmer has written a too-general type signature on f. The programmer *must* know that b=Int in this case otherwise his function definition makes no sense. However, I don't really see a reason why this should be an error rather than just a warning. If some other module K imports both U and (for instance) I2, then we'll get a fundep clash and the whole program will be invalid. Suppose we are in case 2. Then the programmer has clearly screwed up because we know b=Bool and x::Int and x::Bool are incompatible. This should clearly be a type error. Case 3 is impossible, as this will be a fundep clash. Case 4 should produce an error (IMO). Of course, there could be a module K which imports this U and also I1 in which case you might argue that this should be allowed, but I don't think that makes much sense.
I suppose I could use (unsafeCoerce x) as the RHS, which amounts to saying "in every call to f, b will be Int, so we know that the coercion is safe". But that is a scarily global property. For example, if a call site of f does not "see" the instance declaration, it might call f with an argument of type (C Int Bool) or something. Nor can I see an easy way to insert the 'right' coercions in general.
Is this possible? In order for this to happen, this evil module M must import U. This means that it has transitively imported I1 and thus has the instance declaration. Or am I missing something. I think the unsafeCoerce x is safe in these cases.
Bottom line: excellent point, but I can't see how to fix it. Maybe there are some fundep experts out there who can guide us through the swamp?
Yes, please! - Hal