Interesting non-terminating behaviour for recursive classes

[Ralf Laemmel]

Hi Simon and others,

this is an interesting feature.
The three attached files are largely the same.
They don't do too weird stuff except a little bit 
instance-constraint-level recursion among classes.
(and some use of undecidable instances ...)

(There are embedded comments in the files.)

(I used GHC HEAD as of now.)

LoopOfTheDay1.hs really works great.
I was surprised that this works (because hugs' type checker
encounters cut-off limit, likewise for GHC 6.2).
But GHC HEAD seems to try harder in the area of termination checking for 
instance compilation and instance selection.

LoopOfTheDay2.hs does a very minor variation,
but type checking does not terminate anymore.
To me this looks like a real bug.
(Yes, I have enabled undecidable instances but the variation
point does not introduce any challenge whatsoever as far as I can see.)

LoopOfTheDay3.hs again does a minor variation.
Type checking the set of classes and instances works again,
but trying to use the classes leads to non-terminating instance selection.

I have a truly cool application for this in case it can be made work 
more generally.

Thanks for looking into it!
Regards,
Ralf

-------------- next part --------------
{-# OPTIONS -fglasgow-exts #-}
{-# OPTIONS -fallow-undecidable-instances #-}

-- Compiles fine.
-- Instance selection works fine.
-- try: :t foo (T1b T1a)

-- Notice: T1 is a recursive type.
-- Notice: the classes are recursive, too.
-- Why does this work when almost the same thing doesn't?
-- Say: adding an Int component to T1a makes things loop.
-- See LoopOfTheDay2.hs and LoopOfTheDay3.hs.

data T1 = T1a | T1b T1

class C0 x where foo :: x -> (); foo = undefined
class C1 x y
class C1 x y => C2 x y

instance C0 T1              => C1 () T1
instance (C1 x T1)          => C2 x T1
instance C2 () T1           => C0 T1
-------------- next part --------------
{-# OPTIONS -fglasgow-exts #-}
{-# OPTIONS -fallow-undecidable-instances #-}

-- Compilation loops!
-- While LoopOfTheDay1.hs did compile and work,
-- this one loops during compilation, even though
-- there is only an innocent difference regarding T1,
-- i.e., an additional, non-recursive constructor component.

data T1 = T1a Int | T1b T1

class C0 x where foo :: x -> (); foo = undefined
class C1 x y
class C1 x y => C2 x y

instance C0 Int              => C1 () Int
instance C0 T1               => C1 () T1
instance (C1 x T1, C1 x Int) => C2 x T1
instance C1 x Int            => C2 x Int
instance C2 () T1            => C0 T1
instance C2 () Int           => C0 Int
-------------- next part --------------
{-# OPTIONS -fglasgow-exts #-}
{-# OPTIONS -fallow-undecidable-instances #-}
{-# OPTIONS -fallow-overlapping-instances #-}

-- Compiles fine but instance selection loops.
-- try: :t foo (T1a 1)
-- This is essentially the same as LoopOfTheDay2.hs
-- but with the innocent (?) use of overlapping instances.

data T1 = T1a Int | T1b T1

class C0 x where foo :: x -> (); foo = undefined
class C1 x y
class C1 x y => C2 x y

instance C0 a                => C1 () a
instance (C1 x T1, C1 x Int) => C2 x T1
instance C1 x Int            => C2 x Int
instance C2 () a             => C0 a