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

21 Feb 2006

      This is not a counter-example to my conjecture.
Let's consider the general case (which I didn't
describe in my earlier email).

In case we have an n-ary type function T
(or (n+1)-ary type class constraint T)
the conditions says
for each 

type T t1 ... tn = t

(or rule T t1 ... tn x ==> t)

then rank(ti) > rank(t) for each i=1,..,n

Your example violates this condition
...
class E m a b | m a -> b
  instance E m (() -> ()) (m ())
The improvement rule says:

rule E m (() -> ()) x ==> x=(m ())

but rank m < rank (m ())

Your example shows that the condition

rank(t1)+...+rank(tn) > rank(t)

is not sufficient (but that's not a surprise).

Program text
...
test = foo (\f -> (f ()) :: ()) (\f -> (f ()) :: ())
gives rise to
Foo ((->) (() -> ())) ((() -> ()) -> ())

via
...
instance (E m a b, Foo m b) => Foo m (a->()) where
this constraint reduces to

  E ((->) (() -> ())) (()->()) x
  Foo ((->) (() -> ())) x

the above improvement yields x = (((->) (() -> ()))) ()

this leads to

Foo ((->) (() -> ())) ((((->) (() -> ()))) ())

and so on (the second component is increasing).

So, I'll stick to my claim. I don't think I have time
at the moment to work out the details of my claim/proof sketch.
But if somebody is interested. The following is a good
reference how to attack the problem:
@inproceedings{thom-term,
	author = "T. Fr{\"u}hwirth",
	title = "Proving Termination of Constraint Solver Programs",
	booktitle = "Proc.\ of New Trends in Constraints: Joint {ERCIM/Compulog} Net
		Workshop",
	volume = "1865",
	series = "LNAI",
	publisher = "Springer-Verlag",
	year = "2000"
}

Martin

oleg@pobox.com writes:
...
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 ()) :: ())