[Haskell-cafe] Re: [Haskell] [Fwd: undecidable & overlapping instances: a bug?]

[Martin Sulzmann]

Mark P Jones writes:
 > [Sorry, I guess this should have been in the cafe ...]
 > 
 > Simon Peyton-Jones wrote:
 > > The trouble is that
 > > a) the coverage condition ensures that everything is well behaved
 > > b) but it's too restrictive for some uses of FDs, notably the MTL library
 > > c) there are many possibilities for more generous conditions, but
 > >         the useful ones all seem complicated
 > > 
 > > Concerning the last point I've dumped the current brand leader
 > > for (c) into http://hackage.haskell.org/trac/ghc/ticket/1241#comment:15.
 > > 
 > > Better ideas for (c) would be welcome.
 > 
 > Let's take the declaration:  "instance P => C t where ..."
 > The version of the "coverage condition" in my paper [1] requires
 > that TV(t_Y) \subseteq TV(t_X), for each dependency (X->Y) \in F_C.
 > (I'm using the notation from the paper; let me know if you need more
 > help to parse it.)  This formulation is simple and sound, but it
 > doesn't use any dependency information that could be extracted from P.
 > To remedy this, calculate L = F_P, the set of functional dependencies
 > induced by P, and then expand the right hand side of the set inequality
 > above by taking the closure of TV(t_X) with respect to L.  In symbols,
 > we have to check that:
 > 
 >    TV(t_Y) \subseteq TV(t_X)^+_L, for each (X->Y) \in F_C.
 > 
 > I believe (but haven't formally proved) that this is sound; I don't
 > know how to make a more general "coverage condition" without losing
 > that.  I don't know if it's sufficient for examples like MTL (because
 > I'm not sure where to look for details of what that requires), but
 > if it isn't then I'd be very suspicious ...
 > 
 > All the best,
 > Mark
 > 
 > [1] http://www.cs.pdx.edu/~mpj/pubs/fundeps-esop2000.pdf


I think the above is equivalent to the (refined) weak coverage
condition in [2] (see Section 6, p26). The weak coverage condition
give us soundness. More precisely, we obtain confluence from which we
can derive consistency (which in turn guarantees that the type class
program is sound).

*BUT* this only works if we have termination which is often very
tricky to establish.

For the example,

> class Concrete a b | a -> b where
>         bar :: a -> String
> 
> instance (Show a) => Concrete a b

termination holds, but the weak coverage condition does *not*
hold. Indeed, this program should be therefore rejected.

Martin