[Hugs-users] Re: Constraint depth cut off

[Ross Paterson]

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.