Overlapping, undecidable, incoherent -- or worse?

[Alex Ferguson]

On Thu, May 20, 2004 at 08:52:45AM +0100, Simon Peyton-Jones wrote:
| You don't say what you are trying to achieve.  However it looks as if
| you mean "If you want PO T, for some type T, first try (Bounded T, Enum
| T, SemiRing T) and if that fails try CSemiRing T.  Or maybe the other
| way round.

Sorry, I suppose I was a little gnomic.  I mean the other way round,
ideally.  The difference in the remainder of the contexts isn't
significant for my purposes, so I could as well have (some redundantly)
made the latter declaration:

> instance (Bounded a, Enum a, CSemiRing a) => PO a where
>         a |= b = a + b == b

which'd make it strictly more specific than the other.  i.e. if it's a
CSemiRing, use that, if not but is (only) a semiring If that'd
help at all...

 
| In any case, GHC simply does not implement this kind of backtracking
| search.  It would make sense, and some of the more exotic users of type
| classes would like it, but (a) there are numerous tricky corners, and
| (b) it's awkward to implement the way GHC is now.  If the specification
| was completely clear I might be tempted to fix (b), but it isn't.  The
| main difficulty is that a compiler does not solve constraints "all at
| once".  Instead it does a bit of solving, then then a bit more later.
| If the "later" part doesn't pan out, it's jolly difficult to go back to
| the original part (in another module, perhaps) and change it. 

I can see the possible difficulties all right.  Well, enough of them for
it to seem...  difficult.  I'd think this would be relatively easy to do
if Haskell had some notion of 'naming' instance declarations, and then
of specifying a 'priority' to 'em, but that'd by a pretty significant
looking language extension.  I'd just gotten the impression that
-fallow-incoherent-instances might make some ad hoc 'forcing' choice in
such circumstances that might serve my current purposes.

 
> As a trivial example, try
> 
> 	f a = a |= a
> 
> What type shall we infer for f?  
> 	f :: (Bounded a, Enum a, SemiRing a) => a -> a
> or
> 	f :: (CSemiRing a) => a -> a

I'm with Stefan on this one.  Surely the type is simply PO a => a ->
Bool?  Or is there a 'top level binding' issue here?  (Surely not, the
MR doesn't apply.)

Cheers,
Alex.