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.
I now retract this comment :). Clearly this is just as bad as saying:
f :: Bool -> b f x = x
since this claims that it will take a Bool and produce a value of type b for all types b. However, would it be all right to say (in pseudo-Haskell):
f :: exists b . Bool -> b f x = x
? Here, we're simply claiming that there is *some* type b for which f takes a Bool and produces a b? I believe this same analysis extends to something like:
class C a b | a -> b where {} instance C Int Int where {} f :: exists b . C Int b => Int -> b f i = i
It seems that this would be legal in a language like haskell but which allowed existensial quantification. Am I correct?