On Wed, Apr 18, 2007 at 05:10:27PM +0100, Neil Mitchell wrote:
I have now reduced this bug to a smallish test case:
test :: T1 -> T1 test = test2
test2 :: C3 (T2 a) a => a -> a test2 = undefined
data T1 = C1 deriving Show data T2 a = T2 a deriving Show
class C1 a where class C2 a where class C3 a b where
instance C1 T1 where instance C1 a => C1 (T2 a) where instance (C1 a, C2 a) => C3 T1 a where instance (C3 a (T2 a)) => C2 (T2 a) where instance (C2 (T2 a)) => C3 (T2 a) b where
In Hugs I get (overlapping instances and unsafe overlapping instances turned on):
*** The type checker has reached the cutoff limit while trying to *** determine whether: *** C1 T1 *** can be deduced from: *** ()
The explicit instance for this type makes it surprising that it fails to find an instance.
The error message is silly, but there really is a loop here: C3 (T2 T1) T1 <= C2 (T2 T1) <= C3 T1 (T2 T1) <= C2 (T2 T1)
In GHC with -fglasgow-exts -fallow-undecidable-instances, it works fine.
That's because recent GHCs detect the loop when they get to an identical constraint, and declare the constraint solved. Simon calls this feature recursive dictionaries; Martin Sulzmann calls it co-induction. I can't find where it's documented in the GHC User's Guide, though. Hugs does not aim to duplicate that behaviour; the bug here is the error message. Here's a simpler illustration of it: class C a where f :: a -> a instance (Eq a, C a) => C a test = f True with -98 says it can't prove Eq Bool, when it should say C Bool.