[Haskell-cafe] (Un)termination of overloading resolution
oleg at pobox.com
oleg at pobox.com
Tue Feb 21 22:13:17 EST 2006
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 ()) :: ())
More information about the Haskell-Cafe
mailing list