On Fri, Jun 2, 2017 at 2:34 PM, Anthony Clayden
Although your papers/Dissertation cite some of S&S's work, you seem unaware of type disequality guards.
Of course we were aware of inequality guards. They are a special case of the observation in §2.3 of the instance chains paper about unifying but non-overlapping instances; §7 of that paper and §7.1 of my dissertation discuss extending the formal treatment to accept such instances. My Hackage survey ("Using Hackage to inform language design", Haskell 2010) discovered that 85% of overlapping instances were contained within the same module, motivating the formalization of that usage pattern with instance chains.
We can express Russell's paradox:
else f :<: g fails if f :<: g
This is not Russell's paradox, as the lack of set comprehensions in the near vicinity might have suggested. At best, it highlights an incompleteness in the deduction algorithm given in the 2010 paper (from a ⇒ ¬a, we would hope to conclude ¬a). But then, I never claimed completeness.
Haskell very strictly doesn't support instance contexts driving selection of instances. That is confusing for newbies, but it's for very good decidability reasons.
Haskell instance selection is decidable by induction on the number of type constructors in an entailment; if you apply the same restriction to instance chains (i.e., that there be more constructors in the conclusion of an instance than in its hypotheses), you get exactly the same decidability results. There are, of course, less restrictive conditions that would also guarantee decidability, but that is not the point. /g -- Prosperum ac felix scelus virtus vocatur -- Seneca