| 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. Actually, it won't. The spec just says that the function is monomorphic in 'a'. That is, 'a' can be instantiated only one way. So if f is called, say (f True True), then that fixes 'a' to be Bool and all is well. Only if f is exported (with no calls inside the module) will the program be rejected, and even then it'll be rejected on the grounds that 'a' is ambiguous. But these are details. Your general point is well taken: the FD improvement rule will infer f :: Bool -> Bool -> Bool without seeing any calls. Simon