Weird Undecidable Instances Bug

[Martin Sulzmann]

Simon said

> This is a tricky one.  Here's what is going on.

I believe there's nothing tricky going on.

Your type annotation 

g :: (F a b,D b (T r)) => (a,T r)
g = f

is simply incorrect. Keep in mind that GHC does NOT improve
type annotations. For example,

g :: (F a b, C (T r)) => (a,T r)
g = f

type checks.
(I "replaced" D b (T r) by C (T r) )

I understand that it might sound reasonable to accept

g :: (F a b,D b (T r)) => (a,T r)
g = f

Indeed, depending on how we define subsumption among
type schemes

forall a b t. (F a b,D b t) => (a,t)   -- inferred

 "subsumes"

forall a b r. (F a b,D b (T r)) => (a,T r)  -- annotated

wrt the instance and FD.

However, for GHCs evidence translation scheme we need a more
restrictive subsumption check (because GHC never "improves"
user-provided type annotations).


 > > Consider an instance decl like:
 > > 	instance (Lte a b l,If l b a c) => Max a b c
 > > (This is a real example.)   Notice that "l" is used on the LHS of the 
 > > => but not the RHS.  The idea is that "l" will get unified by a 
 > > functional dependency.   But if such a unification re-starts the 
 > > solving process from scratch, we just get into an infinite loop (apply 
 > > instance decl, apply fds, unify, start again, apply instance decl 
 > > again, etc).
 > 

Well, there might not be any immediate problem here.
The only danger with

instance (Lte a b l,If l b a c) => Max a b c

is that we need to uniquely determine l given a, b and c.
(If we can't then type inference (i.e. subsumption checking) might
become incomplete)

However, if there's a FD such as

class Lte a b l | a b -> l

then things should work out. We only get into trouble in case we
find

instance Lte a b l => Lte [a] [b] [l]

By trouble I mean, type inference might become undecidable.

To conclude,

class Max a b c
class Lte a b l | a b -> l
class If l b a c
instance (Lte a b l,If l b a c) => Max a b c

is safe (i.e. type inference is sound and decidable).

Things become unsafe if we add

instance Lte a b l => Lte [a] [b] [l]

Why and how to fix this problem is subject of current investigations.
Will let you know once a readable version is available.

Martin