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

[Mark P Jones]

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