Why context is not considered when selecting typeclass instance in Haskell?

Question

I understand that when having

instance (Foo a) => Bar a
instance (Xyy a) => Bar a

GHC doesn't consider the contexts, and the instances are reported as duplicate.

What is counterintuitive, that (I guess) after selecting an instance, it still needs to check if the context matches, and if not, discard the instance. So why not reverse the order, and discard instances with non-matching contexts, and proceed with the remaining set.

Would this be intractable in some way? I see how it could cause more constraint resolution work upfront, but just as there is UndecidableInstances / IncoherentInstances, couldn't there be a ConsiderInstanceContexts when "I know what I am doing"?

Answer 1

This breaks the open-world assumption. Assume:

class B1 a
class B2 a
class T a

If we allow constraints to disambiguate instances, we may write

instance B1 a => T a
instance B2 a => T a

And may write

instance B1 Int

Now, if I have

f :: T a => a

Then f :: Int works. But, the open world assumption says that, once something works, adding more instances cannot break it. Our new system doesn't obey:

instance B2 Int

will make f :: Int ambiguous. Which implementation of T should be used?

Another way to state this is that you've broken coherence. For typeclasses to be coherent means that there is only one way to satisfy a given constraint. In normal Haskell, a constraint c has only one implementation. Even with overlapping instances, coherence generally holds true. The idea is that instance T a and instance {-# OVERLAPPING #-} T Int do not break coherence, because GHC can't be tricked into using the former instance in a place where the latter would do. (You can trick it with orphans, but you shouldn't.) Coherence, at least to me, seems somewhat desirable. Typeclass usage is "hidden", in some sense, and it makes sense to enforce that it be unambiguous. You can also break coherence with IncoherentInstances and/or unsafeCoerce, but, y'know.

In a category theoretic way, the category Constraint is thin: there is at most one instance/arrow from one Constraint to another. We first construct two arrows a : () => B1 Int and b : () => B2 Int, and then we break thinness by adding new arrows x_Int : B1 Int => T Int, y_Int : B2 Int => T Int such that x_Int . a and y_Int . b are both arrows () => T Int that are not identical. Diamond problem, anyone?

Answer 2

This does not answer you question as to why this is the case. Note, however, that you can always define a newtype wrapper to disambiguate between the two instances:

newtype FooWrapper a = FooWrapper a
newtype XyyWrapper a = XyyWrapper a

instance (Foo a) => Bar (FooWrapper a)
instance (Xyy a) => Bar (XyyWrapper a)

This has the added advantage that by passing around either a FooWrapper or a XyyWrapper you explicitly control which of the two instances you'd like to use if your a happens to satisfy both.

Answer 3

Classes are a bit weird. The original idea (which still pretty much works) is a sort of syntactic sugar around what would otherwise be data statements. For example you can imagine:

data Num a = Num {plus :: a -> a -> a, ... , fromInt :: Integer -> a}
numInteger :: Num Integer
numInteger = Num (+) ... id

then you can write functions which have e.g. type:

test :: Num x -> x -> x -> x -> x
test lib a b c = a + b * (abs (c + b))
    where (+) = plus lib
          (*) = times lib
          abs = absoluteValue lib

So the idea is "we're going to automatically derive all of this library code." The question is, how do we find the library that we want? It's easy if we have a library of type Num Int, but how do we extend it to "constrained instances" based on functions of type:

fooLib :: Foo x -> Bar x
xyyLib :: Xyy x -> Bar x

The present solution in Haskell is to do a type-pattern-match on the output-types of those functions and propagate the inputs to the resulting declaration. But when there's two outputs of the same type, we would need a combinator which merges these into:

eitherLib :: Either (Foo x) (Xyy x) -> Bar x

and basically the problem is that there is no good constraint-combinator of this kind right now. That's your objection.

Well, that's true, but there are ways to achieve something morally similar in practice. Suppose we define some functions with types:

data F
data X
foobar'lib :: Foo x -> Bar' x F
xyybar'lib :: Xyy x -> Bar' x X
bar'barlib :: Bar' x y -> Bar x

Clearly the y is a sort of "phantom type" threaded through all of this, but it remains powerful because given that we want a Bar x we will propagate the need for a Bar' x y and given the need for the Bar' x y we will generate either a Bar' x X or a Bar' x y. So with phantom types and multi-parameter type classes, we get the result we want.

More info: https://www.haskell.org/haskellwiki/GHC/AdvancedOverlap

Answer 4

Adding backtracking would make instance resolution require exponential time, in the worst case.

Essentially, instances become logical statements of the form

P(x) => R(f(x)) /\ Q(x) => R(f(x))

which is equivalent to

(P(x) \/ Q(x)) => R(f(x))

Computationally, the cost of this check is (in the worst case)

c_R(n) = c_P(n-1) + c_Q(n-1)

assuming P and Q have similar costs

c_R(n) = 2 * c_PQ(n-1)

which leads to exponential growth.

To avoid this issue, it is important to have fast ways to choose a branch, i.e. to have clauses of the form

((fastP(x) /\ P(x)) \/ (fastQ(x) /\ Q(x))) => R(f(x))

where fastP and fastQ are computable in constant time, and are incompatible so that at most one branch needs to be visited.

Haskell decided that this "fast check" is head compatibility (hence disregarding contexts). It could use other fast checks, of course -- it's a design decision.