overlapping instances with best-fit overlap resolution are useful because they give us an alternative way to write programs that we cannot write directly as long as current Haskell isn't expressive enough: (a) we can't specify that two types in an instance are not equal; but we can use overlap resolution to ensure that equal types are handled by another, more specific instance (b) we can't enable library users to add instances for their types, yet ensure that there will be some instance for every type; but we can use overlap resolution to provide a default instance, to be overridden by more specific instances in library and user code (c) we can't rely on mutual exclusion properties specified in instance contexts to be used to select the appropriate instance because Haskell only looks at instance heads; but we can sometimes wrap our types in extra constructors so that the mutual exclusion is reflected in more and less specific instance heads, with overlap resolution choosing the right one (this is a real pain, brittle against change, and not always possible..) (d) ..this seems to cover most uses discussed so far, but I don't claim this list to be complete. if you know of examples not covered by a-c, please add them by reply! there hasn't been any enthusiasm about changing (c) for Haskell', which isn't to my liking, but nothing I can do much about. I would, however, like to continue arguing in favour of refining overlap handling until we get at least some progress into Haskell' (and addenda). so I propose to add the something like the following to Haskell': ---------- we know how to handle (a) [no overlap needed]: syntax: permit type inequalities as guards in instance declarations: <topdecls> -> .. | 'instance' [<ctxt> '=>'] <head> [ '|' <ineqs> ] [<body>] <ineqs> -> <typevar> '/=' <type> [ ',' <ineqs>] semantics (sketch): - add inequality guards from an instance as guards to the rules for that instance in the CHR - add inequality guards as attributes to the typevars after successful guard evaluation and rule commit remarks: - we only need the extra guard syntax because of (c) above - we restrict inequalities to variables on lhs to simplify semantics - attributed variables are logic programming folklore: variable attributes are simply goals to be reexamined whenever the attributed variable is instantiated; we need them here to ensure that after we have selected a CHR rule based on an inequality, that inequality is not violated by later instantiations -------------------- we can make (b) more explicit: instead of enabling overlapping instances and overlap resolution on a per-module or per-session basis, we can specify which instances we want to use only as defaults: syntax: <topdecls> -> .. | ['default'] 'instance' [<ctxt> '=>'] <head> [ '|' <ineqs> ] [<body>] semantics (sketch): - default instances may be overridden by more specific instances including other default instances, but no such overlap is permitted unless there is a single most specific instance - default instances only apply if there can be no more specific instances; the easiest way to model this is by collecting all instances for the class, select those that are more specific than some default instance, and add type inequality guards that exclude those instantiations from the rule for the default instance - no other instances are affected by overlap resolution remarks: - by declaring all instances as 'default', we could recover the current, indiscriminate overlap handling; but we hardly ever want that, as declaring default instances allows us to be more precise, limiting the impact of overlap handling - once we have type inequality guards in the language, we can be a bit stricter about ruling out overlaps than GHC is at the moment (see Simon's earlier example) - default instances with ground heads (no variables) can be treated like non-default instances (there can't be any more specific instances) - without further analysis, application of default instances has to be delayed until the whole program is visible; that does not prevent separate compilation, it only prevents early application of some instances (those marked as defaults); in other words, separately compiled modules are parameterized by the set of more specific instances for their default instances - we don't want to go through all that trouble for every instance in every class, which is the motivation for being very specific about where we want overlaps to be permitted and resolved cheers, claus