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

[leesteken at pm.me]

‐‐‐‐‐‐‐ Original Message ‐‐‐‐‐‐‐
On Sunday, February 16, 2020 3:44 PM, Juan Casanova <juan.casanova at ed.ac.uk> wrote:

> 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.

The type 't' will be determined by the calling context of createBar, and I do not see why it could not be String.

> 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.

My apologies, I expected the compiler to complain about overlapping instances, even without anything other than the instance definitions. It turns out that it only starts complaining when the instances are used. I'm afraid it would appear that I don't really know how multiple-parameter classes and existential types influence the overlap checking as implemented in GHC.

> 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.

I would expect that the type checker, when it cannot prove something in general, takes the safe approach of disallowing it. Whether your particular use of this class in your program might be proven to be correct, I really don't know, sorry.

> 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.
>

kind regards, Arjen