Martin Sulzmann wrote:
- The type functions are obviously terminating, e.g. type T [a] = [[a]] clearly terminates. - It's the devious interaction between instances/superclasss and type function which causes the type class program not to terminate.
Is there a possible fix? Here's a guess. For each type definition in the AT case
type T t1 = t2
(or improvement rule in the FD case
rule T1 t1 a ==> a=t2
we demand that the number of constructors in t2 is strictly smaller than the in t1 (plus some of the other usual definitions).
I'm afraid that may still be insufficient, as the following counter-example shows. It causes GHC 6.4.1 to loop in the typechecking phase. I haven't checked the latest GHC. The example corresponds to a type function (realized as a class E with functional dependencies) in the context of an instance. The function in question is class E m a b | m a -> b instance E m (() -> ()) (m ()) We see that the result of the function, "m ()" is smaller (in the number of constructors) that the functions' arguments, "m" and "() -> ()" together. Plus any type variable free in the result is also free in at least one of the arguments. And yet it loops. {-# OPTIONS -fglasgow-exts #-} -- Note the absence of the flag -fallow-undecidable-instances module F where class Foo m a where foo :: m b -> a -> Bool instance Foo m () where foo _ _ = True instance (E m a b, Foo m b) => Foo m (a->()) where foo m f = undefined class E m a b | m a -> b where tr :: m c -> a -> b -- There is only one instance of the class with functional dependencies instance E m (() -> ()) (m ()) where tr x = undefined -- GHC(i) loops test = foo (\f -> (f ()) :: ()) (\f -> (f ()) :: ())