Hi Anthony, This conversation has become deeply mysterious to me. I understand that you're revisiting arguments on the structuring of conditionals that were tried and discarded in the 70s; what I don't understand is why you need to repeatedly mischaracterize my work to do so. For one example, I have no idea why you make the following claim:

Nevertheless, I can only write one Instance Chain per class. So I can't (say in another module) introduce a new datatype with instances.

The instance chains paper is quite explicit in ruling out this interpretation; when introducing the notion of chains, we wrote: In ilab, a class can be populated by multiple, non-overlapping instance chains, where each chain may contain multiple clauses (separated by the keyword else). For another, you give a fanciful description of the problems that might arise in implementing instance chains, including:

There's a persistent problem for the compiler testing for type equality: the usage sites must have the types grounded. It's often more successful to prove disequality.

and also:

I suspect that for the compiler, Instance Chains will be as problematic for type inference as with Closed Type Families: CTFs have a lot of searching under the covers to 'look ahead' for equations that can safely match.

Luckily, both instance chains and closed type families have formalizations that can be checked to evaluate these claims. In neither case do we find either equality limited to ground types or anything that should be construed as 'look ahead'. Perhaps you're trying to refer to the use of infinitary unification in checking apartness (but not in checking equality) for closed type families? Here again, not only is there no use of or need for infinitary unification with instance chains, but I discussed this difference and its consequences in my 2015 paper. Finally, you make various claims about what is and is not a solution to the expression problem which have no apparent relationship to any of the existing work on the expression problem or its encodings. The point of Swierstra's encoding is that you can give a complete definition of the interpretation of (right-recursive) coproducts, and that doing so is sufficient to encode extensible variants. The downside to his approach is that each new elimination of an extensible variant must itself be defined via a new type class. Subsequent work by Bahr, Oliveira et al., and myself, has lifted this restriction in various ways. At no point in any of these encodings is it in any sense necessary or desirable to extend existing instances for the coproduct, and so there is no reason to imagine that using either instance chains or closed type families would be any obstacle to implementing them. Again, this is all laid out, with examples, in my 2015 paper. /g