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

[Simon Peyton-Jones]

Good point Mark!  And yes, the bug is still open Iavor.

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.

Simon

| -----Original Message-----
| From: Iavor Diatchki [mailto:iavor.diatchki at gmail.com]
| Sent: 17 October 2007 19:19
| To: Mark P Jones
| Cc: Simon Peyton-Jones; Haskell users; Tom Schrijvers; Martin Sulzmann
| Subject: Re: [Haskell] [Fwd: undecidable & overlapping instances: a bug?]
|
| Hi,
| Mark is quite right, and there is a bug report that documents the problem:
| http://hackage.haskell.org/trac/ghc/ticket/1241
| The trac ticket is targeting GHC 6.8 but the ticket is still open.  I
| have not had a chance to try out any of the 6.8 release candidates
| yet, so I am not sure if there have been changes in this area.
| -Iavor
|
| On 10/17/07, Mark P Jones <mpj at cs.pdx.edu> wrote:
| > Simon Peyton-Jones wrote:
| > > | I am quite intrigued at the behaviour examplified in the attached
| module.
| > > | It's true I am a newbie and probably don't quite get the whole
| consequence
| > > | spectrum of -fallow-undecidable-instances, but why providing that dummy
| > > | instance (commented out) get the thing to compile?
| > >
| > > Sorry I must have missed this.  It's a nice example of the trickiness of
| > > functional dependencies.  Here's what is happening.  First a very cut-
| down
| > > version of your example:
| > >
| > > class Concrete a b | a -> b where
| > >         bar :: a -> String
| > >
| > > instance (Show a) => Concrete a b
| > >
| > > wib :: Concrete a b => a -> String
| > > wib x = bar x
| > >
| > > Now consider type inference for 'wib'. ...
| >
| > Hold on a second!  There's a more serious problem here, before we
| > get to 'wib'.  The definition of class Concrete asserts that there
| > is a dependency from a to b.  In other words, it promises that, for
| > any a, there must be at most one b such that Concrete a b holds.
| > But then the following instance declaration says that Concrete a b
| > can be instantiated for *any* a and b, the only proviso being that a
| > is an instance of Show.  In particular, there is no functional
| > relationship between the parameters.  As such, these two
| > declarations are in direct conflict with one another!  To quote the
| > error message that Hugs produces, the "Instance is more general than
| > a dependency allows".
| >
| > I thought this must be a typo in your email, but then I discovered
| > that the ghci (6.6.1) installed on my machine accepts this code, at
| > least once the Concrete Bool Bool instance was added.  If the
| > instance declarations are not consistent with the functional
| > dependency, then improvement is unsound, and all bets are off!
| >
| > Further experiments suggest that this behavior occurs only when
| > the-fallow-undecidable-instances flag is specified.  But the reason you
| > need to check for consistency between instance declarations and
| > dependencies is to ensure soundness, not decidability.
| >
| > I don't know if this was the problem in the original example, but
| > perhaps we should debug this cut down version first :-)
| >
| > All the best,
| > Mark
| >
| > _______________________________________________
| > Haskell mailing list
| > Haskell at haskell.org
| > http://www.haskell.org/mailman/listinfo/haskell
| >