Weird Undecidable Instances Bug

[Simon Peyton-Jones]

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

When dealing with the defn of g, the context simplifier tries to deduce

	(F a b, D b (T r))  |-  (F a b', D b' (T r))

The stuff on the left (the "given" context) comes from the type sig, the
stuff on the right (the "wanted" constraints) comes from the call to
'f', suitably instantiated.  Notice that b and b' are not (yet) unified.

Next, the simplifier tries to apply instance declarations and
equalities, so it simplifies

	F a b', D b' (T r)  ===>   F a b', C (T r)

Next, it applies functional dependencies, which unifies b:=:b'.  But
it's too late!  It now thinks it needs C (T r) and that's what it
complains about.

You might think the solution is to apply the functional dependencies
*first*; then we could get D b (T r) from the given context, rather than
using the instance decl.

But in general we might need to *first* apply some instance
declarations, and *then* apply functional dependencies.  For example,
suppose that instead of (F a b') in the "needed" set, we had X (V a) b',
plus an instance decl
	instance F a b => X (V a) b
Then we'd need to apply this instance decl before the functional
dependency in F's class decl is exposed.

So, how do we decide to apply the X instance decl before the D instance
decl??


Another approach might be this: if any functional dependencies kick in,
perform the unifications and then start again from scratch.  But that
doesn't work either. 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).


The bottom line is this: I don't know a confluent solver in the case
where a type signature has a non-simple context (the type sig for g had
the context (D b (T r)), to which an instance declaration applies).  I
guess one possibility might be to make such an instance decl illegal.  


The combination of 
	multi-parameter type classes
	undecidable instances
	functional dependencies
	type sigs with non-simple contexts
makes it difficult to design a confluent solver.  Martin S may have
ideas about what restrictions would make it confluent.  

Simon


| -----Original Message-----
| From: glasgow-haskell-bugs-admin at haskell.org
[mailto:glasgow-haskell-bugs-admin at haskell.org] On
| Behalf Of Ashley Yakeley
| Sent: 08 September 2003 02:24
| To: glasgow-haskell-bugs at haskell.org
| Subject: Weird Undecidable Instances Bug
| 
| This fails to compile. Oddly enough, if you remove the instance
| declaration (1), or if you remove the r parameter to T, or if you do
any
| of the other simplifications I've tried, it compiles successfully.
| 
| -- ghc -fglasgow-exts -fallow-undecidable-instances -c WeirdInsts.hs
| module WeirdInsts where
|     {
|     data T r = MkT;
| 
|     class C t;
| 
|     class D b t;
| 
|     instance (C (T r)) => D b (T r); -- (1)
| 
|     class F a b | a -> b;
| 
|     f :: (F a b,D b t) => (a,t);
|     f = undefined;
| 
|     g :: (F a b,D b (T r)) => (a,T r);
|     g = f;
|     }
| 
| $ ghc -fglasgow-exts -fallow-undecidable-instances -c WeirdInsts.hs
| 
| WeirdInsts.hs:18:
|     Could not deduce (C (T r)) from the context (F a b, D b (T r))
|       arising from use of `f' at WeirdInsts.hs:18
|     Probable fix:
|         Add (C (T r)) to the type signature(s) for `g'
|         Or add an instance declaration for (C (T r))
|     In the definition of `g': g = f
| 
| $ ghc --version
| The Glorious Glasgow Haskell Compilation System, version 6.0.1
| 
| --
| Ashley Yakeley, Seattle WA
| 
| _______________________________________________
| Glasgow-haskell-bugs mailing list
| Glasgow-haskell-bugs at haskell.org
| http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs