overlapping instances and constraints

[Claus Reinke]

>>- Haskell would need to be a lot more specific about exactly where
>>context reduction takes place.  Consider
>>f xs x = xs == [x]
>>Do we infer the type (Eq a) => [a] -> a -> Bool?  Thereby committing to
>>a particular choice of instance?  Or do we (as GHC does) infer the type
>>(Eq [a]) => [a] -> a -> Bool, so that if f is applied at (say) type
>>Char, then an instance Eq [Char] instance would apply.  GHC is careful
>>to do the latter.

is there actually anything unusual about this example? you're saying that
there are at least two instances for Eq:

    instance Eq a => Eq [a]
    instance Eq [Char]

and best-fit overlap resolution demands that we never apply the first if
the second fits, too. we just can't apply any rules unless we have established
that there are no more specific rules.

GHC enables overlap resolution on a pre-module basis, Hugs on a per-session
basis, so this means that we can never apply any rules unless they have ground
heads (no variables), or we've seen the whole program. which is somewhat of
an obstacle, suggesting that we would want to be more specific about enabling
overlap resolution, and use any trick we know to figure out when we no longer
have to wait for further, more specific instances (or be content to delay most 
of instance inference to the compilation of Main).

in "functional logic overloading", POPL 2002, Neubauer et al suggested to
enable overlap resolution on a per-class basis, which seems sensible. even
enabling overlap on a per-instance basis might be worth looking into (that 
is, we would annotate those non-ground instance declarations which we 
want to be allowed to be overridden by more specific declarations 
elsewhere). with such finer control, all unannotated instances/classes 
might become fair game for earlier rule applications.

we can further limit the scope of overlaps by using the module system
to close a set of class instances (this is useful independent of overlaps,
as it allows us to infer when there will be no instance for a given 
constraint): a set of instances for a class is closed if the class is neither 
exported nor imported, and if, for any instances with instance contexts, 
the context constraints are closed as well. [if the class isn't available 
outside this module, there can't be any direct instances outside, and 
if the instance context constraints are closed as well, there can't be 
any indirect instances generated from outside (*)]. 

of course, simply annotating a class or class export as "closed", and
letting the compiler ensure that there are no further direct instances, 
would be somewhat simpler. I'm not sure what to do about further
indirect instances in this case?

cheers,
claus

(*) what do I mean by indirect instances:
    module A () where { class Closed a; instance X a => Closed a}
    module B where { import A; instance X t }
    even if Closed is not exported, creating instances for X indirectly
    creates instances for Closed.