[Haskell-cafe] Re: coherence when overlapping?

[oleg at pobox.com]

> But I am still confused by the exact definition of coherence in the case of
> overlapping. Does the standard coherence theorem apply? If yes, how?
> If no, is there a theorem?

Yes, the is, by Martin Sulzmann et al, the Theory of overloading (the
journal version)
	http://www.comp.nus.edu.sg/~sulzmann/ms_bib.html#overloading-journal

A simple intuition is this: instance selection may produce more than
one candidate instance. Having inferred a polymorphic type with
constraints, the compiler checks to see of some of the constraints can
be reduced. If an instance selection produces no candidate instances,
the typechecking failure is reported. If there is exactly one
candidate instance, it is selected and the constraint is removed
because it is resolved.  An instance selection may produce more then
one candidate instance. Those candidate instances may be incomparable:
for example, given the constraint "C a" and instances "C Int" and "C
Bool", both instances are candidates. If such is the case, the
resolution of that constraint is deferred and it `floats out', to be
incorporated into the type of the parent expression, etc. In the
presence of overlapping instances, the multiple candidate instances
may be comparable, e.g. "C a" and "C Int".  The compiler then checks
to see if the target type is at least as specific as the most specific
of those candidate instances. If so, the constraint is reduced;
otherwise, it is deferred.  Eventually enough type information is
available to reduce all constraints (or else it is a type error).