[Haskell-cafe] (Un)termination of overloading resolution

[oleg at pobox.com]

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 ()) :: ())