On Fri Jun 2 17:35:35 UTC 2017, J. Garrett Morris wrote:

...

On Fri, Jun 2, 2017 at 2:34 PM, Anthony Clayden wrote: 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.

Then I'm sorry Garrett, but if any of those refs are intended to be talking about inequality guards, it's so oblique as to have failed to communicate. In particular, you fail to mention them in your dissertation §7.1, first bullet. Example: "The first challenge is to develop a method to represent negative syntactic constraints on types. For example, in the following instance chain

instance C (Maybe t) else C t

"the second clause can only apply to types that are not of the form Maybeτ for some type τ. To pursue this approach, we would need to develop representations and proof rules for such limitations on the instantiation of type variables." I would write that non-Maybe instance as:

instance C t | t /~ (Maybe _) -- underscore = anonymous

I guess instance chain:

else C t fails if t == (Maybe tau) -- but that must not introduce typevar `tau` to the environment.

The S&S CHR approach did "develop proof rules" to type inequalities (according to the 2002 paper). An explicit inequality guard makes it easy to test whether two instances are apart.

My Hackage survey ("Using Hackage to inform language design", Haskell 2010) discovered that 85% of overlapping instances were contained within the same module, ...

Well of course they are! Putting overlapping instances in separate modules is disastrous, everybody knows that. There's a thorough write-up from SPJ here https://mail.haskell.org/pipermail/haskell-cafe/2010-July/080043.html That does not prove people _want_ to restrict the instances to a single module. They have no choice in practice. So I'm surprised there's as much as 15% of overlapping instances in separate modules. I shudder at the incoherence. If you surveyed a joinery and found everything held together with nails, that would reflect only that there were no screwdrivers on the premisses.

motivating the formalization of that usage pattern with instance chains.

No. I would say (to both Instance Chains and Closed Type Families/Classes): motivating to support something less restrictive. Viz the ability to write stand-alone instances, that can be verified to not overlap (taking guards into account), same approach as the classes in the standard libraries. (Note how the monad transformers library was re-architected, to avoid the dangers of importing overlaps.) AntC