overlapping instances and constraints

[Claus Reinke]

[
 I'll only address some of your issues in this message, as they fall nicely
 under the use of a feature I'd like to see anyway: 
     type disequality constraints
]

>- A program that type checks can have its meaning changed by adding an
>instance declaration
>- Similarly adding "import M()" can change the meaning of a program (by
>changing which instances are visible

yes, these are consequences of the "start with overlapping declarations, 
then avoid overlapping instances by selecting the most specific declaration".

we could avoid that, by using disequality constraints, as some other 
constraint logic systems have done. that way, for many examples, there 
wouldn't be any overlapping instances in the first place:

    class C a where c :: a -> String
    instance C [a]     | a/=Char where c as  = .. -- dealing with most lists
    instance C String                where c s = ..   -- special case for strings

[note that the special syntax for disequality constraints (borrowing from 
 FDs) here is only needed as long as instance contexts are ignored;
 otherwise, type disequality would just be a built-in binary type class,
 and the instance would look like this:
     instance (a/=Char) => C [a] where c as = ..
]

we could now rule out any overlapping instance declarations, while
still permitting instance declarations covering the gaps left by the
disequality constraints.

this should work well for uses of overlapping instances as local conditionals,
but it would rule out the popular pattern of extensible type case with default
rule. the latter explicitly depends on specifying a default instance that may
be replaced by more specific instances in future modules.

so we can avoid these issues for some use cases, and that may be worth
trying out as a first step, but if we want all use cases, it seems we will have
to live with those consequences.

>- When exactly is overlap permitted?  Is this ok?
>instance C a Int
>instance C Bool b
>Previously GHC rejected this, on the grounds that it could be ambiguous
>when you came across (C Bool Int).  But not GHC accepts it, on the
>grounds that (C Bool Char) is quite unambiguous.  

again, a consequence of the best-match rule. but note that in examples
like this, there are two "levels" of overlap: the first level is resolved by
the best-match rule, the second _remains_ overlapping. so GHC is faced
with the choice of rejecting the declarations outright because they _might_
run into this overlap, or to wait and see whether they _will_ run into it.

this could actually be cured by using disequality constraints:

    instance C a Int | a/=Bool
    instance C Bool b | b/=Int
--    instance C Bool Int         -- we can declare this if we want it

even without ruling out overlapping instance declarations, this excludes
the problematic case while permitting the unproblematic ones.

just as unification allows us to prefer specific type instances, disequality
allows us to avoid specific type instances, so we would be able to state
_only_ the first, resolvable, level of overlap in this example, without
having to deal with the by-product of the second, unresolvable, and
therefore possibly erroneous level of overlap.

the other issues you raise are just as important, but won't be addressed
as easily, so I leave them for later (and possibly for others;-).

cheers,
claus

ps I don't know whether additional references are helpful or needed,
    but google for "disequality constraints" or for "disunification" (see
    also "constructive negation").