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