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

[Mark P Jones]

[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