TypeFamilies vs. FunctionalDependencies & type-level recursion

[oleg at okmij.org]

Let me see if I understand the different points of view. You advocate
keeping Overlapping Instances, with changes to instance resolution
algorithm. I advocate abolishing Overlapping Instances,
claiming it results in no loss of expressiveness. In my approach, the
changes in GHC are minor (essentially bug fixing and a matter of
pretty-printing), not involving the algorithms of instance
resolution. Incidentally, I have advocated abolishing Overlapping
Instances in a short presentation at the 2004 Haskell Workshop (almost
immediately after Ralf's HList talk).

> Selecting instances based on inequalities is already implemented in
> GHC and Hugs.  (And has been successfully used for over a decade.)
> You've used it extensively yourself in the HList work, and much other
> type-level manipulation (such as IsFunction).

I'm glad you mentioned Hugs. Indeed, Hugs implements overlapping
instances, and indeed _some_, simple code using overlapping
instances work the same way in GHC and Hugs. However, HList in
full does not work in Hugs; while investigating the matter we have
found many dark corners of the Overlapping Instances
implementation in Hugs; Ralf has even found an example where the order of
the constraints within a type mattered. After that we just abandoned
Hugs. This fact constructively proves that implementation of
overlapping instances is tricky; since there is no meta-theory, it is
even hard to tell what is right.

I don't think Overlapping Instances will be in Haskell' any time soon
since there are doubts about the soundness. Overlapping
instances are clearly unsound with type functions. Whether they are
sound with functional dependencies is not clear, but there are warning
signs:

	http://www.haskell.org/pipermail/haskell-cafe/2010-July/080043.html

Please see the whole discussion on Haskell-Cafe in July 2010.

> I think this could be implemented under the new OutsideIn(X)
> type inference:
I should point out the need to extend the type inference algorithm
(and prove that the extension is sound) on your point of view. My
proposal does not affect the instance resolution algorithm at all.


> I take it the Northern hemisphere is now on academic summer holidays.
Generally, yes. I wish I had a holiday though...