Arjen, Indeed, I think the fundamental point of disagreement is whether t ~ String is a valid potential unification or not. In general it is, but let me bring to you the following example that I put on the initial example on my Stack Overflow question: aretheyreallyeq :: (Eq a, Eq b) => Either a b -> Either a b -> Bool aretheyreallyeq (Left a1) (Right b2) = a1 == b2 This does not compile, and rightly so. Because a and b *need not* be equal, so it is not guaranteed that you will be able to use an Eq instance between them. In other words, within a function body, type variables in the definition of that function are not unifiable, they cannot be instantiated (within the function's body). There cannot be parts of the function's body whose potential outcome depends on what the type variables are instantiated to. Of course, and as the error message on my first example says itself, the thing is that it *depends on the instantiation of t*. But here is the thing, and please evaluate this statement carefully as, if not entirely correct, it might be the entire source of the confusion: A) There is no Class1 constraint on the function createBar. Therefore, the Class1 instance that the function uses is going to be fixed and will not vary on different calls of the function. Sure, that instance may rely on other constraints of the function, for example. If there were other instances whose head matched but did not have matching constraints we would be in a different situation, and I understand why in those cases the overlapping errors are necessary: it is undecidable in general to solve the problem of transitive constraint satisfaction and therefore if the head matches, it is a potential overlap and that's the end of the story. But that is not what happens here. The head of the constraint will only match if t ~ String, but then the Class1 instance used within createBar would need to be variable for different type instantiations of createBar, which contradicts the statement A). Thus, the only sensible thing to do is to use the only instance that matches regardless of the instantiation of t. And to circle back, as I said, this comes back to the fact that if you remove the instance that does not depend on the instantiation of t, then you suddenly get a compile error that says there are *no* instances. So the compiler itself knows that it cannot use an instance that depends on the instantiation of t, but still brings it up to flag an overlapping instances error. I hope that clarifies at the very least what the core of the disagreement is. It is quite possible that there is something I am overlooking, but until you provide me with an example of code that, if the compiler worked the way I want it to, would have an ambiguous instance, or an ambiguous implementation of some function at all, I'll still believe that the compiler is flagging up the overlapping instances error too soon without really checking whether they are really valid instances. Thanks, Juan. -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.