[Haskell-cafe] (Feeling that) GHCi is trying to protect me from myself with overlapping instances and existential types

[Juan Casanova]

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.