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.)