instance inference

[Simon Peyton-Jones]

| 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