termination for FDs and ATs

[Ross Paterson]

On Tue, May 02, 2006 at 12:26:48AM +0100, Ross Paterson wrote:
> So the MR raises the reverse
> question: can you be sure that every tautologous constraint is reducible?

I think the answer is no.  Consider:

	class C a where
		type Result a
		method :: a -> Result a

	instance C (Maybe a) where {
		type Result (Maybe a) = Bool

	f = \ b x -> if b then Just (method x) else x

The AT algorithm will stop after inferring the following type for f:

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

Since the constraint set is non-empty, this definition will be rejected
by the monomorphism restriction.

However, this constraint set has exactly the same set of solutions as
a = Maybe Bool, which is trivially solvable.  (The corresponding FD
version will reduce to this, thanks to instance improvement.)