| I have not followed this completely, but do these new rules now allow: | | class F a b c where | f: a -> b -> c | | instance F a a a where Ross's proposal would allow that. Ignore functional dependencies for the moment. To force instance inference to terminate we need the context of the instance declaration to be "smaller" than the head. Otherwise you can get instance Foo [a] => Foo a One way to do that is to require (a) only type variables in the context (b) at least one non-type-variable as a type-class arg in the head Thus instance Foo a => Foo [a] satisifies (b) because [a] is not a type variable. This check is wildly conservative. One can ensure that things get smaller with something weaker, as Ross suggests. And that would be useful, because it'd provide a machine check of termination (necessarily still approximate), which is better than -fallow-undecidable-instances. However matters get significantly more complicated with fundeps. For example (a) and (b) are not enough. Whether Ross's suggestion guarantees termination when we have fundeps I am not sure Simon