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

[Roman Leshchinskiy]

On Wed, 2006-02-22 at 12:33 +0800, Martin Sulzmann wrote:
> 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

I'm probably misunderstanding something but doesn't this imply that we
cannot declare any instances for

  class C a b | a -> b, b -> a

which do not break the bound variable condition? This would remove one
of the main advantages fundeps have over associated types.

In general, wouldn't it be better to look at *all* visible instance
declarations when they are used instead of looking at each one
individually when it is defined? If the goal is to allow only primitive
recursion, then that would lead to much more permissive rules.

As to the non-termination of GHC's type checker, below is an example
which encodes a stripped-down version of the lambda calculus (with only
one variable) and then evaluates (\x. x x) (\x. x x). Loops nicely with
GHC 6.4.1, but the second Subst instance is invalid under your rule if I
understand correctly.

Roman

----

{-# OPTIONS -fglasgow-exts #-}
data X
data App t u
data Lam t

class Subst s t u | s t -> u
instance Subst X u u
instance (Subst s u s', Subst t u t') => Subst (App s t) u (App s' t') 
instance Subst (Lam t) u (Lam t)

class Apply s t u | s t -> u
instance (Subst s t u, Eval u u') => Apply (Lam s) t u'

class Eval t u | t -> u
instance Eval X X
instance Eval (Lam t) (Lam t)
instance (Eval s s', Apply s' t u) => Eval (App s t) u

x = undefined :: Eval (App (Lam (App X X)) (Lam (App X X))) u => u