termination for FDs and ATs

[Simon Peyton-Jones]

| The important question is whether this will retain *complete* type
| inference? For example, in case of type annotations we need to
| test for equivalence among constraints.

An excellent question.  Here's an example, adapted from Ross:

	class C a where
		type Result a
		method :: a -> Result a
	
	instance C (Maybe a) where 
		type Result (Maybe a) = Bool
	
	g :: (a->a) -> Int
	g f = 3

	w ::Int
	w = g (\b x -> if b then Just (method x) else x)

Now, as Ross pointed out, the (\b x->...) expression has inferred type

	(a = Maybe (Result a), C a) => Bool -> a -> a

Alas, g simply discards its argument, so there are no further
constraints on 'a'.  I think Martin would argue that type inference
should succeed with a=Bool, since there is exactly one solution.  Is
this an example of what you mean?  

However, as a programmer I would not be in the least upset if inference
failed, and I was required to add a type signature.  I don't expect type
inference algorithms to "guess", or to solve recursive equations, and
that's what is happening here. (Notice that it's quite hard to set up
this problem. First you need a program whose equality constraints become
recursive.  Then you need to arrange that the type variables in the
recursion are not mentioned elsewhere -- if they were, they'd be
instantiated there, and everything would be ok.)

What I am less sure of is how to *specify* the type system so that it
describes these hard-to-infer programs as illegal.  Presumably it's a
question of setting up the entailment system so that it has limited
rules of deduction -- more limited than first order logic.

Simon